Theory CZH_ECAT_NTCF

(* Copyright 2021 (C) Mihails Milehins *)

section‹Natural transformation›
theory CZH_ECAT_NTCF
  imports 
    CZH_Foundations.CZH_SMC_NTSMCF
    CZH_ECAT_Functor
begin



subsection‹Background›

named_theorems ntcf_cs_simps
named_theorems ntcf_cs_intros

lemmas [cat_cs_simps] = dg_shared_cs_simps
lemmas [cat_cs_intros] = dg_shared_cs_intros


subsubsection‹Slicing›

definition ntcf_ntsmcf :: "V ⇒ V"
  where "ntcf_ntsmcf 𝔑 =
    [
      𝔑⦇NTMap⦈,
      cf_smcf (𝔑⦇NTDom⦈),
      cf_smcf (𝔑⦇NTCod⦈),
      cat_smc (𝔑⦇NTDGDom⦈),
      cat_smc (𝔑⦇NTDGCod⦈)
    ]⇩∘"


text‹Components.›

lemma ntcf_ntsmcf_components:
  shows [slicing_simps]: "ntcf_ntsmcf 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
    and [slicing_commute]: "ntcf_ntsmcf 𝔑⦇NTDom⦈ = cf_smcf (𝔑⦇NTDom⦈)"
    and [slicing_commute]: "ntcf_ntsmcf 𝔑⦇NTCod⦈ = cf_smcf (𝔑⦇NTCod⦈)"
    and [slicing_commute]: "ntcf_ntsmcf 𝔑⦇NTDGDom⦈ = cat_smc (𝔑⦇NTDGDom⦈)"
    and [slicing_commute]: "ntcf_ntsmcf 𝔑⦇NTDGCod⦈ = cat_smc (𝔑⦇NTDGCod⦈)"
  unfolding ntcf_ntsmcf_def nt_field_simps by (auto simp: nat_omega_simps)



subsection‹Definition and elementary properties›


text‹
The definition of a natural transformation that is used in this work is
is similar to the definition that can be found in Chapter I-4 in 
\<^cite>‹"mac_lane_categories_2010"›.
›

locale is_ntcf = 
  𝒵 α + 
  vfsequence 𝔑 + 
  NTDom: is_functor α 𝔄 𝔅 𝔉 + 
  NTCod: is_functor α 𝔄 𝔅 𝔊
  for α 𝔄 𝔅 𝔉 𝔊 𝔑 +
  assumes ntcf_length[cat_cs_simps]: "vcard 𝔑 = 5⇩ℕ"  
    and ntcf_is_ntsmcf[slicing_intros]: "ntcf_ntsmcf 𝔑 :
      cf_smcf 𝔉 ↦⇩S⇩M⇩C⇩F cf_smcf 𝔊 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc 𝔅"
    and ntcf_NTDom[cat_cs_simps]: "𝔑⦇NTDom⦈ = 𝔉"
    and ntcf_NTCod[cat_cs_simps]: "𝔑⦇NTCod⦈ = 𝔊"
    and ntcf_NTDGDom[cat_cs_simps]: "𝔑⦇NTDGDom⦈ = 𝔄"
    and ntcf_NTDGCod[cat_cs_simps]: "𝔑⦇NTDGCod⦈ = 𝔅"

syntax "_is_ntcf" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦⇩C⇩F _ :/ _ ↦↦⇩Cı _)› [51, 51, 51, 51, 51] 51)
translations "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" ⇌ "CONST is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑"

abbreviation all_ntcfs :: "V ⇒ V"
  where "all_ntcfs α ≡ set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"

abbreviation ntcfs :: "V ⇒ V ⇒ V ⇒ V"
  where "ntcfs α 𝔄 𝔅 ≡ set {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"

abbreviation these_ntcfs :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "these_ntcfs α 𝔄 𝔅 𝔉 𝔊 ≡ set {𝔑. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"

lemmas [cat_cs_simps] = 
  is_ntcf.ntcf_length
  is_ntcf.ntcf_NTDom
  is_ntcf.ntcf_NTCod
  is_ntcf.ntcf_NTDGDom
  is_ntcf.ntcf_NTDGCod

lemma (in is_ntcf) ntcf_is_ntsmcf':
  assumes "𝔉' = cf_smcf 𝔉"
    and "𝔊' = cf_smcf 𝔊"
    and "𝔄' = cat_smc 𝔄"
    and "𝔅' = cat_smc 𝔅"
  shows "ntcf_ntsmcf 𝔑 : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
  unfolding assms(1-4) by (rule ntcf_is_ntsmcf)

lemmas [slicing_intros] = is_ntcf.ntcf_is_ntsmcf'


text‹Rules.›

lemma (in is_ntcf) is_ntcf_axioms'[cat_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅" and "𝔉' = 𝔉" and "𝔊' = 𝔊"
  shows "𝔑 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_ntcf_axioms)

mk_ide rf is_ntcf_def[unfolded is_ntcf_axioms_def]
  |intro is_ntcfI|
  |dest is_ntcfD[dest]|
  |elim is_ntcfE[elim]|

lemmas [cat_cs_intros] = 
  is_ntcfD(3,4)

lemma is_ntcfI':
  assumes "𝒵 α"
    and "vfsequence 𝔑"
    and "vcard 𝔑 = 5⇩ℕ"
    and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑⦇NTDom⦈ = 𝔉"
    and "𝔑⦇NTCod⦈ = 𝔊"
    and "𝔑⦇NTDGDom⦈ = 𝔄"
    and "𝔑⦇NTDGCod⦈ = 𝔅"
    and "vsv (𝔑⦇NTMap⦈)"
    and "𝒟⇩∘ (𝔑⦇NTMap⦈) = 𝔄⦇Obj⦈"
    and "⋀a. a ∈⇩∘ 𝔄⦇Obj⦈ ⟹ 𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"
    and "⋀a b f. f : a ↦⇘𝔄⇙ b ⟹
      𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈"
  shows "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  by (intro is_ntcfI is_ntsmcfI', unfold ntcf_ntsmcf_components slicing_simps)
    (
      simp_all add: 
        assms nat_omega_simps 
        ntcf_ntsmcf_def  
        is_functorD(6)[OF assms(4)] 
        is_functorD(6)[OF assms(5)]
    )

lemma is_ntcfD':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝒵 α"
    and "vfsequence 𝔑"
    and "vcard 𝔑 = 5⇩ℕ"
    and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑⦇NTDom⦈ = 𝔉"
    and "𝔑⦇NTCod⦈ = 𝔊"
    and "𝔑⦇NTDGDom⦈ = 𝔄"
    and "𝔑⦇NTDGCod⦈ = 𝔅"
    and "vsv (𝔑⦇NTMap⦈)"
    and "𝒟⇩∘ (𝔑⦇NTMap⦈) = 𝔄⦇Obj⦈"
    and "⋀a. a ∈⇩∘ 𝔄⦇Obj⦈ ⟹ 𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"
    and "⋀a b f. f : a ↦⇘𝔄⇙ b ⟹
      𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈"
  by 
    (
      simp_all add: 
        is_ntcfD(2-10)[OF assms] 
        is_ntsmcfD'[OF is_ntcfD(6)[OF assms], unfolded slicing_simps]
    )

lemma is_ntcfE':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  obtains "𝒵 α"
    and "vfsequence 𝔑"
    and "vcard 𝔑 = 5⇩ℕ"
    and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑⦇NTDom⦈ = 𝔉"
    and "𝔑⦇NTCod⦈ = 𝔊"
    and "𝔑⦇NTDGDom⦈ = 𝔄"
    and "𝔑⦇NTDGCod⦈ = 𝔅"
    and "vsv (𝔑⦇NTMap⦈)"
    and "𝒟⇩∘ (𝔑⦇NTMap⦈) = 𝔄⦇Obj⦈"
    and "⋀a. a ∈⇩∘ 𝔄⦇Obj⦈ ⟹ 𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"
    and "⋀a b f. f : a ↦⇘𝔄⇙ b ⟹
      𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈"
  using assms by (simp add: is_ntcfD')


text‹Slicing.›

context is_ntcf
begin

interpretation ntsmcf: 
  is_ntsmcf α ‹cat_smc 𝔄› ‹cat_smc 𝔅› ‹cf_smcf 𝔉› ‹cf_smcf 𝔊› ‹ntcf_ntsmcf 𝔑›
  by (rule ntcf_is_ntsmcf)

lemmas_with [unfolded slicing_simps]:
  ntcf_NTMap_vsv(*not cat_cs_intros: clash*) = ntsmcf.ntsmcf_NTMap_vsv
  and ntcf_NTMap_vdomain[cat_cs_simps] = ntsmcf.ntsmcf_NTMap_vdomain
  and ntcf_NTMap_is_arr = ntsmcf.ntsmcf_NTMap_is_arr
  and ntcf_NTMap_is_arr'[cat_cs_intros] = ntsmcf.ntsmcf_NTMap_is_arr'

sublocale NTMap: vsv ‹𝔑⦇NTMap⦈›
  rewrites "𝒟⇩∘ (𝔑⦇NTMap⦈) = 𝔄⦇Obj⦈"
  by (rule ntcf_NTMap_vsv) (simp add: cat_cs_simps)

lemmas_with [unfolded slicing_simps]:
  ntcf_NTMap_app_in_Arr[cat_cs_intros] = ntsmcf.ntsmcf_NTMap_app_in_Arr
  and ntcf_NTMap_vrange_vifunion = ntsmcf.ntsmcf_NTMap_vrange_vifunion
  and ntcf_NTMap_vrange = ntsmcf.ntsmcf_NTMap_vrange
  and ntcf_NTMap_vsubset_Vset = ntsmcf.ntsmcf_NTMap_vsubset_Vset
  and ntcf_NTMap_in_Vset = ntsmcf.ntsmcf_NTMap_in_Vset
  and ntcf_is_ntsmcf_if_ge_Limit = ntsmcf.ntsmcf_is_ntsmcf_if_ge_Limit

lemmas_with [unfolded slicing_simps]:
  ntcf_Comp_commute[cat_cs_intros] = ntsmcf.ntsmcf_Comp_commute
  and ntcf_Comp_commute' = ntsmcf.ntsmcf_Comp_commute'
  and ntcf_Comp_commute'' = ntsmcf.ntsmcf_Comp_commute''

end

lemmas [cat_cs_simps] = is_ntcf.ntcf_NTMap_vdomain

lemmas [cat_cs_intros] = 
  is_ntcf.ntcf_NTMap_vsv
  is_ntcf.ntcf_NTMap_is_arr'
  ntsmcf_hcomp_NTMap_vsv


text‹Elementary properties.›

lemma ntcf_eqI:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
    and "𝔑⦇NTMap⦈ = 𝔑'⦇NTMap⦈"
    and "𝔉 = 𝔉'"
    and "𝔊 = 𝔊'"
    and "𝔄 = 𝔄'"
    and "𝔅 = 𝔅'"
  shows "𝔑 = 𝔑'"
proof-
  interpret L: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret R: is_ntcf α 𝔄' 𝔅' 𝔉' 𝔊' 𝔑' by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom: "𝒟⇩∘ 𝔑 = 5⇩ℕ" 
      by (cs_concl cs_shallow cs_simp: cat_cs_simps V_cs_simps)
    show "𝒟⇩∘ 𝔑 = 𝒟⇩∘ 𝔑'" 
      by (cs_concl cs_shallow cs_simp: cat_cs_simps V_cs_simps)
    from assms(4-7) have sup: 
      "𝔑⦇NTDom⦈ = 𝔑'⦇NTDom⦈" "𝔑⦇NTCod⦈ = 𝔑'⦇NTCod⦈" 
      "𝔑⦇NTDGDom⦈ = 𝔑'⦇NTDGDom⦈" "𝔑⦇NTDGCod⦈ = 𝔑'⦇NTDGCod⦈" 
      by (simp_all add: cat_cs_simps)
    show "a ∈⇩∘ 𝒟⇩∘ 𝔑 ⟹ 𝔑⦇a⦈ = 𝔑'⦇a⦈" for a
      by (unfold dom, elim_in_numeral, insert assms(3) sup) 
        (auto simp: nt_field_simps)
  qed auto
qed

lemma ntcf_ntsmcf_eqI:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
    and "𝔉 = 𝔉'"
    and "𝔊 = 𝔊'"
    and "𝔄 = 𝔄'"
    and "𝔅 = 𝔅'"
    and "ntcf_ntsmcf 𝔑 = ntcf_ntsmcf 𝔑'"
  shows "𝔑 = 𝔑'"
proof(rule ntcf_eqI[of α])
  from assms(7) have "ntcf_ntsmcf 𝔑⦇NTMap⦈ = ntcf_ntsmcf 𝔑'⦇NTMap⦈" by simp
  then show "𝔑⦇NTMap⦈ = 𝔑'⦇NTMap⦈" unfolding slicing_simps by simp_all
  from assms(3-6) show "𝔉 = 𝔉'" "𝔊 = 𝔊'" "𝔄 = 𝔄'" "𝔅 = 𝔅'" by simp_all
qed (auto simp: assms(1,2))

lemma (in is_ntcf) ntcf_def:
  "𝔑 = [𝔑⦇NTMap⦈, 𝔑⦇NTDom⦈, 𝔑⦇NTCod⦈, 𝔑⦇NTDGDom⦈, 𝔑⦇NTDGCod⦈]⇩∘"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ 𝔑 = 5⇩ℕ" 
    by (cs_concl cs_shallow cs_simp: cat_cs_simps V_cs_simps)
  have dom_rhs:
    "𝒟⇩∘ [𝔑⦇NTMap⦈, 𝔑⦇NTDGDom⦈, 𝔑⦇NTDGCod⦈, 𝔑⦇NTDom⦈, 𝔑⦇NTCod⦈]⇩∘ = 5⇩ℕ"
    by (simp add: nat_omega_simps)
  then show 
    "𝒟⇩∘ 𝔑 = 𝒟⇩∘ [𝔑⦇NTMap⦈, 𝔑⦇NTDom⦈, 𝔑⦇NTCod⦈, 𝔑⦇NTDGDom⦈, 𝔑⦇NTDGCod⦈]⇩∘"
    unfolding dom_lhs dom_rhs by (simp add: nat_omega_simps)
  show "a ∈⇩∘ 𝒟⇩∘ 𝔑 ⟹
    𝔑⦇a⦈ = [𝔑⦇NTMap⦈, 𝔑⦇NTDom⦈, 𝔑⦇NTCod⦈, 𝔑⦇NTDGDom⦈, 𝔑⦇NTDGCod⦈]⇩∘⦇a⦈" 
    for a
    by (unfold dom_lhs, elim_in_numeral, unfold nt_field_simps)
      (simp_all add: nat_omega_simps)
qed (auto simp: vsv_axioms)

lemma (in is_ntcf) ntcf_in_Vset: 
  assumes "𝒵 β" and "α ∈⇩∘ β"  
  shows "𝔑 ∈⇩∘ Vset β"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  note [cat_cs_intros] = 
    ntcf_NTMap_in_Vset
    NTDom.cf_in_Vset
    NTCod.cf_in_Vset
    NTDom.HomDom.cat_in_Vset
    NTDom.HomCod.cat_in_Vset
  from assms(2) show ?thesis
    by (subst ntcf_def) 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros V_cs_intros
      )
qed

lemma (in is_ntcf) ntcf_is_ntcf_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘β⇙ 𝔅"
proof(intro is_ntcfI)
  show "ntcf_ntsmcf 𝔑 :
    cf_smcf 𝔉 ↦⇩S⇩M⇩C⇩F cf_smcf 𝔊 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘β⇙ cat_smc 𝔅"
    by (rule is_ntsmcf.ntsmcf_is_ntsmcf_if_ge_Limit[OF ntcf_is_ntsmcf assms])
qed 
  (
    cs_concl cs_shallow 
      cs_simp: cat_cs_simps 
      cs_intro:
        V_cs_intros
        assms 
        NTDom.cf_is_functor_if_ge_Limit
        NTCod.cf_is_functor_if_ge_Limit
   )+

lemma small_all_ntcfs[simp]:
  "small {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
proof(cases ‹𝒵 α›)
  case True
  from is_ntcf.ntcf_in_Vset show ?thesis
    by (intro down[of _ ‹Vset (α + ω)›])
      (auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
  case False
  then have "{𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅} = {}" by auto
  then show ?thesis by simp
qed

lemma small_ntcfs[simp]: "small {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
  by (rule down[of _ ‹set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}›]) auto

lemma small_these_ntcfs[simp]: "small {𝔑. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
  by (rule down[of _ ‹set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}›]) auto


text‹Further elementary results.›

lemma these_ntcfs_iff: (*not simp*) 
  "𝔑 ∈⇩∘ these_ntcfs α 𝔄 𝔅 𝔉 𝔊 ⟷ 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  by auto



subsection‹Opposite natural transformation›


text‹See section 1.5 in \<^cite>‹"bodo_categories_1970"›.›

definition op_ntcf :: "V ⇒ V"
  where "op_ntcf 𝔑 = 
    [
      𝔑⦇NTMap⦈, 
      op_cf (𝔑⦇NTCod⦈), 
      op_cf (𝔑⦇NTDom⦈), 
      op_cat (𝔑⦇NTDGDom⦈), 
      op_cat (𝔑⦇NTDGCod⦈)
    ]⇩∘"


text‹Components.›

lemma op_ntcf_components[cat_op_simps]:
  shows "op_ntcf 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
    and "op_ntcf 𝔑⦇NTDom⦈ = op_cf (𝔑⦇NTCod⦈)"
    and "op_ntcf 𝔑⦇NTCod⦈ = op_cf (𝔑⦇NTDom⦈)"
    and "op_ntcf 𝔑⦇NTDGDom⦈ = op_cat (𝔑⦇NTDGDom⦈)"
    and "op_ntcf 𝔑⦇NTDGCod⦈ = op_cat (𝔑⦇NTDGCod⦈)"
  unfolding op_ntcf_def nt_field_simps by (auto simp: nat_omega_simps)


text‹Slicing.›

lemma ntcf_ntsmcf_op_ntcf[slicing_commute]: 
  "op_ntsmcf (ntcf_ntsmcf 𝔑) = ntcf_ntsmcf (op_ntcf 𝔑)"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ (op_ntsmcf (ntcf_ntsmcf 𝔑)) = 5⇩ℕ"
    unfolding op_ntsmcf_def by (auto simp: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (ntcf_ntsmcf (op_ntcf 𝔑)) = 5⇩ℕ"
    unfolding ntcf_ntsmcf_def by (auto simp: nat_omega_simps)
  show "𝒟⇩∘ (op_ntsmcf (ntcf_ntsmcf 𝔑)) = 𝒟⇩∘ (ntcf_ntsmcf (op_ntcf 𝔑))"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ (op_ntsmcf (ntcf_ntsmcf 𝔑)) ⟹ 
    op_ntsmcf (ntcf_ntsmcf 𝔑)⦇a⦈ = ntcf_ntsmcf (op_ntcf 𝔑)⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs,
        elim_in_numeral,
        unfold nt_field_simps ntcf_ntsmcf_def op_ntcf_def op_ntsmcf_def
      )
      (auto simp: nat_omega_simps slicing_commute[symmetric])
qed (auto simp: ntcf_ntsmcf_def op_ntsmcf_def)


text‹Elementary properties.›

lemma op_ntcf_vsv[cat_op_intros]: "vsv (op_ntcf 𝔉)" 
  unfolding op_ntcf_def by auto


subsubsection‹Further properties›

lemma (in is_ntcf) is_ntcf_op: 
  "op_ntcf 𝔑 : op_cf 𝔊 ↦⇩C⇩F op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇘α⇙ op_cat 𝔅"
proof(rule is_ntcfI, unfold cat_op_simps)
  show "vfsequence (op_ntcf 𝔑)" by (simp add: op_ntcf_def)
  show "vcard (op_ntcf 𝔑) = 5⇩ℕ" by (simp add: op_ntcf_def nat_omega_simps)
qed
  (
    use is_ntcf_axioms in
    ‹
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps slicing_commute[symmetric]
        cs_intro: cat_cs_intros cat_op_intros smc_op_intros slicing_intros
    ›
  )+

lemma (in is_ntcf) is_ntcf_op'[cat_op_intros]:
  assumes "𝔊' = op_cf 𝔊"
    and "𝔉' = op_cf 𝔉"
    and "𝔄' = op_cat 𝔄"
    and "𝔅' = op_cat 𝔅"
  shows "op_ntcf 𝔑 : 𝔊' ↦⇩C⇩F 𝔉' : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
  unfolding assms by (rule is_ntcf_op)

lemmas [cat_op_intros] = is_ntcf.is_ntcf_op'

lemma (in is_ntcf) ntcf_op_ntcf_op_ntcf[cat_op_simps]: 
  "op_ntcf (op_ntcf 𝔑) = 𝔑"
proof(rule ntcf_eqI[of α 𝔄 𝔅 𝔉 𝔊 _ 𝔄 𝔅 𝔉 𝔊], unfold cat_op_simps)
  interpret op: 
    is_ntcf α ‹op_cat 𝔄› ‹op_cat 𝔅› ‹op_cf 𝔊› ‹op_cf 𝔉› ‹op_ntcf 𝔑›
    by (rule is_ntcf_op)
  from op.is_ntcf_op show 
    "op_ntcf (op_ntcf 𝔑) : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (simp add: cat_op_simps)
qed (auto simp: cat_cs_intros)

lemmas ntcf_op_ntcf_op_ntcf[cat_op_simps] = 
  is_ntcf.ntcf_op_ntcf_op_ntcf

lemma eq_op_ntcf_iff[cat_op_simps]: 
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
  shows "op_ntcf 𝔑 = op_ntcf 𝔑' ⟷ 𝔑 = 𝔑'"
proof
  interpret L: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret R: is_ntcf α 𝔄' 𝔅' 𝔉' 𝔊' 𝔑' by (rule assms(2))
  assume prems: "op_ntcf 𝔑 = op_ntcf 𝔑'"
  show "𝔑 = 𝔑'"
  proof(rule ntcf_eqI[OF assms])
    from prems L.ntcf_op_ntcf_op_ntcf R.ntcf_op_ntcf_op_ntcf show 
      "𝔑⦇NTMap⦈ = 𝔑'⦇NTMap⦈"
      by metis+
    from prems L.ntcf_op_ntcf_op_ntcf R.ntcf_op_ntcf_op_ntcf 
    have "𝔑⦇NTDom⦈ = 𝔑'⦇NTDom⦈" 
      and "𝔑⦇NTCod⦈ = 𝔑'⦇NTCod⦈" 
      and "𝔑⦇NTDGDom⦈ = 𝔑'⦇NTDGDom⦈" 
      and "𝔑⦇NTDGCod⦈ = 𝔑'⦇NTDGCod⦈" 
      by metis+
    then show "𝔉 = 𝔉'" "𝔊 = 𝔊'" "𝔄 = 𝔄'" "𝔅 = 𝔅'" 
      by (auto simp: cat_cs_simps)
  qed
qed auto



subsection‹Vertical composition of natural transformations›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-4 in \<^cite>‹"mac_lane_categories_2010"›.›

abbreviation (input) ntcf_vcomp :: "V ⇒ V ⇒ V" (infixl ‹∙⇩N⇩T⇩C⇩F› 55)
  where "ntcf_vcomp ≡ ntsmcf_vcomp"

lemmas [cat_cs_simps] = ntsmcf_vcomp_components(2-5)


text‹Slicing.›

lemma ntcf_ntsmcf_ntcf_vcomp[slicing_commute]: 
  "ntcf_ntsmcf 𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑 = ntcf_ntsmcf (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)"
  unfolding 
    ntsmcf_vcomp_def ntcf_ntsmcf_def cat_smc_def nt_field_simps dg_field_simps 
  by (simp add: nat_omega_simps)


subsubsection‹Natural transformation map›

lemma ntcf_vcomp_NTMap_vdomain[cat_cs_simps]:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝒟⇩∘ ((𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈) = 𝔄⦇Obj⦈"
proof-
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 using assms by auto
  show ?thesis
    by 
      (
        rule ntsmcf_vcomp_NTMap_vdomain
          [
            OF 𝔑.ntcf_is_ntsmcf, 
            of ‹ntcf_ntsmcf 𝔐›,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma ntcf_vcomp_NTMap_app[cat_cs_simps]:
  assumes "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "a ∈⇩∘ 𝔄⦇Obj⦈" 
  shows "(𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ = 𝔐⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈"
proof-
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔊 ℌ 𝔐 using assms by clarsimp
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 using assms by clarsimp
  show ?thesis
    by 
      (
        rule ntsmcf_vcomp_NTMap_app
          [
            OF 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf, 
            unfolded slicing_commute slicing_simps,
            OF assms(3)
          ]
      )
qed

lemma ntcf_vcomp_NTMap_vrange:
  assumes "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈) ⊆⇩∘ 𝔅⦇Arr⦈"
proof-
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔊 ℌ 𝔐 using assms by auto
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 using assms by auto
  show ?thesis
    by 
      (
        rule 
          ntsmcf_vcomp_NTMap_vrange[
            OF 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed


subsubsection‹Further properties›

lemma ntcf_vcomp_composable_commute[cat_cs_simps]:
  ―‹See Chapter II-4 in \cite{mac_lane_categories_2010}.›
  assumes "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and [intro]: "f : a ↦⇘𝔄⇙ b"
  shows 
    "(𝔐⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇b⦈) ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 
      ℌ⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ (𝔐⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈)"
proof-
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(1)) 
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis
    by 
      (
        rule ntsmcf_vcomp_composable_commute[
            OF 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf, 
            unfolded slicing_simps,
            OF assms(3)
          ]
      )
qed 

lemma ntcf_vcomp_is_ntcf[cat_cs_intros]:
  ―‹see Chapter II-4 in \cite{mac_lane_categories_2010}.›
  assumes "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 : 𝔉 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof-
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis 
  proof(intro is_ntcfI)
    show "vfsequence (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)" by (simp add: ntsmcf_vcomp_def)
    show "vcard (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) = 5⇩ℕ"
      unfolding ntsmcf_vcomp_def by (simp add: nat_omega_simps)
    show "ntcf_ntsmcf (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) : 
      cf_smcf 𝔉 ↦⇩S⇩M⇩C⇩F cf_smcf ℌ : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc 𝔅"
      by 
        (
          rule ntsmcf_vcomp_is_ntsmcf[
            OF 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf, 
            unfolded slicing_simps slicing_commute
            ]
        )
  qed (auto simp: ntsmcf_vcomp_components(1) cat_cs_simps cat_cs_intros)
qed

lemma ntcf_vcomp_assoc[cat_cs_simps]:
  ―‹See Chapter II-4 in \cite{mac_lane_categories_2010}.›
  assumes "𝔏 : ℌ ↦⇩C⇩F 𝔎 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "(𝔏 ∙⇩N⇩T⇩C⇩F 𝔐) ∙⇩N⇩T⇩C⇩F 𝔑 = 𝔏 ∙⇩N⇩T⇩C⇩F (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)"
proof-
  interpret 𝔏: is_ntcf α 𝔄 𝔅 ℌ 𝔎 𝔏 by (rule assms(1))
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(2))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(3))
  show ?thesis
  proof(rule ntcf_eqI[of α])
    from ntsmcf_vcomp_assoc[
        OF 𝔏.ntcf_is_ntsmcf 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf,
        unfolded slicing_simps slicing_commute
      ]
    have 
      "ntcf_ntsmcf (𝔏 ∙⇩N⇩T⇩C⇩F 𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈ =
        ntcf_ntsmcf (𝔏 ∙⇩N⇩T⇩C⇩F (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈"
      by simp
    then show "(𝔏 ∙⇩N⇩T⇩C⇩F 𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈ = (𝔏 ∙⇩N⇩T⇩C⇩F (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈"
      unfolding slicing_simps .
  qed (auto intro: cat_cs_intros)
qed


subsubsection‹
The opposite of the vertical composition of natural transformations
›

lemma op_ntcf_ntcf_vcomp[cat_op_simps]: 
  assumes "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "op_ntcf (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) = op_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F op_ntcf 𝔐"
proof-
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔊 ℌ 𝔐 using assms(1) by auto
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 using assms(2) by auto
  show ?thesis
  proof(rule sym, rule ntcf_eqI[of α])
    from 
      op_ntsmcf_ntsmcf_vcomp
        [
          OF 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf, 
          unfolded slicing_simps slicing_commute
        ]
    have "ntcf_ntsmcf (op_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F op_ntcf 𝔐)⦇NTMap⦈ = 
      ntcf_ntsmcf (op_ntcf (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈"
      by simp
    then show "(op_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F op_ntcf 𝔐)⦇NTMap⦈ = op_ntcf (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈"
      unfolding slicing_simps .
  qed (auto intro: cat_cs_intros cat_op_intros)
qed



subsection‹Horizontal composition of natural transformations›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-5 in \<^cite>‹"mac_lane_categories_2010"›.›

abbreviation (input) ntcf_hcomp :: "V ⇒ V ⇒ V" (infixl ‹∘⇩N⇩T⇩C⇩F› 55)
  where "ntcf_hcomp ≡ ntsmcf_hcomp"

lemmas [cat_cs_simps] = ntsmcf_hcomp_components(2-5)


text‹Slicing.›

lemma ntcf_ntsmcf_ntcf_hcomp[slicing_commute]: 
  "ntcf_ntsmcf 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑 = ntcf_ntsmcf (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)"
proof(rule vsv_eqI)
  show "vsv (ntcf_ntsmcf 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑)"
    unfolding ntsmcf_hcomp_def by auto
  show "vsv (ntcf_ntsmcf (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑))" unfolding ntcf_ntsmcf_def by auto
  have dom_lhs: 
    "𝒟⇩∘ (ntcf_ntsmcf 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑) = 5⇩ℕ" 
    unfolding ntsmcf_hcomp_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (ntcf_ntsmcf (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)) = 5⇩ℕ"
    unfolding ntcf_ntsmcf_def by (simp add: nat_omega_simps)
  show "𝒟⇩∘ (ntcf_ntsmcf 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑) = 
    𝒟⇩∘ (ntcf_ntsmcf (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑))"
    unfolding dom_lhs dom_rhs ..
  fix a assume "a ∈⇩∘ 𝒟⇩∘ (ntcf_ntsmcf 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑)"
  then show 
    "(ntcf_ntsmcf 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑)⦇a⦈ = ntcf_ntsmcf (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)⦇a⦈"
    unfolding dom_lhs
    by (elim_in_numeral; fold nt_field_simps) 
      (simp_all add: ntsmcf_hcomp_components slicing_simps slicing_commute)
qed


subsubsection‹Natural transformation map›

lemma ntcf_hcomp_NTMap_vdomain[cat_cs_simps]: 
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝒟⇩∘ ((𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈) = 𝔄⦇Obj⦈"
proof-
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  show ?thesis unfolding ntsmcf_hcomp_components by (simp add: cat_cs_simps)
qed

lemma ntcf_hcomp_NTMap_app[cat_cs_simps]:
  assumes "𝔐 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "a ∈⇩∘ 𝔄⦇Obj⦈" 
  shows "(𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ =
    𝔊'⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇a⦈⦈ ∘⇩A⇘ℭ⇙ 𝔐⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
  interpret 𝔐: is_ntcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  from assms(3) show ?thesis 
    unfolding ntsmcf_hcomp_components by (simp add: cat_cs_simps)
qed

lemma ntcf_hcomp_NTMap_vrange:
  assumes "𝔐 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
  interpret 𝔐: is_ntcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis
    by 
      (
        rule ntsmcf_hcomp_NTMap_vrange[
          OF 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf, 
          unfolded slicing_simps slicing_commute
          ]
      )
qed


subsubsection‹Further properties›

lemma ntcf_hcomp_composable_commute:
  ―‹See Chapter II-5 in \cite{mac_lane_categories_2010}.›
  assumes "𝔐 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "f : a ↦⇘𝔄⇙ b" 
  shows 
    "(𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ (𝔉' ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ = 
      (𝔊' ∘⇩C⇩F 𝔊)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈"
    (is ‹?𝔐𝔑b ∘⇩A⇘ℭ⇙ ?𝔉'𝔉f = ?𝔊'𝔊f ∘⇩A⇘ℭ⇙ ?𝔐𝔑a›)
proof-
  interpret 𝔐: is_ntcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis
    by 
      (
        rule ntsmcf_hcomp_composable_commute[
          OF 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf,
          unfolded slicing_simps slicing_commute, 
          OF assms(3)
          ]
      )
qed

lemma ntcf_hcomp_is_ntcf:
  ―‹See Chapter II-5 in \cite{mac_lane_categories_2010}.›
  assumes "𝔐 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔐 ∘⇩N⇩T⇩C⇩F 𝔑 : 𝔉' ∘⇩C⇩F 𝔉 ↦⇩C⇩F 𝔊' ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔐: is_ntcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis
  proof(intro is_ntcfI) 
    show "vfsequence (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)"
      unfolding ntsmcf_hcomp_def by (simp add: nat_omega_simps)
    show "vcard (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑) = 5⇩ℕ"
      unfolding ntsmcf_hcomp_def by (simp add: nat_omega_simps)
    show "ntcf_ntsmcf (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑) : 
      cf_smcf (𝔉' ∘⇩S⇩M⇩C⇩F 𝔉) ↦⇩S⇩M⇩C⇩F cf_smcf (𝔊' ∘⇩C⇩F 𝔊) : 
      cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
      by 
        (
          rule ntsmcf_hcomp_is_ntsmcf[
            OF 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf, 
            unfolded slicing_simps slicing_commute
            ]
        )
  qed (auto simp: ntsmcf_hcomp_components(1) cat_cs_simps intro: cat_cs_intros)
qed

lemma ntcf_hcomp_is_ntcf'[cat_cs_intros]:
  assumes "𝔐 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔖 = 𝔉' ∘⇩C⇩F 𝔉"
    and "𝔖' = 𝔊' ∘⇩C⇩F 𝔊"
  shows "𝔐 ∘⇩N⇩T⇩C⇩F 𝔑 : 𝔖 ↦⇩C⇩F 𝔖' : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (rule ntcf_hcomp_is_ntcf)

lemma ntcf_hcomp_associativ[cat_cs_simps]: 
  assumes "𝔏 : 𝔉'' ↦⇩C⇩F 𝔊'' : ℭ ↦↦⇩C⇘α⇙ 𝔇" 
    and "𝔐 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "(𝔏 ∘⇩N⇩T⇩C⇩F 𝔐) ∘⇩N⇩T⇩C⇩F 𝔑 = 𝔏 ∘⇩N⇩T⇩C⇩F (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)"
proof-
  interpret 𝔏: is_ntcf α ℭ 𝔇 𝔉'' 𝔊'' 𝔏 by (rule assms(1))
  interpret 𝔐: is_ntcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐 by (rule assms(2))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(3))
  show ?thesis
  proof(rule ntcf_eqI[of α])
    show "𝔏 ∘⇩N⇩T⇩C⇩F (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑) : 
      𝔉'' ∘⇩C⇩F 𝔉' ∘⇩C⇩F 𝔉 ↦⇩C⇩F 𝔊'' ∘⇩C⇩F 𝔊' ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔇"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from ntsmcf_hcomp_assoc[
      OF 𝔏.ntcf_is_ntsmcf 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf,
      unfolded slicing_commute
      ]
    have 
      "ntcf_ntsmcf (𝔏 ∘⇩N⇩T⇩C⇩F 𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈ = 
        ntcf_ntsmcf (𝔏 ∘⇩N⇩T⇩C⇩F (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈"
      by simp
    then show "(𝔏 ∘⇩N⇩T⇩C⇩F 𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈ = (𝔏 ∘⇩N⇩T⇩C⇩F (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈"
      unfolding slicing_simps .
  qed (auto intro: cat_cs_intros)
qed


subsubsection‹
The opposite of the horizontal composition of natural transformations
›

lemma op_ntcf_ntcf_hcomp[cat_op_simps]: 
  assumes "𝔐 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "op_ntcf (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑) = op_ntcf 𝔐 ∘⇩N⇩T⇩C⇩F op_ntcf 𝔑"
proof-
  interpret 𝔐: is_ntcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis
  proof(rule sym, rule ntcf_eqI[of α])
    from op_ntsmcf_ntsmcf_hcomp[
        OF 𝔐.ntcf_is_ntsmcf 𝔑.ntcf_is_ntsmcf, 
        unfolded slicing_simps slicing_commute 
        ]
    have "ntcf_ntsmcf (op_ntcf 𝔐 ∘⇩N⇩T⇩C⇩F op_ntcf 𝔑)⦇NTMap⦈ =
      ntcf_ntsmcf (op_ntcf (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈"
      by simp
    then show "(op_ntcf 𝔐 ∘⇩N⇩T⇩C⇩F op_ntcf 𝔑)⦇NTMap⦈ = op_ntcf (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈"
      unfolding slicing_simps .
    have "𝔐 ∘⇩N⇩T⇩C⇩F 𝔑 : 𝔉' ∘⇩C⇩F 𝔉 ↦⇩C⇩F 𝔊' ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
      by (rule ntcf_hcomp_is_ntcf[OF assms])
    from is_ntcf.is_ntcf_op[OF this] show 
      "op_ntcf (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑) : 
        op_cf 𝔊' ∘⇩C⇩F op_cf 𝔊 ↦⇩C⇩F op_cf 𝔉' ∘⇩C⇩F op_cf 𝔉 : 
        op_cat 𝔄 ↦↦⇩C⇘α⇙ op_cat ℭ"
      unfolding cat_op_simps .
  qed (auto intro: cat_op_intros cat_cs_intros)
qed 



subsection‹Interchange law›

lemma ntcf_comp_interchange_law:
  ―‹See Chapter II-5 in \cite{mac_lane_categories_2010}.›
  assumes "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔐' : 𝔊' ↦⇩C⇩F ℌ' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "((𝔐' ∙⇩N⇩T⇩C⇩F 𝔑') ∘⇩N⇩T⇩C⇩F (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)) = (𝔐' ∘⇩N⇩T⇩C⇩F 𝔐) ∙⇩N⇩T⇩C⇩F (𝔑' ∘⇩N⇩T⇩C⇩F 𝔑)"
proof-
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  interpret 𝔐': is_ntcf α 𝔅 ℭ 𝔊' ℌ' 𝔐' by (rule assms(3))
  interpret 𝔑': is_ntcf α 𝔅 ℭ 𝔉' 𝔊' 𝔑' by (rule assms(4))
  show ?thesis
  proof(rule ntcf_eqI)
    from ntsmcf_comp_interchange_law
      [
        OF 
          𝔐.ntcf_is_ntsmcf 
          𝔑.ntcf_is_ntsmcf 
          𝔐'.ntcf_is_ntsmcf 
          𝔑'.ntcf_is_ntsmcf
      ]
    have 
      "(
        (ntcf_ntsmcf 𝔐' ∙⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑') ∘⇩N⇩T⇩S⇩M⇩C⇩F
        (ntcf_ntsmcf 𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑)
       )⦇NTMap⦈ =
        (
          (ntcf_ntsmcf 𝔐' ∘⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔐) ∙⇩N⇩T⇩C⇩F
          (ntcf_ntsmcf 𝔑' ∘⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑)
        )⦇NTMap⦈"
      by simp
    then show 
      "(𝔐' ∙⇩N⇩T⇩C⇩F 𝔑' ∘⇩N⇩T⇩C⇩F (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈ =
        (𝔐' ∘⇩N⇩T⇩C⇩F 𝔐 ∙⇩N⇩T⇩C⇩F (𝔑' ∘⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈"
      unfolding slicing_simps slicing_commute .
  qed (auto intro: cat_cs_intros)
qed



subsection‹Identity natural transformation›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-4 in \<^cite>‹"mac_lane_categories_2010"›.›

definition ntcf_id :: "V ⇒ V"
  where "ntcf_id 𝔉 = [𝔉⦇HomCod⦈⦇CId⦈ ∘⇩∘ 𝔉⦇ObjMap⦈, 𝔉, 𝔉, 𝔉⦇HomDom⦈, 𝔉⦇HomCod⦈]⇩∘"


text‹Components.›

lemma ntcf_id_components:
  shows "ntcf_id 𝔉⦇NTMap⦈ = 𝔉⦇HomCod⦈⦇CId⦈ ∘⇩∘ 𝔉⦇ObjMap⦈"
    and [dg_shared_cs_simps, cat_cs_simps]: "ntcf_id 𝔉⦇NTDom⦈ = 𝔉" 
    and [dg_shared_cs_simps, cat_cs_simps]: "ntcf_id 𝔉⦇NTCod⦈ = 𝔉" 
    and [dg_shared_cs_simps, cat_cs_simps]: "ntcf_id 𝔉⦇NTDGDom⦈ = 𝔉⦇HomDom⦈" 
    and [dg_shared_cs_simps, cat_cs_simps]: "ntcf_id 𝔉⦇NTDGCod⦈ = 𝔉⦇HomCod⦈" 
  unfolding ntcf_id_def nt_field_simps by (simp_all add: nat_omega_simps)

lemma (in is_functor) is_functor_ntcf_id_components:
  shows "ntcf_id 𝔉⦇NTMap⦈ = 𝔅⦇CId⦈ ∘⇩∘ 𝔉⦇ObjMap⦈"
    and "ntcf_id 𝔉⦇NTDom⦈ = 𝔉" 
    and "ntcf_id 𝔉⦇NTCod⦈ = 𝔉" 
    and "ntcf_id 𝔉⦇NTDGDom⦈ = 𝔄" 
    and "ntcf_id 𝔉⦇NTDGCod⦈ = 𝔅" 
  unfolding ntcf_id_components by (simp_all add: cat_cs_simps)


subsubsection‹Natural transformation map›

lemma (in is_functor) ntcf_id_NTMap_vdomain[cat_cs_simps]: 
  "𝒟⇩∘ (ntcf_id 𝔉⦇NTMap⦈) = 𝔄⦇Obj⦈"
  using cf_ObjMap_vrange unfolding is_functor_ntcf_id_components 
  by (auto simp: cat_cs_simps)

lemmas [cat_cs_simps] = is_functor.ntcf_id_NTMap_vdomain

lemma (in is_functor) ntcf_id_NTMap_app_vdomain[cat_cs_simps]: 
  assumes [simp]: "a ∈⇩∘ 𝔄⦇Obj⦈"
  shows "ntcf_id 𝔉⦇NTMap⦈⦇a⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
  unfolding is_functor_ntcf_id_components
  by (rule vsv_vcomp_at) (auto simp: cf_ObjMap_vrange cat_cs_simps cat_cs_intros)

lemmas [cat_cs_simps] = is_functor.ntcf_id_NTMap_app_vdomain

lemma (in is_functor) ntcf_id_NTMap_vsv[cat_cs_intros]: 
  "vsv (ntcf_id 𝔉⦇NTMap⦈)"
  unfolding is_functor_ntcf_id_components by (auto intro: vsv_vcomp)

lemmas [cat_cs_intros] = is_functor.ntcf_id_NTMap_vsv

lemma (in is_functor) ntcf_id_NTMap_vrange: 
  "ℛ⇩∘ (ntcf_id 𝔉⦇NTMap⦈) ⊆⇩∘ 𝔅⦇Arr⦈"
proof(rule vsubsetI)
  interpret vsv ‹ntcf_id 𝔉⦇NTMap⦈› by (rule ntcf_id_NTMap_vsv)
  fix f assume "f ∈⇩∘ ℛ⇩∘ (ntcf_id 𝔉⦇NTMap⦈)"
  then obtain a 
    where f_def: "f = ntcf_id 𝔉⦇NTMap⦈⦇a⦈" and a: "a ∈⇩∘ 𝒟⇩∘ (ntcf_id 𝔉⦇NTMap⦈)"
    using vrange_atD by metis
  then have "a ∈⇩∘ 𝔄⦇Obj⦈" and "f = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
    by (auto simp: cat_cs_simps)
  then show "f ∈⇩∘ 𝔅⦇Arr⦈"
    by (auto dest: cf_ObjMap_app_in_HomCod_Obj HomCod.cat_CId_is_arr)
qed


subsubsection‹Further properties›

lemma (in is_functor) cf_ntcf_id_is_ntcf[cat_cs_intros]: 
  "ntcf_id 𝔉 : 𝔉 ↦⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof(rule is_ntcfI, unfold is_functor_ntcf_id_components(2,3,4,5))
  show "ntcf_ntsmcf (ntcf_id 𝔉) : 
    cf_smcf 𝔉 ↦⇩S⇩M⇩C⇩F cf_smcf 𝔉 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc 𝔅"
  proof
    (
      rule is_ntsmcfI, 
      unfold slicing_simps slicing_commute is_functor_ntcf_id_components(2,3,4,5)
    )
    show "ntsmcf_tdghm (ntcf_ntsmcf (ntcf_id 𝔉)) : 
      smcf_dghm (cf_smcf 𝔉) ↦⇩D⇩G⇩H⇩M smcf_dghm (cf_smcf 𝔉) : 
      smc_dg (cat_smc 𝔄) ↦↦⇩D⇩G⇘α⇙ smc_dg (cat_smc 𝔅)"
      by
        (
          rule is_tdghmI, 
          unfold 
            slicing_simps 
            slicing_commute 
            is_functor_ntcf_id_components(2,3,4,5)
        )
        (
          auto 
            simp:
              cat_cs_simps
              cat_cs_intros
              nat_omega_simps
              ntsmcf_tdghm_def
              cf_is_semifunctor 
            intro: slicing_intros
        )
    fix f a b assume "f : a ↦⇘𝔄⇙ b"
    with is_functor_axioms show 
      "ntcf_id 𝔉⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 
        𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ ntcf_id 𝔉⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto simp: ntcf_ntsmcf_def nat_omega_simps intro: slicing_intros)
qed (auto simp: ntcf_id_def nat_omega_simps intro: cat_cs_intros)

lemma (in is_functor) cf_ntcf_id_is_ntcf': 
  assumes "𝔊' = 𝔉" and "ℌ' = 𝔉"
  shows "ntcf_id 𝔉 : 𝔊' ↦⇩C⇩F ℌ' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  unfolding assms by (rule cf_ntcf_id_is_ntcf)

lemmas [cat_cs_intros] = is_functor.cf_ntcf_id_is_ntcf'

lemma (in is_ntcf) ntcf_ntcf_vcomp_ntcf_id_left_left[cat_cs_simps]:
  ―‹See Chapter II-4 in \cite{mac_lane_categories_2010}.›
  "ntcf_id 𝔊 ∙⇩N⇩T⇩C⇩F 𝔑 = 𝔑"
proof(rule ntcf_eqI[of α])
  interpret id: is_ntcf α 𝔄 𝔅 𝔊 𝔊 ‹ntcf_id 𝔊› 
    by (rule NTCod.cf_ntcf_id_is_ntcf)
  show "(ntcf_id 𝔊 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈ = 𝔑⦇NTMap⦈"
  proof(rule vsv_eqI)
    show [simp]: "𝒟⇩∘ ((ntcf_id 𝔊 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈) = 𝒟⇩∘ (𝔑⦇NTMap⦈)"
      unfolding ntsmcf_vcomp_components 
      by (simp add: cat_cs_simps)
    fix a assume "a ∈⇩∘ 𝒟⇩∘ ((ntcf_id 𝔊 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈)"
    then have "a ∈⇩∘ 𝔄⦇Obj⦈" by (simp add: cat_cs_simps)
    then show "(ntcf_id 𝔊 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ = 𝔑⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto simp: ntsmcf_vcomp_components)
qed (auto intro: cat_cs_intros)

lemmas [cat_cs_simps] = is_ntcf.ntcf_ntcf_vcomp_ntcf_id_left_left

lemma (in is_ntcf) ntcf_ntcf_vcomp_ntcf_id_right_left[cat_cs_simps]: 
  ―‹See Chapter II-4 in \cite{mac_lane_categories_2010}.›
  "𝔑 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔉 = 𝔑"
proof(rule ntcf_eqI[of α])
  interpret id: is_ntcf α 𝔄 𝔅 𝔉 𝔉 ‹ntcf_id 𝔉›    
    by (rule NTDom.cf_ntcf_id_is_ntcf)
  show "(𝔑 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈ = 𝔑⦇NTMap⦈"
  proof(rule vsv_eqI)
    show [simp]: "𝒟⇩∘ ((𝔑 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈) = 𝒟⇩∘ (𝔑⦇NTMap⦈)"
      unfolding ntsmcf_vcomp_components by (simp add: cat_cs_simps)
    fix a assume "a ∈⇩∘ 𝒟⇩∘ ((𝔑 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈)"
    then have "a ∈⇩∘ 𝔄⦇Obj⦈" by (simp add: cat_cs_simps)
    then show "(𝔑 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈⦇a⦈ = 𝔑⦇NTMap⦈⦇a⦈" 
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto simp: ntsmcf_vcomp_components)
qed (auto intro: cat_cs_intros)

lemmas [cat_cs_simps] = is_ntcf.ntcf_ntcf_vcomp_ntcf_id_right_left

lemma (in is_ntcf) ntcf_ntcf_hcomp_ntcf_id_left_left[cat_cs_simps]:
  ―‹See Chapter II-5 in \cite{mac_lane_categories_2010}.›
  "ntcf_id (cf_id 𝔅) ∘⇩N⇩T⇩C⇩F 𝔑 = 𝔑"
proof(rule ntcf_eqI)
  interpret id: is_ntcf α 𝔅 𝔅 ‹cf_id 𝔅› ‹cf_id 𝔅› ‹ntcf_id (cf_id 𝔅)› 
    by 
      (
        simp add: 
          NTDom.HomCod.cat_cf_id_is_functor is_functor.cf_ntcf_id_is_ntcf
      )
  show "ntcf_id (cf_id 𝔅) ∘⇩N⇩T⇩C⇩F 𝔑 : 
    cf_id 𝔅 ∘⇩C⇩F 𝔉 ↦⇩C⇩F cf_id 𝔅 ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "(ntcf_id (cf_id 𝔅) ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈ = 𝔑⦇NTMap⦈"
  proof(rule vsv_eqI)
    fix a assume "a ∈⇩∘ 𝒟⇩∘ ((ntcf_id (cf_id 𝔅) ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈)"    
    then have a: "a ∈⇩∘ 𝔄⦇Obj⦈" 
      unfolding ntcf_hcomp_NTMap_vdomain[OF is_ntcf_axioms] by simp
    with is_ntcf_axioms show 
      "(ntcf_id (cf_id 𝔅) ∘⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ = 𝔑⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto simp: ntsmcf_hcomp_components(1) cat_cs_simps)
qed (auto simp: cat_cs_simps intro: cat_cs_intros)

lemmas [cat_cs_simps] = is_ntcf.ntcf_ntcf_hcomp_ntcf_id_left_left

lemma (in is_ntcf) ntcf_ntcf_hcomp_ntcf_id_right_left[cat_cs_simps]: 
  ―‹See Chapter II-5 in \cite{mac_lane_categories_2010}.›
  "𝔑 ∘⇩N⇩T⇩C⇩F ntcf_id (cf_id 𝔄) = 𝔑"
proof(rule ntcf_eqI[of α])
  interpret id: is_ntcf α 𝔄 𝔄 ‹cf_id 𝔄› ‹cf_id 𝔄› ‹ntcf_id (cf_id 𝔄)› 
    by 
      (
        simp add: 
          NTDom.HomDom.cat_cf_id_is_functor is_functor.cf_ntcf_id_is_ntcf
      )
  show "𝔑 ∘⇩N⇩T⇩C⇩F ntcf_id (cf_id 𝔄) :
    𝔉 ∘⇩C⇩F cf_id 𝔄 ↦⇩C⇩F 𝔊 ∘⇩C⇩F cf_id 𝔄 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "(𝔑 ∘⇩N⇩T⇩C⇩F ntcf_id (cf_id 𝔄))⦇NTMap⦈ = 𝔑⦇NTMap⦈"
  proof(rule vsv_eqI)
    fix a assume "a ∈⇩∘ 𝒟⇩∘ ((𝔑 ∘⇩N⇩T⇩C⇩F ntcf_id (cf_id 𝔄))⦇NTMap⦈)"
    then have a: "a ∈⇩∘ 𝔄⦇Obj⦈" 
      unfolding ntcf_hcomp_NTMap_vdomain[OF id.is_ntcf_axioms] by simp
    with is_ntcf_axioms show 
      "(𝔑 ∘⇩N⇩T⇩C⇩F ntcf_id (cf_id 𝔄))⦇NTMap⦈⦇a⦈ = 𝔑⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto simp: ntsmcf_hcomp_components(1) cat_cs_simps)
qed (auto simp: cat_cs_simps cat_cs_intros)

lemmas [cat_cs_simps] = is_ntcf.ntcf_ntcf_hcomp_ntcf_id_right_left


subsubsection‹The opposite identity natural transformation›

lemma (in is_functor) cf_ntcf_id_op_cf: "ntcf_id (op_cf 𝔉) = op_ntcf (ntcf_id 𝔉)"
proof(rule ntcf_eqI)
  show ntcfid_op: 
    "ntcf_id (op_cf 𝔉) : op_cf 𝔉 ↦⇩C⇩F op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇘α⇙ op_cat 𝔅"
    by (simp add: is_functor.cf_ntcf_id_is_ntcf local.is_functor_op)
  show "ntcf_id (op_cf 𝔉)⦇NTMap⦈ = op_ntcf (ntcf_id 𝔉)⦇NTMap⦈"
    by (rule vsv_eqI, unfold cat_op_simps)
      (
        auto 
          simp: cat_op_simps cat_cs_simps ntcf_id_components(1) 
          intro: vsv_vcomp
      )
qed (auto intro: cat_op_intros cat_cs_intros)


subsubsection‹Identity natural transformation of a composition of functors›

lemma ntcf_id_cf_comp:
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "ntcf_id (𝔊 ∘⇩C⇩F 𝔉) = ntcf_id 𝔊 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉"
proof(rule ntcf_eqI)
  from assms show 𝔊𝔉: "ntcf_id (𝔊 ∘⇩C⇩F 𝔉) : 𝔊 ∘⇩C⇩F 𝔉 ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  interpret 𝔊𝔉: is_ntcf α 𝔄 ℭ ‹𝔊 ∘⇩C⇩F 𝔉› ‹𝔊 ∘⇩C⇩F 𝔉› ‹ntcf_id (𝔊 ∘⇩C⇩F 𝔉)›
    by (rule 𝔊𝔉)
  from assms show 𝔊_𝔉:
    "ntcf_id 𝔊 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉 : 𝔊 ∘⇩C⇩F 𝔉 ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  interpret 𝔊_𝔉: is_ntcf α 𝔄 ℭ ‹𝔊 ∘⇩C⇩F 𝔉› ‹𝔊 ∘⇩C⇩F 𝔉› ‹ntcf_id 𝔊 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉›
    by (rule 𝔊_𝔉)
  show "ntcf_id (𝔊 ∘⇩C⇩F 𝔉)⦇NTMap⦈ = (ntcf_id 𝔊 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈"
  proof(rule vsv_eqI, unfold 𝔊𝔉.ntcf_NTMap_vdomain 𝔊_𝔉.ntcf_NTMap_vdomain)
    fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
    with assms show 
      "ntcf_id (𝔊 ∘⇩C⇩F 𝔉)⦇NTMap⦈⦇a⦈ = (ntcf_id 𝔊 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed auto
qed auto

lemmas [cat_cs_simps] = ntcf_id_cf_comp[symmetric]



subsection‹Composition of a natural transformation and a functor›


subsubsection‹Definition and elementary properties›

abbreviation (input) ntcf_cf_comp :: "V ⇒ V ⇒ V" (infixl "∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F" 55)
  where "ntcf_cf_comp ≡ tdghm_dghm_comp"


text‹Slicing.›

lemma ntsmcf_tdghm_ntsmcf_smcf_comp[slicing_commute]: 
  "ntcf_ntsmcf 𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F cf_smcf ℌ = ntcf_ntsmcf (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ)"
  unfolding 
    ntcf_ntsmcf_def
    cf_smcf_def
    cat_smc_def
    tdghm_dghm_comp_def 
    dghm_comp_def 
    ntsmcf_tdghm_def 
    smcf_dghm_def
    smc_dg_def
    dg_field_simps
    dghm_field_simps 
    nt_field_simps 
  by (simp add: nat_omega_simps) (*slow*)


subsubsection‹Natural transformation map›

mk_VLambda (in is_functor) 
  tdghm_dghm_comp_components(1)[where ℌ=𝔉, unfolded cf_HomDom]
  |vdomain ntcf_cf_comp_NTMap_vdomain[cat_cs_simps]|
  |app ntcf_cf_comp_NTMap_app[cat_cs_simps]|

lemmas [cat_cs_simps] = 
  is_functor.ntcf_cf_comp_NTMap_vdomain
  is_functor.ntcf_cf_comp_NTMap_app

lemma ntcf_cf_comp_NTMap_vrange: 
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ)⦇NTMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
  interpret 𝔑: is_ntcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_functor α 𝔄 𝔅 ℌ by (rule assms(2))
  show ?thesis unfolding tdghm_dghm_comp_components 
    by (auto simp: cat_cs_simps intro: cat_cs_intros)
qed


subsubsection‹
Opposite of the composition of a natural transformation and a functor
›

lemma op_ntcf_ntcf_cf_comp[cat_op_simps]:
  "op_ntcf (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ) = op_ntcf 𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F op_cf ℌ"
  unfolding 
    tdghm_dghm_comp_def 
    dghm_comp_def 
    op_ntcf_def 
    op_cf_def 
    op_cat_def
    dg_field_simps
    dghm_field_simps
    nt_field_simps
  by (simp add: nat_omega_simps) (*slow*)


subsubsection‹
Composition of a natural transformation and a
functor is a natural transformation
›

lemma ntcf_cf_comp_is_ntcf:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ : 𝔉 ∘⇩C⇩F ℌ ↦⇩C⇩F 𝔊 ∘⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔑: is_ntcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_functor α 𝔄 𝔅 ℌ by (rule assms(2))
  show ?thesis
  proof(rule is_ntcfI)
    show "vfsequence (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ)"
      unfolding tdghm_dghm_comp_def by (simp add: nat_omega_simps)
    from assms show "𝔉 ∘⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ ℭ" 
      by (cs_concl cs_intro: cat_cs_intros)
    from assms show "𝔊 ∘⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ ℭ" 
      by (cs_concl cs_intro: cat_cs_intros)
    show "vcard (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ) = 5⇩ℕ"
      unfolding tdghm_dghm_comp_def by (simp add: nat_omega_simps)
    from assms show 
      "ntcf_ntsmcf (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ) :
        cf_smcf (𝔉 ∘⇩C⇩F ℌ) ↦⇩S⇩M⇩C⇩F cf_smcf (𝔊 ∘⇩C⇩F ℌ) :
        cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
      by 
        (
          cs_concl 
            cs_simp: slicing_commute[symmetric] 
            cs_intro: slicing_intros smc_cs_intros cat_cs_intros
        )
  qed (auto simp: tdghm_dghm_comp_components(1) cat_cs_simps)
qed

lemma ntcf_cf_comp_is_ntcf'[cat_cs_intros]:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉' = 𝔉 ∘⇩C⇩F ℌ"
    and "𝔊' = 𝔊 ∘⇩C⇩F ℌ"
  shows "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (simp add: ntcf_cf_comp_is_ntcf)


subsubsection‹Further properties›

lemma ntcf_cf_comp_ntcf_cf_comp_assoc:
  assumes "𝔑 : ℌ ↦⇩C⇩F ℌ' : ℭ ↦↦⇩C⇘α⇙ 𝔇" 
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "(𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉 = 𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F (𝔊 ∘⇩C⇩F 𝔉)"
proof-
  interpret 𝔑: is_ntcf α ℭ 𝔇 ℌ ℌ' 𝔑 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))
  interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(3))
  show ?thesis  
  proof(rule ntcf_ntsmcf_eqI)
    from assms show
      "(𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉 :
        ℌ ∘⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 ↦⇩C⇩F ℌ' ∘⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔇"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    show "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F (𝔊 ∘⇩C⇩F 𝔉) :
      ℌ ∘⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 ↦⇩C⇩F ℌ' ∘⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔇"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms show 
      "ntcf_ntsmcf ((𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉) =
        ntcf_ntsmcf (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F (𝔊 ∘⇩C⇩F 𝔉))"
      by 
        (
          cs_concl 
            cs_simp: slicing_commute[symmetric] 
            cs_intro: slicing_intros ntsmcf_smcf_comp_ntsmcf_smcf_comp_assoc
        )
  qed simp_all
qed

lemma (in is_ntcf) ntcf_ntcf_cf_comp_cf_id[cat_cs_simps]:
  "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F cf_id 𝔄 = 𝔑"
proof(rule ntcf_ntsmcf_eqI)
  show "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F cf_id 𝔄 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  show "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "ntcf_ntsmcf (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F cf_id 𝔄) = ntcf_ntsmcf 𝔑"
    by
      (
        cs_concl cs_shallow
          cs_simp: slicing_commute[symmetric] 
          cs_intro: cat_cs_intros slicing_intros smc_cs_simps
      )
qed simp_all

lemmas [cat_cs_simps] = is_ntcf.ntcf_ntcf_cf_comp_cf_id

lemma ntcf_vcomp_ntcf_cf_comp[cat_cs_simps]:
  assumes "𝔎 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "(𝔐 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎) ∙⇩N⇩T⇩C⇩F (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎) = (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎"
proof(rule ntcf_ntsmcf_eqI)
  from assms show 
    "𝔐 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎 ∙⇩N⇩T⇩C⇩F (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎) :
      𝔉 ∘⇩C⇩F 𝔎 ↦⇩C⇩F ℌ ∘⇩C⇩F 𝔎 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from assms show 
    "ntcf_ntsmcf (𝔐 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎 ∙⇩N⇩T⇩C⇩F (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎)) =
      ntcf_ntsmcf (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎)"
    unfolding slicing_commute[symmetric]
    by (intro ntsmcf_vcomp_ntsmcf_smcf_comp)
      (cs_concl cs_intro: slicing_intros)
qed (use assms in ‹cs_concl cs_shallow cs_intro: cat_cs_intros›)+



subsection‹Composition of a functor and a natural transformation›


subsubsection‹Definition and elementary properties›

abbreviation (input) cf_ntcf_comp :: "V ⇒ V ⇒ V" (infixl "∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F" 55)
  where "cf_ntcf_comp ≡ dghm_tdghm_comp"


text‹Slicing.›

lemma ntcf_ntsmcf_cf_ntcf_comp[slicing_commute]: 
  "cf_smcf ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F ntcf_ntsmcf 𝔑 = ntcf_ntsmcf (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)"
  unfolding 
    ntcf_ntsmcf_def
    cf_smcf_def
    cat_smc_def
    dghm_tdghm_comp_def 
    dghm_comp_def 
    ntsmcf_tdghm_def 
    smcf_dghm_def 
    smc_dg_def
    dg_field_simps
    dghm_field_simps 
    nt_field_simps 
  by (simp add: nat_omega_simps) (*slow*)


subsubsection‹Natural transformation map›

mk_VLambda (in is_ntcf) 
  dghm_tdghm_comp_components(1)[where 𝔑=𝔑, unfolded ntcf_NTDGDom]
  |vdomain cf_ntcf_comp_NTMap_vdomain|
  |app cf_ntcf_comp_NTMap_app|

lemmas [cat_cs_simps] = 
  is_ntcf.cf_ntcf_comp_NTMap_vdomain
  is_ntcf.cf_ntcf_comp_NTMap_app

lemma cf_ntcf_comp_NTMap_vrange: 
  assumes "ℌ : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
  interpret ℌ: is_functor α 𝔅 ℭ ℌ by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis 
    unfolding dghm_tdghm_comp_components 
    by (auto simp: cat_cs_simps intro: cat_cs_intros)
qed


subsubsection‹
Opposite of the composition of a functor and a natural transformation
›

lemma op_ntcf_cf_ntcf_comp[cat_op_simps]:
  "op_ntcf (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) = op_cf ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F op_ntcf 𝔑"
  unfolding 
    dghm_tdghm_comp_def
    dghm_comp_def
    op_ntcf_def
    op_cf_def
    op_cat_def
    dg_field_simps
    dghm_field_simps
    nt_field_simps
  by (simp add: nat_omega_simps) (*slow*)


subsubsection‹
Composition of a functor and a natural transformation 
is a natural transformation
›

lemma cf_ntcf_comp_is_ntcf:
  assumes "ℌ : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : ℌ ∘⇩C⇩F 𝔉 ↦⇩C⇩F ℌ ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
proof-
  interpret ℌ: is_functor α 𝔅 ℭ ℌ by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis
  proof(rule is_ntcfI)
    show "vfsequence (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)" unfolding dghm_tdghm_comp_def by simp
    from assms show "ℌ ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" 
      by (cs_concl cs_intro: cat_cs_intros)
    from assms show "ℌ ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
      by (cs_concl cs_intro: cat_cs_intros)
    show "vcard (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) = 5⇩ℕ"
      unfolding dghm_tdghm_comp_def by (simp add: nat_omega_simps)
    from assms show "ntcf_ntsmcf (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) :
      cf_smcf (ℌ ∘⇩C⇩F 𝔉) ↦⇩S⇩M⇩C⇩F cf_smcf (ℌ ∘⇩C⇩F 𝔊) :
      cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
      by 
        (
          cs_concl 
            cs_simp: slicing_commute[symmetric]
            cs_intro: slicing_intros smc_cs_intros 
        )
  qed (auto simp: dghm_tdghm_comp_components(1) cat_cs_simps)
qed

lemma cf_ntcf_comp_is_functor'[cat_cs_intros]:
  assumes "ℌ : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉' = ℌ ∘⇩C⇩F 𝔉"
    and "𝔊' = ℌ ∘⇩C⇩F 𝔊"
  shows "ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (simp add: cf_ntcf_comp_is_ntcf)


subsubsection‹Further properties›

lemma cf_comp_cf_ntcf_comp_assoc:
  assumes "𝔑 : ℌ ↦⇩C⇩F ℌ' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔊 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
  shows "(𝔊 ∘⇩C⇩F 𝔉) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 = 𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)"
proof(rule ntcf_ntsmcf_eqI)
  interpret 𝔑: is_ntcf α 𝔄 𝔅 ℌ ℌ' 𝔑 by (rule assms(1))
  interpret 𝔉: is_functor α 𝔅 ℭ 𝔉 by (rule assms(2))
  interpret 𝔊: is_functor α ℭ 𝔇 𝔊 by (rule assms(3))
  from assms show "(𝔊 ∘⇩C⇩F 𝔉) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 :
    𝔊 ∘⇩C⇩F 𝔉 ∘⇩C⇩F ℌ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 ∘⇩C⇩F ℌ' : 𝔄 ↦↦⇩C⇘α⇙ 𝔇"
    by (cs_concl cs_intro: cat_cs_intros)
  from assms show "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) :
    𝔊 ∘⇩C⇩F 𝔉 ∘⇩C⇩F ℌ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 ∘⇩C⇩F ℌ' : 𝔄 ↦↦⇩C⇘α⇙ 𝔇"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms show 
    "ntcf_ntsmcf (𝔊 ∘⇩C⇩F 𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) =
      ntcf_ntsmcf (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑))"
    by
      (
        cs_concl
          cs_simp: slicing_commute[symmetric] 
          cs_intro: slicing_intros smcf_comp_smcf_ntsmcf_comp_assoc
      )
qed simp_all

lemma (in is_ntcf) ntcf_cf_ntcf_comp_cf_id[cat_cs_simps]:
  "cf_id 𝔅 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 = 𝔑"
proof(rule ntcf_ntsmcf_eqI)
  show "cf_id 𝔅 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  show "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "ntcf_ntsmcf (smcf_id 𝔅 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) = ntcf_ntsmcf 𝔑"
    by 
      (
        cs_concl cs_shallow
          cs_simp: slicing_commute[symmetric] 
          cs_intro: cat_cs_intros slicing_intros smc_cs_simps
      )
qed simp_all

lemmas [cat_cs_simps] = is_ntcf.ntcf_cf_ntcf_comp_cf_id

lemma cf_ntcf_comp_ntcf_cf_comp_assoc:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "ℌ : ℭ ↦↦⇩C⇘α⇙ 𝔇"
    and "𝔎 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "(ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎 = ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎)"
proof-
  interpret 𝔑: is_ntcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_functor α ℭ 𝔇 ℌ by (rule assms(2))
  interpret 𝔎: is_functor α 𝔄 𝔅 𝔎 by (rule assms(3))
  show ?thesis
    by (rule ntcf_ntsmcf_eqI)
      (
        use assms in
          ‹
            cs_concl 
              cs_simp: cat_cs_simps slicing_commute[symmetric]
              cs_intro:
                cat_cs_intros
                slicing_intros
                smcf_ntsmcf_comp_ntsmcf_smcf_comp_assoc
          ›
      )+
qed

lemma ntcf_cf_comp_ntcf_id[cat_cs_simps]:
  assumes "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔎 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "ntcf_id 𝔉 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎 = ntcf_id 𝔉 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔎"
proof(rule ntcf_eqI)
  from assms have dom_lhs: "𝒟⇩∘ ((ntcf_id 𝔉 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎)⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from assms have dom_rhs: "𝒟⇩∘ ((ntcf_id 𝔉 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔎)⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  show "(ntcf_id 𝔉 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎)⦇NTMap⦈ = (ntcf_id 𝔉 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔎)⦇NTMap⦈"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
    with assms show 
      "(ntcf_id 𝔉 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎)⦇NTMap⦈⦇a⦈ = (ntcf_id 𝔉 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔎)⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto intro: cat_cs_intros)
qed (use assms in ‹cs_concl cs_shallow cs_intro: cat_cs_intros›)+

lemma cf_ntcf_comp_ntcf_vcomp: 
  assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔎 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) = (𝔎 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔐) ∙⇩N⇩T⇩C⇩F (𝔎 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)"
proof-
  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(2))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(3))
  show "𝔎 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) = 𝔎 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔐 ∙⇩N⇩T⇩C⇩F (𝔎 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)"
    by (rule ntcf_ntsmcf_eqI)
      (
        use assms in
          ‹
            cs_concl 
              cs_simp: smc_cs_simps slicing_commute[symmetric]
              cs_intro:
                cat_cs_intros
                slicing_intros
                smcf_ntsmcf_comp_ntsmcf_vcomp
          ›
      )+
qed



subsection‹Constant natural transformation›


subsubsection‹Definition and elementary properties›


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

definition ntcf_const :: "V ⇒ V ⇒ V ⇒ V"
  where "ntcf_const 𝔍 ℭ f = 
    [
      vconst_on (𝔍⦇Obj⦈) f, 
      cf_const 𝔍 ℭ (ℭ⦇Dom⦈⦇f⦈), 
      cf_const 𝔍 ℭ (ℭ⦇Cod⦈⦇f⦈), 
      𝔍, 
      ℭ
    ]⇩∘"


text‹Components.›

lemma ntcf_const_components:
  shows "ntcf_const 𝔍 ℭ f⦇NTMap⦈ = vconst_on (𝔍⦇Obj⦈) f"
    and "ntcf_const 𝔍 ℭ f⦇NTDom⦈ = cf_const 𝔍 ℭ (ℭ⦇Dom⦈⦇f⦈)"
    and "ntcf_const 𝔍 ℭ f⦇NTCod⦈ = cf_const 𝔍 ℭ (ℭ⦇Cod⦈⦇f⦈)"
    and "ntcf_const 𝔍 ℭ f⦇NTDGDom⦈ = 𝔍"
    and "ntcf_const 𝔍 ℭ f⦇NTDGCod⦈ = ℭ"
  unfolding ntcf_const_def nt_field_simps by (auto simp: nat_omega_simps)


subsubsection‹Natural transformation map›

mk_VLambda ntcf_const_components(1)[folded VLambda_vconst_on]
  |vsv ntcf_const_ObjMap_vsv[cat_cs_intros]|
  |vdomain ntcf_const_ObjMap_vdomain[cat_cs_simps]|
  |app ntcf_const_ObjMap_app[cat_cs_simps]|

lemma ntcf_const_NTMap_ne_vrange: 
  assumes "𝔍⦇Obj⦈ ≠ 0"
  shows "ℛ⇩∘ (ntcf_const 𝔍 ℭ f⦇NTMap⦈) = set {f}"
  using assms unfolding ntcf_const_components by simp

lemma ntcf_const_NTMap_vempty_vrange: 
  assumes "𝔍⦇Obj⦈ = 0"
  shows "ℛ⇩∘ (ntcf_const 𝔍 ℭ f⦇NTMap⦈) = 0"
  using assms unfolding ntcf_const_components by simp


subsubsection‹Constant natural transformation is a natural transformation›

lemma ntcf_const_is_ntcf:
  assumes "category α 𝔍" and "category α ℭ" and "f : a ↦⇘ℭ⇙ b"
  shows "ntcf_const 𝔍 ℭ f : cf_const 𝔍 ℭ a ↦⇩C⇩F cf_const 𝔍 ℭ b : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔍: category α 𝔍 by (rule assms(1))
  interpret ℭ: category α ℭ by (rule assms(2))
  show ?thesis  
  proof(intro is_ntcfI')
    show "vfsequence (ntcf_const 𝔍 ℭ f)" unfolding ntcf_const_def by auto
    show "cf_const 𝔍 ℭ a : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
    proof(rule cf_const_is_functor)
      from assms(3) show "a ∈⇩∘ ℭ⦇Obj⦈" by (simp add: cat_cs_intros)
    qed (auto simp: cat_cs_intros)
    from assms(3) show const_b_is_functor: 
      "cf_const 𝔍 ℭ b : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
      by (auto intro: cf_const_is_functor cat_cs_intros)
    show "vcard (ntcf_const 𝔍 ℭ f) = 5⇩ℕ"
      unfolding ntcf_const_def by (simp add: nat_omega_simps)
    show 
      "ntcf_const 𝔍 ℭ f⦇NTMap⦈⦇a'⦈ : 
        cf_const 𝔍 ℭ a⦇ObjMap⦈⦇a'⦈ ↦⇘ℭ⇙ cf_const 𝔍 ℭ b⦇ObjMap⦈⦇a'⦈"
      if "a' ∈⇩∘ 𝔍⦇Obj⦈" for a'
      by (simp add: that assms(3) ntcf_const_components(1) dghm_const_ObjMap_app)
    from assms(3) show 
      "ntcf_const 𝔍 ℭ f⦇NTMap⦈⦇b'⦈ ∘⇩A⇘ℭ⇙ cf_const 𝔍 ℭ a⦇ArrMap⦈⦇f'⦈ =
        cf_const 𝔍 ℭ b ⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘ℭ⇙ ntcf_const 𝔍 ℭ f⦇NTMap⦈⦇a'⦈"
      if "f' : a' ↦⇘𝔍⇙ b'" for f' a' b'
      using that dghm_const_ArrMap_app 
      by (auto simp: ntcf_const_components cat_cs_intros cat_cs_simps)
  qed (use assms(3) in ‹auto simp: ntcf_const_components›)
qed 

lemma ntcf_const_is_ntcf'[cat_cs_intros]:
  assumes "category α 𝔍" 
    and "category α ℭ"
    and "f : a ↦⇘ℭ⇙ b"
    and "𝔄 = cf_const 𝔍 ℭ a"
    and "𝔅 = cf_const 𝔍 ℭ b"
    and "𝔍' = 𝔍"
    and "ℭ' = ℭ"
  shows "ntcf_const 𝔍 ℭ f : 𝔄 ↦⇩C⇩F 𝔅 : 𝔍' ↦↦⇩C⇘α⇙ ℭ'"
  using assms(1-3) unfolding assms(4-7) by (rule ntcf_const_is_ntcf)


subsubsection‹Opposite constant natural transformation›

lemma op_ntcf_ntcf_const[cat_op_simps]: 
  "op_ntcf (ntcf_const 𝔍 ℭ f) = ntcf_const (op_cat 𝔍) (op_cat ℭ) f"
  unfolding 
    nt_field_simps dghm_field_simps dg_field_simps
    dghm_const_def ntcf_const_def op_cat_def op_cf_def op_ntcf_def 
  by (simp_all add: nat_omega_simps)


subsubsection‹Further properties›

lemma ntcf_const_ntcf_vcomp[cat_cs_simps]:
  assumes "category α 𝔍" 
    and "category α ℭ" 
    and "g : b ↦⇘ℭ⇙ c" 
    and "f : a ↦⇘ℭ⇙ b"
  shows "ntcf_const 𝔍 ℭ g ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f = ntcf_const 𝔍 ℭ (g ∘⇩A⇘ℭ⇙ f)"
proof-
  interpret 𝔍: category α 𝔍 by (rule assms(1))
  interpret ℭ: category α ℭ by (rule assms(2))
  from assms(3,4) have gf: "g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c" by (simp add: cat_cs_intros)
  note 𝔍ℭg = ntcf_const_is_ntcf[OF assms(1,2,3)] 
    and 𝔍ℭf = ntcf_const_is_ntcf[OF assms(1,2,4)]
  show ?thesis
  proof(rule ntcf_eqI)
    from ntcf_const_is_ntcf[OF assms(1,2,3)] ntcf_const_is_ntcf[OF assms(1,2,4)]
    show 
      "ntcf_const 𝔍 ℭ g ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f :
        cf_const 𝔍 ℭ a ↦⇩C⇩F cf_const 𝔍 ℭ c : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
      by (rule ntcf_vcomp_is_ntcf)
    show
      "ntcf_const 𝔍 ℭ (g ∘⇩A⇘ℭ⇙ f) : 
        cf_const 𝔍 ℭ a ↦⇩C⇩F cf_const 𝔍 ℭ c : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
      by (rule ntcf_const_is_ntcf[OF assms(1,2) gf])
    show "(ntcf_const 𝔍 ℭ g ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f)⦇NTMap⦈ = 
      ntcf_const 𝔍 ℭ (g ∘⇩A⇘ℭ⇙ f)⦇NTMap⦈"
      unfolding ntcf_const_components
    proof(rule vsv_eqI, unfold ntcf_vcomp_NTMap_vdomain[OF 𝔍ℭf])
      fix a assume prems: "a ∈⇩∘ 𝔍⦇Obj⦈"
      then show 
        "(ntcf_const 𝔍 ℭ g ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f)⦇NTMap⦈⦇a⦈ =
          vconst_on (𝔍⦇Obj⦈) (g ∘⇩A⇘ℭ⇙ f)⦇a⦈"
        unfolding ntcf_vcomp_NTMap_app[OF 𝔍ℭg 𝔍ℭf prems]  
        by (simp add: ntcf_const_components)
    qed (simp_all add: ntsmcf_vcomp_components)
  qed auto
qed

lemma ntcf_id_cf_const[cat_cs_simps]: 
  assumes "category α 𝔍" and "category α ℭ" and "c ∈⇩∘ ℭ⦇Obj⦈"
  shows "ntcf_id (cf_const 𝔍 ℭ c) = ntcf_const 𝔍 ℭ (ℭ⦇CId⦈⦇c⦈)"
proof(rule ntcf_eqI)
  interpret 𝔍: category α 𝔍 by (rule assms(1))
  interpret ℭ: category α ℭ by (rule assms(2))
  from assms show "ntcf_const 𝔍 ℭ (ℭ⦇CId⦈⦇c⦈) : 
    cf_const 𝔍 ℭ c ↦⇩C⇩F cf_const 𝔍 ℭ c : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
    by (auto intro: ntcf_const_is_ntcf)
  interpret const_c: is_functor α 𝔍 ℭ ‹cf_const 𝔍 ℭ c›
    by (rule cf_const_is_functor) (auto simp: assms(3) cat_cs_intros)
  show "ntcf_id (cf_const 𝔍 ℭ c) : 
    cf_const 𝔍 ℭ c ↦⇩C⇩F cf_const 𝔍 ℭ c : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
    by (rule const_c.cf_ntcf_id_is_ntcf)
  show "ntcf_id (cf_const 𝔍 ℭ c)⦇NTMap⦈ = ntcf_const 𝔍 ℭ (ℭ⦇CId⦈⦇c⦈)⦇NTMap⦈"
  proof(rule vsv_eqI, unfold ntcf_const_components)
    show "vsv (ntcf_id (cf_const 𝔍 ℭ c)⦇NTMap⦈)"
      unfolding ntcf_id_components by (auto simp: cat_cs_simps intro: vsv_vcomp)
  qed (auto simp: cat_cs_simps)
qed simp_all

lemma ntcf_cf_comp_cf_const_right[cat_cs_simps]:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "category α 𝔄"
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F cf_const 𝔄 𝔅 b = ntcf_const 𝔄 ℭ (𝔑⦇NTMap⦈⦇b⦈)"
proof-
  interpret 𝔑: is_ntcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret 𝔄: category α 𝔄 by (rule assms(2))
  show ?thesis
  proof(rule ntcf_eqI)
    from assms(3) show "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F cf_const 𝔄 𝔅 b :
      cf_const 𝔄 ℭ (𝔉⦇ObjMap⦈⦇b⦈) ↦⇩C⇩F cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈) :
      𝔄 ↦↦⇩C⇘α⇙ ℭ"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms(3) show "ntcf_const 𝔄 ℭ (𝔑⦇NTMap⦈⦇b⦈) :
      cf_const 𝔄 ℭ (𝔉⦇ObjMap⦈⦇b⦈) ↦⇩C⇩F cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈) :
      𝔄 ↦↦⇩C⇘α⇙ ℭ"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms(3) have dom_lhs: 
      "𝒟⇩∘ ((𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F cf_const 𝔄 𝔅 b)⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms(3) have dom_rhs: 
      "𝒟⇩∘ (ntcf_const 𝔄 ℭ (𝔑⦇NTMap⦈⦇b⦈)⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show 
      "(𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F cf_const 𝔄 𝔅 b)⦇NTMap⦈ = ntcf_const 𝔄 ℭ (𝔑⦇NTMap⦈⦇b⦈)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
      with assms(3) show 
        "(𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F cf_const 𝔄 𝔅 b)⦇NTMap⦈⦇a⦈ =
          ntcf_const 𝔄 ℭ (𝔑⦇NTMap⦈⦇b⦈)⦇NTMap⦈⦇a⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed (auto intro: cat_cs_intros)
  qed simp_all
qed

lemma cf_ntcf_comp_ntcf_id[cat_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔉 = ntcf_id 𝔊 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉"
proof-
  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
  interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
  proof(rule ntcf_eqI)
    show "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔉 : 𝔊 ∘⇩C⇩F 𝔉 ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    show "ntcf_id 𝔊 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉 : 𝔊 ∘⇩C⇩F 𝔉 ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    have dom_lhs: "𝒟⇩∘ ((𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    have dom_rhs: "𝒟⇩∘ ((ntcf_id 𝔊 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show "(𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈ = (ntcf_id 𝔊 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
      then show 
        "(𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈⦇a⦈ =
          (ntcf_id 𝔊 ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉)⦇NTMap⦈⦇a⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed (cs_concl cs_intro: cat_cs_intros)
  qed simp_all
qed

lemma (in is_functor) cf_ntcf_cf_comp_ntcf_const[cat_cs_simps]:
  assumes "category α ℭ" and "f : a ↦⇘ℭ⇙ b"
  shows "ntcf_const 𝔅 ℭ f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉 = ntcf_const 𝔄 ℭ f"
proof(rule ntcf_eqI)
  interpret ℭ: category α ℭ by (rule assms(1))
  from assms(2) show "ntcf_const 𝔅 ℭ f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉 : 
    cf_const 𝔄 ℭ a ↦⇩C⇩F cf_const 𝔄 ℭ b : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  then have dom_lhs: "𝒟⇩∘ ((ntcf_const 𝔅 ℭ f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉)⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from assms(2) show 
    "ntcf_const 𝔄 ℭ f : cf_const 𝔄 ℭ a ↦⇩C⇩F cf_const 𝔄 ℭ b : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  then have dom_rhs: "𝒟⇩∘ (ntcf_const 𝔄 ℭ f⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  show "(ntcf_const 𝔅 ℭ f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉)⦇NTMap⦈ = ntcf_const 𝔄 ℭ f⦇NTMap⦈"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
    then show 
      "(ntcf_const 𝔅 ℭ f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉)⦇NTMap⦈⦇a⦈ = ntcf_const 𝔄 ℭ f⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed simp_all

lemmas [cat_cs_simps] = is_functor.cf_ntcf_cf_comp_ntcf_const

lemma (in is_functor) cf_ntcf_comp_cf_ntcf_const[cat_cs_simps]:
  assumes "category α 𝔍"
    and "f : r' ↦⇘𝔄⇙ r"
  shows "𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔄 f = ntcf_const 𝔍 𝔅 (𝔉⦇ArrMap⦈⦇f⦈)"
proof(rule ntcf_eqI)
  interpret 𝔍: category α 𝔍 by (rule assms(1))
  from assms(2) have r': "r' ∈⇩∘ 𝔄⦇Obj⦈" and r: "r ∈⇩∘ 𝔄⦇Obj⦈" by auto
  from assms(2) show "𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔄 f :
    cf_const 𝔍 𝔅 (𝔉⦇ObjMap⦈⦇r'⦈) ↦⇩C⇩F cf_const 𝔍 𝔅 (𝔉⦇ObjMap⦈⦇r⦈) :
    𝔍 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  with assms(2) have dom_lhs: 
    "𝒟⇩∘ ((𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔄 f)⦇NTMap⦈) = 𝔍⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  from assms(2) show "ntcf_const 𝔍 𝔅 (𝔉⦇ArrMap⦈⦇f⦈) :
    cf_const 𝔍 𝔅 (𝔉⦇ObjMap⦈⦇r'⦈) ↦⇩C⇩F cf_const 𝔍 𝔅 (𝔉⦇ObjMap⦈⦇r⦈) :
    𝔍 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  with assms(2) have dom_rhs:
    "𝒟⇩∘ (ntcf_const 𝔍 𝔅 (𝔉⦇ArrMap⦈⦇f⦈)⦇NTMap⦈) = 𝔍⦇Obj⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  show 
    "(𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔄 f)⦇NTMap⦈ = 
      ntcf_const 𝔍 𝔅 (𝔉⦇ArrMap⦈⦇f⦈)⦇NTMap⦈"
    by (rule vsv_eqI, unfold dom_lhs dom_rhs)
      (
        use assms(2) in 
          ‹cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros›
      )+
qed simp_all

lemmas [cat_cs_simps] = is_functor.cf_ntcf_comp_cf_ntcf_const



subsection‹Natural isomorphism›


text‹See Chapter I-4 in \<^cite>‹"mac_lane_categories_2010"›.›

locale is_iso_ntcf = is_ntcf +
  assumes iso_ntcf_is_iso_arr[cat_arrow_cs_intros]: 
    "a ∈⇩∘ 𝔄⦇Obj⦈ ⟹ 𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"

syntax "_is_iso_ntcf" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ : _ ↦⇩C⇩F⇩.⇩i⇩s⇩o _ : _ ↦↦⇩Cı _)› [51, 51, 51, 51, 51] 51)
translations "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" ⇌ 
  "CONST is_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑"

lemma (in is_iso_ntcf) iso_ntcf_is_iso_arr':
  assumes "a ∈⇩∘ 𝔄⦇Obj⦈" 
    and "A = 𝔉⦇ObjMap⦈⦇a⦈"
    and "B = 𝔊⦇ObjMap⦈⦇a⦈"
  shows "𝔑⦇NTMap⦈⦇a⦈ : A ↦⇩i⇩s⇩o⇘𝔅⇙ B"
  using assms by (auto intro: cat_arrow_cs_intros)

lemmas [cat_arrow_cs_intros] = 
  is_iso_ntcf.iso_ntcf_is_iso_arr'

lemma (in is_iso_ntcf) iso_ntcf_is_iso_arr'':
  assumes "a ∈⇩∘ 𝔄⦇Obj⦈" 
    and "A = 𝔉⦇ObjMap⦈⦇a⦈"
    and "B = 𝔊⦇ObjMap⦈⦇a⦈"
    and "F = 𝔑⦇NTMap⦈⦇a⦈"
    and "𝔅' = 𝔅"
  shows "F : A ↦⇩i⇩s⇩o⇘𝔅'⇙ B"
  using assms by (auto intro: cat_arrow_cs_intros)


text‹Rules.›

lemma (in is_iso_ntcf) is_iso_ntcf_axioms'[cat_cs_intros]: 
  assumes "α' = α" and "𝔉' = 𝔉" and "𝔊' = 𝔊" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔑 : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_iso_ntcf_axioms)

mk_ide rf is_iso_ntcf_def[unfolded is_iso_ntcf_axioms_def]
  |intro is_iso_ntcfI|
  |dest is_iso_ntcfD[dest]|
  |elim is_iso_ntcfE[elim]|

lemmas [ntcf_cs_intros] = is_iso_ntcfD(1)



subsection‹Inverse natural transformation›


subsubsection‹Definition and elementary properties›

definition inv_ntcf :: "V ⇒ V"
  where "inv_ntcf 𝔑 =
    [
      (λa∈⇩∘𝔑⦇NTDGDom⦈⦇Obj⦈. SOME g. is_inverse (𝔑⦇NTDGCod⦈) g (𝔑⦇NTMap⦈⦇a⦈)),
      𝔑⦇NTCod⦈,
      𝔑⦇NTDom⦈,
      𝔑⦇NTDGDom⦈,
      𝔑⦇NTDGCod⦈
    ]⇩∘"


text‹Slicing.›

lemma inv_ntcf_components:
  shows "inv_ntcf 𝔑⦇NTMap⦈ = 
    (λa∈⇩∘𝔑⦇NTDGDom⦈⦇Obj⦈. SOME g. is_inverse (𝔑⦇NTDGCod⦈) g (𝔑⦇NTMap⦈⦇a⦈))" 
    and [cat_cs_simps]: "inv_ntcf 𝔑⦇NTDom⦈ = 𝔑⦇NTCod⦈" 
    and [cat_cs_simps]: "inv_ntcf 𝔑⦇NTCod⦈ = 𝔑⦇NTDom⦈"
    and [cat_cs_simps]: "inv_ntcf 𝔑⦇NTDGDom⦈ = 𝔑⦇NTDGDom⦈" 
    and [cat_cs_simps]: "inv_ntcf 𝔑⦇NTDGCod⦈ = 𝔑⦇NTDGCod⦈" 
  unfolding inv_ntcf_def nt_field_simps by (simp_all add: nat_omega_simps)


text‹Components.›

lemma (in is_iso_ntcf) is_iso_ntcf_inv_ntcf_components[cat_cs_simps]: 
  "inv_ntcf 𝔑⦇NTDom⦈ = 𝔊"
  "inv_ntcf 𝔑⦇NTCod⦈ = 𝔉"
  "inv_ntcf 𝔑⦇NTDGDom⦈ = 𝔄"
  "inv_ntcf 𝔑⦇NTDGCod⦈ = 𝔅"
  unfolding inv_ntcf_components by (simp_all add: cat_cs_simps)


subsubsection‹Natural transformation map›

lemma inv_ntcf_NTMap_vsv[cat_cs_intros]: "vsv (inv_ntcf 𝔑⦇NTMap⦈)"
  unfolding inv_ntcf_components by auto

lemma (in is_iso_ntcf) iso_ntcf_inv_ntcf_NTMap_app_is_inverse[cat_cs_intros]:
  assumes "a ∈⇩∘ 𝔄⦇Obj⦈"
  shows "is_inverse 𝔅 (inv_ntcf 𝔑⦇NTMap⦈⦇a⦈) (𝔑⦇NTMap⦈⦇a⦈)"
proof-
  from assms is_iso_ntcf_axioms have "∃g. is_inverse 𝔅 g (𝔑⦇NTMap⦈⦇a⦈)" by auto
  from assms someI2_ex[OF this] show 
    "is_inverse 𝔅 (inv_ntcf 𝔑⦇NTMap⦈⦇a⦈) (𝔑⦇NTMap⦈⦇a⦈)"
    unfolding inv_ntcf_components by (simp add: cat_cs_simps)
qed

lemma (in is_iso_ntcf) iso_ntcf_inv_ntcf_NTMap_app_is_the_inverse[cat_cs_intros]:
  assumes "a ∈⇩∘ 𝔄⦇Obj⦈"
  shows "inv_ntcf 𝔑⦇NTMap⦈⦇a⦈ = (𝔑⦇NTMap⦈⦇a⦈)¯⇩C⇘𝔅⇙"
proof- 
  have "is_inverse 𝔅 (inv_ntcf 𝔑⦇NTMap⦈⦇a⦈) (𝔑⦇NTMap⦈⦇a⦈)"
    by (rule iso_ntcf_inv_ntcf_NTMap_app_is_inverse[OF assms])
  from NTDom.HomCod.cat_is_inverse_eq_the_inverse[OF this] show ?thesis .
qed

lemmas [cat_cs_simps] = is_iso_ntcf.iso_ntcf_inv_ntcf_NTMap_app_is_the_inverse

lemma (in is_ntcf) inv_ntcf_NTMap_vdomain[cat_cs_simps]: 
  "𝒟⇩∘ (inv_ntcf 𝔑⦇NTMap⦈) = 𝔄⦇Obj⦈"
  unfolding inv_ntcf_components by (simp add: cat_cs_simps)

lemmas [cat_cs_simps] = is_ntcf.inv_ntcf_NTMap_vdomain

lemma (in is_iso_ntcf) inv_ntcf_NTMap_vrange: 
  "ℛ⇩∘ (inv_ntcf 𝔑⦇NTMap⦈) ⊆⇩∘ 𝔅⦇Arr⦈"
proof(rule vsubsetI)
  interpret inv_𝔑: vsv ‹inv_ntcf 𝔑⦇NTMap⦈› by (rule inv_ntcf_NTMap_vsv)
  fix f assume "f ∈⇩∘ ℛ⇩∘ (inv_ntcf 𝔑⦇NTMap⦈)"
  then obtain a 
    where f_def: "f = inv_ntcf 𝔑⦇NTMap⦈⦇a⦈" and "a ∈⇩∘ 𝒟⇩∘ (inv_ntcf 𝔑⦇NTMap⦈)"
    by (blast elim: inv_𝔑.vrange_atE)
  then have "a ∈⇩∘ 𝔄⦇Obj⦈" by (simp add: cat_cs_simps)
  then have "is_inverse 𝔅 f (𝔑⦇NTMap⦈⦇a⦈)" 
    unfolding f_def by (intro iso_ntcf_inv_ntcf_NTMap_app_is_inverse)    
  then show "f ∈⇩∘ 𝔅⦇Arr⦈" by auto
qed


subsubsection‹Opposite natural isomorphism›

lemma (in is_iso_ntcf) is_iso_ntcf_op: 
  "op_ntcf 𝔑 : op_cf 𝔊 ↦⇩C⇩F⇩.⇩i⇩s⇩o op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇘α⇙ op_cat 𝔅"
proof-
  from is_iso_ntcf_axioms have 
    "op_ntcf 𝔑 : op_cf 𝔊 ↦⇩C⇩F op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇘α⇙ op_cat 𝔅"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
  then show ?thesis 
    by (intro is_iso_ntcfI) (auto simp: cat_op_simps cat_arrow_cs_intros)
qed

lemma (in is_iso_ntcf) is_iso_ntcf_op'[cat_op_intros]:
  assumes "𝔊' = op_cf 𝔊"
    and "𝔉' = op_cf 𝔉"
    and "𝔄' = op_cat 𝔄"
    and "𝔅' = op_cat 𝔅"
  shows "op_ntcf 𝔑 : 𝔊' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉' : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
  unfolding assms by (rule is_iso_ntcf_op)

lemmas is_iso_ntcf_op[cat_op_intros] = is_iso_ntcf.is_iso_ntcf_op



subsection‹A natural isomorphism is an isomorphism in the category ‹Funct››

text‹
The results that are presented in this subsection can be found in 
nLab (see \<^cite>‹"noauthor_nlab_nodate"›\footnote{\url{
https://ncatlab.org/nlab/show/natural+isomorphism
}}).
›

lemma is_iso_arr_is_iso_ntcf:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔐 : 𝔊 ↦⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑 ∙⇩N⇩T⇩C⇩F 𝔐 = ntcf_id 𝔊"
    and "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 = ntcf_id 𝔉"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof-
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔊 𝔉 𝔐 by (rule assms(2))
  show ?thesis
  proof(rule is_iso_ntcfI)
    fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈" 
    show "𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"
    proof(rule is_iso_arrI)
      show "is_inverse 𝔅 (𝔐⦇NTMap⦈⦇a⦈) (𝔑⦇NTMap⦈⦇a⦈)"  
      proof(rule is_inverseI)
        from prems have 
          "𝔐⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈ = (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈"
          by (simp add: ntcf_vcomp_NTMap_app[OF assms(2,1) prems])
        also have "… = ntcf_id 𝔉⦇NTMap⦈⦇a⦈" unfolding assms(4) by simp
        also from prems 𝔑.NTDom.ntcf_id_NTMap_app_vdomain have 
          "… = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
          unfolding ntcf_id_components by auto
        finally show "𝔐⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈".
        from prems have 
          "𝔑⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ 𝔐⦇NTMap⦈⦇a⦈ = (𝔑 ∙⇩N⇩T⇩C⇩F 𝔐)⦇NTMap⦈⦇a⦈"
          by (simp add: ntcf_vcomp_NTMap_app[OF assms(1,2) prems])
        also have "… = ntcf_id 𝔊⦇NTMap⦈⦇a⦈" unfolding assms(3) by simp
        also from prems 𝔑.NTCod.ntcf_id_NTMap_app_vdomain have 
          "… = 𝔅⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈"
          unfolding ntcf_id_components by auto
        finally show "𝔑⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ 𝔐⦇NTMap⦈⦇a⦈ = 𝔅⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈".
      qed (auto simp: prems cat_cs_intros)
    qed (auto simp: prems cat_cs_intros)
  qed (auto simp: cat_cs_intros)
qed

lemma iso_ntcf_is_iso_arr:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows [ntcf_cs_intros]: "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔑 = ntcf_id 𝔊"
    and "inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F 𝔑 = ntcf_id 𝔉"
proof-

  interpret is_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  
  define m where "m a = inv_ntcf 𝔑⦇NTMap⦈⦇a⦈" for a
  have is_inverse[intro]: "a ∈⇩∘ 𝔄⦇Obj⦈ ⟹ is_inverse 𝔅 (m a) (𝔑⦇NTMap⦈⦇a⦈)" 
    for a
    unfolding m_def by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  have [dest, intro, simp]: 
    "a ∈⇩∘ 𝔄⦇Obj⦈ ⟹ m a : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈" for a
  proof-
    assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈" 
    from prems have "𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈" 
      by (auto intro: cat_cs_intros cat_arrow_cs_intros)
    with is_inverse[OF prems] show "m a : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
      by 
        (
          meson 
            NTDom.HomCod.cat_is_inverse_is_iso_arr is_iso_arrD
        )
  qed
  have [intro]: 
    "f : a ↦⇘𝔄⇙ b ⟹ m b ∘⇩A⇘𝔅⇙ 𝔊⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ m a"
    for f a b
  proof-
    assume prems: "f : a ↦⇘𝔄⇙ b"
    then have ma: "m a : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈" 
      and mb: "m b : 𝔊⦇ObjMap⦈⦇b⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
      and 𝔊f: "𝔊⦇ArrMap⦈⦇f⦈ : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇b⦈" 
      and 𝔑a: "𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"
      and 𝔉f: "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
      and 𝔑b: "𝔑⦇NTMap⦈⦇b⦈ : 𝔉⦇ObjMap⦈⦇b⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇b⦈"
      by (auto intro: cat_cs_intros)
    then have 𝔑b𝔉f: 
      "𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇b⦈"
      by (auto intro: cat_cs_intros)
    from prems have inv_ma: "is_inverse 𝔅 (m a) (𝔑⦇NTMap⦈⦇a⦈)" 
      and inv_mb: "is_inverse 𝔅 (𝔑⦇NTMap⦈⦇b⦈) (m b)"
      by (auto simp: is_inverse_sym)
    from mb have mb_𝔑b: "m b ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇b⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇b⦈⦈"
      by (auto intro: is_inverse_Comp_CId_right[OF inv_mb])
    from prems have 𝔑a_ma: "𝔑⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ m a = 𝔅⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈" 
      using 𝔑a inv_ma ma by (meson is_inverse_Comp_CId_right)
    from 𝔊f have "m b ∘⇩A⇘𝔅⇙ 𝔊⦇ArrMap⦈⦇f⦈ = 
      m b ∘⇩A⇘𝔅⇙ (𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ (𝔑⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ m a))"
      unfolding 𝔑a_ma by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    also have "… = m b ∘⇩A⇘𝔅⇙ ((𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈) ∘⇩A⇘𝔅⇙ m a)"
      by 
         (
          metis 
            ma 𝔊f 𝔑a NTDom.HomCod.cat_Comp_assoc is_iso_arrD(1)
        )
    also from prems have 
      "… = m b ∘⇩A⇘𝔅⇙ ((𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈) ∘⇩A⇘𝔅⇙ m a)"
      by (metis ntcf_Comp_commute)
    also have "… = (m b ∘⇩A⇘𝔅⇙ (𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈)) ∘⇩A⇘𝔅⇙ m a"
      by 
        (
          metis 
            𝔑b𝔉f ma mb NTDom.HomCod.cat_Comp_assoc is_iso_arrD(1)
        )
    also from 𝔉f 𝔑b mb NTDom.HomCod.cat_Comp_assoc have 
      "… =  ((m b ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇b⦈) ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈) ∘⇩A⇘𝔅⇙ m a"
      by (metis is_iso_arrD(1))
    also from 𝔉f have "… = 𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ m a" 
      unfolding mb_𝔑b by (simp add: cat_cs_simps)
    finally show "m b ∘⇩A⇘𝔅⇙ 𝔊⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ m a" by simp
  qed

  show 𝔐: "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  proof(intro is_iso_ntcfI is_ntcfI', unfold m_def[symmetric])
    show "vfsequence (inv_ntcf 𝔑)" unfolding inv_ntcf_def by simp
    show "vcard (inv_ntcf 𝔑) = 5⇩ℕ"
      unfolding inv_ntcf_def by (simp add: nat_omega_simps)
  qed (auto simp: cat_cs_simps intro: cat_cs_intros)

  interpret 𝔐: is_iso_ntcf α 𝔄 𝔅 𝔊 𝔉 ‹inv_ntcf 𝔑› by (rule 𝔐)

  show 𝔑𝔐: "𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔑 = ntcf_id 𝔊"
  proof(rule ntcf_eqI)
    from NTCod.cf_ntcf_id_is_ntcf show "ntcf_id 𝔊 : 𝔊 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
      by auto
    show "(𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔑)⦇NTMap⦈ = ntcf_id 𝔊⦇NTMap⦈"
    proof(rule vsv_eqI)
      fix a assume "a ∈⇩∘ 𝒟⇩∘ ((𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔑)⦇NTMap⦈)"
      then have "a ∈⇩∘ 𝔄⦇Obj⦈"
        unfolding ntcf_vcomp_NTMap_vdomain[OF 𝔐.is_ntcf_axioms] by simp
      then show "(𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔑)⦇NTMap⦈⦇a⦈ = ntcf_id 𝔊⦇NTMap⦈⦇a⦈"
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps 
              cs_intro: cat_cs_intros cat_arrow_cs_intros
          )
    qed 
      (
        auto 
          simp: ntsmcf_vcomp_components(1) cat_cs_simps 
          intro: cat_cs_intros
      )
  qed (auto intro: cat_cs_intros)
    
  show 𝔐𝔑: "inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F 𝔑 = ntcf_id 𝔉"
  proof(rule ntcf_eqI)
    show "(inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈ = ntcf_id 𝔉⦇NTMap⦈"
    proof(rule vsv_eqI)
      show "𝒟⇩∘ ((inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈) = 𝒟⇩∘ (ntcf_id 𝔉⦇NTMap⦈)" 
        by (simp add: ntsmcf_vcomp_components(1) cat_cs_simps)
      fix a assume "a ∈⇩∘ 𝒟⇩∘ ((inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈)"
      then have "a ∈⇩∘ 𝔄⦇Obj⦈" 
        unfolding ntsmcf_vcomp_components by (simp add: cat_cs_simps)    
      then show "(inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ = ntcf_id 𝔉⦇NTMap⦈⦇a⦈"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_cs_simps 
              cs_intro: cat_cs_intros cat_arrow_cs_intros
          )
    qed 
      (
        auto simp: 
          ntsmcf_vcomp_components(1) 
          ntcf_id_components(1) 
          cat_cs_simps 
          intro: vsv_vcomp
      )
  qed (auto intro: cat_cs_intros)
qed


subsubsection‹
The operation of taking the inverse natural transformation is an involution
›

lemma (in is_iso_ntcf) iso_ntcf_inv_ntcf_inv_ntcf[ntcf_cs_simps]: 
  "inv_ntcf (inv_ntcf 𝔑) = 𝔑"
proof(rule ntcf_eqI)
  show "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by (cs_concl cs_intro: cat_cs_intros)
  show "inv_ntcf (inv_ntcf 𝔑) : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_intro: ntcf_cs_intros cat_cs_intros)
  then have dom_lhs: "𝒟⇩∘ (inv_ntcf (inv_ntcf 𝔑)⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  show "inv_ntcf (inv_ntcf 𝔑)⦇NTMap⦈ = 𝔑⦇NTMap⦈"
  proof(rule vsv_eqI, unfold cat_cs_simps dom_lhs)
    fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
    then show "inv_ntcf (inv_ntcf 𝔑)⦇NTMap⦈⦇a⦈ = 𝔑⦇NTMap⦈⦇a⦈"
      by
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps
            cs_intro: cat_arrow_cs_intros ntcf_cs_intros cat_cs_intros
        )
  qed (auto intro: cat_cs_intros)
qed simp_all

lemmas [ntcf_cs_simps] = is_iso_ntcf.iso_ntcf_inv_ntcf_inv_ntcf


subsubsection‹Natural isomorphisms from natural transformations›

lemma iso_ntcf_if_is_inverse:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔐 : 𝔊 ↦⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "⋀a. a ∈⇩∘ 𝔄⦇Obj⦈ ⟹ is_inverse 𝔅 (𝔐⦇NTMap⦈⦇a⦈) (𝔑⦇NTMap⦈⦇a⦈)"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔐 : 𝔊 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔐 = inv_ntcf 𝔑"
    and "𝔑 = inv_ntcf 𝔐"
proof-
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔊 𝔉 𝔐 by (rule assms(2))
  show 𝔑: "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  proof(intro is_iso_ntcfI assms(1))
    fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
    show "𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"
      by
        (
          rule is_iso_arrI[
            OF 𝔑.ntcf_NTMap_is_arr[OF prems] assms(3)[OF prems]
            ]
        )
  qed
  show 𝔐: "𝔐 : 𝔊 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  proof(intro is_iso_ntcfI assms(2))
    fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
    show "𝔐⦇NTMap⦈⦇a⦈ : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
      by
        (
          rule is_iso_arrI
            [
              OF 
                𝔐.ntcf_NTMap_is_arr[OF prems] 
                is_inverse_sym[THEN iffD1, OF assms(3)[OF prems]]
            ]
        )
  qed
  have 𝔐_NTMap_unique: "g = 𝔐⦇NTMap⦈⦇a⦈" 
    if "a ∈⇩∘ 𝔄⦇Obj⦈" and "is_inverse 𝔅 g (𝔑⦇NTMap⦈⦇a⦈)" for g a
    by (rule 𝔑.NTDom.HomCod.cat_is_inverse_eq[OF that(2) assms(3)[OF that(1)]])
  show "𝔐 = inv_ntcf 𝔑"
  proof(rule ntcf_eqI, rule assms(2))
    from 𝔑 show "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
      by (cs_concl cs_shallow cs_intro: ntcf_cs_intros)
    show "𝔐⦇NTMap⦈ = inv_ntcf 𝔑⦇NTMap⦈"
    proof(rule vsv_eqI, unfold cat_cs_simps)
      fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
      show "𝔐⦇NTMap⦈⦇a⦈ = inv_ntcf 𝔑⦇NTMap⦈⦇a⦈"
      proof(intro 𝔐_NTMap_unique[symmetric] prems)
        from prems assms(3)[OF prems] show 
          "is_inverse 𝔅 (inv_ntcf 𝔑⦇NTMap⦈⦇a⦈) (𝔑⦇NTMap⦈⦇a⦈)"
          unfolding inv_ntcf_components cat_cs_simps
          by 
            (
              cs_concl cs_shallow 
                cs_intro: V_cs_intros cs_simp: some_eq_ex V_cs_simps
            )
      qed
    qed (auto simp: inv_ntcf_components)
  qed simp_all
  then have "inv_ntcf (inv_ntcf 𝔑) = inv_ntcf 𝔐" by simp
  from this 𝔐 𝔑 show "𝔑 = inv_ntcf 𝔐" 
    by (cs_prems cs_shallow cs_simp: ntcf_cs_simps)
qed


subsubsection‹Vertical composition of natural isomorphisms›

lemma ntcf_vcomp_is_iso_ntcf[cat_cs_intros]:
  assumes "𝔐 : 𝔊 ↦⇩C⇩F⇩.⇩i⇩s⇩o ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof(intro is_iso_arr_is_iso_ntcf)
  note inv_ntcf_𝔐 = iso_ntcf_is_iso_arr[OF assms(1)]
    and inv_ntcf_𝔑 = iso_ntcf_is_iso_arr[OF assms(2)]
  note [cat_cs_simps] = inv_ntcf_𝔐(2,3) inv_ntcf_𝔑(2,3)
  from assms show "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 : 𝔉 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_intro: cat_cs_intros ntcf_cs_intros)
  from inv_ntcf_𝔐(1) inv_ntcf_𝔑(1) show 
    "inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔐 : ℌ ↦⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_intro: cat_cs_intros ntcf_cs_intros)
  from assms inv_ntcf_𝔐(1) inv_ntcf_𝔑(1) have 
    "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 ∙⇩N⇩T⇩C⇩F (inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔐) = 
      𝔐 ∙⇩N⇩T⇩C⇩F (𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔑) ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔐"
    by 
      (
        cs_concl 
          cs_simp: ntcf_vcomp_assoc cs_intro: cat_cs_intros ntcf_cs_intros
      )
  also from assms have "… = ntcf_id ℌ"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: ntcf_cs_intros)
  finally show "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 ∙⇩N⇩T⇩C⇩F (inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔐) = ntcf_id ℌ"
    by simp
  from assms inv_ntcf_𝔐(1) inv_ntcf_𝔑(1) have 
    "inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔐 ∙⇩N⇩T⇩C⇩F (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) = 
      inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F (inv_ntcf 𝔐 ∙⇩N⇩T⇩C⇩F 𝔐) ∙⇩N⇩T⇩C⇩F 𝔑"
    by 
      (
        cs_concl 
          cs_simp: ntcf_vcomp_assoc cs_intro: cat_cs_intros ntcf_cs_intros
      )
  also from assms have "… = ntcf_id 𝔉"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: ntcf_cs_intros)
  finally show "inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔐 ∙⇩N⇩T⇩C⇩F (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) = ntcf_id 𝔉"
    by simp
qed


subsubsection‹Horizontal composition of natural isomorphisms›

lemma ntcf_hcomp_is_iso_ntcf:
  assumes "𝔐 : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔐 ∘⇩N⇩T⇩C⇩F 𝔑 : 𝔉' ∘⇩C⇩F 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
proof(intro is_iso_arr_is_iso_ntcf)
  note inv_ntcf_𝔐 = iso_ntcf_is_iso_arr[OF assms(1)]
    and inv_ntcf_𝔑 = iso_ntcf_is_iso_arr[OF assms(2)]
  note [cat_cs_simps] = inv_ntcf_𝔐(2,3) inv_ntcf_𝔑(2,3)
  from assms show "𝔐 ∘⇩N⇩T⇩C⇩F 𝔑 : 𝔉' ∘⇩C⇩F 𝔉 ↦⇩C⇩F 𝔊' ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_intro: cat_cs_intros ntcf_cs_intros)
  from inv_ntcf_𝔐(1) inv_ntcf_𝔑(1) show 
    "inv_ntcf 𝔐 ∘⇩N⇩T⇩C⇩F inv_ntcf 𝔑 : 𝔊' ∘⇩C⇩F 𝔊 ↦⇩C⇩F 𝔉' ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_intro: cat_cs_intros ntcf_cs_intros)
  from assms inv_ntcf_𝔐(1) inv_ntcf_𝔑(1) have 
    "𝔐 ∘⇩N⇩T⇩C⇩F 𝔑 ∙⇩N⇩T⇩C⇩F (inv_ntcf 𝔐 ∘⇩N⇩T⇩C⇩F inv_ntcf 𝔑) = 
      ntcf_id 𝔊' ∘⇩N⇩T⇩C⇩F ntcf_id 𝔊"
    by 
      (
        cs_concl 
          cs_simp: ntcf_comp_interchange_law[symmetric] cat_cs_simps 
          cs_intro: ntcf_cs_intros
      )
  also from assms have "… = ntcf_id (𝔊' ∘⇩C⇩F 𝔊)"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros ntcf_cs_intros
      )
  finally show 
    "𝔐 ∘⇩N⇩T⇩C⇩F 𝔑 ∙⇩N⇩T⇩C⇩F (inv_ntcf 𝔐 ∘⇩N⇩T⇩C⇩F inv_ntcf 𝔑) = ntcf_id (𝔊' ∘⇩C⇩F 𝔊)"
    by simp
  from assms inv_ntcf_𝔐(1) inv_ntcf_𝔑(1) have 
    "inv_ntcf 𝔐 ∘⇩N⇩T⇩C⇩F inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑) = 
      ntcf_id 𝔉' ∘⇩N⇩T⇩C⇩F ntcf_id 𝔉"
    by 
      (
        cs_concl 
          cs_simp: ntcf_comp_interchange_law[symmetric] cat_cs_simps
          cs_intro: ntcf_cs_intros
      )
  also from assms have "… = ntcf_id (𝔉' ∘⇩C⇩F 𝔉)"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros ntcf_cs_intros)
  finally show 
    "inv_ntcf 𝔐 ∘⇩N⇩T⇩C⇩F inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F (𝔐 ∘⇩N⇩T⇩C⇩F 𝔑) = ntcf_id (𝔉' ∘⇩C⇩F 𝔉)"
    by simp
qed

lemma ntcf_hcomp_is_iso_ntcf'[ntcf_cs_intros]:
  assumes "𝔐 : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "ℌ' = 𝔉' ∘⇩C⇩F 𝔉"
    and "ℌ'' = 𝔊' ∘⇩C⇩F 𝔊"
  shows "𝔐 ∘⇩N⇩T⇩C⇩F 𝔑 : ℌ' ↦⇩C⇩F⇩.⇩i⇩s⇩o ℌ'' : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (rule ntcf_hcomp_is_iso_ntcf)


subsubsection‹Composition of a natural isomorphism and a functor›

lemma ntcf_cf_comp_is_iso_ntcf: 
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ : 𝔉 ∘⇩C⇩F ℌ ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 ∘⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
proof(intro is_iso_ntcfI ntcf_cf_comp_is_ntcf)
  interpret 𝔑: is_iso_ntcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  show "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" by (rule 𝔑.is_ntcf_axioms)
  fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
  with assms(2) show
    "(𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ)⦇NTMap⦈⦇a⦈ : (𝔉 ∘⇩C⇩F ℌ)⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘ℭ⇙ (𝔊 ∘⇩C⇩F ℌ)⦇ObjMap⦈⦇a⦈"
    by
      (
        cs_concl
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_arrow_cs_intros
      )
qed (rule assms(2))

lemma ntcf_cf_comp_is_iso_ntcf'[cat_cs_intros]:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉' = 𝔉 ∘⇩C⇩F ℌ"
    and "𝔊' = 𝔊 ∘⇩C⇩F ℌ"
  shows "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (rule ntcf_cf_comp_is_iso_ntcf)


subsubsection‹An identity natural transformation is a natural isomorphism›

lemma (in is_functor) cf_ntcf_id_is_iso_ntcf:
  "ntcf_id 𝔉 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof-
  have "ntcf_id 𝔉 : 𝔉 ↦⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by (auto intro: cat_cs_intros)
  moreover then have "ntcf_id 𝔉 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔉 = ntcf_id 𝔉" 
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  ultimately show ?thesis by (auto intro: is_iso_arr_is_iso_ntcf)
qed

lemma (in is_functor) cf_ntcf_id_is_iso_ntcf'[ntcf_cs_intros]:
  assumes "𝔊' = 𝔉" and "ℌ' = 𝔉"
  shows "ntcf_id 𝔉 : 𝔊' ↦⇩C⇩F⇩.⇩i⇩s⇩o ℌ' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  unfolding assms by (rule cf_ntcf_id_is_iso_ntcf)

lemmas [ntcf_cs_intros] = is_functor.cf_ntcf_id_is_iso_ntcf'



subsection‹Functor isomorphism›


subsubsection‹Definition and elementary properties›


text‹See subsection 1.5 in \<^cite>‹"bodo_categories_1970"›.›

locale iso_functor =
  fixes α 𝔉 𝔊
  assumes iso_cf_is_iso_ntcf: "∃𝔄 𝔅 𝔑. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"

notation iso_functor (infixl "≈⇩C⇩Fı" 50)


text‹Rules.›

lemma iso_functorI:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔉 ≈⇩C⇩F⇘α⇙ 𝔊"
  using assms unfolding iso_functor_def by auto

lemma iso_functorD[dest]:
  assumes "𝔉 ≈⇩C⇩F⇘α⇙ 𝔊"
  shows "∃𝔄 𝔅 𝔑. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  using assms unfolding iso_functor_def by auto

lemma iso_functorE[elim]:
  assumes "𝔉 ≈⇩C⇩F⇘α⇙ 𝔊"
  obtains 𝔄 𝔅 𝔑 where "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  using assms unfolding iso_functor_def by auto


subsubsection‹A functor isomorphism is an equivalence relation›

lemma iso_functor_refl: 
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔉 ≈⇩C⇩F⇘α⇙ 𝔉"
proof(rule iso_functorI)
  from assms show "ntcf_id 𝔉 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_intro: ntcf_cs_intros)
qed

lemma iso_functor_sym[sym]:
  assumes "𝔉 ≈⇩C⇩F⇘α⇙ 𝔊"
  shows "𝔊 ≈⇩C⇩F⇘α⇙ 𝔉"
proof-
  from assms obtain 𝔄 𝔅 𝔑 where 𝔑: "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by auto
  from iso_ntcf_is_iso_arr(1)[OF 𝔑] show "𝔊 ≈⇩C⇩F⇘α⇙ 𝔉" 
    by (auto simp: iso_functorI)
qed

lemma iso_functor_trans[trans, intro]:
  assumes "𝔉 ≈⇩C⇩F⇘α⇙ 𝔊" and "𝔊 ≈⇩C⇩F⇘α⇙ ℌ"
  shows "𝔉 ≈⇩C⇩F⇘α⇙ ℌ"
proof-
  from assms(1) obtain 𝔄 𝔅 𝔑 where 𝔑: "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    by auto
  moreover from assms(2) obtain 𝔄' 𝔅' 𝔐
    where 𝔐: "𝔐 : 𝔊 ↦⇩C⇩F⇩.⇩i⇩s⇩o ℌ : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'" 
    by auto
  ultimately have "𝔊 : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'" and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by blast+
  then have eq: "𝔄' = 𝔄" "𝔅' = 𝔅" by auto
  from 𝔐 have 𝔐: "𝔐 : 𝔊 ↦⇩C⇩F⇩.⇩i⇩s⇩o ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" unfolding eq .
  from ntcf_vcomp_is_iso_ntcf[OF 𝔐 𝔑] show ?thesis by (rule iso_functorI)
qed


subsubsection‹Opposite functor isomorphism›

lemma (in iso_functor) iso_functor_op: "op_cf 𝔉 ≈⇩C⇩F⇘α⇙ op_cf 𝔊"
proof-
  from iso_functor_axioms obtain 𝔄 𝔅 𝔑 where "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by auto
  from is_iso_ntcf_op[OF this] have "op_cf 𝔊 ≈⇩C⇩F⇘α⇙ op_cf 𝔉" 
    by (auto simp: iso_functorI)
  then show "op_cf 𝔉 ≈⇩C⇩F⇘α⇙ op_cf 𝔊" by (rule iso_functor_sym)
qed

lemmas iso_functor_op[cat_op_intros] = iso_functor.iso_functor_op

text‹\newpage›

end