Theory CZH_ECAT_FUNCT

(* Copyright 2021 (C) Mihails Milehins *)

sectionFUNCT› 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



subsectionFUNCT›


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 α 𝔄 𝔅). 𝔐𝔑0NTCF𝔄,𝔅𝔐𝔑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 α 𝔄 𝔅). 𝔐𝔑0NTCF𝔄,𝔅𝔐𝔑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 𝔐': "𝔐' : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα𝔅"
    by auto
  from prems(2) obtain 𝔑' 𝔉' 𝔊' 
    where 𝔑_def: "𝔑 = ntcf_arrow 𝔑'" and 𝔑': "𝔑' : 𝔉' CF 𝔊' : 𝔄 ↦↦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 𝔐'': "𝔐'' : 𝔉 CF 𝔊 : 𝔄 ↦↦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 𝔐: "𝔐 : 𝔉 CF 𝔊 : 𝔄 ↦↦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 𝔑: "𝔑 : 𝔉 CF 𝔊 : 𝔄 ↦↦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


subsubsectionFUNCT› 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: "?FUNCTCId𝔉' : 𝔉' ?FUNCT𝔉'" if "𝔉'  ?FUNCTObj" 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 "?FUNCTCId𝔊 A?FUNCT𝔑 = 𝔑" if "𝔑 : 𝔉 ?FUNCT𝔊" for 𝔑 𝔉 𝔊
  proof-
    from that obtain 𝔑' 𝔉' 𝔊' 
      where 𝔑': "𝔑' : 𝔉' CF 𝔊' : 𝔄 ↦↦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𝔊 Acat_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?FUNCTCId𝔊 = 𝔑" if "𝔑 : 𝔊 ?FUNCT" for 𝔑 𝔊 
  proof-
    note 𝔑 = cat_FUNCT_is_arrD[OF that]
    from 𝔑(1) show "𝔑 Acat_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 "𝔑 : 𝔉 CF.iso 𝔊 : 𝔄 ↦↦Cα𝔅"
  shows "ntcf_arrow 𝔑 : cf_map 𝔉 isocat_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 𝔑) Acat_FUNCT α 𝔄 𝔅ntcf_arrow 𝔑 = 
      cat_FUNCT α 𝔄 𝔅CIdcf_map 𝔉"
    "ntcf_arrow 𝔑 Acat_FUNCT α 𝔄 𝔅ntcf_arrow (inv_ntcf 𝔑) = 
      cat_FUNCT α 𝔄 𝔅CIdcf_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 "𝔑 : 𝔉 CF.iso 𝔊 : 𝔄 ↦↦Cα𝔅"
    and "𝔑' = ntcf_arrow 𝔑" 
    and "𝔉' = cf_map 𝔉"
    and "𝔊' = cf_map 𝔊"
  shows "𝔑' : 𝔉' isocat_FUNCT α 𝔄 𝔅cf_map 𝔊"
  using assms(1) unfolding assms(2-4) by (rule cat_FUNCT_is_iso_arrI)

lemma cat_FUNCT_is_iso_arrD:
  assumes "𝔑 : 𝔉 isocat_FUNCT α 𝔄 𝔅𝔊" (is 𝔑 : 𝔉 iso?FUNCT𝔊)
  shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
    cf_of_cf_map 𝔄 𝔅 𝔉 CF.iso 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: 𝔊 iso?FUNCT𝔉"
    and inv_𝔑_𝔑: "𝔑¯C?FUNCTA?FUNCT𝔑 = ?FUNCTCId𝔉"
    and 𝔑_inv_𝔑: "𝔑 A?FUNCT𝔑¯C?FUNCT= ?FUNCTCId𝔊"
    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 𝔄 𝔅 (𝔑¯Ccat_FUNCT α 𝔄 𝔅)
  from inv_𝔑_𝔑 𝔑_is_arr(1) inv_𝔑_is_arr(1) have inv_𝔑_𝔑:
    "?inv_𝔑 NTCF ?𝔑 = 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_𝔑:
    "?𝔑 NTCF ?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 𝔄 𝔅 𝔉 CF.iso 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



subsectionFunct›


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 α 𝔄 𝔅). 𝔐𝔑0NTCF𝔄,𝔅𝔐𝔑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 α 𝔄 𝔅). 𝔐𝔑0NTCF𝔄,𝔅𝔐𝔑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.tmα𝔅"
    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


subsubsectionFunct› 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.tmα𝔅" 
        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𝔊 Acat_Funct α 𝔄 𝔅𝔑 = 𝔑"
      if "𝔑 : 𝔉 cat_Funct α 𝔄 𝔅𝔊" for 𝔉 𝔊 𝔑
    proof-
      note 𝔑 = cat_Funct_is_arrD[OF that]
      from assms 𝔑(1) show
        "cat_Funct α 𝔄 𝔅CId𝔊 Acat_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 "𝔑 Acat_Funct α 𝔄 𝔅cat_Funct α 𝔄 𝔅CId𝔊 = 𝔑"
      if "𝔑 : 𝔊 cat_Funct α 𝔄 𝔅" for 𝔊  𝔑
    proof-
      note 𝔑 = cat_Funct_is_arrD[OF that]
      from assms 𝔑(1) show 
        "𝔑 Acat_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)


subsubsectionFunct› 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 α 𝔄 𝔅 SMCβ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.tmα𝔅"
      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 𝔉 isocat_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 𝔑) Acat_Funct α 𝔄 𝔅ntcf_arrow 𝔑 =
      cat_Funct α 𝔄 𝔅CIdcf_map 𝔉"
    "ntcf_arrow 𝔑 Acat_Funct α 𝔄 𝔅ntcf_arrow (inv_ntcf 𝔑) =
      cat_Funct α 𝔄 𝔅CIdcf_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 "𝔑' : 𝔉' isocat_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 "𝔑 : 𝔉 isocat_Funct α 𝔄 𝔅𝔊" (is 𝔑 : 𝔉 iso?Funct𝔊)
  shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
    cf_of_cf_map 𝔄 𝔅 𝔉 CF.tm.iso cf_of_cf_map 𝔄 𝔅 𝔊 : 𝔄 ↦↦C.tmα𝔅" 
    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: 𝔊 iso?Funct𝔉"
    and inv_𝔑_𝔑: "𝔑¯C?FunctA?Funct𝔑 = ?FunctCId𝔉"
    and 𝔑_inv_𝔑: "𝔑 A?Funct𝔑¯C?Funct= ?FunctCId𝔊"
    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 𝔄 𝔅 (𝔑¯Ccat_Funct α 𝔄 𝔅)
  from inv_𝔑_𝔑 𝔑_is_arr(1) inv_𝔑_is_arr(1) have inv_𝔑_𝔑:
    "?inv_𝔑 NTCF ?𝔑 = 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_𝔑:
    "?𝔑 NTCF ?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 𝔄 𝔅 𝔉 CF.tm.iso cf_of_cf_map 𝔄 𝔅 𝔊 : 𝔄 ↦↦C.tmα𝔅"
    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" (ΔCF)
  where "ΔCF α 𝔍  =
    [
      (λaObj. cf_map (cf_const 𝔍  a)),
      (λfArr. ntcf_arrow (ntcf_const 𝔍  f)), 
      ,
      cat_FUNCT α 𝔍 
    ]"


text‹Components.›

lemma cf_diagonal_components:
  shows "ΔCF α 𝔍 ObjMap = (λaObj. cf_map (cf_const 𝔍  a))"
    and "ΔCF α 𝔍 ArrMap = (λfArr. ntcf_arrow (ntcf_const 𝔍  f))"
    and "ΔCF α 𝔍 HomDom = "
    and "ΔCF α 𝔍 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 " (ΔCF α 𝔍 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 "ΔCF α 𝔍  :  ↦↦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)  ?FUNCTObj"
      by (rule cf_diagonal_ObjMap_vrange)
    show "ArrMapf : ObjMapa ?FUNCTObjMapb"
      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 "ArrMapg Af = ArrMapg A?FUNCTArrMapf"
      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 
      "ArrMapCIdc = ?FUNCTCIdObjMapc"
      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 "ΔCF α 𝔍  : 𝔄' ↦↦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" (ΔCF.tm) 
  where "ΔCF.tm α 𝔍  =
    [
      (λaObj. cf_map (cf_const 𝔍  a)),
      (λfArr. ntcf_arrow (ntcf_const 𝔍  f)), 
      ,
      cat_Funct α 𝔍 
    ]"


text‹Components.›

lemma tm_cf_diagonal_components:
  shows "ΔCF.tm α 𝔍 ObjMap = (λaObj. cf_map (cf_const 𝔍  a))"
    and "ΔCF.tm α 𝔍 ArrMap = (λfArr. ntcf_arrow (ntcf_const 𝔍  f))"
    and "ΔCF.tm α 𝔍 HomDom = "
    and "ΔCF.tm α 𝔍 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 " (ΔCF.tm α 𝔍 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 "ΔCF.tm α 𝔍  :  ↦↦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)  ?FunctObj"
      by (rule tm_cf_diagonal_ObjMap_vrange)
    show "ArrMapf : ObjMapa ?FunctObjMapb"
      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 "ArrMapg Af = ArrMapg A?FunctArrMapf"
      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 
      "ArrMapCIdc = ?FunctCIdObjMapc"
      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 "ΔCF.tm α 𝔍  : 𝔄 ↦↦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 (𝔎 CF cf_of_cf_map 𝔄 (𝔎HomDom) 𝔖)
      ),
      (
        λσcat_FUNCT α 𝔄 (𝔎HomDom)Arr.
          ntcf_arrow (𝔎 CF-NTCF 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 (𝔎 CF cf_of_cf_map 𝔄 (𝔎HomDom) 𝔖)
    )"
    and 
    "exp_cf_cat α 𝔎 𝔄ArrMap =
      (
        λσcat_FUNCT α 𝔄 (𝔎HomDom)Arr.
          ntcf_arrow  (𝔎 CF-NTCF (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.tinyβ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 (𝔎 CF 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𝔐 Acat_FUNCT α 𝔄 𝔅𝔑 =
        exp_cf_cat α 𝔎 𝔄ArrMap𝔐 Acat_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 α 𝔎 𝔄ArrMapcat_FUNCT α 𝔄 𝔅CId𝔉 =
        cat_FUNCT α 𝔄 CIdexp_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 α 𝔎 𝔄ArrMapcat_FUNCT α 𝔄 𝔅CId𝔉 =
          cat_FUNCT α 𝔄 CIdexp_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.tinyβ𝔅'"
  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 α (𝔊 CF 𝔉) 𝔇 = exp_cf_cat α 𝔊 𝔇 CF 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 α (𝔊 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 αβ show 
    "exp_cf_cat α 𝔊 𝔇 CF 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 α (𝔊 CF 𝔉) 𝔇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 α 𝔊 𝔇 CF 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 α (𝔊 CF 𝔉) 𝔇ObjMap =
      (exp_cf_cat α 𝔊 𝔇 CF exp_cf_cat α 𝔉 𝔇)ObjMap"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    show "vsv (exp_cf_cat α (𝔊 CF 𝔉) 𝔇ObjMap)"
      by (cs_concl cs_shallow cs_intro: cat_FUNCT_cs_intros)
    from αβ show "vsv ((exp_cf_cat α 𝔊 𝔇 CF 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 α (𝔊 CF 𝔉) 𝔇ObjMap =
        (exp_cf_cat α 𝔊 𝔇 CF 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 α (𝔊 CF 𝔉) 𝔇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 α 𝔊 𝔇 CF 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 α (𝔊 CF 𝔉) 𝔇ArrMap =
      (exp_cf_cat α 𝔊 𝔇 CF exp_cf_cat α 𝔉 𝔇)ArrMap"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    show "vsv (exp_cf_cat α (𝔊 CF 𝔉) 𝔇ArrMap)"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_FUNCT_cs_intros)
    from αβ show "vsv ((exp_cf_cat α 𝔊 𝔇 CF 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 α (𝔊 CF 𝔉) 𝔇ArrMap𝔑 =
        (exp_cf_cat α 𝔊 𝔇 CF 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 α 𝔉 𝔄 CF 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 α 𝔉 𝔄 CF 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 α 𝔉 𝔄 CF 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 α 𝔉 𝔄 CF 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 α 𝔉 𝔄 CF 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 α 𝔉 𝔄 CF 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 α 𝔉 𝔄 CF 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 α 𝔉 𝔄 CF 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 ) 𝔄 CF 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 ) 𝔄 CF 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 ) 𝔄 CF 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 ) 𝔄 CF 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 ) 𝔄 CF 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 ) 𝔄 CF 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 ) 𝔄 CF 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 ) 𝔄 CF 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) 𝔄 𝔖 CF 𝔎)
      ),
      (
        λσcat_FUNCT α (𝔎HomCod) 𝔄Arr.
          ntcf_arrow (ntcf_of_ntcf_arrow (𝔎HomCod) 𝔄 σ NTCF-CF 𝔎)
      ),
      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) 𝔄 𝔖 CF 𝔎)
    )"
    and "exp_cat_cf α 𝔄 𝔎ArrMap = 
    (
      λσcat_FUNCT α (𝔎HomCod) 𝔄Arr.
        ntcf_arrow (ntcf_of_ntcf_arrow (𝔎HomCod) 𝔄 σ NTCF-CF 𝔎)
    )"
    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.tinyβ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  𝔄 𝔉 CF 𝔎)  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𝔐 Acat_FUNCT α  𝔄𝔑 =
        exp_cat_cf α 𝔄 𝔎ArrMap𝔐 Acat_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 α 𝔄 𝔎ArrMapcat_FUNCT α  𝔄CId𝔉 =
        cat_FUNCT α 𝔅 𝔄CIdexp_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