Documentation

d_isEquivalence_32 :: T_Level_18 -> T_Level_18 -> T_IsEquivalence_26 #

du_isEquivalence_32 :: T_IsEquivalence_26 #

d_'8596''45'refl_36 :: T_Level_18 -> () -> T_Inverse_1960 #

du_'8596''45'refl_36 :: T_Inverse_1960 #

d_'8596''45'sym_38 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Inverse_1960 #

du_'8596''45'sym_38 :: T_Inverse_1960 -> T_Inverse_1960 #

d_'8596''45'trans_40 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #

du_'8596''45'trans_40 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #

d_'8596''45'isEquivalence_42 :: T_Level_18 -> T_IsEquivalence_26 #

du_'8596''45'isEquivalence_42 :: T_IsEquivalence_26 #

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 #

du_toFunction_44 :: T_Inverse_1960 -> T_Func_714 #

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 #

du_fromFunction_130 :: T_Inverse_1960 -> T_Func_714 #

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 #

du_Inverse'8658'Injection_216 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Injection_776 #

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 #

du_Inverse'8658'Surjection_328 :: T_Inverse_1960 -> T_Surjection_846 #

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 #

du_Inverse'8658'Bijection_440 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Bijection_926 #

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 #

du_Inverse'8658'Equivalence_552 :: T_Inverse_1960 -> T_Equivalence_1714 #

d_'8596''8658''10230'_638 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Func_714 #

du_'8596''8658''10230'_638 :: T_Inverse_1960 -> T_Func_714 #

d_'8596''8658''10229'_640 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Func_714 #

du_'8596''8658''10229'_640 :: T_Inverse_1960 -> T_Func_714 #

d_'8596''8658''8611'_642 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Injection_776 #

du_'8596''8658''8611'_642 :: T_Inverse_1960 -> T_Injection_776 #

d_'8596''8658''8608'_644 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Surjection_846 #

du_'8596''8658''8608'_644 :: T_Inverse_1960 -> T_Surjection_846 #

d_'8596''8658''10518'_646 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Bijection_926 #

du_'8596''8658''10518'_646 :: T_Inverse_1960 -> T_Bijection_926 #

d_'8596''8658''8660'_648 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Equivalence_1714 #

du_'8596''8658''8660'_648 :: T_Inverse_1960 -> T_Equivalence_1714 #

d_'8596''8658''8617'_650 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_LeftInverse_1792 #

du_'8596''8658''8617'_650 :: T_Inverse_1960 -> T_LeftInverse_1792 #

d_'8596''8658''8618'_652 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_RightInverse_1880 #

du_'8596''8658''8618'_652 :: T_Inverse_1960 -> T_RightInverse_1880 #

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 #

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 #

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 #

du_'8596''45'fun_716 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #

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 -> () #

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 -> () #

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 #

du_to'45'from_834 :: T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #