Documentation

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

data T_Bijective_18 Source #

d_injective_38 :: T_Bijective_18 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_surjective_40 :: T_Bijective_18 -> T_Surjective_18 Source #

d_from_44 :: T_Bijective_18 -> T_Π_16 Source #

d_right'45'inverse'45'of_46 :: T_Bijective_18 -> AgdaAny -> AgdaAny Source #

d_left'45'inverse'45'of_48 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Π_16 -> T_Bijective_18 -> AgdaAny -> AgdaAny Source #

du_left'45'inverse'45'of_48 :: T_Π_16 -> T_Bijective_18 -> AgdaAny -> AgdaAny Source #

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

data T_Bijection_64 Source #

d_to_82 :: T_Bijection_64 -> T_Π_16 Source #

d_bijective_84 :: T_Bijection_64 -> T_Bijective_18 Source #

d_from_88 :: T_Bijection_64 -> T_Π_16 Source #

d_injective_90 :: T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_left'45'inverse'45'of_92 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> AgdaAny -> AgdaAny Source #

du_left'45'inverse'45'of_92 :: T_Bijection_64 -> AgdaAny -> AgdaAny Source #

d_right'45'inverse'45'of_94 :: T_Bijection_64 -> AgdaAny -> AgdaAny Source #

d_surjective_96 :: T_Bijection_64 -> T_Surjective_18 Source #

d_injection_98 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> T_Injection_88 Source #

du_injection_98 :: T_Bijection_64 -> T_Injection_88 Source #

d_surjection_100 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> T_Surjection_54 Source #

du_surjection_100 :: T_Bijection_64 -> T_Surjection_54 Source #

d_equivalence_104 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> T_Equivalence_16 Source #

du_equivalence_104 :: T_Bijection_64 -> T_Equivalence_16 Source #

d_to'45'from_106 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_to'45'from_106 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_right'45'inverse_108 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> T_LeftInverse_82 Source #

du_right'45'inverse_108 :: T_Bijection_64 -> T_LeftInverse_82 Source #

d_left'45'inverse_110 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> T_LeftInverse_82 Source #

du_left'45'inverse_110 :: T_Bijection_64 -> T_LeftInverse_82 Source #

d_to'45'from_114 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_to'45'from_114 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_64 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'10518'__120 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d_bijection_144 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> (AgdaAny -> T__'8801'__12) -> T_Bijection_64 Source #

du_bijection_144 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> (AgdaAny -> T__'8801'__12) -> T_Bijection_64 Source #

d_id_160 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Bijection_64 Source #

du_id_160 :: T_Setoid_44 -> T_Bijection_64 Source #

d__'8728'__182 :: 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_64 -> T_Bijection_64 -> T_Bijection_64 Source #

du__'8728'__182 :: T_Setoid_44 -> T_Bijection_64 -> T_Bijection_64 -> T_Bijection_64 Source #