| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Function.Surjection
Documentation
d_Surjective_18 ∷ p → p → p → p → p → p → p → () Source #
data T_Surjective_18 Source #
Constructors
| C_Surjective'46'constructor_1229 T_Π_16 (AgdaAny → AgdaAny) |
d_Surjection_54 ∷ p → p → p → p → p → p → () Source #
data T_Surjection_54 Source #
Constructors
| C_Surjection'46'constructor_2369 T_Π_16 T_Surjective_18 |
d_right'45'inverse_82 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_54 → T_LeftInverse_82 Source #
d_to'45'from_86 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_54 → T_Injection_88 Source #
d_equivalence_92 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Surjection_54 → T_Equivalence_16 Source #
d_fromRightInverse_106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_82 → T_Surjection_54 Source #
d__'8608'__134 ∷ T_Level_18 → T_Level_18 → () → () → () Source #
d_surjection_154 ∷ T_Level_18 → T_Level_18 → () → () → (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__'8728'__196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 → T_Surjection_54 → T_Surjection_54 → T_Surjection_54 Source #