Documentation

d__'8759''691''8321'__22 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_RawPushout_232 -> T_RawPushout_232 Source #

du__'8759''691''8321'__22 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_RawPushout_232 -> T_RawPushout_232 Source #

d__'8759''691''8322'__24 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_RawPushout_232 -> T_RawPushout_232 Source #

du__'8759''691''8322'__24 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_RawPushout_232 -> T_RawPushout_232 Source #

d_Sublist_27 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d__'8759''7523''45'ub__30 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_UpperBound_388 -> T_UpperBound_388 Source #

du__'8759''7523''45'ub__30 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_UpperBound_388 -> T_UpperBound_388 Source #

d__'8759''8343''45'ub__36 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_UpperBound_388 -> T_UpperBound_388 Source #

du__'8759''8343''45'ub__36 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_UpperBound_388 -> T_UpperBound_388 Source #

d__'8834'__42 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> () Source #

d__'8835'__44 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> () Source #

d__'8836'__46 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> () Source #

d__'8837'__48 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> () Source #

d__'8838'__50 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> () Source #

d__'8839'__52 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> () Source #

d__'8840'__54 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> () Source #

d__'8841'__56 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> () Source #

d_Disjoint_58 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_DisjointUnion_60 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

d_RawPushout_62 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_UpperBound_64 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

d_fromAny_72 :: T_Level_14 -> () -> AgdaAny -> [AgdaAny] -> T_Any_34 -> T_Sublist_26 Source #

du_fromAny_72 :: AgdaAny -> [AgdaAny] -> T_Any_34 -> T_Sublist_26 Source #

d_map_74 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

du_map_74 :: T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 Source #

d_minimum_76 :: T_Level_14 -> () -> [AgdaAny] -> T_Sublist_26 Source #

du_minimum_76 :: [AgdaAny] -> T_Sublist_26 Source #

d_toAny_78 :: T_Level_14 -> () -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Any_34 Source #

du_toAny_78 :: AgdaAny -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Any_34 Source #

d_'8759''45'rpo_80 :: T_Level_14 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T__'8801'__12 -> T__'8801'__12 -> T_RawPushout_232 -> T_RawPushout_232 Source #

du_'8759''45'rpo_80 :: AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T__'8801'__12 -> T__'8801'__12 -> T_RawPushout_232 -> T_RawPushout_232 Source #

d_'8759''8345''45'ub_82 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_UpperBound_388 -> T_UpperBound_388 Source #

du_'8759''8345''45'ub_82 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_UpperBound_388 -> T_UpperBound_388 Source #

d_'8838''45'disjoint'45'union_84 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_UpperBound_388 Source #

du_'8838''45'disjoint'45'union_84 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_UpperBound_388 Source #

d_'8838''45'join'737'_86 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Σ_14 Source #

du_'8838''45'join'737'_86 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Σ_14 Source #

d_'8838''45'pushout'737'_88 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_RawPushout_232 Source #

du_'8838''45'pushout'737'_88 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_RawPushout_232 Source #

d_refl_90 :: T_Level_14 -> () -> [AgdaAny] -> T_Sublist_26 Source #

du_refl_90 :: [AgdaAny] -> T_Sublist_26 Source #

d_trans_92 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

du_trans_92 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

d_leg'8321'_116 :: T_RawPushout_232 -> T_Sublist_26 Source #

d_leg'8322'_118 :: T_RawPushout_232 -> T_Sublist_26 Source #

d_upperBound_120 :: T_RawPushout_232 -> [AgdaAny] Source #

d_inj'8321'_124 :: T_UpperBound_388 -> T_Sublist_26 Source #

d_inj'8322'_126 :: T_UpperBound_388 -> T_Sublist_26 Source #

d_sub_128 :: T_UpperBound_388 -> T_Sublist_26 Source #

d_theUpperBound_130 :: T_UpperBound_388 -> [AgdaAny] Source #

d_lookup_144 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Any_34 -> T_Any_34 Source #

du_lookup_144 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Any_34 -> T_Any_34 Source #

d_'8838''45'reflexive_146 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> T__'8801'__12 -> T_Sublist_26 Source #

du_'8838''45'reflexive_146 :: [AgdaAny] -> T_Sublist_26 Source #

d_'8838''45'antisym_148 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T__'8801'__12 Source #

d_'8838''45'isPreorder_154 :: T_Level_14 -> () -> T_IsPreorder_70 Source #

du_'8838''45'isPreorder_154 :: T_IsPreorder_70 Source #

d_'8838''45'isPartialOrder_156 :: T_Level_14 -> () -> T_IsPartialOrder_162 Source #

du_'8838''45'isPartialOrder_156 :: T_IsPartialOrder_162 Source #

d_'8838''45'preorder_158 :: T_Level_14 -> () -> T_Preorder_132 Source #

du_'8838''45'preorder_158 :: T_Preorder_132 Source #

d_'8838''45'poset_160 :: T_Level_14 -> () -> T_Poset_282 Source #

du_'8838''45'poset_160 :: T_Poset_282 Source #

d_Separation_172 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> () Source #

data T_Separation_172 Source #

d_inflation_196 :: T_Separation_172 -> [AgdaAny] Source #

d_separator'8321'_198 :: T_Separation_172 -> T_Sublist_26 Source #

d_separator'8322'_200 :: T_Separation_172 -> T_Sublist_26 Source #

d_separated'8321'_202 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Separation_172 -> T_Sublist_26 Source #

du_separated'8321'_202 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Separation_172 -> T_Sublist_26 Source #

d_separated'8322'_204 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Separation_172 -> T_Sublist_26 Source #

du_separated'8322'_204 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Separation_172 -> T_Sublist_26 Source #

d_disjoint_206 :: T_Separation_172 -> T_Disjoint_130 Source #

d_'91''93''45'Sep_208 :: T_Level_14 -> () -> T_Separation_172 Source #

du_'91''93''45'Sep_208 :: T_Separation_172 Source #

d__'8759''8345''45'Sep__222 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_Separation_172 -> T_Separation_172 Source #

du__'8759''8345''45'Sep__222 :: AgdaAny -> T_Separation_172 -> T_Separation_172 Source #

d__'8759''8343''45'Sep__248 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Separation_172 -> T_Separation_172 Source #

du__'8759''8343''45'Sep__248 :: AgdaAny -> T_Separation_172 -> T_Separation_172 Source #

d__'8759''7523''45'Sep__272 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Separation_172 -> T_Separation_172 Source #

du__'8759''7523''45'Sep__272 :: AgdaAny -> T_Separation_172 -> T_Separation_172 Source #

d_'8759''45'Sep'737'_300 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T_Separation_172 -> T_Separation_172 Source #

du_'8759''45'Sep'737'_300 :: AgdaAny -> T_Separation_172 -> T_Separation_172 Source #

d_separate'737'_318 :: T_Level_14 -> () -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Separation_172 Source #

du_separate'737'_318 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Separation_172 Source #