Theory CZH_UCAT_PWKan_Example

(* Copyright 2021 (C) Mihails Milehins *)

section‹Pointwise Kan extensions: application example›
theory CZH_UCAT_PWKan_Example
  imports
    CZH_Elementary_Categories.CZH_ECAT_Ordinal
    CZH_UCAT_PWKan
begin



subsection‹Background›


text‹
The application example presented in this section is based on 
Exercise 6.1.ii in cite‹"riehl_category_2016"›. The primary purpose
of this section is the instantiation of the locales associated
with the pointwise Kan extensions.
›

(*TODO: is the explicit elimination rule necessary?*)
lemma cat_ordinal_2_is_arrE:
  assumes "f : a ↦⇘cat_ordinal (2ℕ)⇙ b"
  obtains "f = [0, 0]∘" and "a = 0" and "b = 0" 
    | "f = [0, 1ℕ]∘" and "a = 0" and "b = 1ℕ"
    | "f = [1ℕ, 1ℕ]∘" and "a = 1ℕ" and "b = 1ℕ"
  using cat_ordinal_is_arrD[OF assms] unfolding two by auto

(*TODO: is the explicit elimination rule necessary?*)
lemma cat_ordinal_3_is_arrE:
  assumes "f : a ↦⇘cat_ordinal (3ℕ)⇙ b"
  obtains "f = [0, 0]∘" and " a = 0" and "b = 0" 
    | "f = [0, 1ℕ]∘" and "a = 0" and "b = 1ℕ"
    | "f = [0, 2ℕ]∘" and "a = 0" and "b = 2ℕ"
    | "f = [1ℕ, 1ℕ]∘" and "a = 1ℕ" and "b = 1ℕ"
    | "f = [1ℕ, 2ℕ]∘" and "a = 1ℕ" and "b = 2ℕ"
    | "f = [2ℕ, 2ℕ]∘" and "a = 2ℕ" and "b = 2ℕ"
  using cat_ordinal_is_arrD[OF assms] unfolding three by auto

lemma 0123: "0 ∈∘ 2ℕ" "1ℕ ∈∘ 2ℕ" "0 ∈∘ 3ℕ" "1ℕ ∈∘ 3ℕ" "2ℕ ∈∘ 3ℕ" by auto



subsection‹‹𝔎23››


subsubsection‹Definition and elementary properties›

definition 𝔎23 :: V
  where "𝔎23 =
    [
      (λa∈∘cat_ordinal (2ℕ)⦇Obj⦈. if a = 0 then 0 else 2ℕ), 
      (
        λf∈∘cat_ordinal (2ℕ)⦇Arr⦈.
         if f = [0, 0]∘ ⇒ [0, 0]∘
          | f = [0, 1ℕ]∘ ⇒ [0, 2ℕ]∘
          | f = [1ℕ, 1ℕ]∘ ⇒ [2ℕ, 2ℕ]∘
          | otherwise ⇒ 0
      ), 
      cat_ordinal (2ℕ),
      cat_ordinal (3ℕ)
    ]∘"


text‹Components.›

lemma 𝔎23_components:
  shows "𝔎23⦇ObjMap⦈ = (λa∈∘cat_ordinal (2ℕ)⦇Obj⦈. if a = 0 then 0 else 2ℕ)"
    and "𝔎23⦇ArrMap⦈ =
      (
        λf∈∘cat_ordinal (2ℕ)⦇Arr⦈.
         if f = [0, 0]∘ ⇒ [0, 0]∘
          | f = [0, 1ℕ]∘ ⇒ [0, 2ℕ]∘
          | f = [1ℕ, 1ℕ]∘ ⇒ [2ℕ, 2ℕ]∘
          | otherwise ⇒ 0
      )"
    and [cat_Kan_cs_simps]: "𝔎23⦇HomDom⦈ = cat_ordinal (2ℕ)"
    and [cat_Kan_cs_simps]: "𝔎23⦇HomCod⦈ = cat_ordinal (3ℕ)"
  unfolding 𝔎23_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda 𝔎23_components(1)
  |vsv 𝔎23_ObjMap_vsv[cat_Kan_cs_intros]|
  |vdomain 𝔎23_ObjMap_vdomain[cat_Kan_cs_simps]|
  |app 𝔎23_ObjMap_app|

lemma 𝔎23_ObjMap_app_0[cat_Kan_cs_simps]: 
  assumes "x = 0"
  shows "𝔎23⦇ObjMap⦈⦇x⦈ = 0"
  by 
    (
      cs_concl 
        cs_simp: 𝔎23_ObjMap_app cat_ordinal_cs_simps V_cs_simps assms 
        cs_intro: nat_omega_intros
    )

lemma 𝔎23_ObjMap_app_1[cat_Kan_cs_simps]: 
  assumes "x = 1ℕ"
  shows "𝔎23⦇ObjMap⦈⦇x⦈ = 2ℕ"
  by 
    (
      cs_concl  
        cs_simp: 
          cat_ordinal_cs_simps V_cs_simps omega_of_set 𝔎23_ObjMap_app assms
        cs_intro: nat_omega_intros V_cs_intros
    )


subsubsection‹Arrow map›

mk_VLambda 𝔎23_components(2)
  |vsv 𝔎23_ArrMap_vsv[cat_Kan_cs_intros]|
  |vdomain 𝔎23_ArrMap_vdomain[cat_Kan_cs_simps]|
  |app 𝔎23_ArrMap_app|

lemma 𝔎23_ArrMap_app_00[cat_Kan_cs_simps]: 
  assumes "f = [0, 0]∘"
  shows "𝔎23⦇ArrMap⦈⦇f⦈ = [0, 0]∘"
  unfolding assms
  by 
    (
      cs_concl  
        cs_simp: 𝔎23_ArrMap_app cat_ordinal_cs_simps V_cs_simps 
        cs_intro: cat_ordinal_cs_intros nat_omega_intros
    )

lemma 𝔎23_ArrMap_app_01[cat_Kan_cs_simps]: 
  assumes "f = [0, 1ℕ]∘"
  shows "𝔎23⦇ArrMap⦈⦇f⦈ = [0, 2ℕ]∘"
proof-
  have "[0, 1ℕ]∘ ∈∘ ordinal_arrs (2ℕ)"
    by 
      (
        cs_concl  
          cs_simp: omega_of_set 
          cs_intro: cat_ordinal_cs_intros V_cs_intros nat_omega_intros
      )
  then show ?thesis
    unfolding assms by (simp add: 𝔎23_components cat_ordinal_components)
qed

lemma 𝔎23_ArrMap_app_11[cat_Kan_cs_simps]: 
  assumes "f = [1ℕ, 1ℕ]∘"
  shows "𝔎23⦇ArrMap⦈⦇f⦈ = [2ℕ, 2ℕ]∘"
proof-
  have "[1ℕ, 1ℕ]∘ ∈∘ ordinal_arrs (2ℕ)"
    by 
      (
        cs_concl cs_shallow
          cs_simp: omega_of_set 
          cs_intro: cat_ordinal_cs_intros V_cs_intros nat_omega_intros
      )
  then show ?thesis
    unfolding assms by (simp add: 𝔎23_components cat_ordinal_components)
qed


subsubsection‹‹𝔎23› is a tiny functor›

lemma (in 𝒵) 𝔎23_is_functor: "𝔎23 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ cat_ordinal (3ℕ)"
proof-

  from ord_of_nat_ω interpret cat_ordinal_2: finite_category α ‹cat_ordinal (2ℕ)›
    by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
  from ord_of_nat_ω interpret cat_ordinal_3: finite_category α ‹cat_ordinal (3ℕ)›
    by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)

  show ?thesis
  proof(intro is_tiny_functorI' is_functorI')

    show "vfsequence 𝔎23" unfolding 𝔎23_def by auto
    show "vcard 𝔎23 = 4ℕ" unfolding 𝔎23_def by (simp add: nat_omega_simps)

    show "ℛ∘ (𝔎23⦇ObjMap⦈) ⊆∘ cat_ordinal (3ℕ)⦇Obj⦈"
    proof
      (
        rule vsv.vsv_vrange_vsubset, 
        unfold cat_Kan_cs_simps cat_ordinal_cs_simps, 
        intro cat_Kan_cs_intros
      )
      fix x assume "x ∈∘ 2ℕ"
      then consider ‹x = 0› | ‹x = 1ℕ› unfolding two by auto
      then show "𝔎23⦇ObjMap⦈⦇x⦈ ∈∘ 3ℕ"
        by (cases, use nothing in ‹simp_all only:›)
          (
            cs_concl 
              cs_simp: cat_Kan_cs_simps omega_of_set cs_intro: nat_omega_intros
          )+
    qed

    show "𝔎23⦇ArrMap⦈⦇f⦈ : 𝔎23⦇ObjMap⦈⦇a⦈ ↦⇘cat_ordinal (3ℕ)⇙ 𝔎23⦇ObjMap⦈⦇b⦈"
      if "f : a ↦⇘cat_ordinal (2ℕ)⇙ b" for a b f
      using that 
      by (elim cat_ordinal_2_is_arrE; simp only:) 
        (
          cs_concl 
            cs_simp: omega_of_set cat_Kan_cs_simps
            cs_intro: nat_omega_intros V_cs_intros cat_ordinal_cs_intros
        )

    show 
      "𝔎23⦇ArrMap⦈⦇g ∘A⇘cat_ordinal (2ℕ)⇙ f⦈ =
        𝔎23⦇ArrMap⦈⦇g⦈ ∘A⇘cat_ordinal (3ℕ)⇙ 𝔎23⦇ArrMap⦈⦇f⦈"
      if "g : b ↦⇘cat_ordinal (2ℕ)⇙ c" and "f : a ↦⇘cat_ordinal (2ℕ)⇙ b"
      for b c g a f 
    proof-
      have "0 ∈∘ 3ℕ" "1ℕ ∈∘ 3ℕ" "2ℕ ∈∘ 3ℕ" by auto
      then show ?thesis
        using that
        by (elim cat_ordinal_2_is_arrE; simp only:)
          (
            cs_concl  
              cs_simp: cat_ordinal_cs_simps cat_Kan_cs_simps  
              cs_intro: V_cs_intros cat_ordinal_cs_intros
          )+    
    qed

    show 
      "𝔎23⦇ArrMap⦈⦇cat_ordinal (2ℕ)⦇CId⦈⦇c⦈⦈ =
        cat_ordinal (3ℕ)⦇CId⦈⦇𝔎23⦇ObjMap⦈⦇c⦈⦈"
      if "c ∈∘ cat_ordinal (2ℕ)⦇Obj⦈" for c
    proof-
      from that consider ‹c = 0› | ‹c = 1ℕ›
        unfolding cat_ordinal_components(1) two by auto
      then show ?thesis
        by (cases, use nothing in ‹simp_all only:›) 
          (
            cs_concl 
              cs_simp: omega_of_set cat_Kan_cs_simps cat_ordinal_cs_simps  
              cs_intro: nat_omega_intros cat_ordinal_cs_intros
          )
    qed

  qed (auto intro!: cat_cs_intros simp: 𝔎23_components)

qed

lemma (in 𝒵) 𝔎23_is_functor'[cat_Kan_cs_intros]:
  assumes "𝔄' = cat_ordinal (2ℕ)"
    and "𝔅' = cat_ordinal (3ℕ)"
  shows "𝔎23 : 𝔄' ↦↦C⇘α⇙ 𝔅'"
  unfolding assms by (rule 𝔎23_is_functor)

lemmas [cat_Kan_cs_intros] = 𝒵.𝔎23_is_functor'

lemma (in 𝒵) 𝔎23_is_tiny_functor: 
  "𝔎23 : cat_ordinal (2ℕ) ↦↦C.tiny⇘α⇙ cat_ordinal (3ℕ)"
proof-
  from ord_of_nat_ω interpret cat_ordinal_2: finite_category α ‹cat_ordinal (2ℕ)›
    by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
  from ord_of_nat_ω interpret cat_ordinal_3: finite_category α ‹cat_ordinal (3ℕ)›
    by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
  show ?thesis
    by (intro is_tiny_functorI' 𝔎23_is_functor)
      (auto intro!: cat_small_cs_intros)
qed

lemma (in 𝒵) 𝔎23_is_tiny_functor'[cat_Kan_cs_intros]:
  assumes "𝔄' = cat_ordinal (2ℕ)"
    and "𝔅' = cat_ordinal (3ℕ)"
  shows "𝔎23 : 𝔄' ↦↦C.tiny⇘α⇙ 𝔅'"
  unfolding assms by (rule 𝔎23_is_tiny_functor)

lemmas [cat_Kan_cs_intros] = 𝒵.𝔎23_is_tiny_functor'



subsection‹
‹LK23›: the functor associated with the left Kan extension along const‹𝔎23›
›


subsubsection‹Definition and elementary properties›

definition LK23 :: "V ⇒ V"
  where "LK23 𝔉 =
    [
      (
        λa∈∘cat_ordinal (3ℕ)⦇Obj⦈.
         if a = 0 ⇒ 𝔉⦇ObjMap⦈⦇0⦈
          | a = 1ℕ ⇒ 𝔉⦇ObjMap⦈⦇0⦈
          | a = 2ℕ ⇒ 𝔉⦇ObjMap⦈⦇1ℕ⦈
          | otherwise ⇒ 𝔉⦇HomCod⦈⦇Obj⦈
      ), 
      (
        λf∈∘cat_ordinal (3ℕ)⦇Arr⦈.
         if f = [0, 0]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈∙
          | f = [0, 1ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈∙
          | f = [0, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙
          | f = [1ℕ, 1ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈∙
          | f = [1ℕ, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙
          | f = [2ℕ, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙
          | otherwise ⇒ 𝔉⦇HomCod⦈⦇Arr⦈
      ), 
      cat_ordinal (3ℕ),
      𝔉⦇HomCod⦈
    ]∘"


text‹Components.›

lemma LK23_components:
  shows "LK23 𝔉⦇ObjMap⦈ =
    (
      λa∈∘cat_ordinal (3ℕ)⦇Obj⦈.
        if a = 0 ⇒ 𝔉⦇ObjMap⦈⦇0⦈
         | a = 1ℕ ⇒ 𝔉⦇ObjMap⦈⦇0⦈
         | a = 2ℕ ⇒ 𝔉⦇ObjMap⦈⦇1ℕ⦈
         | otherwise ⇒ 𝔉⦇HomCod⦈⦇Obj⦈
    )"
    and "LK23 𝔉⦇ArrMap⦈ =
      (
        λf∈∘cat_ordinal (3ℕ)⦇Arr⦈.
         if f = [0, 0]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈∙
          | f = [0, 1ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈∙
          | f = [0, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙
          | f = [1ℕ, 1ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈∙
          | f = [1ℕ, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙
          | f = [2ℕ, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙
          | otherwise ⇒ 𝔉⦇HomCod⦈⦇Arr⦈
      )"
    and "LK23 𝔉⦇HomDom⦈ = cat_ordinal (3ℕ)"
    and "LK23 𝔉⦇HomCod⦈ = 𝔉⦇HomCod⦈"
  unfolding LK23_def dghm_field_simps by (simp_all add: nat_omega_simps)

context is_functor
begin

lemmas LK23_components' = LK23_components[where 𝔉=𝔉, unfolded cat_cs_simps]

lemmas [cat_Kan_cs_simps] = LK23_components'(3,4)

end

lemmas [cat_Kan_cs_simps] = is_functor.LK23_components'(3,4)


subsubsection‹Object map›

mk_VLambda LK23_components(1)
  |vsv LK23_ObjMap_vsv[cat_Kan_cs_intros]|
  |vdomain LK23_ObjMap_vdomain[cat_Kan_cs_simps]|
  |app LK23_ObjMap_app|

lemma LK23_ObjMap_app_0[cat_Kan_cs_simps]:
  assumes "a = 0"
  shows "LK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇0⦈"
  unfolding LK23_components assms cat_ordinal_components by simp

lemma LK23_ObjMap_app_1[cat_Kan_cs_simps]:
  assumes "a = 1ℕ"
  shows "LK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇0⦈"
  unfolding LK23_components assms cat_ordinal_components by simp

lemma LK23_ObjMap_app_2[cat_Kan_cs_simps]:
  assumes "a = 2ℕ"
  shows "LK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇1ℕ⦈"
  unfolding LK23_components assms cat_ordinal_components by simp


subsubsection‹Arrow map›

mk_VLambda LK23_components(2)
  |vsv LK23_ArrMap_vsv[cat_Kan_cs_intros]|
  |vdomain LK23_ArrMap_vdomain[cat_Kan_cs_simps]|
  |app LK23_ArrMap_app|

lemma LK23_ArrMap_app_00[cat_Kan_cs_simps]:
  assumes "f = [0, 0]∘"
  shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 0⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_intro: V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding LK23_components assms by auto
qed

lemma LK23_ArrMap_app_01[cat_Kan_cs_simps]:
  assumes "f = [0, 1ℕ]∘"
  shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 0⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_intro: V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding LK23_components assms by auto
qed

lemma LK23_ArrMap_app_02[cat_Kan_cs_simps]:
  assumes "f = [0, 2ℕ]∘"
  shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_intro: V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding LK23_components assms by auto
qed

lemma LK23_ArrMap_app_11[cat_Kan_cs_simps]:
  assumes "f = [1ℕ, 1ℕ]∘"
  shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 0⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_intro: V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding LK23_components assms by auto
qed

lemma LK23_ArrMap_app_12[cat_Kan_cs_simps]:
  assumes "f = [1ℕ, 2ℕ]∘"
  shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl 
          cs_simp: omega_of_set   
          cs_intro: nat_omega_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding LK23_components assms by auto
qed

lemma LK23_ArrMap_app_22[cat_Kan_cs_simps]:
  assumes "f = [2ℕ, 2ℕ]∘"
  shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow
          cs_intro: nat_omega_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding LK23_components assms by simp
qed


subsubsection‹‹LK23› is a functor›

lemma cat_LK23_is_functor:
  assumes "𝔉 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ ℭ"
  shows "LK23 𝔉 : cat_ordinal (3ℕ) ↦↦C⇘α⇙ ℭ"
proof-

  interpret 𝔉: is_functor α ‹cat_ordinal (2ℕ)› ℭ 𝔉 by (rule assms(1))

  from ord_of_nat_ω interpret cat_ordinal_2: finite_category α ‹cat_ordinal (2ℕ)›
    by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
  from ord_of_nat_ω interpret cat_ordinal_3: finite_category α ‹cat_ordinal (3ℕ)›
    by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)

  interpret 𝔉: is_functor α ‹cat_ordinal (2ℕ)› ℭ 𝔉 by (rule assms)

  show ?thesis
  proof(intro is_functorI')
    show "vfsequence (LK23 𝔉)" unfolding LK23_def by auto
    show "vcard (LK23 𝔉) = 4ℕ" unfolding LK23_def by (simp add: nat_omega_simps)
    show "ℛ∘ (LK23 𝔉⦇ObjMap⦈) ⊆∘ ℭ⦇Obj⦈"
    proof(rule vsv.vsv_vrange_vsubset, unfold cat_Kan_cs_simps)
      fix x assume prems: "x ∈∘ cat_ordinal (3ℕ)⦇Obj⦈"
      then consider ‹x = 0› | ‹x = 1ℕ› | ‹x = 2ℕ›
        unfolding cat_ordinal_cs_simps three by auto
      then show "LK23 𝔉⦇ObjMap⦈⦇x⦈ ∈∘ ℭ⦇Obj⦈" 
        by cases
          (
            cs_concl 
              cs_simp: cat_Kan_cs_simps cat_ordinal_cs_simps omega_of_set 
              cs_intro: cat_cs_intros nat_omega_intros
          )+
    qed (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
    show "LK23 𝔉⦇ArrMap⦈⦇f⦈ : LK23 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ LK23 𝔉⦇ObjMap⦈⦇b⦈"
      if "f : a ↦⇘cat_ordinal (3ℕ)⇙ b" for a b f
    proof-
      from 0123 that show ?thesis
        by (elim cat_ordinal_3_is_arrE; simp only:)
          (
            cs_concl 
              cs_simp: cat_Kan_cs_simps
              cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
          )+
    qed
    show 
      "LK23 𝔉⦇ArrMap⦈⦇g ∘A⇘cat_ordinal (3ℕ)⇙ f⦈ =
        LK23 𝔉⦇ArrMap⦈⦇g⦈ ∘A⇘ℭ⇙ LK23 𝔉⦇ArrMap⦈⦇f⦈"
      if "g : b ↦⇘cat_ordinal (3ℕ)⇙ c" and "f : a ↦⇘cat_ordinal (3ℕ)⇙ b"
      for b c g a f
    proof-
      from 0123 that show ?thesis
        by (elim cat_ordinal_3_is_arrE; simp only:; (solves‹simp›)?) (*slow*)
          (
            cs_concl  
              cs_simp: 
                cat_ordinal_cs_simps 
                cat_Kan_cs_simps 
                𝔉.cf_ArrMap_Comp[symmetric]
              cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
          )+
    qed
    show "LK23 𝔉⦇ArrMap⦈⦇cat_ordinal (3ℕ)⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇LK23 𝔉⦇ObjMap⦈⦇c⦈⦈"
      if "c ∈∘ cat_ordinal (3ℕ)⦇Obj⦈" for c
    proof-
      from that consider ‹c = 0› | ‹c = 1ℕ› | ‹c = 2ℕ›
        unfolding cat_ordinal_components three by auto
      moreover have "0 ∈∘ 2ℕ" "1ℕ ∈∘ 2ℕ" "0 ∈∘ 3ℕ" "1ℕ ∈∘ 3ℕ" "2ℕ ∈∘ 3ℕ" by auto
      ultimately show ?thesis
        by (cases, use nothing in ‹simp_all only:›)
          (
            cs_concl 
              cs_simp: 
                cat_ordinal_cs_simps 
                cat_Kan_cs_simps 
                is_functor.cf_ObjMap_CId[symmetric]  
              cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
          )+
    qed
  qed 
    (
      cs_concl cs_shallow
        cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
    )+

qed

lemma cat_LK23_is_functor'[cat_Kan_cs_intros]:
  assumes "𝔉 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ ℭ"
    and "𝔄' = cat_ordinal (3ℕ)"
  shows "LK23 𝔉 : 𝔄' ↦↦C⇘α⇙ ℭ"
  using assms(1) unfolding assms(2) by (rule cat_LK23_is_functor)


subsubsection‹The fundamental property of ‹LK23››

lemma cf_comp_LK23_𝔎23[cat_Kan_cs_simps]: 
  assumes "𝔉 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ ℭ"
  shows "LK23 𝔉 ∘CF 𝔎23 = 𝔉"
proof-

  interpret 𝔉: is_functor α ‹cat_ordinal (2ℕ)› ℭ 𝔉 by (rule assms(1))
  interpret 𝔎23: is_functor α ‹cat_ordinal (2ℕ)› ‹cat_ordinal (3ℕ)› ‹𝔎23›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
  interpret LK23: is_functor α ‹cat_ordinal (3ℕ)› ℭ ‹LK23 𝔉›
    by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)

  show ?thesis
  proof(rule cf_eqI)
    show "𝔉 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ ℭ" by (rule assms)
    have ObjMap_dom_lhs: "𝒟∘ ((LK23 𝔉 ∘CF 𝔎23)⦇ObjMap⦈) = 2ℕ"
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_ordinal_cs_simps cs_intro: cat_cs_intros
        )
    have ObjMap_dom_rhs: "𝒟∘ (𝔉⦇ObjMap⦈) = 2ℕ"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
    show "(LK23 𝔉 ∘CF 𝔎23)⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
    proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
      fix a assume prems: "a ∈∘ 2ℕ"
      then consider ‹a = 0› | ‹a = 1ℕ› by force
      then show "(LK23 𝔉 ∘CF 𝔎23)⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇a⦈"
        by (cases, use nothing in ‹simp_all only:›)
          (
            cs_concl 
              cs_simp:
                omega_of_set cat_cs_simps cat_ordinal_cs_simps cat_Kan_cs_simps
              cs_intro: cat_cs_intros nat_omega_intros
          )+
    qed (cs_concl cs_intro: cat_cs_intros V_cs_intros)+
    have ArrMap_dom_lhs: "𝒟∘ ((LK23 𝔉 ∘CF 𝔎23)⦇ArrMap⦈) = cat_ordinal (2ℕ)⦇Arr⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    have ArrMap_dom_rhs: "𝒟∘ (𝔉⦇ArrMap⦈) = cat_ordinal (2ℕ)⦇Arr⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show "(LK23 𝔉 ∘CF 𝔎23)⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
    proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      fix f assume prems: "f ∈∘ cat_ordinal (2ℕ)⦇Arr⦈"
      then obtain a b where "f : a ↦⇘cat_ordinal (2ℕ)⇙ b" by auto
      then show "(LK23 𝔉 ∘CF 𝔎23)⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇f⦈"
        by (elim cat_ordinal_2_is_arrE; simp only:)
          (
            cs_concl
              cs_simp: cat_cs_simps cat_Kan_cs_simps cs_intro: cat_cs_intros
          )+
    qed (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros V_cs_intros)+
  qed (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)

qed



subsection‹
‹RK23›: the functor associated with the right Kan extension along const‹𝔎23›
›


subsubsection‹Definition and elementary properties›

definition RK23 :: "V ⇒ V"
  where "RK23 𝔉 =
    [
      (
        λa∈∘cat_ordinal (3ℕ)⦇Obj⦈.
         if a = 0 ⇒ 𝔉⦇ObjMap⦈⦇0⦈
          | a = 1ℕ ⇒ 𝔉⦇ObjMap⦈⦇1ℕ⦈
          | a = 2ℕ ⇒ 𝔉⦇ObjMap⦈⦇1ℕ⦈
          | otherwise ⇒ 𝔉⦇HomCod⦈⦇Obj⦈
      ),
      (
        λf∈∘cat_ordinal (3ℕ)⦇Arr⦈.
         if f = [0, 0]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈∙
          | f = [0, 1ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙
          | f = [0, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙
          | f = [1ℕ, 1ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙
          | f = [1ℕ, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙
          | f = [2ℕ, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙
          | otherwise ⇒ 𝔉⦇HomCod⦈⦇Arr⦈
      ), 
      cat_ordinal (3ℕ),
      𝔉⦇HomCod⦈
    ]∘"


text‹Components.›

lemma RK23_components:
  shows "RK23 𝔉⦇ObjMap⦈ =
    (
      λa∈∘cat_ordinal (3ℕ)⦇Obj⦈.
        if a = 0 ⇒ 𝔉⦇ObjMap⦈⦇0⦈
         | a = 1ℕ ⇒ 𝔉⦇ObjMap⦈⦇1ℕ⦈
         | a = 2ℕ ⇒ 𝔉⦇ObjMap⦈⦇1ℕ⦈
         | otherwise ⇒ 𝔉⦇HomCod⦈⦇Obj⦈
    )"
    and "RK23 𝔉⦇ArrMap⦈ =
      (
        λf∈∘cat_ordinal (3ℕ)⦇Arr⦈.
         if f = [0, 0]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈∙
          | f = [0, 1ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙
          | f = [0, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙
          | f = [1ℕ, 1ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙
          | f = [1ℕ, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙
          | f = [2ℕ, 2ℕ]∘ ⇒ 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙
          | otherwise ⇒ 𝔉⦇HomCod⦈⦇Arr⦈
      )"
    and "RK23 𝔉⦇HomDom⦈ = cat_ordinal (3ℕ)"
    and "RK23 𝔉⦇HomCod⦈ = 𝔉⦇HomCod⦈"
  unfolding RK23_def dghm_field_simps by (simp_all add: nat_omega_simps)

context is_functor
begin

lemmas RK23_components' = RK23_components[where 𝔉=𝔉, unfolded cat_cs_simps]

lemmas [cat_Kan_cs_simps] = RK23_components'(3,4)

end

lemmas [cat_Kan_cs_simps] = is_functor.RK23_components'(3,4)


subsubsection‹Object map›

mk_VLambda RK23_components(1)
  |vsv RK23_ObjMap_vsv[cat_Kan_cs_intros]|
  |vdomain RK23_ObjMap_vdomain[cat_Kan_cs_simps]|
  |app RK23_ObjMap_app|

lemma RK23_ObjMap_app_0[cat_Kan_cs_simps]:
  assumes "a = 0"
  shows "RK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇0⦈"
  unfolding RK23_components assms cat_ordinal_components by simp

lemma RK23_ObjMap_app_1[cat_Kan_cs_simps]:
  assumes "a = 1ℕ"
  shows "RK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇1ℕ⦈"
  unfolding RK23_components assms cat_ordinal_components by simp

lemma RK23_ObjMap_app_2[cat_Kan_cs_simps]:
  assumes "a = 2ℕ"
  shows "RK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇1ℕ⦈"
  unfolding RK23_components assms cat_ordinal_components by simp


subsubsection‹Arrow map›

mk_VLambda RK23_components(2)
  |vsv RK23_ArrMap_vsv[cat_Kan_cs_intros]|
  |vdomain RK23_ArrMap_vdomain[cat_Kan_cs_simps]|
  |app RK23_ArrMap_app|

lemma RK23_ArrMap_app_00[cat_Kan_cs_simps]:
  assumes "f = [0, 0]∘"
  shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 0⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow cs_intro:
          V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding RK23_components assms by auto
qed

lemma RK23_ArrMap_app_01[cat_Kan_cs_simps]:
  assumes "f = [0, 1ℕ]∘"
  shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow cs_intro:
          V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding RK23_components assms by auto
qed

lemma RK23_ArrMap_app_02[cat_Kan_cs_simps]:
  assumes "f = [0, 2ℕ]∘"
  shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 1ℕ⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow cs_intro:
          V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding RK23_components assms by auto
qed

lemma RK23_ArrMap_app_11[cat_Kan_cs_simps]:
  assumes "f = [1ℕ, 1ℕ]∘"
  shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow cs_intro:
          V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding RK23_components assms by auto
qed

lemma RK23_ArrMap_app_12[cat_Kan_cs_simps]:
  assumes "f = [1ℕ, 2ℕ]∘"
  shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl 
          cs_simp: omega_of_set   
          cs_intro: nat_omega_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding RK23_components assms by auto
qed

lemma RK23_ArrMap_app_22[cat_Kan_cs_simps]:
  assumes "f = [2ℕ, 2ℕ]∘"
  shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙"
proof-
  from 0123 have f: "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow cs_intro: 
          nat_omega_intros cat_ordinal_cs_intros cat_cs_intros assms
      )
  then show ?thesis unfolding RK23_components assms by simp
qed


subsubsection‹‹RK23› is a functor›

lemma cat_RK23_is_functor:
  assumes "𝔉 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ ℭ"
  shows "RK23 𝔉 : cat_ordinal (3ℕ) ↦↦C⇘α⇙ ℭ"
proof-

  interpret 𝔉: is_functor α ‹cat_ordinal (2ℕ)› ℭ 𝔉 by (rule assms(1))

  from ord_of_nat_ω interpret cat_ordinal_2: finite_category α ‹cat_ordinal (2ℕ)›
    by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
  from ord_of_nat_ω interpret cat_ordinal_3: finite_category α ‹cat_ordinal (3ℕ)›
    by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)

  interpret 𝔉: is_functor α ‹cat_ordinal (2ℕ)› ℭ 𝔉 by (rule assms)

  show ?thesis
  proof(intro is_functorI')
    show "vfsequence (RK23 𝔉)" unfolding RK23_def by auto
    show "vcard (RK23 𝔉) = 4ℕ" unfolding RK23_def by (simp add: nat_omega_simps)
    show "ℛ∘ (RK23 𝔉⦇ObjMap⦈) ⊆∘ ℭ⦇Obj⦈"
    proof(rule vsv.vsv_vrange_vsubset, unfold cat_Kan_cs_simps)
      fix x assume prems: "x ∈∘ cat_ordinal (3ℕ)⦇Obj⦈"
      then consider ‹x = 0› | ‹x = 1ℕ› | ‹x = 2ℕ›
        unfolding cat_ordinal_cs_simps three by auto
      then show "RK23 𝔉⦇ObjMap⦈⦇x⦈ ∈∘ ℭ⦇Obj⦈" 
        by cases
          (
            cs_concl 
              cs_simp: cat_Kan_cs_simps cat_ordinal_cs_simps omega_of_set 
              cs_intro: cat_cs_intros nat_omega_intros
          )+
    qed (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
    show "RK23 𝔉⦇ArrMap⦈⦇f⦈ : RK23 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ RK23 𝔉⦇ObjMap⦈⦇b⦈"
      if "f : a ↦⇘cat_ordinal (3ℕ)⇙ b" for a b f
    proof-
      from 0123 that show ?thesis
        by (elim cat_ordinal_3_is_arrE; simp only:)
          (
            cs_concl 
              cs_simp: cat_Kan_cs_simps
              cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
          )+
    qed
    show 
      "RK23 𝔉⦇ArrMap⦈⦇g ∘A⇘cat_ordinal (3ℕ)⇙ f⦈ =
        RK23 𝔉⦇ArrMap⦈⦇g⦈ ∘A⇘ℭ⇙ RK23 𝔉⦇ArrMap⦈⦇f⦈"
      if "g : b ↦⇘cat_ordinal (3ℕ)⇙ c" and "f : a ↦⇘cat_ordinal (3ℕ)⇙ b"
      for b c g a f
      using 0123 that 
      by (elim cat_ordinal_3_is_arrE; simp only:; (solves‹simp›)?) (*slow*)
        (
          cs_concl 
            cs_simp: 
              cat_ordinal_cs_simps 
              cat_Kan_cs_simps 
              𝔉.cf_ArrMap_Comp[symmetric]
            cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
        )+
    show "RK23 𝔉⦇ArrMap⦈⦇cat_ordinal (3ℕ)⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇RK23 𝔉⦇ObjMap⦈⦇c⦈⦈"
      if "c ∈∘ cat_ordinal (3ℕ)⦇Obj⦈" for c
    proof-
      from that consider ‹c = 0› | ‹c = 1ℕ› | ‹c = 2ℕ›
        unfolding cat_ordinal_components three by auto
      then show ?thesis
        by (cases, use 0123 in ‹simp_all only:›)
          (
            cs_concl 
              cs_simp: 
                cat_ordinal_cs_simps 
                cat_Kan_cs_simps 
                is_functor.cf_ObjMap_CId[symmetric]  
              cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
          )+
    qed
  qed 
    (
      cs_concl cs_shallow
        cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
    )+

qed

lemma cat_RK23_is_functor'[cat_Kan_cs_intros]:
  assumes "𝔉 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ ℭ"
    and "𝔄' = cat_ordinal (3ℕ)"
  shows "RK23 𝔉 : 𝔄' ↦↦C⇘α⇙ ℭ"
  using assms(1) unfolding assms(2) by (rule cat_RK23_is_functor)


subsubsection‹The fundamental property of ‹RK23››

lemma cf_comp_RK23_𝔎23[cat_Kan_cs_simps]: 
  assumes "𝔉 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ ℭ"
  shows "RK23 𝔉 ∘CF 𝔎23 = 𝔉"
proof-

  interpret 𝔉: is_functor α ‹cat_ordinal (2ℕ)› ℭ 𝔉 by (rule assms(1))
  interpret 𝔎23: is_functor α ‹cat_ordinal (2ℕ)› ‹cat_ordinal (3ℕ)› ‹𝔎23›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
  interpret RK23: is_functor α ‹cat_ordinal (3ℕ)› ℭ ‹RK23 𝔉›
    by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)

  show ?thesis
  proof(rule cf_eqI)
    show "𝔉 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ ℭ" by (rule assms)
    have ObjMap_dom_lhs: "𝒟∘ ((RK23 𝔉 ∘CF 𝔎23)⦇ObjMap⦈) = 2ℕ"
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_ordinal_cs_simps cs_intro: cat_cs_intros
        )
    have ObjMap_dom_rhs: "𝒟∘ (𝔉⦇ObjMap⦈) = 2ℕ"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
    show "(RK23 𝔉 ∘CF 𝔎23)⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
    proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
      fix a assume prems: "a ∈∘ 2ℕ"
      then consider ‹a = 0› | ‹a = 1ℕ› by force
      then show "(RK23 𝔉 ∘CF 𝔎23)⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇a⦈"
        by (cases, use nothing in ‹simp_all only:›)
          (
            cs_concl 
              cs_simp:
                omega_of_set cat_cs_simps cat_ordinal_cs_simps cat_Kan_cs_simps
              cs_intro: cat_cs_intros nat_omega_intros
          )+
    qed (cs_concl cs_intro: cat_cs_intros V_cs_intros)+
    have ArrMap_dom_lhs: "𝒟∘ ((RK23 𝔉 ∘CF 𝔎23)⦇ArrMap⦈) = cat_ordinal (2ℕ)⦇Arr⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    have ArrMap_dom_rhs: "𝒟∘ (𝔉⦇ArrMap⦈) = cat_ordinal (2ℕ)⦇Arr⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show "(RK23 𝔉 ∘CF 𝔎23)⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
    proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      fix f assume prems: "f ∈∘ cat_ordinal (2ℕ)⦇Arr⦈"
      then obtain a b where "f : a ↦⇘cat_ordinal (2ℕ)⇙ b" by auto
      then show "(RK23 𝔉 ∘CF 𝔎23)⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇f⦈"
        by (elim cat_ordinal_2_is_arrE; simp only:)
          (
            cs_concl
              cs_simp: cat_cs_simps cat_Kan_cs_simps cs_intro: cat_cs_intros
          )+
    qed (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros V_cs_intros)+
  qed (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)

qed



subsection‹
‹RK_σ23›: towards the universal property of the right Kan extension along ‹𝔎23›
›


subsubsection‹Definition and elementary properties›

definition RK_σ23 :: "V ⇒ V ⇒ V ⇒ V"
  where "RK_σ23 𝔗 ε' 𝔉' =
    [
      (
        λa∈∘cat_ordinal (3ℕ)⦇Obj⦈.
         if a = 0 ⇒ ε'⦇NTMap⦈⦇0⦈
          | a = 1ℕ ⇒ ε'⦇NTMap⦈⦇1ℕ⦈ ∘A⇘𝔗⦇HomCod⦈⇙ 𝔉'⦇ArrMap⦈⦇1ℕ, 2ℕ⦈∙
          | a = 2ℕ ⇒ ε'⦇NTMap⦈⦇1ℕ⦈
          | otherwise ⇒ 𝔗⦇HomCod⦈⦇Arr⦈
      ),
      𝔉',
      RK23 𝔗,
      cat_ordinal (3ℕ),
      𝔉'⦇HomCod⦈
    ]∘"


text‹Components.›

lemma RK_σ23_components:
  shows "RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈ =
    (
      λa∈∘cat_ordinal (3ℕ)⦇Obj⦈.
        if a = 0 ⇒ ε'⦇NTMap⦈⦇0⦈
         | a = 1ℕ ⇒ ε'⦇NTMap⦈⦇1ℕ⦈ ∘A⇘𝔗⦇HomCod⦈⇙ 𝔉'⦇ArrMap⦈⦇1ℕ, 2ℕ⦈∙
         | a = 2ℕ ⇒ ε'⦇NTMap⦈⦇1ℕ⦈
         | otherwise ⇒ 𝔗⦇HomCod⦈⦇Arr⦈
    )"
    and "RK_σ23 𝔗 ε' 𝔉'⦇NTDom⦈ = 𝔉'"
    and "RK_σ23 𝔗 ε' 𝔉'⦇NTCod⦈ = RK23 𝔗"
    and "RK_σ23 𝔗 ε' 𝔉'⦇NTDGDom⦈ = cat_ordinal (3ℕ)"
    and "RK_σ23 𝔗 ε' 𝔉'⦇NTDGCod⦈ = 𝔉'⦇HomCod⦈"
  unfolding RK_σ23_def nt_field_simps by (simp_all add: nat_omega_simps)

context
  fixes α 𝔄 𝔉' 𝔗  
  assumes 𝔉': "𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
    and 𝔗: "𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
begin

interpretation 𝔉': is_functor α ‹cat_ordinal (3ℕ)› 𝔄 𝔉' by (rule 𝔉')
interpretation 𝔗: is_functor α ‹cat_ordinal (2ℕ)› 𝔄 𝔗 by (rule 𝔗)

lemmas RK_σ23_components' = 
  RK_σ23_components[where 𝔉'=𝔉' and 𝔗=𝔗, unfolded cat_cs_simps]

lemmas [cat_Kan_cs_simps] = RK_σ23_components'(2-5)

end


subsubsection‹Natural transformation map›

mk_VLambda RK_σ23_components(1)
  |vsv RK_σ23_NTMap_vsv[cat_Kan_cs_intros]|
  |vdomain RK_σ23_NTMap_vdomain[cat_Kan_cs_simps]|
  |app RK_σ23_NTMap_app|

lemma RK_σ23_NTMap_app_0[cat_Kan_cs_simps]:
  assumes "a = 0"
  shows "RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇a⦈ = ε'⦇NTMap⦈⦇0⦈"
  using assms unfolding RK_σ23_components cat_ordinal_cs_simps by simp

lemma (in is_functor) RK_σ23_NTMap_app_1[cat_Kan_cs_simps]:
  assumes "a = 1ℕ"
  shows "RK_σ23 𝔉 ε' 𝔉'⦇NTMap⦈⦇a⦈ = ε'⦇NTMap⦈⦇1ℕ⦈ ∘A⇘𝔅⇙ 𝔉'⦇ArrMap⦈⦇1ℕ, 2ℕ⦈∙"
  using assms 
  unfolding RK_σ23_components cat_ordinal_cs_simps cat_cs_simps 
  by simp

lemmas [cat_Kan_cs_simps] = is_functor.RK_σ23_NTMap_app_1

lemma RK_σ23_NTMap_app_2[cat_Kan_cs_simps]:
  assumes "a = 2ℕ"
  shows "RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇a⦈ = ε'⦇NTMap⦈⦇1ℕ⦈"
  using assms unfolding RK_σ23_components cat_ordinal_cs_simps by simp


subsubsection‹‹RK_σ23› is a natural transformation›

lemma RK_σ23_is_ntcf:
  assumes "𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄" 
    and "𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
    and "ε' : 𝔉' ∘CF 𝔎23 ↦CF 𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
  shows "RK_σ23 𝔗 ε' 𝔉' : 𝔉' ↦CF RK23 𝔗 : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
proof-
 
  interpret 𝔉': is_functor α ‹cat_ordinal (3ℕ)› 𝔄 𝔉' by (rule assms(1))
  interpret 𝔗: is_functor α ‹cat_ordinal (2ℕ)› 𝔄 𝔗 by (rule assms(2))
  interpret ε': is_ntcf α ‹cat_ordinal (2ℕ)› 𝔄 ‹𝔉' ∘CF 𝔎23› 𝔗 ε' 
    by (rule assms(3))

  interpret 𝔎23: is_functor α ‹cat_ordinal (2ℕ)› ‹cat_ordinal (3ℕ)› ‹𝔎23›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
  interpret RK23: is_functor α ‹cat_ordinal (3ℕ)› 𝔄 ‹RK23 𝔗›
    by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)

  from 0123 have [cat_cs_simps]: "𝔗⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙ = 𝔄⦇CId⦈⦇𝔗⦇ObjMap⦈⦇1ℕ⦈⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_ordinal_cs_simps is_functor.cf_ObjMap_CId[symmetric] 
          cs_intro: cat_cs_intros
      )

  show ?thesis
  proof(rule is_ntcfI')
    show "vfsequence (RK_σ23 𝔗 ε' 𝔉')" unfolding RK_σ23_def by simp
    show "vcard (RK_σ23 𝔗 ε' 𝔉') = 5ℕ"
      unfolding RK_σ23_def by (simp_all add: nat_omega_simps)
    show "RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇a⦈ : 𝔉'⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ RK23 𝔗⦇ObjMap⦈⦇a⦈"
      if "a ∈∘ cat_ordinal (3ℕ)⦇Obj⦈" for a
    proof-
      from that consider ‹a = 0› | ‹a = 1ℕ› | ‹a = 2ℕ›
        unfolding cat_ordinal_cs_simps three by auto
      from this 0123 show ?thesis
        by (cases, use nothing in ‹simp_all only:›)
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_ordinal_cs_simps cat_Kan_cs_simps
              cs_intro:
                cat_cs_intros
                cat_ordinal_cs_intros
                cat_Kan_cs_intros 
                nat_omega_intros
          )+
    qed
    show
      "RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔉'⦇ArrMap⦈⦇f⦈ =
        RK23 𝔗⦇ArrMap⦈⦇f⦈ ∘A⇘𝔄⇙ RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇a⦈"
      if "f : a ↦⇘cat_ordinal (3ℕ)⇙ b" for a b f
      using that 0123
      by (elim cat_ordinal_3_is_arrE, use nothing in ‹simp_all only:›) (*slow*)
        (
          cs_concl
            cs_simp:
              cat_cs_simps
              cat_ordinal_cs_simps
              𝔉'.cf_ArrMap_Comp[symmetric]
              𝔉'.HomCod.cat_Comp_assoc
              ε'.ntcf_Comp_commute[symmetric]
              cat_Kan_cs_simps 
            cs_intro: cat_cs_intros cat_ordinal_cs_intros nat_omega_intros
        )+
  qed
    (
      cs_concl  
        cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
    )+

qed

lemma RK_σ23_is_ntcf'[cat_Kan_cs_intros]:
  assumes "𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄" 
    and "𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
    and "ε' : 𝔉' ∘CF 𝔎23 ↦CF 𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
    and "𝔊' = 𝔉'"
    and "ℌ' = RK23 𝔗"
    and "ℭ' = cat_ordinal (3ℕ)"
  shows "RK_σ23 𝔗 ε' 𝔉' : 𝔊' ↦CF ℌ': ℭ' ↦↦C⇘α⇙ 𝔄"
  using assms(1-3) unfolding assms(4-6) by (rule RK_σ23_is_ntcf)



subsection‹The right Kan extension along ‹𝔎23››

lemma ε23_is_cat_rKe:
  assumes "𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
  shows "ntcf_id 𝔗 :
    RK23 𝔗 ∘CF 𝔎23 ↦CF.rKe⇘α⇙ 𝔗 : cat_ordinal (2ℕ) ↦C cat_ordinal (3ℕ) ↦C 𝔄"
proof-

  interpret 𝔗: is_functor α ‹cat_ordinal (2ℕ)› 𝔄 𝔗 by (rule assms(1))
  interpret 𝔎23: is_functor α ‹cat_ordinal (2ℕ)› ‹cat_ordinal (3ℕ)› ‹𝔎23›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
  interpret RK23: is_functor α ‹cat_ordinal (3ℕ)› 𝔄 ‹RK23 𝔗›
    by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)

  from 0123 have [cat_cs_simps]: "𝔗⦇ArrMap⦈⦇1ℕ, 1ℕ⦈∙ = 𝔄⦇CId⦈⦇𝔗⦇ObjMap⦈⦇1ℕ⦈⦈"
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_ordinal_cs_simps is_functor.cf_ObjMap_CId[symmetric]
          cs_intro: cat_cs_intros
      )

  show ?thesis
  proof(intro is_cat_rKeI')
    
    fix 𝔉' ε' assume prems:
      "𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
      "ε' : 𝔉' ∘CF 𝔎23 ↦CF 𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"

    interpret 𝔉': is_functor α ‹cat_ordinal (3ℕ)› 𝔄 𝔉' by (rule prems(1))
    interpret ε': is_ntcf α ‹cat_ordinal (2ℕ)› 𝔄 ‹𝔉' ∘CF 𝔎23› 𝔗 ε' 
      by (rule prems(2))
    interpret RK_σ23: is_ntcf α ‹cat_ordinal (3ℕ)› 𝔄 𝔉' ‹RK23 𝔗› ‹RK_σ23 𝔗 ε' 𝔉'›
      by (intro RK_σ23_is_ntcf prems assms)

    show "∃!σ.
      σ : 𝔉' ↦CF RK23 𝔗 : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄 ∧
      ε' = ntcf_id 𝔗 ∙NTCF (σ ∘NTCF-CF 𝔎23)"
    proof(intro ex1I conjI; (elim conjE)?)
      show "RK_σ23 𝔗 ε' 𝔉' : 𝔉' ↦CF RK23 𝔗 : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
        by (intro RK_σ23.is_ntcf_axioms)
      show "ε' = ntcf_id 𝔗 ∙NTCF (RK_σ23 𝔗 ε' 𝔉' ∘NTCF-CF 𝔎23)"
      proof(rule ntcf_eqI)
        show "ε' : 𝔉' ∘CF 𝔎23 ↦CF 𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄" 
          by (intro prems)
        then have dom_lhs: "𝒟∘ (ε'⦇NTMap⦈) = 2ℕ"
          by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
        show rhs:
          "ntcf_id 𝔗 ∙NTCF (RK_σ23 𝔗 ε' 𝔉' ∘NTCF-CF 𝔎23) :
            𝔉' ∘CF 𝔎23 ↦CF 𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
          by
            (
              cs_concl cs_shallow 
                cs_simp: cat_Kan_cs_simps cat_cs_simps 
                cs_intro: cat_Kan_cs_intros cat_cs_intros
            )
        then have dom_rhs: 
          "𝒟∘ ((ntcf_id 𝔗 ∙NTCF (RK_σ23 𝔗 ε' 𝔉' ∘NTCF-CF 𝔎23))⦇NTMap⦈) = 2ℕ"
          by (cs_concl cs_simp: cat_ordinal_cs_simps cat_cs_simps)
        show "ε'⦇NTMap⦈ = (ntcf_id 𝔗 ∙NTCF (RK_σ23 𝔗 ε' 𝔉' ∘NTCF-CF 𝔎23))⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix a assume prems: "a ∈∘ 2ℕ"
          then consider ‹a = 0› | ‹a = 1ℕ› unfolding two by auto
          then show 
            "ε'⦇NTMap⦈⦇a⦈ =
              (ntcf_id 𝔗 ∙NTCF (RK_σ23 𝔗 ε' 𝔉' ∘NTCF-CF 𝔎23))⦇NTMap⦈⦇a⦈"
            by (cases; use nothing in ‹simp_all only:›)
              (
                cs_concl 
                  cs_simp:
                    omega_of_set
                    cat_Kan_cs_simps
                    cat_cs_simps
                    cat_ordinal_cs_simps
                  cs_intro: cat_Kan_cs_intros cat_cs_intros nat_omega_intros
              )+
        qed 
          (
            use rhs in
              ‹cs_concl cs_shallow cs_intro: V_cs_intros cat_cs_intros›
          )+
      qed simp_all

      fix σ assume prems': 
        "σ : 𝔉' ↦CF RK23 𝔗 : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
        "ε' = ntcf_id 𝔗 ∙NTCF (σ ∘NTCF-CF 𝔎23)"

      interpret σ: is_ntcf α ‹cat_ordinal (3ℕ)› 𝔄 𝔉' ‹RK23 𝔗› σ 
        by (rule prems'(1))

      from prems'(2) have 
        "ε'⦇NTMap⦈⦇0⦈ = (ntcf_id 𝔗 ∙NTCF (σ ∘NTCF-CF 𝔎23))⦇NTMap⦈⦇0⦈"
        by auto
      then have [cat_cs_simps]: "ε'⦇NTMap⦈⦇0⦈ = σ⦇NTMap⦈⦇0⦈"
        by
          (
            cs_prems cs_shallow
              cs_simp: cat_Kan_cs_simps cat_cs_simps cat_ordinal_cs_simps 
              cs_intro: cat_cs_intros nat_omega_intros
          )
      from prems'(2) have
        "ε'⦇NTMap⦈⦇1ℕ⦈ = (ntcf_id 𝔗 ∙NTCF (σ ∘NTCF-CF 𝔎23))⦇NTMap⦈⦇1ℕ⦈"
        by auto
      then have [cat_cs_simps]: "ε'⦇NTMap⦈⦇1ℕ⦈ = σ⦇NTMap⦈⦇2ℕ⦈"
        by
          (
            cs_prems cs_shallow
              cs_simp:
                omega_of_set cat_Kan_cs_simps cat_cs_simps cat_ordinal_cs_simps
              cs_intro: cat_cs_intros nat_omega_intros
          )

      show "σ = RK_σ23 𝔗 ε' 𝔉'"
      proof(rule ntcf_eqI)
        show "σ : 𝔉' ↦CF RK23 𝔗 : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
          by (rule prems'(1))
        then have dom_lhs: "𝒟∘ (σ⦇NTMap⦈) = 3ℕ"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
        show "RK_σ23 𝔗 ε' 𝔉' : 𝔉' ↦CF RK23 𝔗 : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
          by (cs_concl cs_intro: cat_cs_intros cat_Kan_cs_intros)
        then have dom_rhs: "𝒟∘ (RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈) = 3ℕ"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
        from 0123 have 013: "[0, 1ℕ]∘ : 0 ↦⇘cat_ordinal (3ℕ)⇙ 1ℕ"
          by (cs_concl cs_intro: cat_ordinal_cs_intros nat_omega_intros)
        from 0123 have 123: "[1ℕ, 2ℕ]∘ : 1ℕ ↦⇘cat_ordinal (3ℕ)⇙ 2ℕ"
          by (cs_concl cs_intro: cat_ordinal_cs_intros nat_omega_intros)

        from σ.ntcf_Comp_commute[OF 123] 013 0123 
        have [symmetric, cat_Kan_cs_simps]:
          "σ⦇NTMap⦈⦇2ℕ⦈ ∘A⇘𝔄⇙ 𝔉'⦇ArrMap⦈ ⦇1ℕ, 2ℕ⦈∙ = σ⦇NTMap⦈⦇1ℕ⦈"
          by
            (
              cs_prems  
                cs_simp: cat_cs_simps cat_Kan_cs_simps RK23_ArrMap_app_12 
                cs_intro: cat_cs_intros
            )
        show "σ⦇NTMap⦈ = RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix a assume prems: "a ∈∘ 3ℕ"
          then consider ‹a = 0› | ‹a = 1ℕ› | ‹a = 2ℕ› unfolding three by auto
          then show "σ⦇NTMap⦈⦇a⦈ = RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇a⦈"
            by (cases; use nothing in ‹simp_all only:›) 
              (cs_concl cs_simp: cat_cs_simps cat_Kan_cs_simps)+
        qed auto
      qed simp_all

    qed

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

qed



subsection‹
‹LK_σ23›: towards the universal property of the left Kan extension along ‹𝔎23›
›


subsubsection‹Definition and elementary properties›

definition LK_σ23 :: "V ⇒ V ⇒ V ⇒ V"
  where "LK_σ23 𝔗 η' 𝔉' =
    [
      (
        λa∈∘cat_ordinal (3ℕ)⦇Obj⦈.
         if a = 0 ⇒ η'⦇NTMap⦈⦇0⦈
          | a = 1ℕ ⇒ 𝔉'⦇ArrMap⦈⦇0, 1ℕ⦈∙ ∘A⇘𝔗⦇HomCod⦈⇙ η'⦇NTMap⦈⦇0⦈
          | a = 2ℕ ⇒ η'⦇NTMap⦈⦇1ℕ⦈
          | otherwise ⇒ 𝔗⦇HomCod⦈⦇Arr⦈
      ),
      LK23 𝔗,
      𝔉',
      cat_ordinal (3ℕ),
      𝔉'⦇HomCod⦈
    ]∘"


text‹Components.›

lemma LK_σ23_components:
  shows "LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈ =
    (
      λa∈∘cat_ordinal (3ℕ)⦇Obj⦈.
        if a = 0 ⇒ η'⦇NTMap⦈⦇0⦈
         | a = 1ℕ ⇒ 𝔉'⦇ArrMap⦈⦇0, 1ℕ⦈∙ ∘A⇘𝔗⦇HomCod⦈⇙ η'⦇NTMap⦈⦇0⦈
         | a = 2ℕ ⇒ η'⦇NTMap⦈⦇1ℕ⦈
         | otherwise ⇒ 𝔗⦇HomCod⦈⦇Arr⦈
    )"
    and "LK_σ23 𝔗 η' 𝔉'⦇NTDom⦈ = LK23 𝔗"
    and "LK_σ23 𝔗 η' 𝔉'⦇NTCod⦈ = 𝔉'"
    and "LK_σ23 𝔗 η' 𝔉'⦇NTDGDom⦈ = cat_ordinal (3ℕ)"
    and "LK_σ23 𝔗 η' 𝔉'⦇NTDGCod⦈ = 𝔉'⦇HomCod⦈"
  unfolding LK_σ23_def nt_field_simps by (simp_all add: nat_omega_simps)

context
  fixes α 𝔄 𝔉' 𝔗  
  assumes 𝔉': "𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
    and 𝔗: "𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
begin

interpretation 𝔉': is_functor α ‹cat_ordinal (3ℕ)› 𝔄 𝔉' by (rule 𝔉')
interpretation 𝔗: is_functor α ‹cat_ordinal (2ℕ)› 𝔄 𝔗 by (rule 𝔗)

lemmas LK_σ23_components' = 
  LK_σ23_components[where 𝔉'=𝔉' and 𝔗=𝔗, unfolded cat_cs_simps]

lemmas [cat_Kan_cs_simps] = LK_σ23_components'(2-5)

end


subsubsection‹Natural transformation map›

mk_VLambda LK_σ23_components(1)
  |vsv LK_σ23_NTMap_vsv[cat_Kan_cs_intros]|
  |vdomain LK_σ23_NTMap_vdomain[cat_Kan_cs_simps]|
  |app LK_σ23_NTMap_app|

lemma LK_σ23_NTMap_app_0[cat_Kan_cs_simps]:
  assumes "a = 0"
  shows "LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈ = η'⦇NTMap⦈⦇0⦈"
  using assms unfolding LK_σ23_components cat_ordinal_cs_simps by simp

lemma (in is_functor) LK_σ23_NTMap_app_1[cat_Kan_cs_simps]:
  assumes "a = 1ℕ"
  shows "LK_σ23 𝔉 η' 𝔉'⦇NTMap⦈⦇a⦈ = 𝔉'⦇ArrMap⦈⦇0, 1ℕ⦈∙ ∘A⇘𝔅⇙ η'⦇NTMap⦈⦇0⦈"
  using assms unfolding LK_σ23_components cat_ordinal_cs_simps cat_cs_simps by simp

lemmas [cat_Kan_cs_simps] = is_functor.LK_σ23_NTMap_app_1

lemma LK_σ23_NTMap_app_2[cat_Kan_cs_simps]:
  assumes "a = 2ℕ"
  shows "LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈ = η'⦇NTMap⦈⦇1ℕ⦈"
  using assms unfolding LK_σ23_components cat_ordinal_cs_simps by simp


subsubsection‹‹LK_σ23› is a natural transformation›

lemma LK_σ23_is_ntcf:
  assumes "𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄" 
    and "𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
    and "η' : 𝔗 ↦CF 𝔉' ∘CF 𝔎23 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
  shows "LK_σ23 𝔗 η' 𝔉' : LK23 𝔗 ↦CF 𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
proof-
 
  interpret 𝔉': is_functor α ‹cat_ordinal (3ℕ)› 𝔄 𝔉' by (rule assms(1))
  interpret 𝔗: is_functor α ‹cat_ordinal (2ℕ)› 𝔄 𝔗 by (rule assms(2))
  interpret η': is_ntcf α ‹cat_ordinal (2ℕ)› 𝔄 𝔗 ‹𝔉' ∘CF 𝔎23› η' 
    by (rule assms(3))

  interpret 𝔎23: is_functor α ‹cat_ordinal (2ℕ)› ‹cat_ordinal (3ℕ)› ‹𝔎23›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
  interpret LK23: is_functor α ‹cat_ordinal (3ℕ)› 𝔄 ‹LK23 𝔗›
    by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
 
  show ?thesis
  proof(rule is_ntcfI')
    show "vfsequence (LK_σ23 𝔗 η' 𝔉')" unfolding LK_σ23_def by simp
    show "vcard (LK_σ23 𝔗 η' 𝔉') = 5ℕ"
      unfolding LK_σ23_def by (simp_all add: nat_omega_simps)
    show "LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈ : LK23 𝔗⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
      if "a ∈∘ cat_ordinal (3ℕ)⦇Obj⦈" for a
    proof-
      from that consider ‹a = 0› | ‹a = 1ℕ› | ‹a = 2ℕ›
        unfolding cat_ordinal_cs_simps three by auto
      from this 0123 show 
        "LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈ : LK23 𝔗⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
        by (cases, use nothing in ‹simp_all only:›)
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_ordinal_cs_simps cat_Kan_cs_simps
              cs_intro:
                cat_cs_intros 
                cat_ordinal_cs_intros 
                cat_Kan_cs_intros
                nat_omega_intros
          )+
    qed
    show
      "LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ LK23 𝔗⦇ArrMap⦈⦇f⦈ =
        𝔉'⦇ArrMap⦈⦇f⦈ ∘A⇘𝔄⇙ LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈"
      if "f : a ↦⇘cat_ordinal (3ℕ)⇙ b" for a b f
      using that 0123 (*very slow*)
      by (elim cat_ordinal_3_is_arrE, use nothing in ‹simp_all only:›) 
        (
          cs_concl 
            cs_simp: 
              cat_cs_simps 
              cat_ordinal_cs_simps
              𝔉'.cf_ArrMap_Comp[symmetric]
              𝔉'.HomCod.cat_Comp_assoc[symmetric]
              η'.ntcf_Comp_commute 
              cat_Kan_cs_simps 
            cs_intro: cat_cs_intros cat_ordinal_cs_intros nat_omega_intros
        )+
  qed
    (
      cs_concl 
        cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
    )+

qed

lemma LK_σ23_is_ntcf'[cat_Kan_cs_intros]:
  assumes "𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
    and "𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
    and "η' : 𝔗 ↦CF 𝔉' ∘CF 𝔎23 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
    and "𝔊' = LK23 𝔗"
    and "ℌ' = 𝔉'"
    and "ℭ' = cat_ordinal (3ℕ)"
  shows "LK_σ23 𝔗 η' 𝔉' : 𝔊' ↦CF ℌ': ℭ' ↦↦C⇘α⇙ 𝔄"
  using assms(1-3) unfolding assms(4-6) by (rule LK_σ23_is_ntcf)



subsection‹The left Kan extension along ‹𝔎23››

lemma η23_is_cat_rKe:
  assumes "𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
  shows "ntcf_id 𝔗 :
    𝔗 ↦CF.lKe⇘α⇙ LK23 𝔗 ∘CF 𝔎23 : cat_ordinal (2ℕ) ↦C cat_ordinal (3ℕ) ↦C 𝔄"
proof-

  interpret 𝔗: is_functor α ‹cat_ordinal (2ℕ)› 𝔄 𝔗 by (rule assms(1))
  interpret 𝔎23: is_functor α ‹cat_ordinal (2ℕ)› ‹cat_ordinal (3ℕ)› ‹𝔎23›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
  interpret LK23: is_functor α ‹cat_ordinal (3ℕ)› 𝔄 ‹LK23 𝔗›
    by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)

  show ?thesis
  proof(intro is_cat_lKeI')
    fix 𝔉' η' assume prems:
      "𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
      "η' : 𝔗 ↦CF 𝔉' ∘CF 𝔎23 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"

    interpret 𝔉': is_functor α ‹cat_ordinal (3ℕ)› 𝔄 𝔉' by (rule prems(1))
    interpret η': is_ntcf α ‹cat_ordinal (2ℕ)› 𝔄 𝔗 ‹𝔉' ∘CF 𝔎23› η' 
      by (rule prems(2))
    interpret LK_σ23: is_ntcf α ‹cat_ordinal (3ℕ)› 𝔄 ‹LK23 𝔗› 𝔉' ‹LK_σ23 𝔗 η' 𝔉'›
      by (intro LK_σ23_is_ntcf prems assms)

    show "∃!σ.
      σ : LK23 𝔗 ↦CF 𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄 ∧
      η' = σ ∘NTCF-CF 𝔎23 ∙NTCF ntcf_id 𝔗"
    proof(intro ex1I conjI; (elim conjE)?)
      show "LK_σ23 𝔗 η' 𝔉' : LK23 𝔗 ↦CF 𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
        by (intro LK_σ23.is_ntcf_axioms)
      show "η' = LK_σ23 𝔗 η' 𝔉' ∘NTCF-CF 𝔎23 ∙NTCF ntcf_id 𝔗"
      proof(rule ntcf_eqI)
        show "η' : 𝔗 ↦CF 𝔉' ∘CF 𝔎23 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄" 
          by (intro prems)
        then have dom_lhs: "𝒟∘ (η'⦇NTMap⦈) = 2ℕ"
          by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
        show rhs:
          "LK_σ23 𝔗 η' 𝔉' ∘NTCF-CF 𝔎23 ∙NTCF ntcf_id 𝔗 :
            𝔗 ↦CF 𝔉' ∘CF 𝔎23 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
          by 
            (
              cs_concl cs_shallow
                cs_simp: cat_Kan_cs_simps cat_cs_simps 
                cs_intro: cat_Kan_cs_intros cat_cs_intros
            )
        then have dom_rhs: 
          "𝒟∘ ((LK_σ23 𝔗 η' 𝔉' ∘NTCF-CF 𝔎23 ∙NTCF ntcf_id 𝔗)⦇NTMap⦈) = 2ℕ"
          by (cs_concl cs_simp: cat_ordinal_cs_simps cat_cs_simps)
        show "η'⦇NTMap⦈ = (LK_σ23 𝔗 η' 𝔉' ∘NTCF-CF 𝔎23 ∙NTCF ntcf_id 𝔗)⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix a assume prems: "a ∈∘ 2ℕ"
          then consider ‹a = 0› | ‹a = 1ℕ› unfolding two by auto
          then show 
            "η'⦇NTMap⦈⦇a⦈ = 
              (LK_σ23 𝔗 η' 𝔉' ∘NTCF-CF 𝔎23 ∙NTCF ntcf_id 𝔗)⦇NTMap⦈⦇a⦈"
            by (cases; use nothing in ‹simp_all only:›)
              (
                cs_concl 
                  cs_simp: 
                    omega_of_set 
                    cat_Kan_cs_simps 
                    cat_cs_simps 
                    cat_ordinal_cs_simps 
                  cs_intro: cat_Kan_cs_intros cat_cs_intros nat_omega_intros
              )+
        qed 
          (
            use rhs in 
              ‹cs_concl cs_shallow cs_intro: V_cs_intros cat_cs_intros›
          )+
      qed simp_all

      fix σ assume prems': 
        "σ : LK23 𝔗 ↦CF 𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
        "η' = σ ∘NTCF-CF 𝔎23 ∙NTCF ntcf_id 𝔗"

      interpret σ: is_ntcf α ‹cat_ordinal (3ℕ)› 𝔄 ‹LK23 𝔗› 𝔉' σ 
        by (rule prems'(1))

      from prems'(2) have 
        "η'⦇NTMap⦈⦇0⦈ = (σ ∘NTCF-CF 𝔎23 ∙NTCF ntcf_id 𝔗)⦇NTMap⦈⦇0⦈"
        by auto
      then have [cat_cs_simps]: "η'⦇NTMap⦈⦇0⦈ = σ⦇NTMap⦈⦇0⦈"
        by 
          (
            cs_prems cs_shallow
              cs_simp: cat_Kan_cs_simps cat_cs_simps cat_ordinal_cs_simps 
              cs_intro: cat_cs_intros nat_omega_intros
          )
      from prems'(2) have
        "η'⦇NTMap⦈⦇1ℕ⦈ = (σ ∘NTCF-CF 𝔎23 ∙NTCF ntcf_id 𝔗)⦇NTMap⦈⦇1ℕ⦈"
        by auto
      then have [cat_cs_simps]: "η'⦇NTMap⦈⦇1ℕ⦈ = σ⦇NTMap⦈⦇2ℕ⦈"
        by
          (
            cs_prems cs_shallow
              cs_simp:
                omega_of_set cat_Kan_cs_simps cat_cs_simps cat_ordinal_cs_simps
              cs_intro: cat_cs_intros nat_omega_intros
          )

      show "σ = LK_σ23 𝔗 η' 𝔉'"
      proof(rule ntcf_eqI)

        show "σ : LK23 𝔗 ↦CF 𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄" 
          by (rule prems'(1))
        then have dom_lhs: "𝒟∘ (σ⦇NTMap⦈) = 3ℕ"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
        show "LK_σ23 𝔗 η' 𝔉' : LK23 𝔗 ↦CF 𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ 𝔄"
          by (cs_concl cs_intro: cat_cs_intros cat_Kan_cs_intros)
        then have dom_rhs: "𝒟∘ (LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈) = 3ℕ"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
        from 0123 have 012: "[0, 1ℕ]∘ : 0 ↦⇘cat_ordinal (2ℕ)⇙ 1ℕ"
          by (cs_concl cs_intro: cat_ordinal_cs_intros nat_omega_intros)
        from 0123 have 013: "[0, 1ℕ]∘ : 0 ↦⇘cat_ordinal (3ℕ)⇙ 1ℕ"
          by (cs_concl cs_intro: cat_ordinal_cs_intros nat_omega_intros)
        from 0123 have 00: "[0, 0]∘ = (cat_ordinal (2ℕ))⦇CId⦈⦇0⦈"
          by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps)
        from σ.ntcf_Comp_commute[OF 013] 013 0123 
        have [symmetric, cat_Kan_cs_simps]:
          "σ⦇NTMap⦈⦇1ℕ⦈ = 𝔉'⦇ArrMap⦈⦇0, 1ℕ⦈∙ ∘A⇘𝔄⇙ σ⦇NTMap⦈⦇0⦈"
          by
            (
              cs_prems 
                cs_simp: cat_cs_simps cat_Kan_cs_simps 00 LK23_ArrMap_app_01
                cs_intro: cat_cs_intros cat_ordinal_cs_intros nat_omega_intros
            )

        show "σ⦇NTMap⦈ = LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix a assume prems: "a ∈∘ 3ℕ"
          then consider ‹a = 0› | ‹a = 1ℕ› | ‹a = 2ℕ› unfolding three by auto
          then show "σ⦇NTMap⦈⦇a⦈ = LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈"
            by (cases; use nothing in ‹simp_all only:›) 
              (
                cs_concl  
                  cs_simp: cat_ordinal_cs_simps cat_cs_simps cat_Kan_cs_simps 
                  cs_intro: cat_cs_intros
              )+
        qed auto
      qed simp_all

    qed

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

qed



subsection‹Pointwise Kan extensions along ‹𝔎23››

lemma ε23_is_cat_pw_rKe:
  assumes "𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
  shows "ntcf_id 𝔗 :
    RK23 𝔗 ∘CF 𝔎23 ↦CF.rKe.pw⇘α⇙ 𝔗 :
    cat_ordinal (2ℕ) ↦C cat_ordinal (3ℕ) ↦C 𝔄"
proof-

  interpret 𝔗: is_functor α ‹cat_ordinal (2ℕ)› 𝔄 𝔗 by (rule assms(1))

  show ?thesis
  proof(intro is_cat_pw_rKeI ε23_is_cat_rKe[OF assms])

    fix a assume prems: "a ∈∘ 𝔄⦇Obj⦈"
    
    show
      "ntcf_id 𝔗 : 
        RK23 𝔗 ∘CF 𝔎23 ↦CF.rKe⇘α⇙ 𝔗 :
        cat_ordinal (2ℕ) ↦C
        cat_ordinal (3ℕ) ↦C
        (HomO.C⇘α⇙𝔄(a,-) : 𝔄 ↦↦C cat_Set α)"
    proof(intro is_cat_rKe_preservesI ε23_is_cat_rKe[OF assms])
      from prems show "HomO.C⇘α⇙𝔄(a,-) : 𝔄 ↦↦C⇘α⇙ cat_Set α"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      show "HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF ntcf_id 𝔗 :
        (HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗) ∘CF 𝔎23 ↦CF.rKe⇘α⇙ HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗 :
        cat_ordinal (2ℕ) ↦C cat_ordinal (3ℕ) ↦C cat_Set α"
      proof(intro is_cat_rKeI')
        show "𝔎23 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ cat_ordinal (3ℕ)"
          by (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
        from prems show
          "HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗 : cat_ordinal (3ℕ) ↦↦C⇘α⇙ cat_Set α"
          by (cs_concl cs_intro: cat_cs_intros cat_Kan_cs_intros)
        from prems show 
          "HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF ntcf_id 𝔗 :
            HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗 ∘CF 𝔎23 ↦CF HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗 :
            cat_ordinal (2ℕ) ↦↦C⇘α⇙ cat_Set α"
          by
            (
              cs_concl 
                cs_simp: cat_cs_simps cat_Kan_cs_simps
                cs_intro: cat_cs_intros cat_Kan_cs_intros
            )

        fix 𝔊' ε' assume prems':
          "𝔊' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ cat_Set α"
          "ε' :
            𝔊' ∘CF 𝔎23 ↦CF HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗 :
            cat_ordinal (2ℕ) ↦↦C⇘α⇙ cat_Set α"

        interpret 𝔊': is_functor α ‹cat_ordinal (3ℕ)› ‹cat_Set α› 𝔊' 
          by (rule prems'(1))
        interpret ε': is_ntcf
          α
          ‹cat_ordinal (2ℕ)›
          ‹cat_Set α›
          ‹𝔊' ∘CF 𝔎23›
          ‹HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗›
          ε'
          by (rule prems'(2))

        show "∃!σ.
          σ :
            𝔊' ↦CF HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗 :
            cat_ordinal (3ℕ) ↦↦C⇘α⇙ cat_Set α ∧
          ε' = HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF ntcf_id 𝔗 ∙NTCF (σ ∘NTCF-CF 𝔎23)"
        proof(intro ex1I conjI; (elim conjE)?)
          have [cat_Kan_cs_simps]: 
            "HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗 = RK23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗)"
          proof(rule cf_eqI)
            from prems show lhs: "HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗 : 
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ cat_Set α"
              by
                (
                  cs_concl 
                    cs_simp: cat_cs_simps
                    cs_intro: cat_cs_intros cat_Kan_cs_intros
                )
            from prems show rhs: "RK23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) : 
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ cat_Set α"
              by
                (
                  cs_concl
                    cs_simp: cat_cs_simps
                    cs_intro: cat_cs_intros cat_Kan_cs_intros
                )
            from lhs prems have ObjMap_dom_lhs: 
              "𝒟∘ ((HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗)⦇ObjMap⦈) = 3ℕ"
              by
                (
                  cs_concl 
                    cs_simp: cat_ordinal_cs_simps cat_cs_simps 
                    cs_intro: cat_Kan_cs_intros cat_cs_intros
                )
            from rhs prems have ObjMap_dom_rhs:
              "𝒟∘ ((RK23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗))⦇ObjMap⦈) = 3ℕ"
              by 
                (
                  cs_concl cs_shallow 
                    cs_simp: cat_ordinal_cs_simps cat_cs_simps 
                    cs_intro: cat_Kan_cs_intros 
                )
            show 
              "(HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗)⦇ObjMap⦈ =
                RK23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗)⦇ObjMap⦈"
            proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
              fix c assume prems'': "c ∈∘ 3ℕ"
              with 0123 consider ‹c = 0› | ‹c = 1ℕ› | ‹c = 2ℕ› by force
              from this prems prems'' 0123 show 
                "(HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗)⦇ObjMap⦈⦇c⦈ =
                  RK23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗)⦇ObjMap⦈⦇c⦈"
                by (cases; use nothing in ‹simp_all only:›)
                  (
                    cs_concl 
                      cs_simp:
                        cat_ordinal_cs_simps
                        cat_cs_simps
                        cat_op_simps
                        cat_Kan_cs_simps
                      cs_intro: cat_Kan_cs_intros cat_cs_intros
                 )+
            qed 
              (
                use prems in ‹
                  cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros
                  ›
              )+
            from lhs prems have ArrMap_dom_lhs: 
              "𝒟∘ ((HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗)⦇ArrMap⦈) = 
                cat_ordinal (3ℕ)⦇Arr⦈"
              by
                (
                  cs_concl 
                    cs_simp: cat_ordinal_cs_simps cat_cs_simps 
                    cs_intro: cat_Kan_cs_intros cat_cs_intros
                )
            from rhs prems have ArrMap_dom_rhs:
              "𝒟∘ ((RK23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗))⦇ArrMap⦈) = 
                cat_ordinal (3ℕ)⦇Arr⦈"
              by 
                (
                  cs_concl cs_shallow 
                    cs_simp: cat_ordinal_cs_simps cat_cs_simps 
                    cs_intro: cat_Kan_cs_intros 
                )
            show 
              "(HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗)⦇ArrMap⦈ =
                RK23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗)⦇ArrMap⦈"
            proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
              fix f assume prems'': "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
              then obtain a' b' where "f : a' ↦⇘cat_ordinal (3ℕ)⇙ b'" by auto
              from this 0123 prems show 
                "(HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗)⦇ArrMap⦈⦇f⦈ =
                  RK23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗)⦇ArrMap⦈⦇f⦈"
                by (*slow*)
                  (
                    elim cat_ordinal_3_is_arrE;
                    use nothing in ‹simp_all only:›
                  )
                  (
                    cs_concl
                      cs_simp: cat_cs_simps cat_Kan_cs_simps cat_op_simps
                      cs_intro:
                        cat_ordinal_cs_intros
                        cat_Kan_cs_intros
                        cat_cs_intros
                        nat_omega_intros
                  )+
            qed 
              (
                use prems in 
                  ‹cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros›
              )+
          qed simp_all

          show "RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊' : 
            𝔊' ↦CF HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗 : 
            cat_ordinal (3ℕ) ↦↦C⇘α⇙ cat_Set α"
            by (intro RK_σ23_is_ntcf')
              (
                cs_concl cs_shallow 
                  cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros
              )+
          show "ε' = 
            HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF 
            ntcf_id 𝔗 ∙NTCF 
            (RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊' ∘NTCF-CF 𝔎23)"
          proof(rule ntcf_eqI)
            show "ε' :
              𝔊' ∘CF 𝔎23 ↦CF HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗 :
              cat_ordinal (2ℕ) ↦↦C⇘α⇙ cat_Set α"
              by (intro prems')
            then have dom_lhs: "𝒟∘ (ε'⦇NTMap⦈) = 2ℕ"
              by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
            from prems show 
              "HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF 
                ntcf_id 𝔗 ∙NTCF 
                (RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊' ∘NTCF-CF 𝔎23) :
              𝔊' ∘CF 𝔎23 ↦CF HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗 :
              cat_ordinal (2ℕ) ↦↦C⇘α⇙ cat_Set α"
              by
                (
                  cs_concl 
                    cs_simp: cat_Kan_cs_simps
                    cs_intro: cat_Kan_cs_intros cat_cs_intros
                )
            then have dom_rhs: 
              "𝒟∘ 
                (
                  (HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF
                  ntcf_id 𝔗 ∙NTCF 
                  (RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊' ∘NTCF-CF 𝔎23)
                )⦇NTMap⦈) = 2ℕ"
              by (cs_concl cs_simp: cat_ordinal_cs_simps cat_cs_simps)
            show "ε'⦇NTMap⦈ =
              (
                HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF
                ntcf_id 𝔗 ∙NTCF
                (RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊' ∘NTCF-CF 𝔎23)
              )⦇NTMap⦈"
            proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
              fix c assume prems'': "c ∈∘ 2ℕ"
              then consider ‹c = 0› | ‹c = 1ℕ› unfolding two by auto
              from this prems 0123 show "ε'⦇NTMap⦈⦇c⦈ =
                (
                  HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF 
                  ntcf_id 𝔗 ∙NTCF 
                  (RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊' ∘NTCF-CF 𝔎23)
                )⦇NTMap⦈⦇c⦈"
                by (cases; use nothing in ‹simp_all only:›) 
                  (
                    cs_concl
                      cs_simp: 
                        cat_Kan_cs_simps 
                        cat_ordinal_cs_simps
                        cat_cs_simps 
                        cat_op_simps 
                        RK_σ23_NTMap_app_0 
                        cat_Set_components(1)
                      cs_intro: 
                        cat_Kan_cs_intros 
                        cat_cs_intros 
                        cat_prod_cs_intros 
                        𝔗.HomCod.cat_Hom_in_Vset
                  )+
            qed (cs_concl cs_intro: cat_cs_intros V_cs_intros)+

          qed simp_all

          fix σ assume prems'':
            "σ :
              𝔊' ↦CF HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗 :
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ cat_Set α"
            "ε' = HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF ntcf_id 𝔗 ∙NTCF (σ ∘NTCF-CF 𝔎23)"

          interpret σ: is_ntcf 
            α ‹cat_ordinal (3ℕ)› ‹cat_Set α› 𝔊' ‹HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗› σ
            by (rule prems''(1))

          from prems''(2) have "ε'⦇NTMap⦈⦇0⦈ =
            (HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF ntcf_id 𝔗 ∙NTCF (σ ∘NTCF-CF 𝔎23))⦇NTMap⦈⦇0⦈"
            by auto
          from this prems 0123 have ε'_NTMap_app_0: "ε'⦇NTMap⦈⦇0⦈ = σ⦇NTMap⦈⦇0⦈"
            by
              (
                cs_prems  
                  cs_simp:
                    cat_ordinal_cs_simps
                    cat_cs_simps
                    cat_Kan_cs_simps
                    cat_op_simps
                    𝔎23_ObjMap_app_0
                    cat_Set_components(1)
                  cs_intro: 
                    cat_Kan_cs_intros
                    cat_cs_intros
                    cat_prod_cs_intros
                    𝔗.HomCod.cat_Hom_in_Vset
              )
          from 0123 have 01: "[0, 1ℕ]∘ : 0 ↦⇘cat_ordinal (2ℕ)⇙ 1ℕ"
            by
              (
                cs_concl
                  cs_simp: cat_cs_simps
                  cs_intro: cat_ordinal_cs_intros nat_omega_intros
              )
          from prems''(2) have 
            "ε'⦇NTMap⦈⦇1ℕ⦈ =
              (
                HomO.C⇘α⇙𝔄(a,-) ∘CF-NTCF ntcf_id 𝔗 ∙NTCF (σ ∘NTCF-CF 𝔎23)
              )⦇NTMap⦈⦇1ℕ⦈"
            by auto
          from this prems 0123 have ε'_NTMap_app_1:  
            "ε'⦇NTMap⦈⦇1ℕ⦈ = σ⦇NTMap⦈⦇2ℕ⦈"
            by
              (
                cs_prems
                  cs_simp:
                    cat_ordinal_cs_simps
                    cat_cs_simps
                    cat_Kan_cs_simps
                    cat_op_simps
                    𝔎23_ObjMap_app_1
                    cat_Set_components(1)
                  cs_intro: 
                    cat_Kan_cs_intros
                    cat_cs_intros
                    cat_prod_cs_intros
                    𝔗.HomCod.cat_Hom_in_Vset
              )

          from 0123 have 012: "[0, 1ℕ]∘ : 0 ↦⇘cat_ordinal (2ℕ)⇙ 1ℕ"
            by 
              (
                cs_concl cs_intro:
                  cat_ordinal_cs_intros nat_omega_intros
              )
          from 0123 have 013: "[0, 1ℕ]∘ : 0 ↦⇘cat_ordinal (3ℕ)⇙ 1ℕ"
            by 
              ( 
                cs_concl cs_intro: 
                  cat_ordinal_cs_intros nat_omega_intros
              )
          from 0123 have 123: "[1ℕ, 2ℕ]∘ : 1ℕ ↦⇘cat_ordinal (3ℕ)⇙ 2ℕ"
            by 
              (
                cs_concl cs_intro:
                  cat_ordinal_cs_intros nat_omega_intros
              )
          from 0123 have 11: "[1ℕ, 1ℕ]∘ = (cat_ordinal (2ℕ))⦇CId⦈⦇1ℕ⦈"
            by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps)

          from σ.ntcf_Comp_commute[OF 123] prems 012 013 
          have [cat_Kan_cs_simps]:
            "ε'⦇NTMap⦈⦇1ℕ⦈ ∘A⇘cat_Set α⇙ 𝔊'⦇ArrMap⦈⦇1ℕ, 2ℕ⦈∙ = σ⦇NTMap⦈⦇1ℕ⦈"
            by (*slow*)
              (
                cs_prems 
                  cs_simp:
                    cat_cs_simps
                    cat_Kan_cs_simps
                    ε'_NTMap_app_1[symmetric]
                    is_functor.cf_ObjMap_CId
                    RK23_ArrMap_app_12
                    11
                  cs_intro: cat_cs_intros nat_omega_intros 
              )
          
          show "σ = RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊'"
          proof(rule ntcf_eqI)

            show σ: "σ : 
              𝔊' ↦CF HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗 : 
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ cat_Set α"
              by (rule prems''(1))
            then have dom_lhs: "𝒟∘ (σ⦇NTMap⦈) = 3ℕ"
              by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
            show "RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊' :
              𝔊' ↦CF HomO.C⇘α⇙𝔄(a,-) ∘CF RK23 𝔗 : 
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ cat_Set α"
              by 
                (
                  cs_concl cs_shallow
                    cs_simp: cat_Kan_cs_simps 
                    cs_intro: cat_Kan_cs_intros cat_cs_intros
                )
            then have dom_rhs: 
              "𝒟∘ (RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊'⦇NTMap⦈) = 3ℕ"
              by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
            show "σ⦇NTMap⦈ = RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊'⦇NTMap⦈"
            proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
              fix c assume "c ∈∘ 3ℕ"
              then consider ‹c = 0› | ‹c = 1ℕ› | ‹c = 2ℕ›  
                unfolding three by auto
              from this 0123 show
                "σ⦇NTMap⦈⦇c⦈ = RK_σ23 (HomO.C⇘α⇙𝔄(a,-) ∘CF 𝔗) ε' 𝔊'⦇NTMap⦈⦇c⦈"
                by (cases; use nothing in ‹simp_all only:›)
                  (
                    cs_concl cs_simp:
                      cat_Kan_cs_simps ε'_NTMap_app_1 ε'_NTMap_app_0
                  )+
            qed (cs_concl  cs_intro: cat_Kan_cs_intros V_cs_intros)+

          qed simp_all

        qed

      qed

    qed

  qed

qed

lemma η23_is_cat_pw_lKe:
  assumes "𝔗 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ 𝔄"
  shows "ntcf_id 𝔗 :
    𝔗 ↦CF.lKe.pw⇘α⇙ LK23 𝔗 ∘CF 𝔎23 :
    cat_ordinal (2ℕ) ↦C cat_ordinal (3ℕ) ↦C 𝔄"
proof-

  interpret 𝔗: is_functor α ‹cat_ordinal (2ℕ)› 𝔄 𝔗 by (rule assms(1))

  from ord_of_nat_ω interpret cat_ordinal_3: finite_category α ‹cat_ordinal (3ℕ)›
    by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)

  from 0123 have 002: "[0, 0]∘ : 0 ↦⇘cat_ordinal (2ℕ)⇙ 0"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_ordinal_cs_simps cs_intro: cat_cs_intros
      )

  show ?thesis
  proof(intro is_cat_pw_lKeI η23_is_cat_rKe assms, unfold cat_op_simps)
    fix a assume prems: "a ∈∘ 𝔄⦇Obj⦈"
    show 
      "op_ntcf (ntcf_id 𝔗) :
        op_cf (LK23 𝔗) ∘CF op_cf 𝔎23 ↦CF.rKe⇘α⇙ op_cf 𝔗 :
        op_cat (cat_ordinal (2ℕ)) ↦C op_cat (cat_ordinal (3ℕ)) ↦C
        (HomO.C⇘α⇙𝔄(-,a) : op_cat 𝔄 ↦↦C cat_Set α)"
    proof(intro is_cat_rKe_preservesI)
      show 
        "op_ntcf (ntcf_id 𝔗) :
          op_cf (LK23 𝔗) ∘CF op_cf 𝔎23 ↦CF.rKe⇘α⇙ op_cf 𝔗 :
          op_cat (cat_ordinal (2ℕ)) ↦C op_cat (cat_ordinal (3ℕ)) ↦C op_cat 𝔄"
      proof(cs_intro_step cat_op_intros)
        show "ntcf_id 𝔗 :
          𝔗 ↦CF.lKe⇘α⇙ LK23 𝔗 ∘CF 𝔎23 :
          cat_ordinal (2ℕ) ↦C cat_ordinal (3ℕ) ↦C 𝔄"
          by (intro η23_is_cat_rKe assms)
      qed simp_all
      from prems show "HomO.C⇘α⇙𝔄(-,a) : op_cat 𝔄 ↦↦C⇘α⇙ cat_Set α"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)

      have 
        "op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗 :
          op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗 ↦CF.lKe⇘α⇙
          (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗) ∘CF 𝔎23 :
          cat_ordinal (2ℕ) ↦C cat_ordinal (3ℕ) ↦C op_cat (cat_Set α)"
      proof(intro is_cat_lKeI')
        show "𝔎23 : cat_ordinal (2ℕ) ↦↦C⇘α⇙ cat_ordinal (3ℕ)"
          by (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
        from prems show "op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗 :
          cat_ordinal (3ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
          by 
            (
              cs_concl
                cs_simp: cat_cs_simps cat_op_simps 
                cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
            )

        from prems show 
          "op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗 :
            op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗 ↦CF 
            op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗 ∘CF 𝔎23 :
            cat_ordinal (2ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
          by 
            (
              cs_concl 
                cs_simp: cat_cs_simps cat_Kan_cs_simps cat_op_simps
                cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
            )

        fix 𝔉' η' assume prems':
          "𝔉' : cat_ordinal (3ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
          "η' :
            op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗 ↦CF 𝔉' ∘CF 𝔎23 :
            cat_ordinal (2ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"

        interpret 𝔉': is_functor α ‹cat_ordinal (3ℕ)› ‹op_cat (cat_Set α)› 𝔉'
          by (rule prems'(1))
        interpret η': is_ntcf
          α
          ‹cat_ordinal (2ℕ)›
          ‹op_cat (cat_Set α)›
          ‹op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗› 
          ‹𝔉' ∘CF 𝔎23› 
          η'
          by (rule prems'(2))
        note [unfolded cat_op_simps, cat_cs_intros] = 
          η'.ntcf_NTMap_is_arr'
          𝔉'.cf_ArrMap_is_arr'
        show
          "∃!σ.
            σ :
              op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗 ↦CF 𝔉' :
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α) ∧
            η' = σ ∘NTCF-CF 𝔎23 ∙NTCF (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗)"
        proof(intro ex1I conjI; (elim conjE)?) 
          have [cat_Kan_cs_simps]:
            "op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗 =
              LK23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗)"
          proof(rule cf_eqI)
            from prems show lhs: "op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗 :
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
              by
                (
                  cs_concl 
                    cs_simp: cat_op_simps
                    cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
                )
            from prems show rhs: "LK23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) :
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
              by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
            from lhs prems have ObjMap_dom_lhs:
              "𝒟∘ ((op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗)⦇ObjMap⦈) = 3ℕ"
              by
                (
                  cs_concl 
                    cs_simp: cat_ordinal_cs_simps cat_cs_simps cat_op_simps 
                    cs_intro: cat_Kan_cs_intros cat_cs_intros
                )
            from rhs prems have ObjMap_dom_rhs:
              "𝒟∘ (LK23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗)⦇ObjMap⦈) = 3ℕ"
              by 
                (
                  cs_concl cs_shallow 
                    cs_simp: cat_ordinal_cs_simps cat_cs_simps
                )
            show
              "(op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗)⦇ObjMap⦈ =
                LK23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗)⦇ObjMap⦈"
            proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
             fix c assume prems'': "c ∈∘ 3ℕ"
             then consider ‹c = 0› | ‹c = 1ℕ› | ‹c = 2ℕ› 
               unfolding three by auto
              from this prems 0123 show 
                "(op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗)⦇ObjMap⦈⦇c⦈ =
                  LK23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗)⦇ObjMap⦈⦇c⦈"
                by (cases; use nothing in ‹simp_all only:›)
                  (
                    cs_concl
                      cs_simp:
                        cat_ordinal_cs_simps 
                        cat_Kan_cs_simps 
                        cat_cs_simps 
                        cat_op_simps
                      cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
                  )+
            qed
              (
                use prems in 
                  ‹
                    cs_concl
                      cs_simp: cat_op_simps 
                      cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
                  ›
              )+

            from lhs prems have ArrMap_dom_lhs:
              "𝒟∘ ((op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗)⦇ArrMap⦈) = 
                cat_ordinal (3ℕ)⦇Arr⦈"
              by
                (
                  cs_concl 
                    cs_simp: cat_ordinal_cs_simps cat_cs_simps cat_op_simps 
                    cs_intro: cat_Kan_cs_intros cat_cs_intros
                )
            from rhs prems have ArrMap_dom_rhs:
              "𝒟∘ (LK23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗)⦇ArrMap⦈) =
                cat_ordinal (3ℕ)⦇Arr⦈"
              by (cs_concl cs_shallow cs_simp: cat_cs_simps)

            show
              "(op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗)⦇ArrMap⦈ =
                LK23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗)⦇ArrMap⦈"
            proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
              fix f assume "f ∈∘ cat_ordinal (3ℕ)⦇Arr⦈"
              then obtain a' b' where f: "f : a' ↦⇘cat_ordinal (3ℕ)⇙ b'" 
                by auto
              from f prems 0123 002 show
                "(op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗)⦇ArrMap⦈⦇f⦈ =
                  LK23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗)⦇ArrMap⦈⦇f⦈"
                by (elim cat_ordinal_3_is_arrE, (simp_all only:)?)
                  (
                    cs_concl 
                      cs_simp: cat_cs_simps cat_Kan_cs_simps cat_op_simps 
                      cs_intro: 
                        cat_ordinal_cs_intros 
                        cat_Kan_cs_intros 
                        cat_cs_intros   
                        cat_op_intros 
                        nat_omega_intros
                  )+
            qed
              (
                use prems in
                  ‹
                    cs_concl 
                      cs_simp: cat_op_simps
                      cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros›
              )+
          
          qed simp_all

          show "LK_σ23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉' : 
            op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗 ↦CF 𝔉' : 
            cat_ordinal (3ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
            by
              (
                cs_concl cs_shallow
                  cs_simp: cat_cs_simps cat_Kan_cs_simps cat_op_simps 
                  cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
              )

          show "η' =
            LK_σ23
              (
                op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉' ∘NTCF-CF
                𝔎23 ∙NTCF 
                (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗
              )"
          proof(rule ntcf_eqI)
            show lhs: "η' :
              op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗 ↦CF 𝔉' ∘CF 𝔎23 :
              cat_ordinal (2ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
              by (rule prems'(2))
            from lhs have "𝒟∘ (η'⦇NTMap⦈) = cat_ordinal (2ℕ)⦇Obj⦈"
              by (cs_concl cs_shallow cs_simp: cat_cs_simps)
            from prems show rhs: 
              "LK_σ23
                (
                  op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉' ∘NTCF-CF 
                  𝔎23 ∙NTCF 
                  (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗
                ) : 
              op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗 ↦CF 𝔉' ∘CF 𝔎23 :
              cat_ordinal (2ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
              by 
                (
                  cs_concl
                    cs_simp: cat_Kan_cs_simps cat_op_simps 
                    cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
                )
            from lhs have dom_lhs: "𝒟∘ (η'⦇NTMap⦈) = 2ℕ"
              by 
                (
                  cs_concl cs_shallow 
                    cs_simp: cat_ordinal_cs_simps cat_cs_simps
                )
            from rhs have dom_rhs: "𝒟∘ ((LK_σ23
              (
                op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉' ∘NTCF-CF 
                𝔎23 ∙NTCF
                (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗
              ))⦇NTMap⦈) = 2ℕ"
              by (cs_concl cs_simp: cat_ordinal_cs_simps cat_cs_simps)
            show
              "η'⦇NTMap⦈ =
                (
                  LK_σ23
                    (
                      op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉' ∘NTCF-CF
                      𝔎23 ∙NTCF 
                      (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗
                    )
                )⦇NTMap⦈"
            proof(rule vsv_eqI, unfold dom_lhs dom_rhs cat_ordinal_cs_simps)
              fix c assume "c ∈∘ 2ℕ"
              then consider ‹c = 0› | ‹c = 1ℕ› unfolding two by auto
              from this prems 0123 show 
                "η'⦇NTMap⦈⦇c⦈ = 
                  (
                    LK_σ23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉' ∘NTCF-CF 
                    𝔎23 ∙NTCF (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗)
                  )⦇NTMap⦈⦇c⦈"
                by (cases, use nothing in ‹simp_all only:›)
                  (
                    cs_concl 
                      cs_simp: 
                        cat_ordinal_cs_simps 
                        cat_Kan_cs_simps 
                        cat_cs_simps 
                        cat_op_simps 
                        𝔎23_ObjMap_app_1 
                        𝔎23_ObjMap_app_0 
                        LK_σ23_NTMap_app_0 
                        cat_Set_components(1) 
                      cs_intro: 
                        cat_Kan_cs_intros 
                        cat_cs_intros 
                        cat_prod_cs_intros 
                        cat_op_intros 
                        𝔗.HomCod.cat_Hom_in_Vset
                  )+
            qed (cs_concl cs_intro: V_cs_intros cat_cs_intros)+
          qed simp_all

          fix σ assume prems'':
            "σ : 
              op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗 ↦CF 𝔉' : 
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
            "η' = σ ∘NTCF-CF 𝔎23 ∙NTCF (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗)"

          interpret σ: is_ntcf 
            α
            ‹cat_ordinal (3ℕ)› ‹op_cat (cat_Set α)› 
            ‹op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗› 
            𝔉' 
            σ
            by (rule prems''(1))

          note [cat_Kan_cs_intros] = σ.ntcf_NTMap_is_arr'[unfolded cat_op_simps]

          from prems''(2) have 
            "η'⦇NTMap⦈⦇0⦈ =
              (
                σ ∘NTCF-CF
                𝔎23 ∙NTCF
                (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗)
              )⦇NTMap⦈⦇0⦈"
            by simp
          from this prems 0123 have η'_NTMap_app_0: "η'⦇NTMap⦈⦇0⦈ = σ⦇NTMap⦈⦇0⦈"
            by (*very slow*) 
              (
                cs_prems 
                  cs_simp: 
                    cat_ordinal_cs_simps
                    cat_Kan_cs_simps 
                    cat_cs_simps 
                    cat_op_simps 
                    cat_Set_components(1)
                  cs_intro: 
                    cat_Kan_cs_intros 
                    cat_cs_intros 
                    cat_prod_cs_intros
                    cat_op_intros 
                    𝔗.HomCod.cat_Hom_in_Vset
              )

          from prems''(2) have 
            "η'⦇NTMap⦈⦇1ℕ⦈ =
              (
                σ ∘NTCF-CF
                𝔎23 ∙NTCF
                (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF ntcf_id 𝔗)
              )⦇NTMap⦈⦇1ℕ⦈"
            by simp
          from this prems 0123 have η'_NTMap_app_1: "η'⦇NTMap⦈⦇1ℕ⦈ = σ⦇NTMap⦈⦇2ℕ⦈"
            by (*very slow*) 
              (
                cs_prems
                  cs_simp:
                    cat_ordinal_cs_simps
                    cat_Kan_cs_simps
                    cat_cs_simps
                    cat_op_simps
                    cat_Set_components(1)
                  cs_intro:
                    cat_Kan_cs_intros
                    cat_cs_intros
                    cat_prod_cs_intros
                    cat_op_intros
                    𝔗.HomCod.cat_Hom_in_Vset
              )+

          from 0123 have 013: "[0, 1ℕ]∘ : 0 ↦⇘cat_ordinal (3ℕ)⇙ 1ℕ"
            by (cs_concl cs_intro: cat_ordinal_cs_intros nat_omega_intros)
          from 0123 have 00: "[0, 0]∘ = (cat_ordinal (2ℕ))⦇CId⦈⦇0⦈"
            by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps)

          from σ.ntcf_Comp_commute[OF 013] prems 0123 013
          have [cat_Kan_cs_simps]:
            "σ⦇NTMap⦈⦇1ℕ⦈ = η'⦇NTMap⦈⦇0⦈ ∘A⇘cat_Set α⇙ 𝔉'⦇ArrMap⦈⦇0, 1ℕ⦈∙"
            by
              (
                cs_prems
                  cs_simp:
                    cat_ordinal_cs_simps
                    cat_Kan_cs_simps
                    cat_cs_simps
                    cat_op_simps
                    LK23_ArrMap_app_01
                  cs_intro: 
                    cat_ordinal_cs_intros
                    cat_Kan_cs_intros
                    cat_cs_intros
                    cat_prod_cs_intros
                    cat_op_intros
                    nat_omega_intros
                  cs_simp: 00 η'_NTMap_app_0[symmetric]
              )

          show "σ = LK_σ23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉'"
          proof(rule ntcf_eqI)
            show lhs: "σ :
              op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗 ↦CF 𝔉' :
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
              by (rule prems''(1))
            show rhs: "LK_σ23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉' : 
              op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF LK23 𝔗 ↦CF 𝔉' :
              cat_ordinal (3ℕ) ↦↦C⇘α⇙ op_cat (cat_Set α)"
              by
                (
                  cs_concl cs_shallow
                    cs_simp: cat_Kan_cs_simps 
                    cs_intro: cat_Kan_cs_intros cat_cs_intros
                )
            from lhs have dom_lhs: "𝒟∘ (σ⦇NTMap⦈) = 3ℕ"
              by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
            from rhs have dom_rhs:
              "𝒟∘ (LK_σ23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉'⦇NTMap⦈) = 3ℕ"
              by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)

            show "σ⦇NTMap⦈ = LK_σ23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉'⦇NTMap⦈"
            proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
              fix c assume "c ∈∘ 3ℕ"
              then consider ‹c = 0› | ‹c = 1ℕ› | ‹c = 2ℕ› 
                unfolding three by auto
              from this 0123 show 
                "σ⦇NTMap⦈⦇c⦈ =
                  LK_σ23 (op_cf HomO.C⇘α⇙𝔄(-,a) ∘CF 𝔗) η' 𝔉'⦇NTMap⦈⦇c⦈"
                by (cases, use nothing in ‹simp_all only:›)
                  (
                    cs_concl 
                      cs_simp:
                        cat_ordinal_cs_simps
                        cat_cs_simps
                        cat_Kan_cs_simps
                        cat_op_simps
                        η'_NTMap_app_0
                        LK_σ23_NTMap_app_0
                        η'_NTMap_app_1
                      cs_intro: 
                        cat_ordinal_cs_intros
                        cat_Kan_cs_intros
                        cat_cs_intros
                        cat_op_intros
                        nat_omega_intros
                  )+
            qed (cs_concl cs_intro: cat_Kan_cs_intros V_cs_intros)+

          qed simp_all

        qed

      qed

      then have 
        "op_ntcf (HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF op_ntcf (ntcf_id 𝔗)) :
          op_cf (HomO.C⇘α⇙𝔄(-,a) ∘CF op_cf 𝔗) ↦CF.lKe⇘α⇙
          op_cf ((HomO.C⇘α⇙𝔄(-,a) ∘CF op_cf (LK23 𝔗))) ∘CF op_cf (op_cf 𝔎23) :
          op_cat (op_cat (cat_ordinal (2ℕ))) ↦C
          op_cat (op_cat (cat_ordinal (3ℕ))) ↦C
          op_cat (cat_Set α)"
        by
          (
            cs_concl 
              cs_simp: cat_op_simps 
              cs_intro: cat_cs_intros cat_Kan_cs_intros cat_op_intros
          )
      from is_cat_lKe.is_cat_rKe_op[OF this] prems show
        "HomO.C⇘α⇙𝔄(-,a) ∘CF-NTCF op_ntcf (ntcf_id 𝔗) :
          (HomO.C⇘α⇙𝔄(-,a) ∘CF op_cf (LK23 𝔗)) ∘CF op_cf 𝔎23 ↦CF.rKe⇘α⇙
          HomO.C⇘α⇙𝔄(-,a) ∘CF op_cf 𝔗 :
          op_cat (cat_ordinal (2ℕ)) ↦C 
          op_cat (cat_ordinal (3ℕ)) ↦C
          cat_Set α"
        by
          (
            cs_prems
              cs_simp: cat_op_simps 
              cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
          )

    qed

  qed

qed

text‹\newpage›

end