Documentation

d_f'8315''185'_48 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny -> AgdaAny Source #

du_f'8315''185'_48 :: T_Σ_14 -> AgdaAny -> AgdaAny Source #

d_f'8728'f'8315''185''8801'id_50 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny -> AgdaAny Source #

du_f'8728'f'8315''185''8801'id_50 :: T_Σ_14 -> AgdaAny -> AgdaAny Source #

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

du_injective_52 :: (AgdaAny -> AgdaAny) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (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 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny -> T_Σ_14 Source #

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

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

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

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

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

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

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

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

du_inverse'7495'_102 :: T_Σ_14 -> T_Σ_14 Source #

d_f'8315''185'_196 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> AgdaAny -> AgdaAny Source #

du_f'8315''185'_196 :: T_IsBijection_232 -> AgdaAny -> AgdaAny Source #

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

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

d_isBijection'45''8801'_218 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> T_IsBijection_232 Source #

du_isBijection'45''8801'_218 :: (AgdaAny -> AgdaAny) -> T_IsBijection_232 -> T_IsBijection_232 Source #

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

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

d_isLeftInverse_378 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_390 -> T_IsLeftInverse_312 Source #

du_isLeftInverse_378 :: T_IsRightInverse_390 -> T_IsLeftInverse_312 Source #

d_isRightInverse_448 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_312 -> T_IsRightInverse_390 Source #

du_isRightInverse_448 :: T_IsLeftInverse_312 -> T_IsRightInverse_390 Source #

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

du_isInverse_518 :: T_IsInverse_468 -> T_IsInverse_468 Source #

d__'8776'__640 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> () Source #

d__'8776'__664 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny -> () Source #

d_f'8315''185'_686 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny Source #

du_f'8315''185'_686 :: T_Bijection_844 -> AgdaAny -> AgdaAny Source #

d_bijection_688 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Bijection_844 Source #

du_bijection_688 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Bijection_844 Source #

d_bijection'45''8801'_696 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> () -> T_Bijection_844 -> T_Bijection_844 Source #

du_bijection'45''8801'_696 :: T_Setoid_44 -> T_Bijection_844 -> T_Bijection_844 Source #

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

du_equivalence_792 :: T_Equivalence_928 -> T_Equivalence_928 Source #

d_rightInverse_810 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_946 -> T_RightInverse_1024 Source #

du_rightInverse_810 :: T_LeftInverse_946 -> T_RightInverse_1024 Source #

d_leftInverse_884 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1024 -> T_LeftInverse_946 Source #

du_leftInverse_884 :: T_RightInverse_1024 -> T_LeftInverse_946 Source #

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

du_inverse_910 :: T_Inverse_1052 -> T_Inverse_1052 Source #

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

du_'10518''45'sym_992 :: T_Bijection_844 -> T_Bijection_844 Source #

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

du_'8660''45'sym_996 :: T_Equivalence_928 -> T_Equivalence_928 Source #

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

du_'8617''45'sym_998 :: T_LeftInverse_946 -> T_RightInverse_1024 Source #

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

du_'8618''45'sym_1000 :: T_RightInverse_1024 -> T_LeftInverse_946 Source #

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

du_'8596''45'sym_1002 :: T_Inverse_1052 -> T_Inverse_1052 Source #

d_sym'45''10518'_1004 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Bijection_844 -> T_Bijection_844 Source #

d_sym'45''8660'_1006 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Equivalence_928 -> T_Equivalence_928 Source #

d_sym'45''8617'_1008 :: T_Level_14 -> () -> T_Level_14 -> () -> T_LeftInverse_946 -> T_RightInverse_1024 Source #

d_sym'45''8618'_1010 :: T_Level_14 -> () -> T_Level_14 -> () -> T_RightInverse_1024 -> T_LeftInverse_946 Source #

d_sym'45''8596'_1012 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Inverse_1052 -> T_Inverse_1052 Source #