Documentation

d_Bijective_24 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

d_Congruent_26 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

d_Injective_28 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'691'_30 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'737'_32 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'7495'_34 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_36 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

d_congruent_38 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_congruent_38 :: AgdaAny -> AgdaAny Source #

d_injective_40 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_injective_40 :: AgdaAny -> AgdaAny Source #

d_surjective_42 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14 Source #

du_surjective_42 :: (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14 Source #

d_bijective_48 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_Σ_14 Source #

du_bijective_48 :: (AgdaAny -> AgdaAny) -> T_Σ_14 Source #

d_inverse'737'_52 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #

du_inverse'737'_52 :: (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #

d_inverse'691'_58 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #

du_inverse'691'_58 :: (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #

d_inverse'7495'_64 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_Σ_14 Source #

du_inverse'7495'_64 :: (AgdaAny -> AgdaAny) -> T_Σ_14 Source #

d_IsBijection_86 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_IsCongruent_88 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_IsInjection_90 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_IsInverse_92 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsLeftInverse_94 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsRightInverse_96 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_IsSurjection_98 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_isCongruent_678 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsCongruent_22 Source #

du_isCongruent_678 :: T_IsEquivalence_26 -> T_IsCongruent_22 Source #

d_isInjection_680 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsInjection_92 Source #

du_isInjection_680 :: T_IsEquivalence_26 -> T_IsInjection_92 Source #

d_isSurjection_682 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsSurjection_162 Source #

du_isSurjection_682 :: T_IsEquivalence_26 -> T_IsSurjection_162 Source #

d_isBijection_684 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsBijection_232 Source #

du_isBijection_684 :: T_IsEquivalence_26 -> T_IsBijection_232 Source #

d_isLeftInverse_686 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsLeftInverse_312 Source #

du_isLeftInverse_686 :: T_IsEquivalence_26 -> T_IsLeftInverse_312 Source #

d_isRightInverse_688 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsRightInverse_390 Source #

du_isRightInverse_688 :: T_IsEquivalence_26 -> T_IsRightInverse_390 Source #

d_isInverse_690 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsInverse_468 Source #

du_isInverse_690 :: T_IsEquivalence_26 -> T_IsInverse_468 Source #

d_function_724 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Func_642 Source #

du_function_724 :: T_Func_642 Source #

d_injection_726 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Injection_704 Source #

du_injection_726 :: T_Injection_704 Source #

d_surjection_728 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Surjection_774 Source #

du_surjection_728 :: T_Setoid_44 -> T_Surjection_774 Source #

d_bijection_730 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Bijection_844 Source #

du_bijection_730 :: T_Setoid_44 -> T_Bijection_844 Source #

d_equivalence_732 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Equivalence_928 Source #

du_equivalence_732 :: T_Equivalence_928 Source #

d_leftInverse_734 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_LeftInverse_946 Source #

du_leftInverse_734 :: T_Setoid_44 -> T_LeftInverse_946 Source #

d_rightInverse_736 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_RightInverse_1024 Source #

du_rightInverse_736 :: T_Setoid_44 -> T_RightInverse_1024 Source #

d_inverse_738 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Inverse_1052 Source #

du_inverse_738 :: T_Setoid_44 -> T_Inverse_1052 Source #

d_'10230''45'id_748 :: T_Level_14 -> () -> T_Func_642 Source #

du_'10230''45'id_748 :: T_Func_642 Source #

d_'8611''45'id_750 :: T_Level_14 -> () -> T_Injection_704 Source #

du_'8611''45'id_750 :: T_Injection_704 Source #

d_'8608''45'id_752 :: T_Level_14 -> () -> T_Surjection_774 Source #

du_'8608''45'id_752 :: T_Surjection_774 Source #

d_'10518''45'id_754 :: T_Level_14 -> () -> T_Bijection_844 Source #

du_'10518''45'id_754 :: T_Bijection_844 Source #

d_'8660''45'id_756 :: T_Level_14 -> () -> T_Equivalence_928 Source #

du_'8660''45'id_756 :: T_Equivalence_928 Source #

d_'8617''45'id_758 :: T_Level_14 -> () -> T_LeftInverse_946 Source #

du_'8617''45'id_758 :: T_LeftInverse_946 Source #

d_'8618''45'id_760 :: T_Level_14 -> () -> T_RightInverse_1024 Source #

du_'8618''45'id_760 :: T_RightInverse_1024 Source #

d_'8596''45'id_762 :: T_Level_14 -> () -> T_Inverse_1052 Source #

du_'8596''45'id_762 :: T_Inverse_1052 Source #

d_id'45''10230'_764 :: T_Level_14 -> () -> T_Func_642 Source #

d_id'45''8611'_766 :: T_Level_14 -> () -> T_Injection_704 Source #

d_id'45''8608'_768 :: T_Level_14 -> () -> T_Surjection_774 Source #

d_id'45''10518'_770 :: T_Level_14 -> () -> T_Bijection_844 Source #

d_id'45''8660'_772 :: T_Level_14 -> () -> T_Equivalence_928 Source #

d_id'45''8617'_774 :: T_Level_14 -> () -> T_LeftInverse_946 Source #

d_id'45''8618'_776 :: T_Level_14 -> () -> T_RightInverse_1024 Source #

d_id'45''8596'_778 :: T_Level_14 -> () -> T_Inverse_1052 Source #