Theory CZH_SMC_FUNCT

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹FUNCT› and ‹Funct› as semicategories\label{sec:smc_FUNCT}›
theory CZH_SMC_FUNCT
  imports 
    CZH_DG_FUNCT
    CZH_Foundations.CZH_SMC_Subsemicategory
begin



subsection‹Background›


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

named_theorems smc_FUNCT_cs_simps
named_theorems smc_FUNCT_cs_intros

lemmas [smc_FUNCT_cs_simps] = cat_map_cs_simps
lemmas [smc_FUNCT_cs_intros] =  cat_map_cs_intros



subsection‹‹FUNCT››


subsubsection‹Definition and elementary properties›

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

text‹Components.›

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


text‹Slicing.›

lemma smc_dg_FUNCT: "smc_dg (smc_FUNCT α 𝔄 𝔅) = dg_FUNCT α 𝔄 𝔅"
proof(rule vsv_eqI)
  show "vsv (smc_dg (smc_FUNCT α 𝔄 𝔅))" unfolding smc_dg_def by auto
  show "vsv (dg_FUNCT α 𝔄 𝔅)" unfolding dg_FUNCT_def by auto
  have dom_lhs: "𝒟⇩∘ (smc_dg (smc_FUNCT α 𝔄 𝔅)) = 4⇩ℕ" 
    unfolding smc_dg_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (dg_FUNCT α 𝔄 𝔅) = 4⇩ℕ"
    unfolding dg_FUNCT_def by (simp add: nat_omega_simps)
  show "𝒟⇩∘ (smc_dg (smc_FUNCT α 𝔄 𝔅)) = 𝒟⇩∘ (dg_FUNCT α 𝔄 𝔅)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ (smc_dg (smc_FUNCT α 𝔄 𝔅)) ⟹ 
    smc_dg (smc_FUNCT α 𝔄 𝔅)⦇a⦈ = dg_FUNCT α 𝔄 𝔅⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral,
        unfold smc_dg_def dg_field_simps smc_FUNCT_def dg_FUNCT_def
      )
      (auto simp: nat_omega_simps)
qed

context is_ntcf
begin

lemmas_with [folded smc_dg_FUNCT, unfolded slicing_simps]: 
  smc_FUNCT_Dom_app = dg_FUNCT_Dom_app
  and smc_FUNCT_Cod_app = dg_FUNCT_Cod_app

end

lemmas [smc_FUNCT_cs_simps] = 
  is_ntcf.smc_FUNCT_Dom_app
  is_ntcf.smc_FUNCT_Cod_app

lemmas_with [folded smc_dg_FUNCT, unfolded slicing_simps]: 
  smc_FUNCT_Dom_vsv[intro] = dg_FUNCT_Dom_vsv
  and smc_FUNCT_Dom_vdomain[smc_FUNCT_cs_simps] = dg_FUNCT_Dom_vdomain
  and smc_FUNCT_Cod_vsv[intro] = dg_FUNCT_Cod_vsv
  and smc_FUNCT_Cod_vdomain[smc_FUNCT_cs_simps] = dg_FUNCT_Cod_vdomain
  and smc_FUNCT_Dom_vrange = dg_FUNCT_Dom_vrange
  and smc_FUNCT_Cod_vrange = dg_FUNCT_Cod_vrange
  and smc_FUNCT_is_arrI = dg_FUNCT_is_arrI
  and smc_FUNCT_is_arrI'[smc_FUNCT_cs_intros] = dg_FUNCT_is_arrI'
  and smc_FUNCT_is_arrD = dg_FUNCT_is_arrD
  and smc_FUNCT_is_arrE[elim] = dg_FUNCT_is_arrE



subsubsection‹Composable arrows›

lemma smc_FUNCT_composable_arrs_dg_FUNCT: 
  "composable_arrs (dg_FUNCT α 𝔄 𝔅) = composable_arrs (smc_FUNCT α 𝔄 𝔅)"
  unfolding composable_arrs_def smc_dg_FUNCT[symmetric] slicing_simps by auto

lemma smc_FUNCT_Comp: 
  "smc_FUNCT α 𝔄 𝔅⦇Comp⦈ =
    (λ𝔊𝔉∈⇩∘composable_arrs (smc_FUNCT α 𝔄 𝔅). 𝔊𝔉⦇0⦈ ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔊𝔉⦇1⇩ℕ⦈)"
  unfolding smc_FUNCT_components smc_FUNCT_composable_arrs_dg_FUNCT ..


subsubsection‹Composition›

lemma smc_FUNCT_Comp_vsv[intro]: "vsv (smc_FUNCT α 𝔄 𝔅⦇Comp⦈)" 
  unfolding smc_FUNCT_Comp by simp

lemma smc_FUNCT_Comp_vdomain:
  "𝒟⇩∘ (smc_FUNCT α 𝔄 𝔅⦇Comp⦈) = composable_arrs (smc_FUNCT α 𝔄 𝔅)" 
  unfolding smc_FUNCT_Comp by auto

lemma smc_FUNCT_Comp_app[smc_FUNCT_cs_simps]:
  assumes "𝔐 : 𝔊 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ ℌ" and "𝔑 : 𝔉 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔊"
  shows "𝔐 ∘⇩A⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔑 = 𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔑"
proof-
  from assms have "[𝔐, 𝔑]⇩∘ ∈⇩∘ composable_arrs (smc_FUNCT α 𝔄 𝔅)" 
    by (auto intro: smc_cs_intros)
  then show "𝔐 ∘⇩A⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔑 = 𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔑"
    unfolding smc_FUNCT_Comp by (simp add: nat_omega_simps)
qed

lemma smc_FUNCT_Comp_vrange: "ℛ⇩∘ (smc_FUNCT α 𝔄 𝔅⦇Comp⦈) ⊆⇩∘ ntcf_arrows α 𝔄 𝔅"
proof(rule vsubsetI)
  fix 𝔏 assume prems: "𝔏 ∈⇩∘ ℛ⇩∘ (smc_FUNCT α 𝔄 𝔅⦇Comp⦈)"
  then obtain 𝔐𝔑
    where 𝔏_def: "𝔏 = smc_FUNCT α 𝔄 𝔅⦇Comp⦈⦇𝔐𝔑⦈" 
      and "𝔐𝔑 ∈⇩∘ 𝒟⇩∘ (smc_FUNCT α 𝔄 𝔅⦇Comp⦈)"
    unfolding smc_FUNCT_components by (auto intro: smc_cs_intros)
  then obtain 𝔐 𝔑 𝔉 𝔊 ℌ 
    where "𝔐𝔑 = [𝔐, 𝔑]⇩∘" 
      and 𝔐: "𝔐 : 𝔊 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ ℌ" 
      and 𝔑: "𝔑 : 𝔉 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔊"
    by (auto simp: smc_FUNCT_Comp_vdomain) 
  with 𝔏_def have 𝔏_def': "𝔏 = 𝔐 ∘⇩A⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔑" by simp
  note 𝔐 = smc_FUNCT_is_arrD[OF 𝔐]
    and 𝔑 = smc_FUNCT_is_arrD[OF 𝔑]
  from 𝔐(1) 𝔑(1) show "𝔏 ∈⇩∘ ntcf_arrows α 𝔄 𝔅" 
    unfolding 𝔏_def'
    by (subst 𝔐(2), subst 𝔑(2), remdups)
      (
        cs_concl 
          cs_simp: smc_FUNCT_cs_simps cs_intro: cat_cs_intros smc_FUNCT_cs_intros
      )
qed


subsubsection‹‹FUNCT› is a semicategory›

lemma (in 𝒵) tiny_semicategory_smc_FUNCT: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_semicategory β (smc_FUNCT α 𝔄 𝔅)"
proof(intro tiny_semicategoryI)
  show "vfsequence (smc_FUNCT α 𝔄 𝔅)" by (simp add: smc_FUNCT_def)
  show "vcard (smc_FUNCT α 𝔄 𝔅) = 5⇩ℕ"
    unfolding smc_FUNCT_def by (simp add: nat_omega_simps)
  show "(𝔐𝔑 ∈⇩∘ 𝒟⇩∘ (smc_FUNCT α 𝔄 𝔅⦇Comp⦈)) =
    (
      ∃𝔐 𝔑 𝔊 ℌ 𝔉.
        𝔐𝔑 = [𝔐, 𝔑]⇩∘ ∧
        𝔐 : 𝔊 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ ℌ ∧
        𝔑 : 𝔉 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔊
    )"
    for 𝔐𝔑 
    unfolding smc_FUNCT_Comp by (auto intro: smc_cs_intros)
  show Comp_is_arr: "𝔐 ∘⇩A⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔑 : 𝔉 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ ℌ"
    if "𝔐 : 𝔊 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ ℌ" and "𝔑 : 𝔉 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔊"
    for 𝔐 𝔊 ℌ 𝔑 𝔉
  proof-
    note g = smc_FUNCT_is_arrD[OF that(1)]
    note f = smc_FUNCT_is_arrD[OF that(2)]
    from g(1) f(1) show "𝔐 ∘⇩A⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔑 : 𝔉 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ ℌ"
      by (subst g(2), subst g(4), subst f(2), subst f(3), remdups)
        (
          cs_concl cs_shallow
            cs_simp: smc_FUNCT_cs_simps
            cs_intro: smc_FUNCT_cs_intros cat_cs_intros
        )
  qed
  fix 𝔏 ℌ 𝔎 𝔐 𝔊 𝔑 𝔉
  assume prems:
    "𝔏 : ℌ ↦⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔎"
    "𝔐 : 𝔊 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ ℌ"
    "𝔑 : 𝔉 ↦⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔊"
  note 𝔏 = smc_FUNCT_is_arrD[OF prems(1)]
  note 𝔐 = smc_FUNCT_is_arrD[OF prems(2)]
  note 𝔑 = smc_FUNCT_is_arrD[OF prems(3)]
  from 𝔏(1) 𝔐(1) 𝔑(1) show 
    "(𝔏 ∘⇩A⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔐) ∘⇩A⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔑 =
      𝔏 ∘⇩A⇘smc_FUNCT α 𝔄 𝔅⇙ (𝔐 ∘⇩A⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔑)"    
    by (subst (1 2) 𝔏(2), subst (1 2) 𝔐(2), subst (1 2) 𝔑(2), remdups)
      (
        cs_concl 
          cs_simp: smc_FUNCT_cs_simps cat_cs_simps 
          cs_intro: smc_FUNCT_cs_intros cat_cs_intros
      )
qed 
  (
    simp_all add: 
      assms 
      smc_dg_FUNCT 
      smc_FUNCT_components 
      tiny_digraph_dg_FUNCT[OF assms(1,2)]  
  ) 



subsection‹‹Funct››


subsubsection‹Definition and elementary properties›

definition smc_Funct :: "V ⇒ V ⇒ V ⇒ V"
  where "smc_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⇩ℕ⦈)
    ]⇩∘"


text‹Components.›

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


text‹Slicing.›

lemma smc_dg_Funct: "smc_dg (smc_Funct α 𝔄 𝔅) = dg_Funct α 𝔄 𝔅"
proof(rule vsv_eqI)
  show "vsv (smc_dg (smc_Funct α 𝔄 𝔅))" unfolding smc_dg_def by auto
  show "vsv (dg_Funct α 𝔄 𝔅)" unfolding dg_Funct_def by auto
  have dom_lhs: "𝒟⇩∘ (smc_dg (smc_Funct α 𝔄 𝔅)) = 4⇩ℕ" 
    unfolding smc_dg_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (dg_Funct α 𝔄 𝔅) = 4⇩ℕ"
    unfolding dg_Funct_def by (simp add: nat_omega_simps)
  show "𝒟⇩∘ (smc_dg (smc_Funct α 𝔄 𝔅)) = 𝒟⇩∘ (dg_Funct α 𝔄 𝔅)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ (smc_dg (smc_Funct α 𝔄 𝔅)) ⟹
    smc_dg (smc_Funct α 𝔄 𝔅)⦇a⦈ = dg_Funct α 𝔄 𝔅⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral,
        unfold smc_dg_def dg_field_simps smc_Funct_def dg_Funct_def
      )
      (auto simp: nat_omega_simps)
qed

context is_tm_ntcf
begin

lemmas_with [folded smc_dg_Funct, unfolded slicing_simps]: 
  smc_Funct_Dom_app = dg_Funct_Dom_app
  and smc_Funct_Cod_app = dg_Funct_Cod_app

end

lemmas [smc_FUNCT_cs_simps] = 
  is_tm_ntcf.smc_Funct_Dom_app
  is_tm_ntcf.smc_Funct_Cod_app

lemmas_with [folded smc_dg_Funct, unfolded slicing_simps]: 
  smc_Funct_Dom_vsv[intro] = dg_Funct_Dom_vsv
  and smc_Funct_Dom_vdomain[smc_FUNCT_cs_simps] = dg_Funct_Dom_vdomain
  and smc_Funct_Cod_vsv[intro] = dg_Funct_Cod_vsv
  and smc_Funct_Cod_vdomain[smc_FUNCT_cs_simps] = dg_Funct_Cod_vdomain
  and smc_Funct_Dom_vrange = dg_Funct_Dom_vrange
  and smc_Funct_Cod_vrange = dg_Funct_Cod_vrange
  and smc_Funct_is_arrI = dg_Funct_is_arrI
  and smc_Funct_is_arrI'[smc_FUNCT_cs_intros] = dg_Funct_is_arrI'
  and smc_Funct_is_arrD = dg_Funct_is_arrD
  and smc_Funct_is_arrE[elim] = dg_Funct_is_arrE


subsubsection‹Composable arrows›

lemma smc_Funct_composable_arrs_dg_FUNCT: 
  "composable_arrs (dg_Funct α 𝔄 𝔅) = composable_arrs (smc_Funct α 𝔄 𝔅)"
  unfolding composable_arrs_def smc_dg_Funct[symmetric] slicing_simps by auto

lemma smc_Funct_Comp: 
  "smc_Funct α 𝔄 𝔅⦇Comp⦈ =
    (λ𝔊𝔉∈⇩∘composable_arrs (smc_Funct α 𝔄 𝔅). 𝔊𝔉⦇0⦈ ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔊𝔉⦇1⇩ℕ⦈)"
  unfolding smc_Funct_components smc_Funct_composable_arrs_dg_FUNCT ..


subsubsection‹Composition›

lemma smc_Funct_Comp_vsv[intro]: "vsv (smc_Funct α 𝔄 𝔅⦇Comp⦈)" 
  unfolding smc_Funct_Comp by simp

lemma smc_Funct_Comp_vdomain:
  "𝒟⇩∘ (smc_Funct α 𝔄 𝔅⦇Comp⦈) = composable_arrs (smc_Funct α 𝔄 𝔅)" 
  unfolding smc_Funct_Comp by auto

lemma smc_Funct_Comp_app[smc_FUNCT_cs_simps]:
  assumes "𝔐 : 𝔊 ↦⇘smc_Funct α 𝔄 𝔅⇙ ℌ" and "𝔑 : 𝔉 ↦⇘smc_Funct α 𝔄 𝔅⇙ 𝔊"
  shows "𝔐 ∘⇩A⇘smc_Funct α 𝔄 𝔅⇙ 𝔑 = 𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔑"
proof-
  from assms have "[𝔐, 𝔑]⇩∘ ∈⇩∘ composable_arrs (smc_Funct α 𝔄 𝔅)" 
    by (auto intro: smc_cs_intros)
  then show "𝔐 ∘⇩A⇘smc_Funct α 𝔄 𝔅⇙ 𝔑 = 𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔑"
    unfolding smc_Funct_Comp by (simp add: nat_omega_simps)
qed

lemma smc_Funct_Comp_vrange: 
  assumes "category α 𝔅"
  shows "ℛ⇩∘ (smc_Funct α 𝔄 𝔅⦇Comp⦈) ⊆⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
proof(rule vsubsetI)
  fix 𝔏 assume "𝔏 ∈⇩∘ ℛ⇩∘ (smc_Funct α 𝔄 𝔅⦇Comp⦈)"
  then obtain 𝔐𝔑
    where 𝔏_def: "𝔏 = smc_Funct α 𝔄 𝔅⦇Comp⦈⦇𝔐𝔑⦈" 
      and "𝔐𝔑 ∈⇩∘ 𝒟⇩∘ (smc_Funct α 𝔄 𝔅⦇Comp⦈)"
    unfolding smc_Funct_components 
    by (auto intro: smc_cs_intros)
  then obtain 𝔐 𝔑 𝔉 𝔊 ℌ 
    where "𝔐𝔑 = [𝔐, 𝔑]⇩∘" 
      and 𝔐: "𝔐 : 𝔊 ↦⇘smc_Funct α 𝔄 𝔅⇙ ℌ" 
      and 𝔑: "𝔑 : 𝔉 ↦⇘smc_Funct α 𝔄 𝔅⇙ 𝔊"
    by (auto simp: smc_Funct_Comp_vdomain) 
  with 𝔏_def have 𝔏_def': "𝔏 = 𝔐 ∘⇩A⇘smc_Funct α 𝔄 𝔅⇙ 𝔑" by simp
  note 𝔐 = smc_Funct_is_arrD[OF 𝔐]
    and 𝔑 = smc_Funct_is_arrD[OF 𝔑]
  from assms 𝔐(1) 𝔑(1) show "𝔏 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅" 
    unfolding 𝔏_def'
    by (subst 𝔐(2), use nothing in ‹subst 𝔑(2)›)
      (
        cs_concl  
          cs_simp: smc_FUNCT_cs_simps 
          cs_intro: smc_FUNCT_cs_intros cat_small_cs_intros
      )
qed


subsubsection‹‹Funct› is a semicategory›

lemma semicategory_smc_Funct:
  assumes "tiny_category α 𝔄" and "category α 𝔅"
  shows "semicategory α (smc_Funct α 𝔄 𝔅)" (is ‹semicategory α ?Funct›)
proof-
  interpret tiny_category α 𝔄 by (rule assms(1))
  show ?thesis
  proof(intro semicategoryI)
    show "vfsequence ?Funct" by (simp add: smc_Funct_def)
    show "vcard ?Funct = 5⇩ℕ" 
      unfolding smc_Funct_def by (simp add: nat_omega_simps)
    show "(𝔐𝔑 ∈⇩∘ 𝒟⇩∘ (smc_Funct α 𝔄 𝔅⦇Comp⦈)) =
      (∃𝔐 𝔑 𝔊 ℌ 𝔉. 𝔐𝔑 = [𝔐, 𝔑]⇩∘ ∧ 𝔐 : 𝔊 ↦⇘?Funct⇙ ℌ ∧ 𝔑 : 𝔉 ↦⇘?Funct⇙ 𝔊)"
      for 𝔐𝔑 
      unfolding smc_Funct_Comp by (auto intro: smc_cs_intros)
    show Comp_is_arr: "𝔐 ∘⇩A⇘?Funct⇙ 𝔑 : 𝔉 ↦⇘?Funct⇙ ℌ"
      if "𝔐 : 𝔊 ↦⇘?Funct⇙ ℌ" and "𝔑 : 𝔉 ↦⇘?Funct⇙ 𝔊"
      for 𝔐 𝔊 ℌ 𝔑 𝔉
    proof-
      note 𝔐 = smc_Funct_is_arrD[OF that(1)]
      note 𝔑 = smc_Funct_is_arrD[OF that(2)]
      from assms 𝔐(1) 𝔑(1) show 
        "𝔐 ∘⇩A⇘?Funct⇙ 𝔑 : 𝔉 ↦⇘?Funct⇙ ℌ"
        by (subst 𝔐(2), use nothing in ‹subst 𝔐(4), subst 𝔑(2), subst 𝔑(3)›)
          (
            cs_concl  
              cs_simp: smc_FUNCT_cs_simps 
              cs_intro: smc_FUNCT_cs_intros cat_small_cs_intros
          )
    qed
    show "𝔏 ∘⇩A⇘?Funct⇙ 𝔐 ∘⇩A⇘?Funct⇙ 𝔑 = 𝔏 ∘⇩A⇘?Funct⇙ (𝔐 ∘⇩A⇘?Funct⇙ 𝔑)"
      if "𝔏 : ℌ ↦⇘?Funct⇙ 𝔎" "𝔐 : 𝔊 ↦⇘?Funct⇙ ℌ" "𝔑 : 𝔉 ↦⇘?Funct⇙ 𝔊"
      for 𝔏 ℌ 𝔎 𝔐 𝔊 𝔑 𝔉
    proof-
      note 𝔏 = smc_Funct_is_arrD[OF that(1)]
      note 𝔐 = smc_Funct_is_arrD[OF that(2)]
      note 𝔑 = smc_Funct_is_arrD[OF that(3)]
      from assms 𝔏(1) 𝔐(1) 𝔑(1) show
        "(𝔏 ∘⇩A⇘?Funct⇙ 𝔐) ∘⇩A⇘?Funct⇙ 𝔑 = 𝔏 ∘⇩A⇘?Funct⇙ (𝔐 ∘⇩A⇘?Funct⇙ 𝔑)"    
        by 
          (
            subst (1 2) 𝔏(2),
            use nothing in ‹subst (1 2) 𝔐(2), subst (1 2) 𝔑(2)›
          )
          (
            cs_concl 
              cs_simp: smc_FUNCT_cs_simps cat_cs_simps cat_small_cs_simps 
              cs_intro: smc_FUNCT_cs_intros cat_cs_intros cat_small_cs_intros
          )
    qed
  qed (auto simp: assms smc_dg_Funct smc_Funct_components digraph_dg_Funct)
qed


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

lemma subsemicategory_smc_Funct_smc_FUNCT:
  assumes "𝒵 β" and "α ∈⇩∘ β" and "tiny_category α 𝔄" and "category α 𝔅"
  shows "smc_Funct α 𝔄 𝔅 ⊆⇩S⇩M⇩C⇘β⇙ smc_FUNCT α 𝔄 𝔅"
proof(intro subsemicategoryI, unfold smc_dg_FUNCT smc_dg_Funct)
  interpret category α 𝔅 by (rule assms(4))
  interpret smc_Funct: semicategory α ‹smc_Funct α 𝔄 𝔅›
    by (rule semicategory_smc_Funct[OF assms(3,4)])
  show "semicategory β (smc_Funct α 𝔄 𝔅)"
    by (rule semicategory.smc_semicategory_if_ge_Limit[OF _ assms(1,2)]) 
      (auto simp: smc_cs_simps intro: smc_cs_intros)
  from assms show "semicategory β (smc_FUNCT α 𝔄 𝔅)"
    by 
      (
        cs_concl 
          cs_intro: smc_small_cs_intros tiny_semicategory_smc_FUNCT
      )
  show "dg_Funct α 𝔄 𝔅 ⊆⇩D⇩G⇘β⇙ dg_FUNCT α 𝔄 𝔅"
    by (rule subdigraph_dg_Funct_dg_FUNCT[OF assms])
  show "𝔐 ∘⇩A⇘smc_Funct α 𝔄 𝔅⇙ 𝔑 = 𝔐 ∘⇩A⇘smc_FUNCT α 𝔄 𝔅⇙ 𝔑"
    if "𝔐 : 𝔊 ↦⇘smc_Funct α 𝔄 𝔅⇙ ℌ" and "𝔑 : 𝔉 ↦⇘smc_Funct α 𝔄 𝔅⇙ 𝔊"
    for 𝔊 ℌ 𝔐 𝔉 𝔑
  proof-
    note 𝔐 = smc_Funct_is_arrD[OF that(1)]
    note 𝔑 = smc_Funct_is_arrD[OF that(2)]
    from 𝔐(1) 𝔑(1) show ?thesis
      by (subst (1 2) 𝔐(2), use nothing in ‹subst (1 2) 𝔑(2)›)
        (
          cs_concl cs_shallow 
            cs_simp: smc_FUNCT_cs_simps cat_small_cs_simps 
            cs_intro: smc_FUNCT_cs_intros cat_small_cs_intros
        )
  qed
qed

text‹\newpage›

end