| 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 #
du_f'8315''185'_48 :: T_Σ_14 -> AgdaAny -> AgdaAny #
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 #
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 #
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 #
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 #
du_surjective_64 :: (AgdaAny -> AgdaAny) -> T_Σ_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14 #
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 #
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 #
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 #
du_inverse'691'_102 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
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 #
du_inverse'737'_106 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
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 #
du_inverse'7495'_110 :: T_Σ_14 -> T_Σ_14 #
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 #
du_f'8315''185'_206 :: T_IsBijection_238 -> AgdaAny -> AgdaAny #
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 #
du_isBijection_208 :: (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBijection_238 #
d_isBijection'45''8801'_228 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsBijection_238 #
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 #
du_isCongruent_324 :: T_IsCongruent_22 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCongruent_22 #
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 #
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 #
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 #
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 -> () #
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 -> () #
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 #
du_from_712 :: T_Bijection_926 -> AgdaAny -> AgdaAny #
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 #
du_bijection_714 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Bijection_926 #
d_bijection'45''8801'_722 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> () -> T_Bijection_926 -> T_Bijection_926 #
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 #
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 #
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 #
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 #
d_'10518''45'sym_1138 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Bijection_926 -> T_Bijection_926 #
d_'8660''45'sym_1142 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Equivalence_1714 -> T_Equivalence_1714 #
d_'8617''45'sym_1144 :: T_Level_18 -> () -> T_Level_18 -> () -> T_LeftInverse_1792 -> T_RightInverse_1880 #
d_'8618''45'sym_1146 :: T_Level_18 -> () -> T_Level_18 -> () -> T_RightInverse_1880 -> T_LeftInverse_1792 #
d_'8596''45'sym_1148 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Inverse_1960 #
d_sym'45''10518'_1150 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Bijection_926 -> T_Bijection_926 #
d_sym'45''8660'_1152 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Equivalence_1714 -> T_Equivalence_1714 #
d_sym'45''8617'_1154 :: T_Level_18 -> () -> T_Level_18 -> () -> T_LeftInverse_1792 -> T_RightInverse_1880 #
d_sym'45''8618'_1156 :: T_Level_18 -> () -> T_Level_18 -> () -> T_RightInverse_1880 -> T_LeftInverse_1792 #
d_sym'45''8596'_1158 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Inverse_1960 #