Documentation

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

du_congruent_50 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

du_injective_56 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

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

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

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

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

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

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

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

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

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

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

d_isCongruent_226 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22 Source #

du_isCongruent_226 :: (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22 Source #

d_isInjection_348 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> T_IsInjection_92 -> T_IsInjection_92 Source #

du_isInjection_348 :: (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> T_IsInjection_92 -> T_IsInjection_92 Source #

d_isSurjection_478 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> T_IsSurjection_162 -> T_IsSurjection_162 Source #

du_isSurjection_478 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> T_IsSurjection_162 -> T_IsSurjection_162 Source #

d_isBijection_608 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> T_IsBijection_232 -> T_IsBijection_232 Source #

du_isBijection_608 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> T_IsBijection_232 -> T_IsBijection_232 Source #

d_isLeftInverse_784 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_312 -> T_IsLeftInverse_312 -> T_IsLeftInverse_312 Source #

du_isLeftInverse_784 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_312 -> T_IsLeftInverse_312 -> T_IsLeftInverse_312 Source #

d_isRightInverse_918 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_390 -> T_IsRightInverse_390 -> T_IsRightInverse_390 Source #

du_isRightInverse_918 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_390 -> T_IsRightInverse_390 -> T_IsRightInverse_390 Source #

d_isInverse_1052 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> T_IsInverse_468 -> T_IsInverse_468 Source #

du_isInverse_1052 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_468 -> T_IsInverse_468 -> T_IsInverse_468 Source #

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

du_function_1224 :: T_Func_642 -> T_Func_642 -> T_Func_642 Source #

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

du_injection_1346 :: T_Injection_704 -> T_Injection_704 -> T_Injection_704 Source #

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

du_surjection_1480 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_774 -> T_Surjection_774 -> T_Surjection_774 Source #

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

du_bijection_1614 :: T_Setoid_44 -> T_Bijection_844 -> T_Bijection_844 -> T_Bijection_844 Source #

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

du_equivalence_1768 :: T_Equivalence_928 -> T_Equivalence_928 -> T_Equivalence_928 Source #

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

du_leftInverse_1798 :: T_Setoid_44 -> T_LeftInverse_946 -> T_LeftInverse_946 -> T_LeftInverse_946 Source #

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

du_rightInverse_1940 :: T_Setoid_44 -> T_RightInverse_1024 -> T_RightInverse_1024 -> T_RightInverse_1024 Source #

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

du_inverse_1986 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1052 -> T_Inverse_1052 -> T_Inverse_1052 Source #

d__'10230''45''8728'__2144 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Func_642 -> T_Func_642 -> T_Func_642 Source #

du__'10230''45''8728'__2144 :: T_Func_642 -> T_Func_642 -> T_Func_642 Source #

d__'8611''45''8728'__2146 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Injection_704 -> T_Injection_704 -> T_Injection_704 Source #

du__'8611''45''8728'__2146 :: T_Injection_704 -> T_Injection_704 -> T_Injection_704 Source #

d__'8608''45''8728'__2148 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Surjection_774 -> T_Surjection_774 -> T_Surjection_774 Source #

du__'8608''45''8728'__2148 :: T_Surjection_774 -> T_Surjection_774 -> T_Surjection_774 Source #

d__'10518''45''8728'__2150 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Bijection_844 -> T_Bijection_844 -> T_Bijection_844 Source #

du__'10518''45''8728'__2150 :: T_Bijection_844 -> T_Bijection_844 -> T_Bijection_844 Source #

d__'8660''45''8728'__2152 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Equivalence_928 -> T_Equivalence_928 -> T_Equivalence_928 Source #

du__'8660''45''8728'__2152 :: T_Equivalence_928 -> T_Equivalence_928 -> T_Equivalence_928 Source #

d__'8617''45''8728'__2154 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_LeftInverse_946 -> T_LeftInverse_946 -> T_LeftInverse_946 Source #

du__'8617''45''8728'__2154 :: T_LeftInverse_946 -> T_LeftInverse_946 -> T_LeftInverse_946 Source #

d__'8618''45''8728'__2156 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_RightInverse_1024 -> T_RightInverse_1024 -> T_RightInverse_1024 Source #

du__'8618''45''8728'__2156 :: T_RightInverse_1024 -> T_RightInverse_1024 -> T_RightInverse_1024 Source #

d__'8596''45''8728'__2158 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Inverse_1052 -> T_Inverse_1052 -> T_Inverse_1052 Source #

du__'8596''45''8728'__2158 :: T_Inverse_1052 -> T_Inverse_1052 -> T_Inverse_1052 Source #

d__'8728''45''10230'__2160 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Func_642 -> T_Func_642 -> T_Func_642 Source #

d__'8728''45''8611'__2162 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Injection_704 -> T_Injection_704 -> T_Injection_704 Source #

d__'8728''45''8608'__2164 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Surjection_774 -> T_Surjection_774 -> T_Surjection_774 Source #

d__'8728''45''10518'__2166 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Bijection_844 -> T_Bijection_844 -> T_Bijection_844 Source #

d__'8728''45''8660'__2168 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Equivalence_928 -> T_Equivalence_928 -> T_Equivalence_928 Source #

d__'8728''45''8617'__2170 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_LeftInverse_946 -> T_LeftInverse_946 -> T_LeftInverse_946 Source #

d__'8728''45''8618'__2172 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_RightInverse_1024 -> T_RightInverse_1024 -> T_RightInverse_1024 Source #

d__'8728''45''8596'__2174 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> T_Inverse_1052 -> T_Inverse_1052 -> T_Inverse_1052 Source #