Documentation

d_Null'8658'null_50 ∷ T_Level_18 → () → [AgdaAny] → T_All_44 → AgdaAny Source #

du_Null'8658'null_50 ∷ T_All_44 → AgdaAny Source #

d_null'8658'Null_52 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → T_All_44 Source #

du_null'8658'Null_52 ∷ [AgdaAny] → T_All_44 Source #

d_'91''93''61''45'injective_62 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → AgdaAny → T_All_44 → T_Any_34 → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 → T__'8801'__12 Source #

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

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

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

d_'172'All'8658'Any'172'_94 ∷ 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'_94 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 Source #

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

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

du_'172'Any'8608'All'172'_142 ∷ [AgdaAny] → T_Surjection_846 Source #

d_to'8728'from_152 ∷ 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_188 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T_Equivalence_1714 Source #

du_Any'172''8660''172'All_188 ∷ [AgdaAny] → (AgdaAny → T_Dec_20) → T_Equivalence_1714 Source #

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

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

d_'91''93''61'lookup_252 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → T__'91'_'93''61'__74 Source #

du_'91''93''61'lookup_252 ∷ [AgdaAny] → T_All_44 → T_Any_34 → T__'91'_'93''61'__74 Source #

d_'91''93''61''8658'lookup_270 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → T__'91'_'93''61'__74 → T__'8801'__12 Source #

d_lookup'8658''91''93''61'_280 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → T__'8801'__12 → T__'91'_'93''61'__74 Source #

du_lookup'8658''91''93''61'_280 ∷ [AgdaAny] → T_All_44 → T_Any_34 → T__'91'_'93''61'__74 Source #

d_map'45'cong_294 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_All_44 → (AgdaAny → AgdaAny → T__'8801'__12) → T__'8801'__12 Source #

d_map'45'id_304 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #

d_map'45''8728'_318 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 Source #

d_lookup'45'map_332 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T_All_44 → T_Any_34 → T__'8801'__12 Source #

d_updateAt'45'updates_352 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → AgdaAny → T_All_44 → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 Source #

du_updateAt'45'updates_352 ∷ [AgdaAny] → T_Any_34 → T_All_44 → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 Source #

d_updateAt'45'minimal_376 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → AgdaAny → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_Any_34 → (AgdaAny → AgdaAny) → AgdaAny → T_All_44 → (T__'8801'__12 → T__'8801'__12 → T_Irrelevant_20) → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 Source #

du_updateAt'45'minimal_376 ∷ [AgdaAny] → T_Any_34 → T_Any_34 → T_All_44 → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 Source #

d_lookup'8728'updateAt_420 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → (AgdaAny → AgdaAny) → T__'8801'__12 Source #

d_lookup'8728'updateAt'8242'_436 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → AgdaAny → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_Any_34 → (AgdaAny → AgdaAny) → AgdaAny → T_All_44 → (T__'8801'__12 → T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #

d_updateAt'45'id'45'local_452 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 → T__'8801'__12 Source #

d_updateAt'45'id_476 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_All_44 → T__'8801'__12 Source #

d_updateAt'45''8728''45'local_492 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 → T__'8801'__12 Source #

d_updateAt'45''8728'_518 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 Source #

d_updateAt'45'cong'45'local_532 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 → T__'8801'__12 Source #

d_updateAt'45'cong_558 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T_All_44 → T__'8801'__12 Source #

d_updateAt'45'commutes_574 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → AgdaAny → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (T__'8801'__12 → T__'8801'__12 → T_Irrelevant_20) → T_All_44 → T__'8801'__12 Source #

d_map'45'updateAt_620 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T_Any_34 → T__'8801'__12 → T__'8801'__12 Source #

d_singleton'8315'_638 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_All_44 → AgdaAny Source #

du_singleton'8315'_638 ∷ T_All_44 → AgdaAny Source #

d_head'8314'_642 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #

du_head'8314'_642 ∷ T_All_44 → T_All_18 Source #

d_tail'8314'_646 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #

du_tail'8314'_646 ∷ T_All_44 → T_All_18 Source #

d_last'8314'_650 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #

du_last'8314'_650 ∷ [AgdaAny] → T_All_44 → T_All_18 Source #

d_uncons'8314'_658 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #

du_uncons'8314'_658 ∷ T_All_44 → T_All_18 Source #

d_uncons'8315'_664 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_18 → T_All_44 Source #

du_uncons'8315'_664 ∷ [AgdaAny] → T_All_18 → T_All_44 Source #

d_map'8314'_676 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #

du_map'8314'_676 ∷ [AgdaAny] → T_All_44 → T_All_44 Source #

d_map'8315'_684 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #

du_map'8315'_684 ∷ [AgdaAny] → T_All_44 → T_All_44 Source #

d_gmap'8314'_692 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_gmap'8314'_692 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

d_gmap'8315'_698 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_gmap'8315'_698 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

d_mapMaybe'8314'_704 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → Maybe AgdaAny) → T_All_44 → T_All_44 Source #

du_mapMaybe'8314'_704 ∷ [AgdaAny] → (AgdaAny → Maybe AgdaAny) → T_All_44 → T_All_44 Source #

d_All'45'catMaybes'8314'_750 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [Maybe AgdaAny] → T_All_44 → T_All_44 Source #

du_All'45'catMaybes'8314'_750 ∷ [Maybe AgdaAny] → T_All_44 → T_All_44 Source #

d_Any'45'catMaybes'8314'_758 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [Maybe AgdaAny] → T_All_44 → T_All_44 Source #

du_Any'45'catMaybes'8314'_758 ∷ [Maybe AgdaAny] → T_All_44 → T_All_44 Source #

d_'43''43''8314'_760 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 → T_All_44 Source #

du_'43''43''8314'_760 ∷ [AgdaAny] → T_All_44 → T_All_44 → T_All_44 Source #

d_'43''43''8315''737'_774 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 Source #

du_'43''43''8315''737'_774 ∷ [AgdaAny] → T_All_44 → T_All_44 Source #

d_'43''43''8315''691'_790 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 Source #

du_'43''43''8315''691'_790 ∷ [AgdaAny] → T_All_44 → T_All_44 Source #

d_'43''43''8315'_806 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_Σ_14 Source #

du_'43''43''8315'_806 ∷ [AgdaAny] → T_All_44 → T_Σ_14 Source #

d_'43''43''8596'_820 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Inverse_1960 Source #

du_'43''43''8596'_820 ∷ [AgdaAny] → T_Inverse_1960 Source #

d_'43''43''8314''8728''43''43''8315'_832 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T__'8801'__12 Source #

d_'43''43''8315''8728''43''43''8314'_846 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Σ_14 → T__'8801'__12 Source #

d_concat'8314'_862 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [[AgdaAny]] → T_All_44 → T_All_44 Source #

du_concat'8314'_862 ∷ [[AgdaAny]] → T_All_44 → T_All_44 Source #

d_concat'8315'_870 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [[AgdaAny]] → T_All_44 → T_All_44 Source #

du_concat'8315'_870 ∷ [[AgdaAny]] → T_All_44 → T_All_44 Source #

d_'8759''691''8314'_878 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny → T_All_44 Source #

du_'8759''691''8314'_878 ∷ [AgdaAny] → T_All_44 → AgdaAny → T_All_44 Source #

d_'8759''691''8315'_884 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → T_Σ_14 Source #

du_'8759''691''8315'_884 ∷ [AgdaAny] → T_All_44 → T_Σ_14 Source #

d_unsnoc'8314'_888 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #

du_unsnoc'8314'_888 ∷ [AgdaAny] → T_All_44 → T_All_18 Source #

d_unsnoc'8315'_906 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_18 → T_All_44 Source #

du_unsnoc'8315'_906 ∷ [AgdaAny] → T_All_18 → T_All_44 Source #

d__'8712'__942 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → AgdaAny → [AgdaAny] → () Source #

d__'8712'__946 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → AgdaAny → [AgdaAny] → () Source #

d_cartesianProductWith'8314'_958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #

du_cartesianProductWith'8314'_958 ∷ T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #

d_cartesianProduct'8314'_984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → (T_Σ_14 → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #

du_cartesianProduct'8314'_984 ∷ T_Setoid_44 → T_Setoid_44 → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #

d_drop'8314'_988 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → Integer → T_All_44 → T_All_44 Source #

du_drop'8314'_988 ∷ [AgdaAny] → Integer → T_All_44 → T_All_44 Source #

d_dropWhile'8314'_1002 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T_All_44 → T_All_44 Source #

du_dropWhile'8314'_1002 ∷ [AgdaAny] → (AgdaAny → T_Dec_20) → T_All_44 → T_All_44 Source #

d_dropWhile'8315'_1042 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T__'8801'__12 → T_All_44 Source #

du_dropWhile'8315'_1042 ∷ [AgdaAny] → (AgdaAny → T_Dec_20) → T_All_44 Source #

d_all'45'head'45'dropWhile_1084 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_18 Source #

du_all'45'head'45'dropWhile_1084 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_18 Source #

d_take'8314'_1116 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → Integer → T_All_44 → T_All_44 Source #

du_take'8314'_1116 ∷ [AgdaAny] → Integer → T_All_44 → T_All_44 Source #

d_takeWhile'8314'_1130 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T_All_44 → T_All_44 Source #

du_takeWhile'8314'_1130 ∷ [AgdaAny] → (AgdaAny → T_Dec_20) → T_All_44 → T_All_44 Source #

d_takeWhile'8315'_1170 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T__'8801'__12 → T_All_44 Source #

du_takeWhile'8315'_1170 ∷ [AgdaAny] → (AgdaAny → T_Dec_20) → T_All_44 Source #

d_all'45'takeWhile_1212 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 Source #

du_all'45'takeWhile_1212 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 Source #

d_applyUpTo'8314''8321'_1248 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → T__'8804'__22 → AgdaAny) → T_All_44 Source #

du_applyUpTo'8314''8321'_1248 ∷ Integer → (Integer → T__'8804'__22 → AgdaAny) → T_All_44 Source #

d_applyUpTo'8314''8322'_1266 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → AgdaAny) → T_All_44 Source #

du_applyUpTo'8314''8322'_1266 ∷ Integer → (Integer → AgdaAny) → T_All_44 Source #

d_applyUpTo'8315'_1282 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → T_All_44 → Integer → T__'8804'__22 → AgdaAny Source #

du_applyUpTo'8315'_1282 ∷ T_All_44 → T__'8804'__22 → AgdaAny Source #

d_all'45'upTo_1302 ∷ Integer → T_All_44 Source #

d_applyDownFrom'8314''8321'_1312 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → T__'8804'__22 → AgdaAny) → T_All_44 Source #

du_applyDownFrom'8314''8321'_1312 ∷ Integer → (Integer → T__'8804'__22 → AgdaAny) → T_All_44 Source #

d_applyDownFrom'8314''8322'_1330 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → AgdaAny) → T_All_44 Source #

du_applyDownFrom'8314''8322'_1330 ∷ Integer → (Integer → AgdaAny) → T_All_44 Source #

d_tabulate'8314'_1346 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Integer → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → T_All_44 Source #

du_tabulate'8314'_1346 ∷ Integer → (T_Fin_10 → AgdaAny) → T_All_44 Source #

d_tabulate'8315'_1358 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Integer → (T_Fin_10 → AgdaAny) → T_All_44 → T_Fin_10 → AgdaAny Source #

du_tabulate'8315'_1358 ∷ T_All_44 → T_Fin_10 → AgdaAny Source #

d_'9472''8314'_1368 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_All_44 → T_All_44 Source #

du_'9472''8314'_1368 ∷ [AgdaAny] → T_Any_34 → T_All_44 → T_All_44 Source #

d_'9472''8315'_1382 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → AgdaAny → T_All_44 → T_All_44 Source #

du_'9472''8315'_1382 ∷ [AgdaAny] → T_Any_34 → AgdaAny → T_All_44 → T_All_44 Source #

d_all'45'filter_1408 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 Source #

du_all'45'filter_1408 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 Source #

d_filter'8314'_1428 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_filter'8314'_1428 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 → T_All_44 Source #

d_filter'8315'_1452 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 → T_All_44 Source #

du_filter'8315'_1452 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 → T_All_44 → T_All_44 Source #

d_partition'45'All_1524 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Σ_14 Source #

du_partition'45'All_1524 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_Σ_14 Source #

d_derun'8314'_1544 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_derun'8314'_1544 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 → T_All_44 Source #

d_deduplicate'8314'_1584 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_deduplicate'8314'_1584 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 → T_All_44 Source #

d_derun'8315'_1592 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_derun'8315'_1592 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

d_aux_1616 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 → AgdaAny → [AgdaAny] → T_All_44 → T_All_44 Source #

du_aux_1616 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 → T_All_44 Source #

d_deduplicate'8315'_1664 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_deduplicate'8315'_1664 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

d_aux_1688 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny → T_Any_34 → AgdaAny Source #

du_aux_1688 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zipWith'8314'_1700 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → T_Pointwise_48 → T_All_44 Source #

du_zipWith'8314'_1700 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 Source #

d_fromMaybe'8314'_1712 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Maybe AgdaAny → T_All_18 → T_All_44 Source #

du_fromMaybe'8314'_1712 ∷ T_All_18 → T_All_44 Source #

d_fromMaybe'8315'_1718 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Maybe AgdaAny → T_All_44 → T_All_18 Source #

du_fromMaybe'8315'_1718 ∷ Maybe AgdaAny → T_All_44 → T_All_18 Source #

d_replicate'8314'_1728 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → Integer → AgdaAny → T_All_44 Source #

du_replicate'8314'_1728 ∷ Integer → AgdaAny → T_All_44 Source #

d_replicate'8315'_1738 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → Integer → T_All_44 → AgdaAny Source #

du_replicate'8315'_1738 ∷ T_All_44 → AgdaAny Source #

d_inits'8314'_1742 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_inits'8314'_1742 ∷ [AgdaAny] → T_All_44 → T_All_44 Source #

d_inits'8315'_1752 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_inits'8315'_1752 ∷ [AgdaAny] → T_All_44 → T_All_44 Source #

d_tails'8314'_1768 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_tails'8314'_1768 ∷ [AgdaAny] → T_All_44 → T_All_44 Source #

d_tails'8315'_1776 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_tails'8315'_1776 ∷ [AgdaAny] → T_All_44 → T_All_44 Source #

d_all'8314'_1796 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → AgdaAny → T_All_44 Source #

du_all'8314'_1796 ∷ (AgdaAny → Bool) → [AgdaAny] → AgdaAny → T_All_44 Source #

d_all'8315'_1808 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T_All_44 → AgdaAny Source #

du_all'8315'_1808 ∷ (AgdaAny → Bool) → [AgdaAny] → T_All_44 → AgdaAny Source #

d_anti'45'mono_1814 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Any_34 → T_Any_34) → T_All_44 → T_All_44 Source #

du_anti'45'mono_1814 ∷ [AgdaAny] → [AgdaAny] → (AgdaAny → T_Any_34 → T_Any_34) → T_All_44 → T_All_44 Source #

d_all'45'anti'45'mono_1822 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → (AgdaAny → Bool) → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny → AgdaAny Source #

du_all'45'anti'45'mono_1822 ∷ [AgdaAny] → [AgdaAny] → (AgdaAny → Bool) → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny → AgdaAny Source #

d__'8779'__1862 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → [AgdaAny] → [AgdaAny] → () Source #

d_respects_1916 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #

du_respects_1916 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #

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

d_updateAt'45'id'45'relative_1932 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 → T__'8801'__12 Source #

d_updateAt'45'compose'45'relative_1934 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 → T__'8801'__12 Source #

d_updateAt'45'compose_1936 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 Source #

d_updateAt'45'cong'45'relative_1938 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 → T__'8801'__12 Source #

d_gmap_1940 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

d_map'45'compose_1942 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 Source #

d_'46'generalizedField'45'P'46'a_101595 ∷ T_GeneralizeTel_101603 → T_Level_18 Source #

d_'46'generalizedField'45'P'46'A_101597 ∷ T_GeneralizeTel_101603 → () Source #

d_'46'generalizedField'45'P'46'p_101599 ∷ T_GeneralizeTel_101603 → T_Level_18 Source #

d_'46'generalizedField'45'P_101601 ∷ T_GeneralizeTel_101603 → AgdaAny → () Source #

d_GeneralizeTel_101603 ∷ p → p → p → p → p → () Source #

data T_GeneralizeTel_101603 Source #