Safe Haskell	None

MAlonzo.Code.Function.Surjection

Documentation

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

data T_Surjective_18 Source #

Constructors

C_Surjective'46'constructor_867 T_Π_16 (AgdaAny -> AgdaAny)

d_from_38 :: T_Surjective_18 -> T_Π_16 Source #

d_right'45'inverse'45'of_40 :: T_Surjective_18 -> AgdaAny -> AgdaAny Source #

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

data T_Surjection_54 Source #

Constructors

C_Surjection'46'constructor_1733 T_Π_16 T_Surjective_18

d_to_72 :: T_Surjection_54 -> T_Π_16 Source #

d_surjective_74 :: T_Surjection_54 -> T_Surjective_18 Source #

d_from_78 :: T_Surjection_54 -> T_Π_16 Source #

d_right'45'inverse'45'of_80 :: T_Surjection_54 -> AgdaAny -> AgdaAny Source #

d_right'45'inverse_82 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_54 -> T_LeftInverse_82 Source #

du_right'45'inverse_82 :: T_Surjection_54 -> T_LeftInverse_82 Source #

d_to'45'from_86 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_54 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_to'45'from_86 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_54 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injective_88 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_54 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_injective_88 :: T_Setoid_44 -> T_Surjection_54 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injection_90 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_54 -> T_Injection_88 Source #

du_injection_90 :: T_Setoid_44 -> T_Surjection_54 -> T_Injection_88 Source #

d_equivalence_92 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_54 -> T_Equivalence_16 Source #

du_equivalence_92 :: T_Surjection_54 -> T_Equivalence_16 Source #

d_fromRightInverse_106 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_82 -> T_Surjection_54 Source #

du_fromRightInverse_106 :: T_LeftInverse_82 -> T_Surjection_54 Source #

d__'8608'__134 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d_surjection_154 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T_Surjection_54 Source #

du_surjection_154 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T_Surjection_54 Source #

d_id_168 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Surjection_54 Source #

du_id_168 :: T_Setoid_44 -> T_Surjection_54 Source #

d_id'8242'_176 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_LeftInverse_82 Source #

du_id'8242'_176 :: T_Setoid_44 -> T_LeftInverse_82 Source #

d__'8728'__196 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54 Source #

du__'8728'__196 :: T_Setoid_44 -> T_Surjection_54 -> T_Surjection_54 -> T_Surjection_54 Source #

d_g'8728'f_206 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82 Source #

du_g'8728'f_206 :: T_Setoid_44 -> T_Surjection_54 -> T_Surjection_54 -> T_LeftInverse_82 Source #