Theory CZH_ECAT_Comma

(* Copyright 2021 (C) Mihails Milehins *)

section‹Comma categories›
theory CZH_ECAT_Comma
  imports 
    CZH_ECAT_NTCF
    CZH_ECAT_Simple
begin



subsection‹Background›

named_theorems cat_comma_cs_simps
named_theorems cat_comma_cs_intros



subsection‹Comma category›


subsubsection‹Definition and elementary properties›


text‹
See Exercise 1.3.vi in cite"riehl_category_2016" or 
Chapter II-6 in cite"mac_lane_categories_2010".
›

definition cat_comma_Obj :: "V  V  V"
  where "cat_comma_Obj 𝔊   set
    {
      [a, b, f] | a b f.
        a  𝔊HomDomObj 
        b  HomDomObj 
        f : 𝔊ObjMapa 𝔊HomCodObjMapb
    }"

lemma small_cat_comma_Obj[simp]: 
  "small
    {
      [a, b, f] | a b f.
        a  𝔄Obj  b  𝔅Obj  f : 𝔊ObjMapa ObjMapb
    }"
  (is small ?abfs)
proof-
  define Q where
    "Q i = (if i = 0 then 𝔄Obj else if i = 1 then 𝔅Obj else Arr)" 
    for i
  have "?abfs  elts (i set {0, 1, 2}. Q i)"
    unfolding Q_def
  proof
    (
      intro subsetI, 
      unfold mem_Collect_eq, 
      elim exE conjE, 
      intro vproductI; 
      simp only:
    )
    fix a b f show "𝒟 [a, b, f] = set {0, 1, 2}"
      by (simp add: three nat_omega_simps)
  qed (force simp: nat_omega_simps)+
  then show "small ?abfs" by (rule down)
qed

definition cat_comma_Hom :: "V  V  V  V  V"
  where "cat_comma_Hom 𝔊  A B  set
    {
      [A, B, [g, h]] | g h.
        A  cat_comma_Obj 𝔊  
        B  cat_comma_Obj 𝔊  
        g : A0 𝔊HomDomB0 
        h : A1 HomDomB1 
        B2 A𝔊HomCod𝔊ArrMapg =
         ArrMaph A𝔊HomCodA2
    }"

lemma small_cat_comma_Hom[simp]: "small
  {
    [A, B, [g, h]] | g h.
      A  cat_comma_Obj 𝔊  
      B  cat_comma_Obj 𝔊  
      g : A0 𝔄B0 
      h : A1 𝔅B1 
      B2 A𝔊ArrMapg = ArrMaph AA2
  }"
  (is small ?abf_a'b'f'_gh)
proof-
  define Q where
    "Q i =
      (
        if i = 0
        then cat_comma_Obj 𝔊  
        else if i = 1 then cat_comma_Obj 𝔊  else 𝔄Arr × 𝔅Arr
      )"
    for i
  have "?abf_a'b'f'_gh  elts (i set {0, 1, 2}. Q i)"
    unfolding Q_def
  proof
    (
      intro subsetI, 
      unfold mem_Collect_eq, 
      elim exE conjE,
      intro vproductI; 
      simp only:
    )
    fix a b f show "𝒟 [a, b, f] = ZFC_in_HOL.set {0, 1, 2}"
      by (simp add: three nat_omega_simps)
  qed (force simp : nat_omega_simps)+
  then show "small ?abf_a'b'f'_gh" by (rule down)
qed

definition cat_comma_Arr :: "V  V  V"
  where "cat_comma_Arr 𝔊  
    (
      Acat_comma_Obj 𝔊 . Bcat_comma_Obj 𝔊 .
        cat_comma_Hom 𝔊  A B
    )"

definition cat_comma_composable :: "V  V  V"
  where "cat_comma_composable 𝔊   set
    {
      [[B, C, G], [A, B, F]] | A B C G F.
        [B, C, G]  cat_comma_Arr 𝔊   [A, B, F]  cat_comma_Arr 𝔊 
    }"

lemma small_cat_comma_composable[simp]:
  shows "small
    {
      [[B, C, G], [A, B, F]] | A B C G F.
        [B, C, G]  cat_comma_Arr 𝔊   [A, B, F]  cat_comma_Arr 𝔊 
    }"
  (is small ?S)
proof(rule down)
  show "?S  elts (cat_comma_Arr 𝔊  × cat_comma_Arr 𝔊 )" by auto
qed

definition cat_comma :: "V  V  V" ((_ CFCF _) [1000, 1000] 999)
  where "𝔊 CFCF  =
    [
      cat_comma_Obj 𝔊 ,
      cat_comma_Arr 𝔊 ,
      (λFcat_comma_Arr 𝔊 . F0),
      (λFcat_comma_Arr 𝔊 . F1),
      (
        λGFcat_comma_composable 𝔊 .
          [
            GF10,
            GF01,
            [
              GF020 A𝔊HomDomGF120,
              GF021 AHomDomGF121
            ]
          ]
      ),
      (
        λAcat_comma_Obj 𝔊 .
          [A, A, [𝔊HomDomCIdA0, HomDomCIdA1]]
      )
    ]"


text‹Components.›

lemma cat_comma_components:
  shows "𝔊 CFCF Obj = cat_comma_Obj 𝔊 "
    and "𝔊 CFCF Arr = cat_comma_Arr 𝔊 "
    and "𝔊 CFCF Dom = (λFcat_comma_Arr 𝔊 . F0)"
    and "𝔊 CFCF Cod = (λFcat_comma_Arr 𝔊 . F1)"
    and "𝔊 CFCF Comp =
      (
        λGFcat_comma_composable 𝔊 .
          [
            GF10,
            GF01,
            [
              GF020 A𝔊HomDomGF120,
              GF021 AHomDomGF121
            ]
          ]
      )"
    and "𝔊 CFCF CId =
      (
        λAcat_comma_Obj 𝔊 .
          [A, A, [𝔊HomDomCIdA0, HomDomCIdA1]]
      )"
  unfolding cat_comma_def dg_field_simps by (simp_all add: nat_omega_simps)

context
  fixes α 𝔄 𝔅  𝔊 
  assumes 𝔊: "𝔊 : 𝔄 ↦↦Cα"
    and : " : 𝔅 ↦↦Cα"
begin

interpretation 𝔊: is_functor α 𝔄  𝔊 by (rule 𝔊)
interpretation: is_functor α 𝔅   by (rule )

lemma cat_comma_Obj_def':
  "cat_comma_Obj 𝔊   set
    {
      [a, b, f] | a b f.
        a  𝔄Obj  b  𝔅Obj  f : 𝔊ObjMapa ObjMapb
    }"
  unfolding cat_comma_Obj_def cat_cs_simps by simp

lemma cat_comma_Hom_def':
  "cat_comma_Hom 𝔊  A B  set
    {
      [A, B, [g, h]] | g h.
        A  cat_comma_Obj 𝔊  
        B  cat_comma_Obj 𝔊  
        g : A0 𝔄B0 
        h : A1 𝔅B1 
        B2 A𝔊ArrMapg = ArrMaph AA2
    }"
  unfolding cat_comma_Hom_def cat_cs_simps by simp

lemma cat_comma_components':
  shows "𝔊 CFCF Obj = cat_comma_Obj 𝔊 "
    and "𝔊 CFCF Arr = cat_comma_Arr 𝔊 "
    and "𝔊 CFCF Dom = (λFcat_comma_Arr 𝔊 . F0)"
    and "𝔊 CFCF Cod = (λFcat_comma_Arr 𝔊 . F1)"
    and "𝔊 CFCF Comp =
      (
        λGFcat_comma_composable 𝔊 .
          [
            GF10,
            GF01,
            [
              GF020 A𝔄GF120,
              GF021 A𝔅GF121
            ]
          ]
      )"
    and "𝔊 CFCF CId =
      (λAcat_comma_Obj 𝔊 . [A, A, [𝔄CIdA0, 𝔅CIdA1]])"
  unfolding cat_comma_components cat_cs_simps by simp_all

end


subsubsection‹Objects›

lemma cat_comma_ObjI[cat_comma_cs_intros]:
  assumes "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
    and "A = [a, b, f]"
    and "a  𝔄Obj" 
    and "b  𝔅Obj" 
    and "f : 𝔊ObjMapa ObjMapb"
  shows "A  𝔊 CFCF Obj"
  using assms(4-6) 
  unfolding cat_comma_Obj_def'[OF assms(1,2)] assms(3) cat_comma_components 
  by simp

lemma cat_comma_ObjD[dest]:
  assumes "[a, b, f]  𝔊 CFCF Obj"
    and "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
  shows "a  𝔄Obj" 
    and "b  𝔅Obj" 
    and "f : 𝔊ObjMapa ObjMapb"
  using assms
  unfolding 
    cat_comma_components'[OF assms(2,3)] cat_comma_Obj_def'[OF assms(2,3)] 
  by auto

lemma cat_comma_ObjE[elim]:
  assumes "A  𝔊 CFCF Obj"
    and "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
  obtains a b f where "A = [a, b, f]"
    and "a  𝔄Obj" 
    and "b  𝔅Obj" 
    and "f : 𝔊ObjMapa ObjMapb"
  using assms
  unfolding 
    cat_comma_components'[OF assms(2,3)] cat_comma_Obj_def'[OF assms(2,3)] 
  by auto


subsubsection‹Arrows›

lemma cat_comma_HomI[cat_comma_cs_intros]:
  assumes "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
    and "F = [A, B, [g, h]]"
    and "A = [a, b, f]"
    and "B = [a', b', f']"
    and "g : a 𝔄a'"
    and "h : b 𝔅b'"
    and "f : 𝔊ObjMapa ObjMapb"
    and "f' : 𝔊ObjMapa' ObjMapb'"
    and "f' A𝔊ArrMapg = ArrMaph Af"
  shows "F  cat_comma_Hom 𝔊  A B"
  using assms(1,2,6-10)
  unfolding cat_comma_Hom_def'[OF assms(1,2)] assms(3-5)
  by 
    (
      intro in_set_CollectI exI conjI small_cat_comma_Hom, 
      unfold cat_comma_components'(1,2)[OF assms(1,2), symmetric],
      (
        cs_concl 
          cs_simp: cat_comma_cs_simps 
          cs_intro: cat_cs_intros cat_comma_cs_intros
      )+
    )
    (clarsimp simp: nat_omega_simps)+

lemma cat_comma_HomE[elim]:
  assumes "F  cat_comma_Hom 𝔊  A B"
    and "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
  obtains a b f a' b' f' g h
    where "F = [A, B, [g, h]]"
      and "A = [a, b, f]"
      and "B = [a', b', f']"
      and "g : a 𝔄a'"
      and "h : b 𝔅b'"
      and "f : 𝔊ObjMapa ObjMapb"
      and "f' : 𝔊ObjMapa' ObjMapb'"
      and "f' A𝔊ArrMapg = ArrMaph Af"
  using assms(1) 
  by 
    (
      unfold
        cat_comma_components'[OF assms(2,3)] cat_comma_Hom_def'[OF assms(2,3)],
      elim in_small_setE; 
      (unfold mem_Collect_eq, elim exE conjE cat_comma_ObjE[OF _ assms(2,3)])?,
      insert that,
      all(unfold cat_comma_components'(1,2)[OF assms(2,3), symmetric],
        elim cat_comma_ObjE[OF _ assms(2,3)]) | -
    )
    (auto simp: nat_omega_simps)

lemma cat_comma_HomD[dest]:
  assumes "[[a, b, f], [a', b', f'], [g, h]]  cat_comma_Hom 𝔊  A B"
    and "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
  shows "g : a 𝔄a'"
    and "h : b 𝔅b'"
    and "f : 𝔊ObjMapa ObjMapb"
    and "f' : 𝔊ObjMapa' ObjMapb'"
    and "f' A𝔊ArrMapg = ArrMaph Af"
  using assms(1) by (force elim!: cat_comma_HomE[OF _ assms(2,3)])+

lemma cat_comma_ArrI[cat_comma_cs_intros]: 
  assumes "F  cat_comma_Hom 𝔊  A B"
    and "A  𝔊 CFCF Obj"
    and "B  𝔊 CFCF Obj"
  shows "F  𝔊 CFCF Arr"
  using assms 
  unfolding cat_comma_components cat_comma_Arr_def 
  by (intro vifunionI)

lemma cat_comma_ArrE[elim]:
  assumes "F  𝔊 CFCF Arr"
  obtains A B 
    where "F  cat_comma_Hom 𝔊  A B"
      and "A  𝔊 CFCF Obj"
      and "B  𝔊 CFCF Obj"
  using assms unfolding cat_comma_components cat_comma_Arr_def by auto

lemma cat_comma_ArrD[dest]: 
  assumes "[A, B, F]  𝔊 CFCF Arr"
    and "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
  shows "[A, B, F]  cat_comma_Hom 𝔊  A B"
    and "A  𝔊 CFCF Obj"
    and "B  𝔊 CFCF Obj"
proof-
  from assms obtain C D 
    where "[A, B, F]  cat_comma_Hom 𝔊  C D"
      and "C  𝔊 CFCF Obj"
      and "D  𝔊 CFCF Obj"
    by (elim cat_comma_ArrE)
  moreover from cat_comma_HomE[OF this(1) assms(2,3)] have "A = C" and "B = D"
    by auto
  ultimately show "[A, B, F]  cat_comma_Hom 𝔊  A B"
    and "A  𝔊 CFCF Obj"
    and "B  𝔊 CFCF Obj"
    by auto
qed


subsubsection‹Domain›

lemma cat_comma_Dom_vsv[cat_comma_cs_intros]: "vsv (𝔊 CFCF Dom)"
  unfolding cat_comma_components by simp

lemma cat_comma_Dom_vdomain[cat_comma_cs_simps]:
  "𝒟 (𝔊 CFCF Dom) = 𝔊 CFCF Arr"
  unfolding cat_comma_components by simp

lemma cat_comma_Dom_app[cat_comma_cs_simps]:
  assumes "ABF = [A, B, F]" and "ABF  𝔊 CFCF Arr"
  shows "𝔊 CFCF DomABF = A"
  using assms(2) unfolding assms(1) cat_comma_components by simp

lemma cat_comma_Dom_vrange:
  assumes "𝔊 : 𝔄 ↦↦Cα" and " : 𝔅 ↦↦Cα"
  shows " (𝔊 CFCF Dom)  𝔊 CFCF Obj"
proof(rule vsv.vsv_vrange_vsubset)
  fix ABF assume "ABF  𝒟 (𝔊 CFCF Dom)"
  then have "ABF  𝔊 CFCF Arr" 
    by (cs_prems cs_shallow cs_simp: cat_comma_cs_simps)
  then obtain A B 
    where ABF: "ABF  cat_comma_Hom 𝔊  A B"
      and A: "A  𝔊 CFCF Obj"
      and B: "B  𝔊 CFCF Obj"
    by auto
  from this(1) obtain a b f a' b' f' g h
    where "ABF = [A, B, [g, h]]"
      and "A = [a, b, f]"
      and "B = [a', b', f']"
      and "g : a 𝔄a'"
      and "h : b 𝔅b'"
      and "f : 𝔊ObjMapa ObjMapb"
      and "f' : 𝔊ObjMapa' ObjMapb'"
      and "f' A𝔊ArrMapg = ArrMaph Af"
    by (elim cat_comma_HomE[OF _ assms(1,2)])
  from ABF this A B show "𝔊 CFCF DomABF  𝔊 CFCF Obj"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_comma_cs_simps cs_intro: cat_comma_cs_intros
      )
qed (auto intro: cat_comma_cs_intros)


subsubsection‹Codomain›

lemma cat_comma_Cod_vsv[cat_comma_cs_intros]: "vsv (𝔊 CFCF Cod)"
  unfolding cat_comma_components by simp

lemma cat_comma_Cod_vdomain[cat_comma_cs_simps]:
  "𝒟 (𝔊 CFCF Cod) = 𝔊 CFCF Arr"
  unfolding cat_comma_components by simp

lemma cat_comma_Cod_app[cat_comma_cs_simps]:
  assumes "ABF = [A, B, F]" and "ABF  𝔊 CFCF Arr"
  shows "𝔊 CFCF CodABF = B"
  using assms(2)
  unfolding assms(1) cat_comma_components
  by (simp add: nat_omega_simps)

lemma cat_comma_Cod_vrange:
  assumes "𝔊 : 𝔄 ↦↦Cα" and " : 𝔅 ↦↦Cα"
  shows " (𝔊 CFCF Cod)  𝔊 CFCF Obj"
proof(rule vsv.vsv_vrange_vsubset)
  fix ABF assume "ABF  𝒟 (𝔊 CFCF Cod)"
  then have "ABF  𝔊 CFCF Arr" 
    by (cs_prems cs_shallow cs_simp: cat_comma_cs_simps)
  then obtain A B 
    where F: "ABF  cat_comma_Hom 𝔊  A B"
      and A: "A  𝔊 CFCF Obj"
      and B: "B  𝔊 CFCF Obj"
    by auto
  from this(1) obtain a b f a' b' f' g h
    where "ABF = [A, B, [g, h]]"
      and "A = [a, b, f]"
      and "B = [a', b', f']"
      and "g : a 𝔄a'"
      and "h : b 𝔅b'"
      and "f : 𝔊ObjMapa ObjMapb"
      and "f' : 𝔊ObjMapa' ObjMapb'"
      and "f' A𝔊ArrMapg = ArrMaph Af"
    by (elim cat_comma_HomE[OF _ assms(1,2)])
  from F this A B show "𝔊 CFCF CodABF  𝔊 CFCF Obj"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_comma_cs_simps cs_intro: cat_comma_cs_intros
      )
qed (auto intro: cat_comma_cs_intros)


subsubsection‹Arrow with a domain and a codomain›

lemma cat_comma_is_arrI[cat_comma_cs_intros]:
  assumes "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
    and "ABF = [A, B, F]"
    and "A = [a, b, f]"
    and "B = [a', b', f']"
    and "F = [g, h]"
    and "g : a 𝔄a'"
    and "h : b 𝔅b'"
    and "f : 𝔊ObjMapa ObjMapb"
    and "f' : 𝔊ObjMapa' ObjMapb'"
    and "f' A𝔊ArrMapg = ArrMaph Af"
  shows "ABF : A 𝔊 CFCF B"
proof(intro is_arrI)
  interpret 𝔊: is_functor α 𝔄  𝔊 by (rule assms(1))
  interpret: is_functor α 𝔅   by (rule assms(2))
  from assms(7-11) show "ABF  𝔊 CFCF Arr"
    unfolding assms(3-6)
    by 
      (
        cs_concl  
          cs_simp: cat_comma_cs_simps 
          cs_intro: cat_cs_intros cat_comma_cs_intros
      )
  with assms(7-11) show "𝔊 CFCF DomABF = A" "𝔊 CFCF CodABF = B"
    unfolding assms(3-6) by (cs_concl cs_shallow cs_simp: cat_comma_cs_simps)+
qed

lemma cat_comma_is_arrD[dest]:
  assumes "[[a, b, f], [a', b', f'], [g, h]] :
    [a, b, f] 𝔊 CFCF [a', b', f']"
    and "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
  shows "g : a 𝔄a'"
    and "h : b 𝔅b'"
    and "f : 𝔊ObjMapa ObjMapb"
    and "f' : 𝔊ObjMapa' ObjMapb'"
    and "f' A𝔊ArrMapg = ArrMaph Af"
proof-
  note F_is_arrD = is_arrD[OF assms(1)]
  note F_cat_comma_ArrD = cat_comma_ArrD[OF F_is_arrD(1) assms(2,3)]
  show "g : a 𝔄a'"
    and "h : b 𝔅b'"
    and "f : 𝔊ObjMapa ObjMapb"
    and "f' : 𝔊ObjMapa' ObjMapb'"
    and "f' A𝔊ArrMapg = ArrMaph Af"
    by (intro cat_comma_HomD[OF F_cat_comma_ArrD(1) assms(2,3)])+    
qed

lemma cat_comma_is_arrE[elim]:
  assumes "ABF : A 𝔊 CFCF B"
    and "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
  obtains a b f a' b' f' g h
    where "ABF = [[a, b, f], [a', b', f'], [g, h]]"
      and "A = [a, b, f]"
      and "B = [a', b', f']"
      and "g : a 𝔄a'"
      and "h : b 𝔅b'"
      and "f : 𝔊ObjMapa ObjMapb"
      and "f' : 𝔊ObjMapa' ObjMapb'"
      and "f' A𝔊ArrMapg = ArrMaph Af"
proof-
  note F_is_arrD = is_arrD[OF assms(1)]
  from F_is_arrD(1) obtain C D 
    where "ABF  cat_comma_Hom 𝔊  C D"
      and "C  𝔊 CFCF Obj" 
      and "D  𝔊 CFCF Obj"
    by auto
  from this(1) obtain a b f a' b' f' g h
    where F_def: "ABF = [C, D, [g, h]]"
      and "C = [a, b, f]"
      and "D = [a', b', f']"
      and "g : a 𝔄a'"
      and "h : b 𝔅b'"
      and "f : 𝔊ObjMapa ObjMapb"
      and "f' : 𝔊ObjMapa' ObjMapb'"
      and "f' A𝔊ArrMapg = ArrMaph Af"
     by (elim cat_comma_HomE[OF _ assms(2,3)])
  with that show ?thesis 
    by (metis F_is_arrD(1,2,3) cat_comma_Cod_app cat_comma_Dom_app)
qed


subsubsection‹Composition›

lemma cat_comma_composableI:
  assumes "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
    and "ABCGF = [BCG, ABF]"
    and "BCG : B 𝔊 CFCF C"
    and "ABF : A 𝔊 CFCF B"
  shows "ABCGF  cat_comma_composable 𝔊 "
proof-
  from assms(1,2,5) obtain a b f a' b' f' gh 
    where ABF_def: "ABF = [[a, b, f], [a', b', f'], gh]"
      and "A = [a, b, f]"
      and  "B = [a', b', f']"
    by auto
  with assms(1,2,4) obtain a'' b'' f'' g'h' 
    where BCG_def: "BCG = [[a', b', f'], [a'', b'', f''], g'h']"
      and "B = [a', b', f']"
      and "C = [a'', b'', f'']"
    by auto
  from is_arrD(1)[OF assms(4)] have "BCG  cat_comma_Arr 𝔊 "
    unfolding cat_comma_components'(2)[OF assms(1,2)].
  moreover from is_arrD(1)[OF assms(5)] have "ABF  cat_comma_Arr 𝔊 "
    unfolding cat_comma_components'(2)[OF assms(1,2)].
  ultimately show ?thesis 
    unfolding assms(3) ABF_def BCG_def cat_comma_composable_def 
    by simp
qed

lemma cat_comma_composableE[elim]:
  assumes "ABCGF  cat_comma_composable 𝔊 "
    and "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
  obtains BCG ABF A B C
    where "ABCGF = [BCG, ABF]"
      and "BCG : B 𝔊 CFCF C"
      and "ABF : A 𝔊 CFCF B"
proof-
  from assms(1) obtain A B C G F 
    where ABCGF_def: "ABCGF = [[B, C, G], [A, B, F]]"
      and BCG: "[B, C, G]  𝔊 CFCF Arr"
      and ABF: "[A, B, F]  𝔊 CFCF Arr"
    unfolding cat_comma_composable_def
    by (auto simp: cat_comma_components'[OF assms(2,3)])  
  note BCG = cat_comma_ArrD[OF BCG assms(2,3)]
    and ABF = cat_comma_ArrD[OF ABF assms(2,3)]
  from ABF(1) assms(2,3) obtain a b f a' b' f' g h
    where "[A, B, F] = [A, B, [g, h]]"
      and A_def: "A = [a, b, f]"
      and B_def: "B = [a', b', f']"
      and F_def: "F = [g, h]"
      and g: "g : a 𝔄a'"
      and h: "h : b 𝔅b'"
      and f: "f : 𝔊ObjMapa ObjMapb"
      and f': "f' : 𝔊ObjMapa' ObjMapb'"
      and [cat_comma_cs_simps]: 
        "f' A𝔊ArrMapg = ArrMaph Af"
    by auto
  with BCG(1) assms(2,3) obtain a'' b'' f'' g' h'
    where g'h'_def: "[B, C, G] = [B, C, [g', h']]"
      and C_def: "C = [a'', b'', f'']"
      and G_def: "G = [g', h']"
      and g': "g' : a' 𝔄a''"
      and h': "h' : b' 𝔅b''"
      and f'': "f'' : 𝔊ObjMapa'' ObjMapb''"
      and [cat_comma_cs_simps]: 
        "f'' A𝔊ArrMapg' = ArrMaph' Af'"
    by auto  
  from F_def have "F = [g, h]" by simp
  from assms(2,3) g h f f' g' h' f'' have 
    "[B, C, G] : B 𝔊 CFCF C"
    unfolding ABCGF_def F_def G_def A_def B_def C_def
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_comma_cs_simps cs_intro: cat_comma_is_arrI
      )+
  moreover from assms(2,3) g h f f' g' h' f'' have 
    "[A, B, F] : A 𝔊 CFCF B"
    unfolding ABCGF_def F_def G_def A_def B_def C_def
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_comma_cs_simps cs_intro: cat_comma_is_arrI
      )+
  ultimately show ?thesis using that ABCGF_def by auto
qed

lemma cat_comma_Comp_vsv[cat_comma_cs_intros]: "vsv (𝔊 CFCF Comp)"
  unfolding cat_comma_components by auto

lemma cat_comma_Comp_vdomain[cat_comma_cs_simps]: 
  "𝒟 (𝔊 CFCF Comp) = cat_comma_composable 𝔊 "
  unfolding cat_comma_components by auto

lemma cat_comma_Comp_app[cat_comma_cs_simps]:
  assumes "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
    and "G = [B, C, [g', h']]"
    and "F = [A, B, [g, h]]"
    and "G : B 𝔊 CFCF C" 
    and "F : A 𝔊 CFCF B"
  shows "G A𝔊 CFCF F = [A, C, [g' A𝔄g, h' A𝔅h]]"
  using assms(1,2,5,6)
  unfolding cat_comma_components'[OF assms(1,2)] assms(3,4)
  by (*slow*)
    (
      cs_concl 
        cs_simp: omega_of_set V_cs_simps vfsequence_simps
        cs_intro: nat_omega_intros V_cs_intros cat_comma_composableI TrueI
    )

lemma cat_comma_Comp_is_arr[cat_comma_cs_intros]:
  assumes "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
    and "BCG : B 𝔊 CFCF C" 
    and "ABF : A 𝔊 CFCF B"
  shows "BCG A𝔊 CFCF ABF : A 𝔊 CFCF C"
proof-
  interpret 𝔊: is_functor α 𝔄  𝔊 by (rule assms(1))
  interpret: is_functor α 𝔅   by (rule assms(2))
  from assms(1,2,4) obtain a b f a' b' f' g h
    where ABF_def: "ABF = [[a, b, f], [a', b', f'], [g, h]]"
      and A_def: "A = [a, b, f]"
      and B_def: "B = [a', b', f']"
      and g: "g : a 𝔄a'"
      and h: "h : b 𝔅b'"
      and f: "f : 𝔊ObjMapa ObjMapb"
      and f': "f' : 𝔊ObjMapa' ObjMapb'"
      and [symmetric, cat_cs_simps]: 
        "f' A𝔊ArrMapg = ArrMaph Af"
    by auto
  with assms(1,2,3) obtain a'' b'' f'' g' h'
    where BCG_def: "BCG = [[a', b', f'], [a'', b'', f''], [g', h']]"
      and C_def: "C = [a'', b'', f'']"
      and g': "g' : a' 𝔄a''"
      and h': "h' : b' 𝔅b''"
      and f'': "f'' : 𝔊ObjMapa'' ObjMapb''"
      and [cat_cs_simps]: "f'' A𝔊ArrMapg' = ArrMaph' Af'"
    by auto (*slow*)
  from g' have 𝔊g': "𝔊ArrMapg' : 𝔊ObjMapa' 𝔊ObjMapa''"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  note [cat_cs_simps] = 
    category.cat_assoc_helper[
      where= and h=f'' and g=𝔊ArrMapg' and q=ArrMaph' Af'
      ]
    category.cat_assoc_helper[
      where= and h=f and g=ArrMaph and q=f' A𝔊ArrMapg
      ]
  from assms(1,2,3,4) g h f f' g' h' f'' show ?thesis
    unfolding ABF_def BCG_def A_def B_def C_def
    by (intro cat_comma_is_arrI[OF assms(1,2)])
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_comma_cs_simps cs_intro: cat_cs_intros
      )+
qed


subsubsection‹Identity›

lemma cat_comma_CId_vsv[cat_comma_cs_intros]: "vsv (𝔊 CFCF CId)"
  unfolding cat_comma_components by simp

lemma cat_comma_CId_vdomain[cat_comma_cs_simps]:
  assumes "𝔊 : 𝔄 ↦↦Cα" and " : 𝔅 ↦↦Cα"
  shows "𝒟 (𝔊 CFCF CId) = 𝔊 CFCF Obj"
  unfolding cat_comma_components'[OF assms(1,2)] by simp

lemma cat_comma_CId_app[cat_comma_cs_simps]:
  assumes "𝔊 : 𝔄 ↦↦Cα"
    and " : 𝔅 ↦↦Cα"
    and "A = [a, b ,f]"
    and "A  𝔊 CFCF Obj"
  shows "𝔊 CFCF CIdA = [A, A, [𝔄CIda, 𝔅CIdb]]"
proof-
  from assms(4)[unfolded assms(3), unfolded cat_comma_components'[OF assms(1,2)]]
  have "[a, b, f]  cat_comma_Obj 𝔊 ".
  then show ?thesis
    unfolding cat_comma_components'(6)[OF assms(1,2)] assms(3)
    by (simp add: nat_omega_simps)
qed


subsubsectionHom›-set›

lemma cat_comma_Hom:
  assumes "𝔊 : 𝔄 ↦↦Cα" 
    and " : 𝔅 ↦↦Cα"
    and "A  𝔊 CFCF Obj"
    and "B  𝔊 CFCF Obj"
  shows "Hom (𝔊 CFCF ) A B = cat_comma_Hom 𝔊  A B"
proof(intro vsubset_antisym vsubsetI, unfold in_Hom_iff)
  fix ABF assume "ABF : A 𝔊 CFCF B"
  with assms(1,2) show "ABF  cat_comma_Hom 𝔊  A B"
    by (elim cat_comma_is_arrE[OF _ assms(1,2)], intro cat_comma_HomI) force+
next
  fix ABF assume "ABF  cat_comma_Hom 𝔊  A B"
  with assms(1,2) show "ABF : A 𝔊 CFCF B"
    by (elim cat_comma_HomE[OF _ assms(1,2)], intro cat_comma_is_arrI) force+
qed


subsubsection‹Comma category is a category›

lemma category_cat_comma[cat_comma_cs_intros]:
  assumes "𝔊 : 𝔄 ↦↦Cα" and " : 𝔅 ↦↦Cα"
  shows "category α (𝔊 CFCF )"
proof-

  interpret 𝔊: is_functor α 𝔄  𝔊 by (rule assms(1))
  interpret 𝔉: is_functor α 𝔅   by (rule assms(2))

  show ?thesis
  proof(rule categoryI')

    show "vfsequence (𝔊 CFCF )" unfolding cat_comma_def by auto
    show "vcard (𝔊 CFCF ) = 6"
      unfolding cat_comma_def by (simp add: nat_omega_simps)
    show " (𝔊 CFCF Dom)  𝔊 CFCF Obj"
      by (rule cat_comma_Dom_vrange[OF assms])
    show " (𝔊 CFCF Cod)  𝔊 CFCF Obj"
      by (rule cat_comma_Cod_vrange[OF assms])
    show "(GF  𝒟 (𝔊 CFCF Comp)) 
      (g f b c a. GF = [g, f]  g : b 𝔊 CFCF c  f : a 𝔊 CFCF b)"
      for GF
    proof(intro iffI; (elim exE conjE)?; (simp only: cat_comma_Comp_vdomain)?)
      assume prems: "GF  cat_comma_composable 𝔊 "
      with assms obtain G F abf a'b'f' a''b''f'' 
        where "GF = [G, F]"
          and "G : a'b'f' 𝔊 CFCF a''b''f''"
          and "F : abf 𝔊 CFCF a'b'f'"
        by auto
      with assms show "g f b c a.
        GF = [g, f]  g : b 𝔊 CFCF c  f : a 𝔊 CFCF b"
        by auto
    qed (use assms in cs_concl cs_shallow cs_intro: cat_comma_composableI)
    from assms show "𝒟 (𝔊 CFCF CId) = 𝔊 CFCF Obj"
      by (cs_concl cs_shallow cs_simp: cat_comma_cs_simps)
    from assms show "G A𝔊 CFCF F : A 𝔊 CFCF C"
      if "G : B 𝔊 CFCF C" and "F : A 𝔊 CFCF B"
      for B C G A F
      using that by (cs_concl cs_shallow cs_intro: cat_comma_cs_intros)
    from assms show 
      "H A𝔊 CFCF G A𝔊 CFCF F =
        H A𝔊 CFCF (G A𝔊 CFCF F)"
      if "H : C 𝔊 CFCF D"
        and "G : B 𝔊 CFCF C"
        and "F : A 𝔊 CFCF B"
      for C D H B G A F
      using assms that
    proof-
      from that(3) assms obtain a b f a' b' f' g h
        where F_def: "F = [[a, b, f], [a', b', f'], [g, h]]"
          and A_def: "A = [a, b, f]"
          and B_def: "B = [a', b', f']"
          and g: "g : a 𝔄a'"
          and h: "h : b 𝔅b'"
          and f: "f : 𝔊ObjMapa ObjMapb"
          and f': "f' : 𝔊ObjMapa' ObjMapb'"
          and [cat_cs_simps]: "f' A𝔊ArrMapg = ArrMaph Af"
        by auto
      with that(2) assms obtain a'' b'' f'' g' h'
        where G_def: "G = [[a', b', f'], [a'', b'', f''], [g', h']]"
          and C_def: "C = [a'', b'', f'']"
          and g': "g' : a' 𝔄a''"
          and h': "h' : b' 𝔅b''"
          and f'': "f'' : 𝔊ObjMapa'' ObjMapb''"
          and [cat_cs_simps]: 
            "f'' A𝔊ArrMapg' = ArrMaph' Af'"
        by auto (*slow*)
      with that(1) assms obtain a''' b''' f''' g'' h''
        where H_def: "H = [[a'', b'', f''], [a''', b''', f'''], [g'', h'']]"
          and D_def: "D = [a''', b''', f''']"
          and g'': "g'' : a'' 𝔄a'''"
          and h'': "h'' : b'' 𝔅b'''"
          and f''': "f''' : 𝔊ObjMapa''' ObjMapb'''"
          and [cat_cs_simps]: 
            "f''' A𝔊ArrMapg'' = ArrMaph'' Af''"
        by auto (*slow*)      
      note [cat_cs_simps] =
        category.cat_assoc_helper[
          where=
            and h=f''
            and g=𝔊ArrMapg'
            and q=ArrMaph' Af'
          ]
        category.cat_assoc_helper[
          where=
            and h=f''
            and g=𝔊ArrMapg'
            and q=ArrMaph' Af'
          ]
        category.cat_assoc_helper[
          where= 
            and h=f''' 
            and g=𝔊ArrMapg'' 
            and q=ArrMaph'' Af''
          ]
      from assms that g h f f' g' h' f'' g'' h''  f''' show ?thesis
        unfolding F_def G_def H_def A_def B_def C_def D_def
        by
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_comma_cs_simps 
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
    qed

    show "𝔊 CFCF CIdA : A 𝔊 CFCF A"
      if "A  𝔊 CFCF Obj" for A
      using that
      by (elim cat_comma_ObjE[OF _ assms(1)]; (simp only:)?) 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_comma_cs_simps 
            cs_intro: cat_cs_intros cat_comma_cs_intros
        )+

    show "𝔊 CFCF CIdB A𝔊 CFCF F = F"
      if "F : A 𝔊 CFCF B" for A B F
      using that 
      by (elim cat_comma_is_arrE[OF _ assms]; (simp only:)?)
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_comma_cs_simps 
            cs_intro: cat_cs_intros cat_comma_cs_intros
        )+

    show "F A𝔊 CFCF 𝔊 CFCF CIdB = F"
      if "F : B 𝔊 CFCF C" for B C F
      using that 
      by (elim cat_comma_is_arrE[OF _ assms]; (simp only:)?)
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_comma_cs_simps 
            cs_intro: cat_cs_intros cat_comma_cs_intros
        )+

    show "𝔊 CFCF Obj  Vset α"
    proof(intro vsubsetI, elim cat_comma_ObjE[OF _ assms])
      fix F a b f assume prems: 
        "F = [a, b, f]" 
        "a  𝔄Obj" 
        "b  𝔅Obj"
        "f : 𝔊ObjMapa ObjMapb"
      from prems(2-4) show "F  Vset α"
        unfolding prems(1) by (cs_concl cs_intro: cat_cs_intros V_cs_intros) 
    qed

    show "(aA. bB. Hom (𝔊 CFCF ) a b)  Vset α"
      if "A  𝔊 CFCF Obj"
        and "B  𝔊 CFCF Obj"
        and "A  Vset α"
        and "B  Vset α"
      for A B
    proof-

      define A0 where "A0 =  (λFA. F0)"
      define A1 where "A1 =  (λFA. F1)"
      define B0 where "B0 =  (λFB. F0)"
      define B1 where "B1 =  (λFB. F1)"

      define A0B0 where "A0B0 = (aA0. bB0. Hom 𝔄 a b)"
      define A1B1 where "A1B1 = (aA1. bB1. Hom 𝔅 a b)"

      have A0B0: "A0B0  Vset α"
        unfolding A0B0_def
      proof(rule 𝔊.HomDom.cat_Hom_vifunion_in_Vset; (intro vsubsetI)?)
        show "A0  Vset α"
          unfolding A0_def
        proof(intro vrange_vprojection_in_VsetI that(3))
          fix F assume "F  A"
          with that(1) have "F  𝔊 CFCF Obj" by auto
          with assms obtain a b f where F_def: "F = [a, b, f]" by auto
          show "vsv F" unfolding F_def by auto
          show "0  𝒟 F" unfolding F_def by simp
        qed auto
        show "B0  Vset α"
          unfolding B0_def
        proof(intro vrange_vprojection_in_VsetI that(4))
          fix F assume "F  B"
          with that(2) have "F  𝔊 CFCF Obj" by auto
          with assms obtain a b f where F_def: "F = [a, b, f]" by auto
          show "vsv F" unfolding F_def by auto
          show "0  𝒟 F" unfolding F_def by simp
        qed auto
      next
        fix a assume "a  A0"
        with that(1) obtain F 
          where a_def: "a = F0" and "F  𝔊 CFCF Obj" 
          unfolding A0_def by force
        with assms obtain b f where "F = [a, b, f]" and "a  𝔄Obj" by auto
        then show "a  𝔄Obj" unfolding a_def by simp
      next
        fix a assume "a  B0"
        with that(2) obtain F 
          where a_def: "a = F0" and "F  𝔊 CFCF Obj" 
          unfolding B0_def by force
        with assms obtain b f where "F = [a, b, f]" and "a  𝔄Obj" by auto
        then show "a  𝔄Obj" unfolding a_def by simp
      qed

      have A1B1: "A1B1  Vset α"
        unfolding A1B1_def
      proof(rule 𝔉.HomDom.cat_Hom_vifunion_in_Vset; (intro vsubsetI)?)
        show "A1  Vset α"
          unfolding A1_def
        proof(intro vrange_vprojection_in_VsetI that(3))
          fix F assume "F  A"
          with that(1) have "F  𝔊 CFCF Obj" by auto
          with assms obtain a b f where F_def: "F = [a, b, f]" by auto
          show "vsv F" unfolding F_def by auto
          show "1  𝒟 F" unfolding F_def by (simp add: nat_omega_simps)
        qed auto
        show "B1  Vset α"
          unfolding B1_def
        proof(intro vrange_vprojection_in_VsetI that(4))
          fix F assume "F  B"
          with that(2) have "F  𝔊 CFCF Obj" by auto
          with assms obtain a b f where F_def: "F = [a, b, f]" by auto
          show "vsv F" unfolding F_def by auto
          show "1  𝒟 F" unfolding F_def by (simp add: nat_omega_simps)
        qed auto
      next
        fix b assume "b  A1"
        with that(1) obtain F 
          where b_def: "b = F1" and "F  𝔊 CFCF Obj" 
          unfolding A1_def by force
        with assms obtain a f where "F = [a, b, f]" and "b  𝔅Obj" 
          by (auto simp: nat_omega_simps)
        then show "b  𝔅Obj" unfolding b_def by simp
      next
        fix b assume "b  B1"
        with that(2) obtain F 
          where b_def: "b = F1" and "F  𝔊 CFCF Obj" 
          unfolding B1_def by force
        with assms obtain a f where "F = [a, b, f]" and "b  𝔅Obj" 
          by (auto simp: nat_omega_simps)
        then show "b  𝔅Obj" unfolding b_def by simp
      qed
      
      define Q where 
        "Q i = (if i = 0 then A else if i = 1 then B else (A0B0 × A1B1))" 
        for i
      have 
        "(aA. bB.
          Hom (𝔊 CFCF ) a b)  (i set {0, 1, 2}. Q i)"
      proof
        (
          intro vsubsetI,
          elim vifunionE,
          unfold in_Hom_iff,
          intro vproductI ballI
        )
        fix abf a'b'f' F assume prems: 
          "abf  A" "a'b'f'  B" "F : abf 𝔊 CFCF a'b'f'"
        from prems(3) assms obtain a b f a' b' f' g h
          where F_def: "F = [[a, b, f], [a', b', f'], [g, h]]"
            and abf_def: "abf = [a, b, f]"
            and a'b'f'_def: "a'b'f' = [a', b', f']"
            and g: "g : a 𝔄a'"
            and h: "h : b 𝔅b'"
            and "f : 𝔊ObjMapa ObjMapb"
            and "f' : 𝔊ObjMapa' ObjMapb'"
            and "f' A𝔊ArrMapg = ArrMaph Af"
          by auto
        have gh: "[g, h]  A0B0 × A1B1"
          unfolding A0B0_def A1B1_def 
        proof
          (
            intro ftimesI2 vifunionI, 
            unfold in_Hom_iff A0_def B0_def A1_def B1_def
          )
          from prems(1) show "a   (λFA. F0)"
            by (intro vsv.vsv_vimageI2'[where a=abf]) (simp_all add: abf_def)
          from prems(2) show "a'   (λFB. F0)"
            by (intro vsv.vsv_vimageI2'[where a=a'b'f']) 
              (simp_all add: a'b'f'_def)
          from prems(1) show "b   (λFA. F1)"
            by (intro vsv.vsv_vimageI2'[where a=abf]) 
              (simp_all add: nat_omega_simps abf_def)
          from prems(2) show "b'   (λFB. F1)"
            by (intro vsv.vsv_vimageI2'[where a=a'b'f']) 
              (simp_all add: nat_omega_simps a'b'f'_def)
        qed (intro g h)+
        show "vsv F" unfolding F_def by auto
        show "𝒟 F = set {0, 1, 2}"
          by (simp add: F_def three nat_omega_simps)
        fix i assume "i  set {0, 1, 2}"
        then consider i = 0 | i = 1 | i = 2 by auto
        from this prems show "Fi  Q i" 
          by cases
            (simp_all add: F_def Q_def gh abf_def a'b'f'_def nat_omega_simps)
      qed
      moreover have "(i set {0, 1, 2}. Q i)  Vset α"
      proof(rule Limit_vproduct_in_VsetI)
        show "set {0, 1, 2}  Vset α" 
          by (cs_concl cs_shallow cs_intro: V_cs_intros)
        from A0B0 A1B1 assms(1,2) that(3,4) show 
          "Q i  Vset α" if "i  set {0, 1, 2}" 
          for i 
          by (simp_all add: Q_def Limit_ftimes_in_VsetI nat_omega_simps)
      qed auto
      ultimately show "(aA. bB. Hom (𝔊 CFCF ) a b)  Vset α" by auto
    qed
  qed (auto simp: cat_comma_cs_simps intro: cat_comma_cs_intros)

qed


subsubsection‹Tiny comma category›

lemma tiny_category_cat_comma[cat_comma_cs_intros]:
  assumes "𝔊 : 𝔄 ↦↦C.tmα" and " : 𝔅 ↦↦C.tmα"
  shows "tiny_category α (𝔊 CFCF )"
proof-

  interpret 𝔊: is_tm_functor α 𝔄  𝔊 by (rule assms(1))
  interpret: is_tm_functor α 𝔅   by (rule assms(2))
  note 𝔊 = 𝔊.is_functor_axioms 
    and  = ℌ.is_functor_axioms
  interpret category α 𝔊 CFCF 
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_comma_cs_intros)

  show ?thesis
  proof(intro tiny_categoryI' category_cat_comma)
    have vrange_𝔊: " (𝔊ObjMap)  Vset α"
      by (simp add: vrange_in_VsetI 𝔊.tm_cf_ObjMap_in_Vset)
    moreover have vrange_ℌ: " (ObjMap)  Vset α"
      by (simp add: vrange_in_VsetI ℌ.tm_cf_ObjMap_in_Vset)
    ultimately have UU_Hom_in_Vset:
      "(a (𝔊ObjMap). b (ObjMap). Hom  a b)  Vset α"
      using 𝔊.cf_ObjMap_vrange ℌ.cf_ObjMap_vrange 
      by (auto intro: 𝔊.HomCod.cat_Hom_vifunion_in_Vset) 
    define Q where
      "Q i =
        (
          if i = 0
          then 𝔄Obj
          else
            if i = 1
            then 𝔅Obj
            else (a (𝔊ObjMap). b (ObjMap). Hom  a b)
        )" 
      for i
    have "𝔊 CFCF Obj  (i set {0, 1, 2}. Q i)"
    proof(intro vsubsetI)
      fix A assume "A  𝔊 CFCF Obj"
      then obtain a b f
        where A_def: "A = [a, b, f]"
          and a: "a  𝔄Obj"
          and b: "b  𝔅Obj"
          and f: "f : 𝔊ObjMapa ObjMapb"
        by (elim cat_comma_ObjE[OF _ 𝔊 ])
      from f have f:
        "f  (a (𝔊ObjMap). b (ObjMap). Hom  a b)"
        by (intro vifunionI, unfold in_Hom_iff)
          (
            simp_all add: 
              a b 
              ℌ.ObjMap.vsv_vimageI2 
              ℌ.cf_ObjMap_vdomain 
              𝔊.ObjMap.vsv_vimageI2 
              𝔊.cf_ObjMap_vdomain
          )
      show "A  (i set {0, 1, 2}. Q i)"
      proof(intro vproductI, unfold Ball_def; (intro allI impI)?)
        show "𝒟 A = set {0, 1, 2}"
          unfolding A_def by (simp add: three nat_omega_simps)
        fix i assume "i  set {0, 1, 2}"
        then consider i = 0 | i = 1 | i = 2 by auto
        from this a b f show "Ai  Q i"
          unfolding A_def Q_def by cases (simp_all add: nat_omega_simps)
      qed (auto simp: A_def)
    qed
    moreover have "(i set {0, 1, 2}. Q i)  Vset α"
    proof(rule Limit_vproduct_in_VsetI)
      show "set {0, 1, 2}  Vset α"
        unfolding three[symmetric] by simp
      from this show "Q i  Vset α" if "i  set {0, 1, 2}" for i
        using that assms(1,2) UU_Hom_in_Vset  
        by 
          (
            simp_all add:
              Q_def 
              𝔊.HomDom.tiny_cat_Obj_in_Vset 
              ℌ.HomDom.tiny_cat_Obj_in_Vset 
              nat_omega_simps
          )
    qed auto
    ultimately show [simp]: "𝔊 CFCF Obj  Vset α" by auto 
    define Q where
      "Q i =
        (
          if i = 0
          then 𝔊 CFCF Obj
          else
            if i = 1
            then 𝔊 CFCF Obj
            else 𝔄Arr × 𝔅Arr
        )" 
    for i
    have "𝔊 CFCF Arr  (i set {0, 1, 2}. Q i)"
    proof(intro vsubsetI)
      fix F assume "F  𝔊 CFCF Arr"
      then obtain abf a'b'f' where F: "F : abf 𝔊 CFCF a'b'f'"
        by (auto intro: is_arrI)
      with assms obtain a b f a' b' f' g h
        where F_def: "F = [[a, b, f], [a', b', f'], [g, h]]"
          and abf_def: "abf = [a, b, f]"
          and a'b'f'_def: "a'b'f' = [a', b', f']"
          and g: "g : a 𝔄a'"
          and h: "h : b 𝔅b'"
          and "f : 𝔊ObjMapa ObjMapb"
          and "f' : 𝔊ObjMapa' ObjMapb'"
          and "f' A𝔊ArrMapg = ArrMaph Af"
        by auto
      from g h have "[g, h]  𝔄Arr × 𝔅Arr" by auto      
      show "F  (i set {0, 1, 2}. Q i)"
      proof(intro vproductI, unfold Ball_def; (intro allI impI)?)
        show "𝒟 F = set {0, 1, 2}"
          by (simp add: F_def three nat_omega_simps)
        fix i assume "i  set {0, 1, 2}"
        then consider i = 0 | i = 1 | i = 2 by auto
        from this F g h show "Fi  Q i"
          unfolding Q_def F_def abf_def[symmetric] a'b'f'_def[symmetric]
          by cases (auto simp: nat_omega_simps)
      qed (auto simp: F_def)
    qed
    moreover have "(i set {0, 1, 2}. Q i)  Vset α"
    proof(rule Limit_vproduct_in_VsetI)
      show "set {0, 1, 2}  Vset α"
        by (simp add: three[symmetric] nat_omega_simps)
      moreover have "𝔄Arr × 𝔅Arr  Vset α"
        by 
          (
            auto intro!: 
              Limit_ftimes_in_VsetI 
              𝔊.𝒵_β 𝒵_def 
              𝔊.HomDom.tiny_cat_Arr_in_Vset 
              ℌ.HomDom.tiny_cat_Arr_in_Vset
          )
      ultimately show "Q i  Vset α" if "i  set {0, 1, 2}" for i
        using that assms(1,2) UU_Hom_in_Vset  
        by 
          (
            simp_all add:
              Q_def
              𝔊.HomDom.tiny_cat_Obj_in_Vset 
              ℌ.HomDom.tiny_cat_Obj_in_Vset 
              nat_omega_simps
          )
    qed auto
    ultimately show "𝔊 CFCF Arr  Vset α" by auto
  qed (rule 𝔊, rule )

qed



subsection‹Opposite comma category functor›


subsubsection‹Background›


text‹
See cite"noauthor_wikipedia_2001"\footnote{
\url{https://en.wikipedia.org/wiki/Opposite_category}
} for background information.
›


subsubsection‹Object flip›

definition op_cf_commma_obj_flip :: "V  V  V"
  where "op_cf_commma_obj_flip 𝔊  =
    (λA(𝔊 CFCF )Obj. [A1, A0, A2])"


text‹Elementary properties.›

mk_VLambda op_cf_commma_obj_flip_def
  |vsv op_cf_commma_obj_flip_vsv[cat_comma_cs_intros]|
  |vdomain op_cf_commma_obj_flip_vdomain[cat_comma_cs_simps]|
  |app op_cf_commma_obj_flip_app'|

lemma op_cf_commma_obj_flip_app[cat_comma_cs_simps]:
  assumes "A = [a, b, f]" and "A  (𝔊 CFCF )Obj"
  shows "op_cf_commma_obj_flip 𝔊 A = [b, a, f]"
  using assms unfolding op_cf_commma_obj_flip_def by (simp add: nat_omega_simps)

lemma op_cf_commma_obj_flip_v11[cat_comma_cs_intros]:
  assumes "𝔊 : 𝔄 ↦↦Cα" and " : 𝔅 ↦↦Cα"
  shows "v11 (op_cf_commma_obj_flip 𝔊 )"
proof(rule vsv.vsv_valeq_v11I, unfold op_cf_commma_obj_flip_vdomain)
  fix A B assume prems:
    "A  𝔊 CFCF Obj"
    "B  𝔊 CFCF Obj"
    "op_cf_commma_obj_flip 𝔊 A = op_cf_commma_obj_flip 𝔊 B"
  from prems(1,2) assms obtain a b f a' b' f' 
    where A_def: "A = [a, b, f]" 
      and B_def: "B = [a', b', f']"
    by (elim cat_comma_ObjE[OF _ assms])
  from prems(3,1,2) show "A = B"
    by (simp_all add: A_def B_def op_cf_commma_obj_flip_app nat_omega_simps)
qed (auto intro: op_cf_commma_obj_flip_vsv)

lemma op_cf_commma_obj_flip_vrange[cat_comma_cs_simps]:
  assumes "𝔊 : 𝔄 ↦↦Cα" and " : 𝔅 ↦↦Cα"
  shows " (op_cf_commma_obj_flip 𝔊 ) = (op_cf ) CFCF (op_cf 𝔊)Obj"
proof(intro vsubset_antisym)
  interpret 𝔊: is_functor α 𝔄  𝔊 by (rule assms(1))
  interpret: is_functor α 𝔅   by (rule assms(2))
  show " (op_cf_commma_obj_flip 𝔊 )  (op_cf ) CFCF (op_cf 𝔊)Obj"
  proof
    (
      intro vsv.vsv_vrange_vsubset op_cf_commma_obj_flip_vsv, 
      unfold cat_comma_cs_simps
    )
    fix A assume "A  𝔊 CFCF Obj"
    then obtain a b f
      where A_def: "A = [a, b, f]"
        and a: "a  𝔄Obj"
        and b: "b  𝔅Obj"
        and f: "f : 𝔊ObjMapa ObjMapb"
      by (elim cat_comma_ObjE[OF _ assms])
    from a b f show 
      "op_cf_commma_obj_flip 𝔊 A  (op_cf ) CFCF (op_cf 𝔊)Obj"
      unfolding A_def
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_comma_cs_simps cat_op_simps 
            cs_intro: cat_cs_intros cat_comma_cs_intros cat_op_intros
        )
  qed
  show "(op_cf ) CFCF (op_cf 𝔊)Obj   (op_cf_commma_obj_flip 𝔊 )"
  proof(intro vsubsetI)
    fix B assume "B  (op_cf ) CFCF (op_cf 𝔊)Obj"
    then obtain a b f
      where B_def: "B = [b, a, f]"
        and b: "b  𝔅Obj"
        and a: "a  𝔄Obj"
        and f: "f : 𝔊ObjMapa ObjMapb"
      by 
        (
          elim cat_comma_ObjE[
            OF _ ℌ.is_functor_op 𝔊.is_functor_op, unfolded cat_op_simps
            ]
        )
    from a b f have B_def: "B = op_cf_commma_obj_flip 𝔊 a, b, f"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_comma_cs_simps B_def
            cs_intro: cat_cs_intros cat_comma_cs_intros
        )
    from a b f have "[a, b, f]  𝒟 (op_cf_commma_obj_flip 𝔊 )"
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_comma_cs_simps
            cs_intro: cat_cs_intros cat_comma_cs_intros
        )
    with op_cf_commma_obj_flip_vsv show "B   (op_cf_commma_obj_flip 𝔊 )"
      unfolding B_def by auto
  qed
qed


subsubsection‹Definition and elementary properties›

definition op_cf_comma :: "V  V  V"
  where "op_cf_comma 𝔊