Documentation

d__'8776'__40 ∷ T_GeneralizeTel_503 → T_Func_774 → AgdaAny → AgdaAny → () Source #

d__'8776'__66 ∷ T_GeneralizeTel_503 → T_Func_774 → AgdaAny → AgdaAny → () Source #

d_mkSurjection_90 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Func_774 → (AgdaAny → T_Σ_14) → T_Surjection_918 Source #

du_mkSurjection_90 ∷ T_Func_774 → (AgdaAny → T_Σ_14) → T_Surjection_918 Source #

d_'8608''8658''10230'_158 ∷ T_Level_18 → () → T_Level_18 → () → T_Surjection_918 → T_Func_774 Source #

du_'8608''8658''10230'_158 ∷ T_Surjection_918 → T_Func_774 Source #

d_'8608''8658''8618'_160 ∷ T_Level_18 → () → T_Level_18 → () → T_Surjection_918 → T_RightInverse_2036 Source #

du_'8608''8658''8618'_160 ∷ T_Surjection_918 → T_RightInverse_2036 Source #

d_'46'extendedlambda0_240 ∷ T_Level_18 → () → T_Level_18 → () → T_Surjection_918 → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_'8608''8658''8660'_242 ∷ T_Level_18 → () → T_Level_18 → () → T_Surjection_918 → T_Equivalence_1858 Source #

du_'8608''8658''8660'_242 ∷ T_Surjection_918 → T_Equivalence_1858 Source #

d_refl_322 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Surjection_918 Source #

du_refl_322 ∷ T_Surjection_918 Source #

d_trans_326 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → T_Surjection_918 → T_Surjection_918 Source #

du_trans_326 ∷ T_Surjection_918 → T_Surjection_918 → T_Surjection_918 Source #

d_to'8315'_346 ∷ T_GeneralizeTel_11671 → T_Surjection_918 → AgdaAny → AgdaAny Source #

du_to'8315'_346 ∷ T_Surjection_918 → AgdaAny → AgdaAny Source #

d__'8776'__352 ∷ T_GeneralizeTel_11671 → T_Surjection_918 → AgdaAny → AgdaAny → () Source #

d__'8776'__378 ∷ T_GeneralizeTel_11671 → T_Surjection_918 → AgdaAny → AgdaAny → () Source #

d_injective'8658'to'8315''45'cong_402 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Surjection_918 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_injective'8658'to'8315''45'cong_402 ∷ T_Setoid_46 → T_Setoid_46 → T_Surjection_918 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'46'generalizedField'45'S'46'a_491 ∷ T_GeneralizeTel_503 → T_Level_18 Source #

d_'46'generalizedField'45'S'46'ℓ_493 ∷ T_GeneralizeTel_503 → T_Level_18 Source #

d_'46'generalizedField'45'S_495 ∷ T_GeneralizeTel_503 → T_Setoid_46 Source #

d_'46'generalizedField'45'T'46'a_497 ∷ T_GeneralizeTel_503 → T_Level_18 Source #

d_'46'generalizedField'45'T'46'ℓ_499 ∷ T_GeneralizeTel_503 → T_Level_18 Source #

d_'46'generalizedField'45'T_501 ∷ T_GeneralizeTel_503 → T_Setoid_46 Source #

d_GeneralizeTel_503 ∷ () Source #

data T_GeneralizeTel_503 Source #

d_'46'generalizedField'45'S'46'a_11659 ∷ T_GeneralizeTel_11671 → T_Level_18 Source #

d_'46'generalizedField'45'S'46'ℓ_11661 ∷ T_GeneralizeTel_11671 → T_Level_18 Source #

d_'46'generalizedField'45'S_11663 ∷ T_GeneralizeTel_11671 → T_Setoid_46 Source #

d_'46'generalizedField'45'T'46'a_11665 ∷ T_GeneralizeTel_11671 → T_Level_18 Source #

d_'46'generalizedField'45'T'46'ℓ_11667 ∷ T_GeneralizeTel_11671 → T_Level_18 Source #

d_'46'generalizedField'45'T_11669 ∷ T_GeneralizeTel_11671 → T_Setoid_46 Source #

d_GeneralizeTel_11671 ∷ () Source #

data T_GeneralizeTel_11671 Source #