Documentation

d_Bijective_18 ∷ p → p → p → p → p → p → p → () 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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 ∷ p → p → p → p → p → p → () 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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_18 → T_Level_18 → () → () → () Source #

d_bijection_144 ∷ T_Level_18 → T_Level_18 → () → () → (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_18 → T_Level_18 → T_Setoid_44 → T_Bijection_64 Source #

du_id_160 ∷ T_Setoid_44 → T_Bijection_64 Source #

d__'8728'__182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → 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 #