{-# 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_44 ->
  AgdaAny -> AgdaAny -> ()
d__'8777'__18 :: T_Level_18
-> T_Level_18 -> T_Setoid_44 -> AgdaAny -> AgdaAny -> T_Level_18
d__'8777'__18 = T_Level_18
-> T_Level_18 -> T_Setoid_44 -> AgdaAny -> AgdaAny -> T_Level_18
forall a. a
erased
-- Relation.Binary.Properties.Setoid.isPreorder
d_isPreorder_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_36 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_IsPreorder_70
d_isPreorder_36 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_IsPreorder_70
du_isPreorder_36 T_Setoid_44
v2
du_isPreorder_36 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_isPreorder_36 :: T_Setoid_44 -> T_IsPreorder_70
du_isPreorder_36 T_Setoid_44
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
         AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased)
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
         (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_reflexive_40
           ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
           AgdaAny
v1)
      ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
-- Relation.Binary.Properties.Setoid.≈-isPreorder
d_'8776''45'isPreorder_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8776''45'isPreorder_38 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_IsPreorder_70
d_'8776''45'isPreorder_38 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2
  = T_Setoid_44 -> T_IsPreorder_70
du_'8776''45'isPreorder_38 T_Setoid_44
v2
du_'8776''45'isPreorder_38 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_'8776''45'isPreorder_38 :: T_Setoid_44 -> T_IsPreorder_70
du_'8776''45'isPreorder_38 T_Setoid_44
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
      ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> AgdaAny
v3))
      ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
-- Relation.Binary.Properties.Setoid.≈-isPartialOrder
d_'8776''45'isPartialOrder_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_'8776''45'isPartialOrder_40 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_IsPartialOrder_174
d_'8776''45'isPartialOrder_40 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2
  = T_Setoid_44 -> T_IsPartialOrder_174
du_'8776''45'isPartialOrder_40 T_Setoid_44
v2
du_'8776''45'isPartialOrder_40 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
du_'8776''45'isPartialOrder_40 :: T_Setoid_44 -> T_IsPartialOrder_174
du_'8776''45'isPartialOrder_40 T_Setoid_44
v0
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
      T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
      ((T_Setoid_44 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsPreorder_70
du_'8776''45'isPreorder_38 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
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_46 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_preorder_46 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Preorder_132
d_preorder_46 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_Preorder_132
du_preorder_46 T_Setoid_44
v2
du_preorder_46 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_preorder_46 :: T_Setoid_44 -> T_Preorder_132
du_preorder_46 T_Setoid_44
v0
  = (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
      ((T_Setoid_44 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsPreorder_70
du_isPreorder_36 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
-- Relation.Binary.Properties.Setoid.≈-preorder
d_'8776''45'preorder_48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_'8776''45'preorder_48 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Preorder_132
d_'8776''45'preorder_48 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_Preorder_132
du_'8776''45'preorder_48 T_Setoid_44
v2
du_'8776''45'preorder_48 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_'8776''45'preorder_48 :: T_Setoid_44 -> T_Preorder_132
du_'8776''45'preorder_48 T_Setoid_44
v0
  = (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
      ((T_Setoid_44 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsPreorder_70
du_'8776''45'isPreorder_38 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
-- Relation.Binary.Properties.Setoid.≈-poset
d_'8776''45'poset_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_'8776''45'poset_50 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Poset_314
d_'8776''45'poset_50 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_Poset_314
du_'8776''45'poset_50 T_Setoid_44
v2
du_'8776''45'poset_50 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
du_'8776''45'poset_50 :: T_Setoid_44 -> T_Poset_314
du_'8776''45'poset_50 T_Setoid_44
v0
  = (T_IsPartialOrder_174 -> T_Poset_314) -> AgdaAny -> T_Poset_314
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
      ((T_Setoid_44 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsPartialOrder_174
du_'8776''45'isPartialOrder_40 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
-- Relation.Binary.Properties.Setoid.≉-sym
d_'8777''45'sym_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8777''45'sym_52 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_'8777''45'sym_52 = T_Level_18
-> T_Level_18
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Setoid.≉-respˡ
d_'8777''45'resp'737'_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  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'_56 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_'8777''45'resp'737'_56 = T_Level_18
-> T_Level_18
-> T_Setoid_44
-> 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'_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  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'_62 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_'8777''45'resp'691'_62 = T_Level_18
-> T_Level_18
-> T_Setoid_44
-> 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'_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8777''45'resp'8322'_70 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Σ_14
d_'8777''45'resp'8322'_70 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Σ_14
du_'8777''45'resp'8322'_70
du_'8777''45'resp'8322'_70 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8777''45'resp'8322'_70 :: T_Σ_14
du_'8777''45'resp'8322'_70
  = (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_72 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8777''45'irrefl_72 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Irrelevant_20
d_'8777''45'irrefl_72 = T_Level_18
-> T_Level_18
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Properties.Setoid.≈;≈⇒≈
d_'8776''894''8776''8658''8776'_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
d_'8776''894''8776''8658''8776'_78 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> AgdaAny
d_'8776''894''8776''8658''8776'_78 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 AgdaAny
v3 AgdaAny
v4
  = T_Setoid_44 -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny
du_'8776''894''8776''8658''8776'_78 T_Setoid_44
v2 AgdaAny
v3 AgdaAny
v4
du_'8776''894''8776''8658''8776'_78 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
du_'8776''894''8776''8658''8776'_78 :: T_Setoid_44 -> AgdaAny -> AgdaAny -> T_Σ_14 -> AgdaAny
du_'8776''894''8776''8658''8776'_78 T_Setoid_44
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_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
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'_80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8776''8658''8776''894''8776'_80 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
d_'8776''8658''8776''894''8776'_80 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 AgdaAny
v3 AgdaAny
v4
  = T_Setoid_44 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14
du_'8776''8658''8776''894''8776'_80 T_Setoid_44
v2 AgdaAny
v3 AgdaAny
v4
du_'8776''8658''8776''894''8776'_80 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8776''8658''8776''894''8776'_80 :: T_Setoid_44 -> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14
du_'8776''8658''8776''894''8776'_80 T_Setoid_44
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_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
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_82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_resp'691''45'flip_82 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_resp'691''45'flip_82 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
  = T_Setoid_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'691''45'flip_82 T_Setoid_44
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
du_resp'691''45'flip_82 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'691''45'flip_82 :: T_Setoid_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'691''45'flip_82 T_Setoid_44
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
      (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
      AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v5
      ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
         (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
         AgdaAny
v3 AgdaAny
v2 AgdaAny
v4)
-- Relation.Binary.Properties.Setoid.respˡ-flip
d_resp'737''45'flip_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_resp'737''45'flip_88 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_resp'737''45'flip_88 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = T_Setoid_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'737''45'flip_88 T_Setoid_44
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
du_resp'737''45'flip_88 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'737''45'flip_88 :: T_Setoid_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_resp'737''45'flip_88 T_Setoid_44
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
      (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
      AgdaAny
v3 AgdaAny
v2 AgdaAny
v1