Documentation

d_'172'Any'8658'All'172'_38 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (T_Any_34 → T_Irrelevant_20) → T_All_44 Source #

du_'172'Any'8658'All'172'_38 ∷ [AgdaAny] → (T_Any_34 → T_Irrelevant_20) → T_All_44 Source #

d_All'172''8658''172'Any_50 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_Any_34 → T_Irrelevant_20 Source #

d_'172'All'8658'Any'172'_62 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → (T_All_44 → T_Irrelevant_20) → T_Any_34 Source #

du_'172'All'8658'Any'172'_62 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 Source #

d_Any'172''8658''172'All_102 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_All_44 → T_Irrelevant_20 Source #

d_'172'Any'8608'All'172'_110 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Surjection_918 Source #

du_'172'Any'8608'All'172'_110 ∷ [AgdaAny] → T_Surjection_918 Source #

d_to'8728'from_120 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #

d_Any'172''8660''172'All_156 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T_Equivalence_1858 Source #

du_Any'172''8660''172'All_156 ∷ [AgdaAny] → (AgdaAny → T_Dec_20) → T_Equivalence_1858 Source #

d_All'45'swap_198 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 Source #

du_All'45'swap_198 ∷ [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 Source #

d_'46'generalizedField'45'P'46'a_28211 ∷ T_GeneralizeTel_28219 → T_Level_18 Source #

d_'46'generalizedField'45'P'46'A_28213 ∷ T_GeneralizeTel_28219 → () Source #

d_'46'generalizedField'45'P'46'p_28215 ∷ T_GeneralizeTel_28219 → T_Level_18 Source #

d_'46'generalizedField'45'P_28217 ∷ T_GeneralizeTel_28219 → AgdaAny → () Source #

d_GeneralizeTel_28219 ∷ p → p → p → p → p → () Source #

data T_GeneralizeTel_28219 Source #