Theory CZH_UCAT_Comma

(* Copyright 2021 (C) Mihails Milehins *)

section‹Comma categories and universal constructions›
theory CZH_UCAT_Comma
  imports CZH_UCAT_Limit_IT
begin



subsection‹
Relationship between the universal arrows, initial objects and terminal objects
›

lemma (in is_functor) universal_arrow_of_if_obj_initial:
  ―‹See Chapter III-1 in \cite{mac_lane_categories_2010}.›
  assumes "c ∈∘ 𝔅⦇Obj⦈" and "obj_initial (c ↓CF 𝔉) [0, r, u]∘"
  shows "universal_arrow_of 𝔉 c r u"
proof(intro universal_arrow_ofI)
  have ru: "[0, r, u]∘ ∈∘ c ↓CF 𝔉⦇Obj⦈"
    and f_unique: "C ∈∘ c ↓CF 𝔉⦇Obj⦈ ⟹ ∃!f. f : [0, r, u]∘ ↦⇘c ↓CF 𝔉⇙ C"
    for C
    by (intro obj_initialD[OF assms(2)])+
  show r: "r ∈∘ 𝔄⦇Obj⦈" and u: "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
    by (intro cat_obj_cf_comma_ObjD[OF ru assms(1)])+
  fix r' u' assume prems: "r' ∈∘ 𝔄⦇Obj⦈" "u' : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r'⦈"
  from assms(1) prems have r'u': "[0, r', u']∘ ∈∘ c ↓CF 𝔉⦇Obj⦈"
    by (cs_concl cs_shallow cs_intro: cat_comma_cs_intros)
  from f_unique[OF r'u'] obtain F
    where F: "F : [0, r, u]∘ ↦⇘c ↓CF 𝔉⇙ [0, r', u']∘"
      and F_unique: "F' : [0, r, u]∘ ↦⇘c ↓CF 𝔉⇙ [0, r', u']∘ ⟹ F' = F"
    for F'
    by metis
  from cat_obj_cf_comma_is_arrE[OF F assms(1), simplified] obtain t 
    where F_def: "F = [[0, r, u]∘, [0, r', u']∘, [0, t]∘]∘"
      and t: "t : r ↦⇘𝔄⇙ r'"
      and [cat_cs_simps]: "𝔉⦇ArrMap⦈⦇t⦈ ∘A⇘𝔅⇙ u = u'"
    by metis
  show "∃!f'. f' : r ↦⇘𝔄⇙ r' ∧ u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
  proof(intro ex1I conjI; (elim conjE)?; (rule t)?)
    from t u show "u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇t⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    fix t' assume prems': "t' : r ↦⇘𝔄⇙ r'" "u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇t'⦈"
    from prems'(2,1) u have [symmetric, cat_cs_simps]: 
      "u' = 𝔉⦇ArrMap⦈⦇t'⦈ ∘A⇘𝔅⇙ u"
      by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    define F' where "F' = [[0, r, u]∘, [0, r', u']∘, [0, t']∘]∘"
    from assms(1) prems'(1) u  prems(2) have F':
      "F' : [0, r, u]∘ ↦⇘c ↓CF 𝔉⇙ [0, r', u']∘"
      unfolding F'_def
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_comma_cs_intros)
    from F_unique[OF this] show "t' = t" unfolding F'_def F_def by simp
  qed
qed

lemma (in is_functor) obj_initial_if_universal_arrow_of:
  ―‹See Chapter III-1 in \cite{mac_lane_categories_2010}.›
  assumes "universal_arrow_of 𝔉 c r u" 
  shows "obj_initial (c ↓CF 𝔉) [0, r, u]∘"
proof-
  from universal_arrow_ofD[OF assms] have r: "r ∈∘ 𝔄⦇Obj⦈"
    and u: "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
    and up: "⟦ r' ∈∘ 𝔄⦇Obj⦈; u' : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r'⦈ ⟧ ⟹
      ∃!f'. f' : r ↦⇘𝔄⇙ r' ∧ u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
    for r' u'
    by auto
  from u have c: "c ∈∘ 𝔅⦇Obj⦈" by auto
  show ?thesis
  proof(intro obj_initialI)
    from r u show "[0, r, u]∘ ∈∘ c ↓CF 𝔉⦇Obj⦈"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_comma_cs_intros)
    fix B assume prems: "B ∈∘ c ↓CF 𝔉⦇Obj⦈"
    from cat_obj_cf_comma_ObjE[OF prems c] obtain r' u' 
      where B_def: "B = [0, r', u']∘" 
        and r': "r' ∈∘ 𝔄⦇Obj⦈" 
        and u': "u' : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r'⦈"
      by auto
    from up[OF r' u'] obtain f 
      where f: "f : r ↦⇘𝔄⇙ r'" 
        and u'_def: "u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f⦈"
        and up': "⟦ f' : r ↦⇘𝔄⇙ r'; u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈ ⟧ ⟹
          f' = f"
      for f'
      by auto
    from u'_def f u have [symmetric, cat_cs_simps]: "u' = 𝔉⦇ArrMap⦈⦇f⦈ ∘A⇘𝔅⇙ u"
      by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    define F where "F = [[0, r, u]∘, [0, r', u']∘, [0, f]∘]∘"
    show "∃!f. f : [0, r, u]∘ ↦⇘c ↓CF 𝔉⇙ B"
      unfolding B_def
    proof(rule ex1I)
      from c u f u' show "F : [0, r, u]∘ ↦⇘c ↓CF 𝔉⇙ [0, r', u']∘"
        unfolding F_def
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_cs_simps cs_intro: cat_comma_cs_intros
          )
      fix F' assume prems': "F' : [0, r, u]∘ ↦⇘c ↓CF 𝔉⇙ [0, r', u']∘"
      from cat_obj_cf_comma_is_arrE[OF prems' c, simplified] obtain f' 
        where F'_def: "F' = [[0, r, u]∘, [0, r', u']∘, [0, f']∘]∘"
          and f': "f' : r ↦⇘𝔄⇙ r'"
          and [cat_cs_simps]: "𝔉⦇ArrMap⦈⦇f'⦈ ∘A⇘𝔅⇙ u = u'"
        by auto
      from f' u have "u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      from up'[OF f' this] show "F' = F" unfolding F'_def F_def by simp
    qed
  qed
qed

lemma (in is_functor) universal_arrow_fo_if_obj_terminal:
  ―‹See Chapter III-1 in \cite{mac_lane_categories_2010}.›
  assumes "c ∈∘ 𝔅⦇Obj⦈" and "obj_terminal (𝔉 CF↓ c) [r, 0, u]∘"
  shows "universal_arrow_fo 𝔉 c r u"
proof-
  let ?op_𝔉c = ‹op_cat (𝔉 CF↓ c)› 
    and ?c_op_𝔉 = ‹c ↓CF (op_cf 𝔉)›
    and ?iso = ‹op_cf_obj_comma 𝔉 c› 
  from cat_cf_obj_comma_ObjD[OF obj_terminalD(1)[OF assms(2)] assms(1)] 
  have r: "r ∈∘ 𝔄⦇Obj⦈" and u: "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
    by simp_all
  interpret 𝔉c: is_iso_functor α ?op_𝔉c ?c_op_𝔉 ?iso
    by (rule op_cf_obj_comma_is_iso_functor[OF assms(1)])
  have iso_cocontinuous: "is_cf_cocontinuous α ?iso"
    by
      (
        rule is_iso_functor.iso_cf_is_cf_cocontinuous[
          OF 𝔉c.is_iso_functor_axioms
          ]
      )
  have iso_preserves: "cf_preserves_colimits α ?iso (cf_0 ?op_𝔉c)"
    by 
      (
        rule is_cf_cocontinuousD
          [
            OF 
              iso_cocontinuous 
              cf_0_is_functor[OF 𝔉c.HomDom.category_axioms] 
              𝔉c.is_functor_axioms
          ]
      )
  from category.cat_obj_initial_is_cat_obj_empty_initial[
      OF 𝔉c.HomDom.category_axioms op_cat_obj_initial[THEN iffD2, OF assms(2)]
      ]
  interpret ntcf_0_op_𝔉c: 
    is_cat_obj_empty_initial α ?op_𝔉c ‹[r, 0, u]∘› ‹ntcf_0 ?op_𝔉c›
    by simp
  have "cf_0 ?op_𝔉c : cat_0 ↦↦C⇘α⇙ ?op_𝔉c" 
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from 
    cf_preserves_colimitsD
      [
        OF 
          iso_preserves 
          ntcf_0_op_𝔉c.is_cat_colimit_axioms
          this
          𝔉c.is_functor_axioms
      ]
    assms(1) r u
  have "ntcf_0 ?c_op_𝔉 :
    cf_0 ?c_op_𝔉 >CF.colim [0, r, u]∘ : cat_0 ↦↦C⇘α⇙ ?c_op_𝔉"
    by
      (
        cs_prems cs_shallow
          cs_simp: cat_cs_simps cat_comma_cs_simps 
          cs_intro: cat_cs_intros cat_comma_cs_intros
      )
  then have obj_initial_ru: "obj_initial ?c_op_𝔉 [0, r, u]∘"
    by
      (
        rule is_cat_obj_empty_initial.cat_oei_obj_initial[
          OF is_cat_obj_empty_initialI
          ]
      )
  from assms(1) have "c ∈∘ op_cat 𝔅⦇Obj⦈" 
    by (cs_concl cs_shallow cs_intro: cat_op_intros)
  from
    is_functor.universal_arrow_of_if_obj_initial[
      OF is_functor_op this obj_initial_ru
      ] 
  have "universal_arrow_of (op_cf 𝔉) c r u"
    by simp
  then show ?thesis unfolding cat_op_simps .
qed

lemma (in is_functor) obj_terminal_if_universal_arrow_fo:
  ―‹See Chapter III-1 in \cite{mac_lane_categories_2010}.›
  assumes "universal_arrow_fo 𝔉 c r u" 
  shows "obj_terminal (𝔉 CF↓ c) [r, 0, u]∘"
proof-
  let ?op_𝔉c = ‹op_cat (𝔉 CF↓ c)› 
    and ?c_op_𝔉 = ‹c ↓CF (op_cf 𝔉)›
    and ?iso = ‹inv_cf (op_cf_obj_comma 𝔉 c)›
  from universal_arrow_foD[OF assms] have r: "r ∈∘ 𝔄⦇Obj⦈"
    and u: "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
    by auto
  then have c: "c ∈∘ 𝔅⦇Obj⦈" by auto
  from u have c_op_𝔉: "category α ?c_op_𝔉"
    by 
      (
        cs_concl cs_shallow cs_intro: 
          cat_cs_intros cat_comma_cs_intros cat_op_intros
      )
  interpret 𝔉c: is_iso_functor α ?op_𝔉c ?c_op_𝔉 ‹op_cf_obj_comma 𝔉 c›
    by (rule op_cf_obj_comma_is_iso_functor[OF c])
  interpret inv_𝔉c: is_iso_functor α ?c_op_𝔉 ?op_𝔉c ?iso
    by (cs_concl cs_shallow cs_intro: cf_cs_intros)
  have iso_cocontinuous: "is_cf_cocontinuous α ?iso"
    by
      (
        rule is_iso_functor.iso_cf_is_cf_cocontinuous[
          OF inv_𝔉c.is_iso_functor_axioms
          ]
      )
  have iso_preserves: "cf_preserves_colimits α ?iso (cf_0 ?c_op_𝔉)"
    by 
      (
        rule is_cf_cocontinuousD
          [
            OF
              iso_cocontinuous
              cf_0_is_functor[OF 𝔉c.HomCod.category_axioms] 
              inv_𝔉c.is_functor_axioms
          ]
      )
  from assms have "universal_arrow_of (op_cf 𝔉) c r u" unfolding cat_op_simps.
  from is_cat_obj_empty_initialD
    [
      OF category.cat_obj_initial_is_cat_obj_empty_initial
        [
          OF c_op_𝔉 is_functor.obj_initial_if_universal_arrow_of[
            OF is_functor_op this
            ]
        ]
    ]
  have ntcf_0_c_op_𝔉: "ntcf_0 ?c_op_𝔉 :
    cf_0 ?c_op_𝔉 >CF.colim [0, r, u]∘ : cat_0 ↦↦C⇘α⇙ ?c_op_𝔉".
  have cf_0_c_op_𝔉: "cf_0 ?c_op_𝔉 : cat_0 ↦↦C⇘α⇙ ?c_op_𝔉"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from 
    cf_preserves_colimitsD[
      OF iso_preserves ntcf_0_c_op_𝔉 cf_0_c_op_𝔉 inv_𝔉c.is_functor_axioms
      ]
    r u
  have "ntcf_0 ?op_𝔉c : cf_0 ?op_𝔉c >CF.colim [r, 0, u]∘ : cat_0 ↦↦C⇘α⇙ ?op_𝔉c"
    by 
      (
        cs_prems cs_shallow
          cs_simp: cat_cs_simps cat_comma_cs_simps 𝔉c.inv_cf_ObjMap_app 
          cs_intro: cat_cs_intros cat_comma_cs_intros cat_op_intros
      )
  from 
    is_cat_obj_empty_initial.cat_oei_obj_initial[
      OF is_cat_obj_empty_initialI[OF this]
      ]  
  show "obj_terminal (𝔉 CF↓ c) [r, 0, u]∘" 
    unfolding op_cat_obj_initial[symmetric].
qed



subsection‹
A projection for a comma category constructed from a functor and an object
creates small limits
›

text‹See Chapter V-6 in cite‹"mac_lane_categories_2010"›.›

lemma cf_obj_cf_comma_proj_creates_limits:
  assumes "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔛"
    and "is_tm_cf_continuous α 𝔊"
    and "x ∈∘ 𝔛⦇Obj⦈"
    and "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ x ↓CF 𝔊"
  shows "cf_creates_limits α (x O⨅CF 𝔊) 𝔉"
proof(intro cf_creates_limitsI conjI allI impI)

  interpret 𝔊: is_functor α 𝔄 𝔛 𝔊 by (rule assms(1))
  interpret 𝔉: is_tm_functor α 𝔍 ‹x ↓CF 𝔊› 𝔉 by (rule assms(4))
  interpret x𝔊: is_functor α ‹x ↓CF 𝔊› 𝔄 ‹x O⨅CF 𝔊›
    by (rule 𝔊.cf_obj_cf_comma_proj_is_functor[OF assms(3)])

  show "𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊" by (rule 𝔉.is_functor_axioms)
  show "x O⨅CF 𝔊 : x ↓CF 𝔊 ↦↦C⇘α⇙ 𝔄" by (rule x𝔊.is_functor_axioms)

  define ψ :: V
    where "ψ =
      [
        (λj∈∘𝔍⦇Obj⦈. 𝔉⦇ObjMap⦈⦇j⦈⦇2ℕ⦈),
        cf_const 𝔍 𝔛 x,
        𝔊 ∘CF (x O⨅CF 𝔊 ∘CF 𝔉),
        𝔍,
        𝔛
      ]∘"
  
  have ψ_components: 
    "ψ⦇NTMap⦈ = (λj∈∘𝔍⦇Obj⦈. 𝔉⦇ObjMap⦈⦇j⦈⦇2ℕ⦈)"
    "ψ⦇NTDom⦈ = cf_const 𝔍 𝔛 x"
    "ψ⦇NTCod⦈ = 𝔊 ∘CF (x O⨅CF 𝔊 ∘CF 𝔉)"
    "ψ⦇NTDGDom⦈ = 𝔍"
    "ψ⦇NTDGCod⦈ = 𝔛"
    unfolding ψ_def nt_field_simps by (simp_all add: nat_omega_simps)

  have ψ_NTMap_app: "ψ⦇NTMap⦈⦇j⦈ = f"
    if "j ∈∘ 𝔍⦇Obj⦈" and "𝔉⦇ObjMap⦈⦇j⦈ = [a, b, f]∘" for a b f j
    using that unfolding ψ_components by (simp add: nat_omega_simps)

  interpret ψ: is_cat_cone α x 𝔍 𝔛 ‹𝔊 ∘CF (x O⨅CF 𝔊 ∘CF 𝔉)› ψ
  proof(intro is_cat_coneI is_ntcfI')
    show "vfsequence ψ" unfolding ψ_def by clarsimp
    show "vcard ψ = 5ℕ" unfolding ψ_def by (simp add: nat_omega_simps)
    show "ψ⦇NTMap⦈⦇a⦈ : 
      cf_const 𝔍 𝔛 x⦇ObjMap⦈⦇a⦈ ↦⇘𝔛⇙ (𝔊 ∘CF (x O⨅CF 𝔊 ∘CF 𝔉))⦇ObjMap⦈⦇a⦈"
      if "a ∈∘ 𝔍⦇Obj⦈" for a
    proof-
      from that have "𝔉⦇ObjMap⦈⦇a⦈ ∈∘ x ↓CF 𝔊⦇Obj⦈"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      from 𝔊.cat_obj_cf_comma_ObjE[OF this assms(3)] obtain c g 
        where 𝔉a_def: "𝔉⦇ObjMap⦈⦇a⦈ = [0, c, g]∘"
          and c: "c ∈∘ 𝔄⦇Obj⦈"
          and g: "g : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇c⦈"
        by auto
      from c g show ?thesis
        using that 
        by
          (
            cs_concl
              cs_simp: cat_comma_cs_simps cat_cs_simps 𝔉a_def ψ_NTMap_app 
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
    qed
    show 
      "ψ⦇NTMap⦈⦇b⦈ ∘A⇘𝔛⇙ cf_const 𝔍 𝔛 x⦇ArrMap⦈⦇f⦈ =
        (𝔊 ∘CF (x O⨅CF 𝔊 ∘CF 𝔉))⦇ArrMap⦈⦇f⦈ ∘A⇘𝔛⇙ ψ⦇NTMap⦈⦇a⦈"
      if "f : a ↦⇘𝔍⇙ b" for a b f
    proof-
      from that have 𝔉f: "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘x ↓CF 𝔊⇙ 𝔉⦇ObjMap⦈⦇b⦈"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      from 𝔊.cat_obj_cf_comma_is_arrE[OF this assms(3)] obtain c h c' h' k 
        where 𝔉f_def: "𝔉⦇ArrMap⦈⦇f⦈ = [[0, c, h]∘, [0, c', h']∘, [0, k]∘]∘"
          and 𝔉a_def: "𝔉⦇ObjMap⦈⦇a⦈ = [0, c, h]∘"
          and 𝔉b_def: "𝔉⦇ObjMap⦈⦇b⦈ = [0, c', h']∘"
          and k: "k : c ↦⇘𝔄⇙ c'"
          and h: "h : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇c⦈"
          and h': "h' : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇c'⦈" 
          and [cat_cs_simps]: "𝔊⦇ArrMap⦈⦇k⦈ ∘A⇘𝔛⇙ h = h'" 
        by metis
      from 𝔉f k h h' that show ?thesis
        unfolding 𝔉f_def 𝔉a_def 𝔉b_def
        by (*slow*)
          (
            cs_concl
              cs_simp:
                cat_cs_simps cat_comma_cs_simps
                𝔉f_def 𝔉a_def 𝔉b_def ψ_NTMap_app
              cs_intro: cat_cs_intros
          )
    qed
  qed (auto simp: assms(3) ψ_components intro: cat_cs_intros)

  fix τ b assume prems: "τ : b <CF.lim x O⨅CF 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
  interpret τ: is_cat_limit α 𝔍 𝔄 ‹x O⨅CF 𝔊 ∘CF 𝔉› b τ by (rule prems)

  note x𝔊_𝔉 = cf_comp_cf_obj_cf_comma_proj_is_tm_functor[OF assms(1,4,3)]
  have "cf_preserves_limits α 𝔊 (x O⨅CF 𝔊 ∘CF 𝔉)"
    by (rule is_tm_cf_continuousD [OF assms(2) x𝔊_𝔉 assms(1)])
  then have 𝔊τ: "𝔊 ∘CF-NTCF τ :
    𝔊⦇ObjMap⦈⦇b⦈ <CF.lim 𝔊 ∘CF (x O⨅CF 𝔊 ∘CF 𝔉) : 𝔍 ↦↦C⇘α⇙ 𝔛"
    by 
      (
        rule cf_preserves_limitsD[
          OF _ prems(1) is_tm_functorD(1)[OF x𝔊_𝔉] assms(1)
          ]
      )

  from is_cat_limit.cat_lim_unique_cone'[OF 𝔊τ ψ.is_cat_cone_axioms] obtain f 
    where f: "f : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇b⦈"
      and ψ_f: "⋀j. j ∈∘ 𝔍⦇Obj⦈ ⟹
        ψ⦇NTMap⦈⦇j⦈ = (𝔊 ∘CF-NTCF τ)⦇NTMap⦈⦇j⦈ ∘A⇘𝔛⇙ f"
      and f_unique:
        "⟦
          f' : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇b⦈; 
          ⋀j. j ∈∘ 𝔍⦇Obj⦈ ⟹ ψ⦇NTMap⦈⦇j⦈ = (𝔊 ∘CF-NTCF τ)⦇NTMap⦈⦇j⦈ ∘A⇘𝔛⇙ f'
         ⟧ ⟹ f' = f"
    for f'
    by metis

  define σ :: V 
    where "σ =
      [
        (
          λj∈∘𝔍⦇Obj⦈.
            [
              [0, b, f]∘,
              [0, (x O⨅CF 𝔊 ∘CF 𝔉)⦇ObjMap⦈⦇j⦈, ψ⦇NTMap⦈⦇j⦈]∘,
              [0, τ⦇NTMap⦈⦇j⦈]∘
            ]∘
        ),
        cf_const 𝔍 (x ↓CF 𝔊) [0, b, f]∘,
        𝔉,
        𝔍,
        x ↓CF 𝔊
      ]∘"

  have σ_components: "σ⦇NTMap⦈ =
      (
        λj∈∘𝔍⦇Obj⦈.
          [
            [0, b, f]∘,
            [0, (x O⨅CF 𝔊 ∘CF 𝔉)⦇ObjMap⦈⦇j⦈, ψ⦇NTMap⦈⦇j⦈]∘,
            [0, τ⦇NTMap⦈⦇j⦈]∘
          ]∘
      )"
    and [cat_cs_simps]: "σ⦇NTDom⦈ = cf_const 𝔍 (x ↓CF 𝔊) [0, b, f]∘"
    and [cat_cs_simps]: "σ⦇NTCod⦈ = 𝔉"
    and [cat_cs_simps]: "σ⦇NTDGDom⦈ = 𝔍"
    and [cat_cs_simps]: "σ⦇NTDGCod⦈ = x ↓CF 𝔊"
    unfolding σ_def nt_field_simps by (simp_all add: nat_omega_simps)

  have σ_NTMap_app: "σ⦇NTMap⦈⦇j⦈ =
    [
      [0, b, f]∘,
      [0, (x O⨅CF 𝔊 ∘CF 𝔉)⦇ObjMap⦈⦇j⦈, ψ⦇NTMap⦈⦇j⦈]∘,
      [0, τ⦇NTMap⦈⦇j⦈]∘
    ]∘"
    if "j ∈∘ 𝔍⦇Obj⦈" for j
    using that unfolding σ_components by simp

  interpret σ: is_cat_cone α ‹[0, b, f]∘› 𝔍 ‹x ↓CF 𝔊› 𝔉 σ 
  proof(intro is_cat_coneI is_ntcfI')
    show "vfsequence σ" unfolding σ_def by auto
    show "vcard σ = 5ℕ" unfolding σ_def by (simp add: nat_omega_simps)
    from f show "cf_const 𝔍 (x ↓CF 𝔊) [0, b, f]∘ : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
      by
        (
          cs_concl cs_intro: 
            cat_cs_intros cat_lim_cs_intros cat_comma_cs_intros
        )
    show "vsv (σ⦇NTMap⦈)" unfolding σ_components by auto
    show "𝒟∘ (σ⦇NTMap⦈) = 𝔍⦇Obj⦈" unfolding σ_components by auto
    from assms(3) show "σ⦇NTMap⦈⦇a⦈ :
      cf_const 𝔍 (x ↓CF 𝔊) [0, b, f]∘⦇ObjMap⦈⦇a⦈ ↦⇘x ↓CF 𝔊⇙ 𝔉⦇ObjMap⦈⦇a⦈"
      if "a ∈∘ 𝔍⦇Obj⦈" for a
    proof-
      from that have 𝔉a: "𝔉⦇ObjMap⦈⦇a⦈ ∈∘ x ↓CF 𝔊⦇Obj⦈"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      from 𝔊.cat_obj_cf_comma_ObjE[OF this assms(3)] obtain c g 
        where 𝔉a_def: "𝔉⦇ObjMap⦈⦇a⦈ = [0, c, g]∘"
          and c: "c ∈∘ 𝔄⦇Obj⦈"
          and g: "g : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇c⦈"
        by auto
      from ψ_f[OF that] that c f g 𝔉a have [symmetric, cat_cs_simps]: 
        "g = 𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇a⦈⦈ ∘A⇘𝔛⇙ f"
        by
          (
            cs_prems cs_shallow
              cs_simp: cat_cs_simps ψ_NTMap_app 𝔉a_def cs_intro: cat_cs_intros
          )
      from that c f g 𝔉a show ?thesis
        unfolding 𝔉a_def
        by
          (
            cs_concl 
              cs_simp:
                cat_comma_cs_simps cat_cs_simps
                ψ_NTMap_app σ_NTMap_app 𝔉a_def
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
    qed
    show
      "σ⦇NTMap⦈⦇d⦈ ∘A⇘x ↓CF 𝔊⇙ cf_const 𝔍 (x ↓CF 𝔊) [0, b, f]∘⦇ArrMap⦈⦇g⦈ =
        𝔉⦇ArrMap⦈⦇g⦈ ∘A⇘x ↓CF 𝔊⇙ σ⦇NTMap⦈⦇c⦈"
      if "g : c ↦⇘𝔍⇙ d" for c d g 
    proof-
      from that have 𝔉g: "𝔉⦇ArrMap⦈⦇g⦈ : 𝔉⦇ObjMap⦈⦇c⦈ ↦⇘x ↓CF 𝔊⇙ 𝔉⦇ObjMap⦈⦇d⦈"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      from 𝔊.cat_obj_cf_comma_is_arrE[OF this assms(3)] obtain e h e' h' k 
        where 𝔉g_def: "𝔉⦇ArrMap⦈⦇g⦈ = [[0, e, h]∘, [0, e', h']∘, [0, k]∘]∘"
          and 𝔉c_def: "𝔉⦇ObjMap⦈⦇c⦈ = [0, e, h]∘"
          and 𝔉d_def: "𝔉⦇ObjMap⦈⦇d⦈ = [0, e', h']∘"
          and k: "k : e ↦⇘𝔄⇙ e'"
          and h: "h : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇e⦈"
          and h': "h' : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇e'⦈" 
          and [cat_cs_simps]: "𝔊⦇ArrMap⦈⦇k⦈ ∘A⇘𝔛⇙ h = h'" 
        by metis
      from that have "c ∈∘ 𝔍⦇Obj⦈" by auto
      from ψ_f[OF this] that k f h have [symmetric, cat_cs_simps]: 
        "h = 𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇c⦈⦈ ∘A⇘𝔛⇙ f"
        by
          (
            cs_prems 
              cs_simp: cat_cs_simps ψ_NTMap_app 𝔉c_def cs_intro: cat_cs_intros
          )
      from that have "d ∈∘ 𝔍⦇Obj⦈"by auto
      from ψ_f[OF this] that k f h' have [symmetric, cat_cs_simps]: 
        "h' = 𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇d⦈⦈ ∘A⇘𝔛⇙ f"
        by
          (
            cs_prems cs_shallow
              cs_simp: cat_cs_simps ψ_NTMap_app 𝔉d_def cs_intro: cat_cs_intros
          )
      note τ.cat_cone_Comp_commute[cat_cs_simps del]
      from τ.ntcf_Comp_commute[OF that] that assms(3) k h h' 
      have [symmetric, cat_cs_simps]: "τ⦇NTMap⦈⦇d⦈ = k ∘A⇘𝔄⇙ τ⦇NTMap⦈⦇c⦈"
        by
          (
            cs_prems
              cs_simp: cat_comma_cs_simps cat_cs_simps 𝔉g_def 𝔉c_def 𝔉d_def
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
      from that f 𝔉g k h h' show ?thesis
        unfolding 𝔉g_def 𝔉c_def 𝔉d_def
        by
          (
            cs_concl
              cs_simp:
                cat_comma_cs_simps cat_cs_simps
                ψ_NTMap_app σ_NTMap_app 𝔉g_def 𝔉c_def 𝔉d_def
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
    qed
  qed
    (
      use f in 
        ‹
          cs_concl cs_shallow 
            cs_intro: cat_cs_intros cat_lim_cs_intros cat_comma_cs_intros 
            cs_simp: cat_cs_simps
        ›
    )+

  have τσ: "τ = x O⨅CF 𝔊 ∘CF-NTCF σ"
  proof(rule ntcf_eqI)
    show "τ : cf_const 𝔍 𝔄 b ↦CF x O⨅CF 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
      by (rule τ.is_ntcf_axioms)
    from f show "x O⨅CF 𝔊 ∘CF-NTCF σ : 
      cf_const 𝔍 𝔄 b ↦CF x O⨅CF 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
      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
        )
    have dom_lhs: "𝒟∘ (τ⦇NTMap⦈) = 𝔍⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    have dom_rhs: "𝒟∘ ((x O⨅CF 𝔊 ∘CF-NTCF σ)⦇NTMap⦈) = 𝔍⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show "τ⦇NTMap⦈ = (x O⨅CF 𝔊 ∘CF-NTCF σ)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume prems': "a ∈∘ 𝔍⦇Obj⦈"
      then have "𝔉⦇ObjMap⦈⦇a⦈ ∈∘ x ↓CF 𝔊⦇Obj⦈"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      from 𝔊.cat_obj_cf_comma_ObjE[OF this assms(3)] obtain c g 
        where 𝔉a_def: "𝔉⦇ObjMap⦈⦇a⦈ = [0, c, g]∘"
          and c: "c ∈∘ 𝔄⦇Obj⦈"
          and g: "g : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇c⦈"
        by auto
      from ψ_f[OF prems'] prems' f g have [symmetric, cat_cs_simps]: 
        "g = 𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇a⦈⦈ ∘A⇘𝔛⇙ f"
        by
          (
            cs_prems cs_shallow
              cs_simp: cat_cs_simps ψ_NTMap_app 𝔉a_def cs_intro: cat_cs_intros
          )
      with assms(3) prems' c g f show 
        "τ⦇NTMap⦈⦇a⦈ = (x O⨅CF 𝔊 ∘CF-NTCF σ)⦇NTMap⦈⦇a⦈"
        by
          (
            cs_concl cs_shallow
              cs_simp:
                cat_comma_cs_simps cat_cs_simps
                𝔉a_def ψ_NTMap_app σ_NTMap_app
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
    qed (simp_all add: τ.ntcf_NTMap_vsv cat_cs_intros)
  qed simp_all

  from f have b_def: "b = x O⨅CF 𝔊⦇ObjMap⦈⦇0, b, f⦈∙"
    by (cs_concl cs_simp: cat_comma_cs_simps cs_intro: cat_cs_intros)

  show σa_unique: "∃!σa. ∃σ a.
    σa = ⟨σ, a⟩ ∧
    σ : a <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊 ∧
    τ = x O⨅CF 𝔊 ∘CF-NTCF σ ∧ b = x O⨅CF 𝔊⦇ObjMap⦈⦇a⦈"
  proof
    (
      intro ex1I[where a=‹⟨σ, [0, b, f]∘⟩›] exI conjI, simp only:; 
      (elim exE conjE)?
    )

    show "σ : [0, b, f]∘ <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
      by (rule σ.is_cat_cone_axioms)
    show "τ = x O⨅CF 𝔊 ∘CF-NTCF σ" by (rule τσ)
    show "b = x O⨅CF 𝔊⦇ObjMap⦈ ⦇0, b, f⦈∙" by (rule b_def)

    fix σa σ' a assume prems':
      "σa = ⟨σ', a⟩"
      "σ' : a <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
      "τ = x O⨅CF 𝔊 ∘CF-NTCF σ'"
      "b = x O⨅CF 𝔊⦇ObjMap⦈⦇a⦈" 
    interpret σ': is_cat_cone α a 𝔍 ‹x ↓CF 𝔊› 𝔉 σ' by (rule prems'(2))

    from 𝔊.cat_obj_cf_comma_ObjE[OF σ'.cat_cone_obj assms(3)] obtain c g 
      where a_def'': "a = [0, c, g]∘"
        and c': "c ∈∘ 𝔄⦇Obj⦈"
        and g': "g : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇c⦈"
      by auto
    from prems'(4) c' g' assms(3) have bc: "b = c"
      by
        (
          cs_prems cs_shallow
            cs_simp: cat_comma_cs_simps a_def'' cs_intro: cat_comma_cs_intros
        )
    with a_def'' c' g' have a_def': "a = [0, b, g]∘"
      and b: "b ∈∘ 𝔄⦇Obj⦈"
      and g: "g : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇b⦈"
      by auto

    from prems'(3) have τ_eq_x𝔊_σ': 
      "τ⦇NTMap⦈⦇j⦈ = (x O⨅CF 𝔊 ∘CF-NTCF σ')⦇NTMap⦈⦇j⦈" for j
      by simp

    have "ψ⦇NTMap⦈⦇j⦈ = (𝔊 ∘CF-NTCF τ)⦇NTMap⦈⦇j⦈ ∘A⇘𝔛⇙ g"
      if "j ∈∘ 𝔍⦇Obj⦈" for j
    proof-
      from that have σ'_j: "σ'⦇NTMap⦈⦇j⦈ : [0, b, g]∘ ↦⇘x ↓CF 𝔊⇙ 𝔉⦇ObjMap⦈⦇j⦈"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_cs_simps a_def'[symmetric] cs_intro: cat_cs_intros
          )
      from 𝔊.cat_obj_cf_comma_is_arrE[OF this]  obtain e h k 
        where σ'_j_def: "σ'⦇NTMap⦈⦇j⦈ = [[0, b, g]∘, [0, e, h]∘, [0, k]∘]∘"
          and 𝔉j_def: "𝔉⦇ObjMap⦈⦇j⦈ = [0, e, h]∘"
          and k: "k : b ↦⇘𝔄⇙ e"
          and h: "h : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇e⦈" 
          and [cat_cs_simps]: "𝔊⦇ArrMap⦈⦇k⦈ ∘A⇘𝔛⇙ g = h" 
        by (metis 𝔊.cat_obj_cf_comma_is_arrD(4,7) σ'_j assms(3))
      from that σ'_j show ?thesis
        unfolding σ'_j_def
        by
          (
            cs_concl cs_shallow 
              cs_simp:
                cat_cs_simps cat_comma_cs_simps
                σ'_j_def ψ_NTMap_app 𝔉j_def prems'(3)
              cs_intro: cat_cs_intros
          )
    qed
    from f_unique[OF g this] have gf: "g = f".
    with a_def' have a_def: "a = [0, b, f]∘" by simp

    have σσ': "σ = σ'"
    proof(rule ntcf_eqI)
      show "σ : cf_const 𝔍 (x ↓CF 𝔊) [0, b, f]∘ ↦CF 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      then have dom_lhs: "𝒟∘ (σ⦇NTMap⦈) = 𝔍⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps)
      show "σ' : cf_const 𝔍 (x ↓CF 𝔊) [0, b, f]∘ ↦CF 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
        by (cs_concl cs_shallow cs_simp: a_def cs_intro: cat_cs_intros)
      then 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 j assume prems'': "j ∈∘ 𝔍⦇Obj⦈"
        then have σ'_j: "σ'⦇NTMap⦈⦇j⦈ : [0, b, f]∘ ↦⇘x ↓CF 𝔊⇙ 𝔉⦇ObjMap⦈⦇j⦈"
          by 
            (
              cs_concl cs_shallow
                cs_simp: cat_cs_simps a_def'[symmetric] gf[symmetric] 
                cs_intro: cat_cs_intros
            )
        from 𝔊.cat_obj_cf_comma_is_arrE[OF this] obtain e h k 
          where σ'_j_def: "σ'⦇NTMap⦈⦇j⦈ = [[0, b, f]∘, [0, e, h]∘, [0, k]∘]∘"
            and 𝔉j_def: "𝔉⦇ObjMap⦈⦇j⦈ = [0, e, h]∘"
            and k: "k : b ↦⇘𝔄⇙ e"
            and h: "h : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇e⦈" 
            and [cat_cs_simps]: "𝔊⦇ArrMap⦈⦇k⦈ ∘A⇘𝔛⇙ f = h" 
          by (metis 𝔊.cat_obj_cf_comma_is_arrD(4,7) σ'_j assms(3))
        from prems'' k h assms(3) f h show "σ⦇NTMap⦈⦇j⦈ = σ'⦇NTMap⦈⦇j⦈"
          by
            (
              cs_concl cs_shallow
                cs_simp:
                  cat_cs_simps cat_comma_cs_simps
                  τ_eq_x𝔊_σ' ψ_NTMap_app σ_NTMap_app 𝔉j_def σ'_j_def
                cs_intro: cat_cs_intros cat_comma_cs_intros
            )
      qed (cs_concl cs_shallow cs_intro: V_cs_intros)
    qed simp_all
    show "σa = ⟨σ, [[]∘, b, f]∘⟩" unfolding prems'(1) σσ' a_def by simp
  qed

  show "σ' : a' <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
    if "σ' : a' <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
      and "τ = x O⨅CF 𝔊 ∘CF-NTCF σ'"
      and "b = x O⨅CF 𝔊⦇ObjMap⦈⦇a'⦈"
    for σ' a'
  proof(rule is_cat_limitI)

    interpret σ': is_cat_cone α a' 𝔍 ‹x ↓CF 𝔊› 𝔉 σ' by (rule that(1))

    from σ.is_cat_cone_axioms τσ b_def that σa_unique have 
      "⟨σ', a'⟩ = ⟨σ, [0, b, f]∘⟩" 
      by metis
    then have σ'_def: "σ' = σ" and a'_def: "a' = [0, b, f]∘" by simp_all

    show "σ' : a' <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
      by (rule σ'.is_cat_cone_axioms)

    fix σ'' a'' assume prems: "σ'' : a'' <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
    then interpret σ'': is_cat_cone α a'' 𝔍 ‹x ↓CF 𝔊› 𝔉 σ'' .
    from 𝔊.cat_obj_cf_comma_ObjE[OF σ''.cat_cone_obj assms(3)] obtain b' f' 
      where a''_def: "a'' = [0, b', f']∘"
        and b': "b' ∈∘ 𝔄⦇Obj⦈"
        and f': "f' : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇b'⦈"
      by auto
    from b' f' have x𝔊_A': "x O⨅CF 𝔊⦇ObjMap⦈⦇a''⦈ = b'"
      unfolding a''_def
      by
        (
          cs_concl cs_shallow 
            cs_simp: cat_comma_cs_simps cs_intro: cat_comma_cs_intros
        )
    
    from τ.cat_lim_unique_cone'[
        OF cf_ntcf_comp_cf_cat_cone[OF prems x𝔊.is_functor_axioms],
        unfolded x𝔊_A'
        ]
    obtain h where h: "h : b' ↦⇘𝔄⇙ b"
      and x𝔊_σ''_app: "⋀j. j ∈∘ 𝔍⦇Obj⦈ ⟹
        (x O⨅CF 𝔊 ∘CF-NTCF σ'')⦇NTMap⦈⦇j⦈ = τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ h"
      and h_unique:
        "⟦
          h' : b' ↦⇘𝔄⇙ b;
          ⋀j. j ∈∘ 𝔍⦇Obj⦈ ⟹
            (x O⨅CF 𝔊 ∘CF-NTCF σ'')⦇NTMap⦈⦇j⦈ = τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ h'
         ⟧ ⟹ h' = h"
      for h'
      by metis

    define F where "F = [a'', a', [0, h]∘]∘"

    show "∃!F'.
      F' : a'' ↦⇘x ↓CF 𝔊⇙ a' ∧ σ'' = σ' ∙NTCF ntcf_const 𝔍 (x ↓CF 𝔊) F'"
      unfolding a''_def a'_def σ'_def
    proof(intro ex1I conjI; (elim conjE)?)
      from f' h have 𝔊h_f': "𝔊⦇ArrMap⦈⦇h⦈ ∘A⇘𝔛⇙ f' : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇b⦈"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros )
      have "ψ⦇NTMap⦈⦇j⦈ = (𝔊 ∘CF-NTCF τ)⦇NTMap⦈⦇j⦈ ∘A⇘𝔛⇙ (𝔊⦇ArrMap⦈⦇h⦈ ∘A⇘𝔛⇙ f')"
        if "j ∈∘ 𝔍⦇Obj⦈" for j
      proof-
        from that have σ''_j: 
          "σ''⦇NTMap⦈⦇j⦈ : [0, b', f']∘ ↦⇘x ↓CF 𝔊⇙ 𝔉⦇ObjMap⦈⦇j⦈"
          by 
            (
              cs_concl cs_shallow 
                cs_simp: cat_cs_simps a''_def[symmetric] 
                cs_intro: cat_cs_intros
            )
        from 𝔊.cat_obj_cf_comma_is_arrE[OF this] obtain e h' k 
          where σ''_j_def: "σ''⦇NTMap⦈⦇j⦈ = [[0, b', f']∘, [0, e, h']∘, [0, k]∘]∘"
            and 𝔉j_def: "𝔉⦇ObjMap⦈⦇j⦈ = [0, e, h']∘"
            and k: "k : b' ↦⇘𝔄⇙ e"
            and [cat_cs_simps]: "𝔊⦇ArrMap⦈⦇k⦈ ∘A⇘𝔛⇙ f' = h'" 
          by (metis 𝔊.cat_obj_cf_comma_is_arrD(4,7) σ''_j assms(3))
        from that σ''_j have ψ_NTMap_j: "ψ⦇NTMap⦈⦇j⦈ =
          (𝔊 ∘CF-NTCF (x O⨅CF 𝔊 ∘CF-NTCF σ''))⦇NTMap⦈⦇j⦈ ∘A⇘𝔛⇙ f'"
          unfolding σ''_j_def 𝔉j_def
          by
            (
              cs_concl cs_shallow 
                cs_simp:
                  cat_cs_simps cat_comma_cs_simps σ''_j_def 𝔉j_def ψ_NTMap_app
                cs_intro: cat_cs_intros
            )+
        from that h f' show ?thesis
          unfolding ψ_NTMap_j
          by
            (
              cs_concl cs_shallow
                cs_simp:
                  cat_cs_simps
                  is_ntcf.cf_ntcf_comp_NTMap_app 
                  x𝔊_σ''_app[OF that]
                cs_intro: cat_cs_intros
            )
      qed

      from f_unique[OF 𝔊h_f' this] have [cat_cs_simps]: 
        "𝔊⦇ArrMap⦈⦇h⦈ ∘A⇘𝔛⇙ f' = f".

      from assms(3) h f' f show F: "F : [0, b', f']∘ ↦⇘x ↓CF 𝔊⇙ [0, b, f]∘"
        unfolding F_def a''_def a'_def 
        by
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cs_intro: cat_comma_cs_intros
          )

      show "σ'' = σ ∙NTCF ntcf_const 𝔍 (x ↓CF 𝔊) F"
      proof(rule ntcf_eqI)
        show "σ'' : cf_const 𝔍 (x ↓CF 𝔊) a'' ↦CF 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
          by (rule σ''.is_ntcf_axioms)
        then have dom_lhs: "𝒟∘ (σ''⦇NTMap⦈) = 𝔍⦇Obj⦈"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)
        from F show "σ ∙NTCF ntcf_const 𝔍 (x ↓CF 𝔊) F : 
          cf_const 𝔍 (x ↓CF 𝔊) a'' ↦CF 𝔉 : 𝔍 ↦↦C⇘α⇙ x ↓CF 𝔊"
          unfolding a''_def by (cs_concl cs_shallow cs_intro: cat_cs_intros)
        then have dom_rhs: 
          "𝒟∘ ((σ ∙NTCF ntcf_const 𝔍 (x ↓CF 𝔊) F)⦇NTMap⦈) = 𝔍⦇Obj⦈"
          by (cs_concl cs_simp: cat_cs_simps)
        show "σ''⦇NTMap⦈ = (σ ∙NTCF ntcf_const 𝔍 (x ↓CF 𝔊) F)⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix j assume prems': "j ∈∘ 𝔍⦇Obj⦈"
          then have σ''_j: 
            "σ''⦇NTMap⦈⦇j⦈ : [0, b', f']∘ ↦⇘x ↓CF 𝔊⇙ 𝔉⦇ObjMap⦈⦇j⦈"
            by
              (
                cs_concl cs_shallow
                  cs_simp: cat_cs_simps a''_def[symmetric]
                  cs_intro: cat_cs_intros
              )
          from 𝔊.cat_obj_cf_comma_is_arrE[OF this] obtain e h' k 
            where σ''_j_def: "σ''⦇NTMap⦈⦇j⦈ = [[0, b', f']∘, [0, e, h']∘, [0, k]∘]∘"
              and 𝔉j_def: "𝔉⦇ObjMap⦈⦇j⦈ = [0, e, h']∘"
              and k: "k : b' ↦⇘𝔄⇙ e"
              and h': "h' : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇e⦈" 
              and [cat_cs_simps]: "𝔊⦇ArrMap⦈⦇k⦈ ∘A⇘𝔛⇙ f' = h'" 
            by (metis 𝔊.cat_obj_cf_comma_is_arrD(4,7) σ''_j assms(3))
          from assms(3) prems' F k h' h f f' show  
            "σ''⦇NTMap⦈⦇j⦈ = (σ ∙NTCF ntcf_const 𝔍 (x ↓CF 𝔊) F)⦇NTMap⦈⦇j⦈"
            by (*very slow*)
              (
                cs_concl 
                  cs_simp:
                    cat_cs_simps cat_comma_cs_simps 
                    σ''_j_def x𝔊_σ''_app[OF prems', symmetric] 
                    σ_NTMap_app F_def 𝔉j_def a''_def a'_def 
                  cs_intro: cat_cs_intros cat_comma_cs_intros 
                  cs_simp: ψ_f ψ_NTMap_app
              )
        qed (cs_concl cs_intro: V_cs_intros cat_cs_intros)+
      qed simp_all
      fix F' assume prems':
        "F' : [0, b', f']∘ ↦⇘x ↓CF 𝔊⇙ [0, b, f]∘"
        "σ'' = σ ∙NTCF ntcf_const 𝔍 (x ↓CF 𝔊) F'"
      from 𝔊.cat_obj_cf_comma_is_arrE[OF prems'(1) assms(3), simplified] 
      obtain k
        where F'_def: "F' = [[0, b', f']∘, [0, b, f]∘, [0, k]∘]∘"
          and k: "k : b' ↦⇘𝔄⇙ b"
          and [cat_cs_simps]: "𝔊⦇ArrMap⦈⦇k⦈ ∘A⇘𝔛⇙ f' = f" 
        by metis
      have "k = h"
      proof(rule h_unique[OF k])
        fix j assume prems'': "j ∈∘ 𝔍⦇Obj⦈"
        then have "𝔉⦇ObjMap⦈⦇j⦈ ∈∘ x ↓CF 𝔊⦇Obj⦈"
          by (cs_concl cs_shallow cs_intro: cat_cs_intros)
        from 𝔊.cat_obj_cf_comma_ObjE[OF this assms(3)] obtain c g 
          where 𝔉j_def: "𝔉⦇ObjMap⦈⦇j⦈ = [0, c, g]∘"
            and c: "c ∈∘ 𝔄⦇Obj⦈"
            and g: "g : x ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇c⦈"
          by auto
        from prems'' prems'(1) assms(3) c g f show 
          "(x O⨅CF 𝔊 ∘CF-NTCF σ'')⦇NTMap⦈⦇j⦈ = τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ k"
          unfolding prems'(2) τσ F'_def 
          by (*very slow*)
            (
              cs_concl
                cs_simp: cat_comma_cs_simps cat_cs_simps
                cs_intro: cat_cs_intros cat_comma_cs_intros
                cs_simp: ψ_f σ_NTMap_app 𝔉j_def
            )
      qed
      then show "F' = F" unfolding F'_def F_def a''_def a'_def by simp
    qed

  qed

qed

text‹\newpage›

end