Documentation

d_refl_28 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Bijection_926 #

du_refl_28 :: T_Bijection_926 #

d_sym'45''8801'_30 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> () -> T_Bijection_926 -> T_Bijection_926 #

du_sym'45''8801'_30 :: T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926 #

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 #

du_trans_32 :: T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926 #

d_'10518''45'isEquivalence_34 :: T_Level_18 -> T_IsEquivalence_26 #

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

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 #

du_Bijection'8658'Inverse_36 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Inverse_1960 #

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 #

du_to'8728'to'8315'_118 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> AgdaAny -> AgdaAny #

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 #

du_Bijection'8658'Equivalence_124 :: T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Equivalence_1714 #

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

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

d_'10518''8658''8660'_128 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Bijection_926 -> T_Equivalence_1714 #

du_'10518''8658''8660'_128 :: T_Bijection_926 -> T_Equivalence_1714 #