Documentation

d__'8776'__44 :: T_GeneralizeTel_407 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> () #

d__'8776'__68 :: T_GeneralizeTel_407 -> T_Equivalence_1714 -> AgdaAny -> AgdaAny -> () #

d_mkRightInverse_90 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Equivalence_1714 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_RightInverse_1880 #

du_mkRightInverse_90 :: T_Equivalence_1714 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_RightInverse_1880 #

d_RightInverse'8658'LeftInverse_164 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_RightInverse_1880 -> T_LeftInverse_1792 #

du_RightInverse'8658'LeftInverse_164 :: T_RightInverse_1880 -> T_LeftInverse_1792 #

d_LeftInverse'8658'RightInverse_240 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_RightInverse_1880 #

du_LeftInverse'8658'RightInverse_240 :: T_LeftInverse_1792 -> T_RightInverse_1880 #

d_RightInverse'8658'Surjection_322 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_RightInverse_1880 -> T_Surjection_846 #

du_RightInverse'8658'Surjection_322 :: T_RightInverse_1880 -> T_Surjection_846 #

d_'46'generalizedField'45'S'46'a_395 :: T_GeneralizeTel_407 -> T_Level_18 #

d_'46'generalizedField'45'S'46'ℓ'8321'_397 :: T_GeneralizeTel_407 -> T_Level_18 #

d_'8618''8658''8608'_398 :: T_Level_18 -> () -> T_Level_18 -> () -> T_RightInverse_1880 -> T_Surjection_846 #

du_'8618''8658''8608'_398 :: T_RightInverse_1880 -> T_Surjection_846 #

d_'46'generalizedField'45'S_399 :: T_GeneralizeTel_407 -> T_Setoid_44 #

d_'8618''8658''8617'_400 :: T_Level_18 -> () -> T_Level_18 -> () -> T_RightInverse_1880 -> T_LeftInverse_1792 #

du_'8618''8658''8617'_400 :: T_RightInverse_1880 -> T_LeftInverse_1792 #

d_'46'generalizedField'45'T'46'a_401 :: T_GeneralizeTel_407 -> T_Level_18 #

d_'8617''8658''8618'_402 :: T_Level_18 -> () -> T_Level_18 -> () -> T_LeftInverse_1792 -> T_RightInverse_1880 #

du_'8617''8658''8618'_402 :: T_LeftInverse_1792 -> T_RightInverse_1880 #

d_'46'generalizedField'45'T'46'ℓ'8321'_403 :: T_GeneralizeTel_407 -> T_Level_18 #

d_'46'generalizedField'45'T_405 :: T_GeneralizeTel_407 -> T_Setoid_44 #

d_GeneralizeTel_407 :: () #

data T_GeneralizeTel_407 #

d__'8776'__436 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> () #

d__'8776'__460 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> () #

d_to'45'from_486 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_to'45'from_486 :: T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #