Documentation

d_refl_28 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Bijection_926 Source #

du_refl_28 ∷ T_Bijection_926 Source #

d_sym'45''8801'_30 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → () → T_Bijection_926 → T_Bijection_926 Source #

du_sym'45''8801'_30 ∷ T_Setoid_44 → T_Bijection_926 → T_Bijection_926 Source #

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

du_trans_32 ∷ T_Bijection_926 → T_Bijection_926 → T_Bijection_926 Source #

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

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

d_Bijection'8658'Inverse_36 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Bijection_926 → T_Inverse_1960 Source #

du_Bijection'8658'Inverse_36 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_Inverse_1960 Source #

d_to'8728'to'8315'_118 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny Source #

du_to'8728'to'8315'_118 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → AgdaAny → AgdaAny Source #

d_Bijection'8658'Equivalence_124 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Bijection_926 → T_Equivalence_1714 Source #

du_Bijection'8658'Equivalence_124 ∷ T_Setoid_44 → T_Setoid_44 → T_Bijection_926 → T_Equivalence_1714 Source #

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

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

d_'10518''8658''8660'_128 ∷ T_Level_18 → () → T_Level_18 → () → T_Bijection_926 → T_Equivalence_1714 Source #

du_'10518''8658''8660'_128 ∷ T_Bijection_926 → T_Equivalence_1714 Source #