Theory CZH_ECAT_FUNCT

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹FUNCT› and ‹Funct››
theory CZH_ECAT_FUNCT
  imports
    CZH_SMC_FUNCT
    CZH_ECAT_Subcategory
    CZH_ECAT_NTCF
begin



subsection‹Background›


text‹
The subsection presents the theory of the categories of ‹α›-functors
between two ‹α›-categories.
It continues the development that was initiated in sections 
\ref{sec:dg_FUNCT} and \ref{sec:smc_FUNCT}.
A general reference for this section is Chapter II-4 in 
\<^cite>‹"mac_lane_categories_2010"›.
›

named_theorems cat_FUNCT_cs_simps
named_theorems cat_FUNCT_cs_intros

lemmas (in is_functor) [cat_FUNCT_cs_simps] = cat_map_cs_simps
lemmas (in is_functor) [cat_FUNCT_cs_intros] = cat_map_cs_intros

lemmas [cat_FUNCT_cs_simps] = cat_map_cs_simps
lemmas [cat_FUNCT_cs_intros] = cat_map_cs_intros



subsection‹‹FUNCT››


subsubsection‹Definition and elementary properties›

definition cat_FUNCT :: "V ⇒ V ⇒ V ⇒ V"
  where "cat_FUNCT α 𝔄 𝔅 =
    [
      cf_maps α 𝔄 𝔅,
      ntcf_arrows α 𝔄 𝔅,
      (λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈),
      (λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈),
      (λ𝔐𝔑∈⇩∘composable_arrs (dg_FUNCT α 𝔄 𝔅). 𝔐𝔑⦇0⦈ ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔐𝔑⦇1⇩ℕ⦈),
      (λ𝔉∈⇩∘cf_maps α 𝔄 𝔅. ntcf_arrow_id 𝔄 𝔅 𝔉)
    ]⇩∘"


text‹Components.›

lemma cat_FUNCT_components:
  shows [cat_FUNCT_cs_simps]: "cat_FUNCT α 𝔄 𝔅⦇Obj⦈ = cf_maps α 𝔄 𝔅"
    and "cat_FUNCT α 𝔄 𝔅⦇Arr⦈ = ntcf_arrows α 𝔄 𝔅"
    and "cat_FUNCT α 𝔄 𝔅⦇Dom⦈ = (λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈)"
    and "cat_FUNCT α 𝔄 𝔅⦇Cod⦈ = (λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈)"
    and "cat_FUNCT α 𝔄 𝔅⦇Comp⦈ =
      (λ𝔐𝔑∈⇩∘composable_arrs (dg_FUNCT α 𝔄 𝔅). 𝔐𝔑⦇0⦈ ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔐𝔑⦇1⇩ℕ⦈)"
    and "cat_FUNCT α 𝔄 𝔅⦇CId⦈ = (λ𝔉∈⇩∘cf_maps α 𝔄 𝔅. ntcf_arrow_id 𝔄 𝔅 𝔉)"
  unfolding cat_FUNCT_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cat_smc_FUNCT: "cat_smc (cat_FUNCT α 𝔄 𝔅) = smc_FUNCT α 𝔄 𝔅"
proof(rule vsv_eqI)
  show "vsv (cat_smc (cat_FUNCT α 𝔄 𝔅))" unfolding cat_smc_def by auto
  show "vsv (smc_FUNCT α 𝔄 𝔅)" unfolding smc_FUNCT_def by auto
  have dom_lhs: "𝒟⇩∘ (cat_smc (cat_FUNCT α 𝔄 𝔅)) = 5⇩ℕ" 
    unfolding cat_smc_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (smc_FUNCT α 𝔄 𝔅) = 5⇩ℕ"
    unfolding smc_FUNCT_def by (simp add: nat_omega_simps)
  show "𝒟⇩∘ (cat_smc (cat_FUNCT α 𝔄 𝔅)) = 𝒟⇩∘ (smc_FUNCT α 𝔄 𝔅)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ (cat_smc (cat_FUNCT α 𝔄 𝔅)) ⟹
    cat_smc (cat_FUNCT α 𝔄 𝔅)⦇a⦈ = smc_FUNCT α 𝔄 𝔅⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral, 
        unfold cat_smc_def dg_field_simps cat_FUNCT_def smc_FUNCT_def
      )
      (auto simp: nat_omega_simps)
qed

context is_ntcf
begin

lemmas_with [folded cat_smc_FUNCT, unfolded slicing_simps]: 
  cat_FUNCT_Dom_app = smc_FUNCT_Dom_app
  and cat_FUNCT_Cod_app = smc_FUNCT_Cod_app

end

lemmas [smc_FUNCT_cs_simps] = 
  is_ntcf.cat_FUNCT_Dom_app
  is_ntcf.cat_FUNCT_Cod_app

lemmas_with [folded cat_smc_FUNCT, unfolded slicing_simps]: 
  cat_FUNCT_Dom_vsv[intro] = smc_FUNCT_Dom_vsv
  and cat_FUNCT_Dom_vdomain[cat_FUNCT_cs_simps] = smc_FUNCT_Dom_vdomain
  and cat_FUNCT_Cod_vsv[intro] = smc_FUNCT_Cod_vsv
  and cat_FUNCT_Cod_vdomain[cat_FUNCT_cs_simps] = smc_FUNCT_Cod_vdomain
  and cat_FUNCT_Dom_vrange = smc_FUNCT_Dom_vrange
  and cat_FUNCT_Cod_vrange = smc_FUNCT_Cod_vrange
  and cat_FUNCT_is_arrI = smc_FUNCT_is_arrI
  and cat_FUNCT_is_arrI'[cat_FUNCT_cs_intros] = smc_FUNCT_is_arrI'
  and cat_FUNCT_is_arrD = smc_FUNCT_is_arrD
  and cat_FUNCT_is_arrE[elim] = smc_FUNCT_is_arrE

lemmas_with [folded cat_smc_FUNCT, unfolded slicing_simps]: 
  cat_FUNCT_Comp_app[cat_FUNCT_cs_simps] = smc_FUNCT_Comp_app


subsubsection‹Identity›

mk_VLambda cat_FUNCT_components(6)
  |vsv cat_FUNCT_CId_vsv[cat_FUNCT_cs_intros]|
  |vdomain cat_FUNCT_CId_vdomain[cat_FUNCT_cs_simps]|
  |app cat_FUNCT_CId_app[cat_FUNCT_cs_simps]|

lemma smc_FUNCT_CId_vrange: "ℛ⇩∘ (cat_FUNCT α 𝔄 𝔅⦇CId⦈) ⊆⇩∘ ntcf_arrows α 𝔄 𝔅"
  unfolding cat_FUNCT_components
proof(rule vrange_VLambda_vsubset)
  fix x assume "x ∈⇩∘ cf_maps α 𝔄 𝔅"
  then obtain 𝔉 where x_def: "x = cf_map 𝔉" and 𝔉: "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by clarsimp  
  then show "ntcf_arrow_id 𝔄 𝔅 x ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
    unfolding x_def
    by 
      (
        cs_concl 
          cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros cat_FUNCT_cs_intros
      )
qed



subsubsection‹
The conversion of a natural transformation arrow 
to a natural transformation is a bijection
›

lemma bij_betw_ntcf_of_ntcf_arrow:
  "bij_betw
    (ntcf_of_ntcf_arrow 𝔄 𝔅)
    (elts (ntcf_arrows α 𝔄 𝔅))
    (elts (ntcfs α 𝔄 𝔅))"
proof(intro bij_betw_imageI inj_onI subset_antisym subsetI)
  fix 𝔐 𝔑 assume prems: 
    "𝔐 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
    "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
    "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔐 = ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑"
  from prems(1) obtain 𝔐' 𝔉 𝔊 
    where 𝔐_def: "𝔐 = ntcf_arrow 𝔐'" and 𝔐': "𝔐' : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by auto
  from prems(2) obtain 𝔑' 𝔉' 𝔊' 
    where 𝔑_def: "𝔑 = ntcf_arrow 𝔑'" and 𝔑': "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by auto
  from prems(3) have "𝔐' = 𝔑'"
    unfolding 
      𝔐_def 
      𝔑_def  
      is_ntcf.ntcf_of_ntcf_arrow[OF 𝔐']
      is_ntcf.ntcf_of_ntcf_arrow[OF 𝔑']
    by simp
  then show "𝔐 = 𝔑" unfolding 𝔐_def 𝔑_def by auto
next
  fix 𝔐 assume 
    "𝔐 ∈ ntcf_of_ntcf_arrow 𝔄 𝔅 ` elts (ntcf_arrows α 𝔄 𝔅)"
  then obtain 𝔐' where 𝔐': "𝔐' ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
    and 𝔐_def: "𝔐 = ntcf_of_ntcf_arrow 𝔄 𝔅 𝔐'"
    by auto  
  from 𝔐' obtain 𝔐'' 𝔉 𝔊
    where 𝔐'_def: "𝔐' = ntcf_arrow 𝔐''" 
      and 𝔐'': "𝔐'' : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by auto
  from 𝔐'' show "𝔐 ∈⇩∘ ntcfs α 𝔄 𝔅"
    unfolding 𝔐_def 𝔐'_def is_ntcf.ntcf_of_ntcf_arrow[OF 𝔐''] by auto
next
  fix 𝔐 assume "𝔐 ∈⇩∘ ntcfs α 𝔄 𝔅"
  then obtain 𝔉 𝔊 where 𝔐: "𝔐 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by clarsimp
  then have "𝔐 = ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔐)" 
    by (cs_concl cs_shallow cs_simp: cat_FUNCT_cs_simps)
  moreover from 𝔐 have "ntcf_arrow 𝔐 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
    by (cs_concl cs_intro: cat_FUNCT_cs_intros)
  ultimately show "𝔐 ∈ ntcf_of_ntcf_arrow 𝔄 𝔅 ` elts (ntcf_arrows α 𝔄 𝔅)"
    by simp
qed

lemma bij_betw_ntcf_of_ntcf_arrow_Hom:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "bij_betw
    (ntcf_of_ntcf_arrow 𝔄 𝔅)
    (elts (Hom (cat_FUNCT α 𝔄 𝔅) (cf_map 𝔉) (cf_map 𝔊)))
    (elts (these_ntcfs α 𝔄 𝔅 𝔉 𝔊))"
proof-

  interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔄 𝔅 𝔊  by (rule assms(2))

  from assms have [cat_cs_simps]:
    "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉) = 𝔉"
    "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔊) = 𝔊"
    by (cs_concl cs_shallow cs_simp: cat_FUNCT_cs_simps)+

  show ?thesis
  proof
    (
      rule bij_betw_subset[OF bij_betw_ntcf_of_ntcf_arrow];
      (intro subset_antisym subsetI)?;
      (unfold in_Hom_iff)?
    )
    fix 𝔑 assume prems: "𝔑 : cf_map 𝔉 ↦⇘cat_FUNCT α 𝔄 𝔅⇙ cf_map 𝔊"  
    note 𝔑 = cat_FUNCT_is_arrD[OF prems, unfolded cat_cs_simps]
    from 𝔑(1) show "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
      by (subst 𝔑(2)) (cs_concl cs_intro: cat_FUNCT_cs_intros)  
  next
    fix 𝔑 assume 
      "𝔑 ∈ ntcf_of_ntcf_arrow 𝔄 𝔅 `
        elts (Hom (cat_FUNCT α 𝔄 𝔅) (cf_map 𝔉) (cf_map 𝔊))"
    then obtain 𝔑' 
      where 𝔑': "𝔑' ∈⇩∘ Hom (cat_FUNCT α 𝔄 𝔅) (cf_map 𝔉) (cf_map 𝔊)"
        and 𝔑_def: "𝔑 = ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑'"
      by auto
    note 𝔑' = cat_FUNCT_is_arrD[
        OF 𝔑'[unfolded cat_cs_simps], unfolded cat_cs_simps
        ]
    from 𝔑'(1) show "𝔑 ∈⇩∘ these_ntcfs α 𝔄 𝔅 𝔉 𝔊" unfolding 𝔑_def by simp
  next
    fix 𝔑 assume "𝔑 ∈⇩∘ these_ntcfs α 𝔄 𝔅 𝔉 𝔊"
    then have 𝔑: "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by simp
    then have "𝔑 = ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑)"
      by (cs_concl cs_shallow cs_simp: cat_FUNCT_cs_simps)  
    moreover from 𝔑 have
      "ntcf_arrow 𝔑 ∈⇩∘ Hom (cat_FUNCT α 𝔄 𝔅) (cf_map 𝔉) (cf_map 𝔊)"
      unfolding in_Hom_iff by (cs_concl cs_shallow cs_intro: cat_FUNCT_cs_intros)
    ultimately show 
      "𝔑 ∈ ntcf_of_ntcf_arrow 𝔄 𝔅 `
        elts (Hom (cat_FUNCT α 𝔄 𝔅) (cf_map 𝔉) (cf_map 𝔊))"
      by simp
  qed

qed


subsubsection‹‹FUNCT› is a category›

lemma (in 𝒵) tiny_category_cat_FUNCT[cat_FUNCT_cs_intros]: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_category β (cat_FUNCT α 𝔄 𝔅)" (is ‹tiny_category β ?FUNCT›)
proof(intro tiny_categoryI)
  show "vfsequence ?FUNCT" unfolding cat_FUNCT_def by auto
  show "vcard ?FUNCT = 6⇩ℕ" 
    unfolding cat_FUNCT_def by (simp add: nat_omega_simps)
  from assms show "tiny_semicategory β (cat_smc ?FUNCT)"
    unfolding cat_smc_FUNCT 
    by (auto simp add: tiny_semicategory_smc_FUNCT)
  show CId_a: "?FUNCT⦇CId⦈⦇𝔉'⦈ : 𝔉' ↦⇘?FUNCT⇙ 𝔉'" if "𝔉' ∈⇩∘ ?FUNCT⦇Obj⦈" for 𝔉'
  proof-
    from that obtain 𝔉 where 𝔉'_def: "𝔉' = cf_map 𝔉" and 𝔉: "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
      unfolding cat_FUNCT_components by clarsimp 
    show ?thesis
      using that 𝔉
      unfolding cat_FUNCT_components(1) 𝔉'_def
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
  qed
  show "?FUNCT⦇CId⦈⦇𝔊⦈ ∘⇩A⇘?FUNCT⇙ 𝔑 = 𝔑" if "𝔑 : 𝔉 ↦⇘?FUNCT⇙ 𝔊" for 𝔑 𝔉 𝔊
  proof-
    from that obtain 𝔑' 𝔉' 𝔊' 
      where 𝔑': "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
        and 𝔑_def[cat_FUNCT_cs_simps]: "𝔑 = ntcf_arrow 𝔑'"
        and 𝔉_def[cat_FUNCT_cs_simps]: "𝔉 = cf_map 𝔉'"
        and 𝔊_def[cat_FUNCT_cs_simps]: "𝔊 = cf_map 𝔊'"
      by auto
    from 𝔑' show "cat_FUNCT α 𝔄 𝔅⦇CId⦈⦇𝔊⦈ ∘⇩A⇘cat_FUNCT α 𝔄 𝔅⇙ 𝔑 = 𝔑"
      by 
        (
          cs_concl  
            cs_simp: cat_FUNCT_cs_simps cat_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
  qed 
  show "𝔑 ∘⇩A⇘?FUNCT⇙ ?FUNCT⦇CId⦈⦇𝔊⦈ = 𝔑" if "𝔑 : 𝔊 ↦⇘?FUNCT⇙ ℌ" for 𝔑 𝔊 ℌ
  proof-
    note 𝔑 = cat_FUNCT_is_arrD[OF that]
    from 𝔑(1) show "𝔑 ∘⇩A⇘cat_FUNCT α 𝔄 𝔅⇙ cat_FUNCT α 𝔄 𝔅⦇CId⦈⦇𝔊⦈ = 𝔑"
      by (subst (1 2) 𝔑(2), subst 𝔑(3), remdups) 
        (
          cs_concl 
            cs_simp: cat_FUNCT_cs_simps cat_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
  qed 
qed (simp_all add: assms cat_FUNCT_components)

lemmas (in 𝒵) [cat_FUNCT_cs_intros] = tiny_category_cat_FUNCT



subsubsection‹Isomorphism›

lemma cat_FUNCT_is_iso_arrI: 
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "ntcf_arrow 𝔑 : cf_map 𝔉 ↦⇩i⇩s⇩o⇘cat_FUNCT α 𝔄 𝔅⇙ cf_map 𝔊"
proof(intro is_iso_arrI is_inverseI)
  interpret 𝔑: is_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms)
  show is_arr_𝔑: "ntcf_arrow 𝔑 : cf_map 𝔉 ↦⇘cat_FUNCT α 𝔄 𝔅⇙ cf_map 𝔊"
    by (simp add: assms cat_FUNCT_is_arrI is_iso_ntcf.axioms(1))
  interpret inv_𝔑: is_iso_ntcf α 𝔄 𝔅 𝔊 𝔉 ‹inv_ntcf 𝔑› 
    using CZH_ECAT_NTCF.iso_ntcf_is_iso_arr(1)[OF assms] by simp
  from assms show is_arr_inv_𝔑: 
    "ntcf_arrow (inv_ntcf 𝔑) : cf_map 𝔊 ↦⇘cat_FUNCT α 𝔄 𝔅⇙ cf_map 𝔉"
    by 
      (
        cs_concl cs_shallow cs_intro:
          ntcf_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  from assms show "ntcf_arrow 𝔑 : cf_map 𝔉 ↦⇘cat_FUNCT α 𝔄 𝔅⇙ cf_map 𝔊" 
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
  from assms show 
    "ntcf_arrow (inv_ntcf 𝔑) ∘⇩A⇘cat_FUNCT α 𝔄 𝔅⇙ ntcf_arrow 𝔑 = 
      cat_FUNCT α 𝔄 𝔅⦇CId⦈⦇cf_map 𝔉⦈"
    "ntcf_arrow 𝔑 ∘⇩A⇘cat_FUNCT α 𝔄 𝔅⇙ ntcf_arrow (inv_ntcf 𝔑) = 
      cat_FUNCT α 𝔄 𝔅⦇CId⦈⦇cf_map 𝔊⦈"
    by 
      (
        cs_concl cs_shallow
          cs_simp: iso_ntcf_is_iso_arr(2,3) cat_FUNCT_cs_simps
          cs_intro: ntcf_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )+
qed

lemma cat_FUNCT_is_iso_arrI'[cat_FUNCT_cs_intros]: 
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑' = ntcf_arrow 𝔑" 
    and "𝔉' = cf_map 𝔉"
    and "𝔊' = cf_map 𝔊"
  shows "𝔑' : 𝔉' ↦⇩i⇩s⇩o⇘cat_FUNCT α 𝔄 𝔅⇙ cf_map 𝔊"
  using assms(1) unfolding assms(2-4) by (rule cat_FUNCT_is_iso_arrI)

lemma cat_FUNCT_is_iso_arrD:
  assumes "𝔑 : 𝔉 ↦⇩i⇩s⇩o⇘cat_FUNCT α 𝔄 𝔅⇙ 𝔊" (is ‹𝔑 : 𝔉 ↦⇩i⇩s⇩o⇘?FUNCT⇙ 𝔊›)
  shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
    cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o cf_of_cf_map 𝔄 𝔅 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔑 = ntcf_arrow (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑)"
    and "𝔉 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔉)"
    and "𝔊 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔊)"
proof-
  from assms(1) have 𝔑: "𝔑 : 𝔉 ↦⇘cat_FUNCT α 𝔄 𝔅⇙ 𝔊"
    unfolding is_iso_arr_def by simp
  interpret 𝒵 α by (rule is_ntcfD[OF cat_FUNCT_is_arrD(1)[OF 𝔑]])
  define β where "β = α + ω"
  have 𝒵β: "𝒵 β" and αβ: "α ∈⇩∘ β"
    by (simp_all add: 𝒵_α_αω 𝒵.intro 𝒵_Limit_αω 𝒵_ω_αω β_def)
  interpret FUNCT: tiny_category β ?FUNCT 
    by (rule tiny_category_cat_FUNCT[OF 𝒵β αβ, of 𝔄 𝔅])
  have inv_𝔑: "𝔑¯⇩C⇘?FUNCT⇙ : 𝔊 ↦⇩i⇩s⇩o⇘?FUNCT⇙ 𝔉"
    and inv_𝔑_𝔑: "𝔑¯⇩C⇘?FUNCT⇙ ∘⇩A⇘?FUNCT⇙ 𝔑 = ?FUNCT⦇CId⦈⦇𝔉⦈"
    and 𝔑_inv_𝔑: "𝔑 ∘⇩A⇘?FUNCT⇙ 𝔑¯⇩C⇘?FUNCT⇙ = ?FUNCT⦇CId⦈⦇𝔊⦈"
    by 
      (
        intro 
          FUNCT.cat_the_inverse_is_iso_arr[OF assms] 
          FUNCT.cat_the_inverse_Comp_CId[OF assms]
      )+
  from assms is_iso_arrD inv_𝔑 
  have 𝔑_is_arr: "𝔑 : 𝔉 ↦⇘cat_FUNCT α 𝔄 𝔅⇙ 𝔊" 
    and inv_𝔑_is_arr: "𝔑¯⇩C⇘?FUNCT⇙ : 𝔊 ↦⇘cat_FUNCT α 𝔄 𝔅⇙ 𝔉"
    by auto
  note 𝔑_is_arr = cat_FUNCT_is_arrD[OF 𝔑_is_arr]
  note inv_𝔑_is_arr = cat_FUNCT_is_arrD[OF inv_𝔑_is_arr]
  let ?𝔑 = ‹ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑›
    and ?inv_𝔑 = ‹ntcf_of_ntcf_arrow 𝔄 𝔅 (𝔑¯⇩C⇘cat_FUNCT α 𝔄 𝔅⇙)›
  from inv_𝔑_𝔑 𝔑_is_arr(1) inv_𝔑_is_arr(1) have inv_𝔑_𝔑:
    "?inv_𝔑 ∙⇩N⇩T⇩C⇩F ?𝔑 = ntcf_id (cf_of_cf_map 𝔄 𝔅 𝔉)"
    by  
      (
        subst (asm) inv_𝔑_is_arr(2), 
        use nothing in ‹subst (asm) (2) 𝔑_is_arr(2), subst (asm) 𝔑_is_arr(3)›
      )
      (
        cs_prems cs_shallow
          cs_simp: cat_FUNCT_cs_simps
          cs_intro: cat_FUNCT_cs_intros cat_cs_intros
      )
  from 𝔑_inv_𝔑 inv_𝔑_is_arr(1) 𝔑_is_arr(1) have 𝔑_inv_𝔑:
    "?𝔑 ∙⇩N⇩T⇩C⇩F ?inv_𝔑 = ntcf_id (cf_of_cf_map 𝔄 𝔅 𝔊)"
    by  
      (
        subst (asm) inv_𝔑_is_arr(2), 
        use nothing in ‹subst (asm) 𝔑_is_arr(2), subst (asm) 𝔑_is_arr(4)›
      )
      (
        cs_prems cs_shallow
          cs_simp: cat_FUNCT_cs_simps 
          cs_intro: cat_FUNCT_cs_intros cat_cs_intros
      )
  show "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
    cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o cf_of_cf_map 𝔄 𝔅 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by 
      (
        rule CZH_ECAT_NTCF.is_iso_arr_is_iso_ntcf[
          OF 𝔑_is_arr(1) inv_𝔑_is_arr(1) 𝔑_inv_𝔑 inv_𝔑_𝔑 
          ]
      )
  show "𝔑 = ntcf_arrow (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑)"
    and "𝔉 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔉)"
    and "𝔊 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔊)"
    by (intro 𝔑_is_arr(2-4))+   
qed



subsection‹‹Funct››


subsubsection‹Definition and elementary properties›

definition cat_Funct :: "V ⇒ V ⇒ V ⇒ V"
  where "cat_Funct α 𝔄 𝔅 =
    [
      tm_cf_maps α 𝔄 𝔅,
      tm_ntcf_arrows α 𝔄 𝔅,
      (λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈),
      (λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈),
      (λ𝔐𝔑∈⇩∘composable_arrs (dg_Funct α 𝔄 𝔅). 𝔐𝔑⦇0⦈ ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔐𝔑⦇1⇩ℕ⦈),
      (λ𝔉∈⇩∘tm_cf_maps α 𝔄 𝔅. ntcf_arrow_id 𝔄 𝔅 𝔉)
    ]⇩∘"


text‹Components.›

lemma cat_Funct_components: 
  shows [cat_FUNCT_cs_simps]: "cat_Funct α 𝔄 𝔅⦇Obj⦈ = tm_cf_maps α 𝔄 𝔅"
    and "cat_Funct α 𝔄 𝔅⦇Arr⦈ = tm_ntcf_arrows α 𝔄 𝔅"
    and "cat_Funct α 𝔄 𝔅⦇Dom⦈ = (λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈)"
    and "cat_Funct α 𝔄 𝔅⦇Cod⦈ = (λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈)"
    and "cat_Funct α 𝔄 𝔅⦇Comp⦈ =
      (λ𝔐𝔑∈⇩∘composable_arrs (dg_Funct α 𝔄 𝔅). 𝔐𝔑⦇0⦈ ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔐𝔑⦇1⇩ℕ⦈)"
    and "cat_Funct α 𝔄 𝔅⦇CId⦈ = (λ𝔉∈⇩∘tm_cf_maps α 𝔄 𝔅. ntcf_arrow_id 𝔄 𝔅 𝔉)"
  unfolding cat_Funct_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cat_smc_Funct: "cat_smc (cat_Funct α 𝔄 𝔅) = smc_Funct α 𝔄 𝔅"
proof(rule vsv_eqI)
  show "vsv (cat_smc (cat_Funct α 𝔄 𝔅))" unfolding cat_smc_def by auto
  show "vsv (smc_Funct α 𝔄 𝔅)" unfolding smc_Funct_def by auto
  have dom_lhs: "𝒟⇩∘ (cat_smc (cat_Funct α 𝔄 𝔅)) = 5⇩ℕ" 
    unfolding cat_smc_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (smc_Funct α 𝔄 𝔅) = 5⇩ℕ"
    unfolding smc_Funct_def by (simp add: nat_omega_simps)
  show "𝒟⇩∘ (cat_smc (cat_Funct α 𝔄 𝔅)) = 𝒟⇩∘ (smc_Funct α 𝔄 𝔅)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ (cat_smc (cat_Funct α 𝔄 𝔅)) ⟹
    cat_smc (cat_Funct α 𝔄 𝔅)⦇a⦈ = smc_Funct α 𝔄 𝔅⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral,
        unfold cat_smc_def dg_field_simps cat_Funct_def smc_Funct_def
      )
      (auto simp: nat_omega_simps)
qed

context is_tm_ntcf
begin

lemmas_with [folded cat_smc_Funct, unfolded slicing_simps]: 
  cat_Funct_Dom_app = smc_Funct_Dom_app
  and cat_Funct_Cod_app = smc_Funct_Cod_app

end

lemmas [cat_FUNCT_cs_simps] = 
  is_tm_ntcf.cat_Funct_Dom_app
  is_tm_ntcf.cat_Funct_Cod_app

lemmas_with [folded cat_smc_Funct, unfolded slicing_simps]: 
  cat_Funct_Dom_vsv[cat_FUNCT_cs_intros] = smc_Funct_Dom_vsv
  and cat_Funct_Dom_vdomain[cat_FUNCT_cs_simps] = smc_Funct_Dom_vdomain
  and cat_Funct_Cod_vsv[cat_FUNCT_cs_intros] = smc_Funct_Cod_vsv
  and cat_Funct_Cod_vdomain[cat_FUNCT_cs_simps] = smc_Funct_Cod_vdomain
  and cat_Funct_Dom_vrange = smc_Funct_Dom_vrange
  and cat_Funct_Cod_vrange = smc_Funct_Cod_vrange
  and cat_Funct_is_arrI = smc_Funct_is_arrI
  and cat_Funct_is_arrI'[cat_FUNCT_cs_intros] = smc_Funct_is_arrI'
  and cat_Funct_is_arrD = smc_Funct_is_arrD
  and cat_Funct_is_arrE[elim] = smc_Funct_is_arrE

lemmas_with [folded cat_smc_Funct, unfolded slicing_simps]: 
  cat_Funct_Comp_app[cat_FUNCT_cs_simps] = smc_Funct_Comp_app


subsubsection‹Identity›

mk_VLambda cat_Funct_components(6)
  |vsv cat_Funct_CId_vsv[intro]|
  |vdomain cat_Funct_CId_vdomain[cat_FUNCT_cs_simps]|
  |app cat_Funct_CId_app[cat_FUNCT_cs_simps]|

lemma smc_Funct_CId_vrange: "ℛ⇩∘ (cat_Funct α 𝔄 𝔅⦇CId⦈) ⊆⇩∘ ntcf_arrows α 𝔄 𝔅"
  unfolding cat_Funct_components
proof(rule vrange_VLambda_vsubset)
  fix 𝔉' assume "𝔉' ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
  then obtain 𝔉 where 𝔉'_def: "𝔉' = cf_map 𝔉" and 𝔉: "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    by clarsimp  
  then show "ntcf_arrow_id 𝔄 𝔅 𝔉' ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
    by 
      (
        cs_concl 
          cs_simp: cat_FUNCT_cs_simps 𝔉'_def
          cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros
      )
qed


subsubsection‹‹Funct› is a category›

lemma category_cat_Funct: 
  assumes "tiny_category α 𝔄" and "category α 𝔅"
  shows "category α (cat_Funct α 𝔄 𝔅)" (is ‹category α ?Funct›)
proof-
  interpret tiny_category α 𝔄 by (rule assms(1))
  show ?thesis
  proof(intro categoryI)
    show "vfsequence ?Funct" by (simp add: cat_Funct_def)
    show "vcard ?Funct = 6⇩ℕ" 
      unfolding cat_Funct_def by (simp add: nat_omega_simps)
    from assms show "semicategory α (cat_smc (cat_Funct α 𝔄 𝔅))"
      unfolding cat_smc_Funct by (rule semicategory_smc_Funct)
    show "𝒟⇩∘ (cat_Funct α 𝔄 𝔅⦇CId⦈) = cat_Funct α 𝔄 𝔅⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_Funct_components cat_FUNCT_cs_simps)
    show "cat_Funct α 𝔄 𝔅⦇CId⦈⦇𝔉⦈ : 𝔉 ↦⇘cat_Funct α 𝔄 𝔅⇙ 𝔉"
      if "𝔉 ∈⇩∘ cat_Funct α 𝔄 𝔅⦇Obj⦈" for 𝔉
    proof-
      from that have "𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
        unfolding cat_Funct_components by simp
      then obtain 𝔉' 
        where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉': "𝔉' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" 
        by auto
      from assms 𝔉' show "cat_Funct α 𝔄 𝔅⦇CId⦈⦇𝔉⦈ : 𝔉 ↦⇘cat_Funct α 𝔄 𝔅⇙ 𝔉"
        by 
          (
            cs_concl  
              cs_simp: cat_FUNCT_cs_simps 𝔉_def
              cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros
          )
    qed
    show "cat_Funct α 𝔄 𝔅⦇CId⦈⦇𝔊⦈ ∘⇩A⇘cat_Funct α 𝔄 𝔅⇙ 𝔑 = 𝔑"
      if "𝔑 : 𝔉 ↦⇘cat_Funct α 𝔄 𝔅⇙ 𝔊" for 𝔉 𝔊 𝔑
    proof-
      note 𝔑 = cat_Funct_is_arrD[OF that]
      from assms 𝔑(1) show
        "cat_Funct α 𝔄 𝔅⦇CId⦈⦇𝔊⦈ ∘⇩A⇘cat_Funct α 𝔄 𝔅⇙ 𝔑 = 𝔑"
        by (subst (1 2) 𝔑(2), use nothing in ‹subst 𝔑(4)›)
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros
          )
    qed
    show "𝔑 ∘⇩A⇘cat_Funct α 𝔄 𝔅⇙ cat_Funct α 𝔄 𝔅⦇CId⦈⦇𝔊⦈ = 𝔑"
      if "𝔑 : 𝔊 ↦⇘cat_Funct α 𝔄 𝔅⇙ ℌ" for 𝔊 ℌ 𝔑
    proof-
      note 𝔑 = cat_Funct_is_arrD[OF that]
      from assms 𝔑(1) show 
        "𝔑 ∘⇩A⇘cat_Funct α 𝔄 𝔅⇙ cat_Funct α 𝔄 𝔅⦇CId⦈⦇𝔊⦈ = 𝔑"
        by (subst (1 2) 𝔑(2), use nothing in ‹subst 𝔑(3)›)
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros
          )
    qed
  qed auto
qed

lemma category_cat_Funct'[cat_FUNCT_cs_intros]:
  assumes "tiny_category α 𝔄"
    and "category α 𝔅"
    and "β = α"
  shows "category α (cat_Funct β 𝔄 𝔅)"
  using assms(1,2) unfolding assms(3) by (rule category_cat_Funct)


subsubsection‹‹Funct› is a subcategory of ‹FUNCT››

lemma subcategory_cat_Funct_cat_FUNCT:
  assumes "𝒵 β" and "α ∈⇩∘ β" and "tiny_category α 𝔄" and "category α 𝔅"
  shows "cat_Funct α 𝔄 𝔅 ⊆⇩C⇘β⇙ cat_FUNCT α 𝔄 𝔅"
proof
  (
    intro subcategoryI, 
    unfold cat_smc_FUNCT cat_smc_Funct cat_Funct_components(1)
  )
  interpret category α 𝔅 by (rule assms(4))
  interpret 𝔄𝔅: category α ‹cat_Funct α 𝔄 𝔅›
    by (rule category_cat_Funct[OF assms(3,4)])
  show "category β (cat_Funct α 𝔄 𝔅)"
    by (rule category.cat_category_if_ge_Limit[OF _ assms(1,2)]) 
      (auto intro: cat_cs_intros)
  from assms show "category β (cat_FUNCT α 𝔄 𝔅)"
    by (cs_concl cs_intro: tiny_category_cat_FUNCT cat_small_cs_intros)
  show "smc_Funct α 𝔄 𝔅 ⊆⇩S⇩M⇩C⇘β⇙ smc_FUNCT α 𝔄 𝔅"
    by (rule subsemicategory_smc_Funct_smc_FUNCT[OF assms])
  show "cat_Funct α 𝔄 𝔅⦇CId⦈⦇𝔉⦈ = cat_FUNCT α 𝔄 𝔅⦇CId⦈⦇𝔉⦈" 
    if ‹𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅› for 𝔉
  proof-
    from that obtain 𝔉' where 𝔉_def: "𝔉 = cf_map 𝔉'" 
      and 𝔉': "𝔉' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
      by auto
    from that show ?thesis
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_FUNCT_cs_simps 
            cs_intro: cat_FUNCT_cs_intros tm_cf_maps_in_cf_maps
        )
  qed
qed


subsubsection‹Isomorphism›

lemma (in is_tm_iso_ntcf) cat_Funct_is_iso_arrI: 
  assumes "category α 𝔅"
  shows "ntcf_arrow 𝔑 : cf_map 𝔉 ↦⇩i⇩s⇩o⇘cat_Funct α 𝔄 𝔅⇙ cf_map 𝔊"
proof(intro is_iso_arrI is_inverseI)
  from is_tm_iso_ntcf_axioms show 
    "ntcf_arrow 𝔑 : cf_map 𝔉 ↦⇘cat_Funct α 𝔄 𝔅⇙ cf_map 𝔊"
    by (cs_concl cs_shallow cs_intro: ntcf_cs_intros cat_FUNCT_cs_intros)
  interpret inv_𝔑: is_tm_iso_ntcf α 𝔄 𝔅 𝔊 𝔉 ‹inv_ntcf 𝔑› 
    by (rule iso_tm_ntcf_is_iso_arr(1)[OF assms is_tm_iso_ntcf_axioms]) 
  from inv_𝔑.is_tm_iso_ntcf_axioms show 
    "ntcf_arrow (inv_ntcf 𝔑) : cf_map 𝔊 ↦⇘cat_Funct α 𝔄 𝔅⇙ cf_map 𝔉"
    by (cs_concl cs_shallow cs_intro: ntcf_cs_intros cat_FUNCT_cs_intros)
  from is_tm_iso_ntcf_axioms show 
    "ntcf_arrow 𝔑 : cf_map 𝔉 ↦⇘cat_Funct α 𝔄 𝔅⇙ cf_map 𝔊" 
    by (cs_concl cs_shallow cs_intro: ntcf_cs_intros cat_FUNCT_cs_intros)
  from assms is_tm_iso_ntcf_axioms show 
    "ntcf_arrow (inv_ntcf 𝔑) ∘⇩A⇘cat_Funct α 𝔄 𝔅⇙ ntcf_arrow 𝔑 =
      cat_Funct α 𝔄 𝔅⦇CId⦈⦇cf_map 𝔉⦈"
    "ntcf_arrow 𝔑 ∘⇩A⇘cat_Funct α 𝔄 𝔅⇙ ntcf_arrow (inv_ntcf 𝔑) =
      cat_Funct α 𝔄 𝔅⦇CId⦈⦇cf_map 𝔊⦈"
    by
      (
        cs_concl 
          cs_simp: iso_tm_ntcf_is_iso_arr(2,3) cat_FUNCT_cs_simps
          cs_intro: ntcf_cs_intros cat_FUNCT_cs_intros cat_small_cs_intros
      )+
qed

lemma (in is_tm_iso_ntcf) cat_Funct_is_iso_arrI': 
  assumes "category α 𝔅" 
    and "𝔑' = ntcf_arrow 𝔑" 
    and "𝔉' = cf_map 𝔉"
    and "𝔊' = cf_map 𝔊"
  shows "𝔑' : 𝔉' ↦⇩i⇩s⇩o⇘cat_Funct α 𝔄 𝔅⇙ cf_map 𝔊"
  using assms(1) unfolding assms(2-4) by (rule cat_Funct_is_iso_arrI)

lemmas [cat_FUNCT_cs_intros] = 
  is_tm_iso_ntcf.cat_Funct_is_iso_arrI'[rotated 2]

lemma cat_Funct_is_iso_arrD:
  assumes "tiny_category α 𝔄" 
    and "category α 𝔅" 
    and "𝔑 : 𝔉 ↦⇩i⇩s⇩o⇘cat_Funct α 𝔄 𝔅⇙ 𝔊" (is ‹𝔑 : 𝔉 ↦⇩i⇩s⇩o⇘?Funct⇙ 𝔊›)
  shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
    cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F⇩.⇩t⇩m⇩.⇩i⇩s⇩o cf_of_cf_map 𝔄 𝔅 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" 
    and "𝔑 = ntcf_arrow (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑)"
    and "𝔉 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔉)"
    and "𝔊 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔊)"
proof-
  interpret Funct: category α ?Funct
    by (rule category_cat_Funct[OF assms(1,2)])
  have inv_𝔑: "𝔑¯⇩C⇘?Funct⇙ : 𝔊 ↦⇩i⇩s⇩o⇘?Funct⇙ 𝔉"
    and inv_𝔑_𝔑: "𝔑¯⇩C⇘?Funct⇙ ∘⇩A⇘?Funct⇙ 𝔑 = ?Funct⦇CId⦈⦇𝔉⦈"
    and 𝔑_inv_𝔑: "𝔑 ∘⇩A⇘?Funct⇙ 𝔑¯⇩C⇘?Funct⇙ = ?Funct⦇CId⦈⦇𝔊⦈"
    by 
      (
        intro 
          Funct.cat_the_inverse_is_iso_arr[OF assms(3)] 
          Funct.cat_the_inverse_Comp_CId[OF assms(3)]
      )+
  from assms is_iso_arrD inv_𝔑 
  have 𝔑_is_arr: "𝔑 : 𝔉 ↦⇘cat_Funct α 𝔄 𝔅⇙ 𝔊" 
    and inv_𝔑_is_arr: "𝔑¯⇩C⇘?Funct⇙ : 𝔊 ↦⇘cat_Funct α 𝔄 𝔅⇙ 𝔉"
    by auto
  note 𝔑_is_arr = cat_Funct_is_arrD[OF 𝔑_is_arr]
  note inv_𝔑_is_arr = cat_Funct_is_arrD[OF inv_𝔑_is_arr]
  let ?𝔑 = ‹ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑›
    and ?inv_𝔑 = ‹ntcf_of_ntcf_arrow 𝔄 𝔅 (𝔑¯⇩C⇘cat_Funct α 𝔄 𝔅⇙)›
  from inv_𝔑_𝔑 𝔑_is_arr(1) inv_𝔑_is_arr(1) have inv_𝔑_𝔑:
    "?inv_𝔑 ∙⇩N⇩T⇩C⇩F ?𝔑 = ntcf_id (cf_of_cf_map 𝔄 𝔅 𝔉)"
    by  
      (
        subst (asm) inv_𝔑_is_arr(2), 
        use nothing in ‹subst (asm) (2) 𝔑_is_arr(2), subst (asm) 𝔑_is_arr(3)›
      )
      (
        cs_prems 
          cs_simp: cat_FUNCT_cs_simps 
          cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros
      )
  from 𝔑_inv_𝔑 inv_𝔑_is_arr(1) 𝔑_is_arr(1) have 𝔑_inv_𝔑:
    "?𝔑 ∙⇩N⇩T⇩C⇩F ?inv_𝔑 = ntcf_id (cf_of_cf_map 𝔄 𝔅 𝔊)"
    by
      (
        subst (asm) inv_𝔑_is_arr(2), 
        use nothing in ‹subst (asm) 𝔑_is_arr(2), subst (asm) 𝔑_is_arr(4)›
      )
      (
        cs_prems 
          cs_simp: cat_FUNCT_cs_simps
          cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros
      )
  show "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 : 
    cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F⇩.⇩t⇩m⇩.⇩i⇩s⇩o cf_of_cf_map 𝔄 𝔅 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    by 
      (
        rule is_iso_arr_is_tm_iso_ntcf[
          OF 𝔑_is_arr(1) inv_𝔑_is_arr(1) 𝔑_inv_𝔑 inv_𝔑_𝔑 
          ]
      )
  show "𝔑 = ntcf_arrow (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑)"
    and "𝔉 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔉)"
    and "𝔊 = cf_map (cf_of_cf_map 𝔄 𝔅 𝔊)"
    by (intro 𝔑_is_arr(2-4))+   
qed



subsection‹Diagonal functor›


subsubsection‹Definition and elementary properties›


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

definition cf_diagonal :: "V ⇒ V ⇒ V ⇒ V" (‹Δ⇩C⇩F›)
  where "Δ⇩C⇩F α 𝔍 ℭ =
    [
      (λa∈⇩∘ℭ⦇Obj⦈. cf_map (cf_const 𝔍 ℭ a)),
      (λf∈⇩∘ℭ⦇Arr⦈. ntcf_arrow (ntcf_const 𝔍 ℭ f)), 
      ℭ,
      cat_FUNCT α 𝔍 ℭ
    ]⇩∘"


text‹Components.›

lemma cf_diagonal_components:
  shows "Δ⇩C⇩F α 𝔍 ℭ⦇ObjMap⦈ = (λa∈⇩∘ℭ⦇Obj⦈. cf_map (cf_const 𝔍 ℭ a))"
    and "Δ⇩C⇩F α 𝔍 ℭ⦇ArrMap⦈ = (λf∈⇩∘ℭ⦇Arr⦈. ntcf_arrow (ntcf_const 𝔍 ℭ f))"
    and "Δ⇩C⇩F α 𝔍 ℭ⦇HomDom⦈ = ℭ"
    and "Δ⇩C⇩F α 𝔍 ℭ⦇HomCod⦈ = cat_FUNCT α 𝔍 ℭ"
  unfolding cf_diagonal_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda cf_diagonal_components(1)
  |vsv cf_diagonal_ObjMap_vsv[cat_cs_intros]|
  |vdomain cf_diagonal_ObjMap_vdomain[cat_cs_simps]|
  |app cf_diagonal_ObjMap_app[cat_cs_simps]|

lemma cf_diagonal_ObjMap_vrange:
  assumes "𝒵 β"and "α ∈⇩∘ β" and "category α 𝔍" and "category α ℭ"
  shows "ℛ⇩∘ (Δ⇩C⇩F α 𝔍 ℭ⦇ObjMap⦈) ⊆⇩∘ cat_FUNCT α 𝔍 ℭ⦇Obj⦈"
  unfolding cf_diagonal_components 
proof(rule vrange_VLambda_vsubset)
  interpret β: 𝒵 β by (rule assms(1))
  interpret category α 𝔍 by (rule assms(3))
  interpret FUNCT: tiny_category β ‹(cat_FUNCT α 𝔍 ℭ)›
    by (rule 𝒵.tiny_category_cat_FUNCT[OF 𝒵_axioms assms(1,2)])
  fix x assume prems: "x ∈⇩∘ ℭ⦇Obj⦈"
  from prems assms show "cf_map (cf_const 𝔍 ℭ x) ∈⇩∘ cat_FUNCT α 𝔍 ℭ⦇Obj⦈"
    unfolding cat_FUNCT_components(1)
    by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
qed


subsubsection‹Arrow map›

mk_VLambda cf_diagonal_components(2)
  |vsv cf_diagonal_ArrMap_vsv[cat_cs_intros]|
  |vdomain cf_diagonal_ArrMap_vdomain[cat_cs_simps]|
  |app cf_diagonal_ArrMap_app[cat_cs_simps]|


subsubsection‹Diagonal functor is a functor›

lemma cf_diagonal_is_functor[cat_cs_intros]:
  assumes "𝒵 β" and "α ∈⇩∘ β" and "category α 𝔍" and "category α ℭ"
  shows "Δ⇩C⇩F α 𝔍 ℭ : ℭ ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔍 ℭ" (is ‹?Δ : ℭ ↦↦⇩C⇘β⇙ ?FUNCT›)
proof-

  interpret β: 𝒵 β by (rule assms(1))
  interpret 𝔍: category α 𝔍 by (rule assms(3))
  interpret ℭ: category α ℭ by (rule assms(4))
  interpret FUNCT: tiny_category β ‹(cat_FUNCT α 𝔍 ℭ)›
    by (rule 𝒵.tiny_category_cat_FUNCT[OF 𝔍.𝒵_axioms assms(1,2)])

  show ?thesis
  proof(intro is_functorI')
    show "vfsequence ?Δ" 
      unfolding cf_diagonal_def by (simp add: nat_omega_simps)
    show "category β ℭ" by (rule ℭ.cat_category_if_ge_Limit[OF assms(1,2)])
    from assms show "category β (cat_FUNCT α 𝔍 ℭ)" 
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    show "vcard ?Δ = 4⇩ℕ"
      unfolding cf_diagonal_def by (simp add: nat_omega_simps)
    show "vsv (?Δ⦇ObjMap⦈)" unfolding cf_diagonal_components by simp
    from assms show "ℛ⇩∘ (?Δ⦇ObjMap⦈) ⊆⇩∘ ?FUNCT⦇Obj⦈"
      by (rule cf_diagonal_ObjMap_vrange)
    show "?Δ⦇ArrMap⦈⦇f⦈ : ?Δ⦇ObjMap⦈⦇a⦈ ↦⇘?FUNCT⇙ ?Δ⦇ObjMap⦈⦇b⦈"
      if "f : a ↦⇘ℭ⇙ b" for f a b
      using that
      by 
        (
          cs_concl  
            cs_simp: cat_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_small_cs_intros
        )
    show "?Δ⦇ArrMap⦈⦇g ∘⇩A⇘ℭ⇙ f⦈ = ?Δ⦇ArrMap⦈⦇g⦈ ∘⇩A⇘?FUNCT⇙ ?Δ⦇ArrMap⦈⦇f⦈"
      if "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b" for g b c f a
      using that 𝔍.category_axioms ℭ.category_axioms
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    fix c assume "c ∈⇩∘ ℭ⦇Obj⦈"
    with 𝔍.category_axioms ℭ.category_axioms show 
      "?Δ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ = ?FUNCT⦇CId⦈⦇?Δ⦇ObjMap⦈⦇c⦈⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
  qed (auto simp: cf_diagonal_components cat_smc_FUNCT)

qed

lemma cf_diagonal_is_functor'[cat_cs_intros]:
  assumes "𝒵 β" 
    and "α ∈⇩∘ β"
    and "category α 𝔍" 
    and "category α ℭ"
    and "𝔄' = ℭ"
    and "𝔅' = cat_FUNCT α 𝔍 ℭ"
  shows "Δ⇩C⇩F α 𝔍 ℭ : 𝔄' ↦↦⇩C⇘β⇙ 𝔅'"
  using assms(1-4) unfolding assms(5-6) by (rule cf_diagonal_is_functor)



(*TODO: functor codomain substitution*)
subsection‹Diagonal functor for functors with tiny maps›


subsubsection‹Definition and elementary properties›


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

definition tm_cf_diagonal :: "V ⇒ V ⇒ V ⇒ V" (‹Δ⇩C⇩F⇩.⇩t⇩m›) 
  where "Δ⇩C⇩F⇩.⇩t⇩m α 𝔍 ℭ =
    [
      (λa∈⇩∘ℭ⦇Obj⦈. cf_map (cf_const 𝔍 ℭ a)),
      (λf∈⇩∘ℭ⦇Arr⦈. ntcf_arrow (ntcf_const 𝔍 ℭ f)), 
      ℭ,
      cat_Funct α 𝔍 ℭ
    ]⇩∘"


text‹Components.›

lemma tm_cf_diagonal_components:
  shows "Δ⇩C⇩F⇩.⇩t⇩m α 𝔍 ℭ⦇ObjMap⦈ = (λa∈⇩∘ℭ⦇Obj⦈. cf_map (cf_const 𝔍 ℭ a))"
    and "Δ⇩C⇩F⇩.⇩t⇩m α 𝔍 ℭ⦇ArrMap⦈ = (λf∈⇩∘ℭ⦇Arr⦈. ntcf_arrow (ntcf_const 𝔍 ℭ f))"
    and "Δ⇩C⇩F⇩.⇩t⇩m α 𝔍 ℭ⦇HomDom⦈ = ℭ"
    and "Δ⇩C⇩F⇩.⇩t⇩m α 𝔍 ℭ⦇HomCod⦈ = cat_Funct α 𝔍 ℭ"
  unfolding tm_cf_diagonal_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda tm_cf_diagonal_components(1)
  |vsv tm_cf_diagonal_ObjMap_vsv[cat_cs_intros]|
  |vdomain tm_cf_diagonal_ObjMap_vdomain[cat_cs_simps]|
  |app tm_cf_diagonal_ObjMap_app[cat_cs_simps]|

lemma tm_cf_diagonal_ObjMap_vrange:
  assumes "tiny_category α 𝔍" and "category α ℭ"
  shows "ℛ⇩∘ (Δ⇩C⇩F⇩.⇩t⇩m α 𝔍 ℭ⦇ObjMap⦈) ⊆⇩∘ cat_Funct α 𝔍 ℭ⦇Obj⦈"
  unfolding tm_cf_diagonal_components 
proof(rule vrange_VLambda_vsubset)
  fix x assume "x ∈⇩∘ ℭ⦇Obj⦈" 
  with assms category_cat_Funct[OF assms] show 
    "cf_map (cf_const 𝔍 ℭ x) ∈⇩∘ cat_Funct α 𝔍 ℭ⦇Obj⦈"
    unfolding cat_Funct_components(1)
    by (cs_concl cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros)
qed


subsubsection‹Arrow map›

mk_VLambda tm_cf_diagonal_components(2)
  |vsv tm_cf_diagonal_ArrMap_vsv[cat_cs_intros]|
  |vdomain tm_cf_diagonal_ArrMap_vdomain[cat_cs_simps]|
  |app tm_cf_diagonal_ArrMap_app[cat_cs_simps]|


subsubsection‹Diagonal functor for functors with tiny maps is a functor›

lemma tm_cf_diagonal_is_functor[cat_cs_intros]:
  assumes "tiny_category α 𝔍" and "category α ℭ"
  shows "Δ⇩C⇩F⇩.⇩t⇩m α 𝔍 ℭ : ℭ ↦↦⇩C⇘α⇙ cat_Funct α 𝔍 ℭ" 
    (is ‹?Δ : ℭ ↦↦⇩C⇘α⇙ ?Funct›)
proof-

  interpret 𝔍: tiny_category α 𝔍 by (rule assms(1))
  interpret ℭ: category α ℭ by (rule assms(2))

  show ?thesis
  proof(intro is_functorI')
    show "vfsequence ?Δ"
      unfolding tm_cf_diagonal_def by (simp add: nat_omega_simps)
    from assms(2) show "category α ℭ" 
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    from assms show "category α ?Funct" 
      by (cs_concl cs_shallow cs_intro: cat_cs_intros category_cat_Funct)
    show "vcard ?Δ = 4⇩ℕ"
      unfolding tm_cf_diagonal_def by (simp add: nat_omega_simps)
    show "vsv (?Δ⦇ObjMap⦈)" unfolding tm_cf_diagonal_components by simp
    from assms show "ℛ⇩∘ (?Δ⦇ObjMap⦈) ⊆⇩∘ ?Funct⦇Obj⦈"
      by (rule tm_cf_diagonal_ObjMap_vrange)
    show "?Δ⦇ArrMap⦈⦇f⦈ : ?Δ⦇ObjMap⦈⦇a⦈ ↦⇘?Funct⇙ ?Δ⦇ObjMap⦈⦇b⦈"
      if "f : a ↦⇘ℭ⇙ b" for f a b
      using that
      by 
        (
          cs_concl  
            cs_simp: cat_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_small_cs_intros
        )
    show "?Δ⦇ArrMap⦈⦇g ∘⇩A⇘ℭ⇙ f⦈ = ?Δ⦇ArrMap⦈⦇g⦈ ∘⇩A⇘?Funct⇙ ?Δ⦇ArrMap⦈⦇f⦈"
      if "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b" for g b c f a
      using that 𝔍.category_axioms ℭ.category_axioms
      by 
        (
          cs_concl  
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    fix c assume "c ∈⇩∘ ℭ⦇Obj⦈"
    with 𝔍.category_axioms ℭ.category_axioms show 
      "?Δ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ = ?Funct⦇CId⦈⦇?Δ⦇ObjMap⦈⦇c⦈⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
  qed (auto simp: tm_cf_diagonal_components cat_smc_FUNCT)

qed

lemma tm_cf_diagonal_is_functor'[cat_cs_intros]:
  assumes "tiny_category α 𝔍" 
    and "category α ℭ"
    and "α' = α"
    and "𝔄 = ℭ"
    and "𝔅 = cat_Funct α 𝔍 ℭ"
  shows "Δ⇩C⇩F⇩.⇩t⇩m α 𝔍 ℭ : 𝔄 ↦↦⇩C⇘α'⇙ 𝔅"
  using assms(1-2) unfolding assms(3-5) by (rule tm_cf_diagonal_is_functor)



subsection‹Functor raised to the power of a category›


subsubsection‹Definition and elementary properties›


text‹
Most of the definitions and the results presented in this 
and the remaining subsections
can be found in \<^cite>‹"mac_lane_categories_2010"› and 
\<^cite>‹"riehl_category_2016"› (e.g., see Chapter X-3 
in \<^cite>‹"mac_lane_categories_2010"›).
›

definition exp_cf_cat :: "V ⇒ V ⇒ V ⇒ V"
  where "exp_cf_cat α 𝔎 𝔄 =
    [
      (
        λ𝔖∈⇩∘cat_FUNCT α 𝔄 (𝔎⦇HomDom⦈)⦇Obj⦈.
          cf_map (𝔎 ∘⇩C⇩F cf_of_cf_map 𝔄 (𝔎⦇HomDom⦈) 𝔖)
      ),
      (
        λσ∈⇩∘cat_FUNCT α 𝔄 (𝔎⦇HomDom⦈)⦇Arr⦈.
          ntcf_arrow (𝔎 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_of_ntcf_arrow 𝔄 (𝔎⦇HomDom⦈) σ)
      ),
      cat_FUNCT α 𝔄 (𝔎⦇HomDom⦈),
      cat_FUNCT α 𝔄 (𝔎⦇HomCod⦈)
    ]⇩∘"


text‹Components.›

lemma exp_cf_cat_components:
  shows "exp_cf_cat α 𝔎 𝔄⦇ObjMap⦈ = 
    (
      λ𝔖∈⇩∘cat_FUNCT α 𝔄 (𝔎⦇HomDom⦈)⦇Obj⦈.
        cf_map (𝔎 ∘⇩C⇩F cf_of_cf_map 𝔄 (𝔎⦇HomDom⦈) 𝔖)
    )"
    and 
    "exp_cf_cat α 𝔎 𝔄⦇ArrMap⦈ =
      (
        λσ∈⇩∘cat_FUNCT α 𝔄 (𝔎⦇HomDom⦈)⦇Arr⦈.
          ntcf_arrow  (𝔎 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F (ntcf_of_ntcf_arrow 𝔄 (𝔎⦇HomDom⦈) σ))
      )"
    and "exp_cf_cat α 𝔎 𝔄⦇HomDom⦈ = cat_FUNCT α 𝔄 (𝔎⦇HomDom⦈)"
    and "exp_cf_cat α 𝔎 𝔄⦇HomCod⦈ = cat_FUNCT α 𝔄 (𝔎⦇HomCod⦈)"
  unfolding exp_cf_cat_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda exp_cf_cat_components(1)
  |vsv exp_cf_cat_components_ObjMap_vsv[cat_FUNCT_cs_intros]|

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

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

mk_VLambda exp_cf_cat_components(1)[where 𝔎=𝔎 and α=α, unfolded cat_cs_simps]
  |vdomain exp_cf_cat_components_ObjMap_vdomain[cat_FUNCT_cs_simps]|
  |app exp_cf_cat_components_ObjMap_app[cat_FUNCT_cs_simps]|

end


subsubsection‹Arrow map›

mk_VLambda exp_cf_cat_components(2)
  |vsv exp_cf_cat_components_ArrMap_vsv[cat_FUNCT_cs_intros]|

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

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

mk_VLambda exp_cf_cat_components(2)[where 𝔎=𝔎 and α=α, unfolded cat_cs_simps]
  |vdomain exp_cf_cat_components_ArrMap_vdomain[cat_FUNCT_cs_simps]|
  |app exp_cf_cat_components_ArrMap_app[cat_FUNCT_cs_simps]|

end


subsubsection‹Domain and codomain›

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

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

lemmas exp_cf_cat_HomDom[cat_FUNCT_cs_simps] = 
    exp_cf_cat_components(3)[where 𝔎=𝔎 and α=α, unfolded cat_cs_simps]
  and exp_cf_cat_HomCod[cat_FUNCT_cs_simps] = 
    exp_cf_cat_components(4)[where 𝔎=𝔎 and α=α, unfolded cat_cs_simps]

end


subsubsection‹Functor raised to the power of a category is a functor›

lemma exp_cf_cat_is_tiny_functor: 
  assumes "𝒵 β" and "α ∈⇩∘ β" and "category α 𝔄" and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "exp_cf_cat α 𝔎 𝔄 : cat_FUNCT α 𝔄 𝔅 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ cat_FUNCT α 𝔄 ℭ"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  interpret 𝔄: category α 𝔄 by (rule assms(3))
  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(4))
  from assms(2-4) interpret 𝔄𝔅: tiny_category β ‹cat_FUNCT α 𝔄 𝔅›
    by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
  from assms(2-4) interpret 𝔄ℭ: tiny_category β ‹cat_FUNCT α 𝔄 ℭ›
    by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
  show ?thesis
  proof(intro is_tiny_functorI' is_functorI')
    show "vfsequence (exp_cf_cat α 𝔎 𝔄)" unfolding exp_cf_cat_def by simp
    show "vcard (exp_cf_cat α 𝔎 𝔄) = 4⇩ℕ"
      unfolding exp_cf_cat_def by (simp add: nat_omega_simps)
    show "ℛ⇩∘ (exp_cf_cat α 𝔎 𝔄⦇ObjMap⦈) ⊆⇩∘ cat_FUNCT α 𝔄 ℭ⦇Obj⦈"
    proof
      (
        unfold cat_FUNCT_components exp_cf_cat_components, 
        intro vrange_VLambda_vsubset, 
        unfold cat_cs_simps
      )
      fix 𝔉 assume "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅"
      then obtain 𝔉' where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉': "𝔉' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
        by auto
      from assms(2-4) 𝔉' show 
        "cf_map (𝔎 ∘⇩C⇩F cf_of_cf_map 𝔄 𝔅 𝔉) ∈⇩∘ cf_maps α 𝔄 ℭ"
        by (cs_concl cs_simp: 𝔉_def cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
    qed
    show "exp_cf_cat α 𝔎 𝔄⦇ArrMap⦈⦇𝔑⦈ :
      exp_cf_cat α 𝔎 𝔄⦇ObjMap⦈⦇𝔉⦈ ↦⇘cat_FUNCT α 𝔄 ℭ⇙
      exp_cf_cat α 𝔎 𝔄⦇ObjMap⦈⦇𝔊⦈"
      if "𝔑 : 𝔉 ↦⇘cat_FUNCT α 𝔄 𝔅⇙ 𝔊" for 𝔉 𝔊 𝔑
    proof-
      note 𝔑 = cat_FUNCT_is_arrD[OF that]
      from 𝔑(1,3,4) assms(2-4) show ?thesis
      by (subst 𝔑(2), use nothing in ‹subst 𝔑(3), subst 𝔑(4)›) 
        (
          cs_concl  
            cs_simp: cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    qed
    show 
      "exp_cf_cat α 𝔎 𝔄⦇ArrMap⦈⦇𝔐 ∘⇩A⇘cat_FUNCT α 𝔄 𝔅⇙ 𝔑⦈ =
        exp_cf_cat α 𝔎 𝔄⦇ArrMap⦈⦇𝔐⦈ ∘⇩A⇘cat_FUNCT α 𝔄 ℭ⇙
        exp_cf_cat α 𝔎 𝔄⦇ArrMap⦈⦇𝔑⦈"
      if "𝔐 : 𝔊 ↦⇘cat_FUNCT α 𝔄 𝔅⇙ ℌ" and "𝔑 : 𝔉 ↦⇘cat_FUNCT α 𝔄 𝔅⇙ 𝔊"
      for 𝔊 ℌ 𝔐 𝔉 𝔑
    proof-
      note 𝔐 = cat_FUNCT_is_arrD[OF that(1)]
        and 𝔑 = cat_FUNCT_is_arrD[OF that(2)]  
      from 𝔐(1,3,4) 𝔑(1,3,4) assms(2-4) show ?thesis  
        by (subst (1 2) 𝔐(2), use nothing in ‹subst (1 2) 𝔑(2)›)
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps cf_ntcf_comp_ntcf_vcomp 
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed
    show 
      "exp_cf_cat α 𝔎 𝔄⦇ArrMap⦈⦇cat_FUNCT α 𝔄 𝔅⦇CId⦈⦇𝔉⦈⦈ =
        cat_FUNCT α 𝔄 ℭ⦇CId⦈⦇exp_cf_cat α 𝔎 𝔄⦇ObjMap⦈⦇𝔉⦈⦈"
      if "𝔉 ∈⇩∘ cat_FUNCT α 𝔄 𝔅⦇Obj⦈" for 𝔉
    proof-
      from that[unfolded cat_FUNCT_components] obtain 𝔊 
        where 𝔉_def: "𝔉 = cf_map 𝔊" and 𝔊: "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
        by auto
      from 𝔊 show
        "exp_cf_cat α 𝔎 𝔄⦇ArrMap⦈⦇cat_FUNCT α 𝔄 𝔅⦇CId⦈⦇𝔉⦈⦈ =
          cat_FUNCT α 𝔄 ℭ⦇CId⦈⦇exp_cf_cat α 𝔎 𝔄⦇ObjMap⦈⦇𝔉⦈⦈" 
        by 
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 𝔉_def
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed
  qed 
    (
      use assms(1,2) in
        ‹
          cs_concl cs_shallow
            cs_simp: cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        ›
    )+
qed

lemma exp_cf_cat_is_tiny_functor'[cat_FUNCT_cs_intros]:
  assumes "𝒵 β" 
    and "α ∈⇩∘ β" 
    and "category α 𝔄" 
    and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔄' = cat_FUNCT α 𝔄 𝔅"
    and "𝔅' = cat_FUNCT α 𝔄 ℭ"
  shows "exp_cf_cat α 𝔎 𝔄 : 𝔄' ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ 𝔅'"
  using assms(1-4) unfolding assms(5,6) by (rule exp_cf_cat_is_tiny_functor)


subsubsection‹Further properties›

lemma exp_cf_cat_cf_comp:
  assumes "category α 𝔇" and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "exp_cf_cat α (𝔊 ∘⇩C⇩F 𝔉) 𝔇 = exp_cf_cat α 𝔊 𝔇 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔇"
proof(rule cf_eqI)

  interpret 𝔇: category α 𝔇 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))
  interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(3))

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

  from αβ show 
    "exp_cf_cat α (𝔊 ∘⇩C⇩F 𝔉) 𝔇 : cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔇 ℭ"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  from αβ show 
    "exp_cf_cat α 𝔊 𝔇 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔇 : 
      cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔇 ℭ"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  from αβ have dom_lhs:
    "𝒟⇩∘ (exp_cf_cat α (𝔊 ∘⇩C⇩F 𝔉) 𝔇⦇ObjMap⦈) = cat_FUNCT α 𝔇 𝔄⦇Obj⦈"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  from αβ have dom_rhs: 
    "𝒟⇩∘ ((exp_cf_cat α 𝔊 𝔇 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔇)⦇ObjMap⦈) = 
      cat_FUNCT α 𝔇 𝔄⦇Obj⦈"
    by
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  show 
    "exp_cf_cat α (𝔊 ∘⇩C⇩F 𝔉) 𝔇⦇ObjMap⦈ =
      (exp_cf_cat α 𝔊 𝔇 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔇)⦇ObjMap⦈"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    show "vsv (exp_cf_cat α (𝔊 ∘⇩C⇩F 𝔉) 𝔇⦇ObjMap⦈)"
      by (cs_concl cs_shallow cs_intro: cat_FUNCT_cs_intros)
    from αβ show "vsv ((exp_cf_cat α 𝔊 𝔇 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔇)⦇ObjMap⦈)"
      by 
        (
          cs_concl cs_intro: 
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    fix ℌ assume "ℌ ∈⇩∘ cat_FUNCT α 𝔇 𝔄⦇Obj⦈"
    then have "ℌ ∈⇩∘ cf_maps α 𝔇 𝔄" unfolding cat_FUNCT_components by simp
    then obtain ℌ' where ℌ_def: "ℌ = cf_map ℌ'" and ℌ': "ℌ' : 𝔇 ↦↦⇩C⇘α⇙ 𝔄" 
      by auto
    from assms αβ ℌ' show 
      "exp_cf_cat α (𝔊 ∘⇩C⇩F 𝔉) 𝔇⦇ObjMap⦈⦇ℌ⦈ =
        (exp_cf_cat α 𝔊 𝔇 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔇)⦇ObjMap⦈⦇ℌ⦈"
      by (subst (1 2) ℌ_def)
        (
          cs_concl  
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
  qed simp
  from αβ have dom_lhs:
    "𝒟⇩∘ (exp_cf_cat α (𝔊 ∘⇩C⇩F 𝔉) 𝔇⦇ArrMap⦈) = cat_FUNCT α 𝔇 𝔄⦇Arr⦈"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  from αβ have dom_rhs: 
    "𝒟⇩∘ ((exp_cf_cat α 𝔊 𝔇 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔇)⦇ArrMap⦈) =
      cat_FUNCT α 𝔇 𝔄⦇Arr⦈"
    by
      (
        cs_concl  
          cs_simp: cat_cs_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  show 
    "exp_cf_cat α (𝔊 ∘⇩C⇩F 𝔉) 𝔇⦇ArrMap⦈ =
      (exp_cf_cat α 𝔊 𝔇 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔇)⦇ArrMap⦈"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    show "vsv (exp_cf_cat α (𝔊 ∘⇩C⇩F 𝔉) 𝔇⦇ArrMap⦈)"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_FUNCT_cs_intros)
    from αβ show "vsv ((exp_cf_cat α 𝔊 𝔇 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔇)⦇ArrMap⦈)"
      by 
        (
          cs_concl cs_intro:
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )                           
    fix 𝔑 assume "𝔑 ∈⇩∘ cat_FUNCT α 𝔇 𝔄⦇Arr⦈"
    then obtain ℌ ℌ' where 𝔑: "𝔑 : ℌ ↦⇘cat_FUNCT α 𝔇 𝔄⇙ ℌ'" 
      by (auto intro: is_arrI)
    note 𝔑 = cat_FUNCT_is_arrD[OF 𝔑]
    from αβ assms 𝔑(1,3,4) show 
      "exp_cf_cat α (𝔊 ∘⇩C⇩F 𝔉) 𝔇⦇ArrMap⦈⦇𝔑⦈ =
        (exp_cf_cat α 𝔊 𝔇 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔇)⦇ArrMap⦈⦇𝔑⦈"
      by (subst (1 2) 𝔑(2))
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps cf_comp_cf_ntcf_comp_assoc
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
  qed simp
qed simp_all

lemma exp_cf_cat_cf_id_cat:
  assumes "category α ℭ" and "category α 𝔇"
  shows "exp_cf_cat α (cf_id ℭ) 𝔇 = cf_id (cat_FUNCT α 𝔇 ℭ)"
proof(rule cf_eqI)

  interpret ℭ: category α ℭ by (rule assms)
  interpret 𝔇: category α 𝔇 by (rule assms)

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

  from αβ show
    "cf_id (cat_FUNCT α 𝔇 ℭ) : cat_FUNCT α 𝔇 ℭ ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔇 ℭ"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
      )
  from αβ show
    "exp_cf_cat α (cf_id ℭ) 𝔇 : cat_FUNCT α 𝔇 ℭ ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔇 ℭ"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
      )
  from αβ have ObjMap_dom_lhs:
    "𝒟⇩∘ (exp_cf_cat α (cf_id ℭ) 𝔇⦇ObjMap⦈) = cat_FUNCT α 𝔇 ℭ⦇Obj⦈"
    by (cs_concl cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros)
  from αβ have ObjMap_dom_rhs:
    "𝒟⇩∘ (cf_id (cat_FUNCT α 𝔇 ℭ)⦇ObjMap⦈) = cat_FUNCT α 𝔇 ℭ⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  show "exp_cf_cat α (cf_id ℭ) 𝔇⦇ObjMap⦈ = cf_id (cat_FUNCT α 𝔇 ℭ)⦇ObjMap⦈"
  proof
    (
      rule vsv_eqI, 
      unfold ObjMap_dom_lhs ObjMap_dom_rhs cat_FUNCT_components(1)
    )
    fix ℌ assume prems: "ℌ ∈⇩∘ cf_maps α 𝔇 ℭ"
    then obtain ℌ' where ℌ_def: "ℌ = cf_map ℌ'" and ℌ': "ℌ' : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
      by clarsimp
    from prems ℌ' show 
      "exp_cf_cat α (cf_id ℭ) 𝔇⦇ObjMap⦈⦇ℌ⦈ = cf_id (cat_FUNCT α 𝔇 ℭ)⦇ObjMap⦈⦇ℌ⦈"
      by (subst (1 2) ℌ_def)
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
  qed (cs_concl cs_shallow cs_intro: cat_cs_intros cat_FUNCT_cs_intros)+
  from αβ have ArrMap_dom_lhs:
    "𝒟⇩∘ (cf_id (cat_FUNCT α 𝔇 ℭ)⦇ArrMap⦈) = cat_FUNCT α 𝔇 ℭ⦇Arr⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  from αβ have ArrMap_dom_rhs:
    "𝒟⇩∘ (exp_cf_cat α (cf_id ℭ) 𝔇⦇ArrMap⦈) = cat_FUNCT α 𝔇 ℭ⦇Arr⦈"
    by (cs_concl cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros)
  show "exp_cf_cat α (cf_id ℭ) 𝔇⦇ArrMap⦈ = cf_id (cat_FUNCT α 𝔇 ℭ)⦇ArrMap⦈"
  proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
    fix 𝔑 assume "𝔑 ∈⇩∘ cat_FUNCT α 𝔇 ℭ⦇Arr⦈"
    then obtain 𝔉 𝔊 where 𝔑: "𝔑 : 𝔉 ↦⇘cat_FUNCT α 𝔇 ℭ⇙ 𝔊" 
      by (auto intro: is_arrI)
    note 𝔑 = cat_FUNCT_is_arrD[OF 𝔑]
    from 𝔑(1,3,4) αβ show 
      "exp_cf_cat α (cf_id ℭ) 𝔇⦇ArrMap⦈⦇𝔑⦈ =
        cf_id (cat_FUNCT α 𝔇 ℭ)⦇ArrMap⦈⦇𝔑⦈"
      by (subst (1 2) 𝔑(2))
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
  qed (cs_concl cs_shallow cs_intro: cat_cs_intros cat_FUNCT_cs_intros)

qed simp_all


lemma cf_comp_exp_cf_cat_exp_cf_cat_cf_id[cat_FUNCT_cs_simps]:
  assumes "category α 𝔄" and "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "exp_cf_cat α 𝔉 𝔄 ∘⇩C⇩F exp_cf_cat α (cf_id 𝔅) 𝔄 = exp_cf_cat α 𝔉 𝔄"
proof-

  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔉: is_functor α 𝔅 ℭ 𝔉 by (rule assms(2))

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

  show ?thesis
  proof(rule cf_eqI)
    from assms αβ β show 𝔉𝔄:
      "exp_cf_cat α 𝔉 𝔄 : cat_FUNCT α 𝔄 𝔅 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
      by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros)
    with assms αβ show 
      "exp_cf_cat α 𝔉 𝔄 ∘⇩C⇩F exp_cf_cat α (cf_id 𝔅) 𝔄 :
        cat_FUNCT α 𝔄 𝔅 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
      by 
        (
          cs_concl cs_intro: 
            cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from assms αβ have ObjMap_dom_lhs:
      "𝒟⇩∘ ((exp_cf_cat α 𝔉 𝔄 ∘⇩C⇩F exp_cf_cat α (cf_id 𝔅) 𝔄)⦇ObjMap⦈) =
        cat_FUNCT α 𝔄 𝔅⦇Obj⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from assms have ObjMap_dom_rhs: 
      "𝒟⇩∘ (exp_cf_cat α 𝔉 𝔄⦇ObjMap⦈) = cat_FUNCT α 𝔄 𝔅⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_FUNCT_cs_simps)
    from assms αβ have ArrMap_dom_lhs:
      "𝒟⇩∘ ((exp_cf_cat α 𝔉 𝔄 ∘⇩C⇩F exp_cf_cat α (cf_id 𝔅) 𝔄)⦇ArrMap⦈) =
        cat_FUNCT α 𝔄 𝔅⦇Arr⦈"
      by
        (
          cs_concl 
            cs_simp: cat_cs_simps
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from assms have ArrMap_dom_rhs: 
      "𝒟⇩∘ (exp_cf_cat α 𝔉 𝔄⦇ArrMap⦈) = cat_FUNCT α 𝔄 𝔅⦇Arr⦈"
      by (cs_concl cs_shallow cs_simp: cat_FUNCT_cs_simps)
    show 
      "(exp_cf_cat α 𝔉 𝔄 ∘⇩C⇩F exp_cf_cat α (cf_id 𝔅) 𝔄)⦇ObjMap⦈ =
        exp_cf_cat α 𝔉 𝔄⦇ObjMap⦈"
    proof
      (
        rule vsv_eqI,
        unfold ObjMap_dom_lhs ObjMap_dom_rhs cat_FUNCT_components(1)
      )
      fix ℌ assume prems: "ℌ ∈⇩∘ cf_maps α 𝔄 𝔅"
      then obtain ℌ' where ℌ_def: "ℌ = cf_map ℌ'" and ℌ': "ℌ' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
        by clarsimp
      from prems ℌ' assms 𝔉𝔄 αβ show 
        "(exp_cf_cat α 𝔉 𝔄 ∘⇩C⇩F exp_cf_cat α (cf_id 𝔅) 𝔄)⦇ObjMap⦈⦇ℌ⦈ =
          exp_cf_cat α 𝔉 𝔄⦇ObjMap⦈⦇ℌ⦈"
        unfolding ℌ_def
        by 
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps
              cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros cat_cs_intros
          )
    qed 
      (
        use assms 𝔉𝔄 αβ in
          ‹
            cs_concl 
              cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros cat_cs_intros
          ›
      )
    show 
      "(exp_cf_cat α 𝔉 𝔄 ∘⇩C⇩F exp_cf_cat α (cf_id 𝔅) 𝔄)⦇ArrMap⦈ =
        exp_cf_cat α 𝔉 𝔄⦇ArrMap⦈"
    proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      fix 𝔐 assume "𝔐 ∈⇩∘ cat_FUNCT α 𝔄 𝔅⦇Arr⦈"
      then obtain 𝔉' 𝔊' where 𝔐: "𝔐 : 𝔉' ↦⇘cat_FUNCT α 𝔄 𝔅⇙ 𝔊'"
        by (auto intro: is_arrI)
      note 𝔐 = cat_FUNCT_is_arrD[OF 𝔐]
      from 𝔐(1) assms 𝔉𝔄 αβ show 
        "(exp_cf_cat α 𝔉 𝔄 ∘⇩C⇩F exp_cf_cat α (cf_id 𝔅) 𝔄)⦇ArrMap⦈⦇𝔐⦈ =
          exp_cf_cat α 𝔉 𝔄⦇ArrMap⦈⦇𝔐⦈"
        by (subst (1 2) 𝔐(2))
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps
              cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros cat_cs_intros
          )
    qed
      (
        use assms αβ in 
          ‹
            cs_concl cs_intro:
              cat_FUNCT_cs_intros cat_small_cs_intros cat_cs_intros
          ›
      )
  qed simp_all

qed

lemma cf_comp_exp_cf_cat_cf_id_exp_cf_cat[cat_FUNCT_cs_simps]:
  assumes "category α 𝔄" and "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "exp_cf_cat α (cf_id ℭ) 𝔄 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔄 = exp_cf_cat α 𝔉 𝔄"
proof-

  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔉: is_functor α 𝔅 ℭ 𝔉 by (rule assms(2))

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

  show ?thesis
  proof(rule cf_eqI)
    from assms αβ β show 𝔉𝔄:
      "exp_cf_cat α 𝔉 𝔄 : cat_FUNCT α 𝔄 𝔅 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
      by (cs_concl cs_simp: cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros)
    with assms αβ show 
      "exp_cf_cat α (cf_id ℭ) 𝔄 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔄 :
        cat_FUNCT α 𝔄 𝔅 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
      by 
        (
          cs_concl cs_intro: 
            cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from assms αβ have ObjMap_dom_lhs:
      "𝒟⇩∘ ((exp_cf_cat α (cf_id ℭ) 𝔄 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔄)⦇ObjMap⦈) =
        cat_FUNCT α 𝔄 𝔅⦇Obj⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from assms have ObjMap_dom_rhs: 
      "𝒟⇩∘ (exp_cf_cat α 𝔉 𝔄⦇ObjMap⦈) = cat_FUNCT α 𝔄 𝔅⦇Obj⦈"
      by (cs_concl cs_simp: cat_FUNCT_cs_simps)
    from assms αβ have ArrMap_dom_lhs:
      "𝒟⇩∘ ((exp_cf_cat α (cf_id ℭ) 𝔄 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔄)⦇ArrMap⦈) =
        cat_FUNCT α 𝔄 𝔅⦇Arr⦈"
      by
        (
          cs_concl 
            cs_simp: cat_cs_simps
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from assms have ArrMap_dom_rhs: 
      "𝒟⇩∘ (exp_cf_cat α 𝔉 𝔄⦇ArrMap⦈) = cat_FUNCT α 𝔄 𝔅⦇Arr⦈"
      by (cs_concl cs_simp: cat_FUNCT_cs_simps)
    show 
      "(exp_cf_cat α (cf_id ℭ) 𝔄 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔄)⦇ObjMap⦈ =
        exp_cf_cat α 𝔉 𝔄⦇ObjMap⦈"
    proof
      (
        rule vsv_eqI, 
        unfold ObjMap_dom_lhs ObjMap_dom_rhs cat_FUNCT_components(1)
      )
      fix ℌ assume prems: "ℌ ∈⇩∘ cf_maps α 𝔄 𝔅"
      then obtain ℌ' where ℌ_def: "ℌ = cf_map ℌ'" and ℌ': "ℌ' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
        by clarsimp
      from prems ℌ' assms αβ 𝔉𝔄 show 
        "(exp_cf_cat α (cf_id ℭ) 𝔄 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔄)⦇ObjMap⦈⦇ℌ⦈ =
          exp_cf_cat α 𝔉 𝔄⦇ObjMap⦈⦇ℌ⦈"
        unfolding ℌ_def
        by 
          (
            cs_concl
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros cat_cs_intros
          )
    qed 
      (
        use assms αβ 𝔉𝔄 in 
          ‹
            cs_concl
              cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros cat_cs_intros
          ›
      )
    show 
      "(exp_cf_cat α (cf_id ℭ) 𝔄 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔄)⦇ArrMap⦈ =
        exp_cf_cat α 𝔉 𝔄⦇ArrMap⦈"
    proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      fix 𝔐 assume "𝔐 ∈⇩∘ cat_FUNCT α 𝔄 𝔅⦇Arr⦈"
      then obtain 𝔉' 𝔊' where 𝔐: "𝔐 : 𝔉' ↦⇘cat_FUNCT α 𝔄 𝔅⇙ 𝔊'"
        by (auto intro: is_arrI)
      note 𝔐 = cat_FUNCT_is_arrD[OF 𝔐]
      from 𝔐(1) assms αβ 𝔉𝔄 show 
        "(exp_cf_cat α (cf_id ℭ) 𝔄 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔄)⦇ArrMap⦈⦇𝔐⦈ =
          exp_cf_cat α 𝔉 𝔄⦇ArrMap⦈⦇𝔐⦈"
        by (subst (1 2) 𝔐(2))
          (
            cs_concl
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps
              cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros cat_cs_intros
          )
    qed
      (
        use assms αβ in
          ‹
            cs_concl
              cs_intro: cat_FUNCT_cs_intros cat_small_cs_intros cat_cs_intros
          ›
      )
  qed simp_all

qed



subsection‹Category raised to the power of a functor›


subsubsection‹Definition and elementary properties›

definition exp_cat_cf :: "V ⇒ V ⇒ V ⇒ V"
  where "exp_cat_cf α 𝔄 𝔎 =
    [
      (
        λ𝔖∈⇩∘cat_FUNCT α (𝔎⦇HomCod⦈) 𝔄⦇Obj⦈.
          cf_map (cf_of_cf_map (𝔎⦇HomCod⦈) 𝔄 𝔖 ∘⇩C⇩F 𝔎)
      ),
      (
        λσ∈⇩∘cat_FUNCT α (𝔎⦇HomCod⦈) 𝔄⦇Arr⦈.
          ntcf_arrow (ntcf_of_ntcf_arrow (𝔎⦇HomCod⦈) 𝔄 σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎)
      ),
      cat_FUNCT α (𝔎⦇HomCod⦈) 𝔄,
      cat_FUNCT α (𝔎⦇HomDom⦈) 𝔄 
    ]⇩∘"


text‹Components.›

lemma exp_cat_cf_components:
  shows "exp_cat_cf α 𝔄 𝔎⦇ObjMap⦈ =
    (
      λ𝔖∈⇩∘cat_FUNCT α (𝔎⦇HomCod⦈) 𝔄⦇Obj⦈.
        cf_map (cf_of_cf_map (𝔎⦇HomCod⦈) 𝔄 𝔖 ∘⇩C⇩F 𝔎)
    )"
    and "exp_cat_cf α 𝔄 𝔎⦇ArrMap⦈ = 
    (
      λσ∈⇩∘cat_FUNCT α (𝔎⦇HomCod⦈) 𝔄⦇Arr⦈.
        ntcf_arrow (ntcf_of_ntcf_arrow (𝔎⦇HomCod⦈) 𝔄 σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎)
    )"
    and "exp_cat_cf α 𝔄 𝔎⦇HomDom⦈ = cat_FUNCT α (𝔎⦇HomCod⦈) 𝔄"
    and "exp_cat_cf α 𝔄 𝔎⦇HomCod⦈ = cat_FUNCT α (𝔎⦇HomDom⦈) 𝔄"
  unfolding exp_cat_cf_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

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

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

mk_VLambda exp_cat_cf_components(1)[where 𝔎=𝔎 and α=α, unfolded cat_cs_simps]
  |vsv exp_cat_cf_components_ObjMap_vsv[cat_FUNCT_cs_intros]|
  |vdomain exp_cat_cf_components_ObjMap_vdomain[cat_FUNCT_cs_simps]|
  |app exp_cat_cf_components_ObjMap_app[cat_FUNCT_cs_simps]|

end


subsubsection‹Arrow map›

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

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

mk_VLambda exp_cat_cf_components(2)[where 𝔎=𝔎 and α=α, unfolded cat_cs_simps]
  |vsv exp_cat_cf_components_ArrMap_vsv[cat_FUNCT_cs_intros]|
  |vdomain exp_cat_cf_components_ArrMap_vdomain[cat_FUNCT_cs_simps]|
  |app exp_cat_cf_components_ArrMap_app[cat_FUNCT_cs_simps]|

end


subsubsection‹Domain and codomain›

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

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

lemmas exp_cat_cf_HomDom[cat_FUNCT_cs_simps] = 
    exp_cat_cf_components(3)[where 𝔎=𝔎 and α=α, unfolded cat_cs_simps]
  and exp_cat_cf_HomCod[cat_FUNCT_cs_simps] = 
    exp_cat_cf_components(4)[where 𝔎=𝔎 and α=α, unfolded cat_cs_simps]

end


subsubsection‹Category raised to the power of a functor is a functor›

lemma exp_cat_cf_is_tiny_functor: 
  assumes "𝒵 β" and "α ∈⇩∘ β" and "category α 𝔄" and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "exp_cat_cf α 𝔄 𝔎 : cat_FUNCT α ℭ 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ cat_FUNCT α 𝔅 𝔄"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  interpret 𝔄: category α 𝔄 by (rule assms(3))
  interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(4))
  from assms(2-4) interpret ℭ𝔄: tiny_category β ‹cat_FUNCT α ℭ 𝔄›
    by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
  from assms(2-4) interpret 𝔅𝔄: tiny_category β ‹cat_FUNCT α 𝔅 𝔄›
    by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
  show ?thesis
  proof(intro is_tiny_functorI' is_functorI')
    show "vfsequence (exp_cat_cf α 𝔄 𝔎)" unfolding exp_cat_cf_def by auto
    show "vcard (exp_cat_cf α 𝔄 𝔎) = 4⇩ℕ"
      unfolding exp_cat_cf_def by (simp_all add: nat_omega_simps)
    show "ℛ⇩∘ (exp_cat_cf α 𝔄 𝔎⦇ObjMap⦈) ⊆⇩∘ cat_FUNCT α 𝔅 𝔄⦇Obj⦈"
    proof
      (
        unfold cat_FUNCT_components exp_cat_cf_components, 
        intro vrange_VLambda_vsubset, 
        unfold cat_cs_simps
      )
      fix 𝔉 assume "𝔉 ∈⇩∘ cf_maps α ℭ 𝔄"
      then obtain 𝔉' where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉': "𝔉' : ℭ ↦↦⇩C⇘α⇙ 𝔄" 
        by auto
      from assms(2-4) 𝔉' show 
        "cf_map (cf_of_cf_map ℭ 𝔄 𝔉 ∘⇩C⇩F 𝔎) ∈⇩∘ cf_maps α 𝔅 𝔄"
        unfolding 𝔉_def
        by 
          ( 
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed
    show "exp_cat_cf α 𝔄 𝔎⦇ArrMap⦈⦇𝔑⦈ :
      exp_cat_cf α 𝔄 𝔎⦇ObjMap⦈⦇𝔉⦈ ↦⇘cat_FUNCT α 𝔅 𝔄⇙
      exp_cat_cf α 𝔄 𝔎⦇ObjMap⦈⦇𝔊⦈"
      if "𝔑 : 𝔉 ↦⇘cat_FUNCT α ℭ 𝔄⇙ 𝔊" for 𝔉 𝔊 𝔑 
    proof-
      note 𝔑 = cat_FUNCT_is_arrD[OF that]
      from 𝔑(1) assms(2-4) show ?thesis
        by (subst 𝔑(2), use nothing in ‹subst 𝔑(3), subst 𝔑(4)›) 
          (
            cs_concl
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_cs_intros  cat_FUNCT_cs_intros
          )
    qed
    show
      "exp_cat_cf α 𝔄 𝔎⦇ArrMap⦈⦇𝔐 ∘⇩A⇘cat_FUNCT α ℭ 𝔄⇙ 𝔑⦈ =
        exp_cat_cf α 𝔄 𝔎⦇ArrMap⦈⦇𝔐⦈ ∘⇩A⇘cat_FUNCT α 𝔅 𝔄⇙
        exp_cat_cf α 𝔄 𝔎⦇ArrMap⦈⦇𝔑⦈"
      if "𝔐 : 𝔊 ↦⇘cat_FUNCT α ℭ 𝔄⇙ ℌ" and "𝔑 : 𝔉 ↦⇘cat_FUNCT α ℭ 𝔄⇙ 𝔊" 
      for 𝔊 ℌ 𝔐 𝔉 𝔑
    proof-
      note 𝔐 = cat_FUNCT_is_arrD[OF that(1)]
        and 𝔑 = cat_FUNCT_is_arrD[OF that(2)]  
      from 𝔐(1) 𝔑(1) assms(2-4) show ?thesis  
        by (subst (1 2) 𝔐(2), use nothing in ‹subst (1 2) 𝔑(2)›)
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps  
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed
    show
      "exp_cat_cf α 𝔄 𝔎⦇ArrMap⦈⦇cat_FUNCT α ℭ 𝔄⦇CId⦈⦇𝔉⦈⦈ =
        cat_FUNCT α 𝔅 𝔄⦇CId⦈⦇exp_cat_cf α 𝔄 𝔎⦇ObjMap⦈⦇𝔉⦈⦈"
      if "𝔉 ∈⇩∘ cat_FUNCT α ℭ 𝔄⦇Obj⦈" for 𝔉
    proof-
      from that have 𝔉: "𝔉 ∈⇩∘ cf_maps α ℭ 𝔄" 
        unfolding cat_FUNCT_components by simp
      then obtain 𝔉' where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉': "𝔉' : ℭ ↦↦⇩C⇘α⇙ 𝔄" 
        by auto
      from assms(2-4) 𝔉 𝔉' show ?thesis
        by 
          (
            cs_concl
              cs_simp: 
                cat_cs_simps cat_FUNCT_cs_simps cat_FUNCT_components(1) 𝔉_def
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed
  qed 
    (
      cs_concl 
        cs_simp: cat_FUNCT_cs_simps
        cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros cat_cs_intros
    )+
qed

lemma exp_cat_cf_is_tiny_functor'[cat_FUNCT_cs_intros]: 
  assumes "𝒵 β" 
    and "α ∈⇩∘ β" 
    and "category α 𝔄" 
    and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔄' = cat_FUNCT α ℭ 𝔄"
    and "𝔅' = cat_FUNCT α 𝔅 𝔄"
  shows "exp_cat_cf α 𝔄 𝔎 : 𝔄' ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ 𝔅'"
  using assms(1-4) unfolding assms(5,6) by (rule exp_cat_cf_is_tiny_functor)


subsubsection‹Further properties›

lemma exp_cat_cf_cat_cf_id:
  assumes "category α 𝔄" and "category α ℭ"
  shows "exp_cat_cf α 𝔄 (cf_id ℭ) = cf_id (cat_FUNCT α ℭ 𝔄)"
proof-

  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret ℭ: category α ℭ by (rule assms(2))

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

  show ?thesis
  proof(rule cf_eqI)

    from αβ show "exp_cat_cf α 𝔄 (cf_id ℭ) :
      cat_FUNCT α ℭ 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α ℭ 𝔄"
      by 
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ show 
      "cf_id (cat_FUNCT α ℭ 𝔄) : cat_FUNCT α ℭ 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α ℭ 𝔄"
      by
        (
          cs_concl
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ have ObjMap_dom_lhs:
      "𝒟⇩∘ (exp_cat_cf α 𝔄 (cf_id ℭ)⦇ObjMap⦈) = cat_FUNCT α ℭ 𝔄⦇Obj⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from αβ have ObjMap_dom_rhs:
      "𝒟⇩∘ (cf_id (cat_FUNCT α ℭ 𝔄)⦇ObjMap⦈) = cat_FUNCT α ℭ 𝔄⦇Obj⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros
        )
    show "exp_cat_cf α 𝔄 (cf_id ℭ)⦇ObjMap⦈ = cf_id (cat_FUNCT α ℭ 𝔄)⦇ObjMap⦈"
    proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs cat_FUNCT_components(1))
      fix 𝔉 assume "𝔉 ∈⇩∘ cf_maps α ℭ 𝔄"
      then obtain 𝔉' where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉': "𝔉' : ℭ ↦↦⇩C⇘α⇙ 𝔄" 
        by clarsimp
      from 𝔉' show 
        "exp_cat_cf α 𝔄 (cf_id ℭ)⦇ObjMap⦈⦇𝔉⦈ =
          cf_id (cat_FUNCT α ℭ 𝔄)⦇ObjMap⦈⦇𝔉⦈"
        by 
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 𝔉_def 
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)+

    from αβ have ArrMap_dom_lhs: 
      "𝒟⇩∘ (exp_cat_cf α 𝔄 (cf_id ℭ)⦇ArrMap⦈) = cat_FUNCT α ℭ 𝔄⦇Arr⦈"
      by
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from αβ have ArrMap_dom_rhs:
      "𝒟⇩∘ (cf_id (cat_FUNCT α ℭ 𝔄)⦇ArrMap⦈) = cat_FUNCT α ℭ 𝔄⦇Arr⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros
        )
    show "exp_cat_cf α 𝔄 (cf_id ℭ)⦇ArrMap⦈ = cf_id (cat_FUNCT α ℭ 𝔄)⦇ArrMap⦈"
    proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      fix 𝔑 assume "𝔑 ∈⇩∘ cat_FUNCT α ℭ 𝔄⦇Arr⦈"
      then obtain ℌ ℌ' where 𝔑: "𝔑 : ℌ ↦⇘cat_FUNCT α ℭ 𝔄⇙ ℌ'" 
        by (auto intro: is_arrI)
      note 𝔑 = cat_FUNCT_is_arrD[OF 𝔑]
      from 𝔑(1) show 
        "exp_cat_cf α 𝔄 (cf_id ℭ)⦇ArrMap⦈⦇𝔑⦈ =
          cf_id (cat_FUNCT α ℭ 𝔄)⦇ArrMap⦈⦇𝔑⦈"
        by (subst (1 2) 𝔑(2))
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)+

  qed simp_all

qed

lemma exp_cat_cf_cf_comp:
  assumes "category α 𝔄" and "𝔊 : ℭ ↦↦⇩C⇘α⇙ 𝔇" and "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "exp_cat_cf α 𝔄 (𝔊 ∘⇩C⇩F 𝔉) = exp_cat_cf α 𝔄 𝔉 ∘⇩C⇩F exp_cat_cf α 𝔄 𝔊"
proof-

  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔊: is_functor α ℭ 𝔇 𝔊 by (rule assms(2))
  interpret 𝔉: is_functor α 𝔅 ℭ 𝔉 by (rule assms(3))
 
  define β where "β = α + ω"
  have β: "𝒵 β" and αβ: "α ∈⇩∘ β" 
    by (simp_all add: β_def 𝔄.𝒵_Limit_αω 𝔄.𝒵_ω_αω 𝒵_def 𝔄.𝒵_α_αω)
  then interpret β: 𝒵 β by simp 

  show ?thesis
  proof(rule cf_eqI)  
    from β αβ show "exp_cat_cf α 𝔄 (𝔊 ∘⇩C⇩F 𝔉) :
      cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔅 𝔄"
      by
        (
          cs_concl 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from β αβ show "exp_cat_cf α 𝔄 𝔉 ∘⇩C⇩F exp_cat_cf α 𝔄 𝔊 :
      cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔅 𝔄"
      by 
        (
          cs_concl
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from β αβ have ObjMap_dom_lhs: 
      "𝒟⇩∘ (exp_cat_cf α 𝔄 (𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈) = cat_FUNCT α 𝔇 𝔄⦇Obj⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from β αβ have ObjMap_dom_rhs: 
      "𝒟⇩∘ ((exp_cat_cf α 𝔄 𝔉 ∘⇩C⇩F exp_cat_cf α 𝔄 𝔊)⦇ObjMap⦈) =
        cat_FUNCT α 𝔇 𝔄⦇Obj⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from β αβ have ArrMap_dom_lhs: 
      "𝒟⇩∘ (exp_cat_cf α 𝔄 (𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈) = cat_FUNCT α 𝔇 𝔄⦇Arr⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from β αβ have ArrMap_dom_rhs: 
      "𝒟⇩∘ ((exp_cat_cf α 𝔄 𝔉 ∘⇩C⇩F exp_cat_cf α 𝔄 𝔊)⦇ArrMap⦈) =
        cat_FUNCT α 𝔇 𝔄⦇Arr⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    show 
      "exp_cat_cf α 𝔄 (𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈ =
        (exp_cat_cf α 𝔄 𝔉 ∘⇩C⇩F exp_cat_cf α 𝔄 𝔊)⦇ObjMap⦈"
    proof
      (
        rule vsv_eqI, 
        unfold ObjMap_dom_lhs ObjMap_dom_rhs cat_FUNCT_components(1)
      )
      fix ℌ assume "ℌ ∈⇩∘ cf_maps α 𝔇 𝔄"
      then obtain ℌ' where ℌ_def: "ℌ = cf_map ℌ'" and ℌ': "ℌ' : 𝔇 ↦↦⇩C⇘α⇙ 𝔄"
        by clarsimp
      from β αβ  ℌ' assms show 
        "exp_cat_cf α 𝔄 (𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈⦇ℌ⦈ =
          (exp_cat_cf α 𝔄 𝔉 ∘⇩C⇩F exp_cat_cf α 𝔄 𝔊)⦇ObjMap⦈⦇ℌ⦈"
        unfolding ℌ_def (*slow*)
        by 
          (
            cs_concl
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros 
          )
    qed 
      (
        use β αβ in
          ‹
            cs_concl
              cs_simp: cat_FUNCT_cs_simps
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          ›
      )+
    show "exp_cat_cf α 𝔄 (𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈ =
      (exp_cat_cf α 𝔄 𝔉 ∘⇩C⇩F exp_cat_cf α 𝔄 𝔊)⦇ArrMap⦈"
    proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      fix 𝔑 assume "𝔑 ∈⇩∘ cat_FUNCT α 𝔇 𝔄⦇Arr⦈"
      then obtain ℌ ℌ' where 𝔑: "𝔑 : ℌ ↦⇘cat_FUNCT α 𝔇 𝔄⇙ ℌ'" 
        by (auto intro: is_arrI)
      note 𝔑 = cat_FUNCT_is_arrD[OF 𝔑]
      from assms 𝔑(1) β αβ show 
        "exp_cat_cf α 𝔄 (𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇𝔑⦈ =
          (exp_cat_cf α 𝔄 𝔉 ∘⇩C⇩F exp_cat_cf α 𝔄 𝔊)⦇ArrMap⦈⦇𝔑⦈"
        by (subst (1 2) 𝔑(2))
          (
            cs_concl
              cs_simp:
                cat_FUNCT_cs_simps cat_cs_simps ntcf_cf_comp_ntcf_cf_comp_assoc
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          )
    qed 
      (
        use β αβ in
          ‹
            cs_concl
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          ›
      )+
  qed simp_all

qed



subsection‹Natural transformation raised to the power of a category›


subsubsection‹Definition and elementary properties›

definition exp_ntcf_cat :: "V ⇒ V ⇒ V ⇒ V"
  where "exp_ntcf_cat α 𝔑 𝔇 =
    [
      (
        λ𝔖∈⇩∘cat_FUNCT α 𝔇 (𝔑⦇NTDGDom⦈)⦇Obj⦈.
          ntcf_arrow (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F cf_of_cf_map 𝔇 (𝔑⦇NTDGDom⦈) 𝔖)
      ),
      exp_cf_cat α (𝔑⦇NTDom⦈) 𝔇,
      exp_cf_cat α (𝔑⦇NTCod⦈) 𝔇,
      cat_FUNCT α 𝔇 (𝔑⦇NTDGDom⦈),
      cat_FUNCT α 𝔇 (𝔑⦇NTDGCod⦈)
    ]⇩∘"


text‹Components.›

lemma exp_ntcf_cat_components:
  shows "exp_ntcf_cat α 𝔑 𝔇⦇NTMap⦈ =
    (
      λ𝔖∈⇩∘cat_FUNCT α 𝔇 (𝔑⦇NTDGDom⦈)⦇Obj⦈.
        ntcf_arrow (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F cf_of_cf_map 𝔇 (𝔑⦇NTDGDom⦈) 𝔖)
    )"
    and "exp_ntcf_cat α 𝔑 𝔇⦇NTDom⦈ = exp_cf_cat α (𝔑⦇NTDom⦈) 𝔇"
    and "exp_ntcf_cat α 𝔑 𝔇⦇NTCod⦈ = exp_cf_cat α (𝔑⦇NTCod⦈) 𝔇"
    and "exp_ntcf_cat α 𝔑 𝔇⦇NTDGDom⦈ = cat_FUNCT α 𝔇 (𝔑⦇NTDGDom⦈)"
    and "exp_ntcf_cat α 𝔑 𝔇⦇NTDGCod⦈ = cat_FUNCT α 𝔇 (𝔑⦇NTDGCod⦈)"
  unfolding exp_ntcf_cat_def nt_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Natural transformation map›

mk_VLambda exp_ntcf_cat_components(1)
  |vsv exp_ntcf_cat_components_NTMap_vsv[cat_FUNCT_cs_intros]|

context is_ntcf
begin

lemmas exp_ntcf_cat_components' = 
  exp_ntcf_cat_components[where α=α and 𝔑=𝔑, unfolded cat_cs_simps]

lemmas [cat_FUNCT_cs_simps] = exp_ntcf_cat_components'(2-5)

mk_VLambda exp_ntcf_cat_components(1)[where 𝔑=𝔑, unfolded cat_cs_simps]
  |vdomain exp_ntcf_cat_components_NTMap_vdomain[cat_FUNCT_cs_simps]|
  |app exp_ntcf_cat_components_NTMap_app[cat_FUNCT_cs_simps]|

end

lemmas [cat_FUNCT_cs_simps] = 
  is_ntcf.exp_ntcf_cat_components'(2-5)
  is_ntcf.exp_ntcf_cat_components_NTMap_vdomain
  is_ntcf.exp_ntcf_cat_components_NTMap_app


subsubsection‹
Natural transformation raised to the power of a category 
is a natural transformation
›

lemma exp_ntcf_cat_is_tiny_ntcf:
  assumes "𝒵 β" 
    and "α ∈⇩∘ β" 
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "category α 𝔇"
  shows "exp_ntcf_cat α 𝔑 𝔇 :
    exp_cf_cat α 𝔉 𝔇 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y exp_cf_cat α 𝔊 𝔇 :
    cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ cat_FUNCT α 𝔇 𝔅"
proof(rule is_tiny_ntcfI')

  interpret β: 𝒵 β by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(3))
  interpret 𝔇: category α 𝔇 by (rule assms(4))

  let ?exp_𝔑 = ‹exp_ntcf_cat α 𝔑 𝔇›
  let ?exp_𝔉 = ‹exp_cf_cat α 𝔉 𝔇›
  let ?exp_𝔊 = ‹exp_cf_cat α 𝔊 𝔇›

  from assms(1,2) show 
    "exp_cf_cat α 𝔉 𝔇 : cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ cat_FUNCT α 𝔇 𝔅"
    by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
  from assms(1,2) show 
    "exp_cf_cat α 𝔊 𝔇 : cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ cat_FUNCT α 𝔇 𝔅"
    by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)

  show "?exp_𝔑 : 
    ?exp_𝔉 ↦⇩C⇩F ?exp_𝔊 : cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔇 𝔅"
  proof(rule is_ntcfI')

    show "vfsequence (?exp_𝔑)" unfolding exp_ntcf_cat_def by auto
    show "vcard (?exp_𝔑) = 5⇩ℕ"
      unfolding exp_ntcf_cat_def by (simp add: nat_omega_simps)

    from assms(1,2) show "?exp_𝔉 : cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔇 𝔅"
      by 
        (
          cs_concl cs_intro: 
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from assms(1,2) show "?exp_𝔊 : cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔇 𝔅"
      by 
        (
          cs_concl cs_intro:
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )

    show "?exp_𝔑⦇NTMap⦈⦇ℌ⦈ : 
      ?exp_𝔉⦇ObjMap⦈⦇ℌ⦈ ↦⇘cat_FUNCT α 𝔇 𝔅⇙ ?exp_𝔊⦇ObjMap⦈⦇ℌ⦈"
      if "ℌ ∈⇩∘ cat_FUNCT α 𝔇 𝔄⦇Obj⦈" for ℌ
    proof-
      from that[unfolded cat_FUNCT_cs_simps] have "ℌ ∈⇩∘ cf_maps α 𝔇 𝔄" by simp
      then obtain ℌ' where ℌ_def: "ℌ = cf_map ℌ'" and ℌ': "ℌ' : 𝔇 ↦↦⇩C⇘α⇙ 𝔄" 
        by auto
      from ℌ' show ?thesis
        by 
          (
            cs_concl 
              cs_simp: cat_FUNCT_cs_simps ℌ_def 
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed
    
    show 
      "?exp_𝔑⦇NTMap⦈⦇𝔗⦈ ∘⇩A⇘cat_FUNCT α 𝔇 𝔅⇙ ?exp_𝔉⦇ArrMap⦈⦇𝔏⦈ =
        ?exp_𝔊⦇ArrMap⦈⦇𝔏⦈ ∘⇩A⇘cat_FUNCT α 𝔇 𝔅⇙ ?exp_𝔑⦇NTMap⦈⦇𝔖⦈"
      if "𝔏 : 𝔖 ↦⇘cat_FUNCT α 𝔇 𝔄⇙ 𝔗" for 𝔖 𝔗 𝔏
    proof-
      note 𝔏 = cat_FUNCT_is_arrD[OF that]
      let ?𝔖 = ‹cf_of_cf_map 𝔇 𝔄 𝔖›
        and ?𝔗 = ‹cf_of_cf_map 𝔇 𝔄 𝔗›
        and ?𝔏 = ‹ntcf_of_ntcf_arrow 𝔇 𝔄 𝔏›
      have [cat_cs_simps]:
        "(𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ?𝔗) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?𝔏) =
          (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?𝔏) ∙⇩N⇩T⇩C⇩F (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ?𝔖)"
      proof(rule ntcf_eqI)
        from 𝔏(1) show
          "(𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ?𝔗) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?𝔏) :
            𝔉 ∘⇩C⇩F ?𝔖 ↦⇩C⇩F 𝔊 ∘⇩C⇩F ?𝔗 : 𝔇 ↦↦⇩C⇘α⇙ 𝔅"
          by (cs_concl cs_intro: cat_cs_intros)
        from 𝔏(1) show
          "(𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?𝔏) ∙⇩N⇩T⇩C⇩F (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ?𝔖) :
            𝔉 ∘⇩C⇩F ?𝔖 ↦⇩C⇩F 𝔊 ∘⇩C⇩F ?𝔗 : 𝔇 ↦↦⇩C⇘α⇙ 𝔅"
          by (cs_concl cs_intro: cat_cs_intros)
        from 𝔏(1) have dom_lhs:
          "𝒟⇩∘ (((𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ?𝔗) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?𝔏))⦇NTMap⦈) = 𝔇⦇Obj⦈"
          by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        from 𝔏(1) have dom_rhs:
          "𝒟⇩∘ (((𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?𝔏) ∙⇩N⇩T⇩C⇩F (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ?𝔖))⦇NTMap⦈) = 𝔇⦇Obj⦈"
          by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        show 
          "((𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ?𝔗) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?𝔏))⦇NTMap⦈ =
            ((𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?𝔏) ∙⇩N⇩T⇩C⇩F (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ?𝔖))⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix d assume "d ∈⇩∘ 𝔇⦇Obj⦈"
          with 𝔏(1) show
            "((𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ?𝔗) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?𝔏))⦇NTMap⦈⦇d⦈ =
              ((𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?𝔏) ∙⇩N⇩T⇩C⇩F (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ?𝔖))⦇NTMap⦈⦇d⦈"
            by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        qed (cs_concl cs_intro: cat_cs_intros)
      qed simp_all
      from 𝔏(1,3,4) that show ?thesis
        by (subst (1 2) 𝔏(2), use nothing in ‹subst 𝔏(3), subst 𝔏(4)›)
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed
  qed 
    (
      cs_concl 
        cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros cat_FUNCT_cs_intros
    )+

qed

lemma exp_ntcf_cat_is_tiny_ntcf'[cat_FUNCT_cs_intros]:
  assumes "𝒵 β"
    and "α ∈⇩∘ β"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "category α 𝔇"
    and "𝔉' = exp_cf_cat α 𝔉 𝔇"
    and "𝔊' = exp_cf_cat α 𝔊 𝔇"
    and "𝔄' = cat_FUNCT α 𝔇 𝔄"
    and "𝔅' = cat_FUNCT α 𝔇 𝔅"
  shows "exp_ntcf_cat α 𝔑 𝔇 : 𝔉' ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊' : 𝔄' ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ 𝔅'"
  using assms(1-4) unfolding assms(5-8) by (rule exp_ntcf_cat_is_tiny_ntcf)


subsubsection‹Further properties›

lemma exp_ntcf_cat_cf_ntcf_comp: 
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "ℌ : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "category α 𝔇"
  shows 
    "exp_ntcf_cat α (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) 𝔇 =
      exp_cf_cat α ℌ 𝔇 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_ntcf_cat α 𝔑 𝔇"
proof-

  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_functor α 𝔅 ℭ ℌ by (rule assms(2))
  interpret 𝔇: category α 𝔇 by (rule assms(3))

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

  show ?thesis
  proof(rule ntcf_eqI)
    from αβ have dom_lhs:
      "𝒟⇩∘ (exp_ntcf_cat α (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) 𝔇⦇NTMap⦈) = cat_FUNCT α 𝔇 𝔄⦇Obj⦈"
      by 
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ have dom_rhs: 
      "𝒟⇩∘ ((exp_cf_cat α ℌ 𝔇 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_ntcf_cat α 𝔑 𝔇)⦇NTMap⦈) =
        cat_FUNCT α 𝔇 𝔄⦇Obj⦈"
      by 
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    show
      "exp_ntcf_cat α (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) 𝔇⦇NTMap⦈ =
        (exp_cf_cat α ℌ 𝔇 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_ntcf_cat α 𝔑 𝔇)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs cat_FUNCT_components(1))
      fix 𝔎 assume prems: "𝔎 ∈⇩∘ cf_maps α 𝔇 𝔄"
      then obtain 𝔎' where 𝔎_def: "𝔎 = cf_map 𝔎'" and 𝔎': "𝔎' : 𝔇 ↦↦⇩C⇘α⇙ 𝔄"
        by (auto intro: is_arrI)
      from αβ prems 𝔎' show 
        "exp_ntcf_cat α (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) 𝔇⦇NTMap⦈⦇𝔎⦈ =
          (exp_cf_cat α ℌ 𝔇 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_ntcf_cat α 𝔑 𝔇)⦇NTMap⦈⦇𝔎⦈"
        by 
          (
            cs_concl
              cs_simp:
                cf_ntcf_comp_ntcf_cf_comp_assoc 
                cat_cs_simps cat_FUNCT_cs_simps
                𝔎_def
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          )
    qed (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
  qed
    (
      cs_concl
        cs_simp: exp_cf_cat_cf_comp cat_cs_simps cat_FUNCT_cs_simps
        cs_intro: αβ cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
    )+

qed

lemma exp_ntcf_cat_ntcf_cf_comp: 
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "category α 𝔇"
  shows 
    "exp_ntcf_cat α (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ) 𝔇 =
      exp_ntcf_cat α 𝔑 𝔇 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cf_cat α ℌ 𝔇"
proof-

  interpret 𝔑: is_ntcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_functor α 𝔄 𝔅 ℌ by (rule assms(2))
  interpret 𝔇: category α 𝔇 by (rule assms(3))

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

  show ?thesis
  proof(rule ntcf_eqI)
    from αβ have dom_lhs:
      "𝒟⇩∘ (exp_ntcf_cat α (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ) 𝔇⦇NTMap⦈) = cat_FUNCT α 𝔇 𝔄⦇Obj⦈"
      by 
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ have dom_rhs: 
      "𝒟⇩∘ ((exp_ntcf_cat α 𝔑 𝔇 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cf_cat α ℌ 𝔇)⦇NTMap⦈) =
        cat_FUNCT α 𝔇 𝔄⦇Obj⦈"
      by 
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    show
      "exp_ntcf_cat α (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ) 𝔇⦇NTMap⦈ =
        (exp_ntcf_cat α 𝔑 𝔇 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cf_cat α ℌ 𝔇)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs cat_FUNCT_components(1))
      fix 𝔎 assume prems: "𝔎 ∈⇩∘ cf_maps α 𝔇 𝔄"
      then obtain 𝔎' where 𝔎_def: "𝔎 = cf_map 𝔎'" and 𝔎': "𝔎' : 𝔇 ↦↦⇩C⇘α⇙ 𝔄"
        by (auto intro: is_arrI)
      from αβ assms prems 𝔎' show
        "exp_ntcf_cat α (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ) 𝔇⦇NTMap⦈⦇𝔎⦈ = 
          (exp_ntcf_cat α 𝔑 𝔇 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cf_cat α ℌ 𝔇)⦇NTMap⦈⦇𝔎⦈"
        by 
          (
            cs_concl 
              cs_simp: 
                ntcf_cf_comp_ntcf_cf_comp_assoc 
                cat_cs_simps cat_FUNCT_cs_simps 
                𝔎_def
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          )
    qed (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
  qed
    (
      cs_concl
        cs_simp: exp_cf_cat_cf_comp cat_cs_simps cat_FUNCT_cs_simps
        cs_intro: αβ cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
    )+
qed

lemma exp_ntcf_cat_ntcf_vcomp: 
  assumes "category α 𝔄" 
    and "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows 
    "exp_ntcf_cat α (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) 𝔄 =
      exp_ntcf_cat α 𝔐 𝔄 ∙⇩N⇩T⇩C⇩F exp_ntcf_cat α 𝔑 𝔄"
proof-

  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔐: is_ntcf α 𝔅 ℭ 𝔊 ℌ 𝔐 by (rule assms(2))
  interpret 𝔑: is_ntcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(3))

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

  show ?thesis
  proof(rule ntcf_eqI)
    from αβ show
      "exp_ntcf_cat α (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) 𝔄 :
        exp_cf_cat α 𝔉 𝔄 ↦⇩C⇩F exp_cf_cat α ℌ 𝔄 :
        cat_FUNCT α 𝔄 𝔅 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
      by 
        (
          cs_concl 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ show
      "exp_ntcf_cat α 𝔐 𝔄 ∙⇩N⇩T⇩C⇩F exp_ntcf_cat α 𝔑 𝔄 :
        exp_cf_cat α 𝔉 𝔄 ↦⇩C⇩F exp_cf_cat α ℌ 𝔄 :
        cat_FUNCT α 𝔄 𝔅 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
      by 
        (
          cs_concl 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ have dom_lhs: 
      "𝒟⇩∘ ((exp_ntcf_cat α 𝔐 𝔄 ∙⇩N⇩T⇩C⇩F exp_ntcf_cat α 𝔑 𝔄)⦇NTMap⦈) = 
        cat_FUNCT α 𝔄 𝔅⦇Obj⦈"
      by 
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    have dom_rhs: 
      "𝒟⇩∘ (exp_ntcf_cat α (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) 𝔄⦇NTMap⦈) = cat_FUNCT α 𝔄 𝔅⦇Obj⦈"
      by (cs_concl cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros)
    show 
      "exp_ntcf_cat α (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) 𝔄⦇NTMap⦈ = 
        (exp_ntcf_cat α 𝔐 𝔄 ∙⇩N⇩T⇩C⇩F exp_ntcf_cat α 𝔑 𝔄)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs cat_FUNCT_components(1))
      fix 𝔉' assume "𝔉' ∈⇩∘ cf_maps α 𝔄 𝔅"
      then obtain 𝔉'' 
        where 𝔉'_def: "𝔉' = cf_map 𝔉''" and 𝔉'': "𝔉'' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
        by auto
      from 𝔉'' αβ show 
        "exp_ntcf_cat α (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) 𝔄⦇NTMap⦈⦇𝔉'⦈ =
          (exp_ntcf_cat α 𝔐 𝔄 ∙⇩N⇩T⇩C⇩F exp_ntcf_cat α 𝔑 𝔄)⦇NTMap⦈⦇𝔉'⦈"
        unfolding 𝔉'_def
        by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          )
    qed (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)+
  qed simp_all

qed

lemma ntcf_id_exp_cf_cat:
  assumes "category α 𝔄" and "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "ntcf_id (exp_cf_cat α 𝔉 𝔄) = exp_ntcf_cat α (ntcf_id 𝔉) 𝔄"
proof-

  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔉: is_functor α 𝔅 ℭ 𝔉 by (rule assms(2))

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

  show ?thesis
  proof(rule ntcf_eqI)
    from αβ show "exp_ntcf_cat α (ntcf_id 𝔉) 𝔄 :
      exp_cf_cat α 𝔉 𝔄 ↦⇩C⇩F exp_cf_cat α 𝔉 𝔄 :
      cat_FUNCT α 𝔄 𝔅 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
      by 
        (
          cs_concl 
            cs_simp: cat_FUNCT_cs_simps 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ show "ntcf_id (exp_cf_cat α 𝔉 𝔄) :
      exp_cf_cat α 𝔉 𝔄 ↦⇩C⇩F exp_cf_cat α 𝔉 𝔄 :
      cat_FUNCT α 𝔄 𝔅 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
      by 
        (
          cs_concl 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ assms have dom_lhs: 
      "𝒟⇩∘ (ntcf_id (exp_cf_cat α 𝔉 𝔄)⦇NTMap⦈) = cat_FUNCT α 𝔄 𝔅⦇Obj⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from αβ assms have dom_rhs:
      "𝒟⇩∘ (exp_ntcf_cat α (ntcf_id 𝔉) 𝔄⦇NTMap⦈) = cat_FUNCT α 𝔄 𝔅⦇Obj⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    show
      "ntcf_id (exp_cf_cat α 𝔉 𝔄)⦇NTMap⦈ = exp_ntcf_cat α (ntcf_id 𝔉) 𝔄⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs cat_FUNCT_components(1))
      fix 𝔊 assume "𝔊 ∈⇩∘ cf_maps α 𝔄 𝔅"
      then obtain 𝔊' 
        where 𝔊_def: "𝔊 = cf_map 𝔊'" and 𝔊': "𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
        by auto  
      from 𝔊' αβ show 
        "ntcf_id (exp_cf_cat α 𝔉 𝔄)⦇NTMap⦈⦇𝔊⦈ =
          exp_ntcf_cat α (ntcf_id 𝔉) 𝔄⦇NTMap⦈⦇𝔊⦈"
        unfolding 𝔊_def
        by 
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          )
    qed 
      (
        cs_concl 
          cs_intro: αβ cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )+
  qed simp_all
qed



subsection‹Category raised to the power of the natural transformation›


subsubsection‹Definition and elementary properties›

definition exp_cat_ntcf :: "V ⇒ V ⇒ V ⇒ V"
  where "exp_cat_ntcf α ℭ 𝔑 =
    [
      (
        λ𝔖∈⇩∘cat_FUNCT α (𝔑⦇NTDGCod⦈) ℭ⦇Obj⦈.
          ntcf_arrow (cf_of_cf_map (𝔑⦇NTDGCod⦈) ℭ 𝔖 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)
      ),
      exp_cat_cf α ℭ (𝔑⦇NTDom⦈),
      exp_cat_cf α ℭ (𝔑⦇NTCod⦈),
      cat_FUNCT α (𝔑⦇NTDGCod⦈) ℭ,
      cat_FUNCT α (𝔑⦇NTDGDom⦈) ℭ
    ]⇩∘"


text‹Components.›

lemma exp_cat_ntcf_components:
  shows "exp_cat_ntcf α ℭ 𝔑⦇NTMap⦈ =
    (
      λ𝔖∈⇩∘cat_FUNCT α (𝔑⦇NTDGCod⦈) ℭ⦇Obj⦈.
        ntcf_arrow (cf_of_cf_map (𝔑⦇NTDGCod⦈) ℭ 𝔖 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)
    )"
    and "exp_cat_ntcf α ℭ 𝔑⦇NTDom⦈ = exp_cat_cf α ℭ (𝔑⦇NTDom⦈)"
    and "exp_cat_ntcf α ℭ 𝔑⦇NTCod⦈ = exp_cat_cf α ℭ (𝔑⦇NTCod⦈)"
    and "exp_cat_ntcf α ℭ 𝔑⦇NTDGDom⦈ = cat_FUNCT α (𝔑⦇NTDGCod⦈) ℭ"
    and "exp_cat_ntcf α ℭ 𝔑⦇NTDGCod⦈ = cat_FUNCT α (𝔑⦇NTDGDom⦈) ℭ"
  unfolding exp_cat_ntcf_def nt_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Natural transformation map›

mk_VLambda exp_cat_ntcf_components(1)
  |vsv exp_cat_ntcf_components_NTMap_vsv[cat_FUNCT_cs_intros]|

context is_ntcf
begin

lemmas exp_cat_ntcf_components' = 
  exp_cat_ntcf_components[where α=α and 𝔑=𝔑, unfolded cat_cs_simps]

lemmas [cat_FUNCT_cs_simps] = exp_cat_ntcf_components'(2-5)

mk_VLambda exp_cat_ntcf_components(1)[where 𝔑=𝔑, unfolded cat_cs_simps]
  |vdomain exp_cat_ntcf_components_NTMap_vdomain[cat_FUNCT_cs_simps]|
  |app exp_cat_ntcf_components_NTMap_app[cat_FUNCT_cs_simps]|

end

lemmas exp_cat_ntcf_components' = is_ntcf.exp_cat_ntcf_components'

lemmas [cat_FUNCT_cs_simps] = 
  is_ntcf.exp_cat_ntcf_components'(2-5)
  is_ntcf.exp_cat_ntcf_components_NTMap_vdomain
  is_ntcf.exp_cat_ntcf_components_NTMap_app


subsubsection‹
Category raised to the power of a natural transformation
is a natural transformation
›

lemma exp_cat_ntcf_is_tiny_ntcf:
  assumes "𝒵 β" 
    and "α ∈⇩∘ β" 
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "category α ℭ"
  shows "exp_cat_ntcf α ℭ 𝔑 :
    exp_cat_cf α ℭ 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y exp_cat_cf α ℭ 𝔊 :
    cat_FUNCT α 𝔅 ℭ ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ cat_FUNCT α 𝔄 ℭ"
proof(rule is_tiny_ntcfI')

  interpret β: 𝒵 β by (rule assms(1))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(3))
  interpret ℭ: category α ℭ by (rule assms(4))

  let ?exp_𝔑 = ‹exp_cat_ntcf α ℭ 𝔑›
  let ?exp_𝔉 = ‹exp_cat_cf α ℭ 𝔉›
  let ?exp_𝔊 = ‹exp_cat_cf α ℭ 𝔊›

  from assms(1,2) show
    "exp_cat_cf α ℭ 𝔊 : cat_FUNCT α 𝔅 ℭ ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ cat_FUNCT α 𝔄 ℭ"
    by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
  from assms(1,2) show
    "exp_cat_cf α ℭ 𝔉 : cat_FUNCT α 𝔅 ℭ ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ cat_FUNCT α 𝔄 ℭ"
    by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)

  show "?exp_𝔑 : ?exp_𝔉 ↦⇩C⇩F ?exp_𝔊 : cat_FUNCT α 𝔅 ℭ ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
  proof(rule is_ntcfI')

    show "vfsequence (?exp_𝔑)" unfolding exp_cat_ntcf_def by auto
    show "vcard (?exp_𝔑) = 5⇩ℕ"
      unfolding exp_cat_ntcf_def by (simp add: nat_omega_simps)
  
    from assms(1,2) show
      "exp_cat_cf α ℭ 𝔊 : cat_FUNCT α 𝔅 ℭ ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
      by 
        (
          cs_concl cs_intro:
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )

    from assms(1,2) show 
      "exp_cat_cf α ℭ 𝔉 : cat_FUNCT α 𝔅 ℭ ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔄 ℭ"
      by 
        (
          cs_concl cs_intro: 
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
  
    show "exp_cat_ntcf α ℭ 𝔑⦇NTMap⦈⦇ℌ⦈ : 
      exp_cat_cf α ℭ 𝔉⦇ObjMap⦈⦇ℌ⦈ ↦⇘cat_FUNCT α 𝔄 ℭ⇙ 
      exp_cat_cf α ℭ 𝔊⦇ObjMap⦈⦇ℌ⦈"
      if "ℌ ∈⇩∘ cat_FUNCT α 𝔅 ℭ⦇Obj⦈" for ℌ
    proof-
      from that[unfolded cat_FUNCT_cs_simps] have "ℌ ∈⇩∘ cf_maps α 𝔅 ℭ" by simp
      then obtain ℌ' where ℌ_def: "ℌ = cf_map ℌ'" and ℌ': "ℌ' : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
        by auto
      from ℌ' show ?thesis
        unfolding ℌ_def
        by
          (
            cs_concl
              cs_simp: cat_FUNCT_cs_simps ℌ_def
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed
  
    show 
      "?exp_𝔑⦇NTMap⦈⦇𝔗⦈ ∘⇩A⇘cat_FUNCT α 𝔄 ℭ⇙ ?exp_𝔉⦇ArrMap⦈⦇𝔏⦈ =
        ?exp_𝔊⦇ArrMap⦈⦇𝔏⦈ ∘⇩A⇘cat_FUNCT α 𝔄 ℭ⇙ ?exp_𝔑⦇NTMap⦈⦇𝔖⦈"
      if "𝔏 : 𝔖 ↦⇘cat_FUNCT α 𝔅 ℭ⇙ 𝔗" for 𝔖 𝔗 𝔏
    proof-
      note 𝔏 = cat_FUNCT_is_arrD[OF that]
      let ?𝔖 = ‹cf_of_cf_map 𝔅 ℭ 𝔖›
        and ?𝔗 = ‹cf_of_cf_map 𝔅 ℭ 𝔗›
        and ?𝔏 = ‹ntcf_of_ntcf_arrow 𝔅 ℭ 𝔏›
      have [cat_cs_simps]:
        "(?𝔗 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) ∙⇩N⇩T⇩C⇩F (?𝔏 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉) =
          (?𝔏 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) ∙⇩N⇩T⇩C⇩F (?𝔖 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)"
      proof(rule ntcf_eqI)
        from 𝔏(1) show
          "(?𝔗 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) ∙⇩N⇩T⇩C⇩F (?𝔏 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉) :
            ?𝔖 ∘⇩C⇩F 𝔉 ↦⇩C⇩F ?𝔗 ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
          by (cs_concl cs_intro: cat_cs_intros)
        from 𝔏(1) show
          "(?𝔏 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) ∙⇩N⇩T⇩C⇩F (?𝔖 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) :
            ?𝔖 ∘⇩C⇩F 𝔉 ↦⇩C⇩F ?𝔗 ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
          by (cs_concl cs_intro: cat_cs_intros)
        from 𝔏(1) have dom_lhs:
          "𝒟⇩∘ (((?𝔗 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) ∙⇩N⇩T⇩C⇩F (?𝔏 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉))⦇NTMap⦈) = 𝔄⦇Obj⦈"
          by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        from 𝔏(1) have dom_rhs:
          "𝒟⇩∘ (((?𝔏 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) ∙⇩N⇩T⇩C⇩F (?𝔖 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈) = 𝔄⦇Obj⦈"
          by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        show 
          "((?𝔗 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) ∙⇩N⇩T⇩C⇩F (?𝔏 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉))⦇NTMap⦈ =
            ((?𝔏 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) ∙⇩N⇩T⇩C⇩F (?𝔖 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
          with 𝔏(1) show
            "((?𝔗 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) ∙⇩N⇩T⇩C⇩F (?𝔏 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉))⦇NTMap⦈⦇a⦈ =
              ((?𝔏 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) ∙⇩N⇩T⇩C⇩F (?𝔖 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈⦇a⦈"
            by 
              (
                cs_concl 
                  cs_simp: cat_cs_simps is_ntcf.ntcf_Comp_commute 
                  cs_intro: cat_cs_intros
              )
        qed (cs_concl cs_intro: cat_cs_intros)
      qed simp_all
      from 𝔏(1,3,4) that show ?thesis
        by (subst (1 2) 𝔏(2), use nothing in ‹subst 𝔏(3), subst 𝔏(4)›)
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
    qed

  qed
    (
      cs_concl 
        cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros cat_FUNCT_cs_intros
    )+

qed

lemma exp_cat_ntcf_is_tiny_ntcf'[cat_FUNCT_cs_intros]:
  assumes "𝒵 β"
    and "α ∈⇩∘ β"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "category α ℭ"
    and "𝔉' = exp_cat_cf α ℭ 𝔉"
    and "𝔊' = exp_cat_cf α ℭ 𝔊"
    and "𝔄' = cat_FUNCT α 𝔅 ℭ"
    and "𝔅' = cat_FUNCT α 𝔄 ℭ"
  shows "exp_cat_ntcf α ℭ 𝔑 : 𝔉' ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊' : 𝔄' ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ 𝔅'"
  using assms(1-4) unfolding assms(5-8) by (rule exp_cat_ntcf_is_tiny_ntcf)


subsubsection‹Further properties›

lemma ntcf_id_exp_cat_cf:
  assumes "category α 𝔄" and "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "ntcf_id (exp_cat_cf α 𝔄 𝔉) = exp_cat_ntcf α 𝔄 (ntcf_id 𝔉)"
proof-

  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔉: is_functor α 𝔅 ℭ 𝔉 by (rule assms(2))

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

  show ?thesis
  proof(rule ntcf_eqI)
    from αβ show "exp_cat_ntcf α 𝔄 (ntcf_id 𝔉) :
      exp_cat_cf α 𝔄 𝔉 ↦⇩C⇩F exp_cat_cf α 𝔄 𝔉 :
      cat_FUNCT α ℭ 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔅 𝔄"
      by 
        (
          cs_concl 
            cs_simp: cat_FUNCT_cs_simps 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from assms β αβ show "ntcf_id (exp_cat_cf α 𝔄 𝔉) :
      exp_cat_cf α 𝔄 𝔉 ↦⇩C⇩F exp_cat_cf α 𝔄 𝔉 :
      cat_FUNCT α ℭ 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔅 𝔄"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ assms have dom_lhs: 
      "𝒟⇩∘ (exp_cat_ntcf α 𝔄 (ntcf_id 𝔉)⦇NTMap⦈) = cat_FUNCT α ℭ 𝔄⦇Obj⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    from αβ assms have dom_rhs:
      "𝒟⇩∘ (ntcf_id (exp_cat_cf α 𝔄 𝔉)⦇NTMap⦈) = cat_FUNCT α ℭ 𝔄⦇Obj⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        )
    show
      "ntcf_id (exp_cat_cf α 𝔄 𝔉)⦇NTMap⦈ = exp_cat_ntcf α 𝔄 (ntcf_id 𝔉)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs cat_FUNCT_components(1))
      fix 𝔊 assume "𝔊 ∈⇩∘ cf_maps α ℭ 𝔄"
      then obtain 𝔊' 
        where 𝔊_def: "𝔊 = cf_map 𝔊'" and 𝔊': "𝔊' : ℭ ↦↦⇩C⇘α⇙ 𝔄" 
        by auto  
      from 𝔊' αβ show 
        "ntcf_id (exp_cat_cf α 𝔄 𝔉)⦇NTMap⦈⦇𝔊⦈ =
          exp_cat_ntcf α 𝔄 (ntcf_id 𝔉)⦇NTMap⦈⦇𝔊⦈"
        unfolding 𝔊_def
        by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          )
    qed 
      (
        cs_concl 
          cs_intro: αβ cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )+
  qed simp_all

qed

lemma exp_cat_ntcf_ntcf_cf_comp:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "category α 𝔇"
  shows 
    "exp_cat_ntcf α 𝔇 (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ) =
      exp_cat_cf α 𝔇 ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔇 𝔑"
proof-

  interpret 𝔑: is_ntcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_functor α 𝔄 𝔅 ℌ by (rule assms(2))
  interpret 𝔇: category α 𝔇 by (rule assms(3))

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

  show ?thesis
  proof(rule ntcf_eqI)
    from αβ have dom_lhs:
      "𝒟⇩∘ (exp_cat_ntcf α 𝔇 (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ)⦇NTMap⦈) = cat_FUNCT α ℭ 𝔇⦇Obj⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ have dom_rhs: 
      "𝒟⇩∘ ((exp_cat_cf α 𝔇 ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔇 𝔑)⦇NTMap⦈) =
        cat_FUNCT α ℭ 𝔇⦇Obj⦈"
      by 
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )

    show
      "exp_cat_ntcf α 𝔇 (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ)⦇NTMap⦈ =
        (exp_cat_cf α 𝔇 ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔇 𝔑)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs cat_FUNCT_components(1))
      fix 𝔎 assume prems: "𝔎 ∈⇩∘ cf_maps α ℭ 𝔇"
      then obtain 𝔎' where 𝔎_def: "𝔎 = cf_map 𝔎'" and 𝔎': "𝔎' : ℭ ↦↦⇩C⇘α⇙ 𝔇"
        by (auto intro: is_arrI)
      from αβ assms prems 𝔎' show
        "exp_cat_ntcf α 𝔇 (𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ)⦇NTMap⦈⦇𝔎⦈ = 
          (exp_cat_cf α 𝔇 ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔇 𝔑)⦇NTMap⦈⦇𝔎⦈"
        unfolding 𝔎_def
        by
          (
            cs_concl
              cs_simp:
                cf_ntcf_comp_ntcf_cf_comp_assoc cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          )
    qed (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
  qed
    (
      cs_concl
        cs_simp: exp_cat_cf_cf_comp cat_cs_simps cat_FUNCT_cs_simps
        cs_intro: αβ cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
    )+

qed

lemma exp_cat_ntcf_cf_ntcf_comp: 
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "ℌ : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "category α 𝔇"
  shows
    "exp_cat_ntcf α 𝔇 (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑) =
      exp_cat_ntcf α 𝔇 𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cat_cf α 𝔇 ℌ"
proof-

  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_functor α 𝔅 ℭ ℌ by (rule assms(2))
  interpret 𝔇: category α 𝔇 by (rule assms(3))

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

  show ?thesis
  proof(rule ntcf_eqI)

    from αβ have dom_lhs:
      "𝒟⇩∘ (exp_cat_ntcf α 𝔇 (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈) = cat_FUNCT α ℭ 𝔇⦇Obj⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ have dom_rhs: 
      "𝒟⇩∘ ((exp_cat_ntcf α 𝔇 𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cat_cf α 𝔇 ℌ)⦇NTMap⦈) =
        cat_FUNCT α ℭ 𝔇⦇Obj⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )

    show
      "exp_cat_ntcf α 𝔇 (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈ =
        (exp_cat_ntcf α 𝔇 𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cat_cf α 𝔇 ℌ)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs cat_FUNCT_components(1))
      fix 𝔎 assume prems: "𝔎 ∈⇩∘ cf_maps α ℭ 𝔇"
      then obtain 𝔎' where 𝔎_def: "𝔎 = cf_map 𝔎'" and 𝔎': "𝔎' : ℭ ↦↦⇩C⇘α⇙ 𝔇"
        by (auto intro: is_arrI)
      from assms αβ prems 𝔎' show
        "exp_cat_ntcf α 𝔇 (ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈⦇𝔎⦈ =
          (exp_cat_ntcf α 𝔇 𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cat_cf α 𝔇 ℌ)⦇NTMap⦈⦇𝔎⦈"
        by 
          (
            cs_concl 
              cs_simp: 
                cf_comp_cf_ntcf_comp_assoc cat_cs_simps cat_FUNCT_cs_simps 𝔎_def
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          )
    qed (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)

  qed
    (
      cs_concl
        cs_simp: exp_cat_cf_cf_comp cat_cs_simps cat_FUNCT_cs_simps
        cs_intro: αβ cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
    )+

qed

lemma exp_cat_ntcf_ntcf_vcomp:
  assumes "category α 𝔄" 
    and "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows
    "exp_cat_ntcf α 𝔄 (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) =
      exp_cat_ntcf α 𝔄 𝔐 ∙⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔄 𝔑"
proof-

  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔐: is_ntcf α 𝔅 ℭ 𝔊 ℌ 𝔐 by (rule assms(2))
  interpret 𝔑: is_ntcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(3))

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

  show ?thesis
  proof(rule ntcf_eqI)
    from β αβ show
      "exp_cat_ntcf α 𝔄 (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑) :
        exp_cat_cf α 𝔄 𝔉 ↦⇩C⇩F exp_cat_cf α 𝔄 ℌ :
        cat_FUNCT α ℭ 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔅 𝔄"
      by
        (
          cs_concl cs_intro: 
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ show
      "exp_cat_ntcf α 𝔄 𝔐 ∙⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔄 𝔑 :
        exp_cat_cf α 𝔄 𝔉 ↦⇩C⇩F exp_cat_cf α 𝔄 ℌ :
        cat_FUNCT α ℭ 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔅 𝔄"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ have dom_lhs: 
      "𝒟⇩∘ ((exp_cat_ntcf α 𝔄 (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑))⦇NTMap⦈) = cat_FUNCT α ℭ 𝔄⦇Obj⦈"
      by 
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from αβ have dom_rhs:
      "𝒟⇩∘ ((exp_cat_ntcf α 𝔄 𝔐 ∙⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔄 𝔑)⦇NTMap⦈) =
        cat_FUNCT α ℭ 𝔄⦇Obj⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )

    show 
      "exp_cat_ntcf α 𝔄 (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈ =
        (exp_cat_ntcf α 𝔄 𝔐 ∙⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔄 𝔑)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs cat_FUNCT_components(1))
      fix 𝔉' assume "𝔉' ∈⇩∘ cf_maps α ℭ 𝔄"
      then obtain 𝔉'' 
        where 𝔉'_def: "𝔉' = cf_map 𝔉''" and 𝔉'': "𝔉'' : ℭ ↦↦⇩C⇘α⇙ 𝔄" 
        by clarsimp
      from 𝔉'' αβ show
        "exp_cat_ntcf α 𝔄 (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈⦇𝔉'⦈ =
          (exp_cat_ntcf α 𝔄 𝔐 ∙⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔄 𝔑)⦇NTMap⦈⦇𝔉'⦈"
        by
          (
            cs_concl
              cs_simp:
                cat_cs_simps cat_FUNCT_cs_simps cf_ntcf_comp_ntcf_vcomp 𝔉'_def
              cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
          )
    qed (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)+

  qed simp_all

qed

text‹\newpage›

end