Documentation

d_isEquivalence_32 ∷ T_Level_18 → T_Level_18 → T_IsEquivalence_26 Source #

du_isEquivalence_32 ∷ T_IsEquivalence_26 Source #

d_'8596''45'refl_36 ∷ T_Level_18 → () → T_Inverse_1960 Source #

du_'8596''45'refl_36 ∷ T_Inverse_1960 Source #

d_'8596''45'sym_38 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Inverse_1960 Source #

du_'8596''45'sym_38 ∷ T_Inverse_1960 → T_Inverse_1960 Source #

d_'8596''45'trans_40 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #

du_'8596''45'trans_40 ∷ T_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #

d_'8596''45'isEquivalence_42 ∷ T_Level_18 → T_IsEquivalence_26 Source #

du_'8596''45'isEquivalence_42 ∷ T_IsEquivalence_26 Source #

d_toFunction_44 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → T_Func_714 Source #

du_toFunction_44 ∷ T_Inverse_1960 → T_Func_714 Source #

d_fromFunction_130 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → T_Func_714 Source #

du_fromFunction_130 ∷ T_Inverse_1960 → T_Func_714 Source #

d_Inverse'8658'Injection_216 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → T_Injection_776 Source #

du_Inverse'8658'Injection_216 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → T_Injection_776 Source #

d_Inverse'8658'Surjection_328 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → T_Surjection_846 Source #

du_Inverse'8658'Surjection_328 ∷ T_Inverse_1960 → T_Surjection_846 Source #

d_Inverse'8658'Bijection_440 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → T_Bijection_926 Source #

du_Inverse'8658'Bijection_440 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → T_Bijection_926 Source #

d_Inverse'8658'Equivalence_552 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → T_Equivalence_1714 Source #

du_Inverse'8658'Equivalence_552 ∷ T_Inverse_1960 → T_Equivalence_1714 Source #

d_'8596''8658''10230'_638 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Func_714 Source #

du_'8596''8658''10230'_638 ∷ T_Inverse_1960 → T_Func_714 Source #

d_'8596''8658''10229'_640 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Func_714 Source #

du_'8596''8658''10229'_640 ∷ T_Inverse_1960 → T_Func_714 Source #

d_'8596''8658''8611'_642 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Injection_776 Source #

du_'8596''8658''8611'_642 ∷ T_Inverse_1960 → T_Injection_776 Source #

d_'8596''8658''8608'_644 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Surjection_846 Source #

du_'8596''8658''8608'_644 ∷ T_Inverse_1960 → T_Surjection_846 Source #

d_'8596''8658''10518'_646 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Bijection_926 Source #

du_'8596''8658''10518'_646 ∷ T_Inverse_1960 → T_Bijection_926 Source #

d_'8596''8658''8660'_648 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Equivalence_1714 Source #

du_'8596''8658''8660'_648 ∷ T_Inverse_1960 → T_Equivalence_1714 Source #

d_'8596''8658''8617'_650 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_LeftInverse_1792 Source #

du_'8596''8658''8617'_650 ∷ T_Inverse_1960 → T_LeftInverse_1792 Source #

d_'8596''8658''8618'_652 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_RightInverse_1880 Source #

du_'8596''8658''8618'_652 ∷ T_Inverse_1960 → T_RightInverse_1880 Source #

d_transportVia_694 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → ()) → (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 → AgdaAny → AgdaAny → AgdaAny) → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → AgdaAny) → T_Inverse_1960 → AgdaAny → T_Inverse_1960 → AgdaAny Source #

du_transportVia_694 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → (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 → AgdaAny → AgdaAny → AgdaAny) → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → AgdaAny) → T_Inverse_1960 → AgdaAny → T_Inverse_1960 → AgdaAny Source #

d_'8596''45'fun_716 ∷ (T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12) → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #

du_'8596''45'fun_716 ∷ T_Inverse_1960 → T_Inverse_1960 → T_Inverse_1960 Source #

d__'8776'__784 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → AgdaAny → AgdaAny → () Source #

d__'8776'__808 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → AgdaAny → AgdaAny → () Source #

d_to'45'from_834 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Inverse_1960 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_834 ∷ T_Setoid_44 → T_Setoid_44 → T_Inverse_1960 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #