# 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⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal p ∧
f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal p ∧
f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal p"
"f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal p"
and "f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal p"
and "f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal p"
"f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal n ∧ m ∈⇩∘ A ∧ n ∈⇩∘ A
},
(
λf∈⇩∘ set
{
f. ∃m n.
f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal n ∧ m ∈⇩∘ A ∧ n ∈⇩∘ A
}. f⦇HomDom⦈
),
(
λf∈⇩∘ set
{
f. ∃m n.
f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal n ∧ m ∈⇩∘ A ∧ n ∈⇩∘ A
}. f⦇HomCod⦈
),
(λgf∈⇩∘composable_cat_simplicial α A. gf⦇0⦈ ∘⇩C⇩F 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⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal n ∧ m ∈⇩∘ A ∧ n ∈⇩∘ A}"
and "cat_simplicial α A⦇Dom⦈ =
(
λf∈⇩∘set
{
f. ∃m n.
f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal n ∧ m ∈⇩∘ A ∧ n ∈⇩∘ A
}. f⦇HomDom⦈
)"
and "cat_simplicial α A⦇Cod⦈ =
(
λf∈⇩∘set
{
f. ∃m n.
f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal n ∧ m ∈⇩∘ A ∧ n ∈⇩∘ A
}. f⦇HomCod⦈
)"
and "cat_simplicial α A⦇Comp⦈ =
(λgf∈⇩∘composable_cat_simplicial α A. gf⦇0⦈ ∘⇩C⇩F 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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 ∘⇩C⇩F 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 ∘⇩C⇩F 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ cat_ordinal p"
and f: "f : cat_ordinal m ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ 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
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⇩.⇩P⇩E⇩O⇘α⇙ 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⇩.⇩P⇩E⇩O⇘α⇙ 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])
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⇩.⇩P⇩E⇩O⇘α⇙ 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```