Documentation

d_refl_28 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Bijection_1004 Source #

du_refl_28 ∷ T_Bijection_1004 Source #

d_sym'45''8801'_30 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → () → T_Bijection_1004 → T_Bijection_1004 Source #

du_sym'45''8801'_30 ∷ T_Setoid_46 → T_Bijection_1004 → T_Bijection_1004 Source #

d_trans_32 ∷ 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 → T_Bijection_1004 → T_Bijection_1004 → T_Bijection_1004 Source #

du_trans_32 ∷ T_Bijection_1004 → T_Bijection_1004 → T_Bijection_1004 Source #

d_'10518''45'isEquivalence_34 ∷ T_Level_18 → T_IsEquivalence_28 Source #

du_'10518''45'isEquivalence_34 ∷ T_IsEquivalence_28 Source #

d_Bijection'8658'Inverse_36 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Bijection_1004 → T_Inverse_2122 Source #

du_Bijection'8658'Inverse_36 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_Inverse_2122 Source #

d_to'8728'to'8315'_122 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny Source #

du_to'8728'to'8315'_122 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → AgdaAny → AgdaAny Source #

d_Bijection'8658'Equivalence_128 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Bijection_1004 → T_Equivalence_1858 Source #

du_Bijection'8658'Equivalence_128 ∷ T_Setoid_46 → T_Setoid_46 → T_Bijection_1004 → T_Equivalence_1858 Source #

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

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

d_'10518''8658''8660'_132 ∷ T_Level_18 → () → T_Level_18 → () → T_Bijection_1004 → T_Equivalence_1858 Source #

du_'10518''8658''8660'_132 ∷ T_Bijection_1004 → T_Equivalence_1858 Source #