Theory CZH_UCAT_Kan

(* Copyright 2021 (C) Mihails Milehins *)

section‹Simple Kan extensions›
theory CZH_UCAT_Kan
  imports 
    CZH_Elementary_Categories.CZH_ECAT_Comma
    CZH_UCAT_Adjoints
begin



subsection‹Background›

named_theorems cat_Kan_cs_simps
named_theorems cat_Kan_cs_intros



subsection‹Kan extension›


subsubsection‹Definition and elementary properties›


text‹See Chapter X-3 in cite‹"mac_lane_categories_2010"›.›

locale is_cat_rKe = 
  AG: is_functor α 𝔅 ℭ 𝔎 + 
  Ran: is_functor α ℭ 𝔄 𝔊 +
  ntcf_rKe: is_ntcf α 𝔅 𝔄 ‹𝔊 ∘CF 𝔎› 𝔗 ε
  for α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔊 ε +
  assumes cat_rKe_ua_fo:
    "universal_arrow_fo
      (exp_cat_cf α 𝔄 𝔎)
      (cf_map 𝔗)
      (cf_map 𝔊)
      (ntcf_arrow ε)"

syntax "_is_cat_rKe" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ∘CF _ ↦CF.rKeı _ :/ _ ↦C _ ↦C _)› [51, 51, 51, 51, 51, 51, 51] 51)
translations "ε : 𝔊 ∘CF 𝔎 ↦CF.rKe⇘α⇙ 𝔗 : 𝔅 ↦C ℭ ↦C 𝔄" ⇌ 
  "CONST is_cat_rKe α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔊 ε"

locale is_cat_lKe =
  AG: is_functor α 𝔅 ℭ 𝔎 +
  Lan: is_functor α ℭ 𝔄 𝔉 +
  ntcf_lKe: is_ntcf α 𝔅 𝔄 𝔗 ‹𝔉 ∘CF 𝔎› η
  for α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔉 η +
  assumes cat_lKe_ua_fo:
    "universal_arrow_fo
      (exp_cat_cf α (op_cat 𝔄) (op_cf 𝔎))
      (cf_map 𝔗)
      (cf_map 𝔉)
      (ntcf_arrow (op_ntcf η))"

syntax "_is_cat_lKe" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦CF.lKeı _ ∘CF _ :/ _ ↦C _ ↦C _)› [51, 51, 51, 51, 51, 51, 51] 51)
translations "η : 𝔗 ↦CF.lKe⇘α⇙ 𝔉 ∘CF 𝔎 : 𝔅 ↦C ℭ ↦C 𝔄" ⇌ 
  "CONST is_cat_lKe α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔉 η"


text‹Rules.›

lemma (in is_cat_rKe) is_cat_rKe_axioms'[cat_Kan_cs_intros]:
  assumes "α' = α"
    and "𝔊' = 𝔊"
    and "𝔎' = 𝔎"
    and "𝔗' = 𝔗"
    and "𝔅' = 𝔅"
    and "𝔄' = 𝔄"
    and "ℭ' = ℭ"
  shows "ε : 𝔊' ∘CF 𝔎' ↦CF.rKe⇘α'⇙ 𝔗' : 𝔅' ↦C ℭ' ↦C 𝔄'"
  unfolding assms by (rule is_cat_rKe_axioms)

mk_ide rf is_cat_rKe_def[unfolded is_cat_rKe_axioms_def]
  |intro is_cat_rKeI|
  |dest is_cat_rKeD[dest]|
  |elim is_cat_rKeE[elim]|

lemmas [cat_Kan_cs_intros] = is_cat_rKeD(1-3)

lemma (in is_cat_lKe) is_cat_lKe_axioms'[cat_Kan_cs_intros]:
  assumes "α' = α"
    and "𝔉' = 𝔉"
    and "𝔎' = 𝔎"
    and "𝔗' = 𝔗"
    and "𝔅' = 𝔅"
    and "𝔄' = 𝔄"
    and "ℭ' = ℭ"
  shows "η : 𝔗' ↦CF.lKe⇘α⇙ 𝔉' ∘CF 𝔎' : 𝔅' ↦C ℭ' ↦C 𝔄'"
  unfolding assms by (rule is_cat_lKe_axioms)

mk_ide rf is_cat_lKe_def[unfolded is_cat_lKe_axioms_def]
  |intro is_cat_lKeI|
  |dest is_cat_lKeD[dest]|
  |elim is_cat_lKeE[elim]|

lemmas [cat_Kan_cs_intros] = is_cat_lKeD(1-3)


text‹Duality.›

lemma (in is_cat_rKe) is_cat_lKe_op:
  "op_ntcf ε :
    op_cf 𝔗 ↦CF.lKe⇘α⇙ op_cf 𝔊 ∘CF op_cf 𝔎 :
    op_cat 𝔅 ↦C op_cat ℭ ↦C op_cat 𝔄"
  by (intro is_cat_lKeI, unfold cat_op_simps; (intro cat_rKe_ua_fo)?)
    (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)+

lemma (in is_cat_rKe) is_cat_lKe_op'[cat_op_intros]:
  assumes "𝔗' = op_cf 𝔗"
    and "𝔊' = op_cf 𝔊"
    and "𝔎' = op_cf 𝔎"
    and "𝔅' = op_cat 𝔅"
    and "𝔄' = op_cat 𝔄"
    and "ℭ' = op_cat ℭ"
  shows "op_ntcf ε : 𝔗' ↦CF.lKe⇘α⇙ 𝔊' ∘CF 𝔎' : 𝔅' ↦C ℭ' ↦C 𝔄'"
  unfolding assms by (rule is_cat_lKe_op)

lemmas [cat_op_intros] = is_cat_rKe.is_cat_lKe_op'

lemma (in is_cat_lKe) is_cat_rKe_op:
  "op_ntcf η :
    op_cf 𝔉 ∘CF op_cf 𝔎 ↦CF.rKe⇘α⇙ op_cf 𝔗 :
    op_cat 𝔅 ↦C op_cat ℭ ↦C op_cat 𝔄"
  by (intro is_cat_rKeI, unfold cat_op_simps; (intro cat_lKe_ua_fo)?)
    (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)+

lemma (in is_cat_lKe) is_cat_lKe_op'[cat_op_intros]:
  assumes "𝔗' = op_cf 𝔗"
    and "𝔉' = op_cf 𝔉"
    and "𝔎' = op_cf 𝔎"
    and "𝔅' = op_cat 𝔅"
    and "𝔄' = op_cat 𝔄"
    and "ℭ' = op_cat ℭ"
  shows "op_ntcf η : 𝔉' ∘CF 𝔎' ↦CF.rKe⇘α⇙ 𝔗' : 𝔅' ↦C ℭ' ↦C 𝔄'"
  unfolding assms by (rule is_cat_rKe_op)

lemmas [cat_op_intros] = is_cat_lKe.is_cat_lKe_op'


text‹Elementary properties.›

lemma (in is_cat_rKe) cat_rKe_exp_cat_cf_cat_FUNCT_is_arr:
  assumes "𝒵 β" and "α ∈∘ β"
  shows "exp_cat_cf α 𝔄 𝔎 : cat_FUNCT α ℭ 𝔄 ↦↦C.tiny⇘β⇙ cat_FUNCT α 𝔅 𝔄"
  by 
    ( 
      rule exp_cat_cf_is_tiny_functor[
        OF assms Ran.HomCod.category_axioms AG.is_functor_axioms
        ]
    )

lemma (in is_cat_lKe) cat_lKe_exp_cat_cf_cat_FUNCT_is_arr:
  assumes "𝒵 β" and "α ∈∘ β"
  shows "exp_cat_cf α 𝔄 𝔎 : cat_FUNCT α ℭ 𝔄 ↦↦C.tiny⇘β⇙ cat_FUNCT α 𝔅 𝔄"
  by 
    ( 
      rule exp_cat_cf_is_tiny_functor[
        OF assms Lan.HomCod.category_axioms AG.is_functor_axioms
        ]
    )


subsubsection‹Universal property›


text‹
See Chapter X-3 in cite‹"mac_lane_categories_2010"› and 
cite‹"noauthor_wikipedia_2001"›\footnote{
\url{https://en.wikipedia.org/wiki/Kan_extension}
}.
›

lemma is_cat_rKeI':
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and "𝔊 : ℭ ↦↦C⇘α⇙ 𝔄"
    and "ε : 𝔊 ∘CF 𝔎 ↦CF 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "⋀𝔊' ε'.
      ⟦ 𝔊' : ℭ ↦↦C⇘α⇙ 𝔄; ε' : 𝔊' ∘CF 𝔎 ↦CF 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄 ⟧ ⟹
        ∃!σ. σ : 𝔊' ↦CF 𝔊 : ℭ ↦↦C⇘α⇙ 𝔄 ∧ ε' = ε ∙NTCF (σ ∘NTCF-CF 𝔎)" 
  shows "ε : 𝔊 ∘CF 𝔎 ↦CF.rKe⇘α⇙ 𝔗 : 𝔅 ↦C ℭ ↦C 𝔄"
proof-
  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔊: is_functor α ℭ 𝔄 𝔊 by (rule assms(2))
  interpret ε: is_ntcf α 𝔅 𝔄 ‹𝔊 ∘CF 𝔎› 𝔗 ε by (rule assms(3))
  let ?𝔄𝔎 = ‹exp_cat_cf α 𝔄 𝔎›
    and ?𝔗 = ‹cf_map 𝔗›
    and ?𝔊 = ‹cf_map 𝔊›
  show ?thesis
  proof(intro is_cat_rKeI is_functor.universal_arrow_foI assms)
    define β where "β = α + ω"
    have "𝒵 β" and αβ: "α ∈∘ β" 
      by (simp_all add: β_def 𝔎.𝒵_Limit_αω 𝔎.𝒵_ω_αω 𝒵_def 𝔎.𝒵_α_αω)
    then interpret β: 𝒵 β by simp 
    show "?𝔄𝔎 : cat_FUNCT α ℭ 𝔄 ↦↦C⇘β⇙ cat_FUNCT α 𝔅 𝔄"
      by 
        ( 
          cs_concl cs_shallow cs_intro: 
            cat_small_cs_intros 
            exp_cat_cf_is_tiny_functor[
              OF β.𝒵_axioms αβ 𝔊.HomCod.category_axioms assms(1)
              ]
        )
    from αβ assms(2) show "cf_map 𝔊 ∈∘ cat_FUNCT α ℭ 𝔄⦇Obj⦈"
      unfolding cat_FUNCT_components
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_FUNCT_cs_intros)
    from assms(1-3) show "ntcf_arrow ε :
      ?𝔄𝔎⦇ObjMap⦈⦇?𝔊⦈ ↦⇘cat_FUNCT α 𝔅 𝔄⇙ ?𝔗"
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_Kan_cs_simps cat_FUNCT_cs_simps cat_FUNCT_components(1) 
            cs_intro: cat_FUNCT_cs_intros
        )
    fix 𝔉' ε' assume prems: 
      "𝔉' ∈∘ cat_FUNCT α ℭ 𝔄⦇Obj⦈"
      "ε' : ?𝔄𝔎⦇ObjMap⦈⦇𝔉'⦈ ↦⇘cat_FUNCT α 𝔅 𝔄⇙ ?𝔗"
    from prems(1) have "𝔉' ∈∘ cf_maps α ℭ 𝔄"  
      unfolding cat_FUNCT_components(1) by simp
    then obtain 𝔉 where 𝔉'_def: "𝔉' = cf_map 𝔉" and 𝔉: "𝔉 : ℭ ↦↦C⇘α⇙ 𝔄" 
      by clarsimp
    note ε' = cat_FUNCT_is_arrD[OF prems(2)]
    from ε'(1) 𝔉 have ε'_is_ntcf: 
      "ntcf_of_ntcf_arrow 𝔅 𝔄 ε' : 𝔉 ∘CF 𝔎 ↦CF 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
      by 
        ( 
          cs_prems  
            cs_simp: 𝔉'_def cat_Kan_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    from assms(4)[OF 𝔉 ε'_is_ntcf] obtain σ
      where σ: "σ : 𝔉 ↦CF 𝔊 : ℭ ↦↦C⇘α⇙ 𝔄" 
        and ε'_def': "ntcf_of_ntcf_arrow 𝔅 𝔄 ε' = ε ∙NTCF (σ ∘NTCF-CF 𝔎)"
        and unique_σ: "⋀σ'. 
          ⟦ 
            σ' : 𝔉 ↦CF 𝔊 : ℭ ↦↦C⇘α⇙ 𝔄;
            ntcf_of_ntcf_arrow 𝔅 𝔄 ε' = ε ∙NTCF (σ' ∘NTCF-CF 𝔎) 
          ⟧ ⟹ σ' = σ"
      by metis
    show "∃!f'.
      f' : 𝔉' ↦⇘cat_FUNCT α ℭ 𝔄⇙ ?𝔊 ∧
      ε' = umap_fo ?𝔄𝔎 ?𝔗 ?𝔊 (ntcf_arrow ε) 𝔉'⦇ArrVal⦈⦇f'⦈"
    proof(intro ex1I conjI; (elim conjE)?, unfold 𝔉'_def)
      from σ show "ntcf_arrow σ : cf_map 𝔉 ↦⇘cat_FUNCT α ℭ 𝔄⇙ ?𝔊"
        by (cs_concl cs_shallow cs_intro: cat_FUNCT_cs_intros)
      from αβ assms(1-3) σ ε'(1) show 
        "ε' = umap_fo ?𝔄𝔎 ?𝔗 ?𝔊 (ntcf_arrow ε) (cf_map 𝔉)⦇ArrVal⦈⦇ntcf_arrow σ⦈"
        by (subst ε')
          (
            cs_concl 
              cs_simp: 
                ε'_def'[symmetric] 
                cat_cs_simps 
                cat_FUNCT_cs_simps 
                cat_Kan_cs_simps 
              cs_intro: 
                cat_small_cs_intros 
                cat_cs_intros 
                cat_Kan_cs_intros
                cat_FUNCT_cs_intros
          )
      fix σ' assume prems:
        "σ' : cf_map 𝔉 ↦⇘cat_FUNCT α ℭ 𝔄⇙ ?𝔊"
        "ε' = umap_fo ?𝔄𝔎 ?𝔗 ?𝔊 (ntcf_arrow ε) (cf_map 𝔉)⦇ArrVal⦈⦇σ'⦈"
      note σ' = cat_FUNCT_is_arrD[OF prems(1)]
      from σ'(1) 𝔉 have "ntcf_of_ntcf_arrow ℭ 𝔄 σ' : 𝔉 ↦CF 𝔊 : ℭ ↦↦C⇘α⇙ 𝔄"
        by 
          (
            cs_prems cs_shallow 
              cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros
          )
      moreover from prems(2) prems(1) αβ assms(1-3) this ε'(1) have 
        "ntcf_of_ntcf_arrow 𝔅 𝔄 ε' =
          ε ∙NTCF (ntcf_of_ntcf_arrow ℭ 𝔄 σ' ∘NTCF-CF 𝔎)"
        by (subst (asm) ε'(2))
          (
            cs_prems 
              cs_simp: cat_Kan_cs_simps cat_FUNCT_cs_simps cat_cs_simps 
              cs_intro: 
                cat_Kan_cs_intros
                cat_small_cs_intros
                cat_cs_intros
                cat_FUNCT_cs_intros
          )
      ultimately have σ_def: "σ = ntcf_of_ntcf_arrow ℭ 𝔄 σ'" 
        by (rule unique_σ[symmetric])
      show "σ' = ntcf_arrow σ"
        by (subst σ'(2), use nothing in ‹subst σ_def›)
          (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed
  qed
qed

lemma is_cat_lKeI':
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and "𝔉 : ℭ ↦↦C⇘α⇙ 𝔄"
    and "η : 𝔗 ↦CF 𝔉 ∘CF 𝔎 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "⋀𝔉' η'.
      ⟦ 𝔉' : ℭ ↦↦C⇘α⇙ 𝔄; η' : 𝔗 ↦CF 𝔉' ∘CF 𝔎 : 𝔅 ↦↦C⇘α⇙ 𝔄 ⟧ ⟹
        ∃!σ. σ : 𝔉 ↦CF 𝔉' : ℭ ↦↦C⇘α⇙ 𝔄 ∧ η' = (σ ∘NTCF-CF 𝔎) ∙NTCF η" 
  shows "η : 𝔗 ↦CF.lKe⇘α⇙ 𝔉 ∘CF 𝔎 : 𝔅 ↦C ℭ ↦C 𝔄"
proof-
  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔉: is_functor α ℭ 𝔄 𝔉 by (rule assms(2))
  interpret η: is_ntcf α 𝔅 𝔄 𝔗 ‹𝔉 ∘CF 𝔎› η by (rule assms(3))
  have 
    "∃!σ.
      σ : 𝔊' ↦CF op_cf 𝔉 : op_cat ℭ ↦↦C⇘α⇙ op_cat 𝔄 ∧
      η' = op_ntcf η ∙NTCF (σ ∘NTCF-CF op_cf 𝔎)"
    if "𝔊' : op_cat ℭ ↦↦C⇘α⇙ op_cat 𝔄"
      and "η' : 𝔊' ∘CF op_cf 𝔎 ↦CF op_cf 𝔗 : op_cat 𝔅 ↦↦C⇘α⇙ op_cat 𝔄"
    for 𝔊' η'
  proof-
    interpret 𝔊': is_functor α ‹op_cat ℭ› ‹op_cat 𝔄› 𝔊' by (rule that(1))
    interpret η': 
      is_ntcf α ‹op_cat 𝔅› ‹op_cat 𝔄› ‹𝔊' ∘CF op_cf 𝔎› ‹op_cf 𝔗› η'
      by (rule that(2))
    from assms(4)[
        OF is_functor.is_functor_op[OF that(1), unfolded cat_op_simps],
        OF is_ntcf.is_ntcf_op[OF that(2), unfolded cat_op_simps]
        ]
    obtain σ where σ: "σ : 𝔉 ↦CF op_cf 𝔊' : ℭ ↦↦C⇘α⇙ 𝔄" 
      and op_η'_def: "op_ntcf η' = σ ∘NTCF-CF 𝔎 ∙NTCF η"
      and unique_σ':
        "⟦
          σ' : 𝔉 ↦CF op_cf 𝔊' : ℭ ↦↦C⇘α⇙ 𝔄;
          op_ntcf η' = σ' ∘NTCF-CF 𝔎 ∙NTCF η
         ⟧ ⟹ σ' = σ"
      for σ'
      by metis
    interpret σ: is_ntcf α ℭ 𝔄 𝔉 ‹op_cf 𝔊'› σ by (rule σ)
    show ?thesis
    proof(intro ex1I conjI; (elim conjE)?)
      show "op_ntcf σ : 𝔊' ↦CF op_cf 𝔉 : op_cat ℭ ↦↦C⇘α⇙ op_cat 𝔄"
        by (rule σ.is_ntcf_op[unfolded cat_op_simps])
      from op_η'_def have "op_ntcf (op_ntcf η') = op_ntcf (σ ∘NTCF-CF 𝔎 ∙NTCF η)"
        by simp
      from this σ assms(1-3) show η'_def:
        "η' = op_ntcf η ∙NTCF (op_ntcf σ ∘NTCF-CF op_cf 𝔎)"
        by (cs_prems cs_shallow cs_simp: cat_op_simps cs_intro: cat_cs_intros)
      fix σ' assume prems:
        "σ' : 𝔊' ↦CF op_cf 𝔉 : op_cat ℭ ↦↦C⇘α⇙ op_cat 𝔄"
        "η' = op_ntcf η ∙NTCF (σ' ∘NTCF-CF op_cf 𝔎)"
      interpret σ': is_ntcf α ‹op_cat ℭ› ‹op_cat 𝔄› 𝔊' ‹op_cf 𝔉› σ' 
        by (rule prems(1))
      from prems(2) have 
        "op_ntcf η' = op_ntcf (op_ntcf η ∙NTCF (σ' ∘NTCF-CF op_cf 𝔎))"
        by simp
      also have "… = op_ntcf σ' ∘NTCF-CF 𝔎 ∙NTCF η"   
        by
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_cs_intros cat_op_intros
          )
      finally have "op_ntcf η' = op_ntcf σ' ∘NTCF-CF 𝔎 ∙NTCF η" by simp
      from unique_σ'[OF σ'.is_ntcf_op[unfolded cat_op_simps] this] show 
        "σ' = op_ntcf σ" 
        by (auto simp: cat_op_simps)
    qed
  qed
  from 
    is_cat_rKeI'
      [
        OF 𝔎.is_functor_op 𝔉.is_functor_op η.is_ntcf_op[unfolded cat_op_simps], 
        unfolded cat_op_simps, 
        OF this
      ]
  interpret η: is_cat_rKe 
    α 
    ‹op_cat 𝔅› 
    ‹op_cat ℭ›
    ‹op_cat 𝔄› 
    ‹op_cf 𝔎› 
    ‹op_cf 𝔗› 
    ‹op_cf 𝔉› 
    ‹op_ntcf η›
    by simp
  show "η : 𝔗 ↦CF.lKe⇘α⇙ 𝔉 ∘CF 𝔎 : 𝔅 ↦C ℭ ↦C 𝔄"
    by (rule η.is_cat_lKe_op[unfolded cat_op_simps])
qed

lemma (in is_cat_rKe) cat_rKe_unique:
  assumes "𝔊' : ℭ ↦↦C⇘α⇙ 𝔄" and "ε' : 𝔊' ∘CF 𝔎 ↦CF 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
  shows "∃!σ. σ : 𝔊' ↦CF 𝔊 : ℭ ↦↦C⇘α⇙ 𝔄 ∧ ε' = ε ∙NTCF (σ ∘NTCF-CF 𝔎)" 
proof-

  interpret 𝔊': is_functor α ℭ 𝔄 𝔊' by (rule assms(1))
  interpret ε': is_ntcf α 𝔅 𝔄 ‹𝔊' ∘CF 𝔎› 𝔗 ε' by (rule assms(2))

  let ?𝔗 = ‹cf_map 𝔗›
    and ?𝔊 = ‹cf_map 𝔊›
    and ?𝔊' = ‹cf_map 𝔊'›
    and ?ε = ‹ntcf_arrow ε›
    and ?ε' = ‹ntcf_arrow ε'›

  define β where "β = α + ω"
  have "𝒵 β" and αβ: "α ∈∘ β"
    by (simp_all add: β_def AG.𝒵_Limit_αω AG.𝒵_ω_αω 𝒵_def AG.𝒵_α_αω)
  then interpret β: 𝒵 β by simp
  
  interpret 𝔄𝔎: is_tiny_functor 
    β ‹cat_FUNCT α ℭ 𝔄› ‹cat_FUNCT α 𝔅 𝔄› ‹exp_cat_cf α 𝔄 𝔎›
    by (rule cat_rKe_exp_cat_cf_cat_FUNCT_is_arr[OF β.𝒵_axioms αβ])

  from assms(1) have 𝔊': "?𝔊' ∈∘ cat_FUNCT α ℭ 𝔄⦇Obj⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_FUNCT_components(1) cs_intro: cat_FUNCT_cs_intros
      )
  with assms(2) have
    "?ε' : exp_cat_cf α 𝔄 𝔎⦇ObjMap⦈⦇?𝔊'⦈ ↦⇘cat_FUNCT α 𝔅 𝔄⇙ ?𝔗"
    by 
      ( 
        cs_concl cs_shallow 
          cs_simp: cat_Kan_cs_simps cat_FUNCT_cs_simps 
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros
      )

  from
    is_functor.universal_arrow_foD(3)[
      OF 𝔄𝔎.is_functor_axioms cat_rKe_ua_fo 𝔊' this
      ]
  obtain f' where f': "f' : cf_map 𝔊' ↦⇘cat_FUNCT α ℭ 𝔄⇙ cf_map 𝔊"
    and ε'_def: "?ε' = umap_fo (exp_cat_cf α 𝔄 𝔎) ?𝔗 ?𝔊 ?ε ?𝔊'⦇ArrVal⦈⦇f'⦈"
    and f'_unique: 
      "⟦ 
        f'' : ?𝔊' ↦⇘cat_FUNCT α ℭ 𝔄⇙ ?𝔊;
        ntcf_arrow ε' = umap_fo (exp_cat_cf α 𝔄 𝔎) ?𝔗 ?𝔊 ?ε ?𝔊'⦇ArrVal⦈⦇f''⦈ 
       ⟧ ⟹ f'' = f'"
    for f''
    by metis
  
  show ?thesis
  proof(intro ex1I conjI; (elim conjE)?)
    from ε'_def cat_FUNCT_is_arrD(1)[OF f'] show
      "ε' = ε ∙NTCF (ntcf_of_ntcf_arrow ℭ 𝔄 f' ∘NTCF-CF 𝔎)"
      by (subst (asm) cat_FUNCT_is_arrD(2)[OF f']) (*slow*)
        (
          cs_prems cs_shallow
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_Kan_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    from cat_FUNCT_is_arrD(1)[OF f'] show f'_is_arr:
      "ntcf_of_ntcf_arrow ℭ 𝔄 f' : 𝔊' ↦CF 𝔊 : ℭ ↦↦C⇘α⇙ 𝔄"
      by 
        (
          cs_prems cs_shallow 
            cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros
        )
    fix σ assume prems: 
      "σ : 𝔊' ↦CF 𝔊 : ℭ ↦↦C⇘α⇙ 𝔄" "ε' = ε ∙NTCF (σ ∘NTCF-CF 𝔎)"
    interpret σ: is_ntcf α ℭ 𝔄 𝔊' 𝔊 σ by (rule prems(1))
    from prems(1) have σ: 
      "ntcf_arrow σ : cf_map 𝔊' ↦⇘cat_FUNCT α ℭ 𝔄⇙ cf_map 𝔊"
      by (cs_concl cs_shallow cs_intro: cat_FUNCT_cs_intros)
    from prems have ε'_def: "ntcf_arrow ε' =
      umap_fo (exp_cat_cf α 𝔄 𝔎) ?𝔗 ?𝔊 ?ε ?𝔊'⦇ArrVal⦈⦇ntcf_arrow σ⦈"
      by 
        (
          cs_concl cs_shallow
            cs_simp: prems(2) cat_Kan_cs_simps cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    show "σ = ntcf_of_ntcf_arrow ℭ 𝔄 f'"
      unfolding f'_unique[OF σ ε'_def, symmetric]
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros
        )
  qed

qed

lemma (in is_cat_lKe) cat_lKe_unique:
  assumes "𝔉' : ℭ ↦↦C⇘α⇙ 𝔄" and "η' : 𝔗 ↦CF 𝔉' ∘CF 𝔎 : 𝔅 ↦↦C⇘α⇙ 𝔄"
  shows "∃!σ. σ : 𝔉 ↦CF 𝔉' : ℭ ↦↦C⇘α⇙ 𝔄 ∧ η' = (σ ∘NTCF-CF 𝔎) ∙NTCF η" 
proof-

  interpret 𝔉': is_functor α ℭ 𝔄 𝔉' by (rule assms(1))
  interpret η': is_ntcf α 𝔅 𝔄 𝔗 ‹𝔉' ∘CF 𝔎› η' by (rule assms(2))
  interpret η: is_cat_rKe 
    α ‹op_cat 𝔅› ‹op_cat ℭ› ‹op_cat 𝔄› ‹op_cf 𝔎› ‹op_cf 𝔗› ‹op_cf 𝔉› ‹op_ntcf η›
    by (rule is_cat_rKe_op)

  from η.cat_rKe_unique[OF 𝔉'.is_functor_op η'.is_ntcf_op[unfolded cat_op_simps]]
  obtain σ where σ: "σ : op_cf 𝔉' ↦CF op_cf 𝔉 : op_cat ℭ ↦↦C⇘α⇙ op_cat 𝔄"
    and η'_def: "op_ntcf η' = op_ntcf η ∙NTCF (σ ∘NTCF-CF op_cf 𝔎)"
    and unique_σ': "⋀σ'.
      ⟦
        σ' : op_cf 𝔉' ↦CF op_cf 𝔉 : op_cat ℭ ↦↦C⇘α⇙ op_cat 𝔄;
        op_ntcf η' = op_ntcf η ∙NTCF (σ' ∘NTCF-CF op_cf 𝔎) 
      ⟧ ⟹ σ' = σ"
    by metis

  interpret σ: is_ntcf α ‹op_cat ℭ› ‹op_cat 𝔄› ‹op_cf 𝔉'› ‹op_cf 𝔉› σ 
    by (rule σ)
  
  show ?thesis
  proof(intro ex1I conjI; (elim conjE)?)
    show "op_ntcf σ : 𝔉 ↦CF 𝔉' : ℭ ↦↦C⇘α⇙ 𝔄"
      by (rule σ.is_ntcf_op[unfolded cat_op_simps])
    have "η' = op_ntcf (op_ntcf η')" 
      by (cs_concl cs_shallow cs_simp: cat_op_simps)
    also from η'_def have "… = op_ntcf (op_ntcf η ∙NTCF (σ ∘NTCF-CF op_cf 𝔎))"
      by simp
    also have "… = op_ntcf σ ∘NTCF-CF 𝔎 ∙NTCF η"
      by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_cs_intros)
    finally show "η' = op_ntcf σ ∘NTCF-CF 𝔎 ∙NTCF η" by simp
    fix σ' assume prems: 
      "σ' : 𝔉 ↦CF 𝔉' : ℭ ↦↦C⇘α⇙ 𝔄"
      "η' = σ' ∘NTCF-CF 𝔎 ∙NTCF η"
    interpret σ': is_ntcf α ℭ 𝔄 𝔉 𝔉' σ' by (rule prems(1))
    from prems(2) have "op_ntcf η' = op_ntcf (σ' ∘NTCF-CF 𝔎 ∙NTCF η)"
      by simp
    also have "… = op_ntcf η ∙NTCF (op_ntcf σ' ∘NTCF-CF op_cf 𝔎)"
      by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_cs_intros)
    finally have "op_ntcf η' = op_ntcf η ∙NTCF (op_ntcf σ' ∘NTCF-CF op_cf 𝔎)"
      by simp
    from unique_σ'[OF σ'.is_ntcf_op this] show "σ' = op_ntcf σ"
      by (auto simp: cat_op_simps)
  qed

qed


subsubsection‹Further properties›

lemma (in is_cat_rKe) cat_rKe_ntcf_ua_fo_is_iso_ntcf_if_ge_Limit:
  assumes "𝒵 β" and "α ∈∘ β"
  shows 
    "ntcf_ua_fo β (exp_cat_cf α 𝔄 𝔎) (cf_map 𝔗) (cf_map 𝔊) (ntcf_arrow ε) :
      HomO.C⇘β⇙cat_FUNCT α ℭ 𝔄(-,cf_map 𝔊) ↦CF.iso
      HomO.C⇘β⇙cat_FUNCT α 𝔅 𝔄(-,cf_map 𝔗) ∘CF op_cf (exp_cat_cf α 𝔄 𝔎) :
      op_cat (cat_FUNCT α ℭ 𝔄) ↦↦C⇘β⇙ cat_Set β"
proof-
  interpret 𝔄_𝔎: 
    is_tiny_functor β ‹cat_FUNCT α ℭ 𝔄› ‹cat_FUNCT α 𝔅 𝔄› ‹exp_cat_cf α 𝔄 𝔎›
    by 
      (
        rule exp_cat_cf_is_tiny_functor[
          OF assms Ran.HomCod.category_axioms AG.is_functor_axioms
          ]
      )
  show ?thesis
    by 
      (
        rule is_functor.cf_ntcf_ua_fo_is_iso_ntcf[
          OF 𝔄_𝔎.is_functor_axioms cat_rKe_ua_fo
          ]
      )
qed

lemma (in is_cat_lKe) cat_lKe_ntcf_ua_fo_is_iso_ntcf_if_ge_Limit:
  assumes "𝒵 β" and "α ∈∘ β"
  defines "𝔄𝔎 ≡ exp_cat_cf α (op_cat 𝔄) (op_cf 𝔎)"
    and "𝔄ℭ ≡ cat_FUNCT α (op_cat ℭ) (op_cat 𝔄)"
    and "𝔄𝔅 ≡ cat_FUNCT α (op_cat 𝔅) (op_cat 𝔄)"
  shows 
    "ntcf_ua_fo β 𝔄𝔎 (cf_map 𝔗) (cf_map 𝔉) (ntcf_arrow (op_ntcf η)) :
      HomO.C⇘β⇙𝔄ℭ(-,cf_map 𝔉) ↦CF.iso HomO.C⇘β⇙𝔄𝔅(-,cf_map 𝔗) ∘CF op_cf 𝔄𝔎 :
      op_cat 𝔄ℭ ↦↦C⇘β⇙ cat_Set β"
proof-
  note simps = 𝔄ℭ_def 𝔄𝔅_def 𝔄𝔎_def
  interpret 𝔄_𝔎: is_tiny_functor β 𝔄ℭ 𝔄𝔅 𝔄𝔎
    unfolding simps
    by
      (
        rule exp_cat_cf_is_tiny_functor[
          OF assms(1,2) Lan.HomCod.category_op AG.is_functor_op
          ]
      )
  show ?thesis
    unfolding simps
    by 
      (
        rule is_functor.cf_ntcf_ua_fo_is_iso_ntcf[
          OF 𝔄_𝔎.is_functor_axioms[unfolded simps] cat_lKe_ua_fo
          ]
      )
qed



subsection‹Opposite universal arrow for Kan extensions›


subsubsection‹Definition and elementary properties›


text‹
The following definition is merely a convenience utility for 
the exposition of dual results associated with the formula for 
the right Kan extension and the pointwise right Kan extension.
›

definition op_ua :: "(V ⇒ V) ⇒ V ⇒ V ⇒ V"
  where "op_ua lim_Obj 𝔎 c =
    [
      lim_Obj c⦇UObj⦈,
      op_ntcf (lim_Obj c⦇UArr⦈) ∘NTCF-CF inv_cf (op_cf_obj_comma 𝔎 c)
    ]∘"


text‹Components.›

lemma op_ua_components:
  shows [cat_op_simps]: "op_ua lim_Obj 𝔎 c⦇UObj⦈ = lim_Obj c⦇UObj⦈"
    and "op_ua lim_Obj 𝔎 c⦇UArr⦈ =
      op_ntcf (lim_Obj c⦇UArr⦈) ∘NTCF-CF inv_cf (op_cf_obj_comma 𝔎 c)"
  unfolding op_ua_def ua_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Opposite universal arrow for Kan extensions is a limit›

lemma op_ua_UArr_is_cat_limit:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "c ∈∘ ℭ⦇Obj⦈"
    and "u : 𝔗 ∘CF 𝔎 CF⨅O c >CF.colim r : 𝔎 CF↓ c ↦↦C⇘α⇙ 𝔄"
  shows "op_ntcf u ∘NTCF-CF inv_cf (op_cf_obj_comma 𝔎 c) :
    r <CF.lim op_cf 𝔗 ∘CF c O⨅CF (op_cf 𝔎) : c ↓CF (op_cf 𝔎) ↦↦C⇘α⇙ op_cat 𝔄"
proof-

  note [cf_cs_simps] = is_iso_functor_is_iso_arr(2,3)

  let ?op_𝔎 = ‹λc. op_cf_obj_comma 𝔎 c›
  let ?op_𝔎c = ‹?op_𝔎 c›
    and ?op_ua_UArr = ‹op_ntcf u ∘NTCF-CF inv_cf (op_cf_obj_comma 𝔎 c)›

  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
  interpret u: is_cat_colimit α ‹𝔎 CF↓ c› 𝔄 ‹𝔗 ∘CF 𝔎 CF⨅O c› r u
    by (rule assms(4))

  from 𝔎.op_cf_cf_obj_comma_proj[OF assms(3)] have
    "op_cf (𝔎 CF⨅O c) ∘CF inv_cf (?op_𝔎 c) =
      c O⨅CF (op_cf 𝔎) ∘CF (?op_𝔎 c) ∘CF inv_cf (?op_𝔎 c)"
    by simp
  from this assms(3) have [cat_comma_cs_simps]:
    "op_cf (𝔎 CF⨅O c) ∘CF inv_cf (?op_𝔎 c) = c O⨅CF (op_cf 𝔎)"
    by
      (
        cs_prems 
          cs_simp: cat_cs_simps cat_comma_cs_simps cf_cs_simps cat_op_simps 
          cs_intro: cf_cs_intros cat_cs_intros cat_comma_cs_intros cat_op_intros
      )
  from assms(3) show "?op_ua_UArr :
    r <CF.lim op_cf 𝔗 ∘CF c O⨅CF (op_cf 𝔎) : c ↓CF (op_cf 𝔎) ↦↦C⇘α⇙ op_cat 𝔄"
    by
      (
        cs_concl
          cs_simp:
            cf_cs_simps cat_cs_simps cat_comma_cs_simps cat_op_simps 
            𝔎.op_cf_cf_obj_comma_proj[symmetric]
          cs_intro:
            cat_cs_intros
            cf_cs_intros
            cat_lim_cs_intros
            cat_comma_cs_intros
            cat_op_intros
      )

qed

context
  fixes lim_Obj :: "V ⇒ V" and c :: V
begin

lemmas op_ua_UArr_is_cat_limit' = op_ua_UArr_is_cat_limit
  [
    unfolded op_ua_components(2)[symmetric], 
    where u=‹lim_Obj c⦇UArr⦈› and r=‹lim_Obj c⦇UObj⦈› and c=c,
    folded op_ua_components(2)[where lim_Obj=lim_Obj and c=c]
  ]

end



subsection‹The Kan extension›


text‹
The following subsection is based on the statement and proof of 
Theorem 1 in Chapter X-3 in cite‹"mac_lane_categories_2010"›.
›


subsubsection‹Definition and elementary properties›

definition the_cf_rKe :: "V ⇒ V ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "the_cf_rKe α 𝔗 𝔎 lim_Obj =
    [
      (λc∈∘𝔎⦇HomCod⦈⦇Obj⦈. lim_Obj c⦇UObj⦈),
      (
        λg∈∘𝔎⦇HomCod⦈⦇Arr⦈. THE f.
          f :
            lim_Obj (𝔎⦇HomCod⦈⦇Dom⦈⦇g⦈)⦇UObj⦈ ↦⇘𝔗⦇HomCod⦈⇙
            lim_Obj (𝔎⦇HomCod⦈⦇Cod⦈⦇g⦈)⦇UObj⦈ ∧
          lim_Obj (𝔎⦇HomCod⦈⦇Dom⦈⦇g⦈)⦇UArr⦈ ∘NTCF-CF g A↓CF 𝔎 =
            lim_Obj (𝔎⦇HomCod⦈⦇Cod⦈⦇g⦈)⦇UArr⦈ ∙NTCF 
            ntcf_const ((𝔎⦇HomCod⦈⦇Cod⦈⦇g⦈) ↓CF 𝔎) (𝔗⦇HomCod⦈) f
      ),
      𝔎⦇HomCod⦈,
      𝔗⦇HomCod⦈
    ]∘"

definition the_ntcf_rKe :: "V ⇒ V ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "the_ntcf_rKe α 𝔗 𝔎 lim_Obj =
    [
      (
        λc∈∘𝔗⦇HomDom⦈⦇Obj⦈.
          lim_Obj (𝔎⦇ObjMap⦈⦇c⦈)⦇UArr⦈⦇NTMap⦈⦇0, c, 𝔎⦇HomCod⦈⦇CId⦈⦇𝔎⦇ObjMap⦈⦇c⦈⦈⦈∙
      ),
      the_cf_rKe α 𝔗 𝔎 lim_Obj ∘CF 𝔎,
      𝔗,
      𝔗⦇HomDom⦈,
      𝔗⦇HomCod⦈
    ]∘"

definition the_cf_lKe :: "V ⇒ V ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "the_cf_lKe α 𝔗 𝔎 lim_Obj =
    op_cf (the_cf_rKe α (op_cf 𝔗) (op_cf 𝔎) (op_ua lim_Obj 𝔎))"

definition the_ntcf_lKe :: "V ⇒ V ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "the_ntcf_lKe α 𝔗 𝔎 lim_Obj =
    op_ntcf (the_ntcf_rKe α (op_cf 𝔗) (op_cf 𝔎) (op_ua lim_Obj 𝔎))"


text‹Components.›

lemma the_cf_rKe_components:
  shows "the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ObjMap⦈ = 
    (λc∈∘𝔎⦇HomCod⦈⦇Obj⦈. lim_Obj c⦇UObj⦈)"
    and "the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈ =
    (
      λg∈∘𝔎⦇HomCod⦈⦇Arr⦈. THE f.
        f :
          lim_Obj (𝔎⦇HomCod⦈⦇Dom⦈⦇g⦈)⦇UObj⦈ ↦⇘𝔗⦇HomCod⦈⇙
          lim_Obj (𝔎⦇HomCod⦈⦇Cod⦈⦇g⦈)⦇UObj⦈ ∧
        lim_Obj (𝔎⦇HomCod⦈⦇Dom⦈⦇g⦈)⦇UArr⦈ ∘NTCF-CF g A↓CF 𝔎 =
          lim_Obj (𝔎⦇HomCod⦈⦇Cod⦈⦇g⦈)⦇UArr⦈ ∙NTCF 
          ntcf_const ((𝔎⦇HomCod⦈⦇Cod⦈⦇g⦈) ↓CF 𝔎) (𝔗⦇HomCod⦈) f
    )"
    and "the_cf_rKe α 𝔗 𝔎 lim_Obj⦇HomDom⦈ = 𝔎⦇HomCod⦈"
    and "the_cf_rKe α 𝔗 𝔎 lim_Obj⦇HomCod⦈ = 𝔗⦇HomCod⦈"
  unfolding the_cf_rKe_def dghm_field_simps by (simp_all add: nat_omega_simps)

lemma the_ntcf_rKe_components:
  shows "the_ntcf_rKe α 𝔗 𝔎 lim_Obj⦇NTMap⦈ =
      (
        λc∈∘𝔗⦇HomDom⦈⦇Obj⦈.
          lim_Obj (𝔎⦇ObjMap⦈⦇c⦈)⦇UArr⦈⦇NTMap⦈⦇0, c, 𝔎⦇HomCod⦈⦇CId⦈⦇𝔎⦇ObjMap⦈⦇c⦈⦈⦈∙
      )"
    and "the_ntcf_rKe α 𝔗 𝔎 lim_Obj⦇NTDom⦈ = the_cf_rKe α 𝔗 𝔎 lim_Obj ∘CF 𝔎"
    and "the_ntcf_rKe α 𝔗 𝔎 lim_Obj⦇NTCod⦈ = 𝔗"
    and "the_ntcf_rKe α 𝔗 𝔎 lim_Obj⦇NTDGDom⦈ = 𝔗⦇HomDom⦈"
    and "the_ntcf_rKe α 𝔗 𝔎 lim_Obj⦇NTDGCod⦈ = 𝔗⦇HomCod⦈"
  unfolding the_ntcf_rKe_def nt_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 𝔗)

lemmas the_cf_rKe_components' = the_cf_rKe_components[
    where 𝔎=𝔎 and 𝔗=𝔗 and α=α, unfolded 𝔎.cf_HomCod 𝔗.cf_HomCod
    ]

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

lemmas the_ntcf_rKe_components' = the_ntcf_rKe_components[
    where 𝔎=𝔎 and 𝔗=𝔗 and α=α, unfolded 𝔎.cf_HomCod 𝔗.cf_HomCod 𝔗.cf_HomDom
    ]

lemmas [cat_Kan_cs_simps] = the_ntcf_rKe_components'(2-5)

end


subsubsection‹Functor: object map›

mk_VLambda the_cf_rKe_components(1)
  |vsv the_cf_rKe_ObjMap_vsv[cat_Kan_cs_intros]|

context
  fixes α 𝔄 𝔅 ℭ 𝔎 𝔗
  assumes 𝔎: "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and 𝔗: "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
begin

interpretation 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule 𝔎)

mk_VLambda the_cf_rKe_components'(1)[OF 𝔎 𝔗]
  |vdomain the_cf_rKe_ObjMap_vdomain[cat_Kan_cs_simps]|
  |app the_cf_rKe_ObjMap_impl_app[cat_Kan_cs_simps]|

lemma the_cf_rKe_ObjMap_vrange: 
  assumes "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ lim_Obj c⦇UObj⦈ ∈∘ 𝔄⦇Obj⦈"
  shows "ℛ∘ (the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ObjMap⦈) ⊆∘ 𝔄⦇Obj⦈"
  unfolding the_cf_rKe_components'[OF 𝔎 𝔗]
  by (intro vrange_VLambda_vsubset assms)

end


subsubsection‹Functor: arrow map›

mk_VLambda the_cf_rKe_components(2)
  |vsv the_cf_rKe_ArrMap_vsv[cat_Kan_cs_intros]|

context
  fixes α 𝔅 ℭ 𝔎
  assumes 𝔎: "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
begin

interpretation 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule 𝔎)

mk_VLambda the_cf_rKe_components(2)[where α=α and 𝔎=𝔎, unfolded 𝔎.cf_HomCod]
  |vdomain the_cf_rKe_ArrMap_vdomain[cat_Kan_cs_simps]|

context 
  fixes 𝔄 𝔗 c c' g
  assumes 𝔗: "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and g: "g : c ↦⇘ℭ⇙ c'"
begin

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

lemma g': "g ∈∘ ℭ⦇Arr⦈" using g by auto

mk_VLambda the_cf_rKe_components(2)[
    where α=α and 𝔎=𝔎 and 𝔗=𝔗, unfolded 𝔎.cf_HomCod 𝔗.cf_HomCod
    ]
  |app the_cf_rKe_ArrMap_app_impl'|

lemmas the_cf_rKe_ArrMap_app' = the_cf_rKe_ArrMap_app_impl'[
    OF g', unfolded 𝔎.HomCod.cat_is_arrD[OF g]
    ]

end

end

lemma the_cf_rKe_ArrMap_app_impl:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "g : c ↦⇘ℭ⇙ c'"
    and "u : r <CF.lim 𝔗 ∘CF c O⨅CF 𝔎 : c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
    and "u' : r' <CF.lim 𝔗 ∘CF c' O⨅CF 𝔎 : c' ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
  shows "∃!f.
    f : r ↦⇘𝔄⇙ r' ∧
    u ∘NTCF-CF g A↓CF 𝔎 = u' ∙NTCF ntcf_const (c' ↓CF 𝔎) 𝔄 f"
proof-

  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
  interpret u: is_cat_limit α ‹c ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF c O⨅CF 𝔎› r u
    by (rule assms(4))
  interpret u': is_cat_limit α ‹c' ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF c' O⨅CF 𝔎› r' u'
    by (rule assms(5))

  have const_r_def:
    "cf_const (c' ↓CF 𝔎) 𝔄 r = cf_const (c ↓CF 𝔎) 𝔄 r ∘CF g A↓CF 𝔎"
  proof(rule cf_eqI)
    show const_r: "cf_const (c' ↓CF 𝔎) 𝔄 r : c' ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
      by (cs_concl cs_intro: cat_cs_intros cat_lim_cs_intros)
    from assms(3) show const_r_g𝔎: 
      "cf_const (c ↓CF 𝔎) 𝔄 r ∘CF g A↓CF 𝔎 : c' ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
      by (cs_concl cs_intro: cat_cs_intros cat_comma_cs_intros)
    have ObjMap_dom_lhs: "𝒟∘ (cf_const (c' ↓CF 𝔎) 𝔄 r⦇ObjMap⦈) = c' ↓CF 𝔎⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms(3) have ObjMap_dom_rhs: 
      "𝒟∘ ((cf_const (c ↓CF 𝔎) 𝔄 r ∘CF g A↓CF 𝔎)⦇ObjMap⦈) = c' ↓CF 𝔎⦇Obj⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
        )
    have ArrMap_dom_lhs: "𝒟∘ (cf_const (c' ↓CF 𝔎) 𝔄 r⦇ArrMap⦈) = c' ↓CF 𝔎⦇Arr⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms(3) have ArrMap_dom_rhs: 
      "𝒟∘ ((cf_const (c ↓CF 𝔎) 𝔄 r ∘CF g A↓CF 𝔎)⦇ArrMap⦈) = c' ↓CF 𝔎⦇Arr⦈"
      by
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
        )
    show 
      "cf_const (c' ↓CF 𝔎) 𝔄 r⦇ObjMap⦈ =
        (cf_const (c ↓CF 𝔎) 𝔄 r ∘CF g A↓CF 𝔎)⦇ObjMap⦈"
    proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
      fix A assume prems: "A ∈∘ c' ↓CF 𝔎⦇Obj⦈"
      from prems assms obtain b f 
        where A_def: "A = [0, b, f]∘"
          and b: "b ∈∘ 𝔅⦇Obj⦈" 
          and f: "f : c' ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
        by auto
      from assms(1,3) prems f b show 
        "cf_const (c' ↓CF 𝔎) 𝔄 r⦇ObjMap⦈⦇A⦈ =
          (cf_const (c ↓CF 𝔎) 𝔄 r ∘CF g A↓CF 𝔎)⦇ObjMap⦈⦇A⦈"
        unfolding A_def
        by
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_comma_cs_simps 
              cs_intro: cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
          )
    qed 
      (
        use assms(3) in 
          ‹cs_concl cs_shallow cs_intro: cat_cs_intros cat_comma_cs_intros›
      )+
    show
      "cf_const (c' ↓CF 𝔎) 𝔄 r⦇ArrMap⦈ =
        (cf_const (c ↓CF 𝔎) 𝔄 r ∘CF g A↓CF 𝔎)⦇ArrMap⦈"
    proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      show "vsv (cf_const (c' ↓CF 𝔎) 𝔄 r⦇ArrMap⦈)"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      from assms(3) show "vsv ((cf_const (c ↓CF 𝔎) 𝔄 r ∘CF g A↓CF 𝔎)⦇ArrMap⦈)"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_comma_cs_intros)
      fix F assume prems: "F ∈∘ c' ↓CF 𝔎⦇Arr⦈"
      with prems obtain A B where F: "F : A ↦⇘c' ↓CF 𝔎⇙ B"
        by (auto intro: is_arrI)
      with assms obtain b f b' f' h'
        where F_def: "F = [[0, b, f]∘, [0, b', f']∘, [0, h']∘]∘"
          and A_def: "A = [0, b, f]∘"
          and B_def: "B = [0, b', f']∘"
          and h': "h' : b ↦⇘𝔅⇙ b'"
          and f: "f : c' ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
          and f': "f' : c' ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
          and f'_def: "𝔎⦇ArrMap⦈⦇h'⦈ ∘A⇘ℭ⇙ f = f'"
        by auto
      from prems assms(3) F g' h' f f' show
        "cf_const (c' ↓CF 𝔎) 𝔄 r⦇ArrMap⦈⦇F⦈ =
          (cf_const (c ↓CF 𝔎) 𝔄 r ∘CF g A↓CF 𝔎)⦇ArrMap⦈⦇F⦈"
        unfolding F_def A_def B_def
        by (*slow*)
          (
            cs_concl 
              cs_simp: cat_comma_cs_simps cat_cs_simps f'_def[symmetric]
              cs_intro: cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
          )
    qed simp
  qed simp_all

  have 𝔗c'𝔎: "𝔗 ∘CF c' O⨅CF 𝔎 = 𝔗 ∘CF c O⨅CF 𝔎 ∘CF g A↓CF 𝔎"
  proof(rule cf_eqI)
    show "𝔗 ∘CF c' O⨅CF 𝔎 : c' ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    from assms show " 𝔗 ∘CF c O⨅CF 𝔎 ∘CF g A↓CF 𝔎 : c' ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
      by
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_comma_cs_intros cat_cs_intros
        )
    have ObjMap_dom_lhs: "𝒟∘ ((𝔗 ∘CF c' O⨅CF 𝔎)⦇ObjMap⦈) = c' ↓CF 𝔎⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms have ObjMap_dom_rhs: 
      "𝒟∘ ((𝔗 ∘CF c O⨅CF 𝔎 ∘CF g A↓CF 𝔎)⦇ObjMap⦈) = c' ↓CF 𝔎⦇Obj⦈"
      by
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_comma_cs_intros cat_cs_intros
        )
    show "(𝔗 ∘CF c' O⨅CF 𝔎)⦇ObjMap⦈ = (𝔗 ∘CF c O⨅CF 𝔎 ∘CF g A↓CF 𝔎)⦇ObjMap⦈"
    proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
      from assms show "vsv ((𝔗 ∘CF c' O⨅CF 𝔎)⦇ObjMap⦈)"
        by
          (
            cs_concl cs_shallow
              cs_simp: cat_comma_cs_simps 
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
      from assms show "vsv ((𝔗 ∘CF c O⨅CF 𝔎 ∘CF g A↓CF 𝔎)⦇ObjMap⦈)"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_comma_cs_intros)
      fix A assume prems: "A ∈∘ c' ↓CF 𝔎⦇Obj⦈"
      from assms(3) prems obtain b f
        where A_def: "A = [0, b, f]∘"
          and b: "b ∈∘ 𝔅⦇Obj⦈"
          and f: "f : c' ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
        by auto
      from prems assms b f show 
        "(𝔗 ∘CF c' O⨅CF 𝔎)⦇ObjMap⦈⦇A⦈ =
          (𝔗 ∘CF c O⨅CF 𝔎 ∘CF g A↓CF 𝔎)⦇ObjMap⦈⦇A⦈"
        unfolding A_def
        by
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_comma_cs_simps
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
    qed simp

    have ArrMap_dom_lhs: "𝒟∘ ((𝔗 ∘CF c' O⨅CF 𝔎)⦇ArrMap⦈) = c' ↓CF 𝔎⦇Arr⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms have ArrMap_dom_rhs:
      "𝒟∘ ((𝔗 ∘CF c O⨅CF 𝔎 ∘CF g A↓CF 𝔎)⦇ArrMap⦈) = c' ↓CF 𝔎⦇Arr⦈"
      by
        (
          cs_concl 
            cs_simp: cat_cs_simps
            cs_intro: cat_comma_cs_intros cat_cs_intros
        )

    show "(𝔗 ∘CF c' O⨅CF 𝔎)⦇ArrMap⦈ = (𝔗 ∘CF c O⨅CF 𝔎 ∘CF g A↓CF 𝔎)⦇ArrMap⦈"
    proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      from assms show "vsv ((𝔗 ∘CF c' O⨅CF 𝔎)⦇ArrMap⦈)"
        by
          (
            cs_concl cs_shallow
              cs_simp: cat_comma_cs_simps 
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
      from assms show "vsv ((𝔗 ∘CF c O⨅CF 𝔎 ∘CF g A↓CF 𝔎)⦇ArrMap⦈)"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cs_intro: cat_cs_intros cat_comma_cs_intros
          )

      fix F assume prems: "F ∈∘ c' ↓CF 𝔎⦇Arr⦈"
      with prems obtain A B where F: "F : A ↦⇘c' ↓CF 𝔎⇙ B"
        unfolding cat_comma_cs_simps by (auto intro: is_arrI)
      with assms(3) obtain b f b' f' h'
        where F_def: "F = [[0, b, f]∘, [0, b', f']∘, [0, h']∘]∘"
          and A_def: "A = [0, b, f]∘"
          and B_def: "B = [0, b', f']∘"
          and h': "h' : b ↦⇘𝔅⇙ b'"
          and f: "f : c' ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
          and f': "f' : c' ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
          and f'_def: "𝔎⦇ArrMap⦈⦇h'⦈ ∘A⇘ℭ⇙ f = f'"
        by auto
      from prems assms(3) F g' h' f f' show
        "(𝔗 ∘CF c' O⨅CF 𝔎)⦇ArrMap⦈⦇F⦈ =
          (𝔗 ∘CF c O⨅CF 𝔎 ∘CF g A↓CF 𝔎)⦇ArrMap⦈⦇F⦈"
        unfolding F_def A_def B_def
        by (*slow*)
          (
            cs_concl 
              cs_simp: cat_comma_cs_simps cat_cs_simps f'_def[symmetric]
              cs_intro: cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
          )
    qed simp
  qed simp_all

  from assms(1-3) have
    "u ∘NTCF-CF g A↓CF 𝔎 : r <CF.cone 𝔗 ∘CF c' O⨅CF 𝔎 : c' ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
    by (intro is_cat_coneI)
      (
        cs_concl 
          cs_intro: cat_cs_intros cat_comma_cs_intros cat_lim_cs_intros
          cs_simp: const_r_def 𝔗c'𝔎
      )+
  with u'.cat_lim_ua_fo show
    "∃!G.
      G : r ↦⇘𝔄⇙ r' ∧
      u ∘NTCF-CF g A↓CF 𝔎 = u' ∙NTCF ntcf_const (c' ↓CF 𝔎) 𝔄 G"
    by simp

qed

lemma the_cf_rKe_ArrMap_app:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "g : c ↦⇘ℭ⇙ c'"
    and "lim_Obj c⦇UArr⦈ :
      lim_Obj c⦇UObj⦈ <CF.lim 𝔗 ∘CF c O⨅CF 𝔎 : c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
    and "lim_Obj c'⦇UArr⦈ :
      lim_Obj c'⦇UObj⦈ <CF.lim 𝔗 ∘CF c' O⨅CF 𝔎 : c' ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
  shows "the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇g⦈ :
    lim_Obj c⦇UObj⦈ ↦⇘𝔄⇙ lim_Obj c'⦇UObj⦈"
    and
      "lim_Obj c⦇UArr⦈ ∘NTCF-CF g A↓CF 𝔎 =
        lim_Obj c'⦇UArr⦈ ∙NTCF
          ntcf_const (c' ↓CF 𝔎) 𝔄 (the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇g⦈)"
    and 
      "⟦
        f : lim_Obj c⦇UObj⦈ ↦⇘𝔄⇙ lim_Obj c'⦇UObj⦈;
        lim_Obj c⦇UArr⦈ ∘NTCF-CF g A↓CF 𝔎 =
          lim_Obj c'⦇UArr⦈ ∙NTCF ntcf_const (c' ↓CF 𝔎) 𝔄 f
       ⟧ ⟹ f = the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇g⦈"
proof-

  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
  interpret u: is_cat_limit 
    α ‹c ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF c O⨅CF 𝔎› ‹lim_Obj c⦇UObj⦈› ‹lim_Obj c⦇UArr⦈›
    by (rule assms(4))
  interpret u': is_cat_limit 
    α ‹c' ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF c' O⨅CF 𝔎› ‹lim_Obj c'⦇UObj⦈› ‹lim_Obj c'⦇UArr⦈›
    by (rule assms(5))

  from assms(3) have c: "c ∈∘ ℭ⦇Obj⦈" and c': "c' ∈∘ ℭ⦇Obj⦈" by auto

  note the_cf_rKe_ArrMap_app_impl' =
    the_cf_rKe_ArrMap_app_impl[OF assms]
  note the_f = theI'[OF the_cf_rKe_ArrMap_app_impl[OF assms]]
  note the_f_is_arr = the_f[THEN conjunct1]
    and the_f_commutes = the_f[THEN conjunct2]

  from assms(3) the_f_is_arr show
    "the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇g⦈ :
      lim_Obj c⦇UObj⦈ ↦⇘𝔄⇙ lim_Obj c'⦇UObj⦈"
    by
      (
        cs_concl cs_shallow
          cs_simp: the_cf_rKe_ArrMap_app' cs_intro: cat_cs_intros
      )
  moreover from assms(3) the_f_commutes show
    "lim_Obj c⦇UArr⦈ ∘NTCF-CF g A↓CF 𝔎 =
      lim_Obj c'⦇UArr⦈ ∙NTCF
        ntcf_const (c' ↓CF 𝔎) 𝔄 (the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇g⦈)"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: the_cf_rKe_ArrMap_app' cs_intro: cat_cs_intros
      )
  ultimately show "f = the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇g⦈"
    if "f : lim_Obj c⦇UObj⦈ ↦⇘𝔄⇙ lim_Obj c'⦇UObj⦈"
      and "lim_Obj c⦇UArr⦈ ∘NTCF-CF g A↓CF 𝔎 =
        lim_Obj c'⦇UArr⦈ ∙NTCF ntcf_const (c' ↓CF 𝔎) 𝔄 f"
    by (metis that the_cf_rKe_ArrMap_app_impl')

qed

lemma the_cf_rKe_ArrMap_is_arr'[cat_Kan_cs_intros]:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "g : c ↦⇘ℭ⇙ c'"
    and "lim_Obj c⦇UArr⦈ :
      lim_Obj c⦇UObj⦈ <CF.lim 𝔗 ∘CF c O⨅CF 𝔎 : c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
    and "lim_Obj c'⦇UArr⦈ :
      lim_Obj c'⦇UObj⦈ <CF.lim 𝔗 ∘CF c' O⨅CF 𝔎 : c' ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
    and "a = lim_Obj c⦇UObj⦈"
    and "b = lim_Obj c'⦇UObj⦈"
  shows "the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇g⦈ : a ↦⇘𝔄⇙ b"
  unfolding assms(6,7) by (rule the_cf_rKe_ArrMap_app[OF assms(1-5)])

lemma lim_Obj_the_cf_rKe_commute:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "lim_Obj a⦇UArr⦈ :
      lim_Obj a⦇UObj⦈ <CF.lim 𝔗 ∘CF a O⨅CF 𝔎 : a ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
    and "lim_Obj b⦇UArr⦈ :
      lim_Obj b⦇UObj⦈ <CF.lim 𝔗 ∘CF b O⨅CF 𝔎 : b ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
    and "f : a ↦⇘ℭ⇙ b"
    and "[a', b', f']∘ ∈∘ b ↓CF 𝔎⦇Obj⦈"
  shows  
    "lim_Obj a⦇UArr⦈⦇NTMap⦈⦇a', b', f' ∘A⇘ℭ⇙ f⦈∙ =
      lim_Obj b⦇UArr⦈⦇NTMap⦈⦇a', b', f'⦈∙ ∘A⇘𝔄⇙
        the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇f⦈" 
proof-

  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))

  note f = 𝔎.HomCod.cat_is_arrD[OF assms(5)]

  interpret lim_a: is_cat_limit
    α ‹a ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF a O⨅CF 𝔎› ‹lim_Obj a⦇UObj⦈› ‹lim_Obj a⦇UArr⦈›
    by (rule assms(3))
  interpret lim_b: is_cat_limit 
    α ‹b ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF b O⨅CF 𝔎› ‹lim_Obj b⦇UObj⦈› ‹lim_Obj b⦇UArr⦈› 
    by (rule assms(4))

  note f_app = the_cf_rKe_ArrMap_app[
      where lim_Obj=lim_Obj, OF assms(1,2,5,3,4)
      ]

  from f_app(2) have lim_a_f𝔎_NTMap_app:
    "(lim_Obj a⦇UArr⦈ ∘NTCF-CF f A↓CF 𝔎)⦇NTMap⦈⦇A⦈ =
      (
        lim_Obj b⦇UArr⦈ ∙NTCF
        ntcf_const (b ↓CF 𝔎) 𝔄 (the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇f⦈)
      )⦇NTMap⦈⦇A⦈"
    if ‹A ∈∘ b ↓CF 𝔎⦇Obj⦈› for A
    by simp
  show 
    "lim_Obj a⦇UArr⦈⦇NTMap⦈⦇a', b', f' ∘A⇘ℭ⇙ f⦈∙ =
      lim_Obj b⦇UArr⦈⦇NTMap⦈⦇a', b', f'⦈∙ ∘A⇘𝔄⇙
        the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇f⦈" 
  proof-
    from assms(5,6) have a'_def: "a' = 0"
      and b': "b' ∈∘ 𝔅⦇Obj⦈"
      and f': "f' : b ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
      by auto
    show 
      "lim_Obj a⦇UArr⦈⦇NTMap⦈⦇a', b', f' ∘A⇘ℭ⇙ f⦈∙ =
        lim_Obj b⦇UArr⦈⦇NTMap⦈⦇a', b', f'⦈∙ ∘A⇘𝔄⇙
          the_cf_rKe α 𝔗 𝔎 lim_Obj⦇ArrMap⦈⦇f⦈"
      using lim_a_f𝔎_NTMap_app[OF assms(6)] f' assms(3-6) 
      unfolding a'_def
      by
        (
          cs_prems 
            cs_simp: cat_cs_simps cat_comma_cs_simps cat_Kan_cs_simps
            cs_intro: cat_cs_intros cat_comma_cs_intros cat_Kan_cs_intros
        )      
  qed

qed


subsubsection‹Natural transformation: natural transformation map›

mk_VLambda the_ntcf_rKe_components(1)
  |vsv the_ntcf_rKe_NTMap_vsv[cat_Kan_cs_intros]|

context
  fixes α 𝔄 𝔅 ℭ 𝔎 𝔗
  assumes 𝔎: "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and 𝔗: "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
begin

interpretation 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule 𝔎)
interpretation 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule 𝔗)

mk_VLambda the_ntcf_rKe_components'(1)[OF 𝔎 𝔗]
  |vdomain the_ntcf_rKe_ObjMap_vdomain[cat_Kan_cs_simps]|
  |app the_ntcf_rKe_ObjMap_impl_app[cat_Kan_cs_simps]|

end


subsubsection‹The Kan extension is a Kan extension›

lemma the_cf_rKe_is_functor:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ lim_Obj c⦇UArr⦈ :
      lim_Obj c⦇UObj⦈ <CF.lim 𝔗 ∘CF c O⨅CF 𝔎 : c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
  shows "the_cf_rKe α 𝔗 𝔎 lim_Obj : ℭ ↦↦C⇘α⇙ 𝔄"
proof-

  let ?UObj = ‹λa. lim_Obj a⦇UObj⦈› 
  let ?UArr = ‹λa. lim_Obj a⦇UArr⦈›
  let ?const_comma = ‹λa b. cf_const (a ↓CF 𝔎) 𝔄 (?UObj b)›
  let ?the_cf_rKe = ‹the_cf_rKe α 𝔗 𝔎 lim_Obj›

  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))

  note [cat_lim_cs_intros] = is_cat_cone.cat_cone_obj
  
  show ?thesis
  proof(intro is_functorI')

    show "vfsequence ?the_cf_rKe" unfolding the_cf_rKe_def by simp
    show "vcard ?the_cf_rKe = 4ℕ" 
      unfolding the_cf_rKe_def by (simp add: nat_omega_simps)
    show "vsv (?the_cf_rKe⦇ObjMap⦈)" 
      by (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
    moreover show "𝒟∘ (?the_cf_rKe⦇ObjMap⦈) = ℭ⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros)
    moreover show "ℛ∘ (?the_cf_rKe⦇ObjMap⦈) ⊆∘ 𝔄⦇Obj⦈"
    proof
      (
        intro the_cf_rKe_ObjMap_vrange; 
        (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)?
      )
      fix c assume "c ∈∘ ℭ⦇Obj⦈"
      with assms(3)[OF this] show "?UObj c ∈∘ 𝔄⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_lim_cs_intros)
    qed
    ultimately have [cat_Kan_cs_intros]: 
      "?the_cf_rKe⦇ObjMap⦈⦇c⦈ ∈∘ 𝔄⦇Obj⦈" if ‹c ∈∘ ℭ⦇Obj⦈› for c
      by (metis that vsubsetE vsv.vsv_value)

    show "?the_cf_rKe⦇ArrMap⦈⦇f⦈ :
      ?the_cf_rKe⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ ?the_cf_rKe⦇ObjMap⦈⦇b⦈"
      if "f : a ↦⇘ℭ⇙ b" for a b f
      using assms(2) that
      by 
        (
          cs_concl 
            cs_simp: cat_Kan_cs_simps 
            cs_intro: assms(3) cat_cs_intros cat_Kan_cs_intros
        )
    then have [cat_Kan_cs_intros]: "?the_cf_rKe⦇ArrMap⦈⦇f⦈ : A ↦⇘𝔄⇙ B"
      if "A = ?the_cf_rKe⦇ObjMap⦈⦇a⦈" 
        and "B = ?the_cf_rKe⦇ObjMap⦈⦇b⦈"
        and "f : a ↦⇘ℭ⇙ b" 
      for A B a b f
      by (simp add: that)

    show
      "?the_cf_rKe⦇ArrMap⦈⦇g ∘A⇘ℭ⇙ f⦈ =
        ?the_cf_rKe⦇ArrMap⦈⦇g⦈ ∘A⇘𝔄⇙ ?the_cf_rKe⦇ArrMap⦈⦇f⦈"
      (is ‹?the_cf_rKe⦇ArrMap⦈⦇g ∘A⇘ℭ⇙ f⦈ = ?the_rKe_g ∘A⇘𝔄⇙ ?the_rKe_f›)
      if g_is_arr: "g : b ↦⇘ℭ⇙ c" and f_is_arr: "f : a ↦⇘ℭ⇙ b" for b c g a f
    proof-

      let ?ntcf_const_c = ‹λf. ntcf_const (c ↓CF 𝔎) 𝔄 f›

      note g = 𝔎.HomCod.cat_is_arrD[OF that(1)]
        and f = 𝔎.HomCod.cat_is_arrD[OF that(2)]
      note lim_a = assms(3)[OF f(2)]
        and lim_b = assms(3)[OF g(2)]
        and lim_c = assms(3)[OF g(3)]
      from that have gf: "g ∘A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c" 
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)

      interpret lim_a: is_cat_limit
        α ‹a ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF a O⨅CF 𝔎› ‹?UObj a› ‹?UArr a›
        by (rule lim_a)
      interpret lim_c: is_cat_limit
        α ‹c ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF c O⨅CF 𝔎› ‹?UObj c› ‹?UArr c›
        by (rule lim_c)

      show ?thesis
      proof
        (
          rule sym, 
          rule the_cf_rKe_ArrMap_app(3)[OF assms(1,2) gf lim_a lim_c]
        )

        from assms(1,2) that lim_a lim_b lim_c show 
          "?the_rKe_g ∘A⇘𝔄⇙ ?the_rKe_f : ?UObj a ↦⇘𝔄⇙ ?UObj c"
          by
            (
              cs_concl 
                cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
            )
      
        show
          "?UArr a ∘NTCF-CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎 = 
            ?UArr c ∙NTCF ?ntcf_const_c (?the_rKe_g ∘A⇘𝔄⇙ ?the_rKe_f)"
          (
            is 
              ‹
                ?UArr a ∘NTCF-CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎 =
                  ?UArr c ∙NTCF ?ntcf_const_c ?the_rKe_gf
              ›
           )
        proof(rule ntcf_eqI)
          from that show 
            "?UArr a ∘NTCF-CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎 :
              cf_const (a ↓CF 𝔎) 𝔄 (?UObj a) ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎 ↦CF
              𝔗 ∘CF a O⨅CF 𝔎 ∘CF ((g ∘A⇘ℭ⇙ f) A↓CF 𝔎) :
              c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
            by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_comma_cs_intros)
          have [cat_comma_cs_simps]: 
            "?const_comma a a ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎 = ?const_comma c a"
          proof(rule cf_eqI)
            from g_is_arr f_is_arr show
              "?const_comma a a ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎 : c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
              by
                (
                  cs_concl  
                    cs_simp: cat_comma_cs_simps cat_cs_simps
                    cs_intro: 
                      cat_cs_intros cat_lim_cs_intros cat_comma_cs_intros
                )
            from g_is_arr f_is_arr show "?const_comma c a : c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
              by
                (
                  cs_concl 
                    cs_simp: cat_comma_cs_simps cat_cs_simps
                    cs_intro: 
                      cat_cs_intros cat_lim_cs_intros cat_comma_cs_intros
                )
            from g_is_arr f_is_arr have ObjMap_dom_lhs:
              "𝒟∘ ((?const_comma a a ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇ObjMap⦈) =
                c ↓CF 𝔎⦇Obj⦈"
              by
                (
                  cs_concl 
                    cs_simp: cat_comma_cs_simps cat_cs_simps 
                    cs_intro: 
                      cat_comma_cs_intros cat_lim_cs_intros cat_cs_intros
                )
            from g_is_arr f_is_arr have ObjMap_dom_rhs:
              "𝒟∘ (?const_comma c a⦇ObjMap⦈) = c ↓CF 𝔎⦇Obj⦈"
              by (cs_concl cs_shallow cs_simp: cat_comma_cs_simps cat_cs_simps)

            show
              "(?const_comma a a ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇ObjMap⦈ =
                ?const_comma c a⦇ObjMap⦈"
            proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
              from f_is_arr g_is_arr show 
                "vsv ((?const_comma a a ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇ObjMap⦈)"
                by
                  (
                    cs_concl
                      cs_simp: cat_comma_cs_simps cat_cs_simps 
                      cs_intro:
                        cat_cs_intros cat_lim_cs_intros cat_comma_cs_intros
                  )
              fix A assume prems: "A ∈∘ c ↓CF 𝔎⦇Obj⦈"
              with g_is_arr obtain b' f' 
                where A_def: "A = [0, b', f']∘"
                  and b': "b' ∈∘ 𝔅⦇Obj⦈"
                  and f': "f' : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
                by auto
              from prems b' f' g_is_arr f_is_arr show 
                "(?const_comma a a ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇ObjMap⦈⦇A⦈ =
                  ?const_comma c a⦇ObjMap⦈⦇A⦈"
                unfolding A_def
                by
                  (
                    cs_concl
                      cs_simp: cat_comma_cs_simps cat_cs_simps 
                      cs_intro:
                        cat_cs_intros cat_lim_cs_intros cat_comma_cs_intros
                  )
            qed (cs_concl cs_shallow cs_intro: cat_cs_intros)

            from g_is_arr f_is_arr have ArrMap_dom_lhs:
              "𝒟∘ ((?const_comma a a ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇ArrMap⦈) = 
                c ↓CF 𝔎⦇Arr⦈"
              by
                (
                  cs_concl 
                    cs_simp: cat_comma_cs_simps cat_cs_simps 
                    cs_intro: 
                      cat_comma_cs_intros cat_lim_cs_intros cat_cs_intros
                )
            from g_is_arr f_is_arr have ArrMap_dom_rhs:
              "𝒟∘ (?const_comma c a⦇ArrMap⦈) = c ↓CF 𝔎⦇Arr⦈"
              by (cs_concl cs_shallow cs_simp: cat_comma_cs_simps cat_cs_simps)

            show 
              "(?const_comma a a ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇ArrMap⦈ =
                ?const_comma c a⦇ArrMap⦈"
            proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
              from f_is_arr g_is_arr show
                "vsv ((?const_comma a a ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇ArrMap⦈)"
                by
                  (
                    cs_concl
                      cs_simp: cat_comma_cs_simps cat_cs_simps
                      cs_intro:
                        cat_cs_intros cat_lim_cs_intros cat_comma_cs_intros
                  )
              fix F assume "F ∈∘ c ↓CF 𝔎⦇Arr⦈"
              then obtain A B where F: "F : A ↦⇘c ↓CF 𝔎⇙ B"
                unfolding cat_comma_cs_simps by (auto intro: is_arrI)
              with g_is_arr obtain b' f' b'' f'' h'
                where F_def: "F = [[0, b', f']∘, [0, b'', f'']∘, [0, h']∘]∘"
                  and A_def: "A = [0, b', f']∘"
                  and B_def: "B = [0, b'', f'']∘"
                  and h': "h' : b' ↦⇘𝔅⇙ b''"
                  and f': "f' : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
                  and f'': "f'' : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b''⦈"
                  and f''_def: "𝔎⦇ArrMap⦈⦇h'⦈ ∘A⇘ℭ⇙ f' = f''"
                by auto
              from F f_is_arr g_is_arr g' h' f' f'' show 
                "(?const_comma a a ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇ArrMap⦈⦇F⦈ =
                  ?const_comma c a⦇ArrMap⦈⦇F⦈"
                unfolding F_def A_def B_def
                by
                  (
                    cs_concl 
                      cs_intro:
                        cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
                      cs_simp: 
                        cat_cs_simps cat_comma_cs_simps f''_def[symmetric]
                  )
            qed (cs_concl cs_shallow cs_intro: cat_cs_intros)
          qed simp_all

          from that show
            "?UArr c ∙NTCF ?ntcf_const_c ?the_rKe_gf :
              cf_const (a ↓CF 𝔎) 𝔄 (?UObj a) ∘CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎 ↦CF
              𝔗 ∘CF a O⨅CF 𝔎 ∘CF ((g ∘A⇘ℭ⇙ f) A↓CF 𝔎) :
              c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
            by
              (
                cs_concl 
                  cs_simp: cat_Kan_cs_simps cat_comma_cs_simps cat_cs_simps
                  cs_intro: 
                    cat_lim_cs_intros
                    cat_comma_cs_intros
                    cat_Kan_cs_intros
                    cat_cs_intros
              )
          from that have dom_lhs:
            "𝒟∘ ((?UArr a ∘NTCF-CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇NTMap⦈) = c ↓CF 𝔎⦇Obj⦈"
            by
              (
                cs_concl cs_shallow
                  cs_intro: cat_cs_intros cat_comma_cs_intros
                  cs_simp: cat_cs_simps cat_comma_cs_simps
              )
          from that have dom_rhs: 
            "𝒟∘ ((?UArr c ∙NTCF ?ntcf_const_c ?the_rKe_gf)⦇NTMap⦈) = 
              c ↓CF 𝔎⦇Obj⦈"
            by
              (
                cs_concl
                  cs_intro: cat_cs_intros cat_Kan_cs_intros cat_comma_cs_intros
                  cs_simp: cat_Kan_cs_simps cat_cs_simps cat_comma_cs_simps
              )
          show 
            "(?UArr a ∘NTCF-CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇NTMap⦈ =
              (?UArr c ∙NTCF ?ntcf_const_c ?the_rKe_gf)⦇NTMap⦈"
          proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
            fix A assume prems: "A ∈∘ c ↓CF 𝔎⦇Obj⦈"
            with g_is_arr obtain b' f' 
              where A_def: "A = [0, b', f']∘"
                and b': "b' ∈∘ 𝔅⦇Obj⦈"
                and f': "f' : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
              by auto
            note 𝔗.HomCod.cat_Comp_assoc[cat_cs_simps del]
              and 𝔎.HomCod.cat_Comp_assoc[cat_cs_simps del]
              and category.cat_Comp_assoc[cat_cs_simps del]
            note [symmetric, cat_cs_simps] =
              lim_Obj_the_cf_rKe_commute[where lim_Obj=lim_Obj]
              𝔎.HomCod.cat_Comp_assoc  
              𝔗.HomCod.cat_Comp_assoc
            from assms(1,2) that prems lim_a lim_b lim_c b' f' show
              "(?UArr a ∘NTCF-CF (g ∘A⇘ℭ⇙ f) A↓CF 𝔎)⦇NTMap⦈⦇A⦈ =
                (?UArr c ∙NTCF ?ntcf_const_c ?the_rKe_gf)⦇NTMap⦈⦇A⦈"
              unfolding A_def
              by (*very slow*)
                (
                  cs_concl
                    cs_simp:
                      cat_cs_simps cat_Kan_cs_simps cat_comma_cs_simps 
                    cs_intro: 
                      cat_cs_intros cat_Kan_cs_intros cat_comma_cs_intros
                )+
          qed (cs_concl cs_simp: cs_intro: cat_cs_intros)+
        qed simp_all
      qed
    qed
    
    show "?the_cf_rKe⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ = 𝔄⦇CId⦈⦇?the_cf_rKe⦇ObjMap⦈⦇c⦈⦈"
      if "c ∈∘ ℭ⦇Obj⦈" for c
    proof-

      let ?ntcf_const_c = ‹ntcf_const (c ↓CF 𝔎) 𝔄 (𝔄⦇CId⦈⦇?UObj c⦈)›

      note lim_c = assms(3)[OF that]

      from that have CId_c: "ℭ⦇CId⦈⦇c⦈ : c ↦⇘ℭ⇙ c" 
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)

      interpret lim_c: is_cat_limit 
        α ‹c ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF c O⨅CF 𝔎› ‹?UObj c› ‹?UArr c›
        by (rule lim_c)

      show ?thesis
      proof
        (
          rule sym,
          rule the_cf_rKe_ArrMap_app(3)[
            where lim_Obj=lim_Obj, OF assms(1,2) CId_c lim_c lim_c
            ]
        )
        from that lim_c show 
          "𝔄⦇CId⦈⦇?the_cf_rKe⦇ObjMap⦈⦇c⦈⦈ : ?UObj c ↦⇘𝔄⇙ ?UObj c"
          by 
            (
              cs_concl cs_shallow
                cs_simp: cat_Kan_cs_simps
                cs_intro: cat_cs_intros cat_lim_cs_intros
            )
        have "?UArr c ∘NTCF-CF (ℭ⦇CId⦈⦇c⦈) A↓CF 𝔎 =  ?UArr c ∙NTCF ?ntcf_const_c"
        proof(rule ntcf_eqI)
          from lim_c that show 
            "?UArr c ∘NTCF-CF (ℭ⦇CId⦈⦇c⦈) A↓CF 𝔎 :
              cf_const (c ↓CF 𝔎) 𝔄 (?UObj c) ∘CF (ℭ⦇CId⦈⦇c⦈) A↓CF 𝔎 ↦CF
              𝔗 ∘CF c O⨅CF 𝔎 ∘CF (ℭ⦇CId⦈⦇c⦈) A↓CF 𝔎 :
              c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
            by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_comma_cs_intros)
          from lim_c that show 
            "?UArr c ∙NTCF ?ntcf_const_c :
               cf_const (c ↓CF 𝔎) 𝔄 (?UObj c) ∘CF (ℭ⦇CId⦈⦇c⦈) A↓CF 𝔎 ↦CF
               𝔗 ∘CF c O⨅CF 𝔎 ∘CF (ℭ⦇CId⦈⦇c⦈) A↓CF 𝔎 :
               c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
            by (*very slow*)
              (
                cs_concl 
                  cs_intro: cat_cs_intros 
                  cs_simp: 𝔎.cf_arr_cf_comma_CId cat_cs_simps 
                  cs_intro: cat_lim_cs_intros
              )
          from that have dom_lhs:
            "𝒟∘ ((?UArr c ∘NTCF-CF (ℭ⦇CId⦈⦇c⦈) A↓CF 𝔎)⦇NTMap⦈) = c ↓CF 𝔎⦇Obj⦈"
            by 
              (
                cs_concl cs_shallow
                  cs_simp: cat_cs_simps 
                  cs_intro: cat_cs_intros cat_comma_cs_intros
              )
          
          from that have dom_rhs:
            "𝒟∘ ((?UArr c ∙NTCF ?ntcf_const_c)⦇NTMap⦈) = c ↓CF 𝔎⦇Obj⦈"
            by
              (
                cs_concl 
                  cs_intro: cat_lim_cs_intros cat_cs_intros 
                  cs_simp: cat_cs_simps
              )
          show 
            "(?UArr c ∘NTCF-CF (ℭ⦇CId⦈⦇c⦈) A↓CF 𝔎)⦇NTMap⦈ =
              (?UArr c ∙NTCF ?ntcf_const_c)⦇NTMap⦈"
          proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
            fix A assume prems: "A ∈∘ c ↓CF 𝔎⦇Obj⦈"
            with that obtain b f 
              where A_def: "A = [0, b, f]∘"
                and b: "b ∈∘ 𝔅⦇Obj⦈" 
                and f: "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
              by auto
            from that prems f have 
              "?UArr c⦇NTMap⦈⦇0, b, f⦈∙ : ?UObj c ↦⇘𝔄⇙ 𝔗⦇ObjMap⦈⦇b⦈"
              unfolding A_def
              by
                (
                  cs_concl 
                    cs_simp: cat_cs_simps cat_comma_cs_simps 
                    cs_intro: cat_comma_cs_intros cat_cs_intros
                )
            from that prems f show 
              "(?UArr c ∘NTCF-CF (ℭ⦇CId⦈⦇c⦈) A↓CF 𝔎)⦇NTMap⦈⦇A⦈ =
                (?UArr c ∙NTCF ?ntcf_const_c)⦇NTMap⦈⦇A⦈"
              unfolding A_def 
              by
                (
                  cs_concl 
                    cs_simp: cat_cs_simps cat_comma_cs_simps
                    cs_intro:
                      cat_lim_cs_intros cat_comma_cs_intros cat_cs_intros
                )
          qed (cs_concl cs_intro: cat_cs_intros)
        qed simp_all

        with that show 
          "?UArr c ∘NTCF-CF (ℭ⦇CId⦈⦇c⦈) A↓CF 𝔎 = 
            ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 (𝔄⦇CId⦈⦇?the_cf_rKe⦇ObjMap⦈⦇c⦈⦈)"
          by 
            (
              cs_concl cs_shallow 
                cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros
            )

      qed

    qed

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

qed

lemma the_cf_lKe_is_functor:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ lim_Obj c⦇UArr⦈ :
      𝔗 ∘CF 𝔎 CF⨅O c >CF.colim lim_Obj c⦇UObj⦈ : 𝔎 CF↓ c ↦↦C⇘α⇙ 𝔄"
  shows "the_cf_lKe α 𝔗 𝔎 lim_Obj : ℭ ↦↦C⇘α⇙ 𝔄"
proof-
  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
  {
    fix c assume prems: "c ∈∘ ℭ⦇Obj⦈"
    from assms(3)[OF this] have lim_Obj_UArr: "lim_Obj c⦇UArr⦈ :
      𝔗 ∘CF 𝔎 CF⨅O c >CF.colim lim_Obj c⦇UObj⦈ : 𝔎 CF↓ c ↦↦C⇘α⇙ 𝔄". 
    then interpret lim_Obj_c: is_cat_colimit 
      α ‹𝔎 CF↓ c› 𝔄 ‹𝔗 ∘CF 𝔎 CF⨅O c› ‹lim_Obj c⦇UObj⦈› ‹lim_Obj c⦇UArr⦈›
      by simp
    note op_ua_UArr_is_cat_limit'[
      where lim_Obj=lim_Obj, OF assms(1,2) prems lim_Obj_UArr
      ]
  }
  note the_cf_rKe_is_functor = the_cf_rKe_is_functor
    [
      OF 𝔎.is_functor_op 𝔗.is_functor_op,
      unfolded cat_op_simps,
      where lim_Obj=‹op_ua lim_Obj 𝔎›, 
      unfolded cat_op_simps, 
      OF this,
      simplified,
      folded the_cf_lKe_def
    ]
  show "the_cf_lKe α 𝔗 𝔎 lim_Obj : ℭ ↦↦C⇘α⇙ 𝔄"
    by 
      (
        rule is_functor.is_functor_op
          [
            OF the_cf_rKe_is_functor, 
            folded the_cf_lKe_def,
            unfolded cat_op_simps
          ]
      )
qed

lemma the_ntcf_rKe_is_ntcf:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ" 
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ lim_Obj c⦇UArr⦈ : 
      lim_Obj c⦇UObj⦈ <CF.lim 𝔗 ∘CF c O⨅CF 𝔎 : c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
  shows "the_ntcf_rKe α 𝔗 𝔎 lim_Obj :
    the_cf_rKe α 𝔗 𝔎 lim_Obj ∘CF 𝔎 ↦CF 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
proof-

  let ?UObj = ‹λa. lim_Obj a⦇UObj⦈› 
  let ?UArr = ‹λa. lim_Obj a⦇UArr⦈›
  let ?const_comma = ‹λa b. cf_const (a ↓CF 𝔎) 𝔄 (?UObj b)›
  let ?the_cf_rKe = ‹the_cf_rKe α 𝔗 𝔎 lim_Obj›
  let ?the_ntcf_rKe = ‹the_ntcf_rKe α 𝔗 𝔎 lim_Obj›

  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
  interpret cf_rKe: is_functor α ℭ 𝔄 ‹?the_cf_rKe›
    by (rule the_cf_rKe_is_functor[OF assms, simplified])

  show ?thesis
  proof(rule is_ntcfI')
    show "vfsequence ?the_ntcf_rKe" unfolding the_ntcf_rKe_def by simp
    show "vcard ?the_ntcf_rKe = 5ℕ"
      unfolding the_ntcf_rKe_def by (simp add: nat_omega_simps)
    show "?the_ntcf_rKe⦇NTMap⦈⦇b⦈ : 
      (?the_cf_rKe ∘CF 𝔎)⦇ObjMap⦈⦇b⦈ ↦⇘𝔄⇙ 𝔗⦇ObjMap⦈⦇b⦈"
      if "b ∈∘ 𝔅⦇Obj⦈" for b
    proof-
      let ?𝔎b = ‹𝔎⦇ObjMap⦈⦇b⦈›
      from that have 𝔎b: "𝔎⦇ObjMap⦈⦇b⦈ ∈∘ ℭ⦇Obj⦈"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      note lim_𝔎b = assms(3)[OF 𝔎b]
      interpret lim_𝔎b: is_cat_limit 
        α ‹?𝔎b ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF ?𝔎b O⨅CF 𝔎› ‹?UObj ?𝔎b› ‹?UArr ?𝔎b›
        by (rule lim_𝔎b)
      from that lim_𝔎b show ?thesis
        by
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_comma_cs_simps cat_Kan_cs_simps
              cs_intro: cat_cs_intros cat_comma_cs_intros cat_Kan_cs_intros
          )+
    qed
    show 
      "?the_ntcf_rKe⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ (?the_cf_rKe ∘CF 𝔎)⦇ArrMap⦈⦇f⦈ =
        𝔗⦇ArrMap⦈⦇f⦈ ∘A⇘𝔄⇙ ?the_ntcf_rKe⦇NTMap⦈⦇a⦈"
      if "f : a ↦⇘𝔅⇙ b" for a b f 
    proof-
      let ?𝔎a = ‹𝔎⦇ObjMap⦈⦇a⦈› and ?𝔎b = ‹𝔎⦇ObjMap⦈⦇b⦈› and ?𝔎f = ‹𝔎⦇ArrMap⦈⦇f⦈›
      from that have 𝔎a: "?𝔎a ∈∘ ℭ⦇Obj⦈" 
        and 𝔎b: "?𝔎b ∈∘ ℭ⦇Obj⦈"
        and 𝔎f: "?𝔎f : ?𝔎a ↦⇘ℭ⇙ ?𝔎b"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
      note lim_𝔎a = assms(3)[OF 𝔎a]
        and lim_𝔎b = assms(3)[OF 𝔎b]
      from that have z_b_𝔎b: "[0, b, ℭ⦇CId⦈⦇?𝔎b⦈]∘ ∈∘ ?𝔎b ↓CF 𝔎⦇Obj⦈"
        by (cs_concl cs_intro: cat_cs_intros cat_comma_cs_intros)
      from 
        lim_Obj_the_cf_rKe_commute[
          OF assms(1,2) lim_𝔎a lim_𝔎b 𝔎f z_b_𝔎b, symmetric
          ]
        that
      have [cat_Kan_cs_simps]:
        "?UArr ?𝔎b⦇NTMap⦈⦇0, b, ℭ⦇CId⦈⦇?𝔎b⦈⦈∙ ∘A⇘𝔄⇙ ?the_cf_rKe⦇ArrMap⦈⦇?𝔎f⦈ =
          ?UArr ?𝔎a⦇NTMap⦈⦇0, b, ?𝔎f⦈∙"
        by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      interpret lim_𝔎a: is_cat_limit
        α ‹?𝔎a ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF ?𝔎a O⨅CF 𝔎› ‹?UObj ?𝔎a› ‹?UArr ?𝔎a›
        by (rule lim_𝔎a)
      interpret lim_𝔎b: is_cat_limit 
        α ‹?𝔎b ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF ?𝔎b O⨅CF 𝔎› ‹?UObj ?𝔎b› ‹?UArr ?𝔎b›
        by (rule lim_𝔎b)
      note lim_𝔎a.cat_cone_Comp_commute[cat_cs_simps del]
      note lim_𝔎b.cat_cone_Comp_commute[cat_cs_simps del]
      from that have 
        "[[0, a, ℭ⦇CId⦈⦇?𝔎a⦈]∘, [0, b, ?𝔎f]∘, [0, f]∘]∘ :
          [0, a, ℭ⦇CId⦈⦇?𝔎a⦈]∘ ↦⇘(?𝔎a) ↓CF 𝔎⇙ [0, b, ?𝔎f]∘"
        by
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_comma_cs_simps
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
      from lim_𝔎a.ntcf_Comp_commute[OF this, symmetric] that
      have [cat_Kan_cs_simps]:
        "𝔗⦇ArrMap⦈⦇f⦈ ∘A⇘𝔄⇙ ?UArr (?𝔎a)⦇NTMap⦈ ⦇0, a, ℭ⦇CId⦈⦇?𝔎a⦈⦈∙ =
          ?UArr ?𝔎a⦇NTMap⦈⦇0, b, ?𝔎f⦈∙"
        by 
          (
            cs_prems
              cs_simp: cat_cs_simps cat_comma_cs_simps
              cs_intro: cat_cs_intros cat_comma_cs_intros cat_1_is_arrI
          )
      from that show ?thesis
        by 
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_Kan_cs_simps cs_intro: cat_cs_intros
          )
    qed
  qed
    (
      cs_concl 
        cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
    )+

qed

lemma the_ntcf_lKe_is_ntcf:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ" 
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ lim_Obj c⦇UArr⦈ :
      𝔗 ∘CF 𝔎 CF⨅O c >CF.colim lim_Obj c⦇UObj⦈ : 𝔎 CF↓ c ↦↦C⇘α⇙ 𝔄"
  shows "the_ntcf_lKe α 𝔗 𝔎 lim_Obj :
    𝔗 ↦CF the_cf_lKe α 𝔗 𝔎 lim_Obj ∘CF 𝔎 : 𝔅 ↦↦C⇘α⇙ 𝔄"
proof-
  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
  {
    fix c assume prems: "c ∈∘ ℭ⦇Obj⦈"
    from assms(3)[OF this] have lim_Obj_UArr: "lim_Obj c⦇UArr⦈ :
      𝔗 ∘CF 𝔎 CF⨅O c >CF.colim lim_Obj c⦇UObj⦈ : 𝔎 CF↓ c ↦↦C⇘α⇙ 𝔄". 
    then interpret lim_Obj_c: is_cat_colimit 
      α ‹𝔎 CF↓ c› 𝔄 ‹𝔗 ∘CF 𝔎 CF⨅O c› ‹lim_Obj c⦇UObj⦈› ‹lim_Obj c⦇UArr⦈›
      by simp
    note op_ua_UArr_is_cat_limit'[
      where lim_Obj=lim_Obj, OF assms(1,2) prems lim_Obj_UArr
      ]
  }
  note the_ntcf_rKe_is_ntcf = the_ntcf_rKe_is_ntcf
    [
      OF 𝔎.is_functor_op 𝔗.is_functor_op,
      unfolded cat_op_simps,
      where lim_Obj=‹op_ua lim_Obj 𝔎›,
      unfolded cat_op_simps,
      OF this,
      simplified
    ]
  show "the_ntcf_lKe α 𝔗 𝔎 lim_Obj :
    𝔗 ↦CF the_cf_lKe α 𝔗 𝔎 lim_Obj ∘CF 𝔎 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    by 
      (
        rule is_ntcf.is_ntcf_op
          [
            OF the_ntcf_rKe_is_ntcf,
            unfolded cat_op_simps, 
            folded the_cf_lKe_def the_ntcf_lKe_def
          ]
       )
qed

lemma the_ntcf_rKe_is_cat_rKe:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ"
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ lim_Obj c⦇UArr⦈ :
      lim_Obj c⦇UObj⦈ <CF.lim 𝔗 ∘CF c O⨅CF 𝔎 : c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
  shows "the_ntcf_rKe α 𝔗 𝔎 lim_Obj :
    the_cf_rKe α 𝔗 𝔎 lim_Obj ∘CF 𝔎 ↦CF.rKe⇘α⇙ 𝔗 : 𝔅 ↦C ℭ ↦C 𝔄"
proof-

  let ?UObj = ‹λa. lim_Obj a⦇UObj⦈› 
  let ?UArr = ‹λa. lim_Obj a⦇UArr⦈›
  let ?the_cf_rKe = ‹the_cf_rKe α 𝔗 𝔎 lim_Obj›
  let ?the_ntcf_rKe = ‹the_ntcf_rKe α 𝔗 𝔎 lim_Obj›

  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
  interpret cf_rKe: is_functor α ℭ 𝔄 ?the_cf_rKe
    by (rule the_cf_rKe_is_functor[OF assms, simplified])
  interpret ntcf_rKe: is_ntcf α 𝔅 𝔄 ‹?the_cf_rKe ∘CF 𝔎› 𝔗 ?the_ntcf_rKe
    by (intro the_ntcf_rKe_is_ntcf assms(3))
      (cs_concl cs_shallow cs_intro: cat_cs_intros)+

  show ?thesis
  proof(rule is_cat_rKeI')

    fix 𝔊 ε assume prems: 
      "𝔊 : ℭ ↦↦C⇘α⇙ 𝔄" "ε : 𝔊 ∘CF 𝔎 ↦CF 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"

    interpret 𝔊: is_functor α ℭ 𝔄 𝔊 by (rule prems(1))
    interpret ε: is_ntcf α 𝔅 𝔄 ‹𝔊 ∘CF 𝔎› 𝔗 ε by (rule prems(2))

    define ε' where "ε' c =
      [
        (λA∈∘c ↓CF 𝔎⦇Obj⦈. ε⦇NTMap⦈⦇A⦇1ℕ⦈⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇A⦇2ℕ⦈⦈),
        cf_const (c ↓CF 𝔎) 𝔄 (𝔊⦇ObjMap⦈⦇c⦈),
        𝔗 ∘CF c O⨅CF 𝔎,
        c ↓CF 𝔎,
        𝔄
      ]∘"
      for c

    have ε'_components: 
      "ε' c⦇NTMap⦈ = (λA∈∘c ↓CF 𝔎⦇Obj⦈. ε⦇NTMap⦈⦇A⦇1ℕ⦈⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇A⦇2ℕ⦈⦈)"
      "ε' c⦇NTDom⦈ = cf_const (c ↓CF 𝔎) 𝔄 (𝔊⦇ObjMap⦈⦇c⦈)"
      "ε' c⦇NTCod⦈ = 𝔗 ∘CF c O⨅CF 𝔎"
      "ε' c⦇NTDGDom⦈ = c ↓CF 𝔎"
      "ε' c⦇NTDGCod⦈ = 𝔄"
      for c 
      unfolding ε'_def nt_field_simps by (simp_all add: nat_omega_simps)
    note [cat_Kan_cs_simps] = ε'_components(2-5)
    have [cat_Kan_cs_simps]: "ε' c⦇NTMap⦈⦇A⦈ = ε⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f⦈"
      if "A = [a, b, f]∘" and "[a, b, f]∘ ∈∘ c ↓CF 𝔎⦇Obj⦈" for A a b c f
      using that unfolding ε'_components by (auto simp: nat_omega_simps)

    have ε': "ε' c : 𝔊⦇ObjMap⦈⦇c⦈ <CF.cone 𝔗 ∘CF c O⨅CF 𝔎 : c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
      and ε'_unique: "∃!f'.
        f' : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c ∧
        ε' c = ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 f'" 
      if c: "c ∈∘ ℭ⦇Obj⦈" for c
    proof-
      from that have "?the_cf_rKe⦇ObjMap⦈⦇c⦈ = ?UObj c"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros
          )
      interpret lim_c: is_cat_limit 
        α ‹c ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF c O⨅CF 𝔎› ‹?UObj c› ‹?UArr c›
        by (rule assms(3)[OF that])
      show "ε' c : 𝔊⦇ObjMap⦈⦇c⦈ <CF.cone 𝔗 ∘CF c O⨅CF 𝔎 : c ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
      proof(intro is_cat_coneI is_ntcfI')
        show "vfsequence (ε' c)" unfolding ε'_def by simp
        show "vcard (ε' c) = 5ℕ" unfolding ε'_def by (simp add: nat_omega_simps)
        show "vsv (ε' c⦇NTMap⦈)" unfolding ε'_components by simp 
        show "𝒟∘ (ε' c⦇NTMap⦈) = c ↓CF 𝔎⦇Obj⦈" unfolding ε'_components by simp
        show "ε' c⦇NTMap⦈⦇A⦈ :
          cf_const (c ↓CF 𝔎) 𝔄 (𝔊⦇ObjMap⦈⦇c⦈)⦇ObjMap⦈⦇A⦈ ↦⇘𝔄⇙
          (𝔗 ∘CF c O⨅CF 𝔎)⦇ObjMap⦈⦇A⦈"
          if "A ∈∘ c ↓CF 𝔎⦇Obj⦈" for A
        proof-
          from that prems c obtain b f 
            where A_def: "A = [0, b, f]∘"
              and b: "b ∈∘ 𝔅⦇Obj⦈" 
              and f: "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
            by auto
          from that prems f c that b f show ?thesis
            unfolding A_def
            by
              (
                cs_concl cs_shallow
                  cs_simp: cat_cs_simps cat_Kan_cs_simps cat_comma_cs_simps
                  cs_intro: cat_cs_intros cat_comma_cs_intros
              )
        qed
        show
          "ε' c⦇NTMap⦈⦇B⦈ ∘A⇘𝔄⇙ cf_const (c ↓CF 𝔎) 𝔄 (𝔊⦇ObjMap⦈⦇c⦈)⦇ArrMap⦈⦇F⦈ =
            (𝔗 ∘CF c O⨅CF 𝔎)⦇ArrMap⦈⦇F⦈ ∘A⇘𝔄⇙ ε' c⦇NTMap⦈⦇A⦈"
          if "F : A ↦⇘c ↓CF 𝔎⇙ B" for A B F
        proof-
          from that c 
          obtain b f b' f' k 
            where F_def: "F = [[0, b, f]∘, [0, b', f']∘, [0, k]∘]∘"
              and A_def: "A = [0, b, f]∘"
              and B_def: "B = [0, b', f']∘"
              and k: "k : b ↦⇘𝔅⇙ b'"
              and f: "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
              and f': "f' : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
              and f'_def: "𝔎⦇ArrMap⦈⦇k⦈ ∘A⇘ℭ⇙ f = f'"
            by auto
          from c that k f f' show ?thesis
            unfolding F_def A_def B_def
            by (*slow*)
              (
                cs_concl 
                  cs_simp:
                    cat_cs_simps
                    cat_comma_cs_simps
                    cat_Kan_cs_simps
                    ε.ntcf_Comp_commute''
                    f'_def[symmetric]
                  cs_intro: cat_cs_intros cat_comma_cs_intros
              )
        qed
      qed
        (
          use c that in
            ‹cs_concl cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros›
        )+
      from is_cat_limit.cat_lim_ua_fo[OF assms(3)[OF that] this] show 
        "∃!f'.
          f' : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c ∧
          ε' c = ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 f'"  
        by simp
    qed

    define σ :: V where
      "σ =
        [
          (
            λc∈∘ℭ⦇Obj⦈. THE f.
              f : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c ∧
              ε' c = ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 f
          ),
          𝔊,
          ?the_cf_rKe,
          ℭ,
          𝔄
        ]∘"

    have σ_components:
      "σ⦇NTMap⦈ =
        (
          λc∈∘ℭ⦇Obj⦈. THE f.
            f : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c ∧
            ε' c = ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 f
        )"
      "σ⦇NTDom⦈ = 𝔊"
      "σ⦇NTCod⦈ = ?the_cf_rKe"
      "σ⦇NTDGDom⦈ = ℭ"
      "σ⦇NTDGCod⦈ = 𝔄"
      unfolding σ_def nt_field_simps by (simp_all add: nat_omega_simps)

    note [cat_Kan_cs_simps] = σ_components(2-5)

    have σ_NTMap_app_def: "σ⦇NTMap⦈⦇c⦈ =
      (
        THE f.
          f : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c ∧
          ε' c = ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 f
      )"
      if "c ∈∘ ℭ⦇Obj⦈" for c
      using that unfolding σ_components by simp

    have σ_NTMap_app_is_arr: "σ⦇NTMap⦈⦇c⦈ : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c"
      and ε'_σ_commute:
        "ε' c = ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 (σ⦇NTMap⦈⦇c⦈)"
      and σ_NTMap_app_unique:
        "⟦
          f : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c;
          ε' c = ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 f
         ⟧ ⟹ f = σ⦇NTMap⦈⦇c⦈"
        if c: "c ∈∘ ℭ⦇Obj⦈" for c f
    proof-
      have 
        "σ⦇NTMap⦈⦇c⦈ : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c ∧
        ε' c = ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 (σ⦇NTMap⦈⦇c⦈)"
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_Kan_cs_simps σ_NTMap_app_def 
              cs_intro: theI' ε'_unique that
          )
      then show "σ⦇NTMap⦈⦇c⦈ : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c"
        and "ε' c = ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 (σ⦇NTMap⦈⦇c⦈)"
        by simp_all
      with c ε'_unique[OF c] show "f = σ⦇NTMap⦈⦇c⦈"
        if "f : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c"
          and "ε' c = ?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 f"
        using that by metis
    qed

    have σ_NTMap_app_is_arr'[cat_Kan_cs_intros]: "σ⦇NTMap⦈⦇c⦈ : a ↦⇘𝔄'⇙ b"
      if "c ∈∘ ℭ⦇Obj⦈" 
        and "a = 𝔊⦇ObjMap⦈⦇c⦈" 
        and "b = ?UObj c" 
        and "𝔄' = 𝔄"
      for 𝔄' a b c
      by (simp add: that σ_NTMap_app_is_arr)

    have ε'_NTMap_app_def: 
      "ε' c⦇NTMap⦈⦇A⦈ =
        (?UArr c ∙NTCF ntcf_const (c ↓CF 𝔎) 𝔄 (σ⦇NTMap⦈⦇c⦈))⦇NTMap⦈⦇A⦈"
      if "A ∈∘ c ↓CF 𝔎⦇Obj⦈" and "c ∈∘ ℭ⦇Obj⦈" for A c
      using ε'_σ_commute[OF that(2)] by simp
    have εb_𝔊f:
      "ε⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f⦈ =
        ?UArr c⦇NTMap⦈⦇a, b, f⦈∙ ∘A⇘𝔄⇙ σ⦇NTMap⦈⦇c⦈"
      if "A = [a, b, f]∘" and "A ∈∘ c ↓CF 𝔎⦇Obj⦈" and "c ∈∘ ℭ⦇Obj⦈" 
      for A a b c f
    proof-
      interpret lim_c: is_cat_limit 
        α ‹c ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF c O⨅CF 𝔎› ‹?UObj c› ‹?UArr c›
        by (rule assms(3)[OF that(3)])
      from that have b: "b ∈∘ 𝔅⦇Obj⦈" and f: "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
        by blast+
      show
        "ε⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f⦈ =
          ?UArr c⦇NTMap⦈⦇a, b, f⦈∙ ∘A⇘𝔄⇙ σ⦇NTMap⦈⦇c⦈"
        using ε'_NTMap_app_def[OF that(2,3)] that(2,3)
        unfolding that(1)
        by
          (
            cs_prems cs_shallow
              cs_simp: cat_cs_simps cat_Kan_cs_simps
              cs_intro: cat_cs_intros cat_Kan_cs_intros
          )
    qed

    show "∃!σ.
      σ : 𝔊 ↦CF ?the_cf_rKe : ℭ ↦↦C⇘α⇙ 𝔄 ∧
      ε = ?the_ntcf_rKe ∙NTCF (σ ∘NTCF-CF 𝔎)"
    proof(intro ex1I[where a=σ] conjI; (elim conjE)?)

      define τ where "τ a b f =
        [
          (
            λF∈∘b ↓CF 𝔎⦇Obj⦈.
              ?UArr b⦇NTMap⦈⦇F⦈ ∘A⇘𝔄⇙ σ⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f⦈
          ),
          cf_const (b ↓CF 𝔎) 𝔄 (𝔊⦇ObjMap⦈⦇a⦈),
          𝔗 ∘CF b O⨅CF 𝔎,
          b ↓CF 𝔎,
          𝔄
        ]∘"
        for a b f

      have τ_components:
        "τ a b f⦇NTMap⦈ =
          (
            λF∈∘b ↓CF 𝔎⦇Obj⦈.
              ?UArr b⦇NTMap⦈⦇F⦈ ∘A⇘𝔄⇙ σ⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f⦈
          )"
        "τ a b f⦇NTDom⦈ = cf_const (b ↓CF 𝔎) 𝔄 (𝔊⦇ObjMap⦈⦇a⦈)"
        "τ a b f⦇NTCod⦈ = 𝔗 ∘CF b O⨅CF 𝔎"
        "τ a b f⦇NTDGDom⦈ = b ↓CF 𝔎"
        "τ a b f⦇NTDGCod⦈ = 𝔄"
        for a b f
        unfolding τ_def nt_field_simps by (simp_all add: nat_omega_simps)
      note [cat_Kan_cs_simps] = τ_components(2-5)
      have τ_NTMap_app[cat_Kan_cs_simps]: 
        "τ a b f⦇NTMap⦈⦇F⦈ =
          ?UArr b⦇NTMap⦈⦇F⦈ ∘A⇘𝔄⇙ σ⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f⦈"
        if "F ∈∘ b ↓CF 𝔎⦇Obj⦈" for a b f F
        using that unfolding τ_components by auto
      
      have τ: "τ a b f :
        𝔊⦇ObjMap⦈⦇a⦈ <CF.cone 𝔗 ∘CF b O⨅CF 𝔎 : b ↓CF 𝔎 ↦↦C⇘α⇙ 𝔄"
        if f_is_arr: "f : a ↦⇘ℭ⇙ b" for a b f
      proof-

        note f = 𝔎.HomCod.cat_is_arrD[OF that]
        note lim_a = assms(3)[OF f(2)] and lim_b = assms(3)[OF f(3)]

        interpret lim_b: is_cat_limit 
          α ‹b ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF b O⨅CF 𝔎› ‹?UObj b› ‹?UArr b›
          by (rule lim_b)

        note lim_b.cat_cone_Comp_commute[cat_cs_simps del]

        from f have a: "a ∈∘ ℭ⦇Obj⦈" and b: "b ∈∘ ℭ⦇Obj⦈" by auto

        show ?thesis
        proof(intro is_cat_coneI is_ntcfI')

          show "vfsequence (τ a b f)" unfolding τ_def by simp
          show "vcard (τ a b f) = 5ℕ" 
            unfolding τ_def by (simp add: nat_omega_simps)
          show "vsv (τ a b f⦇NTMap⦈)" unfolding τ_components by auto
          show "𝒟∘ (τ a b f⦇NTMap⦈) = b ↓CF 𝔎⦇Obj⦈" by (auto simp: τ_components)
          show "τ a b f⦇NTMap⦈⦇A⦈ :
            cf_const (b ↓CF 𝔎) 𝔄 (𝔊⦇ObjMap⦈⦇a⦈)⦇ObjMap⦈⦇A⦈ ↦⇘𝔄⇙
            (𝔗 ∘CF b O⨅CF 𝔎)⦇ObjMap⦈⦇A⦈"
            if "A ∈∘ b ↓CF 𝔎⦇Obj⦈" for A
          proof-
            from that f_is_arr obtain b' f' 
              where A_def: "A = [0, b', f']∘"
                and b': "b' ∈∘ 𝔅⦇Obj⦈"
                and f': "f' : b ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
              by auto
            from  f_is_arr that b' f' a b show ?thesis
              unfolding A_def
              by
                (
                  cs_concl cs_shallow
                    cs_simp: cat_cs_simps cat_comma_cs_simps cat_Kan_cs_simps
                    cs_intro: cat_cs_intros cat_comma_cs_intros cat_Kan_cs_intros
                )   
          qed
          show
            "τ a b f⦇NTMap⦈⦇B⦈ ∘A⇘𝔄⇙
              cf_const (b ↓CF 𝔎) 𝔄 (𝔊⦇ObjMap⦈⦇a⦈)⦇ArrMap⦈⦇F⦈ =
              (𝔗 ∘CF b O⨅CF 𝔎)⦇ArrMap⦈⦇F⦈ ∘A⇘𝔄⇙ τ a b f⦇NTMap⦈⦇A⦈"
            if "F : A ↦⇘b ↓CF 𝔎⇙ B" for A B F
          proof-
            from that have F: "F : A ↦⇘b ↓CF 𝔎⇙ B"
              by (auto intro: is_arrI)
            with f_is_arr obtain b' f' b'' f'' h'
              where F_def: "F = [[0, b', f']∘, [0, b'', f'']∘, [0, h']∘]∘"
                and A_def: "A = [0, b', f']∘"
                and B_def: "B = [0, b'', f'']∘"
                and h': "h' : b' ↦⇘𝔅⇙ b''"
                and f': "f' : b ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
                and f'': "f'' : b ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b''⦈"
                and f''_def: "𝔎⦇ArrMap⦈⦇h'⦈ ∘A⇘ℭ⇙ f' = f''"
              by auto
            from
              lim_b.ntcf_Comp_commute[OF that] 
              that f_is_arr g' h' f' f'' 
            have [cat_Kan_cs_simps]:
              "?UArr b⦇NTMap⦈⦇0, b'', 𝔎⦇ArrMap⦈⦇h'⦈ ∘A⇘ℭ⇙ f'⦈∙ =
                𝔗⦇ArrMap⦈⦇h'⦈ ∘A⇘𝔄⇙ ?UArr b⦇NTMap⦈⦇0, b', f'⦈∙"
              unfolding F_def A_def B_def
              by
                (
                  cs_prems 
                    cs_simp: 
                      cat_cs_simps cat_comma_cs_simps f''_def[symmetric]
                    cs_intro: cat_cs_intros cat_comma_cs_intros
                )
            from f_is_arr that g' h' f' f'' show ?thesis
              unfolding F_def A_def B_def (*very slow*)
              by
                (
                  cs_concl 
                    cs_simp:
                      cat_cs_simps 
                      cat_Kan_cs_simps 
                      cat_comma_cs_simps 
                      f''_def[symmetric]
                    cs_intro:
                      cat_cs_intros cat_Kan_cs_intros cat_comma_cs_intros
                )+
          qed

        qed
          (
            use that f_is_arr in
              ‹
                cs_concl 
                  cs_simp: cat_cs_simps cat_Kan_cs_simps cs_intro: cat_cs_intros
              ›
          )+
      qed

      show σ: "σ : 𝔊 ↦CF ?the_cf_rKe : ℭ ↦↦C⇘α⇙ 𝔄"
      proof(rule is_ntcfI')

        show "vfsequence σ" unfolding σ_def by simp
        show "vcard σ = 5ℕ" unfolding σ_def by (simp add: nat_omega_simps)
        show "vsv (σ⦇NTMap⦈)" unfolding σ_components by auto
        show "𝒟∘ (σ⦇NTMap⦈) = ℭ⦇Obj⦈" unfolding σ_components by simp
        show "σ⦇NTMap⦈⦇a⦈ : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ ?the_cf_rKe⦇ObjMap⦈⦇a⦈"
          if "a ∈∘ ℭ⦇Obj⦈" for a
          using that 
          by
            (
              cs_concl 
                cs_simp: cat_cs_simps cat_Kan_cs_simps
                cs_intro: cat_cs_intros cat_Kan_cs_intros
            )

        then have [cat_Kan_cs_intros]: "σ⦇NTMap⦈⦇a⦈ : b ↦⇘𝔄⇙ c"
          if "a ∈∘ ℭ⦇Obj⦈" 
            and "b = 𝔊⦇ObjMap⦈⦇a⦈" 
            and "c = ?the_cf_rKe⦇ObjMap⦈⦇a⦈"
          for a b c
          using that(1) unfolding that(2,3) by simp

        show 
          "σ⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f⦈ =
            ?the_cf_rKe⦇ArrMap⦈⦇f⦈ ∘A⇘𝔄⇙ σ⦇NTMap⦈⦇a⦈"
          if f_is_arr: "f : a ↦⇘ℭ⇙ b" for a b f
        proof-

          note f = 𝔎.HomCod.cat_is_arrD[OF that]
          note lim_a = assms(3)[OF f(2)] and lim_b = assms(3)[OF f(3)]

          interpret lim_a: is_cat_limit 
            α ‹a ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF a O⨅CF 𝔎› ‹?UObj a› ‹?UArr a›
            by (rule lim_a)
          interpret lim_b: is_cat_limit 
            α ‹b ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF b O⨅CF 𝔎› ‹?UObj b› ‹?UArr b›
            by (rule lim_b)

          from f have a: "a ∈∘ ℭ⦇Obj⦈" and b: "b ∈∘ ℭ⦇Obj⦈" by auto
          
          from lim_b.cat_lim_unique_cone'[OF τ[OF that]] obtain g' 
            where g': "g' : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ ?UObj b"
              and τ_NTMap_app: "⋀A. A ∈∘ (b ↓CF 𝔎⦇Obj⦈) ⟹
                τ a b f⦇NTMap⦈⦇A⦈ = ?UArr b⦇NTMap⦈⦇A⦈ ∘A⇘𝔄⇙ g'"
              and g'_unique: "⋀g''.
                ⟦
                  g'' : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ ?UObj b;
                  ⋀A. A ∈∘ b ↓CF 𝔎⦇Obj⦈ ⟹
                    τ a b f⦇NTMap⦈⦇A⦈ = ?UArr b⦇NTMap⦈⦇A⦈ ∘A⇘𝔄⇙ g''
                ⟧ ⟹ g'' = g'"
            by metis

          have lim_Obj_a_f𝔎[symmetric, cat_Kan_cs_simps]:
            "?UArr a⦇NTMap⦈⦇a', b', f' ∘A⇘ℭ⇙ f⦈∙ =
              ?UArr b⦇NTMap⦈⦇A⦈ ∘A⇘𝔄⇙ ?the_cf_rKe⦇ArrMap⦈⦇f⦈"
            if "A = [a', b', f']∘" and "A ∈∘ b ↓CF 𝔎⦇Obj⦈" for A a' b' f'
          proof-
            from that(2) f_is_arr have a'_def: "a' = 0" 
              and b': "b' ∈∘ 𝔅⦇Obj⦈" 
              and f': "f' : b ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
              unfolding that(1) by auto
            show ?thesis 
              unfolding that(1) 
              by 
                (
                  rule 
                    lim_Obj_the_cf_rKe_commute
                      [
                        where lim_Obj=lim_Obj, 
                        OF 
                          assms(1,2) 
                          lim_a 
                          lim_b 
                          f_is_arr 
                          that(2)[unfolded that(1)] 
                      ]
                )
          qed
          {
            fix a' b' f' A
            note 𝔗.HomCod.cat_assoc_helper[
              where h=‹?UArr b⦇NTMap⦈⦇a',b',f'⦈∙› 
                and g=‹?the_cf_rKe⦇ArrMap⦈⦇f⦈›
                and q=‹?UArr a⦇NTMap⦈⦇a', b', f' ∘A⇘ℭ⇙ f⦈∙›
                ]
          }
          note [cat_Kan_cs_simps] = this

          show ?thesis
          proof(rule trans_sym[where s=g'])
            show "σ⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f⦈ = g'"
            proof(rule g'_unique)
              from that show
                "σ⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f⦈ : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ ?UObj b"
                by (cs_concl cs_intro: cat_cs_intros cat_Kan_cs_intros)
              fix A assume prems': "A ∈∘ b ↓CF 𝔎⦇Obj⦈"
              with f_is_arr obtain b' f' 
                where A_def: "A = [0, b', f']∘"
                  and b': "b' ∈∘ 𝔅⦇Obj⦈"
                  and f': "f' : b ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
                by auto
              from f_is_arr prems' show
                "τ a b f⦇NTMap⦈⦇A⦈ =
                  ?UArr b⦇NTMap⦈⦇A⦈ ∘A⇘𝔄⇙ (σ⦇NTMap⦈⦇b⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f⦈)"
                unfolding A_def
                by
                  (
                    cs_concl 
                      cs_simp: cat_cs_simps cat_Kan_cs_simps
                      cs_intro: cat_cs_intros cat_Kan_cs_intros
                  )
            qed
            show "?the_cf_rKe⦇ArrMap⦈⦇f⦈ ∘A⇘𝔄⇙ σ⦇NTMap⦈⦇a⦈ = g'"
            proof(rule g'_unique)                  
              fix A assume prems': "A ∈∘ b ↓CF 𝔎⦇Obj⦈"
              with f_is_arr obtain b' f' 
                where A_def: "A = [0, b', f']∘"
                  and b': "b' ∈∘ 𝔅⦇Obj⦈"
                  and f': "f' : b ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
                by auto
              {
                fix a' b' f' A
                note 𝔗.HomCod.cat_assoc_helper
                  [
                    where h=‹?UArr b⦇NTMap⦈⦇a', b', f'⦈∙› 
                      and g=‹σ⦇NTMap⦈⦇b⦈›
                      and q=‹ε⦇NTMap⦈⦇b'⦈ ∘A⇘𝔄⇙ 𝔊⦇ArrMap⦈⦇f'⦈›
                  ]
              }
              note [cat_Kan_cs_simps] = 
                this
                εb_𝔊f[OF A_def prems' b, symmetric]
                εb_𝔊f[symmetric]
              from f_is_arr prems' b' f' show 
                "τ a b f⦇NTMap⦈⦇A⦈ =
                  ?UArr b⦇NTMap⦈⦇A⦈ ∘A⇘𝔄⇙ 
                    (?the_cf_rKe⦇ArrMap⦈⦇f⦈ ∘A⇘𝔄⇙ σ⦇NTMap⦈⦇a⦈)"
                unfolding A_def
                by
                  (
                    cs_concl
                      cs_simp: 
                        cat_cs_simps 
                        cat_Kan_cs_simps 
                        cat_comma_cs_simps
                        cat_op_simps
                      cs_intro: 
                        cat_cs_intros 
                        cat_Kan_cs_intros 
                        cat_comma_cs_intros 
                        cat_op_intros
                  )
            qed
              (
                use that in
                  ‹
                    cs_concl 
                      cs_simp: cat_Kan_cs_simps
                      cs_intro: cat_cs_intros cat_Kan_cs_intros
                  ›
              )
          qed
        qed
      qed
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_Kan_cs_simps
            cs_intro: cat_cs_intros
        )+
      then interpret σ: is_ntcf α ℭ 𝔄 𝔊 ‹?the_cf_rKe› σ by simp

      show "ε = ?the_ntcf_rKe ∙NTCF (σ ∘NTCF-CF 𝔎)"
      proof(rule ntcf_eqI)
        have dom_lhs: "𝒟∘ (ε⦇NTMap⦈) = 𝔅⦇Obj⦈" 
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)
        have dom_rhs: "𝒟∘ ((?the_ntcf_rKe ∙NTCF (σ ∘NTCF-CF 𝔎))⦇NTMap⦈) = 𝔅⦇Obj⦈"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        show "ε⦇NTMap⦈ = (?the_ntcf_rKe ∙NTCF (σ ∘NTCF-CF 𝔎))⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix b assume prems': "b ∈∘ 𝔅⦇Obj⦈"
          note [cat_Kan_cs_simps] = εb_𝔊f[
            where f=‹ℭ⦇CId⦈⦇𝔎⦇ObjMap⦈⦇b⦈⦈› and c=‹𝔎⦇ObjMap⦈⦇b⦈›, symmetric
            ]
          from prems' σ show 
            "ε⦇NTMap⦈⦇b⦈ = (?the_ntcf_rKe ∙NTCF (σ ∘NTCF-CF 𝔎))⦇NTMap⦈⦇b⦈"
            by
              (
                cs_concl 
                  cs_simp: cat_cs_simps cat_comma_cs_simps cat_Kan_cs_simps 
                  cs_intro: cat_cs_intros cat_comma_cs_intros cat_Kan_cs_intros
              )
        qed (cs_concl cs_intro: cat_cs_intros V_cs_intros)
      qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+

      fix σ' assume prems':
        "σ' : 𝔊 ↦CF ?the_cf_rKe : ℭ ↦↦C⇘α⇙ 𝔄"
        "ε = ?the_ntcf_rKe ∙NTCF (σ' ∘NTCF-CF 𝔎)"

      interpret σ': is_ntcf α ℭ 𝔄 𝔊 ‹?the_cf_rKe› σ' by (rule prems'(1))

      have ε_NTMap_app[symmetric, cat_Kan_cs_simps]: 
        "ε⦇NTMap⦈⦇b'⦈ =
          ?UArr (𝔎⦇ObjMap⦈⦇b'⦈)⦇NTMap⦈⦇a', b', ℭ⦇CId⦈⦇𝔎⦇ObjMap⦈⦇b'⦈⦈⦈∙ ∘A⇘𝔄⇙
          σ'⦇NTMap⦈⦇𝔎⦇ObjMap⦈⦇b'⦈⦈"
        if "b' ∈∘ 𝔅⦇Obj⦈" and "a' = 0" for a' b'
      proof-
        from prems'(2) have ε_NTMap_app: 
          "ε⦇NTMap⦈⦇b'⦈ = (?the_ntcf_rKe ∙NTCF (σ' ∘NTCF-CF 𝔎))⦇NTMap⦈⦇b'⦈"
          for b'
          by simp
        show ?thesis
          using ε_NTMap_app[of b'] that(1)
          unfolding that(2)
          by
            (
              cs_prems cs_shallow
                cs_simp: cat_cs_simps cat_comma_cs_simps cat_Kan_cs_simps
                cs_intro: cat_cs_intros cat_comma_cs_intros
            )
      qed
      {
        fix a' b' f' A
        note 𝔗.HomCod.cat_assoc_helper
          [
            where h= ‹?UArr (𝔎⦇ObjMap⦈⦇b'⦈)⦇NTMap⦈⦇a', b', ℭ⦇CId⦈⦇𝔎⦇ObjMap⦈⦇b'⦈⦈⦈∙›
              and g=‹σ'⦇NTMap⦈⦇𝔎⦇ObjMap⦈⦇b'⦈⦈›
              and q=‹ε⦇NTMap⦈⦇b'⦈›
          ]
      }
      note [cat_Kan_cs_simps] = this εb_𝔊f[symmetric]
      {
        fix a' b' f' A
        note 𝔗.HomCod.cat_assoc_helper
          [
            where h=
              ‹?UArr (𝔎⦇ObjMap⦈⦇b'⦈)⦇NTMap⦈⦇a', b', ℭ⦇CId⦈⦇𝔎⦇ObjMap⦈⦇b'⦈⦈⦈∙›
            and g=‹σ⦇NTMap⦈⦇𝔎⦇ObjMap⦈⦇b'⦈⦈›
            and q=‹ε⦇NTMap⦈⦇b'⦈›
          ]
      }
      note [cat_Kan_cs_simps] = this

      show "σ' = σ"
      proof(rule ntcf_eqI)

        show "σ' : 𝔊 ↦CF ?the_cf_rKe : ℭ ↦↦C⇘α⇙ 𝔄" by (rule prems'(1))
        show "σ : 𝔊 ↦CF ?the_cf_rKe : ℭ ↦↦C⇘α⇙ 𝔄" by (rule σ)

        have dom_lhs: "𝒟∘ (σ⦇NTMap⦈) = ℭ⦇Obj⦈" 
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)
        have dom_rhs: "𝒟∘ (σ'⦇NTMap⦈) = ℭ⦇Obj⦈"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)

        show "σ'⦇NTMap⦈ = σ⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)

          fix c assume prems': "c ∈∘ ℭ⦇Obj⦈"

          note lim_c = assms(3)[OF prems']
          interpret lim_c: is_cat_limit 
            α ‹c ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF c O⨅CF 𝔎› ‹?UObj c› ‹?UArr c›
            by (rule lim_c)
          from prems' have CId_c: "ℭ⦇CId⦈⦇c⦈ : c ↦⇘ℭ⇙ c"
            by (cs_concl cs_shallow cs_intro: cat_cs_intros)

          from lim_c.cat_lim_unique_cone'[OF τ[OF CId_c]] obtain f 
            where f: "f : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c"
              and "⋀A. A ∈∘ c ↓CF 𝔎⦇Obj⦈ ⟹
                τ c c (ℭ⦇CId⦈⦇c⦈)⦇NTMap⦈⦇A⦈ = ?UArr c⦇NTMap⦈⦇A⦈ ∘A⇘𝔄⇙ f"
              and f_unique: "⋀f'.
                ⟦
                  f' : 𝔊⦇ObjMap⦈⦇c⦈ ↦⇘𝔄⇙ ?UObj c;
                  ⋀A. A ∈∘ c ↓CF 𝔎⦇Obj⦈ ⟹
                    τ c c (ℭ⦇CId⦈⦇c⦈)⦇NTMap⦈⦇A⦈ = ?UArr c⦇NTMap⦈⦇A⦈ ∘A⇘𝔄⇙ f'
                ⟧ ⟹ f' = f"
            by metis

          note [symmetric, cat_cs_simps] =
            σ.ntcf_Comp_commute
            σ'.ntcf_Comp_commute

          show "σ'⦇NTMap⦈⦇c⦈ = σ⦇NTMap⦈⦇c⦈"
          proof(rule trans_sym[where s=f])

            show "σ'⦇NTMap⦈⦇c⦈ = f"
            proof(rule f_unique)

              fix A assume prems'': "A ∈∘ c ↓CF 𝔎⦇Obj⦈"

              with prems' obtain b' f' 
                where A_def: "A = [0, b', f']∘"
                  and b': "b' ∈∘ 𝔅⦇Obj⦈"
                  and f': "f' : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
                by auto

              let ?𝔎b' = ‹𝔎⦇ObjMap⦈⦇b'⦈›

              from b' have 𝔎b': "?𝔎b' ∈∘ ℭ⦇Obj⦈"
                by (cs_concl cs_shallow cs_intro: cat_cs_intros)

              interpret lim_𝔎b': is_cat_limit
                α ‹?𝔎b' ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF ?𝔎b' O⨅CF 𝔎› ‹?UObj ?𝔎b'› ‹?UArr ?𝔎b'›
                by (rule assms(3)[OF 𝔎b'])

              from 𝔎b' have CId_𝔎b': "ℭ⦇CId⦈⦇?𝔎b'⦈ : ?𝔎b' ↦⇘ℭ⇙ ?𝔎b'"
                by (cs_concl cs_intro: cat_cs_intros)
              from CId_𝔎b' b' have a'_b'_CId_𝔎b':
                "[0, b', ℭ⦇CId⦈⦇?𝔎b'⦈]∘ ∈∘ ?𝔎b' ↓CF 𝔎⦇Obj⦈"
                by
                  (
                    cs_concl cs_shallow
                      cs_simp: cat_cs_simps cat_comma_cs_simps
                      cs_intro: cat_cs_intros cat_comma_cs_intros
                  )
              from 
                lim_Obj_the_cf_rKe_commute[
                  where lim_Obj=lim_Obj, 
                  OF assms(1,2) lim_c assms(3)[OF 𝔎b'] f' a'_b'_CId_𝔎b'
                  ]
                f'
              have [cat_Kan_cs_simps]:
                "?UArr c⦇NTMap⦈⦇0, b', f'⦈∙ =
                  ?UArr ?𝔎b'⦇NTMap⦈⦇0, b', ℭ⦇CId⦈⦇?𝔎b'⦈⦈∙ ∘A⇘𝔄⇙ 
                    ?the_cf_rKe⦇ArrMap⦈⦇f'⦈"
                by (cs_prems cs_shallow cs_simp: cat_cs_simps)

              from prems' prems'' b' f' show
                "τ c c (ℭ⦇CId⦈⦇c⦈)⦇NTMap⦈⦇A⦈ = ?UArr c⦇NTMap⦈⦇A⦈ ∘A⇘𝔄⇙ σ'⦇NTMap⦈⦇c⦈"
                unfolding A_def (*very slow*)
                by
                  (
                    cs_concl 
                      cs_simp:
                        cat_cs_simps cat_comma_cs_simps cat_Kan_cs_simps
                      cs_intro:
                        cat_lim_cs_intros 
                        cat_cs_intros 
                        cat_comma_cs_intros   
                        cat_Kan_cs_intros
                  )
            qed
              (
                use prems' in
                  ‹
                    cs_concl cs_shallow 
                      cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros
                  ›
              )

            show "σ⦇NTMap⦈⦇c⦈ = f"
            proof(rule f_unique)
              fix A assume prems'': "A ∈∘ c ↓CF 𝔎⦇Obj⦈"
              from this prems' obtain b' f' 
                where A_def: "A = [0, b', f']∘"
                  and b': "b' ∈∘ 𝔅⦇Obj⦈"
                  and f': "f' : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
                by auto
              let ?𝔎b' = ‹𝔎⦇ObjMap⦈⦇b'⦈›
              from b' have 𝔎b': "?𝔎b' ∈∘ ℭ⦇Obj⦈"
                by (cs_concl cs_shallow cs_intro: cat_cs_intros)
              interpret lim_𝔎b': is_cat_limit
                α ‹?𝔎b' ↓CF 𝔎› 𝔄 ‹𝔗 ∘CF ?𝔎b' O⨅CF 𝔎› ‹?UObj ?𝔎b'› ‹?UArr ?𝔎b'›
                by (rule assms(3)[OF 𝔎b'])
              from 𝔎b' have CId_𝔎b': "ℭ⦇CId⦈⦇?𝔎b'⦈ : ?𝔎b' ↦⇘ℭ⇙ ?𝔎b'"
                by (cs_concl cs_intro: cat_cs_intros)
              from CId_𝔎b' b' have a'_b'_CId_𝔎b': 
                "[0, b', ℭ⦇CId⦈⦇?𝔎b'⦈]∘ ∈∘ ?𝔎b' ↓CF 𝔎⦇Obj⦈"
                by
                  (
                    cs_concl cs_shallow
                      cs_simp: cat_cs_simps cat_comma_cs_simps
                      cs_intro: cat_cs_intros cat_comma_cs_intros
                  )

              from 
                lim_Obj_the_cf_rKe_commute
                  [
                    where lim_Obj=lim_Obj, 
                    OF assms(1,2) lim_c assms(3)[OF 𝔎b'] f' a'_b'_CId_𝔎b'
                  ]
                f'
              have [cat_Kan_cs_simps]:
                "?UArr c⦇NTMap⦈⦇0, b', f'⦈∙ =
                  ?UArr (?𝔎b')⦇NTMap⦈⦇0, b', ℭ⦇CId⦈⦇?𝔎b'⦈⦈∙ ∘A⇘𝔄⇙
                    ?the_cf_rKe⦇ArrMap⦈⦇f'⦈"
                by (cs_prems cs_shallow cs_simp: cat_cs_simps)
              from prems' prems'' b' f' show
                "τ c c (ℭ⦇CId⦈⦇c⦈)⦇NTMap⦈⦇A⦈ = ?UArr c⦇NTMap⦈⦇A⦈ ∘A⇘𝔄⇙ σ⦇NTMap⦈⦇c⦈"
                unfolding A_def (*very slow*)
                by
                  (
                    cs_concl 
                      cs_simp:
                        cat_cs_simps cat_comma_cs_simps cat_Kan_cs_simps 
                      cs_intro:
                        cat_lim_cs_intros
                        cat_cs_intros
                        cat_comma_cs_intros
                        cat_Kan_cs_intros
                  )
            qed
              (
                use prems' in
                  ‹
                    cs_concl cs_shallow
                      cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros
                  ›
              )
          qed

        qed auto

      qed simp_all

    qed

  qed (cs_concl cs_shallow cs_intro: cat_cs_intros)+

qed

lemma the_ntcf_lKe_is_cat_lKe:
  assumes "𝔎 : 𝔅 ↦↦C⇘α⇙ ℭ" 
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ lim_Obj c⦇UArr⦈ :
      𝔗 ∘CF 𝔎 CF⨅O c >CF.colim lim_Obj c⦇UObj⦈ : 𝔎 CF↓ c ↦↦C⇘α⇙ 𝔄"
  shows "the_ntcf_lKe α 𝔗 𝔎 lim_Obj :
    𝔗 ↦CF.lKe⇘α⇙ the_cf_lKe α 𝔗 𝔎 lim_Obj ∘CF 𝔎 : 𝔅 ↦C ℭ ↦C 𝔄"
proof-
  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
  {
    fix c assume prems: "c ∈∘ ℭ⦇Obj⦈"
    from assms(3)[OF this] have lim_Obj_UArr: "lim_Obj c⦇UArr⦈ :
      𝔗 ∘CF 𝔎 CF⨅O c >CF.colim lim_Obj c⦇UObj⦈ : 𝔎 CF↓ c ↦↦C⇘α⇙ 𝔄". 
    then interpret lim_Obj_c: is_cat_colimit 
      α ‹𝔎 CF↓ c› 𝔄 ‹𝔗 ∘CF 𝔎 CF⨅O c› ‹lim_Obj c⦇UObj⦈› ‹lim_Obj c⦇UArr⦈›
      by simp
    note op_ua_UArr_is_cat_limit'[
      where lim_Obj=lim_Obj, OF assms(1,2) prems lim_Obj_UArr
      ]
  }
  note the_ntcf_rKe_is_cat_rKe = the_ntcf_rKe_is_cat_rKe
    [
      OF 𝔎.is_functor_op 𝔗.is_functor_op,
      unfolded cat_op_simps,
      where lim_Obj=‹op_ua lim_Obj 𝔎›,
      unfolded cat_op_simps,
      OF this,
      simplified,
      folded the_cf_lKe_def the_ntcf_lKe_def
    ]
  show ?thesis
    by 
      (
        rule is_cat_rKe.is_cat_lKe_op
          [
            OF the_ntcf_rKe_is_cat_rKe, 
            unfolded cat_op_simps, 
            folded the_cf_lKe_def the_ntcf_lKe_def
          ]
      )
qed



subsection‹Preservation of Kan extensions›


text‹
The following definitions are similar to the definitions that can be 
found in cite‹"riehl_category_2016"› or cite‹"lehner_all_2014"›.
›

locale is_cat_rKe_preserves =
  is_cat_rKe α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔊 ε + is_functor α 𝔄 𝔇 ℌ
  for α 𝔅 ℭ 𝔄 𝔇 𝔎 𝔗 𝔊 ℌ ε +
  assumes cat_rKe_preserves:
    "ℌ ∘CF-NTCF ε : (ℌ ∘CF 𝔊) ∘CF 𝔎 ↦CF.rKe⇘α⇙ ℌ ∘CF 𝔗 : 𝔅 ↦C ℭ ↦C 𝔇"

syntax "_is_cat_rKe_preserves" :: 
  "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (
    ‹(_ :/ _ ∘CF _ ↦CF.rKeı _ :/ _ ↦C _ ↦C _ : _ ↦↦C _)› 
    [51, 51, 51, 51, 51, 51, 51, 51, 51] 51
  )
translations "ε : 𝔊 ∘CF 𝔎 ↦CF.rKe⇘α⇙ 𝔗 : 𝔅 ↦C ℭ ↦C (ℌ : 𝔄 ↦↦C 𝔇)" ⇌ 
  "CONST is_cat_rKe_preserves α 𝔅 ℭ 𝔄 𝔇 𝔎 𝔗 𝔊 ℌ ε"

locale is_cat_lKe_preserves =
  is_cat_lKe α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔉 η + is_functor α 𝔄 𝔇 ℌ
  for α 𝔅 ℭ 𝔄 𝔇 𝔎 𝔗 𝔉 ℌ η +
  assumes cat_lKe_preserves:
    "ℌ ∘CF-NTCF η : ℌ ∘CF 𝔗 ↦CF.lKe⇘α⇙ (ℌ ∘CF 𝔉) ∘CF 𝔎 : 𝔅 ↦C ℭ ↦C 𝔇"

syntax "_is_cat_lKe_preserves" :: 
  "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (
    ‹(_ :/ _ ↦CF.lKeı _ ∘CF _ :/ _ ↦C _ ↦C _ : _ ↦↦C _)› 
    [51, 51, 51, 51, 51, 51, 51, 51, 51] 51
  )
translations "η : 𝔗 ↦CF.lKe⇘α⇙ 𝔉 ∘CF 𝔎 : 𝔅 ↦C ℭ ↦C (ℌ : 𝔄 ↦↦C 𝔇)" ⇌
  "CONST is_cat_lKe_preserves α 𝔅 ℭ 𝔄 𝔇 𝔎 𝔗 𝔉 ℌ η"


text‹Rules.›

lemma (in is_cat_rKe_preserves) is_cat_rKe_preserves_axioms':
  assumes "α' = α"
    and "𝔊' = 𝔊"
    and "𝔎' = 𝔎"
    and "𝔗' = 𝔗"
    and "ℌ' = ℌ"
    and "𝔅' = 𝔅"
    and "𝔄' = 𝔄"
    and "ℭ' = ℭ"
    and "𝔇' = 𝔇"
  shows "ε : 𝔊' ∘CF 𝔎' ↦CF.rKe⇘α'⇙ 𝔗' : 𝔅' ↦C ℭ' ↦C (ℌ' : 𝔄' ↦↦C 𝔇')"
  unfolding assms by (rule is_cat_rKe_preserves_axioms)

mk_ide rf is_cat_rKe_preserves_def[unfolded is_cat_rKe_preserves_axioms_def]
  |intro is_cat_rKe_preservesI|
  |dest is_cat_rKe_preservesD[dest]|
  |elim is_cat_rKe_preservesE[elim]|

lemmas [cat_Kan_cs_intros] = is_cat_rKeD(1-3)

lemma (in is_cat_lKe_preserves) is_cat_lKe_preserves_axioms':
  assumes "α' = α"
    and "𝔉' = 𝔉"
    and "𝔎' = 𝔎"
    and "𝔗' = 𝔗"
    and "ℌ' = ℌ"
    and "𝔅' = 𝔅"
    and "𝔄' = 𝔄"
    and "ℭ' = ℭ"
    and "𝔇' = 𝔇"
  shows "η : 𝔗' ↦CF.lKe⇘α⇙ 𝔉' ∘CF 𝔎' : 𝔅' ↦C ℭ' ↦C (ℌ' : 𝔄' ↦↦C 𝔇')"
  unfolding assms by (rule is_cat_lKe_preserves_axioms)

mk_ide rf is_cat_lKe_preserves_def[unfolded is_cat_lKe_preserves_axioms_def]
  |intro is_cat_lKe_preservesI|
  |dest is_cat_lKe_preservesD[dest]|
  |elim is_cat_lKe_preservesE[elim]|

lemmas [cat_Kan_cs_intros] = is_cat_lKe_preservesD(1-3)


text‹Duality.›

lemma (in is_cat_rKe_preserves) is_cat_rKe_preserves_op:
  "op_ntcf ε :
    op_cf 𝔗 ↦CF.lKe⇘α⇙ op_cf 𝔊 ∘CF op_cf 𝔎 :
    op_cat 𝔅 ↦C op_cat ℭ ↦C (op_cf ℌ : op_cat 𝔄 ↦↦C op_cat 𝔇)"
proof(intro is_cat_lKe_preservesI)
  from cat_rKe_preserves show "op_cf ℌ ∘CF-NTCF op_ntcf ε :
    op_cf ℌ ∘CF op_cf 𝔗 ↦CF.lKe⇘α⇙ (op_cf ℌ ∘CF op_cf 𝔊) ∘CF op_cf 𝔎 :
    op_cat 𝔅 ↦C op_cat ℭ ↦C op_cat 𝔇"
    by (cs_concl_step op_ntcf_cf_ntcf_comp[symmetric])
      (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
qed (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)+

lemma (in is_cat_rKe_preserves) is_cat_lKe_preserves_op'[cat_op_intros]:
  assumes "𝔗' = op_cf 𝔗"
    and "𝔊' = op_cf 𝔊"
    and "𝔎' = op_cf 𝔎"
    and "𝔅' = op_cat 𝔅"
    and "𝔄' = op_cat 𝔄"
    and "ℭ' = op_cat ℭ"
    and "𝔇' = op_cat 𝔇"
    and "ℌ' = op_cf ℌ"
  shows "op_ntcf ε :
    𝔗' ↦CF.lKe⇘α⇙ 𝔊' ∘CF 𝔎' : 𝔅' ↦C ℭ' ↦C (ℌ' : 𝔄' ↦↦C 𝔇')"
  unfolding assms by (rule is_cat_rKe_preserves_op)

lemmas [cat_op_intros] = is_cat_rKe_preserves.is_cat_lKe_preserves_op'

lemma (in is_cat_lKe_preserves) is_cat_rKe_preserves_op:
  "op_ntcf η :
    op_cf 𝔉 ∘CF op_cf 𝔎 ↦CF.rKe⇘α⇙ op_cf 𝔗 :
    op_cat 𝔅 ↦C op_cat ℭ ↦C (op_cf ℌ : op_cat 𝔄 ↦↦C op_cat 𝔇)"
proof(intro is_cat_rKe_preservesI)
  from cat_lKe_preserves show "op_cf ℌ ∘CF-NTCF op_ntcf η :
    (op_cf ℌ ∘CF op_cf 𝔉) ∘CF op_cf 𝔎 ↦CF.rKe⇘α⇙ op_cf ℌ ∘CF op_cf 𝔗 :
    op_cat 𝔅 ↦C op_cat ℭ ↦C op_cat 𝔇"
    by (cs_concl_step op_ntcf_cf_ntcf_comp[symmetric])
      (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
qed (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)+

lemma (in is_cat_lKe_preserves) is_cat_rKe_preserves_op'[cat_op_intros]:
  assumes "𝔗' = op_cf 𝔗"
    and "𝔉' = op_cf 𝔉"
    and "𝔎' = op_cf 𝔎"
    and "ℌ' = op_cf ℌ"
    and "𝔅' = op_cat 𝔅"
    and "𝔄' = op_cat 𝔄"
    and "ℭ' = op_cat ℭ"
    and "𝔇' = op_cat 𝔇"
  shows "op_ntcf η :
    𝔉' ∘CF 𝔎' ↦CF.rKe⇘α⇙ 𝔗' : 𝔅' ↦C ℭ' ↦C (ℌ' : 𝔄' ↦↦C 𝔇')"
  unfolding assms by (rule is_cat_rKe_preserves_op)



subsection‹All concepts are Kan extensions›


text‹
Background information for this subsection is provided in 
Chapter X-7 in cite‹"mac_lane_categories_2010"›
and subsection 6.5 in cite‹"riehl_category_2016"›. 
It should be noted that only the connections between the Kan extensions,
limits and adjunctions are exposed (an alternative proof of the Yoneda
lemma using Kan extensions is not provided in the context of this work).
›


subsubsection‹Limits and colimits›

lemma cat_rKe_is_cat_limit:
  ―‹The statement of the theorem is similar to the statement of a part of
    Theorem 1 in Chapter X-7 in \cite{mac_lane_categories_2010}
    or Proposition 6.5.1 in \cite{riehl_category_2016}.›
  assumes "ε : 𝔊 ∘CF 𝔎 ↦CF.rKe⇘α⇙ 𝔗 : 𝔅 ↦C cat_1 𝔞 𝔣 ↦C 𝔄"
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
  shows "ε : 𝔊⦇ObjMap⦈⦇𝔞⦈ <CF.lim 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
proof-

  interpret ε: is_cat_rKe α 𝔅 ‹cat_1 𝔞 𝔣› 𝔄 𝔎 𝔗 𝔊 ε by (rule assms(1))  
  interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
  
  from cat_1_components(1) have 𝔞: "𝔞 ∈∘ Vset α" 
    by (auto simp: ε.AG.HomCod.cat_in_Obj_in_Vset)
  from cat_1_components(2) have 𝔣: "𝔣 ∈∘ Vset α" 
    by (auto simp: ε.AG.HomCod.cat_in_Arr_in_Vset)

  have 𝔎_def: "𝔎 = cf_const 𝔅 (cat_1 𝔞 𝔣) 𝔞"
    by (rule cf_const_if_HomCod_is_cat_1) 
      (cs_concl cs_shallow cs_intro: cat_cs_intros)
  have 𝔊𝔎_def: "𝔊 ∘CF 𝔎 = cf_const 𝔅 𝔄 (𝔊⦇ObjMap⦈⦇𝔞⦈)"
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_1_components(1) 𝔎_def cat_cs_simps 
          cs_intro: V_cs_intros cat_cs_intros
      )

  interpret ε: is_ntcf α 𝔅 𝔄 ‹𝔊 ∘CF 𝔎› 𝔗 ε 
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

  show "ε : 𝔊⦇ObjMap⦈⦇𝔞⦈ <CF.lim 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
  proof(intro is_cat_limitI is_cat_coneI)

    show "ε : cf_const 𝔅 𝔄 (𝔊⦇ObjMap⦈⦇𝔞⦈) ↦CF 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
      by (rule ε.ntcf_rKe.is_ntcf_axioms[unfolded 𝔊𝔎_def])

    fix u' r' assume prems: "u' : r' <CF.cone 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"

    interpret u': is_cat_cone α r' 𝔅 𝔄 𝔗 u' by (rule prems)

    have 𝔊_def: "𝔊 = cf_const (cat_1 𝔞 𝔣) 𝔄 (𝔊⦇ObjMap⦈⦇𝔞⦈)"
      by (rule cf_const_if_HomDom_is_cat_1[OF ε.Ran.is_functor_axioms])

    from prems have const_r': "cf_const (cat_1 𝔞 𝔣) 𝔄 r' : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps cs_intro: cat_lim_cs_intros cat_cs_intros
        )

    have cf_comp_cf_const_r_𝔎_def: 
      "cf_const (cat_1 𝔞 𝔣) 𝔄 r' ∘CF 𝔎 = cf_const 𝔅 𝔄 r'"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps 𝔎_def
            cs_intro: cat_cs_intros cat_lim_cs_intros
        )

    from ε.cat_rKe_unique[
        OF const_r', unfolded cf_comp_cf_const_r_𝔎_def, OF u'.is_ntcf_axioms
        ] 
    obtain σ 
      where σ: "σ : cf_const (cat_1 𝔞 𝔣) 𝔄 r' ↦CF 𝔊 : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄"
        and u'_def: "u' = ε ∙NTCF (σ ∘NTCF-CF 𝔎)"
        and unique_σ: "⋀σ'.
          ⟦
            σ' : cf_const (cat_1 𝔞 𝔣) 𝔄 r' ↦CF 𝔊 : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄;
            u' = ε ∙NTCF (σ' ∘NTCF-CF 𝔎)
          ⟧ ⟹ σ' = σ"
      by auto

    interpret σ: is_ntcf α ‹cat_1 𝔞 𝔣› 𝔄 ‹cf_const (cat_1 𝔞 𝔣) 𝔄 r'› 𝔊 σ
      by (rule σ)
    
    show "∃!f'. f' : r' ↦⇘𝔄⇙ 𝔊⦇ObjMap⦈⦇𝔞⦈ ∧ u' = ε ∙NTCF ntcf_const 𝔅 𝔄 f'"
    proof(intro ex1I conjI; (elim conjE)?)
      fix f' assume prems': 
        "f' : r' ↦⇘𝔄⇙ 𝔊⦇ObjMap⦈⦇𝔞⦈" "u' = ε ∙NTCF ntcf_const 𝔅 𝔄 f'"
      from prems'(1) have "ntcf_const (cat_1 𝔞 𝔣) 𝔄 f' :
        cf_const (cat_1 𝔞 𝔣) 𝔄 r' ↦CF 𝔊 : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄"
        by (subst 𝔊_def) 
          (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      moreover with prems'(1) have "u' = ε ∙NTCF (ntcf_const (cat_1 𝔞 𝔣) 𝔄 f' ∘NTCF-CF 𝔎)"
        by 
          (
            cs_concl 
              cs_simp: cat_cs_simps prems'(2) 𝔎_def cs_intro: cat_cs_intros
          )
      ultimately have σ_def: "σ = ntcf_const (cat_1 𝔞 𝔣) 𝔄 f'"
        by (auto simp: unique_σ[symmetric])
      show "f' = σ⦇NTMap⦈⦇𝔞⦈"
        by (cs_concl cs_simp: cat_cs_simps σ_def cs_intro: cat_cs_intros)
    qed (cs_concl cs_simp: cat_cs_simps u'_def 𝔎_def cs_intro: cat_cs_intros)+

  qed (cs_concl cs_simp: 𝔎_def cs_intro: cat_cs_intros)

qed

lemma cat_lKe_is_cat_colimit:
  assumes "η : 𝔗 ↦CF.lKe⇘α⇙ 𝔉 ∘CF 𝔎 : 𝔅 ↦C cat_1 𝔞 𝔣 ↦C 𝔄"
    and "𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
  shows "η : 𝔗 >CF.colim 𝔉⦇ObjMap⦈⦇𝔞⦈ : 𝔅 ↦↦C⇘α⇙ 𝔄"
proof-
  interpret η: is_cat_lKe α 𝔅 ‹cat_1 𝔞 𝔣› 𝔄 𝔎 𝔗 𝔉 η by (rule assms(1))
  from cat_1_components(1) have 𝔞: "𝔞 ∈∘ Vset α" 
    by (auto simp: η.AG.HomCod.cat_in_Obj_in_Vset)
  from cat_1_components(2) have 𝔣: "𝔣 ∈∘ Vset α" 
    by (auto simp: η.AG.HomCod.cat_in_Arr_in_Vset)
  show ?thesis
    by 
      (
        rule is_cat_limit.is_cat_colimit_op
          [
            OF cat_rKe_is_cat_limit[
              OF 
                η.is_cat_rKe_op[unfolded η.AG.cat_1_op[OF 𝔞 𝔣]] 
                η.ntcf_lKe.NTDom.is_functor_op
              ], 
            unfolded cat_op_simps
          ]
      )
qed

lemma cat_limit_is_rKe:
  ―‹The statement of the theorem is similar to the statement of a part of
    Theorem 1 in Chapter X-7 in \cite{mac_lane_categories_2010} 
    or Proposition 6.5.1 in \cite{riehl_category_2016}.›
  assumes "ε : 𝔊⦇ObjMap⦈⦇𝔞⦈ <CF.lim 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "𝔎 : 𝔅 ↦↦C⇘α⇙ cat_1 𝔞 𝔣"
    and "𝔊 : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄"
  shows "ε : 𝔊 ∘CF 𝔎 ↦CF.rKe⇘α⇙ 𝔗 : 𝔅 ↦C cat_1 𝔞 𝔣 ↦C 𝔄"
proof-

  interpret ε: is_cat_limit α 𝔅 𝔄 𝔗 ‹𝔊⦇ObjMap⦈⦇𝔞⦈› ε by (rule assms)
  interpret 𝔎: is_functor α 𝔅 ‹cat_1 𝔞 𝔣› 𝔎 by (rule assms(2))
  interpret 𝔊: is_functor α ‹cat_1 𝔞 𝔣› 𝔄 𝔊 by (rule assms(3))

  show ?thesis
  proof(rule is_cat_rKeI')

    note 𝔎_def = cf_const_if_HomCod_is_cat_1[OF assms(2)]
    note 𝔊_def = cf_const_if_HomDom_is_cat_1[OF assms(3)]

    have 𝔊𝔎_def: "𝔊 ∘CF 𝔎 = cf_const 𝔅 𝔄 (𝔊⦇ObjMap⦈⦇𝔞⦈)"
      by (subst 𝔎_def, use nothing in ‹subst 𝔊_def›)
        (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

    show "ε : 𝔊 ∘CF 𝔎 ↦CF 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄" 
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps 𝔊𝔎_def cs_intro: cat_cs_intros
        )

    fix 𝔊' ε' assume prems: 
      "𝔊' : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄"
      "ε' : 𝔊' ∘CF 𝔎 ↦CF 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"

    interpret is_functor α ‹cat_1 𝔞 𝔣› 𝔄 𝔊' by (rule prems(1))
  
    note 𝔊'_def = cf_const_if_HomDom_is_cat_1[OF prems(1)]

    from prems(2) have ε': 
      "ε' : cf_const 𝔅 𝔄 (𝔊'⦇ObjMap⦈⦇𝔞⦈) ↦CF 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
      unfolding 𝔎_def 
      by (subst (asm) 𝔊'_def)
        (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from prems(2) have "ε' : 𝔊'⦇ObjMap⦈⦇𝔞⦈ <CF.cone 𝔗 : 𝔅 ↦↦C⇘α⇙ 𝔄"
      by (intro is_cat_coneI ε') (cs_concl cs_intro: cat_cs_intros)+

    from ε.cat_lim_ua_fo[OF this] obtain f'
      where f': "f' : 𝔊'⦇ObjMap⦈⦇𝔞⦈ ↦⇘𝔄⇙ 𝔊⦇ObjMap⦈⦇𝔞⦈"
        and ε_def: "ε' = ε ∙NTCF ntcf_const 𝔅 𝔄 f'"
        and unique_f':
          "⟦
            f'' : 𝔊'⦇ObjMap⦈⦇𝔞⦈ ↦⇘𝔄⇙ 𝔊⦇ObjMap⦈⦇𝔞⦈;
            ε' = ε ∙NTCF ntcf_const 𝔅 𝔄 f''
          ⟧ ⟹ f'' = f'"
        for f''
      by metis

    show "∃!σ.
      σ : 𝔊' ↦CF 𝔊 : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄 ∧ ε' = ε ∙NTCF (σ ∘NTCF-CF 𝔎)"
    proof(intro ex1I conjI; (elim conjE)?)  
      from f' show 
        "ntcf_const (cat_1 𝔞 𝔣) 𝔄 f' : 𝔊' ↦CF 𝔊 : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄"
        by (subst 𝔊'_def, use nothing in ‹subst 𝔊_def›) 
          (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      with f' show "ε' = ε ∙NTCF (ntcf_const (cat_1 𝔞 𝔣) 𝔄 f' ∘NTCF-CF 𝔎)"
        by (cs_concl cs_simp: cat_cs_simps ε_def 𝔎_def cs_intro: cat_cs_intros)
      fix σ assume prems:
        "σ : 𝔊' ↦CF 𝔊 : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄"
        "ε' = ε ∙NTCF (σ ∘NTCF-CF 𝔎)"
      interpret σ: is_ntcf α ‹cat_1 𝔞 𝔣› 𝔄 𝔊' 𝔊 σ by (rule prems(1))
      have "σ⦇NTMap⦈⦇𝔞⦈ : 𝔊'⦇ObjMap⦈⦇𝔞⦈ ↦⇘𝔄⇙ 𝔊⦇ObjMap⦈⦇𝔞⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      moreover have "ε' = ε ∙NTCF ntcf_const 𝔅 𝔄 (σ⦇NTMap⦈⦇𝔞⦈)"
        by
          (
            cs_concl 
              cs_simp: cat_cs_simps prems(2) 𝔎_def cs_intro: cat_cs_intros
          )
      ultimately have σ𝔞: "σ⦇NTMap⦈⦇𝔞⦈ = f'" by (rule unique_f')
      show "σ = ntcf_const (cat_1 𝔞 𝔣) 𝔄 f'"
      proof(rule ntcf_eqI)
        from f' show 
          "ntcf_const (cat_1 𝔞 𝔣) 𝔄 f' : 𝔊' ↦CF 𝔊 : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄"
          by (subst 𝔊'_def, use nothing in ‹subst 𝔊_def›)
            (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        have dom_lhs: "𝒟∘ (σ⦇NTMap⦈) = cat_1 𝔞 𝔣⦇Obj⦈"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro:cat_cs_intros)
        have dom_rhs: "𝒟∘ (ntcf_const (cat_1 𝔞 𝔣) 𝔄 f'⦇NTMap⦈) = cat_1 𝔞 𝔣⦇Obj⦈"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro:cat_cs_intros)
        show "σ⦇NTMap⦈ = ntcf_const (cat_1 𝔞 𝔣) 𝔄 f'⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix a assume prems: "a ∈∘ cat_1 𝔞 𝔣⦇Obj⦈"
          then have a_def: "a = 𝔞" unfolding cat_1_components by simp
          from f' show "σ⦇NTMap⦈⦇a⦈ = ntcf_const (cat_1 𝔞 𝔣) 𝔄 f'⦇NTMap⦈⦇a⦈"
            unfolding a_def σ𝔞
            by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        qed (auto intro: cat_cs_intros)
      qed (simp_all add: prems)
    qed

  qed (auto simp: assms)

qed

lemma cat_colimit_is_lKe:
  assumes "η : 𝔗 >CF.colim 𝔉⦇ObjMap⦈⦇𝔞⦈ : 𝔅 ↦↦C⇘α⇙ 𝔄"
    and "𝔎 : 𝔅 ↦↦C⇘α⇙ cat_1 𝔞 𝔣"
    and "𝔉 : cat_1 𝔞 𝔣 ↦↦C⇘α⇙ 𝔄"
  shows "η : 𝔗 ↦CF.lKe⇘α⇙ 𝔉 ∘CF 𝔎 : 𝔅 ↦C cat_1 𝔞 𝔣 ↦C 𝔄"
proof-
  interpret η: is_cat_colimit α 𝔅 𝔄 𝔗 ‹𝔉⦇ObjMap⦈⦇𝔞⦈› η
    by (rule assms(1))
  interpret 𝔎: is_functor α 𝔅 ‹cat_1 𝔞 𝔣› 𝔎 by (rule assms(2))
  interpret 𝔉: is_functor α ‹cat_1 𝔞 𝔣› 𝔄 𝔉 by (rule assms(3))
  from cat_1_components(1) have 𝔞: "𝔞 ∈∘ Vset α"
    by (auto simp: 𝔎.HomCod.cat_in_Obj_in_Vset)
  from cat_1_components(2) have 𝔣: "𝔣 ∈∘ Vset α" 
    by (auto simp: 𝔎.HomCod.cat_in_Arr_in_Vset)
  have 𝔉𝔞: "𝔉⦇ObjMap⦈⦇𝔞⦈ = op_cf 𝔉⦇ObjMap⦈⦇𝔞⦈" unfolding cat_op_simps by simp
  note cat_1_op = η.cat_1_op[OF 𝔞 𝔣]
  show ?thesis
    by 
      (
        rule is_cat_rKe.is_cat_lKe_op
          [
            OF cat_limit_is_rKe
              [
                OF 
                  η.is_cat_limit_op[unfolded 𝔉𝔞]
                  𝔎.is_functor_op[unfolded cat_1_op]
                  𝔉.is_functor_op[unfolded cat_1_op]
              ],
            unfolded cat_op_simps cat_1_op
          ]
      )
qed


subsubsection‹Adjoints›

lemma (in is_cf_adjunction) cf_adjunction_counit_is_rKe:
  ―‹The statement of the theorem is similar to the statement of a part of
    Theorem 2 in Chapter X-7 in \cite{mac_lane_categories_2010}
    or Proposition 6.5.2 in \cite{riehl_category_2016}.
    The proof follows (approximately) the proof in \cite{riehl_category_2016}.›
  shows "εC Φ : 𝔉 ∘CF 𝔊 ↦CF.rKe⇘α⇙ cf_id 𝔇 : 𝔇 ↦C ℭ ↦C 𝔇"
proof-

  define β where "β = α + ω"
  have β: "𝒵 β" and αβ: "α ∈∘ β" 
    by (simp_all add: β_def 𝒵_Limit_αω 𝒵_ω_αω 𝒵_def 𝒵_α_αω)
  then interpret β: 𝒵 β by simp

  note exp_adj = cf_adj_exp_cf_cat_exp_cf_cat[OF β αβ R.category_axioms]

  let ?η = ‹ηC Φ›
  let ?ε = ‹εC Φ›
  let ?𝔇η = ‹exp_cat_ntcf α 𝔇 ?η›
  let ?𝔇𝔉 = ‹exp_cat_cf α 𝔇 𝔉›
  let ?𝔇𝔊 = ‹exp_cat_cf α 𝔇 𝔊›
  let ?𝔇𝔇 = ‹cat_FUNCT α 𝔇 𝔇›
  let ?ℭ𝔇 = ‹cat_FUNCT α ℭ 𝔇›
  let ?adj_𝔇η = ‹cf_adjunction_of_unit β ?𝔇𝔊 ?𝔇𝔉 ?𝔇η›

  interpret 𝔇η: is_cf_adjunction β ?ℭ𝔇 ?𝔇𝔇 ?𝔇𝔊 ?𝔇𝔉 ?adj_𝔇η by (rule exp_adj)

  show ?thesis
  proof(intro is_cat_rKeI)
    have id_𝔇: "cf_map (cf_id 𝔇) ∈∘ cat_FUNCT α 𝔇 𝔇⦇Obj⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_FUNCT_components(1)
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    then have exp_id_𝔇: 
      "exp_cat_cf α 𝔇 𝔉⦇ObjMap⦈⦇cf_map (cf_id 𝔇)⦈ = cf_map 𝔉"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps cs_intro: cat_cs_intros
        )
    have 𝔉: "cf_map 𝔉 ∈∘ cat_FUNCT α ℭ 𝔇⦇Obj⦈"
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_FUNCT_components(1)
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    have ε: "ntcf_arrow (εC Φ) ∈∘ ntcf_arrows α 𝔇 𝔇"
      by (cs_concl cs_intro: cat_FUNCT_cs_intros adj_cs_intros)
    have 𝔇𝔇: "category β (cat_FUNCT α 𝔇 𝔇)"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    have ℭ𝔇: "category β (cat_FUNCT α ℭ 𝔇)"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)

    from 
      ε 𝔉 αβ id_𝔇 
      𝔇𝔇 ℭ𝔇 LR.is_functor_axioms RL.is_functor_axioms R.cat_cf_id_is_functor
      NT.is_iso_ntcf_axioms 
    have ε_id_𝔇: "εC ?adj_𝔇η⦇NTMap⦈⦇cf_map (cf_id 𝔇)⦈ = ntcf_arrow ?ε"
      by (*slow*)
        (
          cs_concl 
            cs_simp:
              cat_Set_the_inverse[symmetric]
              cat_op_simps
              cat_cs_simps
              cat_FUNCT_cs_simps
              adj_cs_simps 
            cs_intro:
              𝔇η.NT.iso_ntcf_is_iso_arr''
              cat_op_intros
              adj_cs_intros
              cat_cs_intros
              cat_FUNCT_cs_intros
              cat_prod_cs_intros
        )      
   show "universal_arrow_fo ?𝔇𝔊 (cf_map (cf_id 𝔇)) (cf_map 𝔉) (ntcf_arrow ?ε)"
      by 
        (
          rule is_cf_adjunction.cf_adjunction_counit_component_is_ua_fo[
            OF exp_adj id_𝔇, unfolded exp_id_𝔇 ε_id_𝔇
            ]
        )
  qed (cs_concl cs_intro: cat_cs_intros adj_cs_intros)+

qed

lemma (in is_cf_adjunction) cf_adjunction_unit_is_lKe:
  shows "ηC Φ : cf_id ℭ ↦CF.lKe⇘α⇙ 𝔊 ∘CF 𝔉 : ℭ ↦C 𝔇 ↦C ℭ"
  by 
    (
      rule is_cat_rKe.is_cat_lKe_op
        [
          OF is_cf_adjunction.cf_adjunction_counit_is_rKe
            [
              OF is_cf_adjunction_op,
              folded op_ntcf_cf_adjunction_unit op_cf_cf_id
            ],
          unfolded 
            cat_op_simps ntcf_op_ntcf_op_ntcf[OF cf_adjunction_unit_is_ntcf]
        ]
    )

lemma cf_adjunction_if_lKe_preserves:
  ―‹The statement of the theorem is similar to the statement of a part of
    Theorem 2 in Chapter X-7 in \cite{mac_lane_categories_2010}
    or Proposition 6.5.2 in \cite{riehl_category_2016}.›
  assumes "η : cf_id 𝔇 ↦CF.lKe⇘α⇙ 𝔉 ∘CF 𝔊 : 𝔇 ↦C ℭ ↦C (𝔊 : 𝔇 ↦↦C ℭ)"
  shows "cf_adjunction_of_unit α 𝔊 𝔉 η : 𝔊 ⇌CF 𝔉 : 𝔇 ⇌⇌C⇘α⇙ ℭ"
proof-

  interpret η: is_cat_lKe_preserves α 𝔇 ℭ 𝔇 ℭ 𝔊 ‹cf_id 𝔇› 𝔉 𝔊 η 
    by (rule assms)

  from η.cat_lKe_preserves interpret 𝔊η:
    is_cat_lKe α 𝔇 ℭ ℭ 𝔊 𝔊 ‹𝔊 ∘CF 𝔉› ‹𝔊 ∘CF-NTCF η›
    by (cs_prems cs_shallow cs_simp: cat_cs_simps)

  from 
    𝔊η.cat_lKe_unique
      [
        OF η.AG.HomCod.cat_cf_id_is_functor,
        unfolded η.AG.cf_cf_comp_cf_id_left,
        OF η.AG.cf_ntcf_id_is_ntcf
      ]
  obtain ε where ε: "ε : 𝔊 ∘CF 𝔉 ↦CF cf_id ℭ : ℭ ↦↦C⇘α⇙ ℭ"
    and ntcf_id_𝔊_def: "ntcf_id 𝔊 = ε ∘NTCF-CF 𝔊 ∙NTCF (𝔊 ∘CF-NTCF η)"
    by metis
  interpret ε: is_ntcf α ℭ ℭ ‹𝔊 ∘CF 𝔉› ‹cf_id ℭ› ε by (rule ε)
  
  show ?thesis
  proof(rule counit_unit_is_cf_adjunction)

    show [cat_cs_simps]: "ε ∘NTCF-CF 𝔊 ∙NTCF (𝔊 ∘CF-NTCF η) = ntcf_id 𝔊"
      by (rule ntcf_id_𝔊_def[symmetric])

    have η_def: "η = (ntcf_id 𝔉 ∘NTCF-CF 𝔊) ∙NTCF η"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps ntcf_id_cf_comp[symmetric] 
            cs_intro: cat_cs_intros
        )
    note [cat_cs_simps] = this[symmetric]

    let ?𝔉ε𝔊 = ‹𝔉 ∘CF-NTCF ε ∘NTCF-CF 𝔊›
    let ?η𝔉𝔊 = ‹η ∘NTCF-CF 𝔉 ∘NTCF-CF 𝔊›
    let ?𝔉𝔊η = ‹𝔉 ∘CF 𝔊 ∘CF-NTCF η›

    have "(?𝔉ε𝔊 ∙NTCF ?η𝔉𝔊) ∙NTCF η = (?𝔉ε𝔊 ∙NTCF ?𝔉𝔊η) ∙NTCF η"
    proof(rule ntcf_eqI)
      have dom_lhs: "𝒟∘ (((?𝔉ε𝔊 ∙NTCF ?η𝔉𝔊) ∙NTCF η)⦇NTMap⦈) = 𝔇⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      have dom_rhs: "𝒟∘ (((?𝔉ε𝔊 ∙NTCF ?𝔉𝔊η) ∙NTCF η)⦇NTMap⦈) = 𝔇⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      note is_ntcf.ntcf_Comp_commute[cat_cs_simps del]
      note category.cat_Comp_assoc[cat_cs_simps del]
      show
        "((?𝔉ε𝔊 ∙NTCF ?η𝔉𝔊) ∙NTCF η)⦇NTMap⦈ =
          ((?𝔉ε𝔊 ∙NTCF ?𝔉𝔊η) ∙NTCF η)⦇NTMap⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix a assume "a ∈∘ 𝔇⦇Obj⦈"
        then show
          "((?𝔉ε𝔊 ∙NTCF ?η𝔉𝔊) ∙NTCF η)⦇NTMap⦈⦇a⦈ =
            ((?𝔉ε𝔊 ∙NTCF ?𝔉𝔊η) ∙NTCF η)⦇NTMap⦈⦇a⦈"
          by
            (
              cs_concl 
                cs_simp: cat_cs_simps η.ntcf_lKe.ntcf_Comp_commute[symmetric]
                cs_intro: cat_cs_intros
            )
      qed (cs_concl cs_intro: cat_cs_intros)+
    qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
    also have "… = (ntcf_id 𝔉 ∘NTCF-CF 𝔊) ∙NTCF η"
      by
        (
          cs_concl cs_shallow
            cs_simp:
              cat_cs_simps
              cf_comp_cf_ntcf_comp_assoc
              cf_ntcf_comp_ntcf_cf_comp_assoc
              cf_ntcf_comp_ntcf_vcomp[symmetric]
            cs_intro: cat_cs_intros
        )
    also have "… = η" by (cs_concl cs_simp: cat_cs_simps)
    finally have "(?𝔉ε𝔊 ∙NTCF ?η𝔉𝔊) ∙NTCF η = η" by simp
    then have η_def': "η = (𝔉 ∘CF-NTCF ε ∙NTCF (η ∘NTCF-CF 𝔉) ∘NTCF-CF 𝔊) ∙NTCF η"
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps ntcf_vcomp_ntcf_cf_comp[symmetric] 
            cs_intro: cat_cs_intros
        )+
  
    have 𝔉εη𝔉: "𝔉 ∘CF-NTCF ε ∙NTCF (η ∘NTCF-CF 𝔉) : 𝔉 ↦CF 𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

    from η.cat_lKe_unique[OF η.Lan.is_functor_axioms η.ntcf_lKe.is_ntcf_axioms]
    obtain σ where
      "⟦ σ' : 𝔉 ↦CF 𝔉 : ℭ ↦↦C⇘α⇙ 𝔇; η = σ' ∘NTCF-CF 𝔊 ∙NTCF η ⟧ ⟹ σ' = σ"
      for σ'
      by metis
  
    from this[OF η.Lan.cf_ntcf_id_is_ntcf η_def] this[OF 𝔉εη𝔉 η_def'] show
      "𝔉 ∘CF-NTCF ε ∙NTCF (η ∘NTCF-CF 𝔉) = ntcf_id 𝔉"
      by simp

  qed (cs_concl cs_intro: cat_cs_intros)+

qed

lemma cf_adjunction_if_rKe_preserves:
  assumes "ε : 𝔉 ∘CF 𝔊 ↦CF.rKe⇘α⇙ cf_id 𝔇 : 𝔇 ↦C ℭ ↦C (𝔊 : 𝔇 ↦↦C ℭ)"
  shows "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
proof-
  interpret ε: is_cat_rKe_preserves α 𝔇 ℭ 𝔇 ℭ 𝔊 ‹cf_id 𝔇› 𝔉 𝔊 ε 
    by (rule assms)
  have "op_cf (cf_id 𝔇) = cf_id (op_cat 𝔇)" unfolding cat_op_simps by simp
  show ?thesis
    by 
      (
        rule is_cf_adjunction.is_cf_adjunction_op
          [
            OF cf_adjunction_if_lKe_preserves[
              OF ε.is_cat_rKe_preserves_op[unfolded op_cf_cf_id]
              ], 
            folded cf_adjunction_of_counit_def, 
            unfolded cat_op_simps
          ]
      )
qed

text‹\newpage›

end