| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Function.Construct.Composition
Documentation
d_congruent_50 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_congruent_50 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_injective_56 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_injective_56 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_surjective_62 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → (AgdaAny → T_Σ_14) → AgdaAny → T_Σ_14 Source #
du_surjective_62 ∷ (AgdaAny → AgdaAny) → (AgdaAny → T_Σ_14) → (AgdaAny → T_Σ_14) → AgdaAny → T_Σ_14 Source #
d_bijective_102 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_inverse'737'_134 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_inverse'737'_134 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_inverse'691'_140 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_inverse'691'_140 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_inverse'7495'_146 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_inverse'7495'_146 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_isCongruent_174 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsCongruent_22 → T_IsCongruent_22 Source #
du_isCongruent_174 ∷ (AgdaAny → AgdaAny) → T_IsCongruent_22 → T_IsCongruent_22 → T_IsCongruent_22 Source #
d_isInjection_304 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInjection_98 → T_IsInjection_98 → T_IsInjection_98 Source #
du_isInjection_304 ∷ (AgdaAny → AgdaAny) → T_IsInjection_98 → T_IsInjection_98 → T_IsInjection_98 Source #
d_isSurjection_442 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_IsSurjection_174 → T_IsSurjection_174 Source #
du_isSurjection_442 ∷ (AgdaAny → AgdaAny) → T_IsSurjection_174 → T_IsSurjection_174 → T_IsSurjection_174 Source #
d_isBijection_584 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsBijection_256 → T_IsBijection_256 Source #
du_isBijection_584 ∷ (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsBijection_256 → T_IsBijection_256 Source #
d_isLeftInverse_772 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsLeftInverse_346 → T_IsLeftInverse_346 Source #
du_isLeftInverse_772 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsLeftInverse_346 → T_IsLeftInverse_346 Source #
d_isRightInverse_922 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsRightInverse_438 → T_IsRightInverse_438 Source #
du_isRightInverse_922 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsRightInverse_438 → T_IsRightInverse_438 Source #
d_isInverse_1068 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsInverse_526 → T_IsInverse_526 Source #
du_isInverse_1068 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsInverse_526 → T_IsInverse_526 Source #
d_function_1260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → T_Func_774 → T_Func_774 → T_Func_774 Source #
d_injection_1390 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → T_Injection_842 → T_Injection_842 → T_Injection_842 Source #
d_surjection_1532 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_Surjection_918 → T_Surjection_918 Source #
d_bijection_1686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_Bijection_1004 → T_Bijection_1004 Source #
d_equivalence_1852 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_Equivalence_1858 → T_Equivalence_1858 Source #
d_leftInverse_2002 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_LeftInverse_1942 → T_LeftInverse_1942 Source #
d_rightInverse_2168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_RightInverse_2036 → T_RightInverse_2036 Source #
d_inverse_2322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → T_Inverse_2122 → T_Inverse_2122 → T_Inverse_2122 Source #
d__'10230''45''8728'__2496 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Func_774 → T_Func_774 → T_Func_774 Source #
d__'8611''45''8728'__2498 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Injection_842 → T_Injection_842 → T_Injection_842 Source #
d__'8608''45''8728'__2500 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Surjection_918 → T_Surjection_918 → T_Surjection_918 Source #
d__'10518''45''8728'__2502 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Bijection_1004 → T_Bijection_1004 → T_Bijection_1004 Source #
d__'8660''45''8728'__2504 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Equivalence_1858 → T_Equivalence_1858 → T_Equivalence_1858 Source #
d__'8617''45''8728'__2506 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1942 → T_LeftInverse_1942 → T_LeftInverse_1942 Source #
d__'8618''45''8728'__2508 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_RightInverse_2036 → T_RightInverse_2036 → T_RightInverse_2036 Source #
du__'8618''45''8728'__2508 ∷ T_RightInverse_2036 → T_RightInverse_2036 → T_RightInverse_2036 Source #
d__'8596''45''8728'__2510 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_Inverse_2122 → T_Inverse_2122 Source #
d__'8728''45''10230'__2512 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Func_774 → T_Func_774 → T_Func_774 Source #
d__'8728''45''8611'__2514 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Injection_842 → T_Injection_842 → T_Injection_842 Source #
d__'8728''45''8608'__2516 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Surjection_918 → T_Surjection_918 → T_Surjection_918 Source #
d__'8728''45''10518'__2518 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Bijection_1004 → T_Bijection_1004 → T_Bijection_1004 Source #
d__'8728''45''8660'__2520 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Equivalence_1858 → T_Equivalence_1858 → T_Equivalence_1858 Source #
d__'8728''45''8617'__2522 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1942 → T_LeftInverse_1942 → T_LeftInverse_1942 Source #
d__'8728''45''8618'__2524 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_RightInverse_2036 → T_RightInverse_2036 → T_RightInverse_2036 Source #
d__'8728''45''8596'__2526 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_Inverse_2122 → T_Inverse_2122 Source #