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_52 ∷ p → p → p → p → p → p → () Source #

d_IsCongruent_56 ∷ p → p → p → p → p → p → () Source #

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

d_IsInverse_64 ∷ p → p → p → p → p → p → p → () Source #

d_IsLeftInverse_68 ∷ p → p → p → p → p → p → p → () Source #

d_IsRightInverse_72 ∷ p → p → p → p → p → p → p → () Source #

d_IsSurjection_76 ∷ p → p → p → p → p → p → () Source #

d_isInjection_94 ∷ T_IsBijection_256 → T_IsInjection_98 Source #

d_surjective_100 ∷ T_IsBijection_256 → AgdaAny → T_Σ_14 Source #

d_cong_156 ∷ T_IsCongruent_22 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isEquivalence'8321'_158 ∷ T_IsCongruent_22 → T_IsEquivalence_28 Source #

d_isEquivalence'8322'_160 ∷ T_IsCongruent_22 → T_IsEquivalence_28 Source #

d_injective_218 ∷ T_IsInjection_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_220 ∷ T_IsInjection_98 → T_IsCongruent_22 Source #

d_inverse'691'_284 ∷ T_IsInverse_526 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isLeftInverse_294 ∷ T_IsInverse_526 → T_IsLeftInverse_346 Source #

d_from'45'cong_360 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_362 ∷ T_IsLeftInverse_346 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_364 ∷ T_IsLeftInverse_346 → T_IsCongruent_22 Source #

d_from'45'cong_430 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'691'_432 ∷ T_IsRightInverse_438 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_isCongruent_434 ∷ T_IsRightInverse_438 → T_IsCongruent_22 Source #

d_isCongruent_500 ∷ T_IsSurjection_174 → T_IsCongruent_22 Source #

d_surjective_508 ∷ T_IsSurjection_174 → AgdaAny → T_Σ_14 Source #

d_isCongruent_574 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsCongruent_22 Source #

du_isCongruent_574 ∷ T_IsEquivalence_28 → T_IsCongruent_22 Source #

d_isInjection_576 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsInjection_98 Source #

du_isInjection_576 ∷ T_IsEquivalence_28 → T_IsInjection_98 Source #

d_isSurjection_578 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsSurjection_174 Source #

du_isSurjection_578 ∷ T_IsEquivalence_28 → T_IsSurjection_174 Source #

d_isBijection_580 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsBijection_256 Source #

du_isBijection_580 ∷ T_IsEquivalence_28 → T_IsBijection_256 Source #

d_isLeftInverse_582 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsLeftInverse_346 Source #

du_isLeftInverse_582 ∷ T_IsEquivalence_28 → T_IsLeftInverse_346 Source #

d_isRightInverse_584 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsRightInverse_438 Source #

du_isRightInverse_584 ∷ T_IsEquivalence_28 → T_IsRightInverse_438 Source #

d_isInverse_586 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsInverse_526 Source #

du_isInverse_586 ∷ T_IsEquivalence_28 → T_IsInverse_526 Source #

d_function_622 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Func_774 Source #

du_function_622 ∷ T_Func_774 Source #

d_injection_624 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Injection_842 Source #

du_injection_624 ∷ T_Injection_842 Source #

d_surjection_626 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Surjection_918 Source #

du_surjection_626 ∷ T_Surjection_918 Source #

d_bijection_628 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Bijection_1004 Source #

du_bijection_628 ∷ T_Bijection_1004 Source #

d_equivalence_630 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Equivalence_1858 Source #

du_equivalence_630 ∷ T_Equivalence_1858 Source #

d_leftInverse_632 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_LeftInverse_1942 Source #

du_leftInverse_632 ∷ T_LeftInverse_1942 Source #

d_rightInverse_634 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_RightInverse_2036 Source #

du_rightInverse_634 ∷ T_RightInverse_2036 Source #

d_inverse_636 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 Source #

du_inverse_636 ∷ T_Inverse_2122 Source #

d_'10230''45'id_646 ∷ T_Level_18 → () → T_Func_774 Source #

du_'10230''45'id_646 ∷ T_Func_774 Source #

d_'8611''45'id_648 ∷ T_Level_18 → () → T_Injection_842 Source #

du_'8611''45'id_648 ∷ T_Injection_842 Source #

d_'8608''45'id_650 ∷ T_Level_18 → () → T_Surjection_918 Source #

du_'8608''45'id_650 ∷ T_Surjection_918 Source #

d_'10518''45'id_652 ∷ T_Level_18 → () → T_Bijection_1004 Source #

du_'10518''45'id_652 ∷ T_Bijection_1004 Source #

d_'8660''45'id_654 ∷ T_Level_18 → () → T_Equivalence_1858 Source #

du_'8660''45'id_654 ∷ T_Equivalence_1858 Source #

d_'8617''45'id_656 ∷ T_Level_18 → () → T_LeftInverse_1942 Source #

du_'8617''45'id_656 ∷ T_LeftInverse_1942 Source #

d_'8618''45'id_658 ∷ T_Level_18 → () → T_RightInverse_2036 Source #

du_'8618''45'id_658 ∷ T_RightInverse_2036 Source #

d_'8596''45'id_660 ∷ T_Level_18 → () → T_Inverse_2122 Source #

du_'8596''45'id_660 ∷ T_Inverse_2122 Source #

d_id'45''10230'_662 ∷ T_Level_18 → () → T_Func_774 Source #

d_id'45''8611'_664 ∷ T_Level_18 → () → T_Injection_842 Source #

d_id'45''8608'_666 ∷ T_Level_18 → () → T_Surjection_918 Source #

d_id'45''10518'_668 ∷ T_Level_18 → () → T_Bijection_1004 Source #

d_id'45''8660'_670 ∷ T_Level_18 → () → T_Equivalence_1858 Source #

d_id'45''8617'_672 ∷ T_Level_18 → () → T_LeftInverse_1942 Source #

d_id'45''8618'_674 ∷ T_Level_18 → () → T_RightInverse_2036 Source #

d_id'45''8596'_676 ∷ T_Level_18 → () → T_Inverse_2122 Source #