| 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_296 ∷ 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_92 → T_IsInjection_92 → T_IsInjection_92 Source #
du_isInjection_296 ∷ (AgdaAny → AgdaAny) → T_IsInjection_92 → T_IsInjection_92 → T_IsInjection_92 Source #
d_isSurjection_426 ∷ 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_162 → T_IsSurjection_162 → T_IsSurjection_162 Source #
du_isSurjection_426 ∷ (AgdaAny → AgdaAny) → T_IsSurjection_162 → T_IsSurjection_162 → T_IsSurjection_162 Source #
d_isBijection_560 ∷ 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_238 → T_IsBijection_238 → T_IsBijection_238 Source #
du_isBijection_560 ∷ (AgdaAny → AgdaAny) → T_IsBijection_238 → T_IsBijection_238 → T_IsBijection_238 Source #
d_isLeftInverse_740 ∷ 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_322 → T_IsLeftInverse_322 → T_IsLeftInverse_322 Source #
du_isLeftInverse_740 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_IsLeftInverse_322 → T_IsLeftInverse_322 Source #
d_isRightInverse_882 ∷ 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_408 → T_IsRightInverse_408 → T_IsRightInverse_408 Source #
du_isRightInverse_882 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → T_IsRightInverse_408 → T_IsRightInverse_408 Source #
d_isInverse_1020 ∷ 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_490 → T_IsInverse_490 → T_IsInverse_490 Source #
du_isInverse_1020 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_IsInverse_490 → T_IsInverse_490 Source #
d_function_1204 ∷ 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_Func_714 → T_Func_714 → T_Func_714 Source #
d_injection_1326 ∷ 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_Injection_776 → T_Injection_776 → T_Injection_776 Source #
d_surjection_1460 ∷ 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_846 → T_Surjection_846 → T_Surjection_846 Source #
d_bijection_1606 ∷ 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_Bijection_926 → T_Bijection_926 → T_Bijection_926 Source #
d_equivalence_1764 ∷ 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_Equivalence_1714 → T_Equivalence_1714 → T_Equivalence_1714 Source #
d_leftInverse_1906 ∷ 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_LeftInverse_1792 → T_LeftInverse_1792 → T_LeftInverse_1792 Source #
d_rightInverse_2064 ∷ 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_RightInverse_1880 → T_RightInverse_1880 → T_RightInverse_1880 Source #
d_inverse_2210 ∷ 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_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #
d__'10230''45''8728'__2376 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Func_714 → T_Func_714 → T_Func_714 Source #
d__'8611''45''8728'__2378 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Injection_776 → T_Injection_776 → T_Injection_776 Source #
d__'8608''45''8728'__2380 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Surjection_846 → T_Surjection_846 → T_Surjection_846 Source #
d__'10518''45''8728'__2382 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Bijection_926 → T_Bijection_926 → T_Bijection_926 Source #
d__'8660''45''8728'__2384 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Equivalence_1714 → T_Equivalence_1714 → T_Equivalence_1714 Source #
d__'8617''45''8728'__2386 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1792 → T_LeftInverse_1792 → T_LeftInverse_1792 Source #
d__'8618''45''8728'__2388 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_RightInverse_1880 → T_RightInverse_1880 → T_RightInverse_1880 Source #
du__'8618''45''8728'__2388 ∷ T_RightInverse_1880 → T_RightInverse_1880 → T_RightInverse_1880 Source #
d__'8596''45''8728'__2390 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #
d__'8728''45''10230'__2392 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Func_714 → T_Func_714 → T_Func_714 Source #
d__'8728''45''8611'__2394 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Injection_776 → T_Injection_776 → T_Injection_776 Source #
d__'8728''45''8608'__2396 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Surjection_846 → T_Surjection_846 → T_Surjection_846 Source #
d__'8728''45''10518'__2398 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Bijection_926 → T_Bijection_926 → T_Bijection_926 Source #
d__'8728''45''8660'__2400 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Equivalence_1714 → T_Equivalence_1714 → T_Equivalence_1714 Source #
d__'8728''45''8617'__2402 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1792 → T_LeftInverse_1792 → T_LeftInverse_1792 Source #
d__'8728''45''8618'__2404 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_RightInverse_1880 → T_RightInverse_1880 → T_RightInverse_1880 Source #
d__'8728''45''8596'__2406 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #