Documentation

d__'8776'__40 :: T_GeneralizeTel_423 -> T_Func_714 -> AgdaAny -> AgdaAny -> () #

d__'8776'__64 :: T_GeneralizeTel_423 -> T_Func_714 -> AgdaAny -> AgdaAny -> () #

d_mkSurjection_86 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Func_714 -> (AgdaAny -> T_Σ_14) -> T_Surjection_846 #

du_mkSurjection_86 :: T_Func_714 -> (AgdaAny -> T_Σ_14) -> T_Surjection_846 #

d_'8608''8658''10230'_150 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Surjection_846 -> T_Func_714 #

du_'8608''8658''10230'_150 :: T_Surjection_846 -> T_Func_714 #

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

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

d_'46'extendedlambda0_228 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Surjection_846 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #

d_'8608''8658''8660'_230 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Surjection_846 -> T_Equivalence_1714 #

du_'8608''8658''8660'_230 :: T_Surjection_846 -> T_Equivalence_1714 #

d_refl_306 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Surjection_846 #

du_refl_306 :: T_Surjection_846 #

d_trans_310 :: 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_Surjection_846 -> T_Surjection_846 -> T_Surjection_846 #

du_trans_310 :: T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846 #

d_to'8315'_330 :: T_GeneralizeTel_9221 -> T_Surjection_846 -> AgdaAny -> AgdaAny #

du_to'8315'_330 :: T_Surjection_846 -> AgdaAny -> AgdaAny #

d__'8776'__336 :: T_GeneralizeTel_9221 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> () #

d__'8776'__360 :: T_GeneralizeTel_9221 -> T_Surjection_846 -> AgdaAny -> AgdaAny -> () #

d_injective'8658'to'8315''45'cong_382 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Surjection_846 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_injective'8658'to'8315''45'cong_382 :: T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'46'generalizedField'45'S'46'a_411 :: T_GeneralizeTel_423 -> T_Level_18 #

d_'46'generalizedField'45'S'46'ℓ_413 :: T_GeneralizeTel_423 -> T_Level_18 #

d_'46'generalizedField'45'S_415 :: T_GeneralizeTel_423 -> T_Setoid_44 #

d_'46'generalizedField'45'T'46'a_417 :: T_GeneralizeTel_423 -> T_Level_18 #

d_'46'generalizedField'45'T'46'ℓ_419 :: T_GeneralizeTel_423 -> T_Level_18 #

d_'46'generalizedField'45'T_421 :: T_GeneralizeTel_423 -> T_Setoid_44 #

d_GeneralizeTel_423 :: () #

data T_GeneralizeTel_423 #

d_'46'generalizedField'45'S'46'a_9209 :: T_GeneralizeTel_9221 -> T_Level_18 #

d_'46'generalizedField'45'S'46'ℓ_9211 :: T_GeneralizeTel_9221 -> T_Level_18 #

d_'46'generalizedField'45'S_9213 :: T_GeneralizeTel_9221 -> T_Setoid_44 #

d_'46'generalizedField'45'T'46'a_9215 :: T_GeneralizeTel_9221 -> T_Level_18 #

d_'46'generalizedField'45'T'46'ℓ_9217 :: T_GeneralizeTel_9221 -> T_Level_18 #

d_'46'generalizedField'45'T_9219 :: T_GeneralizeTel_9221 -> T_Setoid_44 #

d_GeneralizeTel_9221 :: () #

data T_GeneralizeTel_9221 #