Safe Haskell	None

MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Bundles

Documentation

d_IndexedSetoid_18 :: p1 -> p2 -> p3 -> p4 -> () Source #

newtype T_IndexedSetoid_18 Source #

Constructors

C_IndexedSetoid'46'constructor_285 T_IsIndexedEquivalence_22

d_Carrier_34 :: T_IndexedSetoid_18 -> AgdaAny -> () Source #

d__'8776'__36 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> () Source #

d_isEquivalence_38 :: T_IndexedSetoid_18 -> T_IsIndexedEquivalence_22 Source #

d_refl_42 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_reflexive_44 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_44 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_46 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_48 :: T_IndexedSetoid_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IndexedPreorder_60 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

newtype T_IndexedPreorder_60 Source #

Constructors

C_IndexedPreorder'46'constructor_1439 T_IsIndexedPreorder_44

d_Carrier_80 :: T_IndexedPreorder_60 -> AgdaAny -> () Source #

d__'8776'__82 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> () Source #

d__'8764'__84 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> () Source #

d_isPreorder_86 :: T_IndexedPreorder_60 -> T_IsIndexedPreorder_44 Source #

d_isEquivalence_90 :: T_IndexedPreorder_60 -> T_IsIndexedEquivalence_22 Source #

d_refl_92 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_refl_92 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_reflexive_94 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_96 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_100 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_reflexive_102 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_102 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_104 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_106 :: T_IndexedPreorder_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #