Theory CZH_ECAT_Structure_Example

```(* Copyright 2021 (C) Mihails Milehins *)

theory CZH_ECAT_Structure_Example
imports
CZH_ECAT_Introduction
CZH_ECAT_PCategory
CZH_ECAT_Set
begin

subsection‹Background›

text‹
The examples that are presented in this section showcase
be used for the formalization of the theory of
categories with additional structure. The content of
this section also indicates some of the potential
future directions for this body of work.
›

subsection‹Dagger category›

named_theorems dag_field_simps

named_theorems dagcat_cs_simps
named_theorems dagcat_cs_intros

definition DagCat :: V where [dag_field_simps]: "DagCat = 0"
definition DagDag :: V where [dag_field_simps]: "DagDag = 1⇩ℕ"

abbreviation DagDag_app :: "V ⇒ V" (‹†⇩C›)
where "†⇩C ℭ ≡ ℭ⦇DagDag⦈"

subsubsection‹Definition and elementary properties›

text‹
For further information see
\<^cite>‹"noauthor_nlab_nodate"›\footnote{\url{
https://ncatlab.org/nlab/show/dagger+category
}}.
›

locale dagger_category =
𝒵 α +
vfsequence ℭ +
DagCat: category α ‹ℭ⦇DagCat⦈› +
DagDag: is_functor α ‹op_cat (ℭ⦇DagCat⦈)› ‹ℭ⦇DagCat⦈› ‹†⇩C ℭ›
for α ℭ +
assumes dagcat_length: "vcard ℭ = 2⇩ℕ"
and dagcat_ObjMap_identity[dagcat_cs_simps]:
"a ∈⇩∘ ℭ⦇DagCat⦈⦇Obj⦈ ⟹ (†⇩C ℭ)⦇ObjMap⦈⦇a⦈ = a"
and dagcat_DagCat_idem[dagcat_cs_simps]:
"†⇩C ℭ ⇩C⇩F∘ †⇩C ℭ = cf_id (ℭ⦇DagCat⦈)"

lemmas [dagcat_cs_simps] =
dagger_category.dagcat_ObjMap_identity
dagger_category.dagcat_DagCat_idem

text‹Rules.›

lemma (in dagger_category) dagger_category_axioms'[dagcat_cs_intros]:
assumes "α' = α"
shows "dagger_category α' ℭ"
unfolding assms by (rule dagger_category_axioms)

mk_ide rf dagger_category_def[unfolded dagger_category_axioms_def]
|intro dagger_categoryI|
|dest dagger_categoryD[dest]|
|elim dagger_categoryE[elim]|

lemma category_if_dagger_category[dagcat_cs_intros]:
assumes "ℭ' = (ℭ⦇DagCat⦈)" and "dagger_category α ℭ"
shows "category α ℭ'"
unfolding assms(1) using assms(2) by (rule dagger_categoryD(3))

lemma (in dagger_category) dagcat_is_functor'[dagcat_cs_intros]:
assumes "𝔄' = op_cat (ℭ⦇DagCat⦈)" and "𝔅' = ℭ⦇DagCat⦈"
shows "†⇩C ℭ : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
unfolding assms by (rule DagDag.is_functor_axioms)

lemmas [dagcat_cs_intros] = dagger_category.dagcat_is_functor'

subsection‹‹Rel› as a dagger category›

subsubsection‹Definition and elementary properties›

text‹
For further information see
\<^cite>‹"noauthor_nlab_nodate"›\footnote{\url{
https://ncatlab.org/nlab/show/Rel
}}.
›

definition dagcat_Rel :: "V ⇒ V"
where "dagcat_Rel α = [cat_Rel α, †⇩C⇩.⇩R⇩e⇩l α]⇩∘"

text‹Components.›

lemma dagcat_Rel_components:
shows "dagcat_Rel α⦇DagCat⦈ = cat_Rel α"
and "dagcat_Rel α⦇DagDag⦈ = †⇩C⇩.⇩R⇩e⇩l α"
unfolding dagcat_Rel_def dag_field_simps by (simp_all add: nat_omega_simps)

subsubsection‹‹Rel› is a dagger category›

lemma (in 𝒵) dagger_category_dagcat_Rel: "dagger_category α (dagcat_Rel α)"
proof(intro dagger_categoryI)
show "category α (dagcat_Rel α⦇DagCat⦈)"
by
(
cs_concl cs_shallow
cs_simp: dagcat_Rel_components cs_intro: cat_Rel_cs_intros
)
show "†⇩C (dagcat_Rel α) :
op_cat (dagcat_Rel α⦇DagCat⦈) ↦↦⇩C⇘α⇙ dagcat_Rel α⦇DagCat⦈"
unfolding dagcat_Rel_components
by (cs_concl cs_intro: cf_cs_intros cat_cs_intros)
show "vcard (dagcat_Rel α) = 2⇩ℕ"
unfolding dagcat_Rel_def by (simp add: nat_omega_simps)
show "†⇩C (dagcat_Rel α)⦇ObjMap⦈⦇a⦈ = a"
if "a ∈⇩∘ dagcat_Rel α⦇DagCat⦈⦇Obj⦈" for a
using that
unfolding dagcat_Rel_components cat_Rel_components(1)
by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_Rel_cs_simps)
show "†⇩C (dagcat_Rel α) ⇩C⇩F∘ †⇩C (dagcat_Rel α) = dghm_id (dagcat_Rel α⦇DagCat⦈)"
unfolding dagcat_Rel_components
by (cs_concl cs_shallow cs_simp: cf_cn_comp_cf_dag_Rel_cf_dag_Rel)
qed (auto simp: dagcat_Rel_def)

subsection‹Monoidal category›

text‹
For background information see Chapter 2 in \<^cite>‹"etingof_tensor_2015"›.
›

subsubsection‹Background›

named_theorems mcat_field_simps

named_theorems mcat_cs_simps
named_theorems mcat_cs_intros

definition Mcat :: V where [mcat_field_simps]: "Mcat = 0"
definition Mcf :: V where [mcat_field_simps]: "Mcf = 1⇩ℕ"
definition Me :: V where [mcat_field_simps]: "Me = 2⇩ℕ"
definition Mα :: V where [mcat_field_simps]: "Mα = 3⇩ℕ"
definition Ml :: V where [mcat_field_simps]: "Ml = 4⇩ℕ"
definition Mr :: V where [mcat_field_simps]: "Mr = 5⇩ℕ"

subsubsection‹Definition and elementary properties›

locale monoidal_category =
―‹See Definition 2.2.8 in \cite{etingof_tensor_2015}.›
𝒵 α +
vfsequence ℭ +
Mcat: category α ‹ℭ⦇Mcat⦈› +
Mcf: is_functor α ‹(ℭ⦇Mcat⦈) ×⇩C (ℭ⦇Mcat⦈)› ‹ℭ⦇Mcat⦈› ‹ℭ⦇Mcf⦈› +
Mα: is_iso_ntcf
α ‹ℭ⦇Mcat⦈^⇩C⇩3› ‹ℭ⦇Mcat⦈› ‹cf_blcomp (ℭ⦇Mcf⦈)› ‹cf_brcomp (ℭ⦇Mcf⦈)› ‹ℭ⦇Mα⦈› +
Ml: is_iso_ntcf
α
‹ℭ⦇Mcat⦈›
‹ℭ⦇Mcat⦈›
‹ℭ⦇Mcf⦈⇘ℭ⦇Mcat⦈,ℭ⦇Mcat⦈⇙(ℭ⦇Me⦈,-)⇩C⇩F›
‹cf_id (ℭ⦇Mcat⦈)›
‹ℭ⦇Ml⦈› +
Mr: is_iso_ntcf
α
‹ℭ⦇Mcat⦈›
‹ℭ⦇Mcat⦈›
‹ℭ⦇Mcf⦈⇘ℭ⦇Mcat⦈,ℭ⦇Mcat⦈⇙(-,ℭ⦇Me⦈)⇩C⇩F›
‹cf_id (ℭ⦇Mcat⦈)›
‹ℭ⦇Mr⦈›
for α ℭ +
assumes mcat_length[mcat_cs_simps]: "vcard ℭ = 6⇩ℕ"
and mcat_Me_is_obj[mcat_cs_intros]: "ℭ⦇Me⦈ ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈"
and mcat_pentagon:
"⟦
a ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈;
b ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈;
c ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈;
d ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈
⟧ ⟹
(ℭ⦇Mcat⦈⦇CId⦈⦇a⦈ ⊗⇩H⇩M⇩.⇩A⇘ℭ⦇Mcf⦈⇙ ℭ⦇Mα⦈⦇NTMap⦈⦇b, c, d⦈⇩∙) ∘⇩A⇘ℭ⦇Mcat⦈⇙
ℭ⦇Mα⦈⦇NTMap⦈⦇a, b ⊗⇩H⇩M⇩.⇩O⇘ℭ⦇Mcf⦈⇙ c, d⦈⇩∙ ∘⇩A⇘ℭ⦇Mcat⦈⇙
(ℭ⦇Mα⦈⦇NTMap⦈⦇a, b, c⦈⇩∙ ⊗⇩H⇩M⇩.⇩A⇘ℭ⦇Mcf⦈⇙ ℭ⦇Mcat⦈⦇CId⦈⦇d⦈) =
ℭ⦇Mα⦈⦇NTMap⦈⦇a, b, c ⊗⇩H⇩M⇩.⇩O⇘ℭ⦇Mcf⦈⇙ d⦈⇩∙ ∘⇩A⇘ℭ⦇Mcat⦈⇙
ℭ⦇Mα⦈⦇NTMap⦈⦇a ⊗⇩H⇩M⇩.⇩O⇘ℭ⦇Mcf⦈⇙ b, c, d⦈⇩∙"
and mcat_triangle[mcat_cs_simps]:
"⟦ a ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈; b ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈ ⟧ ⟹
(ℭ⦇Mcat⦈⦇CId⦈⦇a⦈ ⊗⇩H⇩M⇩.⇩A⇘ℭ⦇Mcf⦈⇙ ℭ⦇Ml⦈⦇NTMap⦈⦇b⦈) ∘⇩A⇘ℭ⦇Mcat⦈⇙
ℭ⦇Mα⦈⦇NTMap⦈⦇a, ℭ⦇Me⦈, b⦈⇩∙ =
(ℭ⦇Mr⦈⦇NTMap⦈⦇a⦈ ⊗⇩H⇩M⇩.⇩A⇘ℭ⦇Mcf⦈⇙ ℭ⦇Mcat⦈⦇CId⦈⦇b⦈)"

lemmas [mcat_cs_intros] = monoidal_category.mcat_Me_is_obj
lemmas [mcat_cs_simps] = monoidal_category.mcat_triangle

text‹Rules.›

lemma (in monoidal_category) monoidal_category_axioms'[mcat_cs_intros]:
assumes "α' = α"
shows "monoidal_category α' ℭ"
unfolding assms by (rule monoidal_category_axioms)

mk_ide rf monoidal_category_def[unfolded monoidal_category_axioms_def]
|intro monoidal_categoryI|
|dest monoidal_categoryD[dest]|
|elim monoidal_categoryE[elim]|

text‹Elementary properties.›

lemma mcat_eqI:
assumes "monoidal_category α 𝔄"
and "monoidal_category α 𝔅"
and "𝔄⦇Mcat⦈ = 𝔅⦇Mcat⦈"
and "𝔄⦇Mcf⦈ = 𝔅⦇Mcf⦈"
and "𝔄⦇Me⦈ = 𝔅⦇Me⦈"
and "𝔄⦇Mα⦈ = 𝔅⦇Mα⦈"
and "𝔄⦇Ml⦈ = 𝔅⦇Ml⦈"
and "𝔄⦇Mr⦈ = 𝔅⦇Mr⦈"
shows "𝔄 = 𝔅"
proof-
interpret 𝔄: monoidal_category α 𝔄 by (rule assms(1))
interpret 𝔅: monoidal_category α 𝔅 by (rule assms(2))
show ?thesis
proof(rule vsv_eqI)
have dom: "𝒟⇩∘ 𝔄 = 6⇩ℕ"
by (cs_concl cs_shallow cs_simp: mcat_cs_simps V_cs_simps)
show "𝒟⇩∘ 𝔄 = 𝒟⇩∘ 𝔅"
by (cs_concl cs_shallow cs_simp: mcat_cs_simps V_cs_simps)
show "a ∈⇩∘ 𝒟⇩∘ 𝔄 ⟹ 𝔄⦇a⦈ = 𝔅⦇a⦈" for a
by (unfold dom, elim_in_numeral, insert assms)
(auto simp: mcat_field_simps)
qed auto
qed

subsection‹Components for ‹Mα› for ‹Rel››

subsubsection‹Definition and elementary properties›

definition Mα_Rel_arrow_lr :: "V ⇒ V ⇒ V ⇒ V"
where "Mα_Rel_arrow_lr A B C =
[
(λab_c∈⇩∘(A ×⇩∘ B) ×⇩∘ C. ⟨vfst (vfst ab_c), ⟨vsnd (vfst ab_c), vsnd ab_c⟩⟩),
(A ×⇩∘ B) ×⇩∘ C,
A ×⇩∘ (B ×⇩∘ C)
]⇩∘"

definition Mα_Rel_arrow_rl :: "V ⇒ V ⇒ V ⇒ V"
where "Mα_Rel_arrow_rl A B C =
[
(λa_bc∈⇩∘A ×⇩∘ (B ×⇩∘ C). ⟨⟨vfst a_bc, vfst (vsnd a_bc)⟩, vsnd (vsnd a_bc)⟩),
A ×⇩∘ (B ×⇩∘ C),
(A ×⇩∘ B) ×⇩∘ C
]⇩∘"

text‹Components.›

lemma Mα_Rel_arrow_lr_components:
shows "Mα_Rel_arrow_lr A B C⦇ArrVal⦈ =
(λab_c∈⇩∘(A ×⇩∘ B) ×⇩∘ C. ⟨vfst (vfst ab_c), ⟨vsnd (vfst ab_c), vsnd ab_c⟩⟩)"
and [cat_cs_simps]: "Mα_Rel_arrow_lr A B C⦇ArrDom⦈ = (A ×⇩∘ B) ×⇩∘ C"
and [cat_cs_simps]: "Mα_Rel_arrow_lr A B C⦇ArrCod⦈ = A ×⇩∘ (B ×⇩∘ C)"
unfolding Mα_Rel_arrow_lr_def arr_field_simps by (simp_all add: nat_omega_simps)

lemma Mα_Rel_arrow_rl_components:
shows "Mα_Rel_arrow_rl A B C⦇ArrVal⦈ =
(λa_bc∈⇩∘A ×⇩∘ (B ×⇩∘ C). ⟨⟨vfst a_bc, vfst (vsnd a_bc)⟩, vsnd (vsnd a_bc)⟩)"
and [cat_cs_simps]: "Mα_Rel_arrow_rl A B C⦇ArrDom⦈ = A ×⇩∘ (B ×⇩∘ C)"
and [cat_cs_simps]: "Mα_Rel_arrow_rl A B C⦇ArrCod⦈ = (A ×⇩∘ B) ×⇩∘ C"
unfolding Mα_Rel_arrow_rl_def arr_field_simps by (simp_all add: nat_omega_simps)

subsubsection‹Arrow value›

mk_VLambda Mα_Rel_arrow_lr_components(1)
|vsv Mα_Rel_arrow_lr_ArrVal_vsv[cat_cs_intros]|
|vdomain Mα_Rel_arrow_lr_ArrVal_vdomain[cat_cs_simps]|
|app Mα_Rel_arrow_lr_ArrVal_app'|

lemma Mα_Rel_arrow_lr_ArrVal_app[cat_cs_simps]:
assumes "ab_c = ⟨⟨a, b⟩, c⟩" and "ab_c ∈⇩∘ (A ×⇩∘ B) ×⇩∘ C"
shows "Mα_Rel_arrow_lr A B C⦇ArrVal⦈⦇ab_c⦈ = ⟨a, ⟨b, c⟩⟩"
using assms(2)
unfolding assms(1)

mk_VLambda Mα_Rel_arrow_rl_components(1)
|vsv Mα_Rel_arrow_rl_ArrVal_vsv[cat_cs_intros]|
|vdomain Mα_Rel_arrow_rl_ArrVal_vdomain[cat_cs_simps]|
|app Mα_Rel_arrow_rl_ArrVal_app'|

lemma Mα_Rel_arrow_rl_ArrVal_app[cat_cs_simps]:
assumes "a_bc = ⟨a, ⟨b, c⟩⟩" and "a_bc ∈⇩∘ A ×⇩∘ (B ×⇩∘ C)"
shows "Mα_Rel_arrow_rl A B C⦇ArrVal⦈⦇a_bc⦈ = ⟨⟨a, b⟩, c⟩"
using assms(2)
unfolding assms(1)

subsubsection‹Components for ‹Mα› for ‹Rel› are arrows›

lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Set_arr_Vset:
assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "C ∈⇩∘ Vset α"
shows "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
proof(intro cat_Set_is_arrI arr_SetI)
show "vfsequence (Mα_Rel_arrow_lr A B C)" unfolding Mα_Rel_arrow_lr_def by auto
show "vcard (Mα_Rel_arrow_lr A B C) = 3⇩ℕ"
unfolding Mα_Rel_arrow_lr_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (Mα_Rel_arrow_lr A B C⦇ArrVal⦈) ⊆⇩∘ Mα_Rel_arrow_lr A B C⦇ArrCod⦈"
unfolding Mα_Rel_arrow_lr_components by auto
qed
(
use assms in
‹
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros
›
)+

lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Set_arr_Vset:
assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "C ∈⇩∘ Vset α"
shows "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof(intro cat_Set_is_arrI arr_SetI)
show "vfsequence (Mα_Rel_arrow_rl A B C)" unfolding Mα_Rel_arrow_rl_def by auto
show "vcard (Mα_Rel_arrow_rl A B C) = 3⇩ℕ"
unfolding Mα_Rel_arrow_rl_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (Mα_Rel_arrow_rl A B C⦇ArrVal⦈) ⊆⇩∘ Mα_Rel_arrow_rl A B C⦇ArrCod⦈"
unfolding Mα_Rel_arrow_rl_components by auto
qed
(
use assms in
‹
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros
›
)+

lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Set_arr:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
shows "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
using assms
unfolding cat_Set_components
by (rule Mα_Rel_arrow_lr_is_cat_Set_arr_Vset)

lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Set_arr'[cat_rel_par_Set_cs_intros]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Set α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_lr_is_cat_Set_arr)

lemmas [cat_rel_par_Set_cs_intros] = 𝒵.Mα_Rel_arrow_lr_is_cat_Set_arr'

lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Set_arr:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
shows "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
using assms
unfolding cat_Set_components
by (rule Mα_Rel_arrow_rl_is_cat_Set_arr_Vset)

lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Set_arr'[cat_rel_par_Set_cs_intros]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Set α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_rl_is_cat_Set_arr)

lemmas [cat_rel_par_Set_cs_intros] = 𝒵.Mα_Rel_arrow_rl_is_cat_Set_arr'

lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Par_arr:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
shows "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Par α⇙ A ×⇩∘ (B ×⇩∘ C)"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
from assms show ?thesis
unfolding cat_Par_components(1)
by (intro Set_Par.subcat_is_arrD Mα_Rel_arrow_lr_is_cat_Set_arr_Vset) auto
qed

lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Par_arr'[cat_rel_Par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Par α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_lr_is_cat_Par_arr)

lemmas [cat_rel_Par_set_cs_intros] = 𝒵.Mα_Rel_arrow_lr_is_cat_Par_arr'

lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Par_arr:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
shows "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Par α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
from assms show ?thesis
unfolding cat_Par_components(1)
by (intro Set_Par.subcat_is_arrD Mα_Rel_arrow_rl_is_cat_Set_arr_Vset) auto
qed

lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Par_arr'[cat_rel_Par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Par α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_rl_is_cat_Par_arr)

lemmas [cat_rel_Par_set_cs_intros] = 𝒵.Mα_Rel_arrow_rl_is_cat_Par_arr'

lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Rel_arr:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
shows "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Rel α⇙ A ×⇩∘ (B ×⇩∘ C)"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
interpret Par_Rel: wide_replete_subcategory α ‹cat_Par α› ‹cat_Rel α›
by (rule wide_replete_subcategory_cat_Par_cat_Rel)
interpret Set_Rel: subcategory α ‹cat_Set α› ‹cat_Rel α›
by
(
rule subcat_trans[
OF Set_Par.subcategory_axioms Par_Rel.subcategory_axioms
]
)
from assms show ?thesis
unfolding cat_Rel_components(1)
by (intro Set_Rel.subcat_is_arrD Mα_Rel_arrow_lr_is_cat_Set_arr_Vset) auto
qed

lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Rel_arr'[cat_Rel_par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Rel α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_lr_is_cat_Rel_arr)

lemmas [cat_Rel_par_set_cs_intros] = 𝒵.Mα_Rel_arrow_lr_is_cat_Rel_arr'

lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Rel_arr:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
shows "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Rel α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
interpret Par_Rel: wide_replete_subcategory α ‹cat_Par α› ‹cat_Rel α›
by (rule wide_replete_subcategory_cat_Par_cat_Rel)
interpret Set_Rel: subcategory α ‹cat_Set α› ‹cat_Rel α›
by
(
rule subcat_trans[
OF Set_Par.subcategory_axioms Par_Rel.subcategory_axioms
]
)
from assms show ?thesis
unfolding cat_Rel_components(1)
by (intro Set_Rel.subcat_is_arrD Mα_Rel_arrow_rl_is_cat_Set_arr_Vset) auto
qed

lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Rel_arr'[cat_Rel_par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Rel α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_rl_is_cat_Rel_arr)

lemmas [cat_Rel_par_set_cs_intros] = 𝒵.Mα_Rel_arrow_rl_is_cat_Rel_arr'

subsubsection‹Further properties›

lemma (in 𝒵) Mα_Rel_arrow_rl_Mα_Rel_arrow_lr[cat_cs_simps]:
assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "C ∈⇩∘ Vset α"
shows
"Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C =
cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈"
proof-
interpret Set: category α ‹cat_Set α›
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms have lhs:
"Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C :
(A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
by
(
cs_concl cs_shallow
cs_simp: cat_Set_components(1)
cs_intro: cat_rel_par_Set_cs_intros cat_cs_intros
)
then have dom_lhs:
"𝒟⇩∘ ((Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C)⦇ArrVal⦈) =
(A ×⇩∘ B) ×⇩∘ C"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from assms Set.category_axioms have rhs:
"cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈ :
(A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
by
(
cs_concl
cs_simp: cat_Set_components(1) cs_intro: V_cs_intros cat_cs_intros
)
then have dom_rhs:
"𝒟⇩∘ ((cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈)⦇ArrVal⦈) = (A ×⇩∘ B) ×⇩∘ C"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show ?thesis
proof(rule arr_Set_eqI)
from lhs show arr_Set_lhs:
"arr_Set α (Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C)"
by (auto dest: cat_Set_is_arrD(1))
from rhs show arr_Set_rhs: "arr_Set α (cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈)"
by (auto dest: cat_Set_is_arrD(1))
show
"(Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C)⦇ArrVal⦈ =
cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix ab_c assume prems: "ab_c ∈⇩∘ (A ×⇩∘ B) ×⇩∘ C"
then obtain a b c
where ab_c_def: "ab_c = ⟨⟨a, b⟩, c⟩"
and a: "a ∈⇩∘ A"
and b: "b ∈⇩∘ B"
and c: "c ∈⇩∘ C"
by clarsimp
from assms prems a b c lhs rhs show
"(Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C)⦇ArrVal⦈⦇ab_c⦈ =
cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈⦇ArrVal⦈⦇ab_c⦈"
unfolding ab_c_def
by
(
cs_concl
cs_simp: cat_Set_components(1) cat_cs_simps
cs_intro: cat_rel_par_Set_cs_intros V_cs_intros cat_cs_intros
)
qed (use arr_Set_lhs arr_Set_rhs in auto)
qed (use lhs rhs in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed

lemma (in 𝒵) Mα_Rel_arrow_rl_Mα_Rel_arrow_lr'[cat_cs_simps]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
shows
"Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C =
cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈"
using assms
unfolding cat_Set_components(1)
by (rule Mα_Rel_arrow_rl_Mα_Rel_arrow_lr)

lemmas [cat_cs_simps] = 𝒵.Mα_Rel_arrow_rl_Mα_Rel_arrow_lr'

lemma (in 𝒵) Mα_Rel_arrow_lr_Mα_Rel_arrow_rl[cat_cs_simps]:
assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "C ∈⇩∘ Vset α"
shows
"Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C =
cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈"
proof-
interpret Set: category α ‹cat_Set α›
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms have lhs:
"Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C :
A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
by
(
cs_concl cs_shallow
cs_simp: cat_Set_components(1)
cs_intro: cat_rel_par_Set_cs_intros cat_cs_intros
)
then have dom_lhs:
"𝒟⇩∘ ((Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C)⦇ArrVal⦈) =
A ×⇩∘ (B ×⇩∘ C)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from assms Set.category_axioms have rhs:
"cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈ :
A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
by
(
cs_concl
cs_simp: cat_Set_components(1) cs_intro: V_cs_intros cat_cs_intros
)
then have dom_rhs:
"𝒟⇩∘ ((cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈)⦇ArrVal⦈) = A ×⇩∘ (B ×⇩∘ C)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show ?thesis
proof(rule arr_Set_eqI)
from lhs show arr_Set_lhs:
"arr_Set α (Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C)"
by (auto dest: cat_Set_is_arrD(1))
from rhs show arr_Set_rhs: "arr_Set α (cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈)"
by (auto dest: cat_Set_is_arrD(1))
show
"(Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C)⦇ArrVal⦈ =
cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a_bc assume prems: "a_bc ∈⇩∘ A ×⇩∘ (B ×⇩∘ C)"
then obtain a b c
where a_bc_def: "a_bc = ⟨a, ⟨b, c⟩⟩"
and a: "a ∈⇩∘ A"
and b: "b ∈⇩∘ B"
and c: "c ∈⇩∘ C"
by clarsimp
from assms prems a b c lhs rhs show
"(Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C)⦇ArrVal⦈⦇a_bc⦈ =
cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈⦇ArrVal⦈⦇a_bc⦈"
unfolding a_bc_def
by
(
cs_concl
cs_simp: cat_Set_components(1) cat_cs_simps
cs_intro: V_cs_intros cat_rel_par_Set_cs_intros cat_cs_intros
)
qed (use arr_Set_lhs arr_Set_rhs in auto)
qed (use lhs rhs in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed

lemma (in 𝒵) Mα_Rel_arrow_lr_Mα_Rel_arrow_rl'[cat_cs_simps]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
shows
"Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C =
cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈"
using assms
unfolding cat_Set_components(1)
by (rule Mα_Rel_arrow_lr_Mα_Rel_arrow_rl)

lemmas [cat_cs_simps] = 𝒵.Mα_Rel_arrow_lr_Mα_Rel_arrow_rl'

subsubsection‹Components for ‹Mα› for ‹Rel› are isomorphisms›

lemma (in 𝒵)
assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "C ∈⇩∘ Vset α"
shows Mα_Rel_arrow_lr_is_cat_Set_iso_arr_Vset:
"Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
and Mα_Rel_arrow_rl_is_cat_Set_iso_arr_Vset:
"Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof-
interpret Set: category α ‹cat_Set α›
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
have lhs: "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
by (intro Mα_Rel_arrow_rl_is_cat_Set_arr_Vset assms)
from assms have [cat_cs_simps]:
"Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C =
cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_Set_components(1) cat_cs_simps cs_intro: cat_cs_intros
)
from assms have [cat_cs_simps]:
"Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C =
cat_Set α⦇CId⦈⦇A ×⇩∘ B ×⇩∘ C⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_Set_components(1) cat_cs_simps cs_intro: cat_cs_intros
)
from
Set.is_iso_arrI'
[
OF lhs Mα_Rel_arrow_lr_is_cat_Set_arr_Vset[OF assms],
unfolded cat_cs_simps,
simplified
]
show "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
and "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
by auto
qed

lemma (in 𝒵)
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
shows Mα_Rel_arrow_lr_is_cat_Set_iso_arr:
"Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
and Mα_Rel_arrow_rl_is_cat_Set_iso_arr:
"Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
using assms
unfolding cat_Set_components(1)
by
(
all
‹
intro
Mα_Rel_arrow_lr_is_cat_Set_iso_arr_Vset
Mα_Rel_arrow_rl_is_cat_Set_iso_arr_Vset
›
)

lemma (in 𝒵)
Mα_Rel_arrow_lr_is_cat_Set_iso_arr'[cat_rel_par_Set_cs_intros]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Set α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_lr_is_cat_Set_iso_arr)

lemmas [cat_rel_par_Set_cs_intros] =
𝒵.Mα_Rel_arrow_lr_is_cat_Set_iso_arr'

lemma (in 𝒵)
Mα_Rel_arrow_rl_is_cat_Set_iso_arr'[cat_rel_par_Set_cs_intros]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Set α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_rl_is_cat_Set_iso_arr)

lemmas [cat_rel_par_Set_cs_intros] =
𝒵.Mα_Rel_arrow_rl_is_cat_Set_iso_arr'

lemma (in 𝒵)
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
shows Mα_Rel_arrow_lr_is_cat_Par_iso_arr:
"Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Par α⇙ A ×⇩∘ (B ×⇩∘ C)"
and Mα_Rel_arrow_rl_is_cat_Par_iso_arr:
"Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Par α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
show "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Par α⇙ A ×⇩∘ (B ×⇩∘ C)"
by
(
rule Set_Par.wr_subcat_is_iso_arr_is_iso_arr
[
THEN iffD1,
OF Mα_Rel_arrow_lr_is_cat_Set_iso_arr_Vset[
OF assms[unfolded cat_Par_components]
]
]
)
show "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Par α⇙ (A ×⇩∘ B) ×⇩∘ C"
by
(
rule Set_Par.wr_subcat_is_iso_arr_is_iso_arr
[
THEN iffD1,
OF Mα_Rel_arrow_rl_is_cat_Set_iso_arr_Vset[
OF assms[unfolded cat_Par_components]
]
]
)
qed

lemma (in 𝒵)
Mα_Rel_arrow_lr_is_cat_Par_iso_arr'[cat_rel_Par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Par α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_lr_is_cat_Par_iso_arr)

lemmas [cat_rel_Par_set_cs_intros] =
𝒵.Mα_Rel_arrow_lr_is_cat_Par_iso_arr'

lemma (in 𝒵)
Mα_Rel_arrow_rl_is_cat_Par_iso_arr'[cat_rel_Par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Par α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_rl_is_cat_Par_iso_arr)

lemmas [cat_rel_Par_set_cs_intros] =
𝒵.Mα_Rel_arrow_rl_is_cat_Par_iso_arr'

lemma (in 𝒵)
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
shows Mα_Rel_arrow_lr_is_cat_Rel_iso_arr:
"Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Rel α⇙ A ×⇩∘ (B ×⇩∘ C)"
and Mα_Rel_arrow_rl_is_cat_Rel_iso_arr:
"Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Rel α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
interpret Par_Rel: wide_replete_subcategory α ‹cat_Par α› ‹cat_Rel α›
by (rule wide_replete_subcategory_cat_Par_cat_Rel)
interpret Set_Rel: wide_replete_subcategory α ‹cat_Set α› ‹cat_Rel α›
by
(
rule wr_subcat_trans
[
OF
Set_Par.wide_replete_subcategory_axioms
Par_Rel.wide_replete_subcategory_axioms
]
)
show "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Rel α⇙ A ×⇩∘ (B ×⇩∘ C)"
by
(
rule Set_Rel.wr_subcat_is_iso_arr_is_iso_arr
[
THEN iffD1,
OF Mα_Rel_arrow_lr_is_cat_Set_iso_arr_Vset[
OF assms[unfolded cat_Rel_components]
]
]
)
show "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Rel α⇙ (A ×⇩∘ B) ×⇩∘ C"
by
(
rule Set_Rel.wr_subcat_is_iso_arr_is_iso_arr
[
THEN iffD1,
OF Mα_Rel_arrow_rl_is_cat_Set_iso_arr_Vset[
OF assms[unfolded cat_Rel_components]
]
]
)
qed

lemma (in 𝒵)
Mα_Rel_arrow_lr_is_cat_Rel_iso_arr'[cat_Rel_par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Rel α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_lr_is_cat_Rel_iso_arr)

lemmas [cat_Rel_par_set_cs_intros] =
𝒵.Mα_Rel_arrow_lr_is_cat_Rel_iso_arr'

lemma (in 𝒵)
Mα_Rel_arrow_rl_is_cat_Rel_iso_arr'[cat_Rel_par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Rel α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_rl_is_cat_Rel_iso_arr)

lemmas [cat_Rel_par_set_cs_intros] =
𝒵.Mα_Rel_arrow_rl_is_cat_Rel_iso_arr'

subsection‹‹Mα› for ‹Rel››

subsubsection‹Definition and elementary properties›

definition Mα_Rel :: "V ⇒ V"
where "Mα_Rel ℭ =
[
(λabc∈⇩∘(ℭ^⇩C⇩3)⦇Obj⦈. Mα_Rel_arrow_lr (abc⦇0⦈) (abc⦇1⇩ℕ⦈) (abc⦇2⇩ℕ⦈)),
cf_blcomp (cf_prod_2_Rel ℭ),
cf_brcomp (cf_prod_2_Rel ℭ),
ℭ^⇩C⇩3,
ℭ
]⇩∘"

text‹Components.›

lemma Mα_Rel_components:
shows "Mα_Rel ℭ⦇NTMap⦈ =
(λabc∈⇩∘(ℭ^⇩C⇩3)⦇Obj⦈. Mα_Rel_arrow_lr (abc⦇0⦈) (abc⦇1⇩ℕ⦈) (abc⦇2⇩ℕ⦈))"
and [cat_cs_simps]: "Mα_Rel ℭ⦇NTDom⦈ = cf_blcomp (cf_prod_2_Rel ℭ)"
and [cat_cs_simps]: "Mα_Rel ℭ⦇NTCod⦈ = cf_brcomp (cf_prod_2_Rel ℭ)"
and [cat_cs_simps]: "Mα_Rel ℭ⦇NTDGDom⦈ = ℭ^⇩C⇩3"
and [cat_cs_simps]: "Mα_Rel ℭ⦇NTDGCod⦈ = ℭ"
unfolding Mα_Rel_def nt_field_simps by (simp_all add: nat_omega_simps)

subsubsection‹Natural transformation map›

mk_VLambda Mα_Rel_components(1)
|vsv Mα_Rel_NTMap_vsv[cat_cs_intros]|
|vdomain Mα_Rel_NTMap_vdomain[cat_cs_simps]|
|app Mα_Rel_NTMap_app'|

lemma Mα_Rel_NTMap_app[cat_cs_simps]:
assumes "ABC = [A, B, C]⇩∘" and "ABC ∈⇩∘ (ℭ^⇩C⇩3)⦇Obj⦈"
shows "Mα_Rel ℭ⦇NTMap⦈⦇ABC⦈ = Mα_Rel_arrow_lr A B C"
using assms(2)
unfolding assms(1)

subsubsection‹‹Mα› for ‹Rel› is a natural isomorphism›

lemma (in 𝒵) Mα_Rel_is_iso_ntcf:
"Mα_Rel (cat_Rel α) :
cf_blcomp (cf_prod_2_Rel (cat_Rel α)) ↦⇩C⇩F⇩.⇩i⇩s⇩o
cf_brcomp (cf_prod_2_Rel (cat_Rel α)) :
cat_Rel α^⇩C⇩3 ↦↦⇩C⇘α⇙ cat_Rel α"
proof-

interpret cf_prod: is_functor
α ‹cat_Rel α ×⇩C cat_Rel α› ‹cat_Rel α› ‹cf_prod_2_Rel (cat_Rel α)›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Rel_cs_intros)

show ?thesis
proof(intro is_iso_ntcfI is_ntcfI')

show "vfsequence (Mα_Rel (cat_Rel α))" unfolding Mα_Rel_def by auto
show "vcard (Mα_Rel (cat_Rel α)) = 5⇩ℕ"
unfolding Mα_Rel_def by (simp add: nat_omega_simps)

show "Mα_Rel (cat_Rel α)⦇NTMap⦈⦇ABC⦈ :
cf_blcomp (cf_prod_2_Rel (cat_Rel α))⦇ObjMap⦈⦇ABC⦈ ↦⇩i⇩s⇩o⇘cat_Rel α⇙
cf_brcomp (cf_prod_2_Rel (cat_Rel α))⦇ObjMap⦈⦇ABC⦈"
if "ABC ∈⇩∘ (cat_Rel α^⇩C⇩3)⦇Obj⦈" for ABC
proof-
from that category_cat_Rel obtain A B C
where ABC_def: "ABC = [A, B, C]⇩∘"
and A: "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and B: "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and C: "C ∈⇩∘ cat_Rel α⦇Obj⦈"
by (elim cat_prod_3_ObjE[rotated 3])
from that A B C show ?thesis
unfolding ABC_def
by
(
cs_concl cs_shallow
cs_intro:
cat_cs_intros cat_Rel_par_set_cs_intros cat_prod_cs_intros
cs_simp: cat_cs_simps cat_Rel_cs_simps
)
qed
then show "Mα_Rel (cat_Rel α)⦇NTMap⦈⦇ABC⦈ :
cf_blcomp (cf_prod_2_Rel (cat_Rel α))⦇ObjMap⦈⦇ABC⦈ ↦⇘cat_Rel α⇙
cf_brcomp (cf_prod_2_Rel (cat_Rel α))⦇ObjMap⦈⦇ABC⦈"
if "ABC ∈⇩∘ (cat_Rel α^⇩C⇩3)⦇Obj⦈" for ABC
using that by (simp add: cat_Rel_is_iso_arrD(1))
show
"Mα_Rel (cat_Rel α)⦇NTMap⦈⦇ABC'⦈ ∘⇩A⇘cat_Rel α⇙
cf_blcomp (cf_prod_2_Rel (cat_Rel α))⦇ArrMap⦈⦇HGF⦈ =
cf_brcomp (cf_prod_2_Rel (cat_Rel α))⦇ArrMap⦈⦇HGF⦈ ∘⇩A⇘cat_Rel α⇙
Mα_Rel (cat_Rel α)⦇NTMap⦈⦇ABC⦈"
if "HGF : ABC ↦⇘cat_Rel α^⇩C⇩3⇙ ABC'" for ABC ABC' HGF
proof-

from that obtain H G F A B C A' B' C'
where HGF_def: "HGF = [H, G, F]⇩∘"
and ABC_def: "ABC = [A, B, C]⇩∘"
and ABC'_def: "ABC' = [A', B', C']⇩∘"
and H_is_arr: "H : A ↦⇘cat_Rel α⇙ A'"
and G_is_arr: "G : B ↦⇘cat_Rel α⇙ B'"
and F_is_arr: "F : C ↦⇘cat_Rel α⇙ C'"
by
(
elim cat_prod_3_is_arrE[
OF category_cat_Rel category_cat_Rel category_cat_Rel
]
)

note H = cat_Rel_is_arrD[OF H_is_arr]
note G = cat_Rel_is_arrD[OF G_is_arr]
note F = cat_Rel_is_arrD[OF F_is_arr]

interpret H: arr_Rel α H
rewrites "H⦇ArrDom⦈ = A" and "H⦇ArrCod⦈ = A'"
by (intro H)+
interpret G: arr_Rel α G
rewrites "G⦇ArrDom⦈ = B" and "G⦇ArrCod⦈ = B'"
by (intro G)+
interpret F: arr_Rel α F
rewrites "F⦇ArrDom⦈ = C" and "F⦇ArrCod⦈ = C'"
by (intro F)+

let ?ABC' = ‹Mα_Rel_arrow_lr A' B' C'›
and ?ABC = ‹Mα_Rel_arrow_lr A B C›
and ?HG_F =
‹
prod_2_Rel_ArrVal
(prod_2_Rel_ArrVal (H⦇ArrVal⦈) (G⦇ArrVal⦈))
(F⦇ArrVal⦈)
›
and ?H_GF =
‹
prod_2_Rel_ArrVal
(H⦇ArrVal⦈)
(prod_2_Rel_ArrVal (G⦇ArrVal⦈) (F⦇ArrVal⦈))
›

have [cat_cs_simps]:
"?ABC' ∘⇩A⇘cat_Rel α⇙ (H ⇩A×⇩R⇩e⇩l G) ⇩A×⇩R⇩e⇩l  F =
H ⇩A×⇩R⇩e⇩l (G ⇩A×⇩R⇩e⇩l F) ∘⇩A⇘cat_Rel α⇙ ?ABC"
proof-

from H_is_arr G_is_arr F_is_arr have lhs:
"?ABC' ∘⇩A⇘cat_Rel α⇙ (H ⇩A×⇩R⇩e⇩l G) ⇩A×⇩R⇩e⇩l F :
(A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Rel α⇙ A' ×⇩∘ (B' ×⇩∘ C')"
by
(
cs_concl cs_shallow
cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros
)
from H_is_arr G_is_arr F_is_arr have rhs:
"H ⇩A×⇩R⇩e⇩l (G ⇩A×⇩R⇩e⇩l F) ∘⇩A⇘cat_Rel α⇙ ?ABC :
(A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Rel α⇙ A' ×⇩∘ (B' ×⇩∘ C')"
by (cs_concl cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros)

show ?thesis
proof(rule arr_Rel_eqI)

from lhs show arr_Rel_lhs:
"arr_Rel α (?ABC' ∘⇩A⇘cat_Rel α⇙ (H ⇩A×⇩R⇩e⇩l G) ⇩A×⇩R⇩e⇩l F)"
by (auto dest: cat_Rel_is_arrD)
from rhs show arr_Rel_rhs:
"arr_Rel α (H ⇩A×⇩R⇩e⇩l (G ⇩A×⇩R⇩e⇩l F) ∘⇩A⇘cat_Rel α⇙ ?ABC)"
by (auto dest: cat_Rel_is_arrD)

have [cat_cs_simps]: "?ABC'⦇ArrVal⦈ ∘⇩∘ ?HG_F = ?H_GF ∘⇩∘ ?ABC⦇ArrVal⦈"
proof(intro vsubset_antisym vsubsetI)
fix abc_abc'' assume prems: "abc_abc'' ∈⇩∘ ?ABC'⦇ArrVal⦈ ∘⇩∘ ?HG_F"
then obtain abc abc' abc''
where abc_abc''_def: "abc_abc'' = ⟨abc, abc''⟩"
and abc_abc': "⟨abc, abc'⟩ ∈⇩∘ ?HG_F"
and abc'_abc'': "⟨abc', abc''⟩ ∈⇩∘ ?ABC'⦇ArrVal⦈"
by (elim vcompE)
from abc_abc' obtain ab c ab' c'
where abc_abc'_def: "⟨abc, abc'⟩ = ⟨⟨ab, c⟩, ⟨ab', c'⟩⟩"
and ab_ab':
"⟨ab, ab'⟩ ∈⇩∘ prod_2_Rel_ArrVal (H⦇ArrVal⦈) (G⦇ArrVal⦈)"
and cc': "⟨c, c'⟩ ∈⇩∘ F⦇ArrVal⦈"
by (meson prod_2_Rel_ArrValE)
then have abc_def: "abc = ⟨ab, c⟩" and abc'_def: "abc' = ⟨ab', c'⟩"
by auto
from ab_ab' obtain a b a' b'
where ab_ab'_def: "⟨ab, ab'⟩ = ⟨⟨a, b⟩, ⟨a', b'⟩⟩"
and aa': "⟨a, a'⟩ ∈⇩∘ H⦇ArrVal⦈"
and bb': "⟨b, b'⟩ ∈⇩∘ G⦇ArrVal⦈"
by auto
then have ab_def: "ab = ⟨a, b⟩" and ab'_def: "ab' = ⟨a', b'⟩"
by auto
from cc' F.arr_Rel_ArrVal_vdomain F.arr_Rel_ArrVal_vrange
have c: "c ∈⇩∘ C" and c': "c' ∈⇩∘ C'"
by auto
from bb' G.arr_Rel_ArrVal_vdomain G.arr_Rel_ArrVal_vrange
have b: "b ∈⇩∘ B" and b': "b' ∈⇩∘ B'"
by auto
from aa' H.arr_Rel_ArrVal_vdomain H.arr_Rel_ArrVal_vrange
have a: "a ∈⇩∘ A" and a': "a' ∈⇩∘ A'"
by auto
from abc'_abc'' have "abc'' = ?ABC'⦇ArrVal⦈⦇abc'⦈"
also from a' b' c' have "… = ⟨a', ⟨b', c'⟩⟩"
unfolding abc'_def ab'_def
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: V_cs_intros)
finally have abc''_def: "abc'' = ⟨a', ⟨b', c'⟩⟩" by auto
from aa' bb' cc' a a' b b' c c' show
"abc_abc'' ∈⇩∘ ?H_GF ∘⇩∘ ?ABC⦇ArrVal⦈"
unfolding abc_abc''_def abc_def abc'_def abc''_def ab'_def ab_def
by (intro vcompI prod_2_Rel_ArrValI)
(
cs_concl cs_shallow
cs_simp: cat_cs_simps
cs_intro:
vsv.vsv_ex1_app2[THEN iffD1]
V_cs_intros
cat_cs_intros
cat_Rel_cs_intros
)+
next
fix abc_abc'' assume prems: "abc_abc'' ∈⇩∘ ?H_GF ∘⇩∘ ?ABC⦇ArrVal⦈"
then obtain abc abc' abc''
where abc_abc''_def: "abc_abc'' = ⟨abc, abc''⟩"
and abc_abc': "⟨abc, abc'⟩ ∈⇩∘ ?ABC⦇ArrVal⦈"
and abc'_abc'': "⟨abc', abc''⟩ ∈⇩∘ ?H_GF"
by (elim vcompE)
from abc'_abc'' obtain a' bc' a'' bc''
where abc'_abc''_def: "⟨abc', abc''⟩ = ⟨⟨a', bc'⟩, ⟨a'', bc''⟩⟩"
and aa'': "⟨a', a''⟩ ∈⇩∘ H⦇ArrVal⦈"
and bc'_bc'':
"⟨bc', bc''⟩ ∈⇩∘ prod_2_Rel_ArrVal (G⦇ArrVal⦈) (F⦇ArrVal⦈)"
by (meson prod_2_Rel_ArrValE)
then have abc'_def: "abc' = ⟨a', bc'⟩"
and abc''_def: "abc'' = ⟨a'', bc''⟩"
by auto
from bc'_bc'' obtain b' c' b'' c''
where bc'_bc''_def: "⟨bc', bc''⟩ = ⟨⟨b', c'⟩, ⟨b'', c''⟩⟩"
and bb'': "⟨b', b''⟩ ∈⇩∘ G⦇ArrVal⦈"
and cc'': "⟨c', c''⟩ ∈⇩∘ F⦇ArrVal⦈"
by auto
then have bc'_def: "bc' = ⟨b', c'⟩"
and bc''_def: "bc'' = ⟨b'', c''⟩"
by auto
from cc'' F.arr_Rel_ArrVal_vdomain F.arr_Rel_ArrVal_vrange
have c': "c' ∈⇩∘ C" and c'': "c'' ∈⇩∘ C'"
by auto
from bb'' G.arr_Rel_ArrVal_vdomain G.arr_Rel_ArrVal_vrange
have b': "b' ∈⇩∘ B" and b'': "b'' ∈⇩∘ B'"
by auto
from aa'' H.arr_Rel_ArrVal_vdomain H.arr_Rel_ArrVal_vrange
have a': "a' ∈⇩∘ A" and a'': "a'' ∈⇩∘ A'"
by auto
from abc_abc' have "abc ∈⇩∘ 𝒟⇩∘ (?ABC⦇ArrVal⦈)" by auto
then have "abc ∈⇩∘ (A ×⇩∘ B) ×⇩∘ C" by (simp add: cat_cs_simps)
then obtain a b c
where abc_def: "abc = ⟨⟨a, b⟩, c⟩"
and a: "a ∈⇩∘ A"
and b: "b ∈⇩∘ B"
and c: "c ∈⇩∘ C"
by auto
from abc_abc' have "abc' = ?ABC⦇ArrVal⦈⦇abc⦈"
also from a b c have "… = ⟨a, ⟨b, c⟩⟩"
unfolding abc_def bc'_def
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: V_cs_intros)
finally have abc'_def': "abc' = ⟨a, ⟨b, c⟩⟩" by auto
with abc'_def[unfolded bc'_def] have [cat_cs_simps]:
"a = a'" "b = b'" "c = c'"
by auto
from a'' b'' c'' have "⟨⟨a'', b''⟩, c''⟩ ∈⇩∘ (A' ×⇩∘ B') ×⇩∘ C'"
by (cs_concl cs_shallow cs_intro: V_cs_intros)
with aa'' bb'' cc'' a a' b b' c c' show
"abc_abc'' ∈⇩∘ ?ABC'⦇ArrVal⦈ ∘⇩∘ ?HG_F"
unfolding abc_abc''_def abc_def abc'_def abc''_def bc''_def
by (intro vcompI prod_2_Rel_ArrValI)
(
cs_concl cs_shallow
cs_simp: cat_cs_simps
cs_intro:
vsv.vsv_ex1_app2[THEN iffD1]
V_cs_intros cat_cs_intros cat_Rel_cs_intros
)+
qed

from that H_is_arr G_is_arr F_is_arr show
"(?ABC' ∘⇩A⇘cat_Rel α⇙ (H ⇩A×⇩R⇩e⇩l G) ⇩A×⇩R⇩e⇩l F)⦇ArrVal⦈ =
(H ⇩A×⇩R⇩e⇩l (G ⇩A×⇩R⇩e⇩l F) ∘⇩A⇘cat_Rel α⇙ ?ABC)⦇ArrVal⦈"
by
(
cs_concl
cs_simp:
prod_2_Rel_components comp_Rel_components
cat_Rel_cs_simps cat_cs_simps
cs_intro:
cat_Rel_par_set_cs_intros cat_cs_intros cat_prod_cs_intros
)

qed (use lhs rhs in ‹cs_concl cs_simp: cat_cs_simps›)+

qed

from that H_is_arr G_is_arr F_is_arr show ?thesis
unfolding HGF_def ABC_def ABC'_def
by
(
cs_concl
cs_intro:
cat_Rel_par_set_cs_intros cat_cs_intros cat_prod_cs_intros
cs_simp: cat_Rel_cs_simps cat_cs_simps
)

qed

qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+

qed

lemma (in 𝒵) Mα_Rel_is_iso_ntcf'[cat_cs_intros]:
assumes "𝔉' = cf_blcomp (cf_prod_2_Rel (cat_Rel α))"
and "𝔊' = cf_brcomp (cf_prod_2_Rel (cat_Rel α))"
and "𝔄' = cat_Rel α^⇩C⇩3"
and "𝔅' = cat_Rel α"
and "α' = α"
shows "Mα_Rel (cat_Rel α) : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
unfolding assms by (rule Mα_Rel_is_iso_ntcf)

lemmas [cat_cs_intros] = 𝒵.Mα_Rel_is_iso_ntcf'

subsection‹‹Ml› and ‹Mr› for ‹Rel››

subsubsection‹Definition and elementary properties›

definition Ml_Rel :: "V ⇒ V ⇒ V"
where "Ml_Rel ℭ a =
[
(λB∈⇩∘ℭ⦇Obj⦈. vsnd_arrow (set {a}) B),
cf_prod_2_Rel ℭ⇘ℭ,ℭ⇙(set {a},-)⇩C⇩F,
cf_id ℭ,
ℭ,
ℭ
]⇩∘"

definition Mr_Rel :: "V ⇒ V ⇒ V"
where "Mr_Rel ℭ b =
[
(λA∈⇩∘ℭ⦇Obj⦈. vfst_arrow A (set {b})),
cf_prod_2_Rel ℭ⇘ℭ,ℭ⇙(-,set {b})⇩C⇩F,
cf_id ℭ,
ℭ,
ℭ
]⇩∘"

text‹Components.›

lemma Ml_Rel_components:
shows "Ml_Rel ℭ a⦇NTMap⦈ = (λB∈⇩∘ℭ⦇Obj⦈. vsnd_arrow (set {a}) B)"
and [cat_cs_simps]: "Ml_Rel ℭ a⦇NTDom⦈ = cf_prod_2_Rel ℭ⇘ℭ,ℭ⇙(set {a},-)⇩C⇩F"
and [cat_cs_simps]: "Ml_Rel ℭ a⦇NTCod⦈ = cf_id ℭ"
and [cat_cs_simps]: "Ml_Rel ℭ a⦇NTDGDom⦈ = ℭ"
and [cat_cs_simps]: "Ml_Rel ℭ a⦇NTDGCod⦈ = ℭ"
unfolding Ml_Rel_def nt_field_simps by (simp_all add: nat_omega_simps)

lemma Mr_Rel_components:
shows "Mr_Rel ℭ b⦇NTMap⦈ = (λA∈⇩∘ℭ⦇Obj⦈. vfst_arrow A (set {b}))"
and [cat_cs_simps]: "Mr_Rel ℭ b⦇NTDom⦈ = cf_prod_2_Rel ℭ⇘ℭ,ℭ⇙(-,set {b})⇩C⇩F"
and [cat_cs_simps]: "Mr_Rel ℭ b⦇NTCod⦈ = cf_id ℭ"
and [cat_cs_simps]: "Mr_Rel ℭ b⦇NTDGDom⦈ = ℭ"
and [cat_cs_simps]: "Mr_Rel ℭ b⦇NTDGCod⦈ = ℭ"
unfolding Mr_Rel_def nt_field_simps by (simp_all add: nat_omega_simps)

subsubsection‹Natural transformation map›

mk_VLambda Ml_Rel_components(1)
|vsv Ml_Rel_components_NTMap_vsv[cat_cs_intros]|
|vdomain Ml_Rel_components_NTMap_vdomain[cat_cs_simps]|
|app Ml_Rel_components_NTMap_app[cat_cs_simps]|

mk_VLambda Mr_Rel_components(1)
|vsv Mr_Rel_components_NTMap_vsv[cat_cs_intros]|
|vdomain Mr_Rel_components_NTMap_vdomain[cat_cs_simps]|
|app Mr_Rel_components_NTMap_app[cat_cs_simps]|

subsubsection‹‹Ml› and ‹Mr› for ‹Rel› are natural isomorphisms›

lemma (in 𝒵) Ml_Rel_is_iso_ntcf:
assumes "a ∈⇩∘ cat_Rel α⦇Obj⦈"
shows "Ml_Rel (cat_Rel α) a:
cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙(set {a},-)⇩C⇩F ↦⇩C⇩F⇩.⇩i⇩s⇩o
cf_id (cat_Rel α) :
cat_Rel α ↦↦⇩C⇘α⇙ cat_Rel α"
proof-

let ?cf_prod = ‹cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙ (set {a},-)⇩C⇩F›
note [cat_cs_simps] = set_empty

interpret cf_prod: is_functor
α ‹cat_Rel α ×⇩C cat_Rel α› ‹cat_Rel α› ‹cf_prod_2_Rel (cat_Rel α)›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Rel_cs_intros)

show ?thesis
proof(intro is_iso_ntcfI is_ntcfI')
show "vfsequence (Ml_Rel (cat_Rel α) a)" unfolding Ml_Rel_def by auto
show "vcard (Ml_Rel (cat_Rel α) a) = 5⇩ℕ"
unfolding Ml_Rel_def by (simp add: nat_omega_simps)
from assms show "?cf_prod : cat_Rel α ↦↦⇩C⇘α⇙ cat_Rel α"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_cs_intros V_cs_intros
)
show "Ml_Rel (cat_Rel α) a⦇NTMap⦈⦇B⦈ :
?cf_prod⦇ObjMap⦈⦇B⦈ ↦⇩i⇩s⇩o⇘cat_Rel α⇙ cf_id (cat_Rel α)⦇ObjMap⦈⦇B⦈"
if "B ∈⇩∘ cat_Rel α⦇Obj⦈" for B
using assms that
by
(
cs_concl
cs_simp: cat_Rel_components(1) V_cs_simps cat_cs_simps
cs_intro:
cat_Rel_par_set_cs_intros
cat_cs_intros
V_cs_intros
cat_prod_cs_intros
)
with cat_Rel_is_iso_arrD[OF this] show
"Ml_Rel (cat_Rel α) a⦇NTMap⦈⦇B⦈ :
?cf_prod⦇ObjMap⦈⦇B⦈ ↦⇘cat_Rel α⇙ cf_id (cat_Rel α)⦇ObjMap⦈⦇B⦈"
if "B ∈⇩∘ cat_Rel α⦇Obj⦈" for B
using that by simp
show
"Ml_Rel (cat_Rel α) a⦇NTMap⦈⦇B⦈ ∘⇩A⇘cat_Rel α⇙ ?cf_prod⦇ArrMap⦈⦇F⦈ =
cf_id (cat_Rel α)⦇ArrMap⦈⦇F⦈ ∘⇩A⇘cat_Rel α⇙ Ml_Rel (cat_Rel α) a⦇NTMap⦈⦇A⦈"
if "F : A ↦⇘cat_Rel α⇙ B" for A B F
proof-
note F = cat_Rel_is_arrD[OF that]
interpret F: arr_Rel α F
rewrites "F⦇ArrDom⦈ = A" and "F⦇ArrCod⦈ = B"
by (intro F)+
have [cat_cs_simps]:
"vsnd_arrow (set {a}) B ∘⇩A⇘cat_Rel α⇙
(cat_Rel α⦇CId⦈⦇set {a}⦈) ⇩A×⇩R⇩e⇩l F =
F ∘⇩A⇘cat_Rel α⇙ vsnd_arrow (set {a}) A"
(is ‹?B2 ∘⇩A⇘cat_Rel α⇙ ?aF = F ∘⇩A⇘cat_Rel α⇙ ?A2›)
proof-
from assms that have lhs:
"?B2 ∘⇩A⇘cat_Rel α⇙ ?aF : set {a} ×⇩∘ A ↦⇘cat_Rel α⇙ B"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros V_cs_intros
)
from assms that have rhs:
"F ∘⇩A⇘cat_Rel α⇙ ?A2 : set {a} ×⇩∘ A ↦⇘cat_Rel α⇙ B"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros V_cs_intros
)
have [cat_cs_simps]:
"?B2⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (vid_on (set {a})) (F⦇ArrVal⦈) =
F⦇ArrVal⦈ ∘⇩∘ ?A2⦇ArrVal⦈"
proof(intro vsubset_antisym vsubsetI)
fix xx'_z assume "xx'_z ∈⇩∘
?B2⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (vid_on (set {a})) (F⦇ArrVal⦈)"
then obtain xx' yy' z
where xx'_z_def: "xx'_z = ⟨xx', z⟩"
and xx'_yy':
"⟨xx', yy'⟩ ∈⇩∘ prod_2_Rel_ArrVal (vid_on (set {a})) (F⦇ArrVal⦈)"
and yy'_z: "⟨yy', z⟩ ∈⇩∘ ?B2⦇ArrVal⦈"
by (meson vcompE prod_2_Rel_ArrValE)
from xx'_yy' obtain x x' y y'
where "⟨xx', yy'⟩ = ⟨⟨x, x'⟩, ⟨y, y'⟩⟩"
and "⟨x, y⟩ ∈⇩∘ vid_on (set {a})"
and xy': "⟨x', y'⟩ ∈⇩∘ F⦇ArrVal⦈"
by auto
then have xx'_def: "xx' = ⟨a, x'⟩" and yy'_def: "yy' = ⟨a, y'⟩"
by simp_all
with yy'_z have y': "y' ∈⇩∘ B" and z_def: "z = y'"
unfolding vsnd_arrow_components by auto
from xy' vsubsetD have x': "x' ∈⇩∘ A"
by (auto intro: F.arr_Rel_ArrVal_vdomain)
show "xx'_z ∈⇩∘ F⦇ArrVal⦈ ∘⇩∘ ?A2⦇ArrVal⦈"
unfolding xx'_z_def z_def xx'_def
by (intro vcompI, rule xy')
(auto simp: vsnd_arrow_components x' VLambda_iff2)
next
fix ay_z assume "ay_z ∈⇩∘ F⦇ArrVal⦈ ∘⇩∘ ?A2⦇ArrVal⦈"
then obtain ay y z
where xx'_z_def: "ay_z = ⟨ay, z⟩"
and ay_y: "⟨ay, y⟩ ∈⇩∘ ?A2⦇ArrVal⦈"
and yz[cat_cs_intros]: "⟨y, z⟩ ∈⇩∘ F⦇ArrVal⦈"
by auto
then have ay_z_def: "ay_z = ⟨⟨a, y⟩, z⟩"
and y: "y ∈⇩∘ A"
and ay_def: "ay = ⟨a, y⟩"
unfolding vsnd_arrow_components by auto
from yz vsubsetD have z: "z ∈⇩∘ B"
by (auto intro: F.arr_Rel_ArrVal_vrange)
have [cat_cs_intros]: "⟨a, a⟩ ∈⇩∘ vid_on (set {a})" by auto
show "ay_z ∈⇩∘
?B2⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (vid_on (set {a})) (F⦇ArrVal⦈)"
unfolding ay_z_def
by
(
intro vcompI prod_2_Rel_ArrValI,
rule vsv.vsv_ex1_app1[THEN iffD1],
unfold cat_cs_simps,
insert z
)
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros
)
qed
show ?thesis
proof(rule arr_Rel_eqI)
from lhs show arr_Rel_lhs: "arr_Rel α (?B2 ∘⇩A⇘cat_Rel α⇙ ?aF)"
by (auto dest: cat_Rel_is_arrD)
from rhs show "arr_Rel α (F ∘⇩A⇘cat_Rel α⇙ ?A2)"
by (auto dest: cat_Rel_is_arrD)
note cat_Rel_CId_app[cat_Rel_cs_simps del]
note 𝒵.cat_Rel_CId_app[cat_Rel_cs_simps del]
from that assms show
"(?B2 ∘⇩A⇘cat_Rel α⇙ ?aF)⦇ArrVal⦈ = (F ∘⇩A⇘cat_Rel α⇙ ?A2)⦇ArrVal⦈"
by (*slow*)
(
cs_concl
cs_simp: cat_cs_simps cat_Rel_cs_simps
cs_intro: cat_cs_intros cat_Rel_par_set_cs_intros V_cs_intros
cs_simp:
id_Rel_components
cat_Rel_CId_app
comp_Rel_components(1)
prod_2_Rel_components
cat_Rel_components(1)
)
qed (use lhs rhs in ‹cs_concl cs_simp: cat_cs_simps›)+
qed
from that assms show ?thesis
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros V_cs_intros cat_prod_cs_intros
cs_simp: cat_Rel_components(1) V_cs_simps
)
qed
qed (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+

qed

lemma (in 𝒵) Ml_Rel_is_iso_ntcf'[cat_cs_intros]:
assumes "a ∈⇩∘ cat_Rel α⦇Obj⦈"
and "𝔉' = cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙(set {a},-)⇩C⇩F"
and "𝔊' = cf_id (cat_Rel α)"
and "𝔄' = cat_Rel α"
and "𝔅' = cat_Rel α"
and "α' = α"
shows "Ml_Rel (cat_Rel α) a : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
using assms(1) unfolding assms(2-6) by (rule Ml_Rel_is_iso_ntcf)

lemmas [cat_cs_intros] = 𝒵.Ml_Rel_is_iso_ntcf'

lemma (in 𝒵) Mr_Rel_is_iso_ntcf:
assumes "b ∈⇩∘ cat_Rel α⦇Obj⦈"
shows "Mr_Rel (cat_Rel α) b :
cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙(-,set {b})⇩C⇩F ↦⇩C⇩F⇩.⇩i⇩s⇩o
cf_id (cat_Rel α) :
cat_Rel α ↦↦⇩C⇘α⇙ cat_Rel α"
proof-

let ?cf_prod = ‹cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙ (-,set {b})⇩C⇩F›
note [cat_cs_simps] = set_empty

interpret cf_prod: is_functor
α ‹cat_Rel α ×⇩C cat_Rel α› ‹cat_Rel α› ‹cf_prod_2_Rel (cat_Rel α)›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Rel_cs_intros)

show ?thesis
proof(intro is_iso_ntcfI is_ntcfI')
show "vfsequence (Mr_Rel (cat_Rel α) b)" unfolding Mr_Rel_def by auto
show "vcard (Mr_Rel (cat_Rel α) b) = 5⇩ℕ"
unfolding Mr_Rel_def by (simp add: nat_omega_simps)
from assms show "?cf_prod : cat_Rel α ↦↦⇩C⇘α⇙ cat_Rel α"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_cs_intros V_cs_intros
)
show "Mr_Rel (cat_Rel α) b⦇NTMap⦈⦇B⦈ :
?cf_prod⦇ObjMap⦈⦇B⦈ ↦⇩i⇩s⇩o⇘cat_Rel α⇙ cf_id (cat_Rel α)⦇ObjMap⦈⦇B⦈"
if "B ∈⇩∘ cat_Rel α⦇Obj⦈" for B
using assms that
by
(
cs_concl
cs_simp: cat_Rel_components(1) V_cs_simps cat_cs_simps
cs_intro:
cat_cs_intros
cat_Rel_par_set_cs_intros
V_cs_intros
cat_prod_cs_intros
)
with cat_Rel_is_iso_arrD[OF this] show
"Mr_Rel (cat_Rel α) b⦇NTMap⦈⦇B⦈ :
?cf_prod⦇ObjMap⦈⦇B⦈ ↦⇘cat_Rel α⇙ cf_id (cat_Rel α)⦇ObjMap⦈⦇B⦈"
if "B ∈⇩∘ cat_Rel α⦇Obj⦈" for B
using that by simp
show
"Mr_Rel (cat_Rel α) b⦇NTMap⦈⦇B⦈ ∘⇩A⇘cat_Rel α⇙ ?cf_prod⦇ArrMap⦈⦇F⦈ =
cf_id (cat_Rel α)⦇ArrMap⦈⦇F⦈ ∘⇩A⇘cat_Rel α⇙ Mr_Rel (cat_Rel α) b⦇NTMap⦈⦇A⦈"
if "F : A ↦⇘cat_Rel α⇙ B" for A B F
proof-
note F = cat_Rel_is_arrD[OF that]
interpret F: arr_Rel α F
rewrites "F⦇ArrDom⦈ = A" and "F⦇ArrCod⦈ = B"
by (intro F)+
have [cat_cs_simps]:
"vfst_arrow B (set {b}) ∘⇩A⇘cat_Rel α⇙
F ⇩A×⇩R⇩e⇩l (cat_Rel α⦇CId⦈⦇set {b}⦈) =
F ∘⇩A⇘cat_Rel α⇙ vfst_arrow A (set {b})"
(is ‹?B1 ∘⇩A⇘cat_Rel α⇙ ?bF = F ∘⇩A⇘cat_Rel α⇙ ?A1›)
proof-
from assms that have lhs:
"?B1 ∘⇩A⇘cat_Rel α⇙ ?bF : A ×⇩∘ set {b} ↦⇘cat_Rel α⇙ B"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_cs_intros cat_Rel_par_set_cs_intros V_cs_intros
)
from assms that have rhs:
"F ∘⇩A⇘cat_Rel α⇙ ?A1 : A ×⇩∘ set {b} ↦⇘cat_Rel α⇙ B"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_cs_intros cat_Rel_par_set_cs_intros V_cs_intros
)
have [cat_cs_simps]:
"?B1⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (F⦇ArrVal⦈) (vid_on (set {b})) =
F⦇ArrVal⦈ ∘⇩∘ ?A1⦇ArrVal⦈"
proof(intro vsubset_antisym vsubsetI)
fix xx'_z assume "xx'_z ∈⇩∘
?B1⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (F⦇ArrVal⦈) (vid_on (set {b}))"
then obtain xx' yy' z
where xx'_z_def: "xx'_z = ⟨xx', z⟩"
and xx'_yy':
"⟨xx', yy'⟩ ∈⇩∘ prod_2_Rel_ArrVal (F⦇ArrVal⦈) (vid_on (set {b}))"
and yy'_z: "⟨yy', z⟩ ∈⇩∘ ?B1⦇ArrVal⦈"
by (meson vcompE prod_2_Rel_ArrValE)
from xx'_yy' obtain x x' y y'
where "⟨xx', yy'⟩ = ⟨⟨x, x'⟩, ⟨y, y'⟩⟩"
and "⟨x', y'⟩ ∈⇩∘ vid_on (set {b})"
and xy: "⟨x, y⟩ ∈⇩∘ F⦇ArrVal⦈"
by auto
then have xx'_def: "xx' = ⟨x, b⟩" and yy'_def: "yy' = ⟨y, b⟩"
by simp_all
with yy'_z have y': "y ∈⇩∘ B" and z_def: "z = y"
unfolding vfst_arrow_components by auto
from xy vsubsetD have x: "x ∈⇩∘ A"
by (auto intro: F.arr_Rel_ArrVal_vdomain)
show "xx'_z ∈⇩∘ F⦇ArrVal⦈ ∘⇩∘ ?A1⦇ArrVal⦈"
unfolding xx'_z_def z_def xx'_def
by (intro vcompI, rule xy)
(auto simp: vfst_arrow_components x VLambda_iff2)
next
fix xy_z assume "xy_z ∈⇩∘ F⦇ArrVal⦈ ∘⇩∘ ?A1⦇ArrVal⦈"
then obtain xy y z
where xx'_z_def: "xy_z = ⟨xy, z⟩"
and xy_y: "⟨xy, y⟩ ∈⇩∘ ?A1⦇ArrVal⦈"
and yz[cat_cs_intros]: "⟨y, z⟩ ∈⇩∘ F⦇ArrVal⦈"
by auto
then have xy_z_def: "xy_z = ⟨⟨y, b⟩, z⟩"
and y: "y ∈⇩∘ A"
and xy_def: "xy = ⟨y, b⟩"
unfolding vfst_arrow_components by auto
from yz vsubsetD have z: "z ```