| 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'_210 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → AgdaAny → AgdaAny Source #
d_isBijection_212 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsBijection_256 Source #
du_isBijection_212 ∷ (AgdaAny → AgdaAny) → T_IsBijection_256 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsBijection_256 Source #
d_isBijection'45''8801'_232 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → T_IsBijection_256 → T_IsBijection_256 Source #
d_isCongruent_332 ∷ 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_332 ∷ T_IsCongruent_22 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_IsCongruent_22 Source #
d_isLeftInverse_402 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsRightInverse_438 → T_IsLeftInverse_346 Source #
d_isRightInverse_478 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsLeftInverse_346 → T_IsRightInverse_438 Source #
d_isInverse_556 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_IsInverse_526 → T_IsInverse_526 Source #
d__'8776'__690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → () Source #
d__'8776'__716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny → () Source #
d_from_740 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny Source #
d_bijection_742 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Bijection_1004 Source #
du_bijection_742 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Bijection_1004 Source #
d_bijection'45''8801'_750 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → () → T_Bijection_1004 → T_Bijection_1004 Source #
d_equivalence_852 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Equivalence_1858 → T_Equivalence_1858 Source #
d_rightInverse_930 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_LeftInverse_1942 → T_RightInverse_2036 Source #
d_leftInverse_1016 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_RightInverse_2036 → T_LeftInverse_1942 Source #
d_inverse_1096 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Inverse_2122 → T_Inverse_2122 Source #
d_'10518''45'sym_1186 ∷ T_Level_18 → () → T_Level_18 → () → T_Bijection_1004 → T_Bijection_1004 Source #
d_'8660''45'sym_1190 ∷ T_Level_18 → () → T_Level_18 → () → T_Equivalence_1858 → T_Equivalence_1858 Source #
d_'8617''45'sym_1192 ∷ T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1942 → T_RightInverse_2036 Source #
d_'8618''45'sym_1194 ∷ T_Level_18 → () → T_Level_18 → () → T_RightInverse_2036 → T_LeftInverse_1942 Source #
d_'8596''45'sym_1196 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_Inverse_2122 Source #
d_sym'45''10518'_1198 ∷ T_Level_18 → () → T_Level_18 → () → T_Bijection_1004 → T_Bijection_1004 Source #
d_sym'45''8660'_1200 ∷ T_Level_18 → () → T_Level_18 → () → T_Equivalence_1858 → T_Equivalence_1858 Source #
d_sym'45''8617'_1202 ∷ T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1942 → T_RightInverse_2036 Source #
d_sym'45''8618'_1204 ∷ T_Level_18 → () → T_Level_18 → () → T_RightInverse_2036 → T_LeftInverse_1942 Source #
d_sym'45''8596'_1206 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_Inverse_2122 Source #