Documentation

d_congruent_22 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_congruent_22 ∷ AgdaAny → AgdaAny Source #

d_injective_24 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_injective_24 ∷ AgdaAny → AgdaAny Source #

d_surjective_26 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Σ_14 Source #

du_surjective_26 ∷ AgdaAny → T_Σ_14 Source #

d_bijective_30 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 Source #

du_bijective_30 ∷ T_Σ_14 Source #

d_inverse'737'_32 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_inverse'737'_32 ∷ AgdaAny → AgdaAny Source #

d_inverse'691'_34 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_inverse'691'_34 ∷ AgdaAny → AgdaAny Source #

d_inverse'7495'_36 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 Source #

du_inverse'7495'_36 ∷ T_Σ_14 Source #

d_IsBijection_56 ∷ p → p → p → p → p → p → () Source #

d_IsCongruent_58 ∷ p → p → p → p → p → p → () Source #

d_IsInjection_60 ∷ p → p → p → p → p → p → () Source #

d_IsInverse_62 ∷ p → p → p → p → p → p → p → () Source #

d_IsLeftInverse_64 ∷ p → p → p → p → p → p → p → () Source #

d_IsRightInverse_66 ∷ p → p → p → p → p → p → p → () Source #

d_IsSurjection_70 ∷ p → p → p → p → p → p → () Source #

d_isInjection_214 ∷ T_IsBijection_238 → T_IsInjection_92 Source #

d_surjective_220 ∷ T_IsBijection_238 → AgdaAny → T_Σ_14 Source #

d_cong_272 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_274 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

d_isEquivalence'8322'_276 ∷ T_IsCongruent_22 → T_IsEquivalence_26 Source #

d_injective_330 ∷ T_IsInjection_92 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_332 ∷ T_IsInjection_92 → T_IsCongruent_22 Source #

d_inverse'691'_392 ∷ T_IsInverse_490 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isLeftInverse_402 ∷ T_IsInverse_490 → T_IsLeftInverse_322 Source #

d_from'45'cong_464 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_466 ∷ T_IsLeftInverse_322 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_468 ∷ T_IsLeftInverse_322 → T_IsCongruent_22 Source #

d_from'45'cong_530 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_532 ∷ T_IsRightInverse_408 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_534 ∷ T_IsRightInverse_408 → T_IsCongruent_22 Source #

d_isCongruent_666 ∷ T_IsSurjection_162 → T_IsCongruent_22 Source #

d_surjective_674 ∷ T_IsSurjection_162 → AgdaAny → T_Σ_14 Source #

d_isCongruent_736 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsCongruent_22 Source #

du_isCongruent_736 ∷ T_IsEquivalence_26 → T_IsCongruent_22 Source #

d_isInjection_738 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsInjection_92 Source #

du_isInjection_738 ∷ T_IsEquivalence_26 → T_IsInjection_92 Source #

d_isSurjection_740 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsSurjection_162 Source #

du_isSurjection_740 ∷ T_IsEquivalence_26 → T_IsSurjection_162 Source #

d_isBijection_742 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsBijection_238 Source #

du_isBijection_742 ∷ T_IsEquivalence_26 → T_IsBijection_238 Source #

d_isLeftInverse_744 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsLeftInverse_322 Source #

du_isLeftInverse_744 ∷ T_IsEquivalence_26 → T_IsLeftInverse_322 Source #

d_isRightInverse_746 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsRightInverse_408 Source #

du_isRightInverse_746 ∷ T_IsEquivalence_26 → T_IsRightInverse_408 Source #

d_isInverse_748 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsInverse_490 Source #

du_isInverse_748 ∷ T_IsEquivalence_26 → T_IsInverse_490 Source #

d_function_782 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Func_714 Source #

du_function_782 ∷ T_Func_714 Source #

d_injection_784 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Injection_776 Source #

du_injection_784 ∷ T_Injection_776 Source #

d_surjection_786 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Surjection_846 Source #

du_surjection_786 ∷ T_Surjection_846 Source #

d_bijection_788 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Bijection_926 Source #

du_bijection_788 ∷ T_Bijection_926 Source #

d_equivalence_790 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Equivalence_1714 Source #

du_equivalence_790 ∷ T_Equivalence_1714 Source #

d_leftInverse_792 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_LeftInverse_1792 Source #

du_leftInverse_792 ∷ T_LeftInverse_1792 Source #

d_rightInverse_794 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_RightInverse_1880 Source #

du_rightInverse_794 ∷ T_RightInverse_1880 Source #

d_inverse_796 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 Source #

du_inverse_796 ∷ T_Inverse_1960 Source #

d_'10230''45'id_806 ∷ T_Level_18 → () → T_Func_714 Source #

du_'10230''45'id_806 ∷ T_Func_714 Source #

d_'8611''45'id_808 ∷ T_Level_18 → () → T_Injection_776 Source #

du_'8611''45'id_808 ∷ T_Injection_776 Source #

d_'8608''45'id_810 ∷ T_Level_18 → () → T_Surjection_846 Source #

du_'8608''45'id_810 ∷ T_Surjection_846 Source #

d_'10518''45'id_812 ∷ T_Level_18 → () → T_Bijection_926 Source #

du_'10518''45'id_812 ∷ T_Bijection_926 Source #

d_'8660''45'id_814 ∷ T_Level_18 → () → T_Equivalence_1714 Source #

du_'8660''45'id_814 ∷ T_Equivalence_1714 Source #

d_'8617''45'id_816 ∷ T_Level_18 → () → T_LeftInverse_1792 Source #

du_'8617''45'id_816 ∷ T_LeftInverse_1792 Source #

d_'8618''45'id_818 ∷ T_Level_18 → () → T_RightInverse_1880 Source #

du_'8618''45'id_818 ∷ T_RightInverse_1880 Source #

d_'8596''45'id_820 ∷ T_Level_18 → () → T_Inverse_1960 Source #

du_'8596''45'id_820 ∷ T_Inverse_1960 Source #

d_id'45''10230'_822 ∷ T_Level_18 → () → T_Func_714 Source #

d_id'45''8611'_824 ∷ T_Level_18 → () → T_Injection_776 Source #

d_id'45''8608'_826 ∷ T_Level_18 → () → T_Surjection_846 Source #

d_id'45''10518'_828 ∷ T_Level_18 → () → T_Bijection_926 Source #

d_id'45''8660'_830 ∷ T_Level_18 → () → T_Equivalence_1714 Source #

d_id'45''8617'_832 ∷ T_Level_18 → () → T_LeftInverse_1792 Source #

d_id'45''8618'_834 ∷ T_Level_18 → () → T_RightInverse_1880 Source #

d_id'45''8596'_836 ∷ T_Level_18 → () → T_Inverse_1960 Source #