| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Function.Construct.Symmetry
Documentation
d_f'8315''185'_48 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_Σ_14 → AgdaAny → AgdaAny Source #
d_f'8728'f'8315''185''8801'id_50 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_injective_52 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_injective_52 ∷ (AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_surjective_64 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 Source #
du_surjective_64 ∷ (AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 Source #
d_bijective_72 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
du_bijective_72 ∷ (AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
d_inverse'691'_102 ∷ 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 Source #
du_inverse'691'_102 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_inverse'737'_106 ∷ 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 Source #
du_inverse'737'_106 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_inverse'7495'_110 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
d_f'8315''185'_206 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → AgdaAny → AgdaAny Source #
d_isBijection_208 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsBijection_238 Source #
du_isBijection_208 ∷ (AgdaAny → AgdaAny) → T_IsBijection_238 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsBijection_238 Source #
d_isBijection'45''8801'_228 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_238 → T_IsBijection_238 Source #
d_isCongruent_324 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsCongruent_22 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsCongruent_22 Source #
du_isCongruent_324 ∷ T_IsCongruent_22 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsCongruent_22 Source #
d_isLeftInverse_390 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_408 → T_IsLeftInverse_322 Source #
d_isRightInverse_462 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_322 → T_IsRightInverse_408 Source #
d_isInverse_536 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_490 → T_IsInverse_490 Source #
d__'8776'__666 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny → () Source #
d__'8776'__690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny → () Source #
d_from_712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny Source #
d_bijection_714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Bijection_926 Source #
du_bijection_714 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Bijection_926 Source #
d_bijection'45''8801'_722 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → () → T_Bijection_926 → T_Bijection_926 Source #
d_equivalence_820 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Equivalence_1714 → T_Equivalence_1714 Source #
d_rightInverse_894 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_1792 → T_RightInverse_1880 Source #
d_leftInverse_976 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → T_LeftInverse_1792 Source #
d_inverse_1052 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → T_Inverse_1960 Source #
d_'10518''45'sym_1138 ∷ T_Level_18 → () → T_Level_18 → () → T_Bijection_926 → T_Bijection_926 Source #
d_'8660''45'sym_1142 ∷ T_Level_18 → () → T_Level_18 → () → T_Equivalence_1714 → T_Equivalence_1714 Source #
d_'8617''45'sym_1144 ∷ T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1792 → T_RightInverse_1880 Source #
d_'8618''45'sym_1146 ∷ T_Level_18 → () → T_Level_18 → () → T_RightInverse_1880 → T_LeftInverse_1792 Source #
d_'8596''45'sym_1148 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Inverse_1960 Source #
d_sym'45''10518'_1150 ∷ T_Level_18 → () → T_Level_18 → () → T_Bijection_926 → T_Bijection_926 Source #
d_sym'45''8660'_1152 ∷ T_Level_18 → () → T_Level_18 → () → T_Equivalence_1714 → T_Equivalence_1714 Source #
d_sym'45''8617'_1154 ∷ T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1792 → T_RightInverse_1880 Source #
d_sym'45''8618'_1156 ∷ T_Level_18 → () → T_Level_18 → () → T_RightInverse_1880 → T_LeftInverse_1792 Source #
d_sym'45''8596'_1158 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Inverse_1960 Source #