Documentation

d_refl_28 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Bijection_844 Source #

du_refl_28 :: T_Setoid_44 -> T_Bijection_844 Source #

d_sym'45''8801'_30 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Level_14 -> () -> T_Bijection_844 -> T_Bijection_844 Source #

du_sym'45''8801'_30 :: T_Setoid_44 -> T_Bijection_844 -> T_Bijection_844 Source #

d_trans_32 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_844 -> T_Bijection_844 -> T_Bijection_844 Source #

du_trans_32 :: T_Setoid_44 -> T_Bijection_844 -> T_Bijection_844 -> T_Bijection_844 Source #

d_'10518''45'isEquivalence_34 :: T_Level_14 -> T_IsEquivalence_26 Source #

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

d_Bijection'8658'Inverse_36 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Bijection_844 -> T_Inverse_1052 Source #

du_Bijection'8658'Inverse_36 :: T_Setoid_44 -> T_Bijection_844 -> T_Inverse_1052 Source #

d_f'8728'f'8315'_144 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Bijection_844 -> AgdaAny -> AgdaAny Source #

du_f'8728'f'8315'_144 :: T_Bijection_844 -> AgdaAny -> AgdaAny Source #

d_Bijection'8658'Equivalence_152 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Bijection_844 -> T_Equivalence_928 Source #

du_Bijection'8658'Equivalence_152 :: T_Setoid_44 -> T_Bijection_844 -> T_Equivalence_928 Source #

d_'10518''8658''8596'_154 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Bijection_844 -> T_Inverse_1052 Source #

du_'10518''8658''8596'_154 :: T_Bijection_844 -> T_Inverse_1052 Source #

d_'10518''8658''8660'_156 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Bijection_844 -> T_Equivalence_928 Source #

du_'10518''8658''8660'_156 :: T_Bijection_844 -> T_Equivalence_928 Source #