Theory CZH_ECAT_Structure_Example

(* Copyright 2021 (C) Mihails Milehins *)

section‹Example: categories with additional structure›
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
how the framework developed in this article can 
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  DagCatObj  (C )ObjMapa = a"
    and dagcat_DagCat_idem[dagcat_cs_simps]: 
      "C  CF 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'



subsectionRel› 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.Rel α]"


text‹Components.›

lemma dagcat_Rel_components:
  shows "dagcat_Rel αDagCat = cat_Rel α"
    and "dagcat_Rel αDagDag = C.Rel α"
  unfolding dagcat_Rel_def dag_field_simps by (simp_all add: nat_omega_simps)


subsubsectionRel› 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 α)ObjMapa = a"
    if "a  dagcat_Rel αDagCatObj" 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 α) CF 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  :: V where [mcat_field_simps]: " = 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 +: is_iso_ntcf
    α Mcat^C3 Mcat cf_blcomp (Mcf) cf_brcomp (Mcf)  +
  Ml: is_iso_ntcf
    α
    Mcat
    Mcat
    McfMcat,Mcat(Me,-)CF
    cf_id (Mcat)
    Ml +
  Mr: is_iso_ntcf
    α
    Mcat
    Mcat
    McfMcat,Mcat(-,Me)CF
    cf_id (Mcat)
    Mr
  for α  +
  assumes mcat_length[mcat_cs_simps]: "vcard  = 6"
    and mcat_Me_is_obj[mcat_cs_intros]: "Me  McatObj"
    and mcat_pentagon:
      " 
        a  McatObj;
        b  McatObj;
        c  McatObj;
        d  McatObj
         
        (McatCIda HM.AMcfNTMapb, c, d) AMcatNTMapa, b HM.OMcfc, d AMcat(NTMapa, b, c HM.AMcfMcatCIdd) =
              NTMapa, b, c HM.OMcfd AMcatNTMapa HM.OMcfb, c, d"
    and mcat_triangle[mcat_cs_simps]:
      " a  McatObj; b  McatObj  
        (McatCIda HM.AMcfMlNTMapb) AMcatNTMapa, Me, b =
            (MrNTMapa HM.AMcfMcatCIdb)"

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 "𝔄 = 𝔅"
    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_bcA × (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 CArrVal =
    (λ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 CArrDom = (A × B) × C"
    and [cat_cs_simps]: "Mα_Rel_arrow_lr A B CArrCod = 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 CArrVal =
    (λa_bcA × (B × C). vfst a_bc, vfst (vsnd a_bc), vsnd (vsnd a_bc))"
    and [cat_cs_simps]: "Mα_Rel_arrow_rl A B CArrDom = A × (B × C)"
    and [cat_cs_simps]: "Mα_Rel_arrow_rl A B CArrCod = (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 CArrValab_c = a, b, c"
  using assms(2)
  unfolding assms(1)
  by (simp_all add: Mα_Rel_arrow_lr_ArrVal_app' nat_omega_simps)

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 CArrVala_bc = a, b, c"
  using assms(2)
  unfolding assms(1)
  by (simp_all add: Mα_Rel_arrow_rl_ArrVal_app' nat_omega_simps)


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 CArrVal)  Mα_Rel_arrow_lr A B CArrCod"
    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 CArrVal)  Mα_Rel_arrow_rl A B CArrCod"
    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 Acat_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 Acat_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 Acat_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 Acat_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 Acat_Set αMα_Rel_arrow_lr A B C)ArrVal = 
        cat_Set αCId(A × B) × CArrVal"
    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 Acat_Set αMα_Rel_arrow_lr A B C)ArrValab_c = 
          cat_Set αCId(A × B) × CArrValab_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 Acat_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 Acat_Set αMα_Rel_arrow_rl A B C = 
      cat_Set αCIdA × (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 Acat_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 Acat_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 αCIdA × (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 αCIdA × (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 Acat_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 αCIdA × (B × C))"
      by (auto dest: cat_Set_is_arrD(1))
    show 
      "(Mα_Rel_arrow_lr A B C Acat_Set αMα_Rel_arrow_rl A B C)ArrVal = 
        cat_Set αCIdA × (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 Acat_Set αMα_Rel_arrow_rl A B C)ArrVala_bc = 
          cat_Set αCIdA × (B × C)ArrVala_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 Acat_Set αMα_Rel_arrow_rl A B C = 
      cat_Set αCIdA × (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 isocat_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) isocat_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 Acat_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 Acat_Set αMα_Rel_arrow_rl A B C =
      cat_Set αCIdA × 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 isocat_Set αA × (B × C)"
    and "Mα_Rel_arrow_rl A B C : A × (B × C) isocat_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 isocat_Set αA × (B × C)"
    and Mα_Rel_arrow_rl_is_cat_Set_iso_arr:
    "Mα_Rel_arrow_rl A B C : A × (B × C) isocat_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' isoℭ'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' isoℭ'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 isocat_Par αA × (B × C)"
    and Mα_Rel_arrow_rl_is_cat_Par_iso_arr: 
    "Mα_Rel_arrow_rl A B C : A × (B × C) isocat_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 isocat_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) isocat_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' isoℭ'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' isoℭ'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 isocat_Rel αA × (B × C)"
    and Mα_Rel_arrow_rl_is_cat_Rel_iso_arr: 
    "Mα_Rel_arrow_rl A B C : A × (B × C) isocat_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 isocat_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) isocat_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' isoℭ'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' isoℭ'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'



subsectionMα› for Rel›


subsubsection‹Definition and elementary properties›

definition Mα_Rel :: "V  V"
  where "Mα_Rel  =
    [
      (λabc(^C3)Obj. Mα_Rel_arrow_lr (abc0) (abc1) (abc2)),
      cf_blcomp (cf_prod_2_Rel ),
      cf_brcomp (cf_prod_2_Rel ),
      ^C3,
      
    ]"


text‹Components.›

lemma Mα_Rel_components:
  shows "Mα_Rel NTMap =
    (λabc(^C3)Obj. Mα_Rel_arrow_lr (abc0) (abc1) (abc2))"
    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 = ^C3"
    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  (^C3)Obj"
  shows "Mα_Rel NTMapABC = Mα_Rel_arrow_lr A B C"
  using assms(2) 
  unfolding assms(1) 
  by (simp add: Mα_Rel_NTMap_app' nat_omega_simps)


subsubsectionMα› 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 α)) CF.iso
    cf_brcomp (cf_prod_2_Rel (cat_Rel α)) :
    cat_Rel α^C3 ↦↦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 α)NTMapABC :
      cf_blcomp (cf_prod_2_Rel (cat_Rel α))ObjMapABC isocat_Rel αcf_brcomp (cf_prod_2_Rel (cat_Rel α))ObjMapABC"
      if "ABC  (cat_Rel α^C3)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 α)NTMapABC :
      cf_blcomp (cf_prod_2_Rel (cat_Rel α))ObjMapABC cat_Rel αcf_brcomp (cf_prod_2_Rel (cat_Rel α))ObjMapABC"
      if "ABC  (cat_Rel α^C3)Obj" for ABC
      using that by (simp add: cat_Rel_is_iso_arrD(1))
    show 
      "Mα_Rel (cat_Rel α)NTMapABC' Acat_Rel αcf_blcomp (cf_prod_2_Rel (cat_Rel α))ArrMapHGF =
          cf_brcomp (cf_prod_2_Rel (cat_Rel α))ArrMapHGF Acat_Rel αMα_Rel (cat_Rel α)NTMapABC"
      if "HGF : ABC cat_Rel α^C3ABC'" 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 "HArrDom = A" and "HArrCod = A'"
        by (intro H)+
      interpret G: arr_Rel α G
        rewrites "GArrDom = B" and "GArrCod = B'"
        by (intro G)+
      interpret F: arr_Rel α F
        rewrites "FArrDom = C" and "FArrCod = 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 (HArrVal) (GArrVal)) 
              (FArrVal)
        and ?H_GF = 
          prod_2_Rel_ArrVal
              (HArrVal)
              (prod_2_Rel_ArrVal (GArrVal) (FArrVal))

      have [cat_cs_simps]:
        "?ABC' Acat_Rel α(H A×Rel G) A×Rel  F =
          H A×Rel (G A×Rel F) Acat_Rel α?ABC"
      proof-

        from H_is_arr G_is_arr F_is_arr have lhs:
          "?ABC' Acat_Rel α(H A×Rel G) A×Rel 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×Rel (G A×Rel F) Acat_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' Acat_Rel α(H A×Rel G) A×Rel F)"
            by (auto dest: cat_Rel_is_arrD)
          from rhs show arr_Rel_rhs: 
            "arr_Rel α (H A×Rel (G A×Rel F) Acat_Rel α?ABC)"
            by (auto dest: cat_Rel_is_arrD)

          have [cat_cs_simps]: "?ABC'ArrVal  ?HG_F = ?H_GF  ?ABCArrVal"
          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 (HArrVal) (GArrVal)"
                and cc': "c, c'  FArrVal"
              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'  HArrVal"
                and bb': "b, b'  GArrVal"
              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'ArrValabc'"
              by (simp add: vsv.vsv_appI[OF Mα_Rel_arrow_lr_ArrVal_vsv])
            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  ?ABCArrVal"
              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  ?ABCArrVal"
            then obtain abc abc' abc'' 
              where abc_abc''_def: "abc_abc'' = abc, abc''"
                and abc_abc': "abc, abc'  ?ABCArrVal"
                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''  HArrVal"
                and bc'_bc'':
                  "bc', bc''  prod_2_Rel_ArrVal (GArrVal) (FArrVal)"
              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''  GArrVal"
                and cc'': "c', c''  FArrVal"
              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  𝒟 (?ABCArrVal)" 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' = ?ABCArrValabc"
              by (simp add: vsv.vsv_appI[OF Mα_Rel_arrow_lr_ArrVal_vsv])
            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' Acat_Rel α(H A×Rel G) A×Rel F)ArrVal =
              (H A×Rel (G A×Rel F) Acat_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 α^C3"
    and "𝔅' = cat_Rel α"
    and "α' = α"
  shows "Mα_Rel (cat_Rel α) : 𝔉' CF.iso 𝔊' : 𝔄' ↦↦Cα'𝔅'"
  unfolding assms by (rule Mα_Rel_is_iso_ntcf)

lemmas [cat_cs_intros] = 𝒵.Mα_Rel_is_iso_ntcf'



subsectionMl› and Mr› for Rel›


subsubsection‹Definition and elementary properties›

definition Ml_Rel :: "V  V  V"
  where "Ml_Rel  a =
    [
      (λBObj. vsnd_arrow (set {a}) B),
      cf_prod_2_Rel ,(set {a},-)CF,
      cf_id ,
      ,
      
    ]"

definition Mr_Rel :: "V  V  V"
  where "Mr_Rel  b =
    [
      (λAObj. vfst_arrow A (set {b})),
      cf_prod_2_Rel ,(-,set {b})CF,
      cf_id ,
      ,
      
    ]"


text‹Components.›

lemma Ml_Rel_components:
  shows "Ml_Rel  aNTMap = (λBObj. vsnd_arrow (set {a}) B)"
    and [cat_cs_simps]: "Ml_Rel  aNTDom = cf_prod_2_Rel ,(set {a},-)CF"
    and [cat_cs_simps]: "Ml_Rel  aNTCod = cf_id "
    and [cat_cs_simps]: "Ml_Rel  aNTDGDom = "
    and [cat_cs_simps]: "Ml_Rel  aNTDGCod = "
  unfolding Ml_Rel_def nt_field_simps by (simp_all add: nat_omega_simps)

lemma Mr_Rel_components:
  shows "Mr_Rel  bNTMap = (λAObj. vfst_arrow A (set {b}))"
    and [cat_cs_simps]: "Mr_Rel  bNTDom = cf_prod_2_Rel ,(-,set {b})CF"
    and [cat_cs_simps]: "Mr_Rel  bNTCod = cf_id "
    and [cat_cs_simps]: "Mr_Rel  bNTDGDom = "
    and [cat_cs_simps]: "Mr_Rel  bNTDGCod = "
  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]|


subsubsectionMl› 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},-)CF CF.iso 
    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},-)CF
  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 α) aNTMapB :
      ?cf_prodObjMapB isocat_Rel αcf_id (cat_Rel α)ObjMapB"
      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 α) aNTMapB :
        ?cf_prodObjMapB cat_Rel αcf_id (cat_Rel α)ObjMapB"
      if "B  cat_Rel αObj" for B
      using that by simp
    show
      "Ml_Rel (cat_Rel α) aNTMapB Acat_Rel α?cf_prodArrMapF =
        cf_id (cat_Rel α)ArrMapF Acat_Rel αMl_Rel (cat_Rel α) aNTMapA"
      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 "FArrDom = A" and "FArrCod = B"
        by (intro F)+
      have [cat_cs_simps]:
        "vsnd_arrow (set {a}) B Acat_Rel α(cat_Rel αCIdset {a}) A×Rel F =
            F Acat_Rel αvsnd_arrow (set {a}) A"
        (is ?B2 Acat_Rel α?aF = F Acat_Rel α?A2)
      proof-
        from assms that have lhs:
          "?B2 Acat_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 Acat_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]: 
          "?B2ArrVal  prod_2_Rel_ArrVal (vid_on (set {a})) (FArrVal) =
            FArrVal  ?A2ArrVal"
        proof(intro vsubset_antisym vsubsetI)
          fix xx'_z assume "xx'_z 
            ?B2ArrVal  prod_2_Rel_ArrVal (vid_on (set {a})) (FArrVal)"
          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})) (FArrVal)"
              and yy'_z: "yy', z  ?B2ArrVal" 
            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'  FArrVal"
            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  FArrVal  ?A2ArrVal"
            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  FArrVal  ?A2ArrVal"
          then obtain ay y z
            where xx'_z_def: "ay_z = ay, z" 
              and ay_y: "ay, y  ?A2ArrVal"
              and yz[cat_cs_intros]: "y, z  FArrVal" 
            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 
            ?B2ArrVal  prod_2_Rel_ArrVal (vid_on (set {a})) (FArrVal)"
            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 Acat_Rel α?aF)"
            by (auto dest: cat_Rel_is_arrD)
          from rhs show "arr_Rel α (F Acat_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 Acat_Rel α?aF)ArrVal = (F Acat_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},-)CF"
    and "𝔊' = cf_id (cat_Rel α)"
    and "𝔄' = cat_Rel α"
    and "𝔅' = cat_Rel α"
    and "α' = α"
  shows "Ml_Rel (cat_Rel α) a : 𝔉' CF.iso 𝔊' : 𝔄' ↦↦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})CF CF.iso 
    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})CF
  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 α) bNTMapB :
      ?cf_prodObjMapB isocat_Rel αcf_id (cat_Rel α)ObjMapB"
      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 α) bNTMapB :
        ?cf_prodObjMapB cat_Rel αcf_id (cat_Rel α)ObjMapB"
      if "B  cat_Rel αObj" for B
      using that by simp
    show
      "Mr_Rel (cat_Rel α) bNTMapB Acat_Rel α?cf_prodArrMapF =
        cf_id (cat_Rel α)ArrMapF Acat_Rel αMr_Rel (cat_Rel α) bNTMapA"
      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 "FArrDom = A" and "FArrCod = B"
        by (intro F)+
      have [cat_cs_simps]:
        "vfst_arrow B (set {b}) Acat_Rel αF A×Rel (cat_Rel αCIdset {b}) =
            F Acat_Rel αvfst_arrow A (set {b})"
        (is ?B1 Acat_Rel α?bF = F Acat_Rel α?A1)
      proof-
        from assms that have lhs:
          "?B1 Acat_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 Acat_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]: 
          "?B1ArrVal  prod_2_Rel_ArrVal (FArrVal) (vid_on (set {b})) =
            FArrVal  ?A1ArrVal"
        proof(intro vsubset_antisym vsubsetI)
          fix xx'_z assume "xx'_z 
            ?B1ArrVal  prod_2_Rel_ArrVal (FArrVal) (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 (FArrVal) (vid_on (set {b}))"
              and yy'_z: "yy', z  ?B1ArrVal" 
            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  FArrVal"
            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  FArrVal  ?A1ArrVal"
            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  FArrVal  ?A1ArrVal"
          then obtain xy y z
            where xx'_z_def: "xy_z = xy, z" 
              and xy_y: "xy, y  ?A1ArrVal"
              and yz[cat_cs_intros]: "y, z  FArrVal" 
            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