{-# 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.Indexed.Heterogeneous.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.Primitive
import qualified MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures
d_IndexedSetoid_18 :: p -> p -> p -> p -> ()
d_IndexedSetoid_18 p
a0 p
a1 p
a2 p
a3 = ()
newtype T_IndexedSetoid_18
= C_IndexedSetoid'46'constructor_445 MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedEquivalence_22
d_Carrier_34 :: T_IndexedSetoid_18 -> AgdaAny -> ()
d_Carrier_34 :: T_IndexedSetoid_18 -> AgdaAny -> ()
d_Carrier_34 = T_IndexedSetoid_18 -> AgdaAny -> ()
forall a. a
erased
d__'8776'__36 ::
T_IndexedSetoid_18 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8776'__36 :: T_IndexedSetoid_18
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8776'__36 = T_IndexedSetoid_18
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
d_isEquivalence_38 ::
T_IndexedSetoid_18 ->
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedEquivalence_22
d_isEquivalence_38 :: T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
d_isEquivalence_38 T_IndexedSetoid_18
v0
= case T_IndexedSetoid_18 -> T_IndexedSetoid_18
forall a b. a -> b
coe T_IndexedSetoid_18
v0 of
C_IndexedSetoid'46'constructor_445 T_IsIndexedEquivalence_22
v3 -> T_IsIndexedEquivalence_22 -> T_IsIndexedEquivalence_22
forall a b. a -> b
coe T_IsIndexedEquivalence_22
v3
T_IndexedSetoid_18
_ -> T_IsIndexedEquivalence_22
forall a. a
MAlonzo.RTE.mazUnreachableError
d_refl_42 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_42 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_42 T_IndexedSetoid_18
v0
= (T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_refl_30
((T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
d_isEquivalence_38 (T_IndexedSetoid_18 -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18
v0))
d_reflexive_44 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
T_IndexedSetoid_18 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_44 :: ()
-> ()
-> ()
-> ()
-> T_IndexedSetoid_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_44 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_IndexedSetoid_18
v4 = T_IndexedSetoid_18
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_44 T_IndexedSetoid_18
v4
du_reflexive_44 ::
T_IndexedSetoid_18 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_44 :: T_IndexedSetoid_18
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_44 T_IndexedSetoid_18
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T__'8801'__12
v4
= (T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.du_reflexive_38
((T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
d_isEquivalence_38 (T_IndexedSetoid_18 -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18
v0)) AgdaAny
v1 AgdaAny
v2
d_sym_46 ::
T_IndexedSetoid_18 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_46 :: T_IndexedSetoid_18
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_46 T_IndexedSetoid_18
v0
= (T_IsIndexedEquivalence_22
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsIndexedEquivalence_22
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_sym_32
((T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
d_isEquivalence_38 (T_IndexedSetoid_18 -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18
v0))
d_trans_48 ::
T_IndexedSetoid_18 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_48 :: T_IndexedSetoid_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_48 T_IndexedSetoid_18
v0
= (T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_trans_34
((T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22
d_isEquivalence_38 (T_IndexedSetoid_18 -> AgdaAny
forall a b. a -> b
coe T_IndexedSetoid_18
v0))
d_IndexedPreorder_60 :: p -> p -> p -> p -> p -> ()
d_IndexedPreorder_60 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
newtype T_IndexedPreorder_60
= C_IndexedPreorder'46'constructor_1981 MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedPreorder_44
d_Carrier_80 :: T_IndexedPreorder_60 -> AgdaAny -> ()
d_Carrier_80 :: T_IndexedPreorder_60 -> AgdaAny -> ()
d_Carrier_80 = T_IndexedPreorder_60 -> AgdaAny -> ()
forall a. a
erased
d__'8776'__82 ::
T_IndexedPreorder_60 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8776'__82 :: T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8776'__82 = T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
d__'8764'__84 ::
T_IndexedPreorder_60 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8764'__84 :: T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
d__'8764'__84 = T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
d_isPreorder_86 ::
T_IndexedPreorder_60 ->
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedPreorder_44
d_isPreorder_86 :: T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 T_IndexedPreorder_60
v0
= case T_IndexedPreorder_60 -> T_IndexedPreorder_60
forall a b. a -> b
coe T_IndexedPreorder_60
v0 of
C_IndexedPreorder'46'constructor_1981 T_IsIndexedPreorder_44
v4 -> T_IsIndexedPreorder_44 -> T_IsIndexedPreorder_44
forall a b. a -> b
coe T_IsIndexedPreorder_44
v4
T_IndexedPreorder_60
_ -> T_IsIndexedPreorder_44
forall a. a
MAlonzo.RTE.mazUnreachableError
d_isEquivalence_90 ::
T_IndexedPreorder_60 ->
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.T_IsIndexedEquivalence_22
d_isEquivalence_90 :: T_IndexedPreorder_60 -> T_IsIndexedEquivalence_22
d_isEquivalence_90 T_IndexedPreorder_60
v0
= (T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> T_IsIndexedEquivalence_22
forall a b. a -> b
coe
T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_isEquivalence_60
((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0))
d_refl_92 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_92 :: ()
-> ()
-> ()
-> ()
-> ()
-> T_IndexedPreorder_60
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_refl_92 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 T_IndexedPreorder_60
v5 = T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
du_refl_92 T_IndexedPreorder_60
v5
du_refl_92 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
du_refl_92 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
du_refl_92 T_IndexedPreorder_60
v0
= (T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.du_refl_80
((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0))
d_reflexive_94 ::
T_IndexedPreorder_60 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_94 :: T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_reflexive_94 T_IndexedPreorder_60
v0
= (T_IsIndexedPreorder_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsIndexedPreorder_44
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_reflexive_66
((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0))
d_trans_96 ::
T_IndexedPreorder_60 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_96 :: T_IndexedPreorder_60
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_96 T_IndexedPreorder_60
v0
= (T_IsIndexedPreorder_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsIndexedPreorder_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_trans_68
((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0))
d_refl_100 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_100 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny
d_refl_100 T_IndexedPreorder_60
v0
= (T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_refl_30
((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_isEquivalence_60
((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0)))
d_reflexive_102 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
T_IndexedPreorder_60 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_reflexive_102 :: ()
-> ()
-> ()
-> ()
-> ()
-> T_IndexedPreorder_60
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_reflexive_102 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 T_IndexedPreorder_60
v5 = T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_102 T_IndexedPreorder_60
v5
du_reflexive_102 ::
T_IndexedPreorder_60 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_reflexive_102 :: T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
du_reflexive_102 T_IndexedPreorder_60
v0
= let v1 :: T_IsIndexedPreorder_44
v1 = T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> T_IndexedPreorder_60
forall a b. a -> b
coe T_IndexedPreorder_60
v0) in
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
(T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.du_reflexive_38
((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_isEquivalence_60
(T_IsIndexedPreorder_44 -> AgdaAny
forall a b. a -> b
coe T_IsIndexedPreorder_44
v1))
AgdaAny
v2 AgdaAny
v3)
d_sym_104 ::
T_IndexedPreorder_60 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_104 :: T_IndexedPreorder_60
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_104 T_IndexedPreorder_60
v0
= (T_IsIndexedEquivalence_22
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsIndexedEquivalence_22
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_sym_32
((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_isEquivalence_60
((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0)))
d_trans_106 ::
T_IndexedPreorder_60 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_106 :: T_IndexedPreorder_60
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans_106 T_IndexedPreorder_60
v0
= (T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_IsIndexedEquivalence_22
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_trans_34
((T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22
MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures.d_isEquivalence_60
((T_IndexedPreorder_60 -> T_IsIndexedPreorder_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60 -> T_IsIndexedPreorder_44
d_isPreorder_86 (T_IndexedPreorder_60 -> AgdaAny
forall a b. a -> b
coe T_IndexedPreorder_60
v0)))