# Theory CZH_DG_FUNCT

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹FUNCT› and ‹Funct› as digraphs\label{sec:dg_FUNCT}›
theory CZH_DG_FUNCT
imports
CZH_ECAT_Small_NTCF
CZH_Foundations.CZH_DG_Subdigraph
begin

subsection‹Background›

text‹
A general reference for this section is Chapter II-4 in
\<^cite>‹"mac_lane_categories_2010"›.
›

named_theorems dg_FUNCT_cs_simps
named_theorems dg_FUNCT_cs_intros
named_theorems cat_map_cs_simps
named_theorems cat_map_cs_intros
named_theorems cat_map_extra_cs_simps

subsection‹Functor map›

subsubsection‹Definition and elementary properties›

definition cf_map :: "V ⇒ V"
where "cf_map 𝔉 = [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈]⇩∘"

abbreviation cf_maps :: "V ⇒ V ⇒ V ⇒ V"
where "cf_maps α 𝔄 𝔅 ≡ set {cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"

abbreviation tm_cf_maps :: "V ⇒ V ⇒ V ⇒ V"
where "tm_cf_maps α 𝔄 𝔅 ≡ set {cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅}"

lemma tm_cf_maps_subset_cf_maps:
"{cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅} ⊆ {cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
by auto

text‹Components.›

lemma cf_map_components[cat_map_cs_simps]:
shows "cf_map 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and "cf_map 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
unfolding cf_map_def dghm_field_simps by (simp_all add: nat_omega_simps)

text‹Sequence characterization.›

lemma dg_FUNCT_Obj_components:
shows "[FOM, FAM]⇩∘⦇ObjMap⦈ = FOM"
and "[FOM, FAM]⇩∘⦇ArrMap⦈ = FAM"
unfolding dghm_field_simps by (simp_all add: nat_omega_simps)

lemma cf_map_vfsequence[cat_map_cs_intros]: "vfsequence (cf_map 𝔉)"
unfolding cf_map_def by auto

lemma cf_map_vdomain[cat_map_cs_simps]: "𝒟⇩∘ (cf_map 𝔉) = 2⇩ℕ"
unfolding cf_map_def by (simp add: nat_omega_simps)

lemma (in is_functor) cf_map_vsubset_cf: "cf_map 𝔉 ⊆⇩∘ 𝔉"
by (unfold cf_map_def, subst (3) cf_def)
(cs_concl cs_shallow cs_intro: vcons_vsubset' V_cs_intros)

text‹Size.›

lemma (in is_functor) cf_map_ObjMap_in_Vset:
assumes "α ∈⇩∘ β"
shows "cf_map 𝔉⦇ObjMap⦈ ∈⇩∘ Vset β"
using assms unfolding cf_map_components by (intro cf_ObjMap_in_Vset)

lemma (in is_tm_functor) tm_cf_map_ObjMap_in_Vset: "cf_map 𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
unfolding cf_map_components by (rule tm_cf_ObjMap_in_Vset)

lemma (in is_functor) cf_map_ArrMap_in_Vset:
assumes "α ∈⇩∘ β"
shows "cf_map 𝔉⦇ArrMap⦈ ∈⇩∘ Vset β"
using assms unfolding cf_map_components by (intro cf_ArrMap_in_Vset)

lemma (in is_tm_functor) tm_cf_map_ArrMap_in_Vset: "cf_map 𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
unfolding cf_map_components by (rule tm_cf_ArrMap_in_Vset)

lemma (in is_functor) cf_map_in_Vset_4: "cf_map 𝔉 ∈⇩∘ Vset (α + 4⇩ℕ)"
proof-
note [folded VPow_iff, folded Vset_succ[OF Ord_α], cat_cs_intros] =
cf_ObjMap_vsubset_Vset
cf_ArrMap_vsubset_Vset
show ?thesis
by (subst cf_map_def, succ_of_numeral)
(
cs_concl
cs_simp: plus_V_succ_right V_cs_simps
cs_intro: cat_cs_intros V_cs_intros
)
qed

lemma (in is_tm_functor) tm_cf_map_in_Vset: "cf_map 𝔉 ∈⇩∘ Vset α"
using tm_cf_ObjMap_in_Vset tm_cf_ArrMap_in_Vset unfolding cf_map_def
by (cs_concl cs_shallow cs_intro: V_cs_intros)

lemma (in is_functor) cf_map_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "cf_map 𝔉 ∈⇩∘ Vset β"
using assms cf_map_in_Vset_4 cf_map_vsubset_cf
by (auto intro!: cf_in_Vset)

lemma cf_maps_subset_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "{cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅} ⊆ elts (Vset β)"
proof(intro subsetI, unfold mem_Collect_eq, elim exE conjE)
fix x 𝔉 assume x_def: "x = cf_map 𝔉" and 𝔉: "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
interpret is_functor α 𝔄 𝔅 𝔉 by (rule 𝔉)
show "x ∈⇩∘ Vset β" unfolding x_def by (rule cf_map_in_Vset[OF assms])
qed

lemma small_cf_maps[simp]: "small {cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
proof(cases ‹𝒵 α›)
case True
from is_functor.cf_map_in_Vset show ?thesis
by (intro down[of _ ‹Vset (α + ω)›])
(auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
case False
then have "{cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅} = {}" by auto
then show ?thesis by simp
qed

lemma small_tm_cf_maps[simp]: "small {cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅}"
by (rule smaller_than_small[OF small_cf_maps tm_cf_maps_subset_cf_maps])

lemma (in 𝒵) cf_maps_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "cf_maps α 𝔄 𝔅 ∈⇩∘ Vset β"
proof(rule vsubset_in_VsetI)
interpret β: 𝒵 β by (rule assms(1))
show "cf_maps α 𝔄 𝔅 ⊆⇩∘ Vset (α + 4⇩ℕ)"
proof(intro vsubsetI)
fix 𝔉 assume "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅"
then obtain 𝔄 𝔅 𝔉' where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉: "𝔉' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by auto
interpret is_functor α 𝔄 𝔅 𝔉' using 𝔉 by simp
show "𝔉 ∈⇩∘ Vset (α + 4⇩ℕ)" unfolding 𝔉_def by (rule cf_map_in_Vset_4)
qed
from assms(2) show "Vset (α + 4⇩ℕ) ∈⇩∘ Vset β"
by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed

lemma (in 𝒵) tm_cf_maps_vsubset_Vset: "tm_cf_maps α 𝔄 𝔅 ⊆⇩∘ Vset α"
proof(intro vsubsetI)
fix 𝔉 assume "𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
then obtain 𝔄 𝔅 𝔉'
where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉: "𝔉' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
by auto
then show "𝔉 ∈⇩∘ Vset α" by (force simp: is_tm_functor.tm_cf_map_in_Vset)
qed

text‹Rules.›

lemma (in is_functor) cf_mapsI: "cf_map 𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅"
by (auto intro: cat_cs_intros)

lemma (in is_tm_functor) tm_cf_mapsI: "cf_map 𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
by (auto intro: cat_small_cs_intros)

lemma (in is_functor) cf_mapsI':
assumes "𝔉' = cf_map 𝔉"
shows "𝔉' ∈⇩∘ cf_maps α 𝔄 𝔅"
unfolding assms by (rule cf_mapsI)

lemma (in is_tm_functor) tm_cf_mapsI':
assumes "𝔉' = cf_map 𝔉"
shows "𝔉' ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
unfolding assms by (rule tm_cf_mapsI)

lemmas [cat_map_cs_intros] =
is_functor.cf_mapsI

lemmas cf_mapsI'[cat_map_cs_intros] =
is_functor.cf_mapsI'[rotated]

lemmas [cat_map_cs_intros] =
is_tm_functor.tm_cf_mapsI

lemmas tm_cf_mapsI'[cat_map_cs_intros] =
is_tm_functor.tm_cf_mapsI'[rotated]

lemma cf_mapsE[elim]:
assumes "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅"
obtains 𝔊 where "𝔉 = cf_map 𝔊" and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
using assms by force

lemma tm_cf_mapsE[elim]:
assumes "𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
obtains 𝔊 where "𝔉 = cf_map 𝔊" and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
using assms by force

text‹The opposite functor map.›

lemma (in is_functor) cf_map_op_cf[cat_op_simps]: "cf_map (op_cf 𝔉) = cf_map 𝔉"
proof(rule vsv_eqI, unfold cat_map_cs_simps)
show "a ∈⇩∘ 2⇩ℕ ⟹ cf_map (op_cf 𝔉)⦇a⦈ = cf_map 𝔉⦇a⦈" for a
by
(
elim_in_numeral,
unfold dghm_field_simps[symmetric] cf_map_components cat_op_simps
)
simp_all
qed (auto intro: cat_map_cs_intros)

lemmas [cat_op_simps] = is_functor.cf_map_op_cf

text‹Elementary properties.›

lemma tm_cf_maps_vsubset_cf_maps: "tm_cf_maps α 𝔄 𝔅 ⊆⇩∘ cf_maps α 𝔄 𝔅"
using tm_cf_maps_subset_cf_maps by simp

lemma tm_cf_maps_in_cf_maps:
assumes "𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
shows "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅"
using assms tm_cf_maps_vsubset_cf_maps[of α 𝔄 𝔅] by blast

lemma cf_map_inj:
assumes "cf_map 𝔉 = cf_map 𝔊" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "𝔉 = 𝔊"
proof(rule cf_eqI)
from assms(1) have ObjMap: "cf_map 𝔉⦇ObjMap⦈ = cf_map 𝔊⦇ObjMap⦈"
and ArrMap: "cf_map 𝔉⦇ArrMap⦈ = cf_map 𝔊⦇ArrMap⦈"
by auto
from ObjMap show "𝔉⦇ObjMap⦈ = 𝔊⦇ObjMap⦈" unfolding cf_map_components by simp
from ArrMap show "𝔉⦇ArrMap⦈ = 𝔊⦇ArrMap⦈" unfolding cf_map_components by simp
qed (auto intro: assms(2,3))

lemma cf_map_eq_iff[cat_map_cs_simps]:
assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "cf_map 𝔉 = cf_map 𝔊 ⟷ 𝔉 = 𝔊"
using cf_map_inj[OF _ assms] by auto

lemma cf_map_eqI:
assumes "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅"
and "𝔊 ∈⇩∘ cf_maps α 𝔄 𝔅"
and "𝔉⦇ObjMap⦈ = 𝔊⦇ObjMap⦈"
and "𝔉⦇ArrMap⦈ = 𝔊⦇ArrMap⦈"
shows "𝔉 = 𝔊"
proof-
from assms(1) obtain 𝔉'
where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉': "𝔉' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by auto
from assms(2) obtain 𝔊'
where 𝔊_def: "𝔊 = cf_map 𝔊'" and 𝔊': "𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by auto
show ?thesis
proof(rule vsv_eqI, unfold 𝔉_def 𝔊_def)
show "a ∈⇩∘ 𝒟⇩∘ (cf_map 𝔉') ⟹ cf_map 𝔉'⦇a⦈ = cf_map 𝔊'⦇a⦈" for a
by
(
unfold cf_map_vdomain,
elim_in_numeral,
insert assms(3,4),
unfold 𝔉_def 𝔊_def
)
(auto simp: dghm_field_simps)
qed (auto simp: cat_map_cs_simps intro: cat_map_cs_intros)
qed

subsection‹Conversion of a functor map to a functor›

subsubsection‹Definition and elementary properties›

definition cf_of_cf_map :: "V ⇒ V ⇒ V ⇒ V"
where "cf_of_cf_map 𝔄 𝔅 𝔉 = [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔄, 𝔅]⇩∘"

text‹Components.›

lemma cf_of_cf_map_components:
shows "cf_of_cf_map 𝔄 𝔅 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and "cf_of_cf_map 𝔄 𝔅 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
and "cf_of_cf_map 𝔄 𝔅 𝔉⦇HomDom⦈ = 𝔄"
and "cf_of_cf_map 𝔄 𝔅 𝔉⦇HomCod⦈ = 𝔅"
unfolding cf_of_cf_map_def dghm_field_simps by (simp_all add: nat_omega_simps)

lemmas [cat_map_extra_cs_simps] = cf_of_cf_map_components(1-2)
lemmas [cat_map_cs_simps] = cf_of_cf_map_components(3-4)

subsubsection‹The conversion of a functor map to a functor is a functor›

lemma (in is_functor) cf_of_cf_map_is_functor:
"cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉) : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof(rule is_functorI')
show "vfsequence (cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉))"
unfolding cf_of_cf_map_def by simp
show "vcard (cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)) = 4⇩ℕ"
unfolding cf_of_cf_map_def by (simp add: nat_omega_simps)
show
"cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇f⦈ :
cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙
cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘𝔄⇙ b" for a b f
unfolding cf_of_cf_map_components cf_map_components
using is_functor_axioms that
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
show
"cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ =
cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙
cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇f⦈"
if "g : b ↦⇘𝔄⇙ c" and "f : a ↦⇘𝔄⇙ b" for b c g a f
using is_functor_axioms that
unfolding cf_of_cf_map_components cf_map_components
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show
"cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ =
𝔅⦇CId⦈⦇cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇c⦈⦈"
if "c ∈⇩∘ 𝔄⦇Obj⦈" for c
using is_functor_axioms that
unfolding cf_of_cf_map_components cf_map_components
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
qed
(
auto simp:
cat_cs_simps
cf_of_cf_map_components
cf_map_components
cf_ObjMap_vrange
intro: cat_cs_intros
)

lemma (in is_functor) cf_of_cf_map_is_functor':
assumes "𝔉' = cf_map 𝔉"
and "𝔄' = 𝔄"
and "𝔅' = 𝔅"
shows "cf_of_cf_map 𝔄 𝔅 𝔉' : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
unfolding assms by (rule cf_of_cf_map_is_functor)

lemmas [cat_map_cs_intros] = is_functor.cf_of_cf_map_is_functor'

subsubsection‹The value of the conversion of a functor map to a functor›

lemma (in is_functor) cf_of_cf_map_of_cf_map[cat_map_cs_simps]:
"cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉) = 𝔉"
proof(rule cf_eqI)
show "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉) : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof(rule is_functorI')
show "vfsequence (cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉))"
unfolding cf_of_cf_map_def by auto
show "vcard (cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)) = 4⇩ℕ"
unfolding cf_of_cf_map_def by (simp add: nat_omega_simps)
show
"cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇f⦈ :
cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙
cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘𝔄⇙ b" for a b f
unfolding cf_of_cf_map_components cf_map_components
using is_functor_axioms that
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
show
"cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ =
cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙
cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇f⦈"
if "g : b ↦⇘𝔄⇙ c" and "f : a ↦⇘𝔄⇙ b" for b c g a f
unfolding cf_of_cf_map_components cf_map_components
using is_functor_axioms that
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show
"cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ =
𝔅⦇CId⦈⦇cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇c⦈⦈"
if "c ∈⇩∘ 𝔄⦇Obj⦈" for c
unfolding cf_of_cf_map_components cf_map_components
using is_functor_axioms that
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
qed
(
auto simp:
cat_cs_simps
cf_of_cf_map_components
cf_map_components
cf_ObjMap_vrange
intro: cat_cs_intros
)
qed (auto simp: cf_of_cf_map_components cf_map_components intro: cat_cs_intros)

lemmas [cat_map_cs_simps] = is_functor.cf_of_cf_map_of_cf_map

subsection‹Natural transformation arrow›

subsubsection‹Definition and elementary properties›

definition ntcf_arrow :: "V ⇒ V"
where "ntcf_arrow 𝔑 = [𝔑⦇NTMap⦈, cf_map (𝔑⦇NTDom⦈), cf_map (𝔑⦇NTCod⦈)]⇩∘"

abbreviation ntcf_arrows :: "V ⇒ V ⇒ V ⇒ V"
where "ntcf_arrows α 𝔄 𝔅 ≡
set {ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"

abbreviation tm_ntcf_arrows :: "V ⇒ V ⇒ V ⇒ V"
where "tm_ntcf_arrows α 𝔄 𝔅 ≡
set {ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅}"

lemma tm_ntcf_arrows_subset_ntcf_arrows:
"{ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅} ⊆
{ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
by auto

text‹Components.›

lemma ntcf_arrow_components:
shows [cat_map_cs_simps]: "ntcf_arrow 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
and "ntcf_arrow 𝔑⦇NTDom⦈ = cf_map (𝔑⦇NTDom⦈)"
and "ntcf_arrow 𝔑⦇NTCod⦈ = cf_map (𝔑⦇NTCod⦈)"
unfolding ntcf_arrow_def nt_field_simps by (simp_all add: nat_omega_simps)

lemma (in is_ntcf) ntcf_arrow_components':
shows "ntcf_arrow 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
and "ntcf_arrow 𝔑⦇NTDom⦈ = cf_map 𝔉"
and "ntcf_arrow 𝔑⦇NTCod⦈ = cf_map 𝔊"
unfolding ntcf_arrow_components ntcf_NTDom ntcf_NTCod by simp_all

lemmas [cat_map_cs_simps] = is_ntcf.ntcf_arrow_components'(2,3)

text‹Elementary properties.›

lemma dg_FUNCT_Arr_components:
shows "[NTM, NTD, NTC]⇩∘⦇NTMap⦈ = NTM"
and "[NTM, NTD, NTC]⇩∘⦇NTDom⦈ = NTD"
and "[NTM, NTD, NTC]⇩∘⦇NTCod⦈ = NTC"
unfolding nt_field_simps by (simp_all add: nat_omega_simps)

lemma ntcf_arrow_vfsequence[cat_map_cs_intros]: "vfsequence (ntcf_arrow 𝔑)"
unfolding ntcf_arrow_def by simp

lemma ntcf_arrow_vdomain[cat_map_cs_simps]: "𝒟⇩∘ (ntcf_arrow 𝔑) = 3⇩ℕ"
unfolding ntcf_arrow_def by (simp add: nat_omega_simps)

text‹Size.›

lemma (in is_ntcf) ntcf_arrow_NTMap_in_Vset:
assumes "α ∈⇩∘ β"
shows "ntcf_arrow 𝔑⦇NTMap⦈ ∈⇩∘ Vset β"
using assms unfolding ntcf_arrow_components by (intro ntcf_NTMap_in_Vset)

lemma (in is_tm_ntcf) tm_ntcf_arrow_NTMap_in_Vset:
"ntcf_arrow 𝔑⦇NTMap⦈ ∈⇩∘ Vset α"
unfolding ntcf_arrow_components by (rule tm_ntcf_NTMap_in_Vset)

lemma (in is_ntcf) ntcf_arrow_NTDom_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "ntcf_arrow 𝔑⦇NTDom⦈ ∈⇩∘ Vset β"
using assms unfolding ntcf_arrow_components' by (rule NTDom.cf_map_in_Vset)

lemma (in is_tm_ntcf) tm_ntcf_arrow_NTDom_in_Vset:
"ntcf_arrow 𝔑⦇NTDom⦈ ∈⇩∘ Vset α"
unfolding ntcf_arrow_components' by (rule NTDom.tm_cf_map_in_Vset)

lemma (in is_ntcf) ntcf_arrow_NTCod_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "ntcf_arrow 𝔑⦇NTCod⦈ ∈⇩∘ Vset β"
using assms unfolding ntcf_arrow_components' by (rule NTCod.cf_map_in_Vset)

lemma (in is_tm_ntcf) tm_ntcf_arrow_NTCod_in_Vset:
"ntcf_arrow 𝔑⦇NTCod⦈ ∈⇩∘ Vset α"
unfolding ntcf_arrow_components' by (rule NTCod.tm_cf_map_in_Vset)

lemma (in is_ntcf) ntcf_arrow_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "ntcf_arrow 𝔑 ∈⇩∘ Vset β"
proof-
interpret ntcf_arrow: vfsequence ‹ntcf_arrow 𝔑›
by (auto intro: cat_map_cs_intros)
interpret β: 𝒵 β by (rule assms(1))
show ?thesis
proof(rule vsv.vsv_Limit_vsv_in_VsetI)
from assms show "𝒟⇩∘ (ntcf_arrow 𝔑) ∈⇩∘ Vset β"
by (auto simp: cat_map_cs_simps)
have "n ∈⇩∘ 𝒟⇩∘ (ntcf_arrow 𝔑) ⟹ ntcf_arrow 𝔑⦇n⦈ ∈⇩∘ Vset β" for n
by
(
unfold ntcf_arrow_vdomain,
elim_in_numeral,
all‹rewrite in "⌑ ∈⇩∘ _" nt_field_simps[symmetric]›,
insert assms,
unfold ntcf_arrow_components'
)
(
auto intro:
ntcf_NTMap_in_Vset NTDom.cf_map_in_Vset NTCod.cf_map_in_Vset
)
with ntcf_arrow.vsv_vrange_vsubset show "ℛ⇩∘ (ntcf_arrow 𝔑) ⊆⇩∘ Vset β"
by simp
qed (auto simp: cat_map_cs_simps)
qed

lemma (in is_tm_ntcf) tm_ntcf_arrow_in_Vset: "ntcf_arrow 𝔑 ∈⇩∘ Vset α"
proof-
interpret tm_ntcf_arrow: vfsequence ‹ntcf_arrow 𝔑›
by (auto intro: cat_map_cs_intros)
show ?thesis
proof(rule vsv.vsv_Limit_vsv_in_VsetI)
have "n ∈⇩∘ 𝒟⇩∘ (ntcf_arrow 𝔑) ⟹ ntcf_arrow 𝔑⦇n⦈ ∈⇩∘ Vset α" for n
by
(
unfold ntcf_arrow_vdomain,
elim_in_numeral,
all‹rewrite in "⌑ ∈⇩∘ _" nt_field_simps[symmetric]›
)
(
intro tm_ntcf_arrow_NTMap_in_Vset
tm_ntcf_arrow_NTDom_in_Vset
tm_ntcf_arrow_NTCod_in_Vset
)+
with tm_ntcf_arrow.vsv_vrange_vsubset show "ℛ⇩∘ (ntcf_arrow 𝔑) ⊆⇩∘ Vset α"
by auto
qed (auto simp: cat_map_cs_simps)
qed

lemma ntcf_arrows_subset_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows
"{ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅} ⊆ elts (Vset β)"
proof(intro subsetI, unfold mem_Collect_eq, elim exE conjE)
fix x 𝔑 𝔉 𝔊 assume x_def: "x = ntcf_arrow 𝔑"
and 𝔑: "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
interpret is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑  by (rule 𝔑)
show "x ∈⇩∘ Vset β" unfolding x_def by (rule ntcf_arrow_in_Vset[OF assms])
qed

lemma tm_ntcf_arrows_subset_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows
"{ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅} ⊆
elts (Vset β)"
proof(intro subsetI, unfold mem_Collect_eq, elim exE conjE)
fix x 𝔑 𝔉 𝔊 assume x_def: "x = ntcf_arrow 𝔑"
and 𝔑: "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
interpret is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑  by (rule 𝔑)
show "x ∈⇩∘ Vset β" unfolding x_def by (rule ntcf_arrow_in_Vset[OF assms])
qed

lemma small_ntcf_arrows[simp]:
"small {ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
proof(cases ‹𝒵 α›)
case True
from is_ntcf.ntcf_arrow_in_Vset show ?thesis
by (intro down[of _ ‹Vset (α + ω)›])
(auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
case False
then have "{ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅} = {}"
by auto
then show ?thesis by simp
qed

lemma small_tm_ntcf_arrows[simp]:
"small {ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅}"
by
(
rule smaller_than_small[
OF small_ntcf_arrows tm_ntcf_arrows_subset_ntcf_arrows
]
)

lemma (in is_ntcf) ntcf_arrow_in_Vset_7: "ntcf_arrow 𝔑 ∈⇩∘ Vset (α + 7⇩ℕ)"
proof-
note [folded VPow_iff, folded Vset_succ[OF Ord_α], cat_cs_intros] =
ntcf_NTMap_vsubset_Vset
from NTDom.cf_map_in_Vset_4 have [cat_cs_intros]:
"cf_map 𝔉 ∈⇩∘ Vset (succ (succ (succ (succ α))))"
by succ_of_numeral
(cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
from NTCod.cf_map_in_Vset_4 have [cat_cs_intros]:
"cf_map 𝔊 ∈⇩∘ Vset (succ (succ (succ (succ α))))"
by succ_of_numeral
(cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
show ?thesis
by (subst ntcf_arrow_def, succ_of_numeral, unfold cat_cs_simps)
(
cs_concl
cs_simp: plus_V_succ_right V_cs_simps
cs_intro: V_cs_intros cat_cs_intros
)
qed

lemma (in 𝒵) ntcf_arrows_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "ntcf_arrows α 𝔄 𝔅 ∈⇩∘ Vset β"
proof(rule vsubset_in_VsetI)
interpret β: 𝒵 β by (rule assms(1))
show "ntcf_arrows α 𝔄 𝔅 ⊆⇩∘ Vset (α + 7⇩ℕ)"
proof(intro vsubsetI)
fix 𝔑 assume "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
then obtain 𝔑' 𝔉 𝔊
where 𝔑_def: "𝔑 = ntcf_arrow 𝔑'"
and 𝔑': "𝔑' : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by clarsimp
interpret is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑' using 𝔑' by simp
show "𝔑 ∈⇩∘ Vset (α + 7⇩ℕ)" unfolding 𝔑_def by (rule ntcf_arrow_in_Vset_7)
qed
from assms(2) show "Vset (α + 7⇩ℕ) ∈⇩∘ Vset β"
by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed

lemma (in 𝒵) tm_ntcf_arrows_vsubset_Vset: "tm_ntcf_arrows α 𝔄 𝔅 ⊆⇩∘ Vset α"
by (clarsimp simp: is_tm_ntcf.tm_ntcf_arrow_in_Vset)

text‹Rules.›

lemma (in is_ntcf) ntcf_arrowsI: "ntcf_arrow 𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
using is_ntcf_axioms by auto

lemma (in is_tm_ntcf) tm_ntcf_arrowsI: "ntcf_arrow 𝔑 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
using is_ntcf_axioms by (auto intro: cat_small_cs_intros)

lemma (in is_ntcf) ntcf_arrowsI':
assumes "𝔑' = ntcf_arrow 𝔑"
shows "𝔑' ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
unfolding assms(1) by (rule ntcf_arrowsI)

lemma (in is_tm_ntcf) tm_ntcf_arrowsI':
assumes "𝔑' = ntcf_arrow 𝔑"
shows "𝔑' ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
unfolding assms(1) by (rule tm_ntcf_arrowsI)

lemmas [cat_map_cs_intros] =
is_ntcf.ntcf_arrowsI

lemmas ntcf_arrowsI'[cat_map_cs_intros] =
is_ntcf.ntcf_arrowsI'[rotated]

lemmas [cat_map_cs_intros] =
is_tm_ntcf.tm_ntcf_arrowsI

lemmas tm_ntcf_arrowsI'[cat_map_cs_intros] =
is_tm_ntcf.tm_ntcf_arrowsI'[rotated]

lemma ntcf_arrowsE[elim]:
assumes "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
obtains 𝔐 𝔉 𝔊 where "𝔑 = ntcf_arrow 𝔐" and "𝔐 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
using assms by auto

lemma tm_ntcf_arrowsE[elim]:
assumes "𝔑 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
obtains 𝔐 𝔉 𝔊 where "𝔑 = ntcf_arrow 𝔐"
and "𝔐 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
using assms by auto

text‹Elementary properties.›

lemma tm_ntcf_arrows_vsubset_ntcf_arrows:
"tm_ntcf_arrows α 𝔄 𝔅 ⊆⇩∘ ntcf_arrows α 𝔄 𝔅"
using tm_ntcf_arrows_subset_ntcf_arrows by auto

lemma tm_ntcf_arrows_in_cf_arrows[cat_map_cs_intros]:
assumes "𝔑 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
shows "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
using assms tm_ntcf_arrows_vsubset_ntcf_arrows[of α 𝔄 𝔅] by blast

lemma ntcf_arrow_inj:
assumes "ntcf_arrow 𝔐 = ntcf_arrow 𝔑"
and "𝔐 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "𝔑 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "𝔐 = 𝔑"
proof(rule ntcf_eqI)
interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔐 by (rule assms(2))
interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉' 𝔊' 𝔑 by (rule assms(3))
from assms(1) have NTMap: "ntcf_arrow 𝔐⦇NTMap⦈ = ntcf_arrow 𝔑⦇NTMap⦈"
and NTDom: "ntcf_arrow 𝔐⦇NTDom⦈ = ntcf_arrow 𝔑⦇NTDom⦈"
and NTCod: "ntcf_arrow 𝔐⦇NTCod⦈ = ntcf_arrow 𝔑⦇NTCod⦈"
by auto
from NTMap show "𝔐⦇NTMap⦈ = 𝔑⦇NTMap⦈" unfolding ntcf_arrow_components by simp
from NTDom NTCod show "𝔐⦇NTDom⦈ = 𝔑⦇NTDom⦈" "𝔐⦇NTCod⦈ = 𝔑⦇NTCod⦈"
unfolding ntcf_arrow_components cf_map_components
by
(
auto simp:
cat_cs_simps
cf_map_eq_iff[OF 𝔐.NTDom.is_functor_axioms 𝔑.NTDom.is_functor_axioms]
cf_map_eq_iff[OF 𝔐.NTCod.is_functor_axioms 𝔑.NTCod.is_functor_axioms]
)
from assms(2,3) show
"𝔐 : 𝔐⦇NTDom⦈ ↦⇩C⇩F 𝔐⦇NTCod⦈ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
"𝔑 : 𝔑⦇NTDom⦈ ↦⇩C⇩F 𝔑⦇NTCod⦈ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by (auto simp: cat_cs_simps)
qed auto

lemma ntcf_arrow_eq_iff[cat_map_cs_simps]:
assumes "𝔐 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔑 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "ntcf_arrow 𝔐 = ntcf_arrow 𝔑 ⟷ 𝔐 = 𝔑"
using ntcf_arrow_inj[OF _ assms] by auto

lemma ntcf_arrow_eqI:
assumes "𝔐 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
and "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
and "𝔐⦇NTMap⦈ = 𝔑⦇NTMap⦈"
and "𝔐⦇NTDom⦈ = 𝔑⦇NTDom⦈"
and "𝔐⦇NTCod⦈ = 𝔑⦇NTCod⦈"
shows "𝔐 = 𝔑"
proof-
from assms(1) obtain 𝔐' 𝔉 𝔊
where 𝔐_def: "𝔐 = ntcf_arrow 𝔐'" and 𝔐': "𝔐' : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by auto
from assms(2) obtain 𝔑' 𝔉' 𝔊'
where 𝔑_def: "𝔑 = ntcf_arrow 𝔑'" and 𝔑': "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by auto
show ?thesis
proof(rule vsv_eqI, unfold 𝔐_def 𝔑_def)
show "a ∈⇩∘ 𝒟⇩∘ (ntcf_arrow 𝔐') ⟹ ntcf_arrow 𝔐'⦇a⦈ = ntcf_arrow 𝔑'⦇a⦈"
for a
by
(
unfold ntcf_arrow_vdomain,
elim_in_numeral,
insert assms(3-5),
unfold 𝔐_def 𝔑_def,
fold nt_field_simps
)
simp_all
qed (auto intro: cat_map_cs_intros simp: cat_map_cs_simps)
qed

subsection‹
Conversion of a natural transformation arrow to a natural transformation
›

subsubsection‹Definition and elementary properties›

definition ntcf_of_ntcf_arrow :: "V ⇒ V ⇒ V ⇒ V"
where "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 =
[
𝔑⦇NTMap⦈,
cf_of_cf_map 𝔄 𝔅 (𝔑⦇NTDom⦈),
cf_of_cf_map 𝔄 𝔅 (𝔑⦇NTCod⦈),
𝔄,
𝔅
]⇩∘"

text‹Components.›

lemma ntcf_of_ntcf_arrow_components:
shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
and "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTDom⦈ = cf_of_cf_map 𝔄 𝔅 (𝔑⦇NTDom⦈)"
and "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTCod⦈ = cf_of_cf_map 𝔄 𝔅 (𝔑⦇NTCod⦈)"
and "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTDGDom⦈ = 𝔄"
and "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTDGCod⦈ = 𝔅"
unfolding ntcf_of_ntcf_arrow_def nt_field_simps
by (simp_all add: nat_omega_simps)

lemmas [cat_map_extra_cs_simps] = ntcf_of_ntcf_arrow_components(1)
lemmas [cat_map_cs_simps] = ntcf_of_ntcf_arrow_components(2-5)

subsubsection‹
The conversion of a natural transformation arrow
to a natural transformation is a natural transformation
›

lemma (in is_ntcf) ntcf_of_ntcf_arrow_is_ntcf:
"ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑) : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof(rule is_ntcfI')
show "vfsequence (ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑))"
unfolding ntcf_of_ntcf_arrow_def by auto
show "vcard (ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑)) = 5⇩ℕ"
unfolding ntcf_of_ntcf_arrow_def by (simp add: nat_omega_simps)
show "ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑)⦇NTMap⦈⦇a⦈ :
𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
using is_ntcf_axioms that
by
(
cs_concl cs_shallow
cs_simp: cat_map_cs_simps cat_map_extra_cs_simps
cs_intro: cat_cs_intros
)
show "ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑)⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ =
𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑)⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘𝔄⇙ b" for a b f
using is_ntcf_axioms that
by
(
cs_concl cs_shallow
cs_simp: ntcf_Comp_commute cat_map_cs_simps cat_map_extra_cs_simps
cs_intro: cat_cs_intros
)
qed
(
use is_ntcf_axioms in
‹auto simp: cat_cs_simps cat_map_cs_simps cat_map_extra_cs_simps›
)

lemma (in is_ntcf) ntcf_of_ntcf_arrow_is_ntcf':
assumes "𝔑' = ntcf_arrow 𝔑" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑' : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
unfolding assms by (rule ntcf_of_ntcf_arrow_is_ntcf)

lemmas [cat_map_cs_intros] = is_ntcf.ntcf_of_ntcf_arrow_is_ntcf'

subsubsection‹
The composition of the conversion of a natural transformation arrow
to a natural transformation
›

lemma (in is_ntcf) ntcf_of_ntcf_arrow[cat_map_cs_simps]:
"ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑) = 𝔑"
by (rule ntcf_eqI)
(
auto
simp: cat_map_cs_simps cat_map_extra_cs_simps
intro: cat_cs_intros ntcf_of_ntcf_arrow_is_ntcf
)

lemmas [cat_map_cs_simps] = is_ntcf.ntcf_of_ntcf_arrow

subsection‹Composition of the natural transformation arrows›

definition ntcf_arrow_vcomp :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
where "ntcf_arrow_vcomp 𝔄 𝔅 𝔐 𝔑 =
ntcf_arrow (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔐 ∙⇩N⇩T⇩C⇩F ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑)"

syntax "_ntcf_arrow_vcomp" :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
(‹(_/ ∙⇩N⇩T⇩C⇩F⇘_,_⇙ _)› [55, 56, 57, 58] 55)
translations "𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔑" ⇌ "CONST ntcf_arrow_vcomp 𝔄 𝔅 𝔐 𝔑"

text‹Components.›

lemma (in is_ntcf) ntcf_arrow_vcomp_components:
"(ntcf_arrow 𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ ntcf_arrow 𝔑)⦇NTMap⦈ = (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈"
"(ntcf_arrow 𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ ntcf_arrow 𝔑)⦇NTDom⦈ = cf_map ((𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTDom⦈)"
"(ntcf_arrow 𝔑 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ ntcf_arrow 𝔐)⦇NTCod⦈ = cf_map ((𝔑 ∙⇩N⇩T⇩C⇩F 𝔐)⦇NTCod⦈)"
unfolding
ntcf_arrow_vcomp_def
ntsmcf_vcomp_components
ntcf_arrow_components
ntcf_of_ntcf_arrow_components
by (simp_all add: cat_cs_simps cat_map_cs_simps)

lemmas [cat_map_cs_simps] = is_ntcf.ntcf_arrow_vcomp_components

text‹Elementary properties.›

lemma ntcf_arrow_vcomp_ntcf_vcomp[cat_map_cs_simps]:
assumes "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "ntcf_arrow 𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ ntcf_arrow 𝔑 = ntcf_arrow (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)"
by (rule ntcf_arrow_eqI, insert assms)
(
cs_concl
cs_simp: ntcf_arrow_vcomp_def cat_map_cs_simps cat_cs_simps
cs_intro: cat_map_cs_intros cat_cs_intros
)+

subsection‹Identity natural transformation arrow›

definition ntcf_arrow_id :: "V ⇒ V ⇒ V ⇒ V"
where "ntcf_arrow_id 𝔄 𝔅 𝔉 = ntcf_arrow (ntcf_id (cf_of_cf_map 𝔄 𝔅 𝔉))"

text‹Components.›

lemma (in is_functor) ntcf_arrow_id_components:
"(ntcf_arrow_id 𝔄 𝔅 (cf_map 𝔉))⦇NTMap⦈ = ntcf_id 𝔉⦇NTMap⦈"
"(ntcf_arrow_id 𝔄 𝔅 (cf_map 𝔉))⦇NTDom⦈ = cf_map (ntcf_id 𝔉⦇NTDom⦈)"
"(ntcf_arrow_id 𝔄 𝔅 (cf_map 𝔉))⦇NTCod⦈ = cf_map (ntcf_id 𝔉⦇NTCod⦈)"
unfolding ntcf_arrow_id_def ntcf_arrow_components
by (simp_all add: cat_map_cs_simps)

lemmas [cat_map_cs_simps] = is_functor.ntcf_arrow_id_components

text‹Identity natural transformation arrow is a natural transformation arrow.›

lemma ntcf_arrow_id_ntcf_id[cat_map_cs_simps]:
assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "ntcf_arrow_id 𝔄 𝔅 (cf_map 𝔉) = ntcf_arrow (ntcf_id 𝔉)"
by (rule ntcf_arrow_eqI, insert assms, unfold ntcf_arrow_id_def)
(
cs_concl
cs_simp: cat_map_cs_simps cat_cs_simps
cs_intro: cat_map_cs_intros cat_cs_intros
)

subsection‹‹FUNCT››

subsubsection‹Definition and elementary properties›

definition dg_FUNCT :: "V ⇒ V ⇒ V ⇒ V"
where "dg_FUNCT α 𝔄 𝔅 =
[
cf_maps α 𝔄 𝔅,
ntcf_arrows α 𝔄 𝔅,
(λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈),
(λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈)
]⇩∘"

lemmas [dg_FUNCT_cs_simps] = cat_map_cs_simps
lemmas [dg_FUNCT_cs_intros] = cat_map_cs_intros

text‹Components.›

lemma dg_FUNCT_components:
shows "dg_FUNCT α 𝔄 𝔅⦇Obj⦈ = cf_maps α 𝔄 𝔅"
and "dg_FUNCT α 𝔄 𝔅⦇Arr⦈ = ntcf_arrows α 𝔄 𝔅"
and "dg_FUNCT α 𝔄 𝔅⦇Dom⦈ = (λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈)"
and "dg_FUNCT α 𝔄 𝔅⦇Cod⦈ = (λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈)"
unfolding dg_FUNCT_def dg_field_simps by (simp_all add: nat_omega_simps)

subsubsection‹Objects›

lemma (in is_functor) dg_FUNCT_ObjI: "cf_map 𝔉 ∈⇩∘ dg_FUNCT α 𝔄 𝔅⦇Obj⦈"
unfolding dg_FUNCT_components by (auto intro: cat_cs_intros)

subsubsection‹Domain and codomain›

mk_VLambda dg_FUNCT_components(3)
|vsv dg_FUNCT_Dom_vsv[dg_FUNCT_cs_intros]|
|vdomain dg_FUNCT_Dom_vdomain[dg_FUNCT_cs_simps]|

mk_VLambda dg_FUNCT_components(4)
|vsv dg_FUNCT_Cod_vsv[dg_FUNCT_cs_intros]|
|vdomain dg_FUNCT_Cod_vdomain[dg_FUNCT_cs_simps]|

lemma (in is_ntcf)
shows dg_FUNCT_Dom_app: "dg_FUNCT α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"
and dg_FUNCT_Cod_app: "dg_FUNCT α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
proof-
from is_ntcf_axioms show
"dg_FUNCT α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"
"dg_FUNCT α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
unfolding dg_FUNCT_components
by
(
cs_concl
cs_simp: dg_FUNCT_cs_simps V_cs_simps cs_intro: dg_FUNCT_cs_intros
)+
qed

lemma (in is_ntcf)
assumes "𝔑' = ntcf_arrow 𝔑"
shows dg_FUNCT_Dom_app': "dg_FUNCT α 𝔄 𝔅⦇Dom⦈⦇𝔑'⦈ = cf_map 𝔉"
and dg_FUNCT_Cod_app': "dg_FUNCT α 𝔄 𝔅⦇Cod⦈⦇𝔑'⦈ = cf_map 𝔊"
unfolding assms by (intro dg_FUNCT_Dom_app dg_FUNCT_Cod_app)+

lemmas [dg_FUNCT_cs_simps] =
is_ntcf.dg_FUNCT_Dom_app'
is_ntcf.dg_FUNCT_Cod_app'

lemma
shows dg_FUNCT_Dom_vrange: "ℛ⇩∘ (dg_FUNCT α 𝔄 𝔅⦇Dom⦈) ⊆⇩∘ dg_FUNCT α 𝔄 𝔅⦇Obj⦈"
and dg_FUNCT_Cod_vrange: "ℛ⇩∘ (dg_FUNCT α 𝔄 𝔅⦇Cod⦈) ⊆⇩∘ dg_FUNCT α 𝔄 𝔅⦇Obj⦈"
unfolding dg_FUNCT_components
proof(all‹intro vrange_VLambda_vsubset›)
fix 𝔑 assume "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
then obtain 𝔐 𝔉 𝔊 where 𝔑_def[dg_FUNCT_cs_simps]: "𝔑 = ntcf_arrow 𝔐"
and 𝔐: "𝔐 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by auto
from 𝔐 show "𝔑⦇NTDom⦈ ∈⇩∘ cf_maps α 𝔄 𝔅"
by (cs_concl cs_simp: dg_FUNCT_cs_simps cs_intro: dg_FUNCT_cs_intros cat_cs_intros)
from 𝔐 show "𝔑⦇NTCod⦈ ∈⇩∘ cf_maps α 𝔄 𝔅"
by
(
cs_concl cs_shallow
cs_simp: dg_FUNCT_cs_simps cs_intro: dg_FUNCT_cs_intros cat_cs_intros
)
qed

subsubsection‹‹FUNCT› is a tiny digraph›

lemma (in 𝒵) tiny_digraph_dg_FUNCT:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "tiny_digraph β (dg_FUNCT α 𝔄 𝔅)"
proof-
interpret β: 𝒵 β by (rule assms(1))
show ?thesis
proof(intro tiny_digraphI)
show "vfsequence (dg_FUNCT α 𝔄 𝔅)" unfolding dg_FUNCT_def by simp
show "vcard (dg_FUNCT α 𝔄 𝔅) = 4⇩ℕ"
unfolding dg_FUNCT_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (dg_FUNCT α 𝔄 𝔅⦇Dom⦈) ⊆⇩∘ dg_FUNCT α 𝔄 𝔅⦇Obj⦈"
by (simp add: dg_FUNCT_Dom_vrange dg_FUNCT_Cod_vrange)
show "ℛ⇩∘ (dg_FUNCT α 𝔄 𝔅⦇Cod⦈) ⊆⇩∘ dg_FUNCT α 𝔄 𝔅⦇Obj⦈"
by (simp add: dg_FUNCT_Dom_vrange dg_FUNCT_Cod_vrange)
from assms show "dg_FUNCT α 𝔄 𝔅⦇Obj⦈ ∈⇩∘ Vset β"
unfolding dg_FUNCT_components(1) by (rule cf_maps_in_Vset)
show "dg_FUNCT α 𝔄 𝔅⦇Arr⦈ ∈⇩∘ Vset β"
unfolding dg_FUNCT_components(2) by (rule ntcf_arrows_in_Vset[OF assms])
qed (auto simp: dg_FUNCT_cs_simps dg_FUNCT_components(1,2) intro: dg_FUNCT_cs_intros)
qed

subsubsection‹Arrow with a domain and a codomain›

lemma dg_FUNCT_is_arrI:
assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "ntcf_arrow 𝔑 : cf_map 𝔉 ↦⇘dg_FUNCT α 𝔄 𝔅⇙ cf_map 𝔊"
proof(intro is_arrI, unfold dg_FUNCT_components(1,2))
interpret is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms)
from assms show "ntcf_arrow 𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅" by auto
from assms show
"dg_FUNCT α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"
"dg_FUNCT α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
by (cs_concl cs_shallow cs_simp: dg_FUNCT_cs_simps)+
qed

lemma dg_FUNCT_is_arrI':
assumes "𝔑' = ntcf_arrow 𝔑"
and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "𝔉' = cf_map 𝔉"
and "𝔊' = cf_map 𝔊"
shows "𝔑' : 𝔉' ↦⇘dg_FUNCT α 𝔄 𝔅⇙ 𝔊'"
using assms(2) unfolding assms(1,3,4) by (rule dg_FUNCT_is_arrI)

lemmas [dg_FUNCT_cs_intros] = dg_FUNCT_is_arrI'

lemma dg_FUNCT_is_arrD[dest]:
assumes "𝔑 : 𝔉 ↦⇘dg_FUNCT α 𝔄 𝔅⇙ 𝔊"
shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F cf_of_cf_map 𝔄 𝔅 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "𝔑 = ntcf_arrow (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑)"
and "𝔉 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔉)"
and "𝔊 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔊)"
proof-
note 𝔑 = is_arrD[OF assms, unfolded dg_FUNCT_components(2)]
obtain 𝔑' 𝔉' 𝔊' where 𝔑_def: "𝔑 = ntcf_arrow 𝔑'"
and 𝔑': "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by (elim ntcf_arrowsE[OF 𝔑(1)])
from 𝔑(2) 𝔑' have 𝔉_def: "𝔉 = cf_map 𝔉'"
by (cs_prems cs_simp: 𝔑_def dg_FUNCT_cs_simps) simp
from 𝔑(3) 𝔑' have 𝔊_def: "𝔊 = cf_map 𝔊'"
by (cs_prems cs_simp: 𝔑_def dg_FUNCT_cs_simps) simp
from 𝔑' have 𝔑'_def: "𝔑' = ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑"
unfolding 𝔑_def by (cs_concl cs_shallow cs_simp: dg_FUNCT_cs_simps)
from 𝔑' have 𝔉'_def: "𝔉' = cf_of_cf_map 𝔄 𝔅 𝔉"
and 𝔊'_def: "𝔊' = cf_of_cf_map 𝔄 𝔅 𝔊"
unfolding 𝔉_def 𝔊_def
by (cs_concl cs_simp: dg_FUNCT_cs_simps cs_intro: cat_cs_intros)+
from 𝔑' show "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F cf_of_cf_map 𝔄 𝔅 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "𝔑 = ntcf_arrow (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑)"
and "𝔉 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔉)"
and "𝔊 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔊)"
by (fold 𝔉'_def 𝔊'_def 𝔑'_def 𝔉_def 𝔊_def 𝔑_def) simp_all
qed

lemma dg_FUNCT_is_arrE[elim]:
assumes "𝔑 : 𝔉 ↦⇘dg_FUNCT α 𝔄 𝔅⇙ 𝔊"
obtains 𝔑' 𝔉' 𝔊'
where "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "𝔑 = ntcf_arrow 𝔑'"
and "𝔉 = cf_map 𝔉'"
and "𝔊 = cf_map 𝔊'"
using dg_FUNCT_is_arrD[OF assms] by auto

subsection‹‹Funct››

subsubsection‹Definition and elementary properties›

definition dg_Funct :: "V ⇒ V ⇒ V ⇒ V"
where "dg_Funct α 𝔄 𝔅 =
[
tm_cf_maps α 𝔄 𝔅,
tm_ntcf_arrows α 𝔄 𝔅,
(λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈),
(λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈)
]⇩∘"

text‹Components.›

lemma dg_Funct_components:
shows "dg_Funct α 𝔄 𝔅⦇Obj⦈ = tm_cf_maps α 𝔄 𝔅"
and "dg_Funct α 𝔄 𝔅⦇Arr⦈ = tm_ntcf_arrows α 𝔄 𝔅"
and "dg_Funct α 𝔄 𝔅⦇Dom⦈ = (λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈)"
and "dg_Funct α 𝔄 𝔅⦇Cod⦈ = (λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈)"
unfolding dg_Funct_def dg_field_simps by (simp_all add: nat_omega_simps)

subsubsection‹Objects›

lemma (in is_tm_functor) dg_Funct_ObjI: "cf_map 𝔉 ∈⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
unfolding dg_Funct_components by (auto simp: cat_small_cs_intros)

subsubsection‹Domain and codomain›

mk_VLambda dg_Funct_components(3)
|vsv dg_Funct_Dom_vsv[dg_FUNCT_cs_intros]|
|vdomain dg_Funct_Dom_vdomain[dg_FUNCT_cs_simps]|

mk_VLambda dg_Funct_components(4)
|vsv dg_Funct_Cod_vsv[dg_FUNCT_cs_intros]|
|vdomain dg_Funct_Cod_vdomain[dg_FUNCT_cs_simps]|

lemma (in is_tm_ntcf)
shows dg_Funct_Dom_app: "dg_Funct α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"
and dg_Funct_Cod_app: "dg_Funct α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
proof-
from is_tm_ntcf_axioms show
"dg_Funct α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"
"dg_Funct α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
unfolding dg_Funct_components
by
(
cs_concl cs_shallow
cs_simp: dg_FUNCT_cs_simps V_cs_simps
cs_intro: dg_FUNCT_cs_intros cat_cs_intros
)+
qed

lemma (in is_tm_ntcf)
assumes "𝔑' = ntcf_arrow 𝔑"
shows dg_Funct_Dom_app': "dg_Funct α 𝔄 𝔅⦇Dom⦈⦇𝔑'⦈ = cf_map 𝔉"
and dg_Funct_Cod_app': "dg_Funct α 𝔄 𝔅⦇Cod⦈⦇𝔑'⦈ = cf_map 𝔊"
unfolding assms by (intro dg_Funct_Dom_app dg_Funct_Cod_app)+

lemmas [dg_FUNCT_cs_simps] =
is_tm_ntcf.dg_Funct_Dom_app'
is_tm_ntcf.dg_Funct_Cod_app'

lemma
shows dg_Funct_Dom_vrange: "ℛ⇩∘ (dg_Funct α 𝔄 𝔅⦇Dom⦈) ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
and dg_Funct_Cod_vrange: "ℛ⇩∘ (dg_Funct α 𝔄 𝔅⦇Cod⦈) ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
unfolding dg_Funct_components
proof(all‹intro vrange_VLambda_vsubset›)
fix 𝔑 assume "𝔑 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
then obtain 𝔐 𝔉 𝔊 where 𝔑_def[dg_FUNCT_cs_simps]: "𝔑 = ntcf_arrow 𝔐"
and 𝔐: "𝔐 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
by auto
from 𝔐 show "𝔑⦇NTDom⦈ ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
by
(
cs_concl
cs_simp: dg_FUNCT_cs_simps
cs_intro: dg_FUNCT_cs_intros cat_small_cs_intros
)
from 𝔐 show "𝔑⦇NTCod⦈ ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
by
(
cs_concl cs_shallow
cs_simp: dg_FUNCT_cs_simps
cs_intro: dg_FUNCT_cs_intros cat_small_cs_intros
)
qed

subsubsection‹Arrow with a domain and a codomain›

lemma dg_Funct_is_arrI:
assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
shows "ntcf_arrow 𝔑 : cf_map 𝔉 ↦⇘dg_Funct α 𝔄 𝔅⇙ cf_map 𝔊"
proof(intro is_arrI, unfold dg_Funct_components(1,2))
interpret is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms)
from assms show "ntcf_arrow 𝔑 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅" by auto
from assms show
"dg_Funct α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"
"dg_Funct α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
by (cs_concl cs_shallow cs_simp: dg_FUNCT_cs_simps)+
qed

lemma dg_Funct_is_arrI':
assumes "𝔑' = ntcf_arrow 𝔑"
and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
and "𝔉' = cf_map 𝔉"
and "𝔊' = cf_map 𝔊"
shows "𝔑' : 𝔉' ↦⇘dg_Funct α 𝔄 𝔅⇙ 𝔊'"
using assms(2) unfolding assms(1,3,4) by (rule dg_Funct_is_arrI)

lemmas [dg_FUNCT_cs_intros] = dg_Funct_is_arrI'

lemma dg_Funct_is_arrD[dest]:
assumes "𝔑 : 𝔉 ↦⇘dg_Funct α 𝔄 𝔅⇙ 𝔊"
shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F⇩.⇩t⇩m cf_of_cf_map 𝔄 𝔅 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
and "𝔑 = ntcf_arrow (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑)"
and "𝔉 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔉)"
and "𝔊 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔊)"
proof-
note 𝔑 = is_arrD[OF assms, unfolded dg_Funct_components(2)]
obtain 𝔑' 𝔉' 𝔊' where 𝔑_def: "𝔑 = ntcf_arrow 𝔑'"
and 𝔑': "𝔑' : 𝔉' ↦⇩C⇩F⇩.⇩t⇩m 𝔊' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
by (elim tm_ntcf_arrowsE[OF 𝔑(1)])
from 𝔑(2) 𝔑' have 𝔉_def: "𝔉 = cf_map 𝔉'"
by (cs_prems cs_simp: 𝔑_def dg_FUNCT_cs_simps) simp
from 𝔑(3) 𝔑' have 𝔊_def: "𝔊 = cf_map 𝔊'"
by (cs_prems cs_simp: 𝔑_def dg_FUNCT_cs_simps) simp
from 𝔑' have 𝔑'_def: "𝔑' = ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑"
unfolding 𝔑_def
by
(
cs_concl cs_shallow
cs_simp: dg_FUNCT_cs_simps cs_intro: cat_small_cs_intros cat_cs_intros
)
from 𝔑' have 𝔉'_def: "𝔉' = cf_of_cf_map 𝔄 𝔅 𝔉"
and 𝔊'_def: "𝔊' = cf_of_cf_map 𝔄 𝔅 𝔊"
unfolding 𝔉_def 𝔊_def
by
(
cs_concl
cs_simp: dg_FUNCT_cs_simps cs_intro: cat_small_cs_intros cat_cs_intros
)+
from 𝔑' show "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F⇩.⇩t⇩m cf_of_cf_map 𝔄 𝔅 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
and "𝔑 = ntcf_arrow (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑)"
and "𝔉 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔉)"
and "𝔊 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔊)"
by (fold 𝔉'_def 𝔊'_def 𝔑'_def 𝔉_def 𝔊_def 𝔑_def) simp_all
qed

lemma dg_Funct_is_arrE[elim]:
assumes "𝔑 : 𝔉 ↦⇘dg_Funct α 𝔄 𝔅⇙ 𝔊"
obtains 𝔑' 𝔉' 𝔊' where "𝔑' : 𝔉' ↦⇩C⇩F⇩.⇩t⇩m 𝔊' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
and "𝔑 = ntcf_arrow 𝔑'"
and "𝔉 = cf_map 𝔉'"
and "𝔊 = cf_map 𝔊'"
using dg_Funct_is_arrD[OF assms] by auto

subsubsection‹‹Funct› is a digraph›

lemma digraph_dg_Funct:
assumes "tiny_category α 𝔄" and "category α 𝔅"
shows "digraph α (dg_Funct α 𝔄 𝔅)"
proof-

interpret tiny_category α 𝔄 by (rule assms(1))
interpret 𝔅: category α 𝔅 by (rule assms(2))

show ?thesis

proof(intro digraphI)

show "vfsequence (dg_Funct α 𝔄 𝔅)" unfolding dg_Funct_def by simp
show "vcard (dg_Funct α 𝔄 𝔅) = 4⇩ℕ"
unfolding dg_Funct_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (dg_Funct α 𝔄 𝔅⦇Dom⦈) ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
by (simp add: dg_Funct_Dom_vrange dg_Funct_Cod_vrange)
show "ℛ⇩∘ (dg_Funct α 𝔄 𝔅⦇Cod⦈) ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
by (simp add: dg_Funct_Dom_vrange dg_Funct_Cod_vrange)
show "dg_Funct α 𝔄 𝔅⦇Obj⦈ ⊆⇩∘ Vset α"
unfolding dg_Funct_components(1,2) by (rule tm_cf_maps_vsubset_Vset)

have RA:
"(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ∈⇩∘ Vset α"
"(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ⊆⇩∘ 𝔅⦇Obj⦈"
if "A ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈" and "A ∈⇩∘ Vset α" for A
proof-
have "(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ⊆⇩∘ 𝔅⦇Obj⦈"
and "(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ⊆⇩∘ ⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘A)))))"
proof(all‹intro vsubsetI›)
fix f assume "f ∈⇩∘ (⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈))"
then obtain 𝔉 where 𝔉: "𝔉 ∈⇩∘ A" and f: "f ∈⇩∘ ℛ⇩∘ (𝔉⦇ObjMap⦈)" by auto
with that(1) have "𝔉 ∈⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈" by (elim vsubsetE)
then obtain 𝔉'
where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉': "𝔉' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
unfolding dg_Funct_components by auto
interpret 𝔉': is_tm_functor α 𝔄 𝔅 𝔉' by (rule 𝔉')
from f obtain a where "a ∈⇩∘ 𝒟⇩∘ (𝔉'⦇ObjMap⦈)" and af: "⟨a, f⟩ ∈⇩∘ 𝔉'⦇ObjMap⦈"
unfolding 𝔉_def cf_map_components vdomain_iff by force
then show "f ∈⇩∘ 𝔅⦇Obj⦈"
using 𝔉'.cf_ObjMap_vrange 𝔉_def cf_map_components(1) f vsubsetE by auto
show "f ∈⇩∘ ⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘A)))))"
proof(intro VUnionI)
show "𝔉 ∈⇩∘ A" by (rule 𝔉)
show "set {0, 𝔉⦇ObjMap⦈} ∈⇩∘ ⟨[]⇩∘, 𝔉⦇ObjMap⦈⟩" unfolding vpair_def by simp
show "⟨a, f⟩ ∈⇩∘ 𝔉⦇ObjMap⦈"
unfolding 𝔉_def cf_map_components by (intro af)
show "set {a, f} ∈⇩∘ ⟨a, f⟩" unfolding vpair_def by clarsimp
qed (clarsimp simp: 𝔉_def cf_map_def dg_FUNCT_Obj_components)+
qed
moreover have "⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘A))))) ∈⇩∘ Vset α"
by (intro VUnion_in_VsetI that(2))
ultimately show
"(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ∈⇩∘ Vset α"
"(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ⊆⇩∘ 𝔅⦇Obj⦈"
by blast+
qed

fix A B assume prems:
"A ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
"B ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
"A ∈⇩∘ Vset α"
"B ∈⇩∘ Vset α"

define ARs where "ARs = (⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈))"
define BRs where "BRs = (⋃⇩∘𝔊∈⇩∘B. ℛ⇩∘ (𝔊⦇ObjMap⦈))"
define Hom_AB where "Hom_AB = (⋃⇩∘a∈⇩∘ARs. ⋃⇩∘b∈⇩∘BRs. Hom 𝔅 a b)"

define Q where
"Q i = (if i = 0 then VPow (𝔄⦇Obj⦈ ×⇩∘ Hom_AB) else if i = 1⇩ℕ then A else B)"
for i
have
"{[𝔑, 𝔉, 𝔊]⇩∘ |𝔑 𝔉 𝔊. 𝔑 ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB ∧ 𝔉 ∈⇩∘ A ∧ 𝔊 ∈⇩∘ B} ⊆
elts (∏⇩∘i∈⇩∘set {0, 1⇩ℕ, 2⇩ℕ}. Q i)"
proof(intro subsetI, unfold mem_Collect_eq, elim exE conjE)
fix 𝔑𝔉𝔊 𝔑 𝔉 𝔊 assume prems':
"𝔑𝔉𝔊 = [𝔑, 𝔉, 𝔊]⇩∘" "𝔑 ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB" "𝔉 ∈⇩∘ A" "𝔊 ∈⇩∘ B"
show "𝔑𝔉𝔊 ∈⇩∘ (∏⇩∘i∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}. Q i)"
proof(intro vproductI, unfold Ball_def; (intro allI impI)?)
fix i assume "i ∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}"
then consider ‹i = 0› | ‹i = 1⇩ℕ› | ‹i = 2⇩ℕ› by auto
then show "𝔑𝔉𝔊⦇i⦈ ∈⇩∘ Q i"
by cases (auto simp: Q_def prems' nat_omega_simps)
qed (auto simp: prems'(1) three nat_omega_simps)
qed
moreover then have small[simp]:
"small {[r, a, b]⇩∘ | r a b. r ⊆⇩∘𝔄⦇Obj⦈ ×⇩∘ Hom_AB ∧ a ∈⇩∘ A ∧ b ∈⇩∘ B}"
by (rule down)
ultimately have
"set {[r, a, b]⇩∘ |r a b. r ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB ∧ a ∈⇩∘ A ∧ b ∈⇩∘ B} ⊆⇩∘
(∏⇩∘i∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}. Q i)"
by auto
moreover have "(∏⇩∘i∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}. Q i) ∈⇩∘ Vset α"
proof(rule Limit_vproduct_in_VsetI)
show "set {0, 1⇩ℕ, 2⇩ℕ} ∈⇩∘ Vset α"
by (cs_concl cs_intro: V_cs_intros cat_cs_intros cs_simp: V_cs_simps)
have "Hom_AB ∈⇩∘ Vset α"
unfolding Hom_AB_def
by
(
intro 𝔅.cat_Hom_vifunion_in_Vset prems(3,4),
unfold ARs_def BRs_def;
intro RA prems
)
moreover have "𝔄⦇Obj⦈ ∈⇩∘ Vset α" by (intro tiny_cat_Obj_in_Vset)
ultimately have "VPow (𝔄⦇Obj⦈ ×⇩∘ Hom_AB) ∈⇩∘ Vset α"
by (cs_concl cs_shallow cs_intro: V_cs_intros)
with prems(3,4) show "Q i ∈⇩∘ Vset α" if "i ∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}" for i
unfolding Q_def by (simp_all add: nat_omega_simps)
qed auto
moreover have
"(⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom (dg_Funct α 𝔄 𝔅) a b) ⊆⇩∘
set {[r, a, b]⇩∘ | r a b. r ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB ∧ a ∈⇩∘ A ∧ b ∈⇩∘ B}"
proof(rule vsubsetI)
fix 𝔑 assume "𝔑 ∈⇩∘ (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom (dg_Funct α 𝔄 𝔅) a b)"
then obtain 𝔉 𝔊
where 𝔉: "𝔉 ∈⇩∘ A"
and 𝔊: "𝔊 ∈⇩∘ B"
and 𝔑_ab: "𝔑 ∈⇩∘ Hom (dg_Funct α 𝔄 𝔅) 𝔉 𝔊"
by auto
then have "𝔑 : 𝔉 ↦⇘dg_Funct α 𝔄 𝔅⇙ 𝔊" by simp
note 𝔑 = dg_Funct_is_arrD[OF this]
show
"𝔑 ∈⇩∘ set {[r, a, b]⇩∘ | r a b. r ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB ∧ a ∈⇩∘ A ∧ b ∈⇩∘ B}"
proof(intro in_set_CollectI small exI conjI)
show "𝔑 =
[
ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTMap⦈,
cf_map (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTDom⦈),
cf_map (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTCod⦈)
]⇩∘"
by (rule 𝔑(2)[unfolded ntcf_arrow_def])
interpret 𝔑: is_tm_ntcf α
𝔄 𝔅
‹cf_of_cf_map 𝔄 𝔅 𝔉› ‹cf_of_cf_map 𝔄 𝔅 𝔊›
‹ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑›
rewrites "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
and "cf_of_cf_map 𝔄 𝔅 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and "cf_of_cf_map 𝔄 𝔅 𝔊⦇ObjMap⦈ = 𝔊⦇ObjMap⦈"
by
(
rule 𝔑(1),
unfold ntcf_of_ntcf_arrow_components cf_of_cf_map_components
)
simp_all
show "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTMap⦈ ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB"
proof(intro vsubsetI, unfold ntcf_of_ntcf_arrow_components)
fix af assume prems'': "af ∈⇩∘ 𝔑⦇NTMap⦈"
then obtain a f where af_def: "af = ⟨a, f⟩"
and a: "a ∈⇩∘ 𝔄⦇Obj⦈"
and f: "f ∈⇩∘ ℛ⇩∘ (𝔑⦇NTMap⦈)"
by (elim 𝔑.NTMap.vbrelation_vinE)
from prems'' have f_def: "f = 𝔑⦇NTMap⦈⦇a⦈"
unfolding af_def 𝔑.NTMap.vsv_ex1_app1[OF a] .
have 𝔑a: "𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"
by (rule 𝔑.ntcf_NTMap_is_arr[OF a])
have "f ∈⇩∘ Hom_AB"
unfolding f_def Hom_AB_def ARs_def BRs_def
proof(intro vifunionI, unfold in_Hom_iff)
show "𝔉 ∈⇩∘ A" by (intro 𝔉)
from a show "𝔉⦇ObjMap⦈⦇a⦈ ∈⇩∘ ℛ⇩∘ (𝔉⦇ObjMap⦈)"
by (metis 𝔑.NTDom.ObjMap.vdomain_atD 𝔑.NTDom.cf_ObjMap_vdomain)
show "𝔊 ∈⇩∘ B" by (intro 𝔊)
from a show "𝔊⦇ObjMap⦈⦇a⦈ ∈⇩∘ ℛ⇩∘ (𝔊⦇ObjMap⦈)"
by (metis 𝔑.NTCod.ObjMap.vdomain_atD 𝔑.NTCod.cf_ObjMap_vdomain)
show "𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈" by (intro 𝔑a)
qed
with a show "af ∈⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB" unfolding af_def f_def by simp
qed
show "cf_map (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTDom⦈) ∈⇩∘ A"
unfolding 𝔑.ntcf_NTDom 𝔑(3)[symmetric] by (rule 𝔉)
show "cf_map (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTCod⦈) ∈⇩∘ B"
unfolding 𝔑.ntcf_NTCod 𝔑(4)[symmetric] by (rule 𝔊)
qed
qed
ultimately show "(⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom (dg_Funct α 𝔄 𝔅) a b) ∈⇩∘ Vset α"
by blast
qed (auto simp: dg_Funct_components)

qed

subsubsection‹‹Funct› is a subdigraph of ‹FUNCT››

lemma subdigraph_dg_Funct_dg_FUNCT:
assumes "𝒵 β" and "α ∈⇩∘ β" and "tiny_category α 𝔄" and "category α 𝔅"
shows "dg_Funct α 𝔄 𝔅 ⊆⇩D⇩G⇘β⇙ dg_FUNCT α 𝔄 𝔅"
proof(intro subdigraphI, unfold dg_FUNCT_components(1) dg_Funct_components(1))
interpret 𝔄: tiny_category α 𝔄 by (rule assms(3))
interpret β: 𝒵 β by (rule assms(1))
show "digraph β (dg_Funct α 𝔄 𝔅)"
by (intro digraph.dg_digraph_if_ge_Limit[OF digraph_dg_Funct] assms)
from assms show "digraph β (dg_FUNCT α 𝔄 𝔅)"
by (cs_concl cs_shallow cs_intro: dg_small_cs_intros 𝔄.tiny_digraph_dg_FUNCT)
show "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅" if "𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅" for 𝔉
using that
by (cs_concl cs_shallow cs_intro: dg_FUNCT_cs_intros tm_cf_maps_in_cf_maps)
show "𝔑 : 𝔉 ↦⇘dg_FUNCT α 𝔄 𝔅⇙ 𝔊" if "𝔑 : 𝔉 ↦⇘dg_Funct α 𝔄 𝔅⇙ 𝔊"
for 𝔑 𝔉 𝔊
proof-
note f = dg_Funct_is_arrD[OF that]
from f(1) show ?thesis
by (subst f(2), use nothing in ‹subst f(3), subst f(4)›)
(cs_concl cs_shallow cs_intro: dg_FUNCT_cs_intros cat_small_cs_intros)
qed
qed

text‹\newpage›

end