Documentation

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

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

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

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

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

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

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

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

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

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

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

d_fromAny_166 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> AgdaAny -> [AgdaAny] -> T_Any_34 -> T_Sublist_26 Source #

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

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

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

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

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

d_minimum_172 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> T_Sublist_26 Source #

du_minimum_172 :: [AgdaAny] -> T_Sublist_26 Source #

d_toAny_174 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Any_34 Source #

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

d_'8838''45'reflexive_196 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Sublist_26 Source #

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

d_refl_200 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> T_Sublist_26 Source #

du_refl_200 :: T_Setoid_44 -> [AgdaAny] -> T_Sublist_26 Source #

d_trans_204 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

du_trans_204 :: T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Sublist_26 Source #

d_antisym_212 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Pointwise_48 Source #

du_antisym_212 :: [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Pointwise_48 Source #

d_'8838''45'isPreorder_214 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_IsPreorder_70 Source #

du_'8838''45'isPreorder_214 :: T_Setoid_44 -> T_IsPreorder_70 Source #

d_'8838''45'isPartialOrder_216 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_IsPartialOrder_162 Source #

du_'8838''45'isPartialOrder_216 :: T_Setoid_44 -> T_IsPartialOrder_162 Source #

d_'8838''45'preorder_218 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Preorder_132 Source #

du_'8838''45'preorder_218 :: T_Setoid_44 -> T_Preorder_132 Source #

d_'8838''45'poset_220 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Poset_282 Source #

du_'8838''45'poset_220 :: T_Setoid_44 -> T_Poset_282 Source #

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

data T_RawPushout_232 Source #

d_upperBound_250 :: T_RawPushout_232 -> [AgdaAny] Source #

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

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

d__'8759''691''8321'__268 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_RawPushout_232 -> T_RawPushout_232 Source #

du__'8759''691''8321'__268 :: T_Setoid_44 -> AgdaAny -> T_RawPushout_232 -> T_RawPushout_232 Source #

d__'8759''691''8322'__286 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_RawPushout_232 -> T_RawPushout_232 Source #

du__'8759''691''8322'__286 :: T_Setoid_44 -> AgdaAny -> T_RawPushout_232 -> T_RawPushout_232 Source #

d_'8759''45'rpo_312 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> T_RawPushout_232 -> T_RawPushout_232 Source #

du_'8759''45'rpo_312 :: T_Setoid_44 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_RawPushout_232 -> T_RawPushout_232 Source #

d_'8838''45'pushout'737'_330 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_RawPushout_232 Source #

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

d_'8838''45'join'737'_366 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Σ_14 Source #

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

d_rpo_376 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_RawPushout_232 Source #

du_rpo_376 :: T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_RawPushout_232 Source #

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

data T_UpperBound_388 Source #

d_theUpperBound_408 :: T_UpperBound_388 -> [AgdaAny] Source #

d_sub_410 :: T_UpperBound_388 -> T_Sublist_26 Source #

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

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

d_'8759''8345''45'ub_428 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> T_UpperBound_388 -> T_UpperBound_388 Source #

du_'8759''8345''45'ub_428 :: T_UpperBound_388 -> T_UpperBound_388 Source #

d__'8759''8343''45'ub__448 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> AgdaAny -> T_UpperBound_388 -> T_UpperBound_388 Source #

du__'8759''8343''45'ub__448 :: T_Setoid_44 -> AgdaAny -> AgdaAny -> T_UpperBound_388 -> T_UpperBound_388 Source #

d__'8759''7523''45'ub__470 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> AgdaAny -> AgdaAny -> AgdaAny -> T_UpperBound_388 -> T_UpperBound_388 Source #

du__'8759''7523''45'ub__470 :: T_Setoid_44 -> AgdaAny -> AgdaAny -> T_UpperBound_388 -> T_UpperBound_388 Source #

d_'8838''45'disjoint'45'union_486 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Sublist_26 -> T_Sublist_26 -> T_Disjoint_130 -> T_UpperBound_388 Source #

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

d_Sublist_2011 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #