Theory CZH_SMC_CAT
section‹‹CAT› as a semicategory\label{sec:smc_CAT}›
theory CZH_SMC_CAT
imports
CZH_DG_CAT
CZH_ECAT_Simple
begin
subsection‹Background›
text‹
The subsection presents the theory of the semicategories of ‹α›-categories.
It continues the development that was initiated in section
\ref{sec:dg_CAT}.
›
named_theorems smc_CAT_simps
named_theorems smc_CAT_intros
subsection‹Definition and elementary properties›
definition smc_CAT :: "V ⇒ V"
where "smc_CAT α =
[
set {ℭ. category α ℭ},
all_cfs α,
(λ𝔉∈⇩∘all_cfs α. 𝔉⦇HomDom⦈),
(λ𝔉∈⇩∘all_cfs α. 𝔉⦇HomCod⦈),
(λ𝔊𝔉∈⇩∘composable_arrs (dg_CAT α). 𝔊𝔉⦇0⦈ ∘⇩C⇩F 𝔊𝔉⦇1⇩ℕ⦈)
]⇩∘"
text‹Components.›
lemma smc_CAT_components:
shows "smc_CAT α⦇Obj⦈ = set {ℭ. category α ℭ}"
and "smc_CAT α⦇Arr⦈ = all_cfs α"
and "smc_CAT α⦇Dom⦈ = (λ𝔉∈⇩∘all_cfs α. 𝔉⦇HomDom⦈)"
and "smc_CAT α⦇Cod⦈ = (λ𝔉∈⇩∘all_cfs α. 𝔉⦇HomCod⦈)"
and "smc_CAT α⦇Comp⦈ = (λ𝔊𝔉∈⇩∘composable_arrs (dg_CAT α). 𝔊𝔉⦇0⦈ ∘⇩C⇩F 𝔊𝔉⦇1⇩ℕ⦈)"
unfolding smc_CAT_def dg_field_simps by (simp_all add: nat_omega_simps)
text‹Slicing.›
lemma smc_dg_CAT: "smc_dg (smc_CAT α) = dg_CAT α"
proof(rule vsv_eqI)
show "vsv (smc_dg (smc_CAT α))" unfolding smc_dg_def by auto
show "vsv (dg_CAT α)" unfolding dg_CAT_def by auto
have dom_lhs: "𝒟⇩∘ (smc_dg (smc_CAT α)) = 4⇩ℕ"
unfolding smc_dg_def by (simp add: nat_omega_simps)
have dom_rhs: "𝒟⇩∘ (dg_CAT α) = 4⇩ℕ"
unfolding dg_CAT_def by (simp add: nat_omega_simps)
show "𝒟⇩∘ (smc_dg (smc_CAT α)) = 𝒟⇩∘ (dg_CAT α)"
unfolding dom_lhs dom_rhs by simp
show "𝔄 ∈⇩∘ 𝒟⇩∘ (smc_dg (smc_CAT α)) ⟹ smc_dg (smc_CAT α)⦇𝔄⦈ = dg_CAT α⦇𝔄⦈"
for 𝔄
by
(
unfold dom_lhs,
elim_in_numeral,
unfold smc_dg_def dg_field_simps smc_CAT_def dg_CAT_def
)
(auto simp: nat_omega_simps)
qed
lemmas_with [folded smc_dg_CAT, unfolded slicing_simps]:
smc_CAT_ObjI = dg_CAT_ObjI
and smc_CAT_ObjD = dg_CAT_ObjD
and smc_CAT_ObjE = dg_CAT_ObjE
and smc_CAT_Obj_iff[smc_CAT_simps] = dg_CAT_Obj_iff
and smc_CAT_Dom_app[smc_CAT_simps] = dg_CAT_Dom_app
and smc_CAT_Cod_app[smc_CAT_simps] = dg_CAT_Cod_app
and smc_CAT_is_arrI = dg_CAT_is_arrI
and smc_CAT_is_arrD = dg_CAT_is_arrD
and smc_CAT_is_arrE = dg_CAT_is_arrE
and smc_CAT_is_arr_iff[smc_CAT_simps] = dg_CAT_is_arr_iff
subsection‹Composable arrows›
lemma smc_CAT_composable_arrs_dg_CAT:
"composable_arrs (dg_CAT α) = composable_arrs (smc_CAT α)"
unfolding composable_arrs_def smc_dg_CAT[symmetric] slicing_simps by auto
lemma smc_CAT_Comp:
"smc_CAT α⦇Comp⦈ = (λ𝔊𝔉∈⇩∘composable_arrs (smc_CAT α). 𝔊𝔉⦇0⦈ ∘⇩S⇩M⇩C⇩F 𝔊𝔉⦇1⇩ℕ⦈)"
unfolding smc_CAT_components smc_CAT_composable_arrs_dg_CAT ..
subsection‹Composition›
lemma smc_CAT_Comp_app[smc_CAT_simps]:
assumes "𝔊 : 𝔅 ↦⇘smc_CAT α⇙ ℭ" and "𝔉 : 𝔄 ↦⇘smc_CAT α⇙ 𝔅"
shows "𝔊 ∘⇩A⇘smc_CAT α⇙ 𝔉 = 𝔊 ∘⇩S⇩M⇩C⇩F 𝔉"
proof-
from assms have "[𝔊, 𝔉]⇩∘ ∈⇩∘ composable_arrs (smc_CAT α)"
by (auto simp: smc_cs_intros)
then show "𝔊 ∘⇩A⇘smc_CAT α⇙ 𝔉 = 𝔊 ∘⇩S⇩M⇩C⇩F 𝔉"
unfolding smc_CAT_Comp by (simp add: nat_omega_simps)
qed
lemma smc_CAT_Comp_vdomain: "𝒟⇩∘ (smc_CAT α⦇Comp⦈) = composable_arrs (smc_CAT α)"
unfolding smc_CAT_Comp by auto
lemma smc_CAT_Comp_vrange: "ℛ⇩∘ (smc_CAT α⦇Comp⦈) ⊆⇩∘ all_cfs α"
proof(rule vsubsetI)
fix ℌ assume "ℌ ∈⇩∘ ℛ⇩∘ (smc_CAT α⦇Comp⦈)"
then obtain 𝔊𝔉
where ℌ_def: "ℌ = smc_CAT α⦇Comp⦈⦇𝔊𝔉⦈"
and "𝔊𝔉 ∈⇩∘ 𝒟⇩∘ (smc_CAT α⦇Comp⦈)"
by (auto simp: smc_CAT_components intro: smc_cs_intros)
then obtain 𝔊 𝔉 𝔄 𝔅 ℭ
where "𝔊𝔉 = [𝔊, 𝔉]⇩∘"
and 𝔊: "𝔊 : 𝔅 ↦⇘smc_CAT α⇙ ℭ"
and 𝔉: "𝔉 : 𝔄 ↦⇘smc_CAT α⇙ 𝔅"
by (auto simp: smc_CAT_Comp_vdomain)
with ℌ_def have ℌ_def': "ℌ = 𝔊 ∘⇩A⇘smc_CAT α⇙ 𝔉" by simp
from 𝔊 𝔉 show "ℌ ∈⇩∘ all_cfs α"
unfolding ℌ_def' by (auto simp: smc_CAT_simps intro: cat_cs_intros)
qed
subsection‹‹CAT› is a category›
lemma (in 𝒵) tiny_semicategory_smc_CAT:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "tiny_semicategory β (smc_CAT α)"
proof(intro tiny_semicategoryI, unfold smc_CAT_is_arr_iff)
show "vfsequence (smc_CAT α)" unfolding smc_CAT_def by auto
show "vcard (smc_CAT α) = 5⇩ℕ"
unfolding smc_CAT_def by (simp add: nat_omega_simps)
show "(𝔊𝔉 ∈⇩∘ 𝒟⇩∘ (smc_CAT α⦇Comp⦈)) ⟷
(∃𝔊 𝔉 𝔅 ℭ 𝔄. 𝔊𝔉 = [𝔊, 𝔉]⇩∘ ∧ 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ ∧ 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅)"
for 𝔊𝔉
unfolding smc_CAT_Comp_vdomain
proof
show "𝔊𝔉 ∈⇩∘ composable_arrs (smc_CAT α) ⟹
∃𝔊 𝔉 𝔅 ℭ 𝔄. 𝔊𝔉 = [𝔊, 𝔉]⇩∘ ∧ 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ ∧ 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by (elim composable_arrsE) (auto simp: smc_CAT_is_arr_iff)
next
assume "∃𝔊 𝔉 𝔅 ℭ 𝔄. 𝔊𝔉 = [𝔊, 𝔉]⇩∘ ∧ 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ ∧ 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
with smc_CAT_is_arr_iff show "𝔊𝔉 ∈⇩∘ composable_arrs (smc_CAT α)"
unfolding smc_CAT_Comp_vdomain by (auto intro: smc_cs_intros)
qed
show "⟦ 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ; 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅 ⟧ ⟹
𝔊 ∘⇩A⇘smc_CAT α⇙ 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
for 𝔊 𝔅 ℭ 𝔉 𝔄
by (cs_concl cs_simp: smc_CAT_simps cs_intro: cat_cs_intros)
fix ℌ ℭ 𝔇 𝔊 𝔅 𝔉 𝔄
assume "ℌ : ℭ ↦↦⇩C⇘α⇙ 𝔇" "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
moreover then have "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" "ℌ ∘⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ 𝔇"
by (cs_concl cs_simp: smc_CAT_simps cs_intro: cat_cs_intros)+
ultimately show
"ℌ ∘⇩A⇘smc_CAT α⇙ 𝔊 ∘⇩A⇘smc_CAT α⇙ 𝔉 = ℌ ∘⇩A⇘smc_CAT α⇙ (𝔊 ∘⇩A⇘smc_CAT α⇙ 𝔉)"
by (simp add: smc_CAT_is_arr_iff smc_CAT_Comp_app cf_comp_assoc)
qed (auto simp: assms smc_dg_CAT tiny_category_dg_CAT smc_CAT_components)
subsection‹Initial object›
lemma (in 𝒵) smc_CAT_obj_initialI: "obj_initial (smc_CAT α) cat_0"
unfolding obj_initial_def
proof(intro obj_terminalI, unfold smc_op_simps smc_CAT_is_arr_iff smc_CAT_Obj_iff)
show "category α cat_0" by (intro category_cat_0)
fix 𝔄 assume "category α 𝔄"
then interpret category α 𝔄 .
show "∃!f. f : cat_0 ↦↦⇩C⇘α⇙ 𝔄"
proof
show cf_0: "cf_0 𝔄 : cat_0 ↦↦⇩C⇘α⇙ 𝔄"
by (simp add: cf_0_is_ft_functor category_axioms is_ft_functor.axioms(1))
fix 𝔉 assume prems: "𝔉 : cat_0 ↦↦⇩C⇘α⇙ 𝔄"
interpret 𝔉: is_functor α cat_0 𝔄 𝔉 using prems .
show "𝔉 = cf_0 𝔄"
proof(rule cf_eqI)
show "𝔉 : cat_0 ↦↦⇩C⇘α⇙ 𝔄" by (simp add: prems)
from cf_0 show "cf_0 𝔄 : cat_0 ↦↦⇩C⇘α⇙ 𝔄"
unfolding smc_CAT_is_arr_iff by simp
have "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 0" by (auto simp: cat_0_components cat_cs_simps)
then show "𝔉⦇ObjMap⦈ = cf_0 𝔄⦇ObjMap⦈"
using 𝔉.ObjMap.vbrelation_vintersection_vdomain
by (auto simp: cf_0_components)
have "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 0" by (auto simp: cat_0_components cat_cs_simps)
with 𝔉.ArrMap.vbrelation_vintersection_vdomain show
"𝔉⦇ArrMap⦈ = cf_0 𝔄⦇ArrMap⦈"
by (auto simp: cf_0_components)
qed (simp_all add: cf_0_components)
qed
qed
lemma (in 𝒵) smc_CAT_obj_initialD:
assumes "obj_initial (smc_CAT α) 𝔄"
shows "𝔄 = cat_0"
using assms unfolding obj_initial_def
proof(elim obj_terminalE, unfold smc_op_simps smc_CAT_is_arr_iff smc_CAT_Obj_iff)
assume prems:
"category α 𝔄"
"category α 𝔅 ⟹ ∃!𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
for 𝔅
from prems(2)[OF category_cat_0] obtain 𝔉 where 𝔉: "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ cat_0"
by meson
interpret 𝔉: is_functor α 𝔄 cat_0 𝔉 by (rule 𝔉)
have "ℛ⇩∘ (𝔉⦇ObjMap⦈) ⊆⇩∘ 0"
unfolding cat_0_components(1)[symmetric] by (simp add: 𝔉.cf_ObjMap_vrange)
then have "𝔉⦇ObjMap⦈ = 0" by (auto intro: 𝔉.ObjMap.vsv_vrange_vempty)
with 𝔉.cf_ObjMap_vdomain have Obj[simp]: "𝔄⦇Obj⦈ = 0" by auto
have "ℛ⇩∘ (𝔉⦇ArrMap⦈) ⊆⇩∘ 0"
unfolding cat_0_components(2)[symmetric] by (simp add: 𝔉.cf_ArrMap_vrange)
then have "𝔉⦇ArrMap⦈ = 0" by (auto intro: 𝔉.ArrMap.vsv_vrange_vempty)
with 𝔉.cf_ArrMap_vdomain have Arr[simp]: "𝔄⦇Arr⦈ = 0" by auto
from 𝔉.HomDom.Dom.vdomain_vrange_is_vempty have [simp]: "𝔄⦇Dom⦈ = 0"
by (fastforce simp: 𝔉.HomDom.cat_Dom_vempty_if_Arr_vempty)
from 𝔉.HomDom.Cod.vdomain_vrange_is_vempty have [simp]: "𝔄⦇Cod⦈ = 0"
by (fastforce simp: 𝔉.HomDom.cat_Cod_vempty_if_Arr_vempty)
from Arr have "𝔄⦇Arr⦈ ^⇩× 2⇩ℕ = 0" by (simp add: vcpower_of_vempty)
with 𝔉.HomDom.Comp.pnop_vdomain have "𝒟⇩∘ (𝔄⦇Comp⦈) = 0" by simp
with 𝔉.HomDom.Comp.vdomain_vrange_is_vempty have [simp]: "𝔄⦇Comp⦈ = 0"
by (auto intro: 𝔉.HomDom.Comp.vsv_vrange_vempty)
have "𝒟⇩∘ (𝔄⦇CId⦈) = 0"
by (simp add: 𝔉.HomDom.cat_CId_vdomain)
with 𝔉.HomDom.CId.vdomain_vrange_is_vempty 𝔉.HomDom.CId.vsv_vrange_vempty
have [simp]: "𝔄⦇CId⦈ = 0"
by simp
show "𝔄 = cat_0"
by (rule cat_eqI[of α])
(simp_all add: prems(1) cat_0_components category_cat_0)
qed
lemma (in 𝒵) smc_CAT_obj_initialE:
assumes "obj_initial (smc_CAT α) 𝔄"
obtains "𝔄 = cat_0"
using assms by (auto dest: smc_CAT_obj_initialD)
lemma (in 𝒵) smc_CAT_obj_initial_iff[smc_CAT_simps]:
"obj_initial (smc_CAT α) 𝔄 ⟷ 𝔄 = cat_0"
using smc_CAT_obj_initialI smc_CAT_obj_initialD by auto
subsection‹Terminal object›
lemma (in 𝒵) smc_CAT_obj_terminalI:
assumes "a ∈⇩∘ Vset α" and "f ∈⇩∘ Vset α"
shows "obj_terminal (smc_CAT α) (cat_1 a f)"
proof(intro obj_terminalI, unfold smc_op_simps smc_CAT_is_arr_iff smc_CAT_Obj_iff)
fix 𝔄 assume prems: "category α 𝔄"
then interpret category α 𝔄 .
show "∃!𝔉'. 𝔉' : 𝔄 ↦↦⇩C⇘α⇙ cat_1 a f"
proof
show cf_1: "cf_const 𝔄 (cat_1 a f) a : 𝔄 ↦↦⇩C⇘α⇙ cat_1 a f"
by (rule cf_const_is_functor)
(auto simp: assms prems category_cat_1 cat_1_components)
fix 𝔉' assume "𝔉' : 𝔄 ↦↦⇩C⇘α⇙ cat_1 a f"
then interpret 𝔉': is_functor α 𝔄 ‹cat_1 a f› 𝔉' .
show "𝔉' = cf_const 𝔄 (cat_1 a f) a"
proof(rule cf_eqI, unfold dghm_const_components)
from cf_1 show "cf_const 𝔄 (cat_1 a f) a : 𝔄 ↦↦⇩C⇘α⇙ cat_1 a f" by simp
show "𝔉'⦇ObjMap⦈ = vconst_on (𝔄⦇Obj⦈) a"
proof(cases‹𝔄⦇Obj⦈ = 0›)
case True
with 𝔉'.ObjMap.vbrelation_vintersection_vdomain have "𝔉'⦇ObjMap⦈ = 0"
by (auto simp: cat_cs_simps)
with True show ?thesis by simp
next
case False
then have "𝒟⇩∘ (𝔉'⦇ObjMap⦈) ≠ 0" by (auto simp: cat_cs_simps)
then have "ℛ⇩∘ (𝔉'⦇ObjMap⦈) ≠ 0"
by (simp add: 𝔉'.ObjMap.vsv_vdomain_vempty_vrange_vempty)
moreover from 𝔉'.cf_ObjMap_vrange have "ℛ⇩∘ (𝔉'⦇ObjMap⦈) ⊆⇩∘ set {a}"
by (simp add: cat_1_components)
ultimately have "ℛ⇩∘ (𝔉'⦇ObjMap⦈) = set {a}" by auto
then show ?thesis
by (intro vsv.vsv_is_vconst_onI) (auto simp: cat_cs_simps)
qed
show "𝔉'⦇ArrMap⦈ = vconst_on (𝔄⦇Arr⦈) (cat_1 a f⦇CId⦈⦇a⦈)"
proof(cases‹𝔄⦇Arr⦈ = 0›)
case True
with
𝔉'.ArrMap.vdomain_vrange_is_vempty
vsv.vsv_vrange_vempty[OF 𝔉'.cf_ArrMap_vsv]
have "𝔉'⦇ArrMap⦈ = 0"
by (auto simp: cat_cs_simps)
with True show ?thesis by simp
next
case False
then have "𝒟⇩∘ (𝔉'⦇ArrMap⦈) ≠ 0" by (auto simp: cat_cs_simps)
then have "ℛ⇩∘ (𝔉'⦇ArrMap⦈) ≠ 0"
by (simp add: 𝔉'.ArrMap.vsv_vdomain_vempty_vrange_vempty)
moreover from 𝔉'.cf_ArrMap_vrange have "ℛ⇩∘ (𝔉'⦇ArrMap⦈) ⊆⇩∘ set {f}"
by (simp add: cat_1_components)
ultimately have "ℛ⇩∘ (𝔉'⦇ArrMap⦈) = set {f}" by auto
then show ?thesis
by
(
cs_concl cs_shallow
cs_simp: V_cs_simps cat_cs_simps cat_1_components
cs_intro: V_cs_intros vsv.vsv_is_vconst_onI
)+
qed
qed (auto intro: cat_cs_intros)
qed
qed (simp add: assms category_cat_1)
lemma (in 𝒵) smc_CAT_obj_terminalE:
assumes "obj_terminal (smc_CAT α) 𝔅"
obtains a f where "a ∈⇩∘ Vset α" and "f ∈⇩∘ Vset α" and "𝔅 = cat_1 a f"
using assms
proof(elim obj_terminalE, unfold cat_op_simps smc_CAT_is_arr_iff smc_CAT_Obj_iff)
assume prems: "category α 𝔅" "category α 𝔄 ⟹ ∃!𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" for 𝔄
interpret 𝔅: category α 𝔅 by (rule prems(1))
obtain a where 𝔅_Obj: "𝔅⦇Obj⦈ = set {a}" and a: "a ∈⇩∘ Vset α"
proof-
have cat_1: "category α (cat_1 0 0)" by (rule category_cat_1) auto
from prems(2)[OF cat_1] obtain 𝔉
where 𝔉: "𝔉 : cat_1 0 0 ↦↦⇩C⇘α⇙ 𝔅"
and 𝔊𝔉: "𝔊 : cat_1 0 0 ↦↦⇩C⇘α⇙ 𝔅 ⟹ 𝔊 = 𝔉" for 𝔊
by fastforce
interpret 𝔉: is_functor α ‹cat_1 0 0› 𝔅 𝔉 by (rule 𝔉)
have "𝒟⇩∘ (𝔉⦇ObjMap⦈) = set {0}" by (simp add: cat_1_components cat_cs_simps)
then obtain a where vrange_𝔉[simp]: "ℛ⇩∘ (𝔉⦇ObjMap⦈) = set {a}"
by (auto intro: 𝔉.ObjMap.vsv_vdomain_vsingleton_vrange_vsingleton)
with 𝔅.cat_Obj_vsubset_Vset 𝔉.cf_ObjMap_vrange have [simp]: "a ∈⇩∘ Vset α"
by auto
from 𝔉.cf_ObjMap_vrange have "set {a} ⊆⇩∘ 𝔅⦇Obj⦈" by simp
moreover have "𝔅⦇Obj⦈ ⊆⇩∘ set {a}"
proof(rule ccontr)
assume "¬𝔅⦇Obj⦈ ⊆⇩∘ set {a}"
then obtain b where ba: "b ≠ a" and b: "b ∈⇩∘ 𝔅⦇Obj⦈" by force
have "cf_const (cat_1 0 0) 𝔅 b : cat_1 0 0 ↦↦⇩C⇘α⇙ 𝔅"
by (rule cf_const_is_functor)
(simp_all add: 𝔅.category_axioms category_cat_1 b)
then have 𝔊_def: "cf_const (cat_1 0 0) 𝔅 b = 𝔉" by (rule 𝔊𝔉)
have "ℛ⇩∘ (cf_const (cat_1 0 0) 𝔅 b⦇ObjMap⦈) = set {b}"
unfolding dghm_const_components cat_1_components by simp
with vrange_𝔉 ba show False unfolding 𝔊_def by simp
qed
ultimately have "𝔅⦇Obj⦈ = set {a}" by simp
with that show ?thesis by simp
qed
have 𝔅_Arr: "𝔅⦇Arr⦈ = set {𝔅⦇CId⦈⦇a⦈}"
proof(rule vsubset_antisym)
from 𝔅_Obj show "set {𝔅⦇CId⦈⦇a⦈} ⊆⇩∘ 𝔅⦇Arr⦈"
by (blast intro: 𝔅.cat_is_arrD(1) cat_cs_intros)
show "𝔅⦇Arr⦈ ⊆⇩∘ set {𝔅⦇CId⦈⦇a⦈}"
proof(intro vsubsetI)
fix f assume "f ∈⇩∘ 𝔅⦇Arr⦈"
with 𝔅_Obj have f: "f : a ↦⇘𝔅⇙ a"
by (metis 𝔅.cat_is_arrD(2,3) is_arrI vsingleton_iff)
from f have "cf_const 𝔅 𝔅 a : 𝔅 ↦↦⇩C⇘α⇙ 𝔅"
by (intro cf_const_is_functor) (auto simp: 𝔅.category_axioms)
moreover from f have "cf_id 𝔅 : 𝔅 ↦↦⇩C⇘α⇙ 𝔅"
by (intro category.cat_cf_id_is_functor)
(auto simp: 𝔅.category_axioms)
ultimately have "cf_const 𝔅 𝔅 a = cf_id 𝔅"
by (metis prems(2) 𝔅.category_axioms)
moreover from f have "cf_const 𝔅 𝔅 a⦇ArrMap⦈⦇f⦈ = 𝔅⦇CId⦈⦇a⦈"
by (simp add: ‹f ∈⇩∘ 𝔅⦇Arr⦈› dghm_const_ArrMap_app)
moreover from f have "cf_id 𝔅⦇ArrMap⦈⦇f⦈ = f"
unfolding dghm_id_components by (simp add: cat_cs_intros)
ultimately show "f ∈⇩∘ set {𝔅⦇CId⦈⦇a⦈}" by simp
qed
qed
have "𝔅 = cat_1 a (𝔅⦇CId⦈⦇a⦈)"
proof(rule cat_eqI[of α], unfold cat_1_components)
from 𝔅.cat_Arr_vsubset_Vset 𝔅_Arr show "category α (cat_1 a (𝔅⦇CId⦈⦇a⦈))"
by (intro category_cat_1) (auto simp: a)
show "𝔅⦇Arr⦈ = set {𝔅⦇CId⦈⦇a⦈}" by (simp add: 𝔅_Arr)
then have "𝒟⇩∘ (𝔅⦇Dom⦈) = set {𝔅⦇CId⦈⦇a⦈}"
by (simp add: cat_cs_simps cat_cs_intros)
moreover have "ℛ⇩∘ (𝔅⦇Dom⦈) = set {a}"
using 𝔅.cat_Dom_vrange 𝔅.cat_CId_is_arr 𝔅.cat_Dom_vdomain
by (auto simp: 𝔅_Obj elim: 𝔅.Dom.vbrelation_vinE)
ultimately show "𝔅⦇Dom⦈ = set {⟨𝔅⦇CId⦈⦇a⦈, a⟩}"
using 𝔅.Dom.vsv_vdomain_vrange_vsingleton by simp
have "𝒟⇩∘ (𝔅⦇Cod⦈) = set {𝔅⦇CId⦈⦇a⦈}"
by (simp add: 𝔅_Arr cat_cs_simps)
moreover have "ℛ⇩∘ (𝔅⦇Cod⦈) = set {a}"
using 𝔅.cat_Cod_vrange 𝔅.cat_CId_is_arr 𝔅.cat_Cod_vdomain
by (auto simp: 𝔅_Obj elim: 𝔅.Cod.vbrelation_vinE)
ultimately show "𝔅⦇Cod⦈ = set {⟨𝔅⦇CId⦈⦇a⦈, a⟩}"
by (auto intro: 𝔅.Cod.vsv_vdomain_vrange_vsingleton)
show "𝔅⦇Comp⦈ = set {⟨[𝔅⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇a⦈]⇩∘, 𝔅⦇CId⦈⦇a⦈⟩}"
proof(rule vsv_eqI)
show dom:
"𝒟⇩∘ (𝔅⦇Comp⦈) = 𝒟⇩∘ (set {⟨[𝔅⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇a⦈]⇩∘, 𝔅⦇CId⦈⦇a⦈⟩})"
unfolding vdomain_vsingleton
proof(rule vsubset_antisym)
show "𝒟⇩∘ (𝔅⦇Comp⦈) ⊆⇩∘ set {[𝔅⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇a⦈]⇩∘}"
by (intro vsubsetI)
(metis 𝔅.cat_Comp_vdomain 𝔅_Arr vsingleton_iff 𝔅.cat_is_arrD(1))
show "set {[𝔅⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇a⦈]⇩∘} ⊆⇩∘ 𝒟⇩∘ (𝔅⦇Comp⦈)"
by
(
metis
𝔅_Obj vsingleton_iff
𝔅.cat_CId_is_arr
𝔅.cat_Comp_vdomainI
vsubset_vsingleton_left
)
qed
have "𝔅⦇CId⦈⦇a⦈ ∘⇩A⇘𝔅⇙ 𝔅⦇CId⦈⦇a⦈ = 𝔅⦇CId⦈⦇a⦈"
by (metis 𝔅_Obj 𝔅.cat_CId_is_arr 𝔅.cat_CId_left_left vsingletonI)
then show "a' ∈⇩∘ 𝒟⇩∘ (𝔅⦇Comp⦈) ⟹
𝔅⦇Comp⦈⦇a'⦈ = set {⟨[𝔅⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇a⦈]⇩∘, 𝔅⦇CId⦈⦇a⦈⟩}⦇a'⦈"
for a'
unfolding dom by simp
qed (auto simp: 𝔅_Obj 𝔅_Arr)
have "𝒟⇩∘ (𝔅⦇CId⦈) = set {a}" by (simp add: 𝔅_Obj 𝔅.cat_CId_vdomain)
moreover then have "ℛ⇩∘ (𝔅⦇CId⦈) = set {𝔅⦇CId⦈⦇a⦈}"
by
(
metis
𝔅.CId.vdomain_atE
𝔅.CId.vsv_vdomain_vsingleton_vrange_vsingleton
vsingleton_iff
)
ultimately show "𝔅⦇CId⦈ = set {⟨a, 𝔅⦇CId⦈⦇a⦈⟩}"
by (blast intro: 𝔅.CId.vsv_vdomain_vrange_vsingleton)
qed (auto simp: 𝔅_Obj cat_cs_intros)
with a that 𝔅.cat_Arr_vsubset_Vset 𝔅_Arr show ?thesis by auto
qed
text‹\newpage›
end