Theory CZH_SMC_NTSMCF

(* Copyright 2021 (C) Mihails Milehins *)

section‹Natural transformation of a semifunctor›
theory CZH_SMC_NTSMCF
  imports 
    CZH_SMC_Semifunctor
    CZH_DG_TDGHM
begin



subsection‹Background›

named_theorems ntsmcf_cs_simps
named_theorems ntsmcf_cs_intros

lemmas [smc_cs_simps] = dg_shared_cs_simps
lemmas [smc_cs_intros] = dg_shared_cs_intros


subsubsection‹Slicing›

definition ntsmcf_tdghm :: "V ⇒ V"
  where "ntsmcf_tdghm 𝔑 = 
    [
      𝔑⦇NTMap⦈, 
      smcf_dghm (𝔑⦇NTDom⦈),
      smcf_dghm (𝔑⦇NTCod⦈),
      smc_dg (𝔑⦇NTDGDom⦈),
      smc_dg (𝔑⦇NTDGCod⦈)
    ]⇩∘"


text‹Components.›

lemma ntsmcf_tdghm_components:
  shows [slicing_simps]: "ntsmcf_tdghm 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
    and [slicing_commute]: "ntsmcf_tdghm 𝔑⦇NTDom⦈ = smcf_dghm (𝔑⦇NTDom⦈)"
    and [slicing_commute]: "ntsmcf_tdghm 𝔑⦇NTCod⦈ = smcf_dghm (𝔑⦇NTCod⦈)"
    and [slicing_commute]: "ntsmcf_tdghm 𝔑⦇NTDGDom⦈ = smc_dg (𝔑⦇NTDGDom⦈)"
    and [slicing_commute]: "ntsmcf_tdghm 𝔑⦇NTDGCod⦈ = smc_dg (𝔑⦇NTDGCod⦈)"
  unfolding ntsmcf_tdghm_def nt_field_simps by (auto simp: nat_omega_simps)



subsection‹Definition and elementary properties›


text‹
A natural transformation of semifunctors, as presented in this work,
is a generalization of the concept of a natural transformation, as presented in
Chapter I-4 in \<^cite>‹"mac_lane_categories_2010"›, to semicategories and
semifunctors.
›

locale is_ntsmcf = 
  𝒵 α + 
  vfsequence 𝔑 + 
  NTDom: is_semifunctor α 𝔄 𝔅 𝔉 + 
  NTCod: is_semifunctor α 𝔄 𝔅 𝔊
  for α 𝔄 𝔅 𝔉 𝔊 𝔑 +
  assumes ntsmcf_length[smc_cs_simps]: "vcard 𝔑 = 5⇩ℕ"  
    and ntsmcf_is_tdghm[slicing_intros]: "ntsmcf_tdghm 𝔑 :
      smcf_dghm 𝔉 ↦⇩D⇩G⇩H⇩M smcf_dghm 𝔊 : smc_dg 𝔄 ↦↦⇩D⇩G⇘α⇙ smc_dg 𝔅"
    and ntsmcf_NTDom[smc_cs_simps]: "𝔑⦇NTDom⦈ = 𝔉"
    and ntsmcf_NTCod[smc_cs_simps]: "𝔑⦇NTCod⦈ = 𝔊"
    and ntsmcf_NTDGDom[smc_cs_simps]: "𝔑⦇NTDGDom⦈ = 𝔄"
    and ntsmcf_NTDGCod[smc_cs_simps]: "𝔑⦇NTDGCod⦈ = 𝔅"
    and ntsmcf_Comp_commute[smc_cs_intros]: "f : a ↦⇘𝔄⇙ b ⟹
      𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈" 

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

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

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

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

lemmas [smc_cs_simps] =
  is_ntsmcf.ntsmcf_length
  is_ntsmcf.ntsmcf_NTDom
  is_ntsmcf.ntsmcf_NTCod
  is_ntsmcf.ntsmcf_NTDGDom
  is_ntsmcf.ntsmcf_NTDGCod
  is_ntsmcf.ntsmcf_Comp_commute

lemmas [smc_cs_intros] = is_ntsmcf.ntsmcf_Comp_commute

lemma (in is_ntsmcf) ntsmcf_is_tdghm':
  assumes "𝔉' = smcf_dghm 𝔉"
    and "𝔊' = smcf_dghm 𝔊"
    and "𝔄' = smc_dg 𝔄"
    and "𝔅' = smc_dg 𝔅"
  shows "ntsmcf_tdghm 𝔑 : 𝔉' ↦⇩D⇩G⇩H⇩M 𝔊' : 𝔄' ↦↦⇩D⇩G⇘α⇙ 𝔅'"
  unfolding assms(1-4) by (rule ntsmcf_is_tdghm)

lemmas [slicing_intros] = is_ntsmcf.ntsmcf_is_tdghm'


text‹Rules.›

lemma (in is_ntsmcf) is_ntsmcf_axioms'[smc_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅" and "𝔉' = 𝔉" and "𝔊' = 𝔊"
  shows "𝔑 : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔄' ↦↦⇩S⇩M⇩C⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_ntsmcf_axioms)

mk_ide rf is_ntsmcf_def[unfolded is_ntsmcf_axioms_def]
  |intro is_ntsmcfI|
  |dest is_ntsmcfD[dest]|
  |elim is_ntsmcfE[elim]|

lemmas [smc_cs_intros] = 
  is_ntsmcfD(3,4)

lemma is_ntsmcfI':
  assumes "𝒵 α"
    and "vfsequence 𝔑"
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "vcard 𝔑 = 5⇩ℕ"
    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 "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  by (intro is_ntsmcfI is_tdghmI, unfold ntsmcf_tdghm_components slicing_simps)
    (
      simp_all add: 
        assms nat_omega_simps 
        ntsmcf_tdghm_def  
        is_semifunctorD(6)[OF assms(3)] 
        is_semifunctorD(6)[OF assms(4)]
    )

lemma is_ntsmcfD':
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝒵 α"
    and "vfsequence 𝔑"
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "vcard 𝔑 = 5⇩ℕ"
    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_ntsmcfD(2-11)[OF assms] 
        is_tdghmD[OF is_ntsmcfD(6)[OF assms], unfolded slicing_simps]
    )

lemma is_ntsmcfE':
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  obtains "𝒵 α"
    and "vfsequence 𝔑"
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "vcard 𝔑 = 5⇩ℕ"
    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_ntsmcfD')


text‹Slicing.›

context is_ntsmcf
begin

interpretation tdghm: is_tdghm 
  α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉› ‹smcf_dghm 𝔊› ‹ntsmcf_tdghm 𝔑›
  by (rule ntsmcf_is_tdghm)

lemmas_with [unfolded slicing_simps]:
  ntsmcf_NTMap_vsv = tdghm.tdghm_NTMap_vsv
  and ntsmcf_NTMap_vdomain[smc_cs_simps] = tdghm.tdghm_NTMap_vdomain
  and ntsmcf_NTMap_is_arr = tdghm.tdghm_NTMap_is_arr
  and ntsmcf_NTMap_is_arr'[smc_cs_intros]  = tdghm.tdghm_NTMap_is_arr'

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

lemmas_with [unfolded slicing_simps]:
  ntsmcf_NTMap_app_in_Arr[smc_cs_intros] = tdghm.tdghm_NTMap_app_in_Arr
  and ntsmcf_NTMap_vrange_vifunion = tdghm.tdghm_NTMap_vrange_vifunion
  and ntsmcf_NTMap_vrange = tdghm.tdghm_NTMap_vrange
  and ntsmcf_NTMap_vsubset_Vset = tdghm.tdghm_NTMap_vsubset_Vset
  and ntsmcf_NTMap_in_Vset = tdghm.tdghm_NTMap_in_Vset
  and ntsmcf_is_tdghm_if_ge_Limit = tdghm.tdghm_is_tdghm_if_ge_Limit

end

lemmas [smc_cs_intros] = is_ntsmcf.ntsmcf_NTMap_is_arr'

lemma (in is_ntsmcf) ntsmcf_Comp_commute':
  assumes "f : a ↦⇘𝔄⇙ b" and "g : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
  shows 
    "𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ (𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ g) =
      (𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈) ∘⇩A⇘𝔅⇙ g"
  using assms
  by 
    (
      cs_concl cs_shallow
        cs_simp: ntsmcf_Comp_commute semicategory.smc_Comp_assoc[symmetric] 
        cs_intro: smc_cs_intros
    )

lemma (in is_ntsmcf) ntsmcf_Comp_commute'':
  assumes "f : a ↦⇘𝔄⇙ b" and "g : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
  shows 
    "𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ (𝔑⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ g) =
      (𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈) ∘⇩A⇘𝔅⇙ g"
  using assms
  by 
    (
      cs_concl  
        cs_simp: ntsmcf_Comp_commute semicategory.smc_Comp_assoc[symmetric] 
        cs_intro: smc_cs_intros
    )


text‹Elementary properties.›

lemma ntsmcf_eqI:
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔑' : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
    and "𝔑⦇NTMap⦈ = 𝔑'⦇NTMap⦈"
    and "𝔉 = 𝔉'"
    and "𝔊 = 𝔊'"
    and "𝔄 = 𝔄'"
    and "𝔅 = 𝔅'"
  shows "𝔑 = 𝔑'"
proof-
  interpret L: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret R: is_ntsmcf α 𝔄' 𝔅' 𝔉' 𝔊' 𝔑' by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom: "𝒟⇩∘ 𝔑 = 5⇩ℕ" 
      by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
    show "𝒟⇩∘ 𝔑 = 𝒟⇩∘ 𝔑'" 
      by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
    from assms(4-7) have sup: 
      "𝔑⦇NTDom⦈ = 𝔑'⦇NTDom⦈" "𝔑⦇NTCod⦈ = 𝔑'⦇NTCod⦈" 
      "𝔑⦇NTDGDom⦈ = 𝔑'⦇NTDGDom⦈" "𝔑⦇NTDGCod⦈ = 𝔑'⦇NTDGCod⦈" 
      by (simp_all add: smc_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 ntsmcf_tdghm_eqI:
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔑' : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
    and "𝔉 = 𝔉'"
    and "𝔊 = 𝔊'"
    and "𝔄 = 𝔄'"
    and "𝔅 = 𝔅'"
    and "ntsmcf_tdghm 𝔑 = ntsmcf_tdghm 𝔑'"
  shows "𝔑 = 𝔑'"
proof(rule ntsmcf_eqI[of α])
  from assms(7) have "ntsmcf_tdghm 𝔑⦇NTMap⦈ = ntsmcf_tdghm 𝔑'⦇NTMap⦈" by simp
  then show "𝔑⦇NTMap⦈ = 𝔑'⦇NTMap⦈" unfolding slicing_simps by simp_all
  from assms(3-6) show "𝔉 = 𝔉'" "𝔊 = 𝔊'" "𝔄 = 𝔄'" "𝔅 = 𝔅'" by simp_all
qed (simp_all add: assms(1,2))

lemma (in is_ntsmcf) ntsmcf_def:
  "𝔑 = [𝔑⦇NTMap⦈, 𝔑⦇NTDom⦈, 𝔑⦇NTCod⦈, 𝔑⦇NTDGDom⦈, 𝔑⦇NTDGCod⦈]⇩∘"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ 𝔑 = 5⇩ℕ" 
    by (cs_concl cs_shallow cs_simp: smc_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)


text‹Size.›

lemma (in is_ntsmcf) ntsmcf_in_Vset: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔑 ∈⇩∘ Vset β"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  note [smc_cs_intros] = 
    ntsmcf_NTMap_in_Vset
    NTDom.smcf_in_Vset
    NTCod.smcf_in_Vset
    NTDom.HomDom.smc_in_Vset
    NTDom.HomCod.smc_in_Vset
  from assms(2) show ?thesis
    by (subst ntsmcf_def) 
      (
        cs_concl cs_shallow 
          cs_simp: smc_cs_simps cs_intro: smc_cs_intros V_cs_intros
      )
qed

lemma (in is_ntsmcf) ntsmcf_is_ntsmcf_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘β⇙ 𝔅"
proof(intro is_ntsmcfI )
  show "ntsmcf_tdghm 𝔑 :
    smcf_dghm 𝔉 ↦⇩D⇩G⇩H⇩M smcf_dghm 𝔊 : smc_dg 𝔄 ↦↦⇩D⇩G⇘β⇙ smc_dg 𝔅"
    by (rule is_tdghm.tdghm_is_tdghm_if_ge_Limit[OF ntsmcf_is_tdghm assms])
  show "𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈"
    if "f : a ↦⇘𝔄⇙ b" for f a b
    by 
      (
        use that in 
          ‹cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros›
      )+
qed 
  (
    cs_concl cs_shallow
      cs_simp: smc_cs_simps 
      cs_intro:
        smc_cs_intros
        V_cs_intros
        assms 
        NTDom.smcf_is_semifunctor_if_ge_Limit
        NTCod.smcf_is_semifunctor_if_ge_Limit
   )+

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

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

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


text‹Further elementary results.›

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



subsection‹Opposite natural transformation of semifunctors›


subsubsection‹Definition and elementary properties›


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

definition op_ntsmcf :: "V ⇒ V"
  where "op_ntsmcf 𝔑 =
    [
      𝔑⦇NTMap⦈,
      op_smcf (𝔑⦇NTCod⦈),
      op_smcf (𝔑⦇NTDom⦈),
      op_smc (𝔑⦇NTDGDom⦈),
      op_smc (𝔑⦇NTDGCod⦈)
    ]⇩∘"


text‹Components.›

lemma op_ntsmcf_components[smc_op_simps]:
  shows "op_ntsmcf 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
    and "op_ntsmcf 𝔑⦇NTDom⦈ = op_smcf (𝔑⦇NTCod⦈)"
    and "op_ntsmcf 𝔑⦇NTCod⦈ = op_smcf (𝔑⦇NTDom⦈)"
    and "op_ntsmcf 𝔑⦇NTDGDom⦈ = op_smc (𝔑⦇NTDGDom⦈)"
    and "op_ntsmcf 𝔑⦇NTDGCod⦈ = op_smc (𝔑⦇NTDGCod⦈)"
  unfolding op_ntsmcf_def nt_field_simps by (auto simp: nat_omega_simps)


text‹Slicing.›

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


subsubsection‹Further properties›

lemma (in is_ntsmcf) is_ntsmcf_op: 
  "op_ntsmcf 𝔑 : op_smcf 𝔊 ↦⇩S⇩M⇩C⇩F op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ op_smc 𝔅"
proof(rule is_ntsmcfI, unfold smc_op_simps)
  show "vfsequence (op_ntsmcf 𝔑)" by (simp add: op_ntsmcf_def)
  show "vcard (op_ntsmcf 𝔑) = 5⇩ℕ" by (simp add: op_ntsmcf_def nat_omega_simps)
  fix f a b assume "f : b ↦⇘𝔄⇙ a"
  with is_ntsmcf_axioms show 
    "𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘op_smc 𝔅⇙ 𝔊⦇ArrMap⦈⦇f⦈ =
      𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘op_smc 𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈"
    by (cs_concl cs_simp: smc_cs_simps smc_op_simps cs_intro: smc_cs_intros)
qed
  (
    insert is_ntsmcf_axioms,
    (
      cs_concl cs_shallow 
        cs_simp: smc_cs_simps slicing_commute[symmetric]
        cs_intro: smc_cs_intros smc_op_intros dg_op_intros slicing_intros
    )+
  )

lemma (in is_ntsmcf) is_ntsmcf_op'[smc_op_intros]: 
  assumes "𝔊' = op_smcf 𝔊"
    and "𝔉' = op_smcf 𝔉"
    and "𝔄' = op_smc 𝔄"
    and "𝔅' = op_smc 𝔅"
  shows "op_ntsmcf 𝔑 : 𝔊' ↦⇩S⇩M⇩C⇩F 𝔉' : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
  unfolding assms by (rule is_ntsmcf_op)

lemmas [smc_op_intros] = is_ntsmcf.is_ntsmcf_op'

lemma (in is_ntsmcf) ntsmcf_op_ntsmcf_op_ntsmcf[smc_op_simps]: 
  "op_ntsmcf (op_ntsmcf 𝔑) = 𝔑"
proof(rule ntsmcf_eqI[of α 𝔄 𝔅 𝔉 𝔊 _ 𝔄 𝔅 𝔉 𝔊], unfold smc_op_simps)
  interpret op: 
    is_ntsmcf α ‹op_smc 𝔄› ‹op_smc 𝔅› ‹op_smcf 𝔊› ‹op_smcf 𝔉› ‹op_ntsmcf 𝔑›
    by (rule is_ntsmcf_op)
  from op.is_ntsmcf_op show 
    "op_ntsmcf (op_ntsmcf 𝔑) : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    by (simp add: smc_op_simps)
qed (auto simp: smc_cs_intros)

lemmas ntsmcf_op_ntsmcf_op_ntsmcf[smc_op_simps] =
  is_ntsmcf.ntsmcf_op_ntsmcf_op_ntsmcf

lemma eq_op_ntsmcf_iff: 
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔑' : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
  shows "op_ntsmcf 𝔑 = op_ntsmcf 𝔑' ⟷ 𝔑 = 𝔑'"
proof
  interpret L: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret R: is_ntsmcf α 𝔄' 𝔅' 𝔉' 𝔊' 𝔑' by (rule assms(2))
  assume prems: "op_ntsmcf 𝔑 = op_ntsmcf 𝔑'"
  show "𝔑 = 𝔑'"
  proof(rule ntsmcf_eqI[OF assms])
    from prems L.ntsmcf_op_ntsmcf_op_ntsmcf R.ntsmcf_op_ntsmcf_op_ntsmcf show 
      "𝔑⦇NTMap⦈ = 𝔑'⦇NTMap⦈"
      by metis+
    from prems L.ntsmcf_op_ntsmcf_op_ntsmcf R.ntsmcf_op_ntsmcf_op_ntsmcf 
    have "𝔑⦇NTDom⦈ = 𝔑'⦇NTDom⦈" 
      and "𝔑⦇NTCod⦈ = 𝔑'⦇NTCod⦈" 
      and "𝔑⦇NTDGDom⦈ = 𝔑'⦇NTDGDom⦈" 
      and "𝔑⦇NTDGCod⦈ = 𝔑'⦇NTDGCod⦈" 
      by metis+
    then show "𝔉 = 𝔉'" "𝔊 = 𝔊'" "𝔄 = 𝔄'" "𝔅 = 𝔅'" by (auto simp: smc_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"›.›

definition ntsmcf_vcomp :: "V ⇒ V ⇒ V" (infixl ‹∙⇩N⇩T⇩S⇩M⇩C⇩F› 55)
  where "ntsmcf_vcomp 𝔐 𝔑 = 
    [
      (λa∈⇩∘𝔑⦇NTDGDom⦈⦇Obj⦈. (𝔐⦇NTMap⦈⦇a⦈) ∘⇩A⇘𝔑⦇NTDGCod⦈⇙ (𝔑⦇NTMap⦈⦇a⦈)),
      𝔑⦇NTDom⦈,
      𝔐⦇NTCod⦈,
      𝔑⦇NTDGDom⦈,
      𝔐⦇NTDGCod⦈
    ]⇩∘"


text‹Components.›

lemma ntsmcf_vcomp_components:
  shows
    "(𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈ =
      (λa∈⇩∘𝔑⦇NTDGDom⦈⦇Obj⦈. (𝔐⦇NTMap⦈⦇a⦈) ∘⇩A⇘𝔑⦇NTDGCod⦈⇙ (𝔑⦇NTMap⦈⦇a⦈))"
    and [dg_shared_cs_simps, smc_cs_simps]: "(𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTDom⦈ = 𝔑⦇NTDom⦈" 
    and [dg_shared_cs_simps, smc_cs_simps]: "(𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTCod⦈ = 𝔐⦇NTCod⦈"
    and [dg_shared_cs_simps, smc_cs_simps]: 
      "(𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTDGDom⦈ = 𝔑⦇NTDGDom⦈"
    and [dg_shared_cs_simps, smc_cs_simps]: 
      "(𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTDGCod⦈ = 𝔐⦇NTDGCod⦈"
  unfolding nt_field_simps ntsmcf_vcomp_def by (simp_all add: nat_omega_simps)


subsubsection‹Natural transformation map›

lemma ntsmcf_vcomp_NTMap_vsv[dg_shared_cs_intros, smc_cs_intros]: 
  "vsv ((𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈)"
  unfolding ntsmcf_vcomp_components by simp

lemma ntsmcf_vcomp_NTMap_vdomain[smc_cs_simps]:
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝒟⇩∘ ((𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈) = 𝔄⦇Obj⦈"
proof-
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 using assms by auto
  show ?thesis unfolding ntsmcf_vcomp_components by (simp add: smc_cs_simps)
qed

lemma ntsmcf_vcomp_NTMap_app[smc_cs_simps]:
  assumes "𝔐 : 𝔊 ↦⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "a ∈⇩∘ 𝔄⦇Obj⦈" 
  shows "(𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ = 𝔐⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈"
proof-
  interpret 𝔐: is_ntsmcf α 𝔄 𝔅 𝔊 ℌ 𝔐 using assms by auto
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 using assms by auto
  from assms show ?thesis 
    unfolding ntsmcf_vcomp_components by (simp add: smc_cs_simps)
qed

lemma ntsmcf_vcomp_NTMap_vrange:
  assumes "𝔐 : 𝔊 ↦⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈) ⊆⇩∘ 𝔅⦇Arr⦈"
  unfolding ntsmcf_vcomp_components
proof(rule vrange_VLambda_vsubset)
  fix x assume prems: "x ∈⇩∘ 𝔑⦇NTDGDom⦈⦇Obj⦈"
  from prems assms show "𝔐⦇NTMap⦈⦇x⦈ ∘⇩A⇘𝔑⦇NTDGCod⦈⇙ 𝔑⦇NTMap⦈⦇x⦈ ∈⇩∘ 𝔅⦇Arr⦈"
    by (cs_prems cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
      (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
qed


subsubsection‹Further properties›

lemma ntsmcf_vcomp_composable_commute[smc_cs_simps]:
  ―‹See Chapter II-4 in \cite{mac_lane_categories_2010}).›
  assumes "𝔐 : 𝔊 ↦⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "f : a ↦⇘𝔄⇙ b"
  shows 
    "(𝔐⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇b⦈) ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 
      ℌ⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ (𝔐⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔅⇙ 𝔑⦇NTMap⦈⦇a⦈)"
    (is ‹(?MC ∘⇩A⇘𝔅⇙ ?NC) ∘⇩A⇘𝔅⇙ ?R = ?T ∘⇩A⇘𝔅⇙ (?MD ∘⇩A⇘𝔅⇙ ?ND)›)
proof-
  interpret 𝔐: is_ntsmcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(1)) 
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  from assms show ?thesis
    by (intro 𝔐.NTDom.HomCod.smc_pattern_rectangle_left)
      (cs_concl cs_intro: smc_cs_intros cs_simp: 𝔑.ntsmcf_Comp_commute)
qed 

lemma ntsmcf_vcomp_is_ntsmcf[smc_cs_intros]:
  ―‹See Chapter II-4 in \cite{mac_lane_categories_2010}.›
  assumes "𝔐 : 𝔊 ↦⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
proof-
  interpret 𝔐: is_ntsmcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis 
  proof(intro is_ntsmcfI')
    show "vfsequence (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)" by (simp add: ntsmcf_vcomp_def)
    show "vcard (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) = 5⇩ℕ"
      by (auto simp: nat_omega_simps ntsmcf_vcomp_def)
    show "vsv ((𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈)"
      unfolding ntsmcf_vcomp_components by simp
    from assms show "(𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ ℌ⦇ObjMap⦈⦇a⦈"
      if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
      by 
        (
          use that in 
            ‹cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros›
        )
    fix f a b assume "f : a ↦⇘𝔄⇙ b"
    with assms show 
      "(𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ =
        ℌ⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈"
      by 
        (
          cs_concl  
            cs_simp: smc_cs_simps is_ntsmcf.ntsmcf_Comp_commute' 
            cs_intro: smc_cs_intros
        )
  qed (use assms in ‹auto simp: smc_cs_simps ntsmcf_vcomp_NTMap_vrange›)
qed

lemma ntsmcf_vcomp_assoc[smc_cs_simps]: 
  ―‹See Chapter II-4 in \cite{mac_lane_categories_2010}.›
  assumes "𝔏 : ℌ ↦⇩S⇩M⇩C⇩F 𝔎 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔐 : 𝔊 ↦⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "(𝔏 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔐) ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 = 𝔏 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)"
proof-
  interpret 𝔏: is_ntsmcf α 𝔄 𝔅 ℌ 𝔎 𝔏 by (rule assms(1))
  interpret 𝔐: is_ntsmcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(2))
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(3))
  show ?thesis
  proof(rule ntsmcf_eqI[of α])
    show "((𝔏 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔐) ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈ = (𝔏 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈"
    proof(rule vsv_eqI)
      fix a assume "a ∈⇩∘ 𝒟⇩∘ ((𝔏 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈)"
      then have "a ∈⇩∘ 𝔄⦇Obj⦈" 
        unfolding ntsmcf_vcomp_components by (simp add: smc_cs_simps)
      with assms show 
        "((𝔏 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔐) ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ =
          (𝔏 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈⦇a⦈"
        by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
    qed (simp_all add: ntsmcf_vcomp_components)
  qed (auto intro: smc_cs_intros)
qed


subsubsection‹
Opposite of the vertical composition of natural transformations
of semifunctors
›

lemma op_ntsmcf_ntsmcf_vcomp[smc_op_simps]: 
  assumes "𝔐 : 𝔊 ↦⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "op_ntsmcf (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) = op_ntsmcf 𝔑 ∙⇩N⇩T⇩S⇩M⇩C⇩F op_ntsmcf 𝔐"
proof-
  interpret 𝔐: is_ntsmcf α 𝔄 𝔅 𝔊 ℌ 𝔐 using assms(1) by auto
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 using assms(2) by auto
  show ?thesis
  proof(rule ntsmcf_eqI[of α]; (intro symmetric)?)
    show "op_ntsmcf (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈ = 
      (op_ntsmcf 𝔑 ∙⇩N⇩T⇩S⇩M⇩C⇩F op_ntsmcf 𝔐)⦇NTMap⦈"
    proof(rule vsv_eqI)
      fix a assume "a ∈⇩∘ 𝒟⇩∘ (op_ntsmcf (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈)"
      then have a: "a ∈⇩∘ 𝔄⦇Obj⦈"
        unfolding smc_op_simps ntsmcf_vcomp_NTMap_vdomain[OF assms(2)] by simp
      with 
        𝔐.NTDom.HomCod.op_smc_Comp 
        𝔐.ntsmcf_NTMap_is_arr[OF a]
        𝔑.ntsmcf_NTMap_is_arr[OF a] 
      show "op_ntsmcf (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ =
        (op_ntsmcf 𝔑 ∙⇩N⇩T⇩S⇩M⇩C⇩F op_ntsmcf 𝔐)⦇NTMap⦈⦇a⦈"
        unfolding smc_op_simps ntsmcf_vcomp_components 
        by (simp add: smc_cs_simps)
    qed (simp_all add: smc_op_simps smc_cs_simps ntsmcf_vcomp_components(1))
  qed (auto intro: smc_cs_intros smc_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"›.›

definition ntsmcf_hcomp :: "V ⇒ V ⇒ V" (infixl ‹∘⇩N⇩T⇩S⇩M⇩C⇩F› 55)
  where "ntsmcf_hcomp 𝔐 𝔑 =
    [
      (
        λa∈⇩∘𝔑⦇NTDGDom⦈⦇Obj⦈.
          (
            𝔐⦇NTCod⦈⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇a⦈⦈ ∘⇩A⇘𝔐⦇NTDGCod⦈⇙ 
            𝔐⦇NTMap⦈⦇𝔑⦇NTDom⦈⦇ObjMap⦈⦇a⦈⦈
          )
      ),
      (𝔐⦇NTDom⦈ ∘⇩S⇩M⇩C⇩F 𝔑⦇NTDom⦈),
      (𝔐⦇NTCod⦈ ∘⇩S⇩M⇩C⇩F 𝔑⦇NTCod⦈),
      (𝔑⦇NTDGDom⦈),
      (𝔐⦇NTDGCod⦈)
    ]⇩∘"


text‹Components.›                                            

lemma ntsmcf_hcomp_components:
  shows 
    "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈ = 
      (
        λa∈⇩∘𝔑⦇NTDGDom⦈⦇Obj⦈.
          (
            𝔐⦇NTCod⦈⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇a⦈⦈ ∘⇩A⇘𝔐⦇NTDGCod⦈⇙ 
            𝔐⦇NTMap⦈⦇𝔑⦇NTDom⦈⦇ObjMap⦈⦇a⦈⦈
          )
      )"
    and [dg_shared_cs_simps, smc_cs_simps]:
      "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTDom⦈ = 𝔐⦇NTDom⦈ ∘⇩S⇩M⇩C⇩F 𝔑⦇NTDom⦈" 
    and [dg_shared_cs_simps, smc_cs_simps]:
      "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTCod⦈ = 𝔐⦇NTCod⦈ ∘⇩S⇩M⇩C⇩F 𝔑⦇NTCod⦈"
    and [dg_shared_cs_simps, smc_cs_simps]: 
      "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTDGDom⦈ = 𝔑⦇NTDGDom⦈"
    and [dg_shared_cs_simps, smc_cs_simps]:
      "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTDGCod⦈ = 𝔐⦇NTDGCod⦈"
  unfolding nt_field_simps ntsmcf_hcomp_def by (auto simp: nat_omega_simps)


subsubsection‹Natural transformation map›

lemma ntsmcf_hcomp_NTMap_vsv[smc_cs_intros]: "vsv ((𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈)"
  unfolding ntsmcf_hcomp_components by auto

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

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

lemma ntsmcf_hcomp_NTMap_vrange:
  assumes "𝔐 : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" 
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof
  interpret 𝔐: is_ntsmcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  fix f assume "f ∈⇩∘ ℛ⇩∘ ((𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈)"
  with ntsmcf_hcomp_NTMap_vdomain obtain a 
    where a: "a ∈⇩∘ 𝔄⦇Obj⦈" and f_def: "f = (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈"
    unfolding ntsmcf_hcomp_components by (force simp: smc_cs_simps)
  have 𝔉a: "𝔉⦇ObjMap⦈⦇a⦈ ∈⇩∘ 𝔅⦇Obj⦈" 
    by (simp add: 𝔑.NTDom.smcf_ObjMap_app_in_HomCod_Obj a)
  from 𝔑.ntsmcf_NTMap_is_arr[OF a] have "𝔊'⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇a⦈⦈ :
    𝔊'⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈ ↦⇘ℭ⇙ 𝔊'⦇ObjMap⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈"
    by (force intro: smc_cs_intros)
  then have "𝔊'⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇a⦈⦈ ∘⇩A⇘ℭ⇙ 𝔐⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈ ∈⇩∘ ℭ⦇Arr⦈"
    by 
      (
        meson 
          𝔐.ntsmcf_NTMap_is_arr[OF 𝔉a] 
          𝔐.NTDom.HomCod.smc_is_arrE 
          𝔐.NTDom.HomCod.smc_Comp_is_arr
      )
  with a show "f ∈⇩∘ ℭ⦇Arr⦈" 
    unfolding f_def ntsmcf_hcomp_components by (simp add: smc_cs_simps)
qed


subsubsection‹Further properties›

lemma ntsmcf_hcomp_composable_commute:
  ―‹See Chapter II-5 in \cite{mac_lane_categories_2010}.›
  assumes "𝔐 : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "f : a ↦⇘𝔄⇙ b" 
  shows 
    "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ (𝔉' ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ = 
      (𝔊' ∘⇩S⇩M⇩C⇩F 𝔊)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈"
proof-
  interpret 𝔐: is_ntsmcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  from assms(3) have [simp]: "b ∈⇩∘ 𝔄⦇Obj⦈" and a: "a ∈⇩∘ 𝔄⦇Obj⦈" by auto
  from 𝔐.is_ntsmcf_axioms 𝔑.is_ntsmcf_axioms have 𝔐𝔑b: 
    "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇b⦈ =
      (𝔊'⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇b⦈⦈) ∘⇩A⇘ℭ⇙ (𝔐⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇b⦈⦈)"
    by (auto simp: smc_cs_simps)
  let ?𝔊'𝔉f = ‹𝔊'⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈›
  from a 𝔐.is_ntsmcf_axioms 𝔑.is_ntsmcf_axioms have 𝔐𝔑a: 
    "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ =
      𝔊'⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇a⦈⦈ ∘⇩A⇘ℭ⇙ 𝔐⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
    by (cs_concl cs_shallow cs_simp: smc_cs_simps)+
  note 𝔐.NTCod.smcf_ArrMap_Comp[smc_cs_simps del]
  from assms show ?thesis
    unfolding 𝔐𝔑b 𝔐𝔑a 
    by (intro 𝔐.NTDom.HomCod.smc_pattern_rectangle_left)
      (
        cs_concl  
          cs_simp: smc_cs_simps is_semifunctor.smcf_ArrMap_Comp[symmetric] 
          cs_intro: smc_cs_intros
      )+
qed

lemma ntsmcf_hcomp_is_ntsmcf:
  ―‹See Chapter II-5 in \cite{mac_lane_categories_2010}.›
  assumes "𝔐 : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" 
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 : 𝔉' ∘⇩S⇩M⇩C⇩F 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊' ∘⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔐: is_ntsmcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis
  proof(intro is_ntsmcfI', unfold ntsmcf_hcomp_components(3,4)) 
    show "vfsequence (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)" unfolding ntsmcf_hcomp_def by auto
    show "vcard (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) = 5⇩ℕ"
      unfolding ntsmcf_hcomp_def by (simp add: nat_omega_simps)
    from assms show "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ : 
      (𝔉' ∘⇩S⇩M⇩C⇩F 𝔉)⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ (𝔊' ∘⇩S⇩M⇩C⇩F 𝔊)⦇ObjMap⦈⦇a⦈"
      if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
      by 
        (
          use that in 
            ‹cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros›
        )
    fix f a b assume "f : a ↦⇘𝔄⇙ b"
    with ntsmcf_hcomp_composable_commute[OF assms] 
    show "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ (𝔉' ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ = 
      (𝔊' ∘⇩S⇩M⇩C⇩F 𝔊)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈"
      by auto
  qed (auto simp: ntsmcf_hcomp_components(1) smc_cs_simps intro: smc_cs_intros)
qed

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

lemma ntsmcf_hcomp_assoc[smc_cs_simps]: 
  ―‹See Chapter II-5 in \cite{mac_lane_categories_2010}.›
  assumes "𝔏 : 𝔉'' ↦⇩S⇩M⇩C⇩F 𝔊'' : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇" 
    and "𝔐 : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "(𝔏 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔐) ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 = 𝔏 ∘⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)"
proof-
  interpret 𝔏: is_ntsmcf α ℭ 𝔇 𝔉'' 𝔊'' 𝔏 by (rule assms(1))
  interpret 𝔐: is_ntsmcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐  by (rule assms(2))
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(3))
  interpret 𝔏𝔐: is_ntsmcf α 𝔅 𝔇 ‹𝔉'' ∘⇩S⇩M⇩C⇩F 𝔉'› ‹𝔊'' ∘⇩S⇩M⇩C⇩F 𝔊'› ‹𝔏 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔐› 
    by (auto intro: smc_cs_intros)
  interpret 𝔐𝔑: is_ntsmcf α 𝔄 ℭ ‹𝔉' ∘⇩S⇩M⇩C⇩F 𝔉› ‹𝔊' ∘⇩S⇩M⇩C⇩F 𝔊› ‹𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑› 
    by (auto intro: smc_cs_intros)
  note smcf_axioms =
    𝔏.NTDom.is_semifunctor_axioms 
    𝔏.NTCod.is_semifunctor_axioms 
    𝔐.NTDom.is_semifunctor_axioms 
    𝔐.NTCod.is_semifunctor_axioms 
    𝔑.NTDom.is_semifunctor_axioms 
    𝔑.NTCod.is_semifunctor_axioms 
  show ?thesis
  proof(rule ntsmcf_eqI)
    from assms show 
      "𝔏 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 :
        (𝔉'' ∘⇩S⇩M⇩C⇩F 𝔉') ∘⇩S⇩M⇩C⇩F 𝔉 ↦⇩S⇩M⇩C⇩F (𝔊'' ∘⇩S⇩M⇩C⇩F 𝔊') ∘⇩S⇩M⇩C⇩F 𝔊 :
        𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
      by (auto intro: smc_cs_intros)
    from 𝔏𝔐.is_ntsmcf_axioms 𝔑.is_ntsmcf_axioms have dom_lhs:
      "𝒟⇩∘ ((𝔏 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (simp add: smc_cs_simps)
    from 𝔐𝔑.is_ntsmcf_axioms 𝔏.is_ntsmcf_axioms have dom_rhs:  
      "𝒟⇩∘ ((𝔏 ∘⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (simp add: smc_cs_simps)
    show "(𝔏 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈ = (𝔏 ∘⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
      with assms show
        "(𝔏 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈ =
          (𝔏 ∘⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈⦇a⦈"
        by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
    qed (simp_all add: ntsmcf_hcomp_components)
  qed 
    (
      insert smcf_axioms, 
      auto simp: smcf_comp_assoc intro!: smc_cs_intros
    )
qed


subsubsection‹Opposite of the horizontal composition of the 
natural transformation of semifunctors›

lemma op_ntsmcf_ntsmcf_hcomp[smc_op_simps]: 
  assumes "𝔐 : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "op_ntsmcf (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) = op_ntsmcf 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F op_ntsmcf 𝔑"
proof-
  interpret 𝔐: is_ntsmcf α 𝔅 ℭ 𝔉' 𝔊' 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  have op_𝔐: "op_ntsmcf 𝔐 :
    op_smcf 𝔊' ↦⇩S⇩M⇩C⇩F op_smcf 𝔉' : op_smc 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ op_smc ℭ"
    and op_𝔑: "op_ntsmcf 𝔑 :
    op_smcf 𝔊 ↦⇩S⇩M⇩C⇩F op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ op_smc 𝔅" 
    by 
      (
        cs_concl cs_shallow 
          cs_simp: smc_op_simps cs_intro: smc_cs_intros smc_op_intros
      )
  show ?thesis
  proof(rule sym, rule ntsmcf_eqI, unfold smc_op_simps slicing_simps)
    show 
      "op_ntsmcf 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F op_ntsmcf 𝔑 :
        op_smcf 𝔊' ∘⇩S⇩M⇩C⇩F op_smcf 𝔊 ↦⇩S⇩M⇩C⇩F op_smcf 𝔉' ∘⇩S⇩M⇩C⇩F op_smcf 𝔉 :
        op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ op_smc ℭ"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: smc_op_simps cs_intro: smc_cs_intros smc_op_intros
        )
    show "op_ntsmcf (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) :
      op_smcf 𝔊' ∘⇩S⇩M⇩C⇩F op_smcf 𝔊 ↦⇩S⇩M⇩C⇩F op_smcf 𝔉' ∘⇩S⇩M⇩C⇩F op_smcf 𝔉 :
      op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ op_smc ℭ"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: smc_op_simps cs_intro: smc_cs_intros smc_op_intros
        )
    show "(op_ntsmcf 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F op_ntsmcf 𝔑)⦇NTMap⦈ = (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈"
    proof
      (
        rule vsv_eqI, 
        unfold 
          ntsmcf_hcomp_NTMap_vdomain[OF assms(2)]
          ntsmcf_hcomp_NTMap_vdomain[OF op_𝔑]
          smc_op_simps
      )
      fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
      with assms show 
        "(op_ntsmcf 𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F op_ntsmcf 𝔑)⦇NTMap⦈⦇a⦈ = (𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈"
        by 
          (
            cs_concl cs_shallow
              cs_simp: smc_cs_simps smc_op_simps 
              cs_intro: smc_cs_intros smc_op_intros
          )
    qed (auto simp: ntsmcf_hcomp_components)
  qed simp_all
qed 



subsection‹Interchange law›

lemma ntsmcf_comp_interchange_law:
  ―‹See Chapter II-5 in \cite{mac_lane_categories_2010}.›
  assumes "𝔐 : 𝔊 ↦⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔐' : 𝔊' ↦⇩S⇩M⇩C⇩F ℌ' : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    and "𝔑' : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
  shows 
    "((𝔐' ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑') ∘⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)) =
      (𝔐' ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔐) ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔑' ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)"
proof-
  interpret 𝔐: is_ntsmcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(1))
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  interpret 𝔐': is_ntsmcf α 𝔅 ℭ 𝔊' ℌ' 𝔐' by (rule assms(3))
  interpret 𝔑': is_ntsmcf α 𝔅 ℭ 𝔉' 𝔊' 𝔑' by (rule assms(4))
  interpret 𝔑'𝔑: 
    is_ntsmcf α 𝔄 ℭ ‹𝔉' ∘⇩S⇩M⇩C⇩F 𝔉› ‹𝔊' ∘⇩S⇩M⇩C⇩F 𝔊› ‹𝔑' ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑› 
    by (auto intro: smc_cs_intros)
  interpret 𝔐𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 ℌ ‹𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑› 
    by (auto intro: smc_cs_intros)
  show ?thesis
  proof(rule ntsmcf_eqI[of α])
    show 
      "(𝔐' ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑' ∘⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈ =
        (𝔐' ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔑' ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈"
    proof
      (
        rule vsv_eqI,
        unfold 
          ntsmcf_vcomp_NTMap_vdomain[OF 𝔑'𝔑.is_ntsmcf_axioms]
          ntsmcf_hcomp_NTMap_vdomain[OF 𝔐𝔑.is_ntsmcf_axioms]
      )
      fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
      with assms show
        "(𝔐' ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑' ∘⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈⦇a⦈ =
          ((𝔐' ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔐) ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔑' ∘⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈⦇a⦈"
        by
          (
            cs_concl 
              cs_simp: smc_cs_simps is_ntsmcf.ntsmcf_Comp_commute' 
              cs_intro: smc_cs_intros
          )
    qed (auto intro: smc_cs_intros)
  qed (auto intro: smc_cs_intros)
qed



subsection‹
Composition of a natural transformation of semifunctors and a semifunctor
›


subsubsection‹Definition and elementary properties›

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


text‹Slicing.›

lemma ntsmcf_tdghm_ntsmcf_smcf_comp[slicing_commute]: 
  "ntsmcf_tdghm 𝔑 ∘⇩T⇩D⇩G⇩H⇩M⇩-⇩D⇩G⇩H⇩M smcf_dghm ℌ = ntsmcf_tdghm (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F ℌ)"
  unfolding 
    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_semifunctor) 
  tdghm_dghm_comp_components(1)[where ℌ=𝔉, unfolded smcf_HomDom]
  |vdomain ntsmcf_smcf_comp_NTMap_vdomain[smc_cs_simps]|
  |app ntsmcf_smcf_comp_NTMap_app[smc_cs_simps]|

lemmas [smc_cs_simps] = 
  is_semifunctor.ntsmcf_smcf_comp_NTMap_vdomain
  is_semifunctor.ntsmcf_smcf_comp_NTMap_app

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


subsubsection‹
Opposite of the composition of a natural transformation of 
semifunctors and a semifunctor
›

lemma op_ntsmcf_ntsmcf_smcf_comp[smc_op_simps]: 
  "op_ntsmcf (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F ℌ) = op_ntsmcf 𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F op_smcf ℌ"
  unfolding 
    tdghm_dghm_comp_def 
    dghm_comp_def 
    op_ntsmcf_def 
    op_smcf_def 
    op_smc_def
    dg_field_simps
    dghm_field_simps
    nt_field_simps
  by (simp add: nat_omega_simps) (*slow*)


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

lemma ntsmcf_smcf_comp_is_ntsmcf[intro]:
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F ℌ : 𝔉 ∘⇩S⇩M⇩C⇩F ℌ ↦⇩S⇩M⇩C⇩F 𝔊 ∘⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔑: is_ntsmcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_semifunctor α 𝔄 𝔅 ℌ by (rule assms(2))
  show ?thesis
  proof(rule is_ntsmcfI)
    show "vfsequence (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F ℌ)"
      unfolding tdghm_dghm_comp_def by (simp add: nat_omega_simps)
    from assms show "𝔉 ∘⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
      by (cs_concl cs_intro: smc_cs_intros)
    from assms show "𝔊 ∘⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" 
      by (cs_concl cs_intro: smc_cs_intros)
    show "vcard (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F ℌ) = 5⇩ℕ"
      unfolding tdghm_dghm_comp_def by (simp add: nat_omega_simps)
    from assms show 
      "ntsmcf_tdghm (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F ℌ) :
        smcf_dghm (𝔉 ∘⇩S⇩M⇩C⇩F ℌ) ↦⇩D⇩G⇩H⇩M smcf_dghm (𝔊 ∘⇩S⇩M⇩C⇩F ℌ) :
        smc_dg 𝔄 ↦↦⇩D⇩G⇘α⇙ smc_dg ℭ"
      by 
        (
          cs_concl 
            cs_simp: slicing_commute[symmetric] 
            cs_intro: slicing_intros dg_cs_intros
        )
    show 
      "(𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F ℌ)⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ (𝔉 ∘⇩S⇩M⇩C⇩F ℌ)⦇ArrMap⦈⦇f⦈ =
        (𝔊 ∘⇩S⇩M⇩C⇩F ℌ)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F ℌ)⦇NTMap⦈⦇a⦈"
      if "f : a ↦⇘𝔄⇙ b" for a b f
      using that by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  qed (auto simp: smc_cs_simps)
qed

lemma ntsmcf_smcf_comp_is_semifunctor'[smc_cs_intros]:
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" 
    and "ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔉' = 𝔉 ∘⇩S⇩M⇩C⇩F ℌ"
    and "𝔊' = 𝔊 ∘⇩S⇩M⇩C⇩F ℌ"
  shows "𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F ℌ : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) ..


subsubsection‹Further properties›

lemma ntsmcf_smcf_comp_ntsmcf_smcf_comp_assoc:
  assumes "𝔑 : ℌ ↦⇩S⇩M⇩C⇩F ℌ' : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇" 
    and "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" 
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "(𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔊) ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔉 = 𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)"
proof-
  interpret 𝔑: is_ntsmcf α ℭ 𝔇 ℌ ℌ' 𝔑 by (rule assms(1))
  interpret 𝔊: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(2))
  interpret 𝔉: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(3))
  show ?thesis  
  proof(rule ntsmcf_tdghm_eqI)
    from assms show 
      "(𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔊) ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔉 :
        ℌ ∘⇩S⇩M⇩C⇩F 𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 ↦⇩S⇩M⇩C⇩F ℌ' ∘⇩S⇩M⇩C⇩F 𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 :
        𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
      by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
    show "𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) :
      ℌ ∘⇩S⇩M⇩C⇩F 𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 ↦⇩S⇩M⇩C⇩F ℌ' ∘⇩S⇩M⇩C⇩F 𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 :
      𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
      by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
    from assms show 
      "ntsmcf_tdghm ((𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔊) ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔉) =
        ntsmcf_tdghm (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉))"
      by 
        (
          cs_concl 
            cs_simp: slicing_commute[symmetric] 
            cs_intro: slicing_intros tdghm_dghm_comp_tdghm_dghm_comp_assoc
        )
  qed simp_all
qed

lemma (in is_ntsmcf) ntsmcf_ntsmcf_smcf_comp_smcf_id[smc_cs_simps]:
  "𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F smcf_id 𝔄 = 𝔑"
proof(rule ntsmcf_tdghm_eqI)
  show "𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F smcf_id 𝔄 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  show "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  show "ntsmcf_tdghm (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F smcf_id 𝔄) = ntsmcf_tdghm 𝔑"
    by 
      (
        cs_concl cs_shallow
          cs_simp: slicing_simps slicing_commute[symmetric] 
          cs_intro: smc_cs_intros slicing_intros dg_cs_simps
      )
qed simp_all

lemmas [smc_cs_simps] = is_ntsmcf.ntsmcf_ntsmcf_smcf_comp_smcf_id

lemma ntsmcf_vcomp_ntsmcf_smcf_comp[smc_cs_simps]:
  assumes "𝔎 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔐 : 𝔊 ↦⇩S⇩M⇩C⇩F ℌ : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
  shows 
    "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎) ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎) = 
      (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎"
proof(rule ntsmcf_eqI)
  from assms show "(𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎 : 
    𝔉 ∘⇩S⇩M⇩C⇩F 𝔎 ↦⇩S⇩M⇩C⇩F ℌ ∘⇩S⇩M⇩C⇩F 𝔎 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_intro: smc_cs_intros)
  from assms show "𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎) : 
    𝔉 ∘⇩S⇩M⇩C⇩F 𝔎 ↦⇩S⇩M⇩C⇩F ℌ ∘⇩S⇩M⇩C⇩F 𝔎 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_intro: smc_cs_intros)
  from assms have dom_lhs: 
    "𝒟⇩∘ ((𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎))⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  from assms have dom_rhs: "𝒟⇩∘ ((𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎)⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  show 
    "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎))⦇NTMap⦈ = 
      (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎)⦇NTMap⦈"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
    with assms show 
      "(𝔐 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎))⦇NTMap⦈⦇a⦈ =
        (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎)⦇NTMap⦈⦇a⦈"
      by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  qed (cs_concl cs_shallow cs_intro: smc_cs_intros)+
qed simp_all



subsection‹
Composition of a semifunctor and a natural transformation of semifunctors
›


subsubsection‹Definition and elementary properties›

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


text‹Slicing.›

lemma ntsmcf_tdghm_smcf_ntsmcf_comp[slicing_commute]: 
  "smcf_dghm ℌ ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M ntsmcf_tdghm 𝔑 = ntsmcf_tdghm (ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)"
  unfolding 
    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_ntsmcf) 
  dghm_tdghm_comp_components(1)[where 𝔑=𝔑, unfolded ntsmcf_NTDGDom]
  |vdomain smcf_ntsmcf_comp_NTMap_vdomain[smc_cs_simps]|
  |app smcf_ntsmcf_comp_NTMap_app[smc_cs_simps]|

lemmas [smc_cs_simps] = 
  is_ntsmcf.smcf_ntsmcf_comp_NTMap_vdomain
  is_ntsmcf.smcf_ntsmcf_comp_NTMap_app

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


subsubsection‹
Opposite of the composition of a semifunctor
and a natural transformation of semifunctors 
›

lemma op_ntsmcf_smcf_ntsmcf_comp[smc_op_simps]: 
  "op_ntsmcf (ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) = op_smcf ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F op_ntsmcf 𝔑"
  unfolding 
    dghm_tdghm_comp_def
    dghm_comp_def
    op_ntsmcf_def
    op_smcf_def
    op_smc_def
    dg_field_simps
    dghm_field_simps
    nt_field_simps
  by (simp add: nat_omega_simps) (*slow*)


subsubsection‹
Composition of a semifunctor and a natural transformation of
semifunctors is a natural transformation of semifunctors
›

lemma smcf_ntsmcf_comp_is_ntsmcf[intro]:
  assumes "ℌ : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 : ℌ ∘⇩S⇩M⇩C⇩F 𝔉 ↦⇩S⇩M⇩C⇩F ℌ ∘⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
proof-
  interpret ℌ: is_semifunctor α 𝔅 ℭ ℌ by (rule assms(1))
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis
  proof(rule is_ntsmcfI)
    show "vfsequence (ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)" unfolding dghm_tdghm_comp_def by simp
    from assms show "ℌ ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
      by (cs_concl cs_intro: smc_cs_intros)
    from assms show "ℌ ∘⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
      by (cs_concl cs_intro: smc_cs_intros)
    show "vcard (ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) = 5⇩ℕ"
      unfolding dghm_tdghm_comp_def by (simp add: nat_omega_simps)
    from assms show "ntsmcf_tdghm (ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) :
      smcf_dghm (ℌ ∘⇩S⇩M⇩C⇩F 𝔉) ↦⇩D⇩G⇩H⇩M smcf_dghm (ℌ ∘⇩S⇩M⇩C⇩F 𝔊) :
      smc_dg 𝔄 ↦↦⇩D⇩G⇘α⇙ smc_dg ℭ"
      by 
        (
          cs_concl  
            cs_simp: slicing_commute[symmetric]  
            cs_intro: dg_cs_intros slicing_intros
        )
    have [smc_cs_simps]:  
      "ℌ⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇b⦈⦈ ∘⇩A⇘ℭ⇙ ℌ⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈ =
        ℌ⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇f⦈⦈ ∘⇩A⇘ℭ⇙ ℌ⦇ArrMap⦈⦇𝔑⦇NTMap⦈⦇a⦈⦈"
      if "f : a ↦⇘𝔄⇙ b" for a b f
      using assms that 
      by 
        (
          cs_concl  
            cs_simp:
              is_ntsmcf.ntsmcf_Comp_commute 
              is_semifunctor.smcf_ArrMap_Comp[symmetric]
            cs_intro: smc_cs_intros
        )
    from assms show 
      "(ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ (ℌ ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ =
        (ℌ ∘⇩S⇩M⇩C⇩F 𝔊)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ (ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)⦇NTMap⦈⦇a⦈"
      if "f : a ↦⇘𝔄⇙ b" for a b f
      using assms that
      by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  qed (auto simp: smc_cs_simps)
qed

lemma smcf_ntsmcf_comp_is_semifunctor'[smc_cs_intros]:
  assumes "ℌ : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔉' = ℌ ∘⇩S⇩M⇩C⇩F 𝔉"
    and "𝔊' = ℌ ∘⇩S⇩M⇩C⇩F 𝔊"
  shows "ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) ..


subsubsection‹Further properties›

lemma smcf_comp_smcf_ntsmcf_comp_assoc:
  assumes "𝔑 : ℌ ↦⇩S⇩M⇩C⇩F ℌ' : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    and "𝔊 : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
  shows "(𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 = 𝔊 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F (𝔉 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)"
proof(rule ntsmcf_tdghm_eqI)
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 ℌ ℌ' 𝔑 by (rule assms(1))
  interpret 𝔉: is_semifunctor α 𝔅 ℭ 𝔉 by (rule assms(2))
  interpret 𝔊: is_semifunctor α ℭ 𝔇 𝔊 by (rule assms(3))
  from assms show "(𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 :
    𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 ∘⇩S⇩M⇩C⇩F ℌ ↦⇩S⇩M⇩C⇩F 𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 ∘⇩S⇩M⇩C⇩F ℌ' : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
    by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  from assms show "𝔊 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F (𝔉 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) :
    𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 ∘⇩S⇩M⇩C⇩F ℌ ↦⇩S⇩M⇩C⇩F 𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 ∘⇩S⇩M⇩C⇩F ℌ' : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
    by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  from assms show 
    "ntsmcf_tdghm (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) =
      ntsmcf_tdghm (𝔊 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F (𝔉 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))"
    by
      (
        cs_concl 
          cs_simp: slicing_commute[symmetric] 
          cs_intro: slicing_intros dghm_comp_dghm_tdghm_comp_assoc
      )
qed simp_all

lemma (in is_ntsmcf) ntsmcf_smcf_ntsmcf_comp_smcf_id[smc_cs_simps]:
  "smcf_id 𝔅 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 = 𝔑"
proof(rule ntsmcf_tdghm_eqI)
  show "smcf_id 𝔅 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  show "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  show "ntsmcf_tdghm (dghm_id 𝔅 ∘⇩D⇩G⇩H⇩M⇩-⇩T⇩D⇩G⇩H⇩M 𝔑) = ntsmcf_tdghm 𝔑"
    by 
      (
        cs_concl cs_shallow
          cs_simp: slicing_simps slicing_commute[symmetric] 
          cs_intro: smc_cs_intros slicing_intros dg_cs_simps
      )
qed simp_all

lemmas [smc_cs_simps] = is_ntsmcf.ntsmcf_smcf_ntsmcf_comp_smcf_id

lemma smcf_ntsmcf_comp_ntsmcf_smcf_comp_assoc:
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    and "ℌ : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
    and "𝔎 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "(ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎 = ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F (𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F 𝔎)"
proof-
  interpret 𝔑: is_ntsmcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_semifunctor α ℭ 𝔇 ℌ by (rule assms(2))
  interpret 𝔎: is_semifunctor α 𝔄 𝔅 𝔎 by (rule assms(3))
  show ?thesis
    by (rule ntsmcf_tdghm_eqI)
      (
        use assms in
          ‹
            cs_concl 
              cs_simp: smc_cs_simps slicing_commute[symmetric]
              cs_intro:
                smc_cs_intros
                slicing_intros
                dghm_tdghm_comp_tdghm_dghm_comp_assoc
          ›
      )+
qed

lemma smcf_ntsmcf_comp_ntsmcf_vcomp: 
  assumes "𝔎 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    and "𝔐 : 𝔊 ↦⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows 
    "𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) =
      (𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔐) ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)"
proof-
  interpret 𝔎: is_semifunctor α 𝔅 ℭ 𝔎 by (rule assms(1))
  interpret 𝔐: is_ntsmcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(2))
  interpret 𝔑: is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(3))
  show 
    "𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑) = 𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑)"
  proof(rule ntsmcf_eqI)
    have dom_lhs: "𝒟⇩∘ ((𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈) = 𝔄⦇Obj⦈"
      unfolding dghm_tdghm_comp_components smc_cs_simps by simp
    have dom_rhs: 
      "𝒟⇩∘ ((𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈) = 𝔄⦇Obj⦈"
      unfolding ntsmcf_vcomp_components smc_cs_simps by simp
    show
      "(𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈ =
        (𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs smc_cs_simps)
      fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
      then show 
        "(𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F (𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈⦇a⦈ =
          (𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F (𝔎 ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑))⦇NTMap⦈⦇a⦈"
        by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
    qed (cs_concl cs_shallow cs_intro: smc_cs_intros)+
  qed (cs_concl cs_shallow cs_intro: smc_cs_intros)+
qed

text‹\newpage›

end