Theory CZH_ECAT_CSimplicial

(* Copyright 2020 (C) Mihails Milehins *)

section‹Simplicial category›
theory CZH_ECAT_CSimplicial
  imports CZH_ECAT_Ordinal
begin



subsection‹Background›


text‹
The content of this section is based, primarily, on the elements of the 
content of Chapter I-2 in cite‹"mac_lane_categories_2010"›.
›

named_theorems cat_simplicial_cs_simps
named_theorems cat_simplicial_cs_intros



subsection‹Composable arrows for simplicial category›

definition composable_cat_simplicial :: "V ⇒ V ⇒ V"
  where "composable_cat_simplicial α A = set
    {
      [g, f]∘ | g f. ∃m n p.
        g : cat_ordinal n ≤C.PEO⇘α⇙ cat_ordinal p ∧
        f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n ∧
        m ∈∘ A ∧ n ∈∘ A ∧ p ∈∘ A
    }"

lemma small_composable_cat_simplicial[simp]:
  "small
    {
      [g, f]∘ | g f. ∃m n p.
        g : cat_ordinal n ≤C.PEO⇘α⇙ cat_ordinal p ∧
        f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n ∧
        m ∈∘ A ∧ n ∈∘ A ∧ p ∈∘ A
    }"
  (is ‹small ?S›)
proof(rule down)
  show "?S ⊆ elts (all_cfs α ×∙ all_cfs α)"
  proof
    (
      intro subsetI, 
      unfold mem_Collect_eq, elim exE conjE; simp only:; intro ftimesI2
    )
    fix m n p g f 
    assume prems: 
      "m ∈∘ A"
      "n ∈∘ A"
      "p ∈∘ A"
      "g : cat_ordinal n ≤C.PEO⇘α⇙ cat_ordinal p"
      "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
    interpret g: is_preorder_functor α ‹cat_ordinal n› ‹cat_ordinal p› g
      by (rule prems(4))
    interpret f: is_preorder_functor α ‹cat_ordinal m› ‹cat_ordinal n› f
      by (rule prems(5))
    from g.is_functor_axioms show "g ∈∘ all_cfs α" by auto
    from f.is_functor_axioms show "f ∈∘ all_cfs α" by auto
  qed
qed


text‹Rules.›

lemma composable_cat_simplicialI:
  assumes "g : cat_ordinal n ≤C.PEO⇘α⇙ cat_ordinal p"
    and "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
    and "m ∈∘ A" 
    and "n ∈∘ A"
    and "p ∈∘ A"
    and "gf = [g, f]∘"
  shows "gf ∈∘ composable_cat_simplicial α A"
  using assms
  unfolding composable_cat_simplicial_def
  by (intro in_small_setI small_composable_cat_simplicial) auto

lemma composable_cat_simplicialE[elim]:
  assumes "gf ∈∘ composable_cat_simplicial α A"
  obtains g f m n p where "gf = [g, f]∘" 
    and "g : cat_ordinal n ≤C.PEO⇘α⇙ cat_ordinal p"
    and "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
    and "m ∈∘ A" 
    and "n ∈∘ A"
    and "p ∈∘ A"
proof-
  from assms obtain g f m n p where 
    "gf = [g, f]∘"
    "g : cat_ordinal n ≤C.PEO⇘α⇙ cat_ordinal p"
    "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
    "m ∈∘ A" 
    "n ∈∘ A" 
    "p ∈∘ A"
    unfolding composable_cat_simplicial_def
    by (elim in_small_setE, intro small_composable_cat_simplicial) auto
  with that show ?thesis by auto
qed



subsection‹Simplicial category›


subsubsection‹Definition and elementary properties›

definition cat_simplicial :: "V ⇒ V ⇒ V"
  where "cat_simplicial α A =
    [
      set {cat_ordinal m | m. m ∈∘ A},
      set
        {
          f. ∃m n.
            f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n ∧ m ∈∘ A ∧ n ∈∘ A
        },
      (
        λf∈∘ set
          {
            f. ∃m n.
              f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n ∧ m ∈∘ A ∧ n ∈∘ A
          }. f⦇HomDom⦈
      ),
      (
        λf∈∘ set
          {
            f. ∃m n.
              f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n ∧ m ∈∘ A ∧ n ∈∘ A
          }. f⦇HomCod⦈
      ),
      (λgf∈∘composable_cat_simplicial α A. gf⦇0⦈ ∘CF gf⦇1ℕ⦈),
      (λm∈∘set {cat_ordinal m | m. m ∈∘ A}. cf_id m)
    ]∘"


text‹Components.›

lemma cat_simplicial_components:
  shows "cat_simplicial α A⦇Obj⦈ = set {cat_ordinal m | m. m ∈∘ A}"
    and "cat_simplicial α A⦇Arr⦈ = 
      set {f. ∃m n. f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n ∧ m ∈∘ A ∧ n ∈∘ A}"
    and "cat_simplicial α A⦇Dom⦈ =
      (
        λf∈∘set
          {
            f. ∃m n.
              f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n ∧ m ∈∘ A ∧ n ∈∘ A
          }. f⦇HomDom⦈
      )"
    and "cat_simplicial α A⦇Cod⦈ =
      (
        λf∈∘set
          {
            f. ∃m n.
              f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n ∧ m ∈∘ A ∧ n ∈∘ A
          }. f⦇HomCod⦈
      )"
    and "cat_simplicial α A⦇Comp⦈ =
      (λgf∈∘composable_cat_simplicial α A. gf⦇0⦈ ∘CF gf⦇1ℕ⦈)"
    and "cat_simplicial α A⦇CId⦈ =
      (λm∈∘set {cat_ordinal m | m. m ∈∘ A}. cf_id m)"
  unfolding cat_simplicial_def dg_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Objects›

lemma cat_simplicial_ObjI[cat_simplicial_cs_intros]:
  assumes "m ∈∘ A" and "a = cat_ordinal m"
  shows "a ∈∘ cat_simplicial α A⦇Obj⦈ "
  using assms unfolding cat_simplicial_components by auto

lemma cat_simplicial_ObjD:
  assumes "cat_ordinal m ∈∘ cat_simplicial α A⦇Obj⦈ "
  shows "m ∈∘ A" 
  using assms cat_ordinal_inj unfolding cat_simplicial_components by auto

lemma cat_simplicial_ObjE:
  assumes "M ∈∘ cat_simplicial α A⦇Obj⦈ "
  obtains m where "M = cat_ordinal m" and "m ∈∘ A" 
  using assms cat_ordinal_inj that unfolding cat_simplicial_components by auto


subsubsection‹Arrows›

lemma small_cat_simplicial_Arr[simp]: 
  "small {f. ∃m n. f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n ∧ m ∈∘ A ∧ n ∈∘ A}"
  (is ‹small ?S›)
proof(rule down)
  show "?S ⊆ elts (all_cfs α)" by auto
qed

lemma cat_simplicial_ArrI[cat_simplicial_cs_intros]:
  assumes "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n" and "m ∈∘ A" and "n ∈∘ A" 
  shows "f ∈∘ cat_simplicial α A⦇Arr⦈"
  using assms 
  unfolding cat_simplicial_components
  by (intro in_small_setI small_cat_simplicial_Arr) auto

lemma cat_simplicial_ArrE:
  assumes "f ∈∘ cat_simplicial α A⦇Arr⦈"
  obtains m n 
    where "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n" and "m ∈∘ A" and "n ∈∘ A" 
proof-
  from assms cat_ordinal_inj obtain m n 
    where "m ∈∘ A" "n ∈∘ A" "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
    unfolding cat_simplicial_components
    by (elim in_small_setE, intro small_cat_simplicial_Arr) auto
  with that show ?thesis by simp
qed


subsubsection‹Domain›

mk_VLambda cat_simplicial_components(3)
  |vsv cat_simplicial_Dom_vsv[cat_simplicial_cs_intros]|
  |vdomain 
    cat_simplicial_Dom_vdomain[
      folded cat_simplicial_components, cat_simplicial_cs_simps
    ]
  |
  |app cat_simplicial_Dom_app[folded cat_simplicial_components]|

lemma cat_simplicial_Dom_app'[cat_simplicial_cs_simps]:
  assumes "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n" and "m ∈∘ A" and "n ∈∘ A" 
  shows "cat_simplicial α A⦇Dom⦈⦇f⦈ = cat_ordinal m"
proof-
  interpret f: is_preorder_functor α ‹cat_ordinal m› ‹cat_ordinal n› f 
    by (rule assms(1))
  from assms show "cat_simplicial α A⦇Dom⦈⦇f⦈ = cat_ordinal m"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cat_simplicial_Dom_app 
          cs_intro: cat_simplicial_cs_intros
      )
qed


subsubsection‹Codomain›

mk_VLambda cat_simplicial_components(4)
  |vsv cat_simplicial_Cod_vsv[cat_simplicial_cs_intros]|
  |vdomain 
    cat_simplicial_Cod_vdomain[
      folded cat_simplicial_components, cat_simplicial_cs_simps
    ]
  |
  |app cat_simplicial_Cod_app[folded cat_simplicial_components]|


lemma cat_simplicial_Cod_app'[cat_simplicial_cs_simps]:
  assumes "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n" and "m ∈∘ A" and "n ∈∘ A" 
  shows "cat_simplicial α A⦇Cod⦈⦇f⦈ = cat_ordinal n"
proof-
  interpret f: is_preorder_functor α ‹cat_ordinal m› ‹cat_ordinal n› f 
    by (rule assms(1))
  from assms show "cat_simplicial α A⦇Cod⦈⦇f⦈ = cat_ordinal n"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_simplicial_Cod_app 
          cs_intro: cat_simplicial_cs_intros
      )
qed


subsubsection‹Arrow with a domain and a codomain›

lemma cat_simplicial_is_arrI: 
  assumes "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
    and "m ∈∘ A" 
    and "n ∈∘ A"
  shows "f : cat_ordinal m ↦⇘cat_simplicial α A⇙ cat_ordinal n"
proof(intro is_arrI cat_simplicial_ArrI, rule assms; (intro assms(2,3))?)
  from assms show 
    "cat_simplicial α A⦇Dom⦈⦇f⦈ = cat_ordinal m"
    "cat_simplicial α A⦇Cod⦈⦇f⦈ = cat_ordinal n"
    by (cs_concl cs_shallow cs_simp: cat_simplicial_cs_simps)+
qed

lemma cat_simplicial_is_arrI'[cat_simplicial_cs_intros]: 
  assumes "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
    and "m ∈∘ A" 
    and "n ∈∘ A"
    and "a = cat_ordinal m"
    and "b = cat_ordinal n"
  shows "f : a ↦⇘cat_simplicial α A⇙ b"
  using assms(1-3) unfolding assms(4-5) by (rule cat_simplicial_is_arrI)

lemma cat_simplicial_is_arrD[dest]: 
  assumes "f : cat_ordinal m ↦⇘cat_simplicial α A⇙ cat_ordinal n"
    and "m ∈∘ A" 
    and "n ∈∘ A"
  shows "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
proof-
  note f = is_arrD[OF assms(1)]
  from f(1) obtain m' n' 
    where f_is_preorder_functor: "f : cat_ordinal m' ≤C.PEO⇘α⇙ cat_ordinal n'" 
      and "m' ∈∘ A"
      and "n' ∈∘ A"
    by (elim cat_simplicial_ArrE)  
  then have 
    "cat_simplicial α A⦇Dom⦈⦇f⦈ = cat_ordinal m'"
    "cat_simplicial α A⦇Cod⦈⦇f⦈ = cat_ordinal n'"
    by (cs_concl cs_shallow cs_simp: cat_simplicial_cs_simps)+
  with f(2,3) have 
    "cat_ordinal m' = cat_ordinal m" "cat_ordinal n' = cat_ordinal n"
    by auto
  with f(2,3) cat_ordinal_inj have [simp]: "m' = m" "n' = n" by auto
  from f_is_preorder_functor show ?thesis by simp
qed

lemma cat_simplicial_is_arrE[elim]: 
  assumes "f : a ↦⇘cat_simplicial α A⇙ b"
  obtains m n where "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
    and "m ∈∘ A" 
    and "n ∈∘ A"
    and "a = cat_ordinal m"
    and "b = cat_ordinal n"
proof-
  note f = is_arrD[OF assms(1)]
  from f(1) obtain m n
    where f_is_preorder_functor: "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n" 
      and m: "m ∈∘ A"
      and n: "n ∈∘ A"
    by (elim cat_simplicial_ArrE)  
  then have 
    "cat_simplicial α A⦇Dom⦈⦇f⦈ = cat_ordinal m"
    "cat_simplicial α A⦇Cod⦈⦇f⦈ = cat_ordinal n"
    by (cs_concl cs_shallow cs_simp: cat_simplicial_cs_simps)+
  with f(2,3) have "cat_ordinal m = a" "cat_ordinal n = b"
    by auto
  with f_is_preorder_functor m n that show ?thesis by auto
qed


subsubsection‹Composition›

mk_VLambda cat_simplicial_components(5)
  |vsv cat_simplicial_Comp_vsv[cat_simplicial_cs_intros]|
  |vdomain cat_simplicial_Comp_vdomain[cat_simplicial_cs_simps]|

lemma cat_simplicial_Comp_app[cat_simplicial_cs_simps]:
  assumes "g : cat_ordinal n ↦⇘cat_simplicial α A⇙ cat_ordinal p"
    and "f : cat_ordinal m ↦⇘cat_simplicial α A⇙ cat_ordinal n"
    and "m ∈∘ A" 
    and "n ∈∘ A" 
    and "p ∈∘ A"
  shows "g ∘A⇘cat_simplicial α A⇙ f = g ∘CF f"
proof- 
  note g = cat_simplicial_is_arrD[OF assms(1,4,5)]
  note f = cat_simplicial_is_arrD[OF assms(2,3,4)]
  interpret g: is_preorder_functor α ‹cat_ordinal n› ‹cat_ordinal p› g
    by (rule g)
  interpret f: is_preorder_functor α ‹cat_ordinal m› ‹cat_ordinal n› f
    by (rule f)
  have "[g, f]∘ ∈∘ composable_cat_simplicial α A"
    by 
      (
        intro composable_cat_simplicialI, rule g, rule f; 
        (intro assms refl)?
      )
  then show "g ∘A⇘cat_simplicial α A⇙ f = g ∘CF f"
    unfolding cat_simplicial_components by (simp add: nat_omega_simps)
qed


subsubsection‹Identity›

context
  fixes α A :: V
begin

mk_VLambda cat_simplicial_components(6)[where α=α and A=A]
  |vsv cat_simplicial_CId_vsv[cat_simplicial_cs_intros]|
  |vdomain 
    cat_simplicial_CId_vdomain'[
      folded cat_simplicial_components(1)[where α=α and A=A]
    ]
  |
  |app cat_simplicial_CId_app'[
    folded cat_simplicial_components(1)[where α=α and A=A]
    ]
  |

lemmas cat_simplicial_CId_vdomain[cat_simplicial_cs_simps] = 
  cat_simplicial_CId_vdomain'
lemmas cat_simplicial_CId_app[cat_simplicial_cs_simps] = 
  cat_simplicial_CId_app'

end


subsubsection‹Simplicial category is a category›

lemma (in 𝒵) category_simplicial:
  assumes "Ord A" and "A ⊆∘ α"
  shows "category α (cat_simplicial α A)"
proof-

  show ?thesis 
  proof(intro categoryI')

    show "vfsequence (cat_simplicial α A)" unfolding cat_simplicial_def by simp
    show "vcard (cat_simplicial α A) = 6ℕ"
      unfolding cat_simplicial_def by (simp add: nat_omega_simps)

    show "ℛ∘ (cat_simplicial α A⦇Dom⦈) ⊆∘ cat_simplicial α A⦇Obj⦈"
    proof(rule vsv.vsv_vrange_vsubset, unfold cat_simplicial_cs_simps)
      fix f assume "f ∈∘ cat_simplicial α A⦇Arr⦈"
      then obtain m n 
        where "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n" 
          and "m ∈∘ A" 
          and "n ∈∘ A"
        by (elim cat_simplicial_ArrE)
      then show "cat_simplicial α A⦇Dom⦈⦇f⦈ ∈∘ cat_simplicial α A⦇Obj⦈"
        by (auto simp: cat_simplicial_Dom_app' intro: cat_simplicial_ObjI)
    qed (auto simp: cat_simplicial_components)

    show "ℛ∘ (cat_simplicial α A⦇Cod⦈) ⊆∘ cat_simplicial α A⦇Obj⦈"
    proof(rule vsv.vsv_vrange_vsubset, unfold cat_simplicial_cs_simps)
      fix f assume "f ∈∘ cat_simplicial α A⦇Arr⦈"
      then obtain m n 
        where "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n" 
          and "m ∈∘ A" 
          and "n ∈∘ A"
        by (elim cat_simplicial_ArrE)
      then show "cat_simplicial α A⦇Cod⦈⦇f⦈ ∈∘ cat_simplicial α A⦇Obj⦈"
        by (auto simp: cat_simplicial_Cod_app' intro: cat_simplicial_ObjI)
    qed (auto simp: cat_simplicial_components)

    show "(gf ∈∘ 𝒟∘ (cat_simplicial α A⦇Comp⦈)) ⟷
      (
        ∃g f b c a.
          gf = [g, f]∘ ∧
          g : b ↦⇘cat_simplicial α A⇙ c ∧
          f : a ↦⇘cat_simplicial α A⇙ b
      )"
      for gf
    proof(intro iffI; (elim exE conjE)?)
      assume "gf ∈∘ 𝒟∘ (cat_simplicial α A⦇Comp⦈)"
      then have "gf ∈∘ composable_cat_simplicial α A"
        unfolding cat_simplicial_components by simp
      then obtain g f m n p 
        where gf_def: "gf = [g, f]∘" 
          and g: "g : cat_ordinal n ≤C.PEO⇘α⇙ cat_ordinal p"
          and f: "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
          and m: "m ∈∘ A" 
          and n: "n ∈∘ A"
          and p: "p ∈∘ A"
        by auto
      show "∃g f b c a.
        gf = [g, f]∘ ∧
        g : b ↦⇘cat_simplicial α A⇙ c ∧
        f : a ↦⇘cat_simplicial α A⇙ b"
      proof(intro exI conjI)
        from g n p show "g : cat_ordinal n ↦⇘cat_simplicial α A⇙ cat_ordinal p"
          by (intro cat_simplicial_is_arrI) simp_all
        from f m n show "f : cat_ordinal m ↦⇘cat_simplicial α A⇙ cat_ordinal n"
          by (intro cat_simplicial_is_arrI) simp_all
      qed (simp add: gf_def)
    next
      fix g f a b c assume prems:
        "gf = [g, f]∘" 
        "g : b ↦⇘cat_simplicial α A⇙ c"
        "f : a ↦⇘cat_simplicial α A⇙ b"
      from prems(2) obtain n p 
        where g: "g : cat_ordinal n ≤C.PEO⇘α⇙ cat_ordinal p"
          and n: "n ∈∘ A" 
          and p: "p ∈∘ A"
          and b_def: "b = cat_ordinal n" 
          and "c = cat_ordinal p"
        by auto
      from prems(3) obtain m n'
        where f: "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n'"
          and m: "m ∈∘ A" 
          and n': "n' ∈∘ A"
          and a_def: "a = cat_ordinal m" 
          and b_def': "b = cat_ordinal n'"
        by auto
      from b_def b_def' have n'n: "n' = n" by (auto simp: cat_ordinal_inj)
      show "gf ∈∘ 𝒟∘ (cat_simplicial α A⦇Comp⦈)"
        unfolding prems(1) cat_simplicial_Comp_vdomain
        by (intro composable_cat_simplicialI, rule g, rule f[unfolded n'n])
          (simp_all add:  m n p)
    qed
    show "g ∘A⇘cat_simplicial α A⇙ f : a ↦⇘cat_simplicial α A⇙ c"
      if "g : b ↦⇘cat_simplicial α A⇙ c" and "f : a ↦⇘cat_simplicial α A⇙ b"
      for b c g a f
      using that  
      by (elim cat_simplicial_is_arrE; simp only: cat_ordinal_inj)
        (
          cs_concl cs_shallow
            cs_simp: cat_simplicial_cs_simps 
            cs_intro: cat_order_cs_intros cat_simplicial_cs_intros
        )

    show "h ∘A⇘cat_simplicial α A⇙ g ∘A⇘cat_simplicial α A⇙ f =
      h ∘A⇘cat_simplicial α A⇙ (g ∘A⇘cat_simplicial α A⇙ f)"
      if "h : c ↦⇘cat_simplicial α A⇙ d"
        and "g : b ↦⇘cat_simplicial α A⇙ c"
        and "f : a ↦⇘cat_simplicial α A⇙ b"
      for c d h b g a f
      using that
      apply(elim cat_simplicial_is_arrE; simp only:)
      subgoal for m n m' n' m'' n'' (*FIXME: investigate comp_no_flatten*)
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_simplicial_cs_simps 
              cs_intro: cat_order_cs_intros cat_simplicial_cs_intros
          )+
      done

    show "cat_simplicial α A⦇CId⦈⦇a⦈ : a ↦⇘cat_simplicial α A⇙ a"
      if "a ∈∘ cat_simplicial α A⦇Obj⦈" for a
      using that
    proof(elim cat_simplicial_ObjE; simp only:)
      fix m assume prems: "m ∈∘ A" "cat_ordinal m ∈∘ cat_simplicial α A⦇Obj⦈"
      moreover from prems(1) assms(1) have "Ord m" by auto
      moreover from prems assms have "m ⊆∘ α" 
        by (meson Ord_trans vsubsetI rev_vsubsetD)
      ultimately show "cat_simplicial α A⦇CId⦈⦇cat_ordinal m⦈ :
        cat_ordinal m ↦⇘cat_simplicial α A⇙ cat_ordinal m"
        by 
          (
            cs_concl 
              cs_simp: cat_simplicial_cs_simps 
              cs_intro: 
                cat_ordinal_cs_intros 
                cat_order_cs_intros
                cat_simplicial_cs_intros
          )
    qed
    show "cat_simplicial α A⦇CId⦈⦇b⦈ ∘A⇘cat_simplicial α A⇙ f = f"
      if "f : a ↦⇘cat_simplicial α A⇙ b" for a b f
      using that
      by (elim cat_simplicial_is_arrE; simp only:)
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_simplicial_cs_simps
            cs_intro: cat_order_cs_intros cat_simplicial_cs_intros
        )
    show "f ∘A⇘cat_simplicial α A⇙ cat_simplicial α A⦇CId⦈⦇b⦈ = f"
      if "f : b ↦⇘cat_simplicial α A⇙ c" for b c f
      using that
      by (elim cat_simplicial_is_arrE; simp only:)
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_simplicial_cs_simps
            cs_intro: cat_order_cs_intros cat_simplicial_cs_intros
        )
    show "cat_simplicial α A⦇Obj⦈ ⊆∘ Vset α"
    proof(intro vsubsetI, elim cat_simplicial_ObjE; simp only:)
      fix m assume prems: "m ∈∘ A"
      then have "Ord m" using assms(1) by auto
      moreover from prems have "m ∈∘ α" using assms(2) by auto
      ultimately interpret m: cat_tiny_linear_order α ‹cat_ordinal m›
        by (intro cat_tiny_linear_order_cat_ordinal)
      show "cat_ordinal m ∈∘ Vset α" by (rule m.tiny_cat_in_Vset)
    qed

    show "(⋃∘a∈∘A'. ⋃∘b∈∘B'. Hom (cat_simplicial α A) a b) ∈∘ Vset α"
      if "A' ⊆∘ cat_simplicial α A⦇Obj⦈"
        and "B' ⊆∘ cat_simplicial α A⦇Obj⦈"
        and "A' ∈∘ Vset α"
        and "B' ∈∘ Vset α"
      for A' B' 
    proof-
      define Q where "Q i =
        (
          if i = 0 ⇒ VPow ((⋃∘a'∈∘A'. a'⦇Obj⦈) ×∘ (⋃∘b'∈∘B'. b'⦇Obj⦈))
           | i = 1ℕ ⇒ VPow 
              (((⋃∘a'∈∘A'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘A'. a'⦇Obj⦈)) ×∘
              ((⋃∘a'∈∘B'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘B'. a'⦇Obj⦈)))
           | i = 2ℕ ⇒ A'
           | i = 3ℕ ⇒ B'
           | otherwise ⇒ 0
        )"
        for i
      let ?Q = 
        ‹{
          [fo, fa, a, b]∘ | fo fa a b.
            fo ⊆∘ ((⋃∘a'∈∘A'. a'⦇Obj⦈) ×∘ (⋃∘b'∈∘B'. b'⦇Obj⦈)) ∧
            fa ⊆∘
              ((⋃∘a'∈∘A'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘A'. a'⦇Obj⦈)) ×∘
              ((⋃∘a'∈∘B'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘B'. a'⦇Obj⦈)) ∧
            a ∈∘ A' ∧
            b ∈∘ B'
         }›

      have QQ: "?Q ⊆ elts (∏∘i∈∘set {0, 1ℕ, 2ℕ, 3ℕ}. Q i)"
      proof(intro subsetI, unfold mem_Collect_eq, elim exE conjE)
        fix x fo fa a b assume prems: 
          "x = [fo, fa, a, b]∘"
          "fo ⊆∘ ((⋃∘a'∈∘A'. a'⦇Obj⦈) ×∘ (⋃∘b'∈∘B'. b'⦇Obj⦈))"
          "fa ⊆∘
            ((⋃∘a'∈∘A'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘A'. a'⦇Obj⦈)) ×∘
            ((⋃∘a'∈∘B'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘B'. a'⦇Obj⦈))"
          "a ∈∘ A'"
          "b ∈∘ B'"
        show "x ∈∘ (∏∘i∈∘set {0, 1ℕ, 2ℕ, 3ℕ}. Q i)"
        proof(intro vproductI, unfold Ball_def; (intro allI impI)?)
          show "𝒟∘ x = set {[]∘, 1ℕ, 2ℕ, 3ℕ}"
            unfolding prems(1) by (force simp: nat_omega_simps)
          fix i assume "i ∈∘ set {0, 1ℕ, 2ℕ, 3ℕ}"
          then consider ‹i = 0› | ‹i = 1ℕ› | ‹i = 2ℕ› | ‹i = 3ℕ› by auto
          then show "x⦇i⦈ ∈∘ Q i" 
            by cases (auto simp: Q_def prems nat_omega_simps)
        qed (auto simp: prems)
      qed
      then have small_Q[simp]: "small ?Q" by (intro down)

      have "(⋃∘a∈∘A'. ⋃∘b∈∘B'. Hom (cat_simplicial α A) a b) ⊆∘ set ?Q" 
      proof(intro vsubsetI in_small_setI small_Q)
        fix f assume "f ∈∘ (⋃∘a∈∘A'. ⋃∘b∈∘B'. Hom (cat_simplicial α A) a b)"
        then obtain a b 
          where a: "a ∈∘ A'" 
            and b: "b ∈∘ B'" 
            and "f : a ↦⇘cat_simplicial α A⇙ b"
          by auto
        then obtain m n 
          where f: "f : cat_ordinal m ≤C.PEO⇘α⇙ cat_ordinal n"
            and m: "m ∈∘ A" 
            and n: "n ∈∘ A" 
            and a_def: "a = cat_ordinal m" 
            and b_def: "b = cat_ordinal n"
          by auto
        interpret f: is_preorder_functor α ‹cat_ordinal m› ‹cat_ordinal n› f 
          by (rule f)
        show "f ∈ ?Q"
        proof(unfold mem_Collect_eq, intro exI conjI)
          show "f⦇ObjMap⦈ ⊆∘ (⋃∘a'∈∘A'. a'⦇Obj⦈) ×∘ (⋃∘b'∈∘B'. b'⦇Obj⦈)"
          proof(intro vsubsetI)
            fix x assume prems: "x ∈∘ f⦇ObjMap⦈"
            obtain xl xr 
              where x_def: "x = ⟨xl, xr⟩" 
                and xl: "xl ∈∘ cat_ordinal m⦇Obj⦈" 
                and xr: "xr ∈∘ (ℛ∘ (f⦇ObjMap⦈))"
              by (elim f.ObjMap.vbrelation_vinE[OF prems, unfolded cat_cs_simps])
            show "x ∈∘ (⋃∘a'∈∘A'. a'⦇Obj⦈) ×∘ (⋃∘b'∈∘B'. b'⦇Obj⦈)"
              unfolding x_def
            proof(standard; (intro vifunionI))
              from xr f.cf_ObjMap_vrange show "xr ∈∘ cat_ordinal n⦇Obj⦈" by auto
            qed (use a b in ‹auto intro: xl simp: a_def b_def›)
          qed
          show "f⦇ArrMap⦈ ⊆∘
            ((⋃∘a'∈∘A'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘A'. a'⦇Obj⦈)) ×∘
            ((⋃∘a'∈∘B'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘B'. a'⦇Obj⦈))"
          proof(intro vsubsetI)
            fix x assume prems: "x ∈∘ f⦇ArrMap⦈"
            obtain xl xr 
              where x_def: "x = ⟨xl, xr⟩" 
                and xl: "xl ∈∘ cat_ordinal m⦇Arr⦈" 
                and xr: "xr ∈∘ (ℛ∘ (f⦇ArrMap⦈))"
              by (elim f.ArrMap.vbrelation_vinE[OF prems, unfolded cat_cs_simps])
            from xr vsubsetD have xr: "xr ∈∘ cat_ordinal n⦇Arr⦈"
              by (auto intro: f.cf_ArrMap_vrange)
            from xl obtain xll xlr where xl_def: "xl = [xll, xlr]∘" 
              and xll_m: "xll ∈∘ m" 
              and xlr_m: "xlr ∈∘ m" 
              and "xll ⊆∘ xlr" 
              unfolding ordinal_arrs_def cat_ordinal_components by clarsimp
            from xr obtain xrl xrr where xr_def: "xr = [xrl, xrr]∘" 
              and xrl_n: "xrl ∈∘ n"
              and xrr_n:"xrr ∈∘ n"
              and "xrl ⊆∘ xrr"
              unfolding ordinal_arrs_def cat_ordinal_components by clarsimp
            show "x ∈∘
              ((⋃∘a'∈∘A'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘A'. a'⦇Obj⦈)) ×∘
              ((⋃∘a'∈∘B'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘B'. a'⦇Obj⦈))"
              unfolding x_def
              by (standard; (intro vifunionI ftimesI1)?)
                (
                  use a b in ‹
                    auto
                      simp: xl_def xr_def a_def b_def cat_ordinal_components
                      intro: xrr_n xrl_n xlr_m xll_m
                    ›
                )
          qed 
        qed 
          (
            auto 
              simp: cat_cs_simps 
              intro: a[unfolded a_def] b[unfolded b_def] f.cf_def
          )
      qed
      moreover have "set ?Q ⊆∘ (∏∘i∈∘set {0, 1ℕ, 2ℕ, 3ℕ}. Q i)"
        by 
          (
            intro vsubset_if_subset, 
            unfold small_elts_of_set[OF small_Q], 
            intro QQ
          )
      moreover have "(∏∘i∈∘set {0, 1ℕ, 2ℕ, 3ℕ}. Q i) ∈∘ Vset α"
      proof(intro Limit_vproduct_in_VsetI)
        show "set {0, 1ℕ, 2ℕ, 3ℕ} ∈∘ Vset α"
          unfolding four[symmetric] by simp
        have "(⋃∘a'∈∘A'. a'⦇Obj⦈) ⊆∘ ⋃∘(⋃∘r∈∘A'. ℛ∘ r)"
        proof(intro vsubsetI)
          fix x assume "x ∈∘ (⋃∘a'∈∘A'. a'⦇Obj⦈)"
          then obtain a' where a': "a' ∈∘ A'" and x: "x ∈∘ a'⦇Obj⦈" by auto
          from a' that(1) have "a' ∈∘ cat_simplicial α A⦇Obj⦈" by auto
          then obtain m where a'_def: "a' = cat_ordinal m" and m: "m ∈∘ A"
            unfolding cat_simplicial_components by clarsimp
          show "x ∈∘ ⋃∘(⋃∘r∈∘A'. ℛ∘ r)"
          proof(rule VUnionI, rule vifunionI)
            from a'_def have "vsv a'" and "Obj ∈∘ 𝒟∘ a'"
              unfolding a'_def cat_ordinal_def Obj_def by auto
            then show "a'⦇Obj⦈ ∈∘ ℛ∘ a'" by auto
          qed (auto simp: x a')
        qed
        moreover have "(⋃∘r∈∘A'. ℛ∘ r) ∈∘ Vset α"
          by (intro Limit_VUnion_vrange_in_VsetI[OF Limit_α] that)
        ultimately have UA': "(⋃∘a'∈∘A'. a'⦇Obj⦈) ∈∘ Vset α" by blast
        have B': "(⋃∘b'∈∘B'. b'⦇Obj⦈) ⊆∘ ⋃∘(⋃∘r∈∘B'. ℛ∘ r)"
          (*FIXME: code duplication*)
        proof(intro vsubsetI)
          fix x assume "x ∈∘ (⋃∘b'∈∘B'. b'⦇Obj⦈)"
          then obtain b' where b': "b' ∈∘ B'" and x: "x ∈∘ b'⦇Obj⦈" by auto
          from b' that(2) have "b' ∈∘ cat_simplicial α A⦇Obj⦈" by auto
          then obtain m where b'_def: "b' = cat_ordinal m" and m: "m ∈∘ A"
            unfolding cat_simplicial_components by clarsimp
          show "x ∈∘ ⋃∘(⋃∘r∈∘B'. ℛ∘ r)"
          proof(rule VUnionI, rule vifunionI)
            from b'_def have "vsv b'" and "Obj ∈∘ 𝒟∘ b'"
              unfolding b'_def cat_ordinal_def Obj_def by auto
            then show "b'⦇Obj⦈ ∈∘ ℛ∘ b'" by auto
          qed (auto simp: x b')
        qed
        moreover have "(⋃∘r∈∘B'. ℛ∘ r) ∈∘ Vset α"
          by (intro Limit_VUnion_vrange_in_VsetI[OF Limit_α] that)
        ultimately have UB': "(⋃∘a'∈∘B'. a'⦇Obj⦈) ∈∘ Vset α" by blast
        have [simp]: 
          "VPow ((⋃∘a'∈∘A'. a'⦇Obj⦈) ×∘ (⋃∘b'∈∘B'. b'⦇Obj⦈)) ∈∘ Vset α"
          by (intro Limit_VPow_in_VsetI Limit_vtimes_in_VsetI UA' UB') auto
        have [simp]:
          "VPow
            (
              ((⋃∘a'∈∘A'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘A'. a'⦇Obj⦈)) ×∘
              ((⋃∘a'∈∘B'. a'⦇Obj⦈) ×∙ (⋃∘a'∈∘B'. a'⦇Obj⦈))
            ) ∈∘ Vset α"
          by 
            (
              intro 
                Limit_VPow_in_VsetI 
                Limit_vtimes_in_VsetI 
                Limit_ftimes_in_VsetI  
                UA' UB'
            )
            auto
        fix i assume "i ∈∘ set {0, 1ℕ, 2ℕ, 3ℕ}"
        then consider ‹i = 0› | ‹i = 1ℕ› | ‹i = 2ℕ› | ‹i = 3ℕ› by auto
        then show "Q i ∈∘ Vset α" 
          by cases (simp_all add: Q_def that nat_omega_simps)
      qed auto
      ultimately show ?thesis by (simp add: vsubset_in_VsetI)
    qed
  qed (auto simp: cat_simplicial_components)

qed

text‹\newpage›

end