Theory CZH_UCAT_Pointed

(* Copyright 2021 (C) Mihails Milehins *)

section‹Pointed arrows and natural transformations›
theory CZH_UCAT_Pointed
  imports 
    CZH_Elementary_Categories.CZH_ECAT_NTCF
    CZH_Elementary_Categories.CZH_ECAT_Hom
begin



subsection‹Pointed arrow›


text‹
The terminology that is used in this section deviates from convention: a 
pointed arrow is merely an arrow in ‹Set› from a singleton set to another set.
›


subsubsection‹Definition and elementary properties›


text‹See Chapter III-2 in \<^cite>‹"mac_lane_categories_2010"›.›

definition ntcf_paa :: "V ⇒ V ⇒ V ⇒ V"
  where "ntcf_paa 𝔞 B b = [(λa∈⇩∘set {𝔞}. b), set {𝔞}, B]⇩∘"


text‹Components.›

lemma ntcf_paa_components:
  shows "ntcf_paa 𝔞 B b⦇ArrVal⦈ = (λa∈⇩∘set {𝔞}. b)"
    and [cat_cs_simps]: "ntcf_paa 𝔞 B b⦇ArrDom⦈ = set {𝔞}"
    and [cat_cs_simps]: "ntcf_paa 𝔞 B b⦇ArrCod⦈ = B"
  unfolding ntcf_paa_def arr_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Arrow value›

mk_VLambda ntcf_paa_components(1)
  |vsv ntcf_paa_ArrVal_vsv[cat_cs_intros]|
  |vdomain ntcf_paa_ArrVal_vdomain[cat_cs_simps]|
  |app ntcf_paa_ArrVal_app[unfolded vsingleton_iff, cat_cs_simps]|


subsubsection‹Pointed arrow is an arrow in ‹Set››

lemma (in 𝒵) ntcf_paa_is_arr:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈" and "A ∈⇩∘ cat_Set α⦇Obj⦈" and "a ∈⇩∘ A"
  shows "ntcf_paa 𝔞 A a : set {𝔞} ↦⇘cat_Set α⇙ A"
proof(intro cat_Set_is_arrI arr_SetI cat_cs_intros, unfold cat_cs_simps)
  show "vfsequence (ntcf_paa 𝔞 A a)" unfolding ntcf_paa_def by simp
  show "vcard (ntcf_paa 𝔞 A a) = 3⇩ℕ"
    unfolding ntcf_paa_def by (simp add: nat_omega_simps)
  show "ℛ⇩∘ (ntcf_paa 𝔞 A a⦇ArrVal⦈) ⊆⇩∘ A"
    unfolding ntcf_paa_components by (intro vrange_VLambda_vsubset assms)
qed (use assms in ‹auto simp: cat_Set_components(1) Limit_vsingleton_in_VsetI›)

lemma (in 𝒵) ntcf_paa_is_arr'[cat_cs_intros]:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈" 
    and "A ∈⇩∘ cat_Set α⦇Obj⦈" 
    and "a ∈⇩∘ A"
    and "A' = set {𝔞}"
    and "B' = A"
    and "ℭ' = cat_Set α"
  shows "ntcf_paa 𝔞 A a : A' ↦⇘ℭ'⇙ B'"
  using assms(1-3) unfolding assms(4-6) by (rule ntcf_paa_is_arr) 

lemmas [cat_cs_intros] = 𝒵.ntcf_paa_is_arr'


subsubsection‹Further properties›

lemma ntcf_paa_injective[cat_cs_simps]: 
  "ntcf_paa 𝔞 A b = ntcf_paa 𝔞 A c ⟷ b = c"
proof
  assume "ntcf_paa 𝔞 A b = ntcf_paa 𝔞 A c"
  then have "ntcf_paa 𝔞 A b⦇ArrVal⦈⦇𝔞⦈ = ntcf_paa 𝔞 A c⦇ArrVal⦈⦇𝔞⦈" by simp
  then show "b = c" by (cs_prems cs_simp: cat_cs_simps)
qed simp

lemma (in 𝒵) ntcf_paa_ArrVal:
  assumes "F : set {𝔞} ↦⇘cat_Set α⇙ X"
  shows "ntcf_paa 𝔞 X (F⦇ArrVal⦈⦇𝔞⦈) = F"
proof-
  interpret F: arr_Set α F
    rewrites [cat_cs_simps]: "F⦇ArrDom⦈ = set {𝔞}" 
      and [cat_cs_simps]: "F⦇ArrCod⦈ = X"
    by (auto simp: cat_Set_is_arrD[OF assms])
  from F.arr_Par_ArrDom_in_Vset have 𝔞: "𝔞 ∈⇩∘ Vset α" by auto
  from assms 𝔞 F.arr_Par_ArrCod_in_Vset have lhs_is_arr:
    "ntcf_paa 𝔞 X (F⦇ArrVal⦈⦇𝔞⦈) : set {𝔞} ↦⇘cat_Set α⇙ X"
    by
      (
        cs_concl cs_shallow 
          cs_simp: cat_Set_components(1)
          cs_intro: V_cs_intros cat_Set_cs_intros cat_cs_intros
      )
  then have dom_lhs: "𝒟⇩∘ (ntcf_paa 𝔞 X (F⦇ArrVal⦈⦇𝔞⦈)⦇ArrVal⦈) = set {𝔞}"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from assms have dom_rhs: "𝒟⇩∘ (F⦇ArrVal⦈) = set {𝔞}" 
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  show ?thesis
  proof(rule arr_Set_eqI)
    from lhs_is_arr assms 
    show arr_Set_lhs: "arr_Set α (ntcf_paa 𝔞 X (F⦇ArrVal⦈⦇𝔞⦈))" 
      and arr_Set_rhs: "arr_Set α F"
      by (auto dest: cat_Set_is_arrD)
    show "ntcf_paa 𝔞 X (F⦇ArrVal⦈⦇𝔞⦈)⦇ArrVal⦈ = F⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs vsingleton_iff; (simp only:)?)
      show "ntcf_paa 𝔞 X (F⦇ArrVal⦈⦇𝔞⦈)⦇ArrVal⦈⦇𝔞⦈ = F⦇ArrVal⦈⦇𝔞⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed (use arr_Set_lhs arr_Set_rhs in auto)
  qed (use assms in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed

lemma (in 𝒵) ntcf_paa_ArrVal'(*not cat_cs_simps*):
  assumes "F : set {𝔞} ↦⇘cat_Set α⇙ X" and "a = 𝔞"
  shows "ntcf_paa 𝔞 X (F⦇ArrVal⦈⦇a⦈) = F"
  using assms(1) unfolding assms(2) by (rule ntcf_paa_ArrVal)

lemma (in 𝒵) ntcf_paa_Comp_right[cat_cs_simps]:
  assumes "F : A ↦⇘cat_Set α⇙ B" 
    and "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈" 
    and "a ∈⇩∘ A"
  shows "F ∘⇩A⇘cat_Set α⇙ ntcf_paa 𝔞 A a = ntcf_paa 𝔞 B (F⦇ArrVal⦈⦇a⦈)"
proof-
  from assms have F_paa:
    "F ∘⇩A⇘cat_Set α⇙ ntcf_paa 𝔞 A a : set {𝔞} ↦⇘cat_Set α⇙ B"
    by (cs_concl cs_intro: cat_cs_intros)
  then have dom_lhs: "𝒟⇩∘ ((F ∘⇩A⇘cat_Set α⇙ ntcf_paa 𝔞 A a)⦇ArrVal⦈) = set {𝔞}"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from assms have paa: "ntcf_paa 𝔞 B (F⦇ArrVal⦈⦇a⦈) : set {𝔞} ↦⇘cat_Set α⇙ B"
    by (cs_concl cs_shallow cs_intro: cat_Set_cs_intros cat_cs_intros)
  then have dom_rhs: "𝒟⇩∘ ((ntcf_paa 𝔞 B (F⦇ArrVal⦈⦇a⦈))⦇ArrVal⦈) = set {𝔞}"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  show ?thesis
  proof(rule arr_Set_eqI)
    from F_paa paa assms 
    show arr_Set_lhs: "arr_Set α (F ∘⇩A⇘cat_Set α⇙ ntcf_paa 𝔞 A a)" 
      and arr_Set_rhs: "arr_Set α (ntcf_paa 𝔞 B (F⦇ArrVal⦈⦇a⦈))"
      by (auto dest: cat_Set_is_arrD)
    show 
      "(F ∘⇩A⇘cat_Set α⇙ ntcf_paa 𝔞 A a)⦇ArrVal⦈ =
        ntcf_paa 𝔞 B (F⦇ArrVal⦈⦇a⦈)⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs vsingleton_iff; (simp only:)?)
      from assms show 
        "(F ∘⇩A⇘cat_Set α⇙ ntcf_paa 𝔞 A a)⦇ArrVal⦈⦇𝔞⦈ =
          ntcf_paa 𝔞 B (F⦇ArrVal⦈⦇a⦈)⦇ArrVal⦈⦇𝔞⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros)
    qed (use arr_Set_lhs arr_Set_rhs in auto)
  qed (use F_paa paa in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed

lemmas [cat_cs_simps] = 𝒵.ntcf_paa_Comp_right



subsection‹Pointed natural transformation›


subsubsection‹Definition and elementary properties›


text‹See Chapter III-2 in \<^cite>‹"mac_lane_categories_2010"›.›

definition ntcf_pointed :: "V ⇒ V ⇒ V"
  where "ntcf_pointed α 𝔞 =
    [
      (
        λx∈⇩∘cat_Set α⦇Obj⦈.
          [
            (λf∈⇩∘Hom (cat_Set α) (set {𝔞}) x. f⦇ArrVal⦈⦇𝔞⦈),
            Hom (cat_Set α) (set {𝔞}) x,
            x
          ]⇩∘
      ),
      Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-),
      cf_id (cat_Set α),
      cat_Set α,
      cat_Set α
    ]⇩∘"


text‹Components.›

lemma ntcf_pointed_components:
  shows "ntcf_pointed α 𝔞⦇NTMap⦈ =
      (
        λx∈⇩∘cat_Set α⦇Obj⦈.
          [
            (λf∈⇩∘Hom (cat_Set α) (set {𝔞}) x. f⦇ArrVal⦈⦇𝔞⦈),
            Hom (cat_Set α) (set {𝔞}) x, 
            x
          ]⇩∘
      )"
    and [cat_cs_simps]: "ntcf_pointed α 𝔞⦇NTDom⦈ = Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-)"
    and [cat_cs_simps]: "ntcf_pointed α 𝔞⦇NTCod⦈ = cf_id (cat_Set α)"
    and [cat_cs_simps]: "ntcf_pointed α 𝔞⦇NTDGDom⦈ = cat_Set α"
    and [cat_cs_simps]: "ntcf_pointed α 𝔞⦇NTDGCod⦈ = cat_Set α"
  unfolding ntcf_pointed_def nt_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Natural transformation map›

mk_VLambda ntcf_pointed_components(1)
  |vsv ntcf_pointed_NTMap_vsv[cat_cs_intros]|
  |vdomain ntcf_pointed_NTMap_vdomain[cat_cs_simps]|
  |app ntcf_pointed_NTMap_app'|

lemma (in 𝒵) ntcf_pointed_NTMap_app_ArrVal_app[cat_cs_simps]: 
  assumes "X ∈⇩∘ cat_Set α⦇Obj⦈" and "F : set {𝔞} ↦⇘cat_Set α⇙ X"
  shows "ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈⦇F⦈ = F⦇ArrVal⦈⦇𝔞⦈"
  by (simp add: assms(2) ntcf_pointed_NTMap_app'[OF assms(1)] arr_Rel_components)

lemma (in 𝒵) ntcf_pointed_NTMap_app_is_iso_arr: 
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈" and "X ∈⇩∘ cat_Set α⦇Obj⦈"
  shows "ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈ :
    Hom (cat_Set α) (set {𝔞}) X ↦⇩i⇩s⇩o⇘cat_Set α⇙ X"
proof-
  interpret Set: category α ‹cat_Set α› by (rule category_cat_Set)
  note app_X = ntcf_pointed_NTMap_app'[OF assms(2)]
  show ?thesis 
  proof(intro cat_Set_is_iso_arrI cat_Set_is_arrI arr_SetI)
    show ArrVal_vsv: "vsv (ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈)"
      unfolding app_X arr_Rel_components by simp
    show "vcard (ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈) = 3⇩ℕ"
      unfolding app_X arr_Rel_components by (simp add: nat_omega_simps)
    show ArrVal_vdomain: 
      "𝒟⇩∘ (ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈) = Hom (cat_Set α) (set {𝔞}) X"
      unfolding app_X arr_Rel_components by simp
    show vrange_left: 
      "ℛ⇩∘ (ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈) ⊆⇩∘
        ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrCod⦈"
      unfolding app_X arr_Rel_components 
      by
        (
          auto
            simp: in_Hom_iff
            intro: cat_Set_cs_intros
            intro!: vrange_VLambda_vsubset
        )
    show "ℛ⇩∘ (ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈) = X"
    proof(intro vsubset_antisym)
      show "X ⊆⇩∘ ℛ⇩∘ (ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈)"
      proof(intro vsubsetI)
        fix x assume prems: "x ∈⇩∘ X"
        from assms prems have F_in_vdomain: 
          "ntcf_paa 𝔞 X x ∈⇩∘ 𝒟⇩∘ ((ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈))"
          unfolding app_X arr_Rel_components vdomain_VLambda in_Hom_iff
          by (cs_concl cs_shallow cs_intro: cat_cs_intros)
        from assms prems have x_def: 
          "x = ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈⦇ntcf_paa 𝔞 X x⦈"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        show "x ∈⇩∘ ℛ⇩∘ (ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈)"
           by (subst x_def) (intro vsv.vsv_vimageI2 F_in_vdomain ArrVal_vsv)
      qed
    qed (use vrange_left in ‹simp add: app_X arr_Rel_components›)
    from assms show "ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrDom⦈ ∈⇩∘ Vset α"
      unfolding app_X arr_Rel_components cat_Set_components(1) 
      by (intro Set.cat_Hom_in_Vset[OF _ assms(2)])
        (auto simp: cat_Set_components(1))
    show "v11 (ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈)"
    proof(intro vsv.vsv_valeq_v11I ArrVal_vsv, unfold ArrVal_vdomain in_Hom_iff)
      fix F G assume prems:
        "F : set {𝔞} ↦⇘cat_Set α⇙ X"
        "G : set {𝔞} ↦⇘cat_Set α⇙ X"
        "ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈⦇F⦈ =
          ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈⦇G⦈"
      note F = cat_Set_is_arrD[OF prems(1)] and G = cat_Set_is_arrD[OF prems(2)]
      from prems(3,1,2) assms have F_ArrVal_G_ArrVal: "F⦇ArrVal⦈⦇𝔞⦈ = G⦇ArrVal⦈⦇𝔞⦈"
        by (cs_prems cs_simp: cat_cs_simps)
      interpret F: arr_Set α F + G: arr_Set α G by (simp_all add: F G)
      show "F = G"
      proof(rule arr_Set_eqI)
        show "arr_Set α F" "arr_Set α G" 
          by (intro F.arr_Set_axioms G.arr_Set_axioms)+
        show "F⦇ArrVal⦈ = G⦇ArrVal⦈"
          by 
            (
              rule vsv_eqI, 
              unfold F.arr_Set_ArrVal_vdomain G.arr_Set_ArrVal_vdomain F(2) G(2)
            )
            (auto simp: F_ArrVal_G_ArrVal)
      qed (simp_all add: F G)
    qed
  qed (use assms in ‹auto simp: app_X arr_Rel_components cat_Set_components(1)›)
qed

lemma (in 𝒵) ntcf_pointed_NTMap_app_is_iso_arr'[cat_cs_intros]: 
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈" 
    and "X ∈⇩∘ cat_Set α⦇Obj⦈"
    and "A' = Hom (cat_Set α) (set {𝔞}) X"
    and "B' = X"
    and "ℭ' = cat_Set α"
  shows "ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈ : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
  using assms(1,2)
  unfolding assms(3-5)
  by (rule ntcf_pointed_NTMap_app_is_iso_arr)

lemmas [cat_cs_intros] = 𝒵.ntcf_pointed_NTMap_app_is_iso_arr'

lemmas (in 𝒵) ntcf_pointed_NTMap_app_is_arr'[cat_cs_intros] = 
  is_iso_arrD(1)[OF 𝒵.ntcf_pointed_NTMap_app_is_iso_arr']

lemmas [cat_cs_intros] = 𝒵.ntcf_pointed_NTMap_app_is_arr'


subsubsection‹Pointed natural transformation is a natural isomorphism›

lemma (in 𝒵) ntcf_pointed_is_iso_ntcf:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
  shows "ntcf_pointed α 𝔞 :
    Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-) ↦⇩C⇩F⇩.⇩i⇩s⇩o cf_id (cat_Set α) :
    cat_Set α ↦↦⇩C⇘α⇙ cat_Set α"
proof(intro is_iso_ntcfI is_ntcfI')

  note 𝔞 = assms[unfolded cat_Set_components(1)]
  from assms have set_𝔞: "set {𝔞} ∈⇩∘ cat_Set α⦇Obj⦈" 
    unfolding cat_Set_components by auto

  show "vfsequence (ntcf_pointed α 𝔞)" unfolding ntcf_pointed_def by auto
  show "vcard (ntcf_pointed α 𝔞) = 5⇩ℕ"
    unfolding ntcf_pointed_def by (auto simp: nat_omega_simps)
  from assms set_𝔞 show 
    "Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-) : cat_Set α ↦↦⇩C⇘α⇙ cat_Set α"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "ntcf_pointed α 𝔞⦇NTMap⦈⦇a⦈ :
    Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-)⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set α⇙
    cf_id (cat_Set α)⦇ObjMap⦈⦇a⦈"
    if "a ∈⇩∘ cat_Set α⦇Obj⦈" for a
    using assms that set_𝔞
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
      )
  show 
    "ntcf_pointed α 𝔞⦇NTMap⦈⦇b⦈ ∘⇩A⇘cat_Set α⇙
      Hom⇩O⇩.⇩C⇘α⇙cat_Set α (set {𝔞},-)⦇ArrMap⦈⦇f⦈ =
        cf_id (cat_Set α)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ ntcf_pointed α 𝔞⦇NTMap⦈⦇a⦈"
    if "f : a ↦⇘cat_Set α⇙ b" for a b f
  proof-
    let ?pb = ‹ntcf_pointed α 𝔞⦇NTMap⦈⦇b⦈›
      and ?pa = ‹ntcf_pointed α 𝔞⦇NTMap⦈⦇a⦈›
      and ?hom = ‹cf_hom (cat_Set α) [cat_Set α⦇CId⦈⦇set {𝔞}⦈, f]⇩∘›
    from assms set_𝔞 that have pb_hom: 
      "?pb ∘⇩A⇘cat_Set α⇙ ?hom : Hom (cat_Set α) (set {𝔞}) a ↦⇘cat_Set α⇙ b"
      by 
        (
          cs_concl cs_shallow 
            cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
        )
    then have dom_lhs: 
      "𝒟⇩∘ ((?pb ∘⇩A⇘cat_Set α⇙ ?hom)⦇ArrVal⦈) = Hom (cat_Set α) (set {𝔞}) a"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    from assms set_𝔞 that have f_pa:
      "f ∘⇩A⇘cat_Set α⇙ ?pa : Hom (cat_Set α) (set {𝔞}) a ↦⇘cat_Set α⇙ b"
      by (cs_concl cs_intro: cat_cs_intros)
    then have dom_rhs: 
      "𝒟⇩∘ ((f ∘⇩A⇘cat_Set α⇙ ?pa)⦇ArrVal⦈) = Hom (cat_Set α) (set {𝔞}) a"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    have [cat_cs_simps]: "?pb ∘⇩A⇘cat_Set α⇙ ?hom = f ∘⇩A⇘cat_Set α⇙ ?pa"
    proof(rule arr_Set_eqI)
      from pb_hom show arr_Set_pb_hom: "arr_Set α (?pb ∘⇩A⇘cat_Set α⇙ ?hom)"
        by (auto dest: cat_Set_is_arrD(1))
      from f_pa show arr_Set_f_pa: "arr_Set α (f ∘⇩A⇘cat_Set α⇙ ?pa)"
        by (auto dest: cat_Set_is_arrD(1))
      show "(?pb ∘⇩A⇘cat_Set α⇙ ?hom)⦇ArrVal⦈ = (f ∘⇩A⇘cat_Set α⇙ ?pa)⦇ArrVal⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
        fix g assume "g : set {𝔞} ↦⇘cat_Set α⇙ a"
        with assms 𝔞 set_𝔞 that show 
          "(?pb ∘⇩A⇘cat_Set α⇙ ?hom)⦇ArrVal⦈⦇g⦈ = (f ∘⇩A⇘cat_Set α⇙ ?pa)⦇ArrVal⦈⦇g⦈"
          by
            (
              cs_concl cs_shallow
                cs_simp: V_cs_simps cat_cs_simps 
                cs_intro:
                  V_cs_intros cat_cs_intros cat_op_intros cat_prod_cs_intros
            )
      qed (use arr_Set_pb_hom arr_Set_f_pa in auto)
    qed (use pb_hom f_pa in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
    from assms that set_𝔞 show ?thesis
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
        )
  qed
  show "ntcf_pointed α 𝔞⦇NTMap⦈⦇a⦈ :
    Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-)⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘cat_Set α⇙
    cf_id (cat_Set α)⦇ObjMap⦈⦇a⦈"
    if "a ∈⇩∘ cat_Set α⦇Obj⦈" for a
    using assms 𝔞 set_𝔞 that
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
      )

qed (auto simp: ntcf_pointed_components intro: cat_cs_intros)

lemma (in 𝒵) ntcf_pointed_is_iso_ntcf'[cat_cs_intros]:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
    and "𝔉' = Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-)"
    and "𝔊' = cf_id (cat_Set α)"
    and "𝔄' = cat_Set α"
    and "𝔅' = cat_Set α"
    and "α' = α"
  shows "ntcf_pointed α 𝔞 : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
  using assms(1) unfolding assms(2-6) by (rule ntcf_pointed_is_iso_ntcf)

lemmas [cat_cs_intros] = 𝒵.ntcf_pointed_is_iso_ntcf'



subsection‹Inverse pointed natural transformation›


subsubsection‹Definition and elementary properties›


text‹See Chapter III-2 in \<^cite>‹"mac_lane_categories_2010"›.›

definition ntcf_pointed_inv :: "V ⇒ V ⇒ V"
  where "ntcf_pointed_inv α 𝔞 =
    [
      (
        λX∈⇩∘cat_Set α⦇Obj⦈.
          [(λx∈⇩∘X. ntcf_paa 𝔞 X x), X, Hom (cat_Set α) (set {𝔞}) X]⇩∘
      ),
      cf_id (cat_Set α),
      Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-),
      cat_Set α,
      cat_Set α
    ]⇩∘"


text‹Components.›

lemma ntcf_pointed_inv_components:
  shows "ntcf_pointed_inv α 𝔞⦇NTMap⦈ =
      (
        λX∈⇩∘cat_Set α⦇Obj⦈.
          [(λx∈⇩∘X. ntcf_paa 𝔞 X x), X, Hom (cat_Set α) (set {𝔞}) X]⇩∘
      )"
    and [cat_cs_simps]: "ntcf_pointed_inv α 𝔞⦇NTDom⦈ = cf_id (cat_Set α)"
    and [cat_cs_simps]: 
      "ntcf_pointed_inv α 𝔞⦇NTCod⦈ = Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-)"
    and [cat_cs_simps]: "ntcf_pointed_inv α 𝔞⦇NTDGDom⦈ = cat_Set α"
    and [cat_cs_simps]: "ntcf_pointed_inv α 𝔞⦇NTDGCod⦈ = cat_Set α"
  unfolding ntcf_pointed_inv_def nt_field_simps
  by (simp_all add: nat_omega_simps)


subsubsection‹Natural transformation map›

mk_VLambda ntcf_pointed_inv_components(1)
  |vsv ntcf_pointed_inv_NTMap_vsv[cat_cs_intros]|
  |vdomain ntcf_pointed_inv_NTMap_vdomain[cat_cs_simps]|
  |app ntcf_pointed_inv_NTMap_app'|

lemma (in 𝒵) ntcf_pointed_inv_NTMap_app_ArrVal_app[cat_cs_simps]: 
  assumes "X ∈⇩∘ cat_Set α⦇Obj⦈" and "x ∈⇩∘ X"
  shows "ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈⦇x⦈ = ntcf_paa 𝔞 X x"
  by 
    (
      simp add: 
        assms(2) ntcf_pointed_inv_NTMap_app'[OF assms(1)] arr_Rel_components
    )

lemma (in 𝒵) ntcf_pointed_inv_NTMap_app_is_arr: 
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈" and "X ∈⇩∘ cat_Set α⦇Obj⦈"
  shows "ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈ :
    X ↦⇘cat_Set α⇙ Hom (cat_Set α) (set {𝔞}) X"
proof-
  interpret Set: category α ‹cat_Set α› by (rule category_cat_Set)
  note app_X = ntcf_pointed_inv_NTMap_app'[OF assms(2)]
  show ?thesis 
  proof(intro cat_Set_is_arrI arr_SetI)
    show ArrVal_vsv: "vsv (ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈)"
      unfolding app_X arr_Rel_components by simp
    show "vcard (ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈) = 3⇩ℕ"
      unfolding app_X arr_Rel_components by (simp add: nat_omega_simps)
    show ArrVal_vdomain: 
      "𝒟⇩∘ (ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈) =
        ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈⦇ArrDom⦈"
      unfolding app_X arr_Rel_components by simp
    from assms show vrange_left: 
      "ℛ⇩∘ (ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈⦇ArrVal⦈) ⊆⇩∘
        ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈⦇ArrCod⦈"
      unfolding app_X arr_Rel_components by (auto intro: cat_cs_intros)
    from assms show "ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈⦇ArrCod⦈ ∈⇩∘ Vset α"
      unfolding app_X arr_Rel_components cat_Set_components(1) 
      by (intro Set.cat_Hom_in_Vset[OF _ assms(2)])
        (auto simp: cat_Set_components(1))  
  qed (use assms in ‹auto simp: app_X arr_Rel_components cat_Set_components(1)›)
qed

lemma (in 𝒵) ntcf_pointed_inv_NTMap_app_is_arr'[cat_cs_intros]: 
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈" 
    and "X ∈⇩∘ cat_Set α⦇Obj⦈"
    and "A' = X"
    and "B' = Hom (cat_Set α) (set {𝔞}) X"
    and "ℭ' = cat_Set α"
  shows "ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈ : A' ↦⇘ℭ'⇙ B'"
  using assms(1,2) 
  unfolding assms(3-5) 
  by (rule ntcf_pointed_inv_NTMap_app_is_arr)

lemmas [cat_cs_intros] = 𝒵.ntcf_pointed_inv_NTMap_app_is_arr'

lemma (in 𝒵) is_inverse_ntcf_pointed_inv_NTMap_app:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈" and "X ∈⇩∘ cat_Set α⦇Obj⦈"
  shows 
    "is_inverse
      (cat_Set α)
      (ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇X⦈)
      (ntcf_pointed α 𝔞⦇NTMap⦈⦇X⦈)"
  (is ‹is_inverse (cat_Set α) ?bwd ?fwd›)
proof(intro is_inverseI)

  let ?Hom = ‹Hom (cat_Set α) (set {𝔞}) X›

  interpret Set: category α ‹cat_Set α› by (rule category_cat_Set)

  from assms(1) have set_𝔞: "set {𝔞} ∈⇩∘ cat_Set α⦇Obj⦈"
    unfolding cat_Set_components(1) by blast
  have Hom_𝔞X: "?Hom ∈⇩∘ cat_Set α⦇Obj⦈"
     by
       (
         auto 
          simp: cat_Set_components(1) 
          intro!: Set.cat_Hom_in_Vset set_𝔞 assms(2)
       )

  from assms show "?bwd : X ↦⇘cat_Set α⇙ ?Hom"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from assms show "?fwd : ?Hom ↦⇘cat_Set α⇙ X"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)

  from assms set_𝔞 Hom_𝔞X have lhs_is_arr:
    "?bwd ∘⇩A⇘cat_Set α⇙ ?fwd : ?Hom ↦⇘cat_Set α⇙ ?Hom"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  then have dom_lhs: "𝒟⇩∘ ((?bwd ∘⇩A⇘cat_Set α⇙ ?fwd)⦇ArrVal⦈) = ?Hom"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)

  from Hom_𝔞X have rhs_is_arr: "cat_Set α⦇CId⦈⦇?Hom⦈ : ?Hom ↦⇘cat_Set α⇙ ?Hom"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  then have dom_rhs: "𝒟⇩∘ ((cat_Set α⦇CId⦈⦇?Hom⦈)⦇ArrVal⦈) = ?Hom"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)

  show "?bwd ∘⇩A⇘cat_Set α⇙ ?fwd = cat_Set α⦇CId⦈⦇?Hom⦈"
  proof(rule arr_Set_eqI)
    from lhs_is_arr show arr_Set_lhs: "arr_Set α (?bwd ∘⇩A⇘cat_Set α⇙ ?fwd)"
      by (auto dest: cat_Set_is_arrD)
    from rhs_is_arr show arr_Set_rhs: "arr_Set α (cat_Set α⦇CId⦈⦇?Hom⦈)"
      by (auto dest: cat_Set_is_arrD)
    show "(?bwd ∘⇩A⇘cat_Set α⇙ ?fwd)⦇ArrVal⦈ = cat_Set α⦇CId⦈⦇?Hom⦈⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
      fix F assume "F : set {𝔞} ↦⇘cat_Set α⇙ X"
      with assms Hom_𝔞X show 
        "(?bwd ∘⇩A⇘cat_Set α⇙ ?fwd)⦇ArrVal⦈⦇F⦈ = cat_Set α⦇CId⦈⦇?Hom⦈⦇ArrVal⦈⦇F⦈"
        by
          (
            cs_concl  
              cs_simp: cat_cs_simps ntcf_paa_ArrVal
              cs_intro: V_cs_intros cat_Set_cs_intros cat_cs_intros
          )
    qed (use arr_Set_lhs arr_Set_rhs in auto)
  qed (use lhs_is_arr rhs_is_arr in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+

  from assms have lhs_is_arr: "?fwd ∘⇩A⇘cat_Set α⇙ ?bwd : X ↦⇘cat_Set α⇙ X"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  then have dom_lhs: "𝒟⇩∘ ((?fwd ∘⇩A⇘cat_Set α⇙ ?bwd)⦇ArrVal⦈) = X"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)

  from assms have rhs_is_arr: "cat_Set α⦇CId⦈⦇X⦈ : X ↦⇘cat_Set α⇙ X"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  then have dom_rhs: "𝒟⇩∘ ((cat_Set α⦇CId⦈⦇X⦈)⦇ArrVal⦈) = X"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)

  show "?fwd ∘⇩A⇘cat_Set α⇙ ?bwd = cat_Set α⦇CId⦈⦇X⦈"
  proof(rule arr_Set_eqI)
    from lhs_is_arr show arr_Set_lhs: "arr_Set α (?fwd ∘⇩A⇘cat_Set α⇙ ?bwd)"
      by (auto dest: cat_Set_is_arrD)
    from rhs_is_arr show arr_Set_rhs: "arr_Set α (cat_Set α⦇CId⦈⦇X⦈)"
      by (auto dest: cat_Set_is_arrD)
    show "(?fwd ∘⇩A⇘cat_Set α⇙ ?bwd)⦇ArrVal⦈ = cat_Set α⦇CId⦈⦇X⦈⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix x assume "x ∈⇩∘ X"
      with assms show 
        "(?fwd ∘⇩A⇘cat_Set α⇙ ?bwd)⦇ArrVal⦈⦇x⦈ = cat_Set α⦇CId⦈⦇X⦈⦇ArrVal⦈⦇x⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed (use arr_Set_lhs arr_Set_rhs in auto)
  qed (use lhs_is_arr rhs_is_arr in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+

qed


subsubsection‹Inverse pointed natural transformation is a natural isomorphism›

lemma (in 𝒵) ntcf_pointed_inv_is_ntcf:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
  shows "ntcf_pointed_inv α 𝔞 :
    cf_id (cat_Set α) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-) :
    cat_Set α ↦↦⇩C⇘α⇙ cat_Set α"
proof(intro is_ntcfI')

  interpret Set: category α ‹cat_Set α› by (rule category_cat_Set)

  note 𝔞 = assms[unfolded cat_Set_components(1)]
  from assms have set_𝔞: "set {𝔞} ∈⇩∘ cat_Set α⦇Obj⦈" 
    unfolding cat_Set_components by auto

  show "vfsequence (ntcf_pointed_inv α 𝔞)" 
    unfolding ntcf_pointed_inv_def by simp
  show "vcard (ntcf_pointed_inv α 𝔞) = 5⇩ℕ"
    unfolding ntcf_pointed_inv_def by (simp add: nat_omega_simps)
  from set_𝔞 show "Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-) : cat_Set α ↦↦⇩C⇘α⇙ cat_Set α"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)

  show "ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇a⦈ :
    cf_id (cat_Set α)⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set α⇙
    Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-)⦇ObjMap⦈⦇a⦈"
    if "a ∈⇩∘ cat_Set α⦇Obj⦈" for a
    using that assms set_𝔞
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
      )

  show 
    "ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇B⦈ ∘⇩A⇘cat_Set α⇙ cf_id (cat_Set α)⦇ArrMap⦈⦇F⦈ =
      Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-)⦇ArrMap⦈⦇F⦈ ∘⇩A⇘cat_Set α⇙
        ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇A⦈"
    if "F : A ↦⇘cat_Set α⇙ B" for A B F
  proof-
    let ?pb = ‹ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇B⦈›
      and ?pa = ‹ntcf_pointed_inv α 𝔞⦇NTMap⦈⦇A⦈›
      and ?hom = ‹cf_hom (cat_Set α) [cat_Set α⦇CId⦈⦇set {𝔞}⦈, F]⇩∘›
    from assms set_𝔞 that have pb_F: 
      "?pb ∘⇩A⇘cat_Set α⇙ F : A ↦⇘cat_Set α⇙ Hom (cat_Set α) (set {𝔞}) B"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_prod_cs_intros)
    then have dom_lhs: "𝒟⇩∘ ((?pb ∘⇩A⇘cat_Set α⇙ F)⦇ArrVal⦈) = A"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    from that assms set_𝔞 that have hom_pa:
      "?hom ∘⇩A⇘cat_Set α⇙ ?pa : A ↦⇘cat_Set α⇙ Hom (cat_Set α) (set {𝔞}) B"
      by (cs_concl cs_intro: cat_cs_intros cat_prod_cs_intros cat_op_intros)
    then have dom_rhs: "𝒟⇩∘ ((?hom ∘⇩A⇘cat_Set α⇙ ?pa)⦇ArrVal⦈) = A"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    have [cat_cs_simps]: "?pb ∘⇩A⇘cat_Set α⇙ F = ?hom ∘⇩A⇘cat_Set α⇙ ?pa"
    proof(rule arr_Set_eqI)
      from pb_F show arr_Set_pb_F: "arr_Set α (?pb ∘⇩A⇘cat_Set α⇙ F)"
        by (auto dest: cat_Set_is_arrD(1))
      from hom_pa show arr_Set_hom_pa: "arr_Set α (?hom ∘⇩A⇘cat_Set α⇙ ?pa)"
        by (auto dest: cat_Set_is_arrD(1))
      show "(?pb ∘⇩A⇘cat_Set α⇙ F)⦇ArrVal⦈ = (?hom ∘⇩A⇘cat_Set α⇙ ?pa)⦇ArrVal⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix a assume "a ∈⇩∘ A"
        with assms 𝔞 set_𝔞 that show 
          "(?pb ∘⇩A⇘cat_Set α⇙ F)⦇ArrVal⦈⦇a⦈ = (?hom ∘⇩A⇘cat_Set α⇙ ?pa)⦇ArrVal⦈⦇a⦈"
          by
            (
              cs_concl 
                cs_simp: cat_cs_simps
                cs_intro: 
                  cat_Set_cs_intros
                  cat_cs_intros
                  cat_prod_cs_intros
                  cat_op_intros
            )
      qed (use arr_Set_pb_F arr_Set_hom_pa in auto)
    qed (use pb_F hom_pa in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
    from assms that set_𝔞 show ?thesis
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
        )
  qed

qed (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+

lemma (in 𝒵) ntcf_pointed_inv_is_ntcf'[cat_cs_intros]:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
    and "𝔉' = cf_id (cat_Set α)"
    and "𝔊' = Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-)"
    and "𝔄' = cat_Set α"
    and "𝔅' = cat_Set α"
    and "α' = α"
  shows "ntcf_pointed_inv α 𝔞 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
  using assms(1) unfolding assms(2-6) by (rule ntcf_pointed_inv_is_ntcf)

lemmas [cat_cs_intros] = 𝒵.ntcf_pointed_inv_is_ntcf'

lemma (in 𝒵) inv_ntcf_ntcf_pointed[cat_cs_simps]:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
  shows "inv_ntcf (ntcf_pointed α 𝔞) = ntcf_pointed_inv α 𝔞"
  by 
    (
      rule iso_ntcf_if_is_inverse(3)[symmetric], 
      rule is_iso_ntcfD(1)[OF ntcf_pointed_is_iso_ntcf[OF assms]],
      rule ntcf_pointed_inv_is_ntcf[OF assms],
      rule is_inverse_ntcf_pointed_inv_NTMap_app[OF assms]
    )

lemma (in 𝒵) inv_ntcf_ntcf_pointed_inv[cat_cs_simps]:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
  shows "inv_ntcf (ntcf_pointed_inv α 𝔞) = ntcf_pointed α 𝔞"
  by
    (
      rule iso_ntcf_if_is_inverse(4)[symmetric], 
      rule is_iso_ntcfD(1)[OF ntcf_pointed_is_iso_ntcf[OF assms]],
      rule ntcf_pointed_inv_is_ntcf[OF assms],
      rule is_inverse_ntcf_pointed_inv_NTMap_app[OF assms]
    )

lemma (in 𝒵) ntcf_pointed_inv_is_iso_ntcf:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
  shows "ntcf_pointed_inv α 𝔞 :
    cf_id (cat_Set α) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-) :
    cat_Set α ↦↦⇩C⇘α⇙ cat_Set α"
  by
    (
      rule iso_ntcf_if_is_inverse(2), 
      rule is_iso_ntcfD(1)[OF ntcf_pointed_is_iso_ntcf[OF assms]],
      rule ntcf_pointed_inv_is_ntcf[OF assms],
      rule is_inverse_ntcf_pointed_inv_NTMap_app[OF assms]
    )

lemma (in 𝒵) ntcf_pointed_inv_is_iso_ntcf'[cat_cs_intros]:
  assumes "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
    and "𝔉' = cf_id (cat_Set α)"
    and "𝔊' = Hom⇩O⇩.⇩C⇘α⇙cat_Set α(set {𝔞},-)"
    and "𝔄' = cat_Set α"
    and "𝔅' = cat_Set α"
    and "α' = α"
  shows "ntcf_pointed_inv α 𝔞 : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
  using assms(1) unfolding assms(2-6) by (rule ntcf_pointed_inv_is_iso_ntcf)

lemmas [cat_cs_intros] = 𝒵.ntcf_pointed_inv_is_iso_ntcf'

text‹\newpage›

end