{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Relation.Binary.Properties.Setoid where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Composition
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Relation.Binary.Properties.Setoid._._≉_
d__'8777'__18 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny -> AgdaAny -> ()
d__'8777'__18 :: T_Level_18
-> T_Level_18 -> T_Setoid_46 -> AgdaAny -> AgdaAny -> T_Level_18
d__'8777'__18 = T_Level_18
-> T_Level_18 -> T_Setoid_46 -> AgdaAny -> AgdaAny -> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Setoid.isPreorder
d_isPreorder_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_isPreorder_38 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_IsPreorder_76
d_isPreorder_38 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 = T_Setoid_46 -> T_IsPreorder_76
du_isPreorder_38 T_Setoid_46
v2
du_isPreorder_38 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_isPreorder_38 :: T_Setoid_46 -> T_IsPreorder_76
du_isPreorder_38 T_Setoid_46
v0
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_76)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsPreorder_76
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46 AgdaAny
forall a. a
erased
         AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased)
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
         (T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_reflexive_42
           ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0))
           AgdaAny
v1)
      ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
         ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0)))
-- Relation.Binary.Properties.Setoid.≈-isPreorder
d_'8776''45'isPreorder_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_'8776''45'isPreorder_40 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_IsPreorder_76
d_'8776''45'isPreorder_40 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2
  = T_Setoid_46 -> T_IsPreorder_76
du_'8776''45'isPreorder_40 T_Setoid_46
v2
du_'8776''45'isPreorder_40 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_'8776''45'isPreorder_40 :: T_Setoid_46 -> T_IsPreorder_76
du_'8776''45'isPreorder_40 T_Setoid_46
v0
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_76
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
      ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny
v3))
      ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
         ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0)))
-- Relation.Binary.Properties.Setoid.≈-isPartialOrder
d_'8776''45'isPartialOrder_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
d_'8776''45'isPartialOrder_42 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_IsPartialOrder_248
d_'8776''45'isPartialOrder_42 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2
  = T_Setoid_46 -> T_IsPartialOrder_248
du_'8776''45'isPartialOrder_42 T_Setoid_46
v2
du_'8776''45'isPartialOrder_42 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
du_'8776''45'isPartialOrder_42 :: T_Setoid_46 -> T_IsPartialOrder_248
du_'8776''45'isPartialOrder_42 T_Setoid_46
v0
  = (T_IsPreorder_76
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
      T_IsPreorder_76
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.C_constructor_294
      ((T_Setoid_46 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_46 -> T_IsPreorder_76
du_'8776''45'isPreorder_40 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
-- Relation.Binary.Properties.Setoid.preorder
d_preorder_48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_preorder_48 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Preorder_142
d_preorder_48 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 = T_Setoid_46 -> T_Preorder_142
du_preorder_48 T_Setoid_46
v2
du_preorder_48 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_preorder_48 :: T_Setoid_46 -> T_Preorder_142
du_preorder_48 T_Setoid_46
v0
  = (T_IsPreorder_76 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      ((T_Setoid_46 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_46 -> T_IsPreorder_76
du_isPreorder_38 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0))
-- Relation.Binary.Properties.Setoid.≈-preorder
d_'8776''45'preorder_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_'8776''45'preorder_50 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Preorder_142
d_'8776''45'preorder_50 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 = T_Setoid_46 -> T_Preorder_142
du_'8776''45'preorder_50 T_Setoid_46
v2
du_'8776''45'preorder_50 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_'8776''45'preorder_50 :: T_Setoid_46 -> T_Preorder_142
du_'8776''45'preorder_50 T_Setoid_46
v0
  = (T_IsPreorder_76 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      ((T_Setoid_46 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_46 -> T_IsPreorder_76
du_'8776''45'isPreorder_40 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0))
-- Relation.Binary.Properties.Setoid.≈-poset
d_'8776''45'poset_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_'8776''45'poset_52 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Poset_492
d_'8776''45'poset_52 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 = T_Setoid_46 -> T_Poset_492
du_'8776''45'poset_52 T_Setoid_46
v2
du_'8776''45'poset_52 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
du_'8776''45'poset_52 :: T_Setoid_46 -> T_Poset_492
du_'8776''45'poset_52 T_Setoid_46
v0
  = (T_IsPartialOrder_248 -> T_Poset_492) -> AgdaAny -> T_Poset_492
forall a b. a -> b
coe
      T_IsPartialOrder_248 -> T_Poset_492
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_588
      ((T_Setoid_46 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_46 -> T_IsPartialOrder_248
du_'8776''45'isPartialOrder_42 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0))
-- Relation.Binary.Properties.Setoid.≉-sym
d_'8777''45'sym_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8777''45'sym_54 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_'8777''45'sym_54 = T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Setoid.≉-respˡ
d_'8777''45'resp'737'_58 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8777''45'resp'737'_58 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_'8777''45'resp'737'_58 = T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Setoid.≉-respʳ
d_'8777''45'resp'691'_64 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8777''45'resp'691'_64 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_'8777''45'resp'691'_64 = T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Setoid.≉-resp₂
d_'8777''45'resp'8322'_72 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8777''45'resp'8322'_72 :: T_Level_18 -> T_Level_18 -> T_Setoid_46 -> T_Σ_14
d_'8777''45'resp'8322'_72 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_46
v2 = T_Σ_14
du_'8777''45'resp'8322'_72
du_'8777''45'resp'8322'_72 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8777''45'resp'8322'_72 :: T_Σ_14
du_'8777''45'resp'8322'_72
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Relation.Binary.Properties.Setoid.≉-irrefl
d_'8777''45'irrefl_74 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8777''45'irrefl_74 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Irrelevant_20
d_'8777''45'irrefl_74 = T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Setoid.≈;≈⇒≈
d_'8776''894''8776''8658''8776'_80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
d_'8776''894''8776''8658''8776'_80 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
d_'8776''894''8776''8658''8776'_80 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 AgdaAny
v3 AgdaAny
v4
  = T_Setoid_46 -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny
du_'8776''894''8776''8658''8776'_80 T_Setoid_46
v2 AgdaAny
v3 AgdaAny
v4
du_'8776''894''8776''8658''8776'_80 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
du_'8776''894''8776''8658''8776'_80 :: T_Setoid_46 -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny
du_'8776''894''8776''8658''8776'_80 T_Setoid_46
v0 AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Relation.Binary.Construct.Composition.du_transitive'8658''8776''894''8776''8838''8776'_366
      ((T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
         ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0)))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
-- Relation.Binary.Properties.Setoid.≈⇒≈;≈
d_'8776''8658''8776''894''8776'_82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8776''8658''8776''894''8776'_82 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_'8776''8658''8776''894''8776'_82 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 AgdaAny
v3 AgdaAny
v4
  = T_Setoid_46 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14
du_'8776''8658''8776''894''8776'_82 T_Setoid_46
v2 AgdaAny
v3 AgdaAny
v4
du_'8776''8658''8776''894''8776'_82 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8776''8658''8776''894''8776'_82 :: T_Setoid_46 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14
du_'8776''8658''8776''894''8776'_82 T_Setoid_46
v0 AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Relation.Binary.Construct.Composition.du_implies'737'_194
      ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
         ((T_Setoid_46 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe T_Setoid_46
v0)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v5)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
-- Relation.Binary.Properties.Setoid.respʳ-flip
d_resp'691''45'flip_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_resp'691''45'flip_84 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_resp'691''45'flip_84 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
  = T_Setoid_46
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'691''45'flip_84 T_Setoid_46
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
du_resp'691''45'flip_84 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'691''45'flip_84 :: T_Setoid_46
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'691''45'flip_84 T_Setoid_46
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = (T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
      (T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46
v0))
      AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v5
      ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
         (T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46
v0))
         AgdaAny
v3 AgdaAny
v2 AgdaAny
v4)
-- Relation.Binary.Properties.Setoid.respˡ-flip
d_resp'737''45'flip_90 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_resp'737''45'flip_90 :: T_Level_18
-> T_Level_18
-> T_Setoid_46
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_resp'737''45'flip_90 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_46
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = T_Setoid_46
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'737''45'flip_90 T_Setoid_46
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_resp'737''45'flip_90 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'737''45'flip_90 :: T_Setoid_46
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'737''45'flip_90 T_Setoid_46
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40
      (T_Setoid_46 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_62 (T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46
v0))
      AgdaAny
v3 AgdaAny
v2 AgdaAny
v1