Documentation

d_isEquivalence_32 ∷ T_Level_18 → T_Level_18 → T_IsEquivalence_28 Source #

du_isEquivalence_32 ∷ T_IsEquivalence_28 Source #

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

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

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

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

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

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

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

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

d_toFunction_44 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → T_Func_774 Source #

du_toFunction_44 ∷ T_Inverse_2122 → T_Func_774 Source #

d_fromFunction_134 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → T_Func_774 Source #

du_fromFunction_134 ∷ T_Inverse_2122 → T_Func_774 Source #

d_Inverse'8658'Injection_224 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → T_Injection_842 Source #

du_Inverse'8658'Injection_224 ∷ T_Setoid_46 → T_Setoid_46 → T_Inverse_2122 → T_Injection_842 Source #

d_Inverse'8658'Surjection_326 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → T_Surjection_918 Source #

du_Inverse'8658'Surjection_326 ∷ T_Inverse_2122 → T_Surjection_918 Source #

d_Inverse'8658'Bijection_428 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → T_Bijection_1004 Source #

du_Inverse'8658'Bijection_428 ∷ T_Setoid_46 → T_Setoid_46 → T_Inverse_2122 → T_Bijection_1004 Source #

d_Inverse'8658'Equivalence_530 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → T_Equivalence_1858 Source #

du_Inverse'8658'Equivalence_530 ∷ T_Inverse_2122 → T_Equivalence_1858 Source #

d_'8596''8658''10230'_620 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_Func_774 Source #

du_'8596''8658''10230'_620 ∷ T_Inverse_2122 → T_Func_774 Source #

d_'8596''8658''10229'_622 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_Func_774 Source #

du_'8596''8658''10229'_622 ∷ T_Inverse_2122 → T_Func_774 Source #

d_'8596''8658''8611'_624 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_Injection_842 Source #

du_'8596''8658''8611'_624 ∷ T_Inverse_2122 → T_Injection_842 Source #

d_'8596''8658''8608'_626 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_Surjection_918 Source #

du_'8596''8658''8608'_626 ∷ T_Inverse_2122 → T_Surjection_918 Source #

d_'8596''8658''10518'_628 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_Bijection_1004 Source #

du_'8596''8658''10518'_628 ∷ T_Inverse_2122 → T_Bijection_1004 Source #

d_'8596''8658''8660'_630 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_Equivalence_1858 Source #

du_'8596''8658''8660'_630 ∷ T_Inverse_2122 → T_Equivalence_1858 Source #

d_'8596''8658''8617'_632 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_LeftInverse_1942 Source #

du_'8596''8658''8617'_632 ∷ T_Inverse_2122 → T_LeftInverse_1942 Source #

d_'8596''8658''8618'_634 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 → T_RightInverse_2036 Source #

du_'8596''8658''8618'_634 ∷ T_Inverse_2122 → T_RightInverse_2036 Source #

d_transportVia_676 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → ()) → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny) → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Inverse_2122 → AgdaAny) → T_Inverse_2122 → AgdaAny → T_Inverse_2122 → AgdaAny Source #

du_transportVia_676 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → AgdaAny → AgdaAny → AgdaAny) → (T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Inverse_2122 → AgdaAny) → T_Inverse_2122 → AgdaAny → T_Inverse_2122 → AgdaAny Source #

d_'8596''45'fun_698 ∷ (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_2122 → T_Inverse_2122 → T_Inverse_2122 Source #

du_'8596''45'fun_698 ∷ T_Inverse_2122 → T_Inverse_2122 → T_Inverse_2122 Source #

d__'8776'__766 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → AgdaAny → AgdaAny → () Source #

d__'8776'__792 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → AgdaAny → AgdaAny → () Source #

d_to'45'from_820 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Inverse_2122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_820 ∷ T_Setoid_46 → T_Setoid_46 → T_Inverse_2122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #