{-# 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.Bundles 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Relation.Binary.Bundles.PartialSetoid
d_PartialSetoid_10 :: p -> p -> ()
d_PartialSetoid_10 p
a0 p
a1 = ()
newtype T_PartialSetoid_10
  = C_PartialSetoid'46'constructor_133 MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
-- Relation.Binary.Bundles.PartialSetoid.Carrier
d_Carrier_22 :: T_PartialSetoid_10 -> ()
d_Carrier_22 :: T_PartialSetoid_10 -> ()
d_Carrier_22 = T_PartialSetoid_10 -> ()
forall a. a
erased
-- Relation.Binary.Bundles.PartialSetoid._≈_
d__'8776'__24 :: T_PartialSetoid_10 -> AgdaAny -> AgdaAny -> ()
d__'8776'__24 :: T_PartialSetoid_10 -> AgdaAny -> AgdaAny -> ()
d__'8776'__24 = T_PartialSetoid_10 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.PartialSetoid.isPartialEquivalence
d_isPartialEquivalence_26 ::
  T_PartialSetoid_10 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
d_isPartialEquivalence_26 :: T_PartialSetoid_10 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_26 T_PartialSetoid_10
v0
  = case T_PartialSetoid_10 -> T_PartialSetoid_10
forall a b. a -> b
coe T_PartialSetoid_10
v0 of
      C_PartialSetoid'46'constructor_133 T_IsPartialEquivalence_16
v3 -> T_IsPartialEquivalence_16 -> T_IsPartialEquivalence_16
forall a b. a -> b
coe T_IsPartialEquivalence_16
v3
      T_PartialSetoid_10
_ -> T_IsPartialEquivalence_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Bundles.PartialSetoid._.sym
d_sym_30 ::
  T_PartialSetoid_10 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_30 :: T_PartialSetoid_10 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_30 T_PartialSetoid_10
v0
  = (T_IsPartialEquivalence_16
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPartialEquivalence_16
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_22
      ((T_PartialSetoid_10 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_PartialSetoid_10 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_26 (T_PartialSetoid_10 -> AgdaAny
forall a b. a -> b
coe T_PartialSetoid_10
v0))
-- Relation.Binary.Bundles.PartialSetoid._.trans
d_trans_32 ::
  T_PartialSetoid_10 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_32 :: T_PartialSetoid_10
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_32 T_PartialSetoid_10
v0
  = (T_IsPartialEquivalence_16
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPartialEquivalence_16
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_24
      ((T_PartialSetoid_10 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_PartialSetoid_10 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_26 (T_PartialSetoid_10 -> AgdaAny
forall a b. a -> b
coe T_PartialSetoid_10
v0))
-- Relation.Binary.Bundles.PartialSetoid._≉_
d__'8777'__34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_PartialSetoid_10 -> AgdaAny -> AgdaAny -> ()
d__'8777'__34 :: () -> () -> T_PartialSetoid_10 -> AgdaAny -> AgdaAny -> ()
d__'8777'__34 = () -> () -> T_PartialSetoid_10 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Setoid
d_Setoid_44 :: p -> p -> ()
d_Setoid_44 p
a0 p
a1 = ()
newtype T_Setoid_44
  = C_Setoid'46'constructor_733 MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
-- Relation.Binary.Bundles.Setoid.Carrier
d_Carrier_56 :: T_Setoid_44 -> ()
d_Carrier_56 :: T_Setoid_44 -> ()
d_Carrier_56 = T_Setoid_44 -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Setoid._≈_
d__'8776'__58 :: T_Setoid_44 -> AgdaAny -> AgdaAny -> ()
d__'8776'__58 :: T_Setoid_44 -> AgdaAny -> AgdaAny -> ()
d__'8776'__58 = T_Setoid_44 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Setoid.isEquivalence
d_isEquivalence_60 ::
  T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_60 :: T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 T_Setoid_44
v0
  = case T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0 of
      C_Setoid'46'constructor_733 T_IsEquivalence_26
v3 -> T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
v3
      T_Setoid_44
_ -> T_IsEquivalence_26
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Bundles.Setoid._.isPartialEquivalence
d_isPartialEquivalence_64 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
d_isPartialEquivalence_64 :: () -> () -> T_Setoid_44 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_64 ~()
v0 ~()
v1 T_Setoid_44
v2
  = T_Setoid_44 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_64 T_Setoid_44
v2
du_isPartialEquivalence_64 ::
  T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
du_isPartialEquivalence_64 :: T_Setoid_44 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_64 T_Setoid_44
v0
  = (T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_IsPartialEquivalence_16
MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
      ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
-- Relation.Binary.Bundles.Setoid._.refl
d_refl_66 :: T_Setoid_44 -> AgdaAny -> AgdaAny
d_refl_66 :: T_Setoid_44 -> AgdaAny -> AgdaAny
d_refl_66 T_Setoid_44
v0
  = (T_IsEquivalence_26 -> AgdaAny -> 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
d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
-- Relation.Binary.Bundles.Setoid._.reflexive
d_reflexive_68 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Setoid_44 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_68 :: ()
-> ()
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_68 ~()
v0 ~()
v1 T_Setoid_44
v2 = T_Setoid_44 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_68 T_Setoid_44
v2
du_reflexive_68 ::
  T_Setoid_44 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_68 :: T_Setoid_44 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_68 T_Setoid_44
v0 AgdaAny
v1 AgdaAny
v2 T__'8801'__12
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
d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)) AgdaAny
v1
-- Relation.Binary.Bundles.Setoid.partialSetoid
d_partialSetoid_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Setoid_44 -> T_PartialSetoid_10
d_partialSetoid_70 :: () -> () -> T_Setoid_44 -> T_PartialSetoid_10
d_partialSetoid_70 ~()
v0 ~()
v1 T_Setoid_44
v2 = T_Setoid_44 -> T_PartialSetoid_10
du_partialSetoid_70 T_Setoid_44
v2
du_partialSetoid_70 :: T_Setoid_44 -> T_PartialSetoid_10
du_partialSetoid_70 :: T_Setoid_44 -> T_PartialSetoid_10
du_partialSetoid_70 T_Setoid_44
v0
  = (T_IsPartialEquivalence_16 -> T_PartialSetoid_10)
-> AgdaAny -> T_PartialSetoid_10
forall a b. a -> b
coe
      T_IsPartialEquivalence_16 -> T_PartialSetoid_10
C_PartialSetoid'46'constructor_133
      ((T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsPartialEquivalence_16
MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
-- Relation.Binary.Bundles.Setoid._._≉_
d__'8777'__74 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Setoid_44 -> AgdaAny -> AgdaAny -> ()
d__'8777'__74 :: () -> () -> T_Setoid_44 -> AgdaAny -> AgdaAny -> ()
d__'8777'__74 = () -> () -> T_Setoid_44 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Setoid._.sym
d_sym_76 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Setoid_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_76 :: () -> () -> T_Setoid_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_76 ~()
v0 ~()
v1 T_Setoid_44
v2 = T_Setoid_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_76 T_Setoid_44
v2
du_sym_76 ::
  T_Setoid_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_76 :: T_Setoid_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_76 T_Setoid_44
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> 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) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
-- Relation.Binary.Bundles.Setoid._.trans
d_trans_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Setoid_44 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_78 :: ()
-> ()
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_78 ~()
v0 ~()
v1 T_Setoid_44
v2 = T_Setoid_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_78 T_Setoid_44
v2
du_trans_78 ::
  T_Setoid_44 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_78 :: T_Setoid_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_78 T_Setoid_44
v0
  = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> 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
d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0))
-- Relation.Binary.Bundles.DecSetoid
d_DecSetoid_84 :: p -> p -> ()
d_DecSetoid_84 p
a0 p
a1 = ()
newtype T_DecSetoid_84
  = C_DecSetoid'46'constructor_1389 MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
-- Relation.Binary.Bundles.DecSetoid.Carrier
d_Carrier_96 :: T_DecSetoid_84 -> ()
d_Carrier_96 :: T_DecSetoid_84 -> ()
d_Carrier_96 = T_DecSetoid_84 -> ()
forall a. a
erased
-- Relation.Binary.Bundles.DecSetoid._≈_
d__'8776'__98 :: T_DecSetoid_84 -> AgdaAny -> AgdaAny -> ()
d__'8776'__98 :: T_DecSetoid_84 -> AgdaAny -> AgdaAny -> ()
d__'8776'__98 = T_DecSetoid_84 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.DecSetoid.isDecEquivalence
d_isDecEquivalence_100 ::
  T_DecSetoid_84 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_isDecEquivalence_100 :: T_DecSetoid_84 -> T_IsDecEquivalence_44
d_isDecEquivalence_100 T_DecSetoid_84
v0
  = case T_DecSetoid_84 -> T_DecSetoid_84
forall a b. a -> b
coe T_DecSetoid_84
v0 of
      C_DecSetoid'46'constructor_1389 T_IsDecEquivalence_44
v3 -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44
forall a b. a -> b
coe T_IsDecEquivalence_44
v3
      T_DecSetoid_84
_ -> T_IsDecEquivalence_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Bundles.DecSetoid._._≟_
d__'8799'__104 ::
  T_DecSetoid_84 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__104 :: T_DecSetoid_84 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8799'__104 T_DecSetoid_84
v0
  = (T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      T_IsDecEquivalence_44 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52
      ((T_DecSetoid_84 -> T_IsDecEquivalence_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84 -> T_IsDecEquivalence_44
d_isDecEquivalence_100 (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0))
-- Relation.Binary.Bundles.DecSetoid._.isEquivalence
d_isEquivalence_106 ::
  T_DecSetoid_84 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_106 :: T_DecSetoid_84 -> T_IsEquivalence_26
d_isEquivalence_106 T_DecSetoid_84
v0
  = (T_IsDecEquivalence_44 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
      ((T_DecSetoid_84 -> T_IsDecEquivalence_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84 -> T_IsDecEquivalence_44
d_isDecEquivalence_100 (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0))
-- Relation.Binary.Bundles.DecSetoid.setoid
d_setoid_108 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecSetoid_84 -> T_Setoid_44
d_setoid_108 :: () -> () -> T_DecSetoid_84 -> T_Setoid_44
d_setoid_108 ~()
v0 ~()
v1 T_DecSetoid_84
v2 = T_DecSetoid_84 -> T_Setoid_44
du_setoid_108 T_DecSetoid_84
v2
du_setoid_108 :: T_DecSetoid_84 -> T_Setoid_44
du_setoid_108 :: T_DecSetoid_84 -> T_Setoid_44
du_setoid_108 T_DecSetoid_84
v0
  = (T_IsEquivalence_26 -> T_Setoid_44)
-> T_IsEquivalence_26 -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
C_Setoid'46'constructor_733
      (T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
         ((T_DecSetoid_84 -> T_IsDecEquivalence_44)
-> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe T_DecSetoid_84 -> T_IsDecEquivalence_44
d_isDecEquivalence_100 (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0)))
-- Relation.Binary.Bundles.DecSetoid._._≉_
d__'8777'__112 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecSetoid_84 -> AgdaAny -> AgdaAny -> ()
d__'8777'__112 :: () -> () -> T_DecSetoid_84 -> AgdaAny -> AgdaAny -> ()
d__'8777'__112 = () -> () -> T_DecSetoid_84 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.DecSetoid._.isPartialEquivalence
d_isPartialEquivalence_114 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecSetoid_84 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
d_isPartialEquivalence_114 :: () -> () -> T_DecSetoid_84 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_114 ~()
v0 ~()
v1 T_DecSetoid_84
v2
  = T_DecSetoid_84 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_114 T_DecSetoid_84
v2
du_isPartialEquivalence_114 ::
  T_DecSetoid_84 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
du_isPartialEquivalence_114 :: T_DecSetoid_84 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_114 T_DecSetoid_84
v0
  = let v1 :: t
v1 = (T_DecSetoid_84 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_DecSetoid_84 -> T_Setoid_44
du_setoid_108 (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0) in
    AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      ((T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsPartialEquivalence_16
MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.DecSetoid._.partialSetoid
d_partialSetoid_116 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecSetoid_84 -> T_PartialSetoid_10
d_partialSetoid_116 :: () -> () -> T_DecSetoid_84 -> T_PartialSetoid_10
d_partialSetoid_116 ~()
v0 ~()
v1 T_DecSetoid_84
v2 = T_DecSetoid_84 -> T_PartialSetoid_10
du_partialSetoid_116 T_DecSetoid_84
v2
du_partialSetoid_116 :: T_DecSetoid_84 -> T_PartialSetoid_10
du_partialSetoid_116 :: T_DecSetoid_84 -> T_PartialSetoid_10
du_partialSetoid_116 T_DecSetoid_84
v0
  = (T_Setoid_44 -> T_PartialSetoid_10)
-> AgdaAny -> T_PartialSetoid_10
forall a b. a -> b
coe T_Setoid_44 -> T_PartialSetoid_10
du_partialSetoid_70 ((T_DecSetoid_84 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84 -> T_Setoid_44
du_setoid_108 (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0))
-- Relation.Binary.Bundles.DecSetoid._.refl
d_refl_118 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecSetoid_84 -> AgdaAny -> AgdaAny
d_refl_118 :: () -> () -> T_DecSetoid_84 -> AgdaAny -> AgdaAny
d_refl_118 ~()
v0 ~()
v1 T_DecSetoid_84
v2 = T_DecSetoid_84 -> AgdaAny -> AgdaAny
du_refl_118 T_DecSetoid_84
v2
du_refl_118 :: T_DecSetoid_84 -> AgdaAny -> AgdaAny
du_refl_118 :: T_DecSetoid_84 -> AgdaAny -> AgdaAny
du_refl_118 T_DecSetoid_84
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
      ((T_IsDecEquivalence_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
         ((T_DecSetoid_84 -> T_IsDecEquivalence_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84 -> T_IsDecEquivalence_44
d_isDecEquivalence_100 (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0)))
-- Relation.Binary.Bundles.DecSetoid._.reflexive
d_reflexive_120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecSetoid_84 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_120 :: ()
-> ()
-> T_DecSetoid_84
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_120 ~()
v0 ~()
v1 T_DecSetoid_84
v2 = T_DecSetoid_84 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_120 T_DecSetoid_84
v2
du_reflexive_120 ::
  T_DecSetoid_84 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_120 :: T_DecSetoid_84 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_120 T_DecSetoid_84
v0
  = let v1 :: t
v1 = (T_DecSetoid_84 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_DecSetoid_84 -> T_Setoid_44
du_setoid_108 (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0) in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (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
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)) AgdaAny
v2)
-- Relation.Binary.Bundles.DecSetoid._.sym
d_sym_122 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecSetoid_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_122 :: ()
-> () -> T_DecSetoid_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_122 ~()
v0 ~()
v1 T_DecSetoid_84
v2 = T_DecSetoid_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_122 T_DecSetoid_84
v2
du_sym_122 ::
  T_DecSetoid_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_122 :: T_DecSetoid_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_122 T_DecSetoid_84
v0
  = let v1 :: t
v1 = (T_DecSetoid_84 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_DecSetoid_84 -> T_Setoid_44
du_setoid_108 (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0) in
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> 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) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.DecSetoid._.trans
d_trans_124 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecSetoid_84 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_124 :: ()
-> ()
-> T_DecSetoid_84
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_124 ~()
v0 ~()
v1 T_DecSetoid_84
v2 = T_DecSetoid_84
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_124 T_DecSetoid_84
v2
du_trans_124 ::
  T_DecSetoid_84 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_124 :: T_DecSetoid_84
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_124 T_DecSetoid_84
v0
  = let v1 :: t
v1 = (T_DecSetoid_84 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_DecSetoid_84 -> T_Setoid_44
du_setoid_108 (T_DecSetoid_84 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_84
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((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
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Preorder
d_Preorder_132 :: p -> p -> p -> ()
d_Preorder_132 p
a0 p
a1 p
a2 = ()
newtype T_Preorder_132
  = C_Preorder'46'constructor_2267 MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
-- Relation.Binary.Bundles.Preorder.Carrier
d_Carrier_148 :: T_Preorder_132 -> ()
d_Carrier_148 :: T_Preorder_132 -> ()
d_Carrier_148 = T_Preorder_132 -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Preorder._≈_
d__'8776'__150 :: T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8776'__150 :: T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8776'__150 = T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Preorder._≲_
d__'8818'__152 :: T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8818'__152 :: T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8818'__152 = T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Preorder.isPreorder
d_isPreorder_154 ::
  T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_154 :: T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 T_Preorder_132
v0
  = case T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0 of
      C_Preorder'46'constructor_2267 T_IsPreorder_70
v4 -> T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v4
      T_Preorder_132
_ -> T_IsPreorder_70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Bundles.Preorder._.isEquivalence
d_isEquivalence_158 ::
  T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_158 :: T_Preorder_132 -> T_IsEquivalence_26
d_isEquivalence_158 T_Preorder_132
v0
  = (T_IsPreorder_70 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder._.refl
d_refl_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> AgdaAny -> AgdaAny
d_refl_160 :: () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny
d_refl_160 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3 = T_Preorder_132 -> AgdaAny -> AgdaAny
du_refl_160 T_Preorder_132
v3
du_refl_160 :: T_Preorder_132 -> AgdaAny -> AgdaAny
du_refl_160 :: T_Preorder_132 -> AgdaAny -> AgdaAny
du_refl_160 T_Preorder_132
v0
  = (T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder._.reflexive
d_reflexive_162 ::
  T_Preorder_132 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_162 :: T_Preorder_132 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_162 T_Preorder_132
v0
  = (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder._.trans
d_trans_164 ::
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_164 :: T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_164 T_Preorder_132
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder._.∼-resp-≈
d_'8764''45'resp'45''8776'_166 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8764''45'resp'45''8776'_166 :: () -> () -> () -> T_Preorder_132 -> T_Σ_14
d_'8764''45'resp'45''8776'_166 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3
  = T_Preorder_132 -> T_Σ_14
du_'8764''45'resp'45''8776'_166 T_Preorder_132
v3
du_'8764''45'resp'45''8776'_166 ::
  T_Preorder_132 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8764''45'resp'45''8776'_166 :: T_Preorder_132 -> T_Σ_14
du_'8764''45'resp'45''8776'_166 T_Preorder_132
v0
  = (T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'45''8776'_118
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder._.∼-respʳ-≈
d_'8764''45'resp'691''45''8776'_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'691''45''8776'_168 :: ()
-> ()
-> ()
-> T_Preorder_132
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'691''45''8776'_168 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3
  = T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_168 T_Preorder_132
v3
du_'8764''45'resp'691''45''8776'_168 ::
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_168 :: T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_168 T_Preorder_132
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'691''45''8776'_116
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder._.∼-respˡ-≈
d_'8764''45'resp'737''45''8776'_170 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'737''45''8776'_170 :: ()
-> ()
-> ()
-> T_Preorder_132
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'737''45''8776'_170 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3
  = T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_170 T_Preorder_132
v3
du_'8764''45'resp'737''45''8776'_170 ::
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_170 :: T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_170 T_Preorder_132
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'737''45''8776'_114
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder._.≲-resp-≈
d_'8818''45'resp'45''8776'_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8818''45'resp'45''8776'_172 :: () -> () -> () -> T_Preorder_132 -> T_Σ_14
d_'8818''45'resp'45''8776'_172 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3
  = T_Preorder_132 -> T_Σ_14
du_'8818''45'resp'45''8776'_172 T_Preorder_132
v3
du_'8818''45'resp'45''8776'_172 ::
  T_Preorder_132 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8818''45'resp'45''8776'_172 :: T_Preorder_132 -> T_Σ_14
du_'8818''45'resp'45''8776'_172 T_Preorder_132
v0
  = (T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'45''8776'_112
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder._.≲-respʳ-≈
d_'8818''45'resp'691''45''8776'_174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8818''45'resp'691''45''8776'_174 :: ()
-> ()
-> ()
-> T_Preorder_132
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8818''45'resp'691''45''8776'_174 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3
  = T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'691''45''8776'_174 T_Preorder_132
v3
du_'8818''45'resp'691''45''8776'_174 ::
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'691''45''8776'_174 :: T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'691''45''8776'_174 T_Preorder_132
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'691''45''8776'_106
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder._.≲-respˡ-≈
d_'8818''45'resp'737''45''8776'_176 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8818''45'resp'737''45''8776'_176 :: ()
-> ()
-> ()
-> T_Preorder_132
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8818''45'resp'737''45''8776'_176 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3
  = T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'737''45''8776'_176 T_Preorder_132
v3
du_'8818''45'resp'737''45''8776'_176 ::
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'737''45''8776'_176 :: T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'737''45''8776'_176 T_Preorder_132
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'737''45''8776'_100
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder.Eq.setoid
d_setoid_180 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> T_Setoid_44
d_setoid_180 :: () -> () -> () -> T_Preorder_132 -> T_Setoid_44
d_setoid_180 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3 = T_Preorder_132 -> T_Setoid_44
du_setoid_180 T_Preorder_132
v3
du_setoid_180 :: T_Preorder_132 -> T_Setoid_44
du_setoid_180 :: T_Preorder_132 -> T_Setoid_44
du_setoid_180 T_Preorder_132
v0
  = (T_IsEquivalence_26 -> T_Setoid_44)
-> T_IsEquivalence_26 -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
C_Setoid'46'constructor_733
      (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0)))
-- Relation.Binary.Bundles.Preorder.Eq._._≈_
d__'8776'__184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8776'__184 :: () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8776'__184 = () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Preorder.Eq._._≉_
d__'8777'__186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8777'__186 :: () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8777'__186 = () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Preorder.Eq._.Carrier
d_Carrier_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> T_Preorder_132 -> ()
d_Carrier_188 :: () -> () -> () -> T_Preorder_132 -> ()
d_Carrier_188 = () -> () -> () -> T_Preorder_132 -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Preorder.Eq._.isEquivalence
d_isEquivalence_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_190 :: () -> () -> () -> T_Preorder_132 -> T_IsEquivalence_26
d_isEquivalence_190 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3 = T_Preorder_132 -> T_IsEquivalence_26
du_isEquivalence_190 T_Preorder_132
v3
du_isEquivalence_190 ::
  T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_190 :: T_Preorder_132 -> T_IsEquivalence_26
du_isEquivalence_190 T_Preorder_132
v0
  = (T_IsPreorder_70 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
      ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder.Eq._.isPartialEquivalence
d_isPartialEquivalence_192 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
d_isPartialEquivalence_192 :: () -> () -> () -> T_Preorder_132 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_192 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3
  = T_Preorder_132 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_192 T_Preorder_132
v3
du_isPartialEquivalence_192 ::
  T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
du_isPartialEquivalence_192 :: T_Preorder_132 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_192 T_Preorder_132
v0
  = let v1 :: t
v1 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0) in
    AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      ((T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsPartialEquivalence_16
MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
         ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Preorder.Eq._.partialSetoid
d_partialSetoid_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> T_PartialSetoid_10
d_partialSetoid_194 :: () -> () -> () -> T_Preorder_132 -> T_PartialSetoid_10
d_partialSetoid_194 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3 = T_Preorder_132 -> T_PartialSetoid_10
du_partialSetoid_194 T_Preorder_132
v3
du_partialSetoid_194 :: T_Preorder_132 -> T_PartialSetoid_10
du_partialSetoid_194 :: T_Preorder_132 -> T_PartialSetoid_10
du_partialSetoid_194 T_Preorder_132
v0
  = (T_Setoid_44 -> T_PartialSetoid_10)
-> AgdaAny -> T_PartialSetoid_10
forall a b. a -> b
coe T_Setoid_44 -> T_PartialSetoid_10
du_partialSetoid_70 ((T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))
-- Relation.Binary.Bundles.Preorder.Eq._.refl
d_refl_196 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> AgdaAny -> AgdaAny
d_refl_196 :: () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny
d_refl_196 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3 = T_Preorder_132 -> AgdaAny -> AgdaAny
du_refl_196 T_Preorder_132
v3
du_refl_196 :: T_Preorder_132 -> AgdaAny -> AgdaAny
du_refl_196 :: T_Preorder_132 -> AgdaAny -> AgdaAny
du_refl_196 T_Preorder_132
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0)))
-- Relation.Binary.Bundles.Preorder.Eq._.reflexive
d_reflexive_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_198 :: ()
-> ()
-> ()
-> T_Preorder_132
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_198 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3 = T_Preorder_132 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_198 T_Preorder_132
v3
du_reflexive_198 ::
  T_Preorder_132 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_198 :: T_Preorder_132 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_198 T_Preorder_132
v0
  = let v1 :: t
v1 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0) in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (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
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)) AgdaAny
v2)
-- Relation.Binary.Bundles.Preorder.Eq._.sym
d_sym_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_200 :: ()
-> ()
-> ()
-> T_Preorder_132
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_sym_200 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3 = T_Preorder_132 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_200 T_Preorder_132
v3
du_sym_200 ::
  T_Preorder_132 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_200 :: T_Preorder_132 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_200 T_Preorder_132
v0
  = let v1 :: t
v1 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0) in
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> 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) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Preorder.Eq._.trans
d_trans_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_202 :: ()
-> ()
-> ()
-> T_Preorder_132
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_202 ~()
v0 ~()
v1 ~()
v2 T_Preorder_132
v3 = T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_202 T_Preorder_132
v3
du_trans_202 ::
  T_Preorder_132 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_202 :: T_Preorder_132
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_202 T_Preorder_132
v0
  = let v1 :: t
v1 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((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
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Preorder._⋦_
d__'8934'__204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8934'__204 :: () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8934'__204 = () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Preorder._≳_
d__'8819'__210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8819'__210 :: () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8819'__210 = () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Preorder._⋧_
d__'8935'__212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8935'__212 :: () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8935'__212 = () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Preorder._∼_
d__'8764'__214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8764'__214 :: () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
d__'8764'__214 = () -> () -> () -> T_Preorder_132 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder
d_TotalPreorder_222 :: p -> p -> p -> ()
d_TotalPreorder_222 p
a0 p
a1 p
a2 = ()
newtype T_TotalPreorder_222
  = C_TotalPreorder'46'constructor_4573 MAlonzo.Code.Relation.Binary.Structures.T_IsTotalPreorder_124
-- Relation.Binary.Bundles.TotalPreorder.Carrier
d_Carrier_238 :: T_TotalPreorder_222 -> ()
d_Carrier_238 :: T_TotalPreorder_222 -> ()
d_Carrier_238 = T_TotalPreorder_222 -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder._≈_
d__'8776'__240 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8776'__240 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8776'__240 = T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder._≲_
d__'8818'__242 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8818'__242 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8818'__242 = T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder.isTotalPreorder
d_isTotalPreorder_244 ::
  T_TotalPreorder_222 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalPreorder_124
d_isTotalPreorder_244 :: T_TotalPreorder_222 -> T_IsTotalPreorder_124
d_isTotalPreorder_244 T_TotalPreorder_222
v0
  = case T_TotalPreorder_222 -> T_TotalPreorder_222
forall a b. a -> b
coe T_TotalPreorder_222
v0 of
      C_TotalPreorder'46'constructor_4573 T_IsTotalPreorder_124
v4 -> T_IsTotalPreorder_124 -> T_IsTotalPreorder_124
forall a b. a -> b
coe T_IsTotalPreorder_124
v4
      T_TotalPreorder_222
_ -> T_IsTotalPreorder_124
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Bundles.TotalPreorder._.isPreorder
d_isPreorder_248 ::
  T_TotalPreorder_222 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_248 :: T_TotalPreorder_222 -> T_IsPreorder_70
d_isPreorder_248 T_TotalPreorder_222
v0
  = (T_IsTotalPreorder_124 -> T_IsPreorder_70)
-> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsTotalPreorder_124 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_132
      ((T_TotalPreorder_222 -> T_IsTotalPreorder_124)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222 -> T_IsTotalPreorder_124
d_isTotalPreorder_244 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
-- Relation.Binary.Bundles.TotalPreorder._.total
d_total_250 ::
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_total_250 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> T__'8846'__30
d_total_250 T_TotalPreorder_222
v0
  = (T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      T_IsTotalPreorder_124 -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Relation.Binary.Structures.d_total_134
      ((T_TotalPreorder_222 -> T_IsTotalPreorder_124)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222 -> T_IsTotalPreorder_124
d_isTotalPreorder_244 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
-- Relation.Binary.Bundles.TotalPreorder.preorder
d_preorder_252 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> T_Preorder_132
d_preorder_252 :: () -> () -> () -> T_TotalPreorder_222 -> T_Preorder_132
d_preorder_252 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 T_TotalPreorder_222
v3
du_preorder_252 :: T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 :: T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 T_TotalPreorder_222
v0
  = (T_IsPreorder_70 -> T_Preorder_132)
-> T_IsPreorder_70 -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
C_Preorder'46'constructor_2267
      (T_IsTotalPreorder_124 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_132
         ((T_TotalPreorder_222 -> T_IsTotalPreorder_124)
-> AgdaAny -> T_IsTotalPreorder_124
forall a b. a -> b
coe T_TotalPreorder_222 -> T_IsTotalPreorder_124
d_isTotalPreorder_244 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0)))
-- Relation.Binary.Bundles.TotalPreorder._._∼_
d__'8764'__256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8764'__256 :: () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8764'__256 = () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder._._≳_
d__'8819'__258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8819'__258 :: () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8819'__258 = () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder._._⋦_
d__'8934'__260 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8934'__260 :: () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8934'__260 = () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder._._⋧_
d__'8935'__262 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8935'__262 :: () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8935'__262 = () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder._.isEquivalence
d_isEquivalence_264 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_264 :: () -> () -> () -> T_TotalPreorder_222 -> T_IsEquivalence_26
d_isEquivalence_264 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222 -> T_IsEquivalence_26
du_isEquivalence_264 T_TotalPreorder_222
v3
du_isEquivalence_264 ::
  T_TotalPreorder_222 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_264 :: T_TotalPreorder_222 -> T_IsEquivalence_26
du_isEquivalence_264 T_TotalPreorder_222
v0
  = (T_IsPreorder_70 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
      ((T_IsTotalPreorder_124 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsTotalPreorder_124 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_132
         ((T_TotalPreorder_222 -> T_IsTotalPreorder_124)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222 -> T_IsTotalPreorder_124
d_isTotalPreorder_244 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0)))
-- Relation.Binary.Bundles.TotalPreorder._.refl
d_refl_266 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny
d_refl_266 :: () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny
d_refl_266 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222 -> AgdaAny -> AgdaAny
du_refl_266 T_TotalPreorder_222
v3
du_refl_266 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny
du_refl_266 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny
du_refl_266 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.TotalPreorder._.reflexive
d_reflexive_268 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_268 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_reflexive_268 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_268 T_TotalPreorder_222
v3
du_reflexive_268 ::
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_268 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_268 T_TotalPreorder_222
v0
  = (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
      ((T_IsTotalPreorder_124 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsTotalPreorder_124 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_132
         ((T_TotalPreorder_222 -> T_IsTotalPreorder_124)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222 -> T_IsTotalPreorder_124
d_isTotalPreorder_244 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0)))
-- Relation.Binary.Bundles.TotalPreorder._.trans
d_trans_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_270 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_270 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_270 T_TotalPreorder_222
v3
du_trans_270 ::
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_270 :: T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_270 T_TotalPreorder_222
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
      ((T_IsTotalPreorder_124 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsTotalPreorder_124 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_132
         ((T_TotalPreorder_222 -> T_IsTotalPreorder_124)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222 -> T_IsTotalPreorder_124
d_isTotalPreorder_244 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0)))
-- Relation.Binary.Bundles.TotalPreorder._.∼-resp-≈
d_'8764''45'resp'45''8776'_272 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8764''45'resp'45''8776'_272 :: () -> () -> () -> T_TotalPreorder_222 -> T_Σ_14
d_'8764''45'resp'45''8776'_272 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3
  = T_TotalPreorder_222 -> T_Σ_14
du_'8764''45'resp'45''8776'_272 T_TotalPreorder_222
v3
du_'8764''45'resp'45''8776'_272 ::
  T_TotalPreorder_222 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8764''45'resp'45''8776'_272 :: T_TotalPreorder_222 -> T_Σ_14
du_'8764''45'resp'45''8776'_272 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'45''8776'_118
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.TotalPreorder._.∼-respʳ-≈
d_'8764''45'resp'691''45''8776'_274 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'691''45''8776'_274 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'691''45''8776'_274 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3
  = T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_274 T_TotalPreorder_222
v3
du_'8764''45'resp'691''45''8776'_274 ::
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_274 :: T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_274 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'691''45''8776'_116
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.TotalPreorder._.∼-respˡ-≈
d_'8764''45'resp'737''45''8776'_276 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'737''45''8776'_276 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'737''45''8776'_276 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3
  = T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_276 T_TotalPreorder_222
v3
du_'8764''45'resp'737''45''8776'_276 ::
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_276 :: T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_276 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'737''45''8776'_114
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.TotalPreorder._.≲-resp-≈
d_'8818''45'resp'45''8776'_278 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8818''45'resp'45''8776'_278 :: () -> () -> () -> T_TotalPreorder_222 -> T_Σ_14
d_'8818''45'resp'45''8776'_278 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3
  = T_TotalPreorder_222 -> T_Σ_14
du_'8818''45'resp'45''8776'_278 T_TotalPreorder_222
v3
du_'8818''45'resp'45''8776'_278 ::
  T_TotalPreorder_222 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8818''45'resp'45''8776'_278 :: T_TotalPreorder_222 -> T_Σ_14
du_'8818''45'resp'45''8776'_278 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'45''8776'_112
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.TotalPreorder._.≲-respʳ-≈
d_'8818''45'resp'691''45''8776'_280 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8818''45'resp'691''45''8776'_280 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8818''45'resp'691''45''8776'_280 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3
  = T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'691''45''8776'_280 T_TotalPreorder_222
v3
du_'8818''45'resp'691''45''8776'_280 ::
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'691''45''8776'_280 :: T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'691''45''8776'_280 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'691''45''8776'_106
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.TotalPreorder._.≲-respˡ-≈
d_'8818''45'resp'737''45''8776'_282 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8818''45'resp'737''45''8776'_282 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8818''45'resp'737''45''8776'_282 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3
  = T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'737''45''8776'_282 T_TotalPreorder_222
v3
du_'8818''45'resp'737''45''8776'_282 ::
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'737''45''8776'_282 :: T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'737''45''8776'_282 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'737''45''8776'_100
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.TotalPreorder._.Eq._≈_
d__'8776'__286 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8776'__286 :: () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8776'__286 = () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder._.Eq._≉_
d__'8777'__288 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8777'__288 :: () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8777'__288 = () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder._.Eq.Carrier
d_Carrier_290 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> T_TotalPreorder_222 -> ()
d_Carrier_290 :: () -> () -> () -> T_TotalPreorder_222 -> ()
d_Carrier_290 = () -> () -> () -> T_TotalPreorder_222 -> ()
forall a. a
erased
-- Relation.Binary.Bundles.TotalPreorder._.Eq.isEquivalence
d_isEquivalence_292 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_292 :: () -> () -> () -> T_TotalPreorder_222 -> T_IsEquivalence_26
d_isEquivalence_292 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222 -> T_IsEquivalence_26
du_isEquivalence_292 T_TotalPreorder_222
v3
du_isEquivalence_292 ::
  T_TotalPreorder_222 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_292 :: T_TotalPreorder_222 -> T_IsEquivalence_26
du_isEquivalence_292 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.TotalPreorder._.Eq.isPartialEquivalence
d_isPartialEquivalence_294 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
d_isPartialEquivalence_294 :: () -> () -> () -> T_TotalPreorder_222 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_294 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3
  = T_TotalPreorder_222 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_294 T_TotalPreorder_222
v3
du_isPartialEquivalence_294 ::
  T_TotalPreorder_222 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
du_isPartialEquivalence_294 :: T_TotalPreorder_222 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_294 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> T_IsPartialEquivalence_16
MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
            ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
-- Relation.Binary.Bundles.TotalPreorder._.Eq.partialSetoid
d_partialSetoid_296 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> T_PartialSetoid_10
d_partialSetoid_296 :: () -> () -> () -> T_TotalPreorder_222 -> T_PartialSetoid_10
d_partialSetoid_296 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222 -> T_PartialSetoid_10
du_partialSetoid_296 T_TotalPreorder_222
v3
du_partialSetoid_296 :: T_TotalPreorder_222 -> T_PartialSetoid_10
du_partialSetoid_296 :: T_TotalPreorder_222 -> T_PartialSetoid_10
du_partialSetoid_296 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny -> T_PartialSetoid_10
forall a b. a -> b
coe ((T_Setoid_44 -> T_PartialSetoid_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_PartialSetoid_10
du_partialSetoid_70 ((T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.TotalPreorder._.Eq.refl
d_refl_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny
d_refl_298 :: () -> () -> () -> T_TotalPreorder_222 -> AgdaAny -> AgdaAny
d_refl_298 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222 -> AgdaAny -> AgdaAny
du_refl_298 T_TotalPreorder_222
v3
du_refl_298 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny
du_refl_298 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny
du_refl_298 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((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_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1))))
-- Relation.Binary.Bundles.TotalPreorder._.Eq.reflexive
d_reflexive_300 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_300 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_300 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_300 T_TotalPreorder_222
v3
du_reflexive_300 ::
  T_TotalPreorder_222 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_300 :: T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_300 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
            (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
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2)) AgdaAny
v3))
-- Relation.Binary.Bundles.TotalPreorder._.Eq.setoid
d_setoid_302 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> T_Setoid_44
d_setoid_302 :: () -> () -> () -> T_TotalPreorder_222 -> T_Setoid_44
d_setoid_302 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222 -> T_Setoid_44
du_setoid_302 T_TotalPreorder_222
v3
du_setoid_302 :: T_TotalPreorder_222 -> T_Setoid_44
du_setoid_302 :: T_TotalPreorder_222 -> T_Setoid_44
du_setoid_302 T_TotalPreorder_222
v0 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 ((T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0))
-- Relation.Binary.Bundles.TotalPreorder._.Eq.sym
d_sym_304 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_304 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_sym_304 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_304 T_TotalPreorder_222
v3
du_sym_304 ::
  T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_304 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_304 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> 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) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
-- Relation.Binary.Bundles.TotalPreorder._.Eq.trans
d_trans_306 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_306 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_306 ~()
v0 ~()
v1 ~()
v2 T_TotalPreorder_222
v3 = T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_306 T_TotalPreorder_222
v3
du_trans_306 ::
  T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_306 :: T_TotalPreorder_222
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_306 T_TotalPreorder_222
v0
  = let v1 :: t
v1 = (T_TotalPreorder_222 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_TotalPreorder_222 -> T_Preorder_132
du_preorder_252 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((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
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
-- Relation.Binary.Bundles.Poset
d_Poset_314 :: p -> p -> p -> ()
d_Poset_314 p
a0 p
a1 p
a2 = ()
newtype T_Poset_314
  = C_Poset'46'constructor_6389 MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
-- Relation.Binary.Bundles.Poset.Carrier
d_Carrier_330 :: T_Poset_314 -> ()
d_Carrier_330 :: T_Poset_314 -> ()
d_Carrier_330 = T_Poset_314 -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Poset._≈_
d__'8776'__332 :: T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8776'__332 :: T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8776'__332 = T_Poset_314 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Poset._≤_
d__'8804'__334 :: T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8804'__334 :: T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8804'__334 = T_Poset_314 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Poset.isPartialOrder
d_isPartialOrder_336 ::
  T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_isPartialOrder_336 :: T_Poset_314 -> T_IsPartialOrder_174
d_isPartialOrder_336 T_Poset_314
v0
  = case T_Poset_314 -> T_Poset_314
forall a b. a -> b
coe T_Poset_314
v0 of
      C_Poset'46'constructor_6389 T_IsPartialOrder_174
v4 -> T_IsPartialOrder_174 -> T_IsPartialOrder_174
forall a b. a -> b
coe T_IsPartialOrder_174
v4
      T_Poset_314
_ -> T_IsPartialOrder_174
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Bundles.Poset._.antisym
d_antisym_340 ::
  T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_340 :: T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_340 T_Poset_314
v0
  = (T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
      ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsPartialOrder_174
d_isPartialOrder_336 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
-- Relation.Binary.Bundles.Poset._.isPreorder
d_isPreorder_342 ::
  T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_342 :: T_Poset_314 -> T_IsPreorder_70
d_isPreorder_342 T_Poset_314
v0
  = (T_IsPartialOrder_174 -> T_IsPreorder_70)
-> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
      ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsPartialOrder_174
d_isPartialOrder_336 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
-- Relation.Binary.Bundles.Poset.preorder
d_preorder_344 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> T_Preorder_132
d_preorder_344 :: () -> () -> () -> T_Poset_314 -> T_Preorder_132
d_preorder_344 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314 -> T_Preorder_132
du_preorder_344 T_Poset_314
v3
du_preorder_344 :: T_Poset_314 -> T_Preorder_132
du_preorder_344 :: T_Poset_314 -> T_Preorder_132
du_preorder_344 T_Poset_314
v0
  = (T_IsPreorder_70 -> T_Preorder_132)
-> T_IsPreorder_70 -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
C_Preorder'46'constructor_2267
      (T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
         ((T_Poset_314 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe T_Poset_314 -> T_IsPartialOrder_174
d_isPartialOrder_336 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0)))
-- Relation.Binary.Bundles.Poset._._∼_
d__'8764'__348 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8764'__348 :: () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8764'__348 = () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Poset._._≳_
d__'8819'__350 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8819'__350 :: () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8819'__350 = () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Poset._._⋦_
d__'8934'__352 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8934'__352 :: () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8934'__352 = () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Poset._._⋧_
d__'8935'__354 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8935'__354 :: () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8935'__354 = () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Poset._.isEquivalence
d_isEquivalence_356 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_356 :: () -> () -> () -> T_Poset_314 -> T_IsEquivalence_26
d_isEquivalence_356 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314 -> T_IsEquivalence_26
du_isEquivalence_356 T_Poset_314
v3
du_isEquivalence_356 ::
  T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_356 :: T_Poset_314 -> T_IsEquivalence_26
du_isEquivalence_356 T_Poset_314
v0
  = (T_IsPreorder_70 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
      ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
         ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsPartialOrder_174
d_isPartialOrder_336 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0)))
-- Relation.Binary.Bundles.Poset._.refl
d_refl_358 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> AgdaAny -> AgdaAny
d_refl_358 :: () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny
d_refl_358 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314 -> AgdaAny -> AgdaAny
du_refl_358 T_Poset_314
v3
du_refl_358 :: T_Poset_314 -> AgdaAny -> AgdaAny
du_refl_358 :: T_Poset_314 -> AgdaAny -> AgdaAny
du_refl_358 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Poset._.reflexive
d_reflexive_360 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_360 :: ()
-> ()
-> ()
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_reflexive_360 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_360 T_Poset_314
v3
du_reflexive_360 ::
  T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_360 :: T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_360 T_Poset_314
v0
  = (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
      ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
         ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsPartialOrder_174
d_isPartialOrder_336 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0)))
-- Relation.Binary.Bundles.Poset._.trans
d_trans_362 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_362 :: ()
-> ()
-> ()
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_362 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_362 T_Poset_314
v3
du_trans_362 ::
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_362 :: T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_362 T_Poset_314
v0
  = (T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
      ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
         ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsPartialOrder_174
d_isPartialOrder_336 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0)))
-- Relation.Binary.Bundles.Poset._.∼-resp-≈
d_'8764''45'resp'45''8776'_364 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8764''45'resp'45''8776'_364 :: () -> () -> () -> T_Poset_314 -> T_Σ_14
d_'8764''45'resp'45''8776'_364 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3
  = T_Poset_314 -> T_Σ_14
du_'8764''45'resp'45''8776'_364 T_Poset_314
v3
du_'8764''45'resp'45''8776'_364 ::
  T_Poset_314 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8764''45'resp'45''8776'_364 :: T_Poset_314 -> T_Σ_14
du_'8764''45'resp'45''8776'_364 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'45''8776'_118
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Poset._.∼-respʳ-≈
d_'8764''45'resp'691''45''8776'_366 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'691''45''8776'_366 :: ()
-> ()
-> ()
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'691''45''8776'_366 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3
  = T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_366 T_Poset_314
v3
du_'8764''45'resp'691''45''8776'_366 ::
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_366 :: T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'691''45''8776'_366 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'691''45''8776'_116
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Poset._.∼-respˡ-≈
d_'8764''45'resp'737''45''8776'_368 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8764''45'resp'737''45''8776'_368 :: ()
-> ()
-> ()
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8764''45'resp'737''45''8776'_368 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3
  = T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_368 T_Poset_314
v3
du_'8764''45'resp'737''45''8776'_368 ::
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_368 :: T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8764''45'resp'737''45''8776'_368 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'737''45''8776'_114
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Poset._.≲-resp-≈
d_'8818''45'resp'45''8776'_370 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8818''45'resp'45''8776'_370 :: () -> () -> () -> T_Poset_314 -> T_Σ_14
d_'8818''45'resp'45''8776'_370 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3
  = T_Poset_314 -> T_Σ_14
du_'8818''45'resp'45''8776'_370 T_Poset_314
v3
du_'8818''45'resp'45''8776'_370 ::
  T_Poset_314 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8818''45'resp'45''8776'_370 :: T_Poset_314 -> T_Σ_14
du_'8818''45'resp'45''8776'_370 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'45''8776'_112
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Poset._.≲-respʳ-≈
d_'8818''45'resp'691''45''8776'_372 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8818''45'resp'691''45''8776'_372 :: ()
-> ()
-> ()
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8818''45'resp'691''45''8776'_372 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3
  = T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'691''45''8776'_372 T_Poset_314
v3
du_'8818''45'resp'691''45''8776'_372 ::
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'691''45''8776'_372 :: T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'691''45''8776'_372 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'691''45''8776'_106
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Poset._.≲-respˡ-≈
d_'8818''45'resp'737''45''8776'_374 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_'8818''45'resp'737''45''8776'_374 :: ()
-> ()
-> ()
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8818''45'resp'737''45''8776'_374 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3
  = T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'737''45''8776'_374 T_Poset_314
v3
du_'8818''45'resp'737''45''8776'_374 ::
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'737''45''8776'_374 :: T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_'8818''45'resp'737''45''8776'_374 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8818''45'resp'737''45''8776'_100
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Poset._.Eq._≈_
d__'8776'__378 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8776'__378 :: () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8776'__378 = () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Poset._.Eq._≉_
d__'8777'__380 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8777'__380 :: () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
d__'8777'__380 = () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Poset._.Eq.Carrier
d_Carrier_382 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> T_Poset_314 -> ()
d_Carrier_382 :: () -> () -> () -> T_Poset_314 -> ()
d_Carrier_382 = () -> () -> () -> T_Poset_314 -> ()
forall a. a
erased
-- Relation.Binary.Bundles.Poset._.Eq.isEquivalence
d_isEquivalence_384 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_384 :: () -> () -> () -> T_Poset_314 -> T_IsEquivalence_26
d_isEquivalence_384 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314 -> T_IsEquivalence_26
du_isEquivalence_384 T_Poset_314
v3
du_isEquivalence_384 ::
  T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_384 :: T_Poset_314 -> T_IsEquivalence_26
du_isEquivalence_384 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
         ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Poset._.Eq.isPartialEquivalence
d_isPartialEquivalence_386 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
d_isPartialEquivalence_386 :: () -> () -> () -> T_Poset_314 -> T_IsPartialEquivalence_16
d_isPartialEquivalence_386 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3
  = T_Poset_314 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_386 T_Poset_314
v3
du_isPartialEquivalence_386 ::
  T_Poset_314 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialEquivalence_16
du_isPartialEquivalence_386 :: T_Poset_314 -> T_IsPartialEquivalence_16
du_isPartialEquivalence_386 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> T_IsPartialEquivalence_16
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsEquivalence_26 -> T_IsPartialEquivalence_16)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> T_IsPartialEquivalence_16
MAlonzo.Code.Relation.Binary.Structures.du_isPartialEquivalence_42
            ((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
-- Relation.Binary.Bundles.Poset._.Eq.partialSetoid
d_partialSetoid_388 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> T_PartialSetoid_10
d_partialSetoid_388 :: () -> () -> () -> T_Poset_314 -> T_PartialSetoid_10
d_partialSetoid_388 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314 -> T_PartialSetoid_10
du_partialSetoid_388 T_Poset_314
v3
du_partialSetoid_388 :: T_Poset_314 -> T_PartialSetoid_10
du_partialSetoid_388 :: T_Poset_314 -> T_PartialSetoid_10
du_partialSetoid_388 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> T_PartialSetoid_10
forall a b. a -> b
coe ((T_Setoid_44 -> T_PartialSetoid_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_PartialSetoid_10
du_partialSetoid_70 ((T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)))
-- Relation.Binary.Bundles.Poset._.Eq.refl
d_refl_390 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> AgdaAny -> AgdaAny
d_refl_390 :: () -> () -> () -> T_Poset_314 -> AgdaAny -> AgdaAny
d_refl_390 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314 -> AgdaAny -> AgdaAny
du_refl_390 T_Poset_314
v3
du_refl_390 :: T_Poset_314 -> AgdaAny -> AgdaAny
du_refl_390 :: T_Poset_314 -> AgdaAny -> AgdaAny
du_refl_390 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((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_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1))))
-- Relation.Binary.Bundles.Poset._.Eq.reflexive
d_reflexive_392 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_392 :: ()
-> ()
-> ()
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_392 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_392 T_Poset_314
v3
du_reflexive_392 ::
  T_Poset_314 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_392 :: T_Poset_314 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_392 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
            (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
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2)) AgdaAny
v3))
-- Relation.Binary.Bundles.Poset._.Eq.setoid
d_setoid_394 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> T_Setoid_44
d_setoid_394 :: () -> () -> () -> T_Poset_314 -> T_Setoid_44
d_setoid_394 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314 -> T_Setoid_44
du_setoid_394 T_Poset_314
v3
du_setoid_394 :: T_Poset_314 -> T_Setoid_44
du_setoid_394 :: T_Poset_314 -> T_Setoid_44
du_setoid_394 T_Poset_314
v0 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 ((T_Poset_314 -> T_Preorder_132) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0))
-- Relation.Binary.Bundles.Poset._.Eq.sym
d_sym_396 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_396 :: ()
-> ()
-> ()
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_sym_396 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_396 T_Poset_314
v3
du_sym_396 ::
  T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_396 :: T_Poset_314 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_sym_396 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> 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) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> T_IsEquivalence_26
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
-- Relation.Binary.Bundles.Poset._.Eq.trans
d_trans_398 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_398 :: ()
-> ()
-> ()
-> T_Poset_314
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_398 ~()
v0 ~()
v1 ~()
v2 T_Poset_314
v3 = T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_398 T_Poset_314
v3
du_trans_398 ::
  T_Poset_314 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_398 :: T_Poset_314
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_trans_398 T_Poset_314
v0
  = let v1 :: t
v1 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (T_Poset_314 -> AgdaAny
forall a b. a -> b
coe T_Poset_314
v0) in
    AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_Preorder_132 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe T_Preorder_132 -> T_Setoid_44
du_setoid_180 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((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
d_isEquivalence_60 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
-- Relation.Binary.Bundles.DecPoset
d_DecPoset_406 :: p -> p -> p -> ()
d_DecPoset_406 p
a0 p
a1 p
a2 = ()
newtype T_DecPoset_406
  = C_DecPoset'46'constructor_8213 MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224
-- Relation.Binary.Bundles.DecPoset.Carrier
d_Carrier_422 :: T_DecPoset_406 -> ()
d_Carrier_422 :: T_DecPoset_406 -> ()
d_Carrier_422 = T_DecPoset_406 -> ()
forall a. a
erased
-- Relation.Binary.Bundles.DecPoset._≈_
d__'8776'__424 :: T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8776'__424 :: T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8776'__424 = T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.DecPoset._≤_
d__'8804'__426 :: T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8804'__426 :: T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8804'__426 = T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.DecPoset.isDecPartialOrder
d_isDecPartialOrder_428 ::
  T_DecPoset_406 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224
d_isDecPartialOrder_428 :: T_DecPoset_406 -> T_IsDecPartialOrder_224
d_isDecPartialOrder_428 T_DecPoset_406
v0
  = case T_DecPoset_406 -> T_DecPoset_406
forall a b. a -> b
coe T_DecPoset_406
v0 of
      C_DecPoset'46'constructor_8213 T_IsDecPartialOrder_224
v4 -> T_IsDecPartialOrder_224 -> T_IsDecPartialOrder_224
forall a b. a -> b
coe T_IsDecPartialOrder_224
v4
      T_DecPoset_406
_ -> T_IsDecPartialOrder_224
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Bundles.DecPoset.DPO._≟_
d__'8799'__432 ::
  T_DecPoset_406 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__432 :: T_DecPoset_406 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8799'__432 T_DecPoset_406
v0
  = (T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__236
      ((T_DecPoset_406 -> T_IsDecPartialOrder_224) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406 -> T_IsDecPartialOrder_224
d_isDecPartialOrder_428 (T_DecPoset_406 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406
v0))
-- Relation.Binary.Bundles.DecPoset.DPO._≤?_
d__'8804''63'__434 ::
  T_DecPoset_406 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8804''63'__434 :: T_DecPoset_406 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8804''63'__434 T_DecPoset_406
v0
  = (T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      T_IsDecPartialOrder_224 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8804''63'__238
      ((T_DecPoset_406 -> T_IsDecPartialOrder_224) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406 -> T_IsDecPartialOrder_224
d_isDecPartialOrder_428 (T_DecPoset_406 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406
v0))
-- Relation.Binary.Bundles.DecPoset.DPO.isPartialOrder
d_isPartialOrder_440 ::
  T_DecPoset_406 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_isPartialOrder_440 :: T_DecPoset_406 -> T_IsPartialOrder_174
d_isPartialOrder_440 T_DecPoset_406
v0
  = (T_IsDecPartialOrder_224 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
      T_IsDecPartialOrder_224 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_234
      ((T_DecPoset_406 -> T_IsDecPartialOrder_224) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406 -> T_IsDecPartialOrder_224
d_isDecPartialOrder_428 (T_DecPoset_406 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406
v0))
-- Relation.Binary.Bundles.DecPoset.poset
d_poset_480 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 -> T_Poset_314
d_poset_480 :: () -> () -> () -> T_DecPoset_406 -> T_Poset_314
d_poset_480 ~()
v0 ~()
v1 ~()
v2 T_DecPoset_406
v3 = T_DecPoset_406 -> T_Poset_314
du_poset_480 T_DecPoset_406
v3
du_poset_480 :: T_DecPoset_406 -> T_Poset_314
du_poset_480 :: T_DecPoset_406 -> T_Poset_314
du_poset_480 T_DecPoset_406
v0
  = (T_IsPartialOrder_174 -> T_Poset_314)
-> T_IsPartialOrder_174 -> T_Poset_314
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_Poset_314
C_Poset'46'constructor_6389
      (T_IsDecPartialOrder_224 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_234
         ((T_DecPoset_406 -> T_IsDecPartialOrder_224)
-> AgdaAny -> T_IsDecPartialOrder_224
forall a b. a -> b
coe T_DecPoset_406 -> T_IsDecPartialOrder_224
d_isDecPartialOrder_428 (T_DecPoset_406 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406
v0)))
-- Relation.Binary.Bundles.DecPoset._._∼_
d__'8764'__484 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8764'__484 :: () -> () -> () -> T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8764'__484 = () -> () -> () -> T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.DecPoset._._≳_
d__'8819'__486 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8819'__486 :: () -> () -> () -> T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8819'__486 = () -> () -> () -> T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.DecPoset._._⋦_
d__'8934'__488 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8934'__488 :: () -> () -> () -> T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8934'__488 = () -> () -> () -> T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.DecPoset._._⋧_
d__'8935'__490 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8935'__490 :: () -> () -> () -> T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
d__'8935'__490 = () -> () -> () -> T_DecPoset_406 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Relation.Binary.Bundles.DecPoset._.antisym
d_antisym_492 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antisym_492 :: ()
-> ()
-> ()
-> T_DecPoset_406
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antisym_492 ~()
v0 ~()
v1 ~()
v2 T_DecPoset_406
v3 = T_DecPoset_406
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_492 T_DecPoset_406
v3
du_antisym_492 ::
  T_DecPoset_406 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_492 :: T_DecPoset_406
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antisym_492 T_DecPoset_406
v0
  = (T_IsPartialOrder_174
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPartialOrder_174
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_184
      ((T_IsDecPartialOrder_224 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecPartialOrder_224 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_234
         ((T_DecPoset_406 -> T_IsDecPartialOrder_224) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406 -> T_IsDecPartialOrder_224
d_isDecPartialOrder_428 (T_DecPoset_406 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406
v0)))
-- Relation.Binary.Bundles.DecPoset._.isEquivalence
d_isEquivalence_494 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_494 :: () -> () -> () -> T_DecPoset_406 -> T_IsEquivalence_26
d_isEquivalence_494 ~()
v0 ~()
v1 ~()
v2 T_DecPoset_406
v3 = T_DecPoset_406 -> T_IsEquivalence_26
du_isEquivalence_494 T_DecPoset_406
v3
du_isEquivalence_494 ::
  T_DecPoset_406 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_494 :: T_DecPoset_406 -> T_IsEquivalence_26
du_isEquivalence_494 T_DecPoset_406
v0
  = let v1 :: t
v1 = (T_DecPoset_406 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_DecPoset_406 -> T_Poset_314
du_poset_480 (T_DecPoset_406 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406
v0) in
    AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
         ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
            ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsPartialOrder_174
d_isPartialOrder_336 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1))))
-- Relation.Binary.Bundles.DecPoset._.isPreorder
d_isPreorder_496 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_496 :: () -> () -> () -> T_DecPoset_406 -> T_IsPreorder_70
d_isPreorder_496 ~()
v0 ~()
v1 ~()
v2 T_DecPoset_406
v3 = T_DecPoset_406 -> T_IsPreorder_70
du_isPreorder_496 T_DecPoset_406
v3
du_isPreorder_496 ::
  T_DecPoset_406 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_isPreorder_496 :: T_DecPoset_406 -> T_IsPreorder_70
du_isPreorder_496 T_DecPoset_406
v0
  = (T_IsPartialOrder_174 -> T_IsPreorder_70)
-> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
      ((T_IsDecPartialOrder_224 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecPartialOrder_224 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_234
         ((T_DecPoset_406 -> T_IsDecPartialOrder_224) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406 -> T_IsDecPartialOrder_224
d_isDecPartialOrder_428 (T_DecPoset_406 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406
v0)))
-- Relation.Binary.Bundles.DecPoset._.preorder
d_preorder_498 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 -> T_Preorder_132
d_preorder_498 :: () -> () -> () -> T_DecPoset_406 -> T_Preorder_132
d_preorder_498 ~()
v0 ~()
v1 ~()
v2 T_DecPoset_406
v3 = T_DecPoset_406 -> T_Preorder_132
du_preorder_498 T_DecPoset_406
v3
du_preorder_498 :: T_DecPoset_406 -> T_Preorder_132
du_preorder_498 :: T_DecPoset_406 -> T_Preorder_132
du_preorder_498 T_DecPoset_406
v0
  = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 ((T_DecPoset_406 -> T_Poset_314) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406 -> T_Poset_314
du_poset_480 (T_DecPoset_406 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406
v0))
-- Relation.Binary.Bundles.DecPoset._.refl
d_refl_500 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 -> AgdaAny -> AgdaAny
d_refl_500 :: () -> () -> () -> T_DecPoset_406 -> AgdaAny -> AgdaAny
d_refl_500 ~()
v0 ~()
v1 ~()
v2 T_DecPoset_406
v3 = T_DecPoset_406 -> AgdaAny -> AgdaAny
du_refl_500 T_DecPoset_406
v3
du_refl_500 :: T_DecPoset_406 -> AgdaAny -> AgdaAny
du_refl_500 :: T_DecPoset_406 -> AgdaAny -> AgdaAny
du_refl_500 T_DecPoset_406
v0
  = let v1 :: t
v1 = (T_DecPoset_406 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_DecPoset_406 -> T_Poset_314
du_poset_480 (T_DecPoset_406 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406
v0) in
    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v2 :: t
v2 = (T_Poset_314 -> T_Preorder_132) -> AgdaAny -> t
forall a b. a -> b
coe T_Poset_314 -> T_Preorder_132
du_preorder_344 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsPreorder_70 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
            ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
d_isPreorder_154 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2))))
-- Relation.Binary.Bundles.DecPoset._.reflexive
d_reflexive_502 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_502 :: ()
-> ()
-> ()
-> T_DecPoset_406
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_reflexive_502 ~()
v0 ~()
v1 ~()
v2 T_DecPoset_406
v3 = T_DecPoset_406 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_502 T_DecPoset_406
v3
du_reflexive_502 ::
  T_DecPoset_406 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_502 :: T_DecPoset_406 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_reflexive_502 T_DecPoset_406
v0
  = let v1 :: t
v1 = (T_DecPoset_406 -> T_Poset_314) -> AgdaAny -> t
forall a b. a -> b
coe T_DecPoset_406 -> T_Poset_314
du_poset_480 (T_DecPoset_406 -> AgdaAny
forall a b. a -> b
coe T_DecPoset_406
v0) in
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      ((T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
         ((T_IsPartialOrder_174 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_174 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182
            ((T_Poset_314 -> T_IsPartialOrder_174) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Poset_314 -> T_IsPartialOrder_174
d_isPartialOrder_336 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1))))
-- Relation.Binary.Bundles.DecPoset._.trans
d_trans_504 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_DecPoset_406 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_504 :: ()
-> ()
-> ()
-> T_DecPoset_406
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_504 ~()