Documentation

d_map_18 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20 #

du_map_18 :: T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20 #

d__'8776'__114 :: T_GeneralizeTel_1875 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> () #

d__'8776'__138 :: T_GeneralizeTel_1875 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> AgdaAny -> AgdaAny -> () #

d_via'45'injection_160 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20 #

du_via'45'injection_160 :: T_Injection_776 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20 #

d_True'45''8596'_238 :: T_Level_18 -> () -> T_Dec_20 -> (AgdaAny -> AgdaAny -> T__'8801'__12) -> T_Inverse_1960 #

du_True'45''8596'_238 :: T_Dec_20 -> T_Inverse_1960 #

d_isYes'8791'does_256 :: T_Level_18 -> () -> T_Dec_20 -> T__'8801'__12 #

d_dec'45'true_260 :: T_Level_18 -> () -> T_Dec_20 -> AgdaAny -> T__'8801'__12 #

d_dec'45'false_270 :: T_Level_18 -> () -> T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> T__'8801'__12 #

d_dec'45'yes_282 :: T_Level_18 -> () -> T_Dec_20 -> AgdaAny -> T_Σ_14 #

du_dec'45'yes_282 :: T_Dec_20 -> T_Σ_14 #

d_dec'45'no_298 :: T_Level_18 -> () -> T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> T__'8801'__12 #

d_dec'45'yes'45'irr_312 :: T_Level_18 -> () -> T_Dec_20 -> (AgdaAny -> AgdaAny -> T__'8801'__12) -> AgdaAny -> T__'8801'__12 #

d_'8970''8971''45'map'8242'_338 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T__'8801'__12 #

d_'46'generalizedField'45'a_1867 :: T_GeneralizeTel_1875 -> T_Level_18 #

d_'46'generalizedField'45'ℓ'8321'_1869 :: T_GeneralizeTel_1875 -> T_Level_18 #

d_'46'generalizedField'45'b_1871 :: T_GeneralizeTel_1875 -> T_Level_18 #

d_'46'generalizedField'45'ℓ'8322'_1873 :: T_GeneralizeTel_1875 -> T_Level_18 #

d_GeneralizeTel_1875 :: () #

data T_GeneralizeTel_1875 #