Safe Haskell	None

MAlonzo.Code.Relation.Binary.Indexed.Heterogeneous.Structures

Documentation

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

data T_IsIndexedEquivalence_22 Source #

Constructors

C_IsIndexedEquivalence'46'constructor_719 (AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_refl_30 :: T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_sym_32 :: T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_34 :: T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_reflexive_38 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) -> T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_38 :: T_IsIndexedEquivalence_22 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_IsIndexedPreorder_44 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

data T_IsIndexedPreorder_44 Source #

Constructors

C_IsIndexedPreorder'46'constructor_3265 T_IsIndexedEquivalence_22 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_isEquivalence_60 :: T_IsIndexedPreorder_44 -> T_IsIndexedEquivalence_22 Source #

d_reflexive_66 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_68 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_72 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_reflexive_74 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) -> T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

du_reflexive_74 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny Source #

d_sym_76 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_78 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_refl_80 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> ()) -> T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_refl_80 :: T_IsIndexedPreorder_44 -> AgdaAny -> AgdaAny -> AgdaAny Source #