Documentation

d__LeftInverseOf__16 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Π_16 → T_Π_16 → () Source #

d__RightInverseOf__64 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Π_16 → T_Π_16 → () Source #

d_LeftInverse_82 ∷ p → p → p → p → p → p → () Source #

data T_LeftInverse_82 Source #

d_to_102 ∷ T_LeftInverse_82 → T_Π_16 Source #

d_from_104 ∷ T_LeftInverse_82 → T_Π_16 Source #

d_left'45'inverse'45'of_106 ∷ T_LeftInverse_82 → AgdaAny → AgdaAny Source #

d__'8776'__110 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_82 → AgdaAny → AgdaAny → () Source #

d__'8776'__132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_82 → AgdaAny → AgdaAny → () Source #

d_injective_176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_82 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_injective_176 ∷ T_Setoid_44 → T_LeftInverse_82 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_injection_184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_82 → T_Injection_88 Source #

du_injection_184 ∷ T_Setoid_44 → T_LeftInverse_82 → T_Injection_88 Source #

d_equivalence_186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_82 → T_Equivalence_16 Source #

du_equivalence_186 ∷ T_LeftInverse_82 → T_Equivalence_16 Source #

d_to'45'from_192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_LeftInverse_82 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_192 ∷ T_Setoid_44 → T_Setoid_44 → T_LeftInverse_82 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_RightInverse_212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → () Source #

d__'8606'__222 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

d_leftInverse_242 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T_LeftInverse_82 Source #

du_leftInverse_242 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T_LeftInverse_82 Source #

d_id_256 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_LeftInverse_82 Source #

du_id_256 ∷ T_Setoid_44 → T_LeftInverse_82 Source #

d__'8728'__280 ∷ 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_LeftInverse_82 → T_LeftInverse_82 → T_LeftInverse_82 Source #

du__'8728'__280 ∷ T_Setoid_44 → T_LeftInverse_82 → T_LeftInverse_82 → T_LeftInverse_82 Source #