Documentation

d_congruent_22 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_congruent_22 :: AgdaAny -> AgdaAny #

d_injective_24 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_injective_24 :: AgdaAny -> AgdaAny #

d_surjective_26 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Σ_14 #

du_surjective_26 :: AgdaAny -> T_Σ_14 #

d_bijective_30 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 #

du_bijective_30 :: T_Σ_14 #

d_inverse'737'_32 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_inverse'737'_32 :: AgdaAny -> AgdaAny #

d_inverse'691'_34 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_inverse'691'_34 :: AgdaAny -> AgdaAny #

d_inverse'7495'_36 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 #

du_inverse'7495'_36 :: T_Σ_14 #

d_IsBijection_56 :: p -> p -> p -> p -> p -> p -> () #

d_IsCongruent_58 :: p -> p -> p -> p -> p -> p -> () #

d_IsInjection_60 :: p -> p -> p -> p -> p -> p -> () #

d_IsInverse_62 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsLeftInverse_64 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsRightInverse_66 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsSurjection_70 :: p -> p -> p -> p -> p -> p -> () #

d_isInjection_214 :: T_IsBijection_238 -> T_IsInjection_92 #

d_surjective_220 :: T_IsBijection_238 -> AgdaAny -> T_Σ_14 #

d_cong_272 :: T_IsCongruent_22 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isEquivalence'8321'_274 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

d_isEquivalence'8322'_276 :: T_IsCongruent_22 -> T_IsEquivalence_26 #

d_injective_330 :: T_IsInjection_92 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_332 :: T_IsInjection_92 -> T_IsCongruent_22 #

d_inverse'691'_392 :: T_IsInverse_490 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isLeftInverse_402 :: T_IsInverse_490 -> T_IsLeftInverse_322 #

d_from'45'cong_464 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'737'_466 :: T_IsLeftInverse_322 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_468 :: T_IsLeftInverse_322 -> T_IsCongruent_22 #

d_from'45'cong_530 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'691'_532 :: T_IsRightInverse_408 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_isCongruent_534 :: T_IsRightInverse_408 -> T_IsCongruent_22 #

d_isCongruent_666 :: T_IsSurjection_162 -> T_IsCongruent_22 #

d_surjective_674 :: T_IsSurjection_162 -> AgdaAny -> T_Σ_14 #

d_isCongruent_736 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsCongruent_22 #

du_isCongruent_736 :: T_IsEquivalence_26 -> T_IsCongruent_22 #

d_isInjection_738 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsInjection_92 #

du_isInjection_738 :: T_IsEquivalence_26 -> T_IsInjection_92 #

d_isSurjection_740 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsSurjection_162 #

du_isSurjection_740 :: T_IsEquivalence_26 -> T_IsSurjection_162 #

d_isBijection_742 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsBijection_238 #

du_isBijection_742 :: T_IsEquivalence_26 -> T_IsBijection_238 #

d_isLeftInverse_744 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsLeftInverse_322 #

du_isLeftInverse_744 :: T_IsEquivalence_26 -> T_IsLeftInverse_322 #

d_isRightInverse_746 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsRightInverse_408 #

du_isRightInverse_746 :: T_IsEquivalence_26 -> T_IsRightInverse_408 #

d_isInverse_748 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsInverse_490 #

du_isInverse_748 :: T_IsEquivalence_26 -> T_IsInverse_490 #

d_function_782 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Func_714 #

du_function_782 :: T_Func_714 #

d_injection_784 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Injection_776 #

du_injection_784 :: T_Injection_776 #

d_surjection_786 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Surjection_846 #

du_surjection_786 :: T_Surjection_846 #

d_bijection_788 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Bijection_926 #

du_bijection_788 :: T_Bijection_926 #

d_equivalence_790 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Equivalence_1714 #

du_equivalence_790 :: T_Equivalence_1714 #

d_leftInverse_792 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_LeftInverse_1792 #

du_leftInverse_792 :: T_LeftInverse_1792 #

d_rightInverse_794 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_RightInverse_1880 #

du_rightInverse_794 :: T_RightInverse_1880 #

d_inverse_796 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Inverse_1960 #

du_inverse_796 :: T_Inverse_1960 #

d_'10230''45'id_806 :: T_Level_18 -> () -> T_Func_714 #

du_'10230''45'id_806 :: T_Func_714 #

d_'8611''45'id_808 :: T_Level_18 -> () -> T_Injection_776 #

du_'8611''45'id_808 :: T_Injection_776 #

d_'8608''45'id_810 :: T_Level_18 -> () -> T_Surjection_846 #

du_'8608''45'id_810 :: T_Surjection_846 #

d_'10518''45'id_812 :: T_Level_18 -> () -> T_Bijection_926 #

du_'10518''45'id_812 :: T_Bijection_926 #

d_'8660''45'id_814 :: T_Level_18 -> () -> T_Equivalence_1714 #

du_'8660''45'id_814 :: T_Equivalence_1714 #

d_'8617''45'id_816 :: T_Level_18 -> () -> T_LeftInverse_1792 #

du_'8617''45'id_816 :: T_LeftInverse_1792 #

d_'8618''45'id_818 :: T_Level_18 -> () -> T_RightInverse_1880 #

du_'8618''45'id_818 :: T_RightInverse_1880 #

d_'8596''45'id_820 :: T_Level_18 -> () -> T_Inverse_1960 #

du_'8596''45'id_820 :: T_Inverse_1960 #

d_id'45''10230'_822 :: T_Level_18 -> () -> T_Func_714 #

d_id'45''8611'_824 :: T_Level_18 -> () -> T_Injection_776 #

d_id'45''8608'_826 :: T_Level_18 -> () -> T_Surjection_846 #

d_id'45''10518'_828 :: T_Level_18 -> () -> T_Bijection_926 #

d_id'45''8660'_830 :: T_Level_18 -> () -> T_Equivalence_1714 #

d_id'45''8617'_832 :: T_Level_18 -> () -> T_LeftInverse_1792 #

d_id'45''8618'_834 :: T_Level_18 -> () -> T_RightInverse_1880 #

d_id'45''8596'_836 :: T_Level_18 -> () -> T_Inverse_1960 #