Documentation

d__'8776'__40 ∷ T_GeneralizeTel_423 → T_Func_714 → AgdaAny → AgdaAny → () Source #

d__'8776'__64 ∷ T_GeneralizeTel_423 → T_Func_714 → AgdaAny → AgdaAny → () Source #

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 Source #

du_mkSurjection_86 ∷ T_Func_714 → (AgdaAny → T_Σ_14) → T_Surjection_846 Source #

d_'8608''8658''10230'_150 ∷ T_Level_18 → () → T_Level_18 → () → T_Surjection_846 → T_Func_714 Source #

du_'8608''8658''10230'_150 ∷ T_Surjection_846 → T_Func_714 Source #

d_'8608''8658''8618'_152 ∷ T_Level_18 → () → T_Level_18 → () → T_Surjection_846 → T_RightInverse_1880 Source #

du_'8608''8658''8618'_152 ∷ T_Surjection_846 → T_RightInverse_1880 Source #

d_'46'extendedlambda0_228 ∷ T_Level_18 → () → T_Level_18 → () → T_Surjection_846 → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_'8608''8658''8660'_230 ∷ T_Level_18 → () → T_Level_18 → () → T_Surjection_846 → T_Equivalence_1714 Source #

du_'8608''8658''8660'_230 ∷ T_Surjection_846 → T_Equivalence_1714 Source #

d_refl_306 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Surjection_846 Source #

du_refl_306 ∷ T_Surjection_846 Source #

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 Source #

du_trans_310 ∷ T_Surjection_846 → T_Surjection_846 → T_Surjection_846 Source #

d_to'8315'_330 ∷ T_GeneralizeTel_9221 → T_Surjection_846 → AgdaAny → AgdaAny Source #

du_to'8315'_330 ∷ T_Surjection_846 → AgdaAny → AgdaAny Source #

d__'8776'__336 ∷ T_GeneralizeTel_9221 → T_Surjection_846 → AgdaAny → AgdaAny → () Source #

d__'8776'__360 ∷ T_GeneralizeTel_9221 → T_Surjection_846 → AgdaAny → AgdaAny → () Source #

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 Source #

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 Source #

d_'46'generalizedField'45'S'46'a_411 ∷ T_GeneralizeTel_423 → T_Level_18 Source #

d_'46'generalizedField'45'S'46'ℓ_413 ∷ T_GeneralizeTel_423 → T_Level_18 Source #

d_'46'generalizedField'45'S_415 ∷ T_GeneralizeTel_423 → T_Setoid_44 Source #

d_'46'generalizedField'45'T'46'a_417 ∷ T_GeneralizeTel_423 → T_Level_18 Source #

d_'46'generalizedField'45'T'46'ℓ_419 ∷ T_GeneralizeTel_423 → T_Level_18 Source #

d_'46'generalizedField'45'T_421 ∷ T_GeneralizeTel_423 → T_Setoid_44 Source #

d_GeneralizeTel_423 ∷ () Source #

data T_GeneralizeTel_423 Source #

d_'46'generalizedField'45'S'46'a_9209 ∷ T_GeneralizeTel_9221 → T_Level_18 Source #

d_'46'generalizedField'45'S'46'ℓ_9211 ∷ T_GeneralizeTel_9221 → T_Level_18 Source #

d_'46'generalizedField'45'S_9213 ∷ T_GeneralizeTel_9221 → T_Setoid_44 Source #

d_'46'generalizedField'45'T'46'a_9215 ∷ T_GeneralizeTel_9221 → T_Level_18 Source #

d_'46'generalizedField'45'T'46'ℓ_9217 ∷ T_GeneralizeTel_9221 → T_Level_18 Source #

d_'46'generalizedField'45'T_9219 ∷ T_GeneralizeTel_9221 → T_Setoid_44 Source #

d_GeneralizeTel_9221 ∷ () Source #

data T_GeneralizeTel_9221 Source #