Theory CZH_DG_FUNCT

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹FUNCT› and ‹Funct› as digraphs\label{sec:dg_FUNCT}›
theory CZH_DG_FUNCT
  imports 
    CZH_ECAT_Small_NTCF
    CZH_Foundations.CZH_DG_Subdigraph
begin



subsection‹Background›


text‹
A general reference for this section is Chapter II-4 in 
\<^cite>‹"mac_lane_categories_2010"›.
›

named_theorems dg_FUNCT_cs_simps
named_theorems dg_FUNCT_cs_intros
named_theorems cat_map_cs_simps
named_theorems cat_map_cs_intros
named_theorems cat_map_extra_cs_simps



subsection‹Functor map›


subsubsection‹Definition and elementary properties›

definition cf_map :: "V ⇒ V"
  where "cf_map 𝔉 = [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈]⇩∘"

abbreviation cf_maps :: "V ⇒ V ⇒ V ⇒ V"
  where "cf_maps α 𝔄 𝔅 ≡ set {cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"

abbreviation tm_cf_maps :: "V ⇒ V ⇒ V ⇒ V"
  where "tm_cf_maps α 𝔄 𝔅 ≡ set {cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅}"

lemma tm_cf_maps_subset_cf_maps:
  "{cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅} ⊆ {cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
  by auto


text‹Components.›

lemma cf_map_components[cat_map_cs_simps]:
  shows "cf_map 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
    and "cf_map 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
  unfolding cf_map_def dghm_field_simps by (simp_all add: nat_omega_simps)


text‹Sequence characterization.›

lemma dg_FUNCT_Obj_components:
  shows "[FOM, FAM]⇩∘⦇ObjMap⦈ = FOM"
    and "[FOM, FAM]⇩∘⦇ArrMap⦈ = FAM"
  unfolding dghm_field_simps by (simp_all add: nat_omega_simps)

lemma cf_map_vfsequence[cat_map_cs_intros]: "vfsequence (cf_map 𝔉)"
  unfolding cf_map_def by auto

lemma cf_map_vdomain[cat_map_cs_simps]: "𝒟⇩∘ (cf_map 𝔉) = 2⇩ℕ"
  unfolding cf_map_def by (simp add: nat_omega_simps)

lemma (in is_functor) cf_map_vsubset_cf: "cf_map 𝔉 ⊆⇩∘ 𝔉"
  by (unfold cf_map_def, subst (3) cf_def)
    (cs_concl cs_shallow cs_intro: vcons_vsubset' V_cs_intros)


text‹Size.›

lemma (in is_functor) cf_map_ObjMap_in_Vset:
  assumes "α ∈⇩∘ β"
  shows "cf_map 𝔉⦇ObjMap⦈ ∈⇩∘ Vset β"
  using assms unfolding cf_map_components by (intro cf_ObjMap_in_Vset)

lemma (in is_tm_functor) tm_cf_map_ObjMap_in_Vset: "cf_map 𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
  unfolding cf_map_components by (rule tm_cf_ObjMap_in_Vset)

lemma (in is_functor) cf_map_ArrMap_in_Vset:
  assumes "α ∈⇩∘ β"
  shows "cf_map 𝔉⦇ArrMap⦈ ∈⇩∘ Vset β"
  using assms unfolding cf_map_components by (intro cf_ArrMap_in_Vset)

lemma (in is_tm_functor) tm_cf_map_ArrMap_in_Vset: "cf_map 𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
  unfolding cf_map_components by (rule tm_cf_ArrMap_in_Vset)

lemma (in is_functor) cf_map_in_Vset_4: "cf_map 𝔉 ∈⇩∘ Vset (α + 4⇩ℕ)"
proof-
  note [folded VPow_iff, folded Vset_succ[OF Ord_α], cat_cs_intros] =
    cf_ObjMap_vsubset_Vset 
    cf_ArrMap_vsubset_Vset
  show ?thesis
    by (subst cf_map_def, succ_of_numeral)
      (
        cs_concl 
          cs_simp: plus_V_succ_right V_cs_simps 
          cs_intro: cat_cs_intros V_cs_intros
      )
qed

lemma (in is_tm_functor) tm_cf_map_in_Vset: "cf_map 𝔉 ∈⇩∘ Vset α"
  using tm_cf_ObjMap_in_Vset tm_cf_ArrMap_in_Vset unfolding cf_map_def
  by (cs_concl cs_shallow cs_intro: V_cs_intros)

lemma (in is_functor) cf_map_in_Vset: 
  assumes "𝒵 β" and "α ∈⇩∘ β"  
  shows "cf_map 𝔉 ∈⇩∘ Vset β"
  using assms cf_map_in_Vset_4 cf_map_vsubset_cf  
  by (auto intro!: cf_in_Vset)

lemma cf_maps_subset_Vset:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "{cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅} ⊆ elts (Vset β)"
proof(intro subsetI, unfold mem_Collect_eq, elim exE conjE)
  fix x 𝔉 assume x_def: "x = cf_map 𝔉" and 𝔉: "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  interpret is_functor α 𝔄 𝔅 𝔉 by (rule 𝔉)
  show "x ∈⇩∘ Vset β" unfolding x_def by (rule cf_map_in_Vset[OF assms])
qed

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

lemma small_tm_cf_maps[simp]: "small {cf_map 𝔉 | 𝔉. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅}"
  by (rule smaller_than_small[OF small_cf_maps tm_cf_maps_subset_cf_maps])

lemma (in 𝒵) cf_maps_in_Vset: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "cf_maps α 𝔄 𝔅 ∈⇩∘ Vset β"
proof(rule vsubset_in_VsetI)
  interpret β: 𝒵 β by (rule assms(1))
  show "cf_maps α 𝔄 𝔅 ⊆⇩∘ Vset (α + 4⇩ℕ)"
  proof(intro vsubsetI)
    fix 𝔉 assume "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅"
    then obtain 𝔄 𝔅 𝔉' where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉: "𝔉' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
      by auto
    interpret is_functor α 𝔄 𝔅 𝔉' using 𝔉 by simp
    show "𝔉 ∈⇩∘ Vset (α + 4⇩ℕ)" unfolding 𝔉_def by (rule cf_map_in_Vset_4)
  qed
  from assms(2) show "Vset (α + 4⇩ℕ) ∈⇩∘ Vset β"
    by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed

lemma (in 𝒵) tm_cf_maps_vsubset_Vset: "tm_cf_maps α 𝔄 𝔅 ⊆⇩∘ Vset α"
proof(intro vsubsetI)
  fix 𝔉 assume "𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
  then obtain 𝔄 𝔅 𝔉' 
    where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉: "𝔉' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    by auto
  then show "𝔉 ∈⇩∘ Vset α" by (force simp: is_tm_functor.tm_cf_map_in_Vset)
qed


text‹Rules.›

lemma (in is_functor) cf_mapsI: "cf_map 𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅" 
  by (auto intro: cat_cs_intros)

lemma (in is_tm_functor) tm_cf_mapsI: "cf_map 𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
  by (auto intro: cat_small_cs_intros)

lemma (in is_functor) cf_mapsI':
  assumes "𝔉' = cf_map 𝔉"
  shows "𝔉' ∈⇩∘ cf_maps α 𝔄 𝔅" 
  unfolding assms by (rule cf_mapsI)

lemma (in is_tm_functor) tm_cf_mapsI':
  assumes "𝔉' = cf_map 𝔉"
  shows "𝔉' ∈⇩∘ tm_cf_maps α 𝔄 𝔅" 
  unfolding assms by (rule tm_cf_mapsI)

lemmas [cat_map_cs_intros] = 
  is_functor.cf_mapsI

lemmas cf_mapsI'[cat_map_cs_intros] = 
  is_functor.cf_mapsI'[rotated]

lemmas [cat_map_cs_intros] = 
  is_tm_functor.tm_cf_mapsI

lemmas tm_cf_mapsI'[cat_map_cs_intros] = 
  is_tm_functor.tm_cf_mapsI'[rotated]

lemma cf_mapsE[elim]:
  assumes "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅"
  obtains 𝔊 where "𝔉 = cf_map 𝔊" and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  using assms by force

lemma tm_cf_mapsE[elim]:
  assumes "𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
  obtains 𝔊 where "𝔉 = cf_map 𝔊" and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  using assms by force


text‹The opposite functor map.›

lemma (in is_functor) cf_map_op_cf[cat_op_simps]: "cf_map (op_cf 𝔉) = cf_map 𝔉"
proof(rule vsv_eqI, unfold cat_map_cs_simps)
  show "a ∈⇩∘ 2⇩ℕ ⟹ cf_map (op_cf 𝔉)⦇a⦈ = cf_map 𝔉⦇a⦈" for a
    by 
      (
        elim_in_numeral, 
        unfold dghm_field_simps[symmetric] cf_map_components cat_op_simps
      )
      simp_all
qed (auto intro: cat_map_cs_intros)

lemmas [cat_op_simps] = is_functor.cf_map_op_cf


text‹Elementary properties.›

lemma tm_cf_maps_vsubset_cf_maps: "tm_cf_maps α 𝔄 𝔅 ⊆⇩∘ cf_maps α 𝔄 𝔅"
  using tm_cf_maps_subset_cf_maps by simp

lemma tm_cf_maps_in_cf_maps:
  assumes "𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
  shows "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅"
  using assms tm_cf_maps_vsubset_cf_maps[of α 𝔄 𝔅] by blast

lemma cf_map_inj:
  assumes "cf_map 𝔉 = cf_map 𝔊" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔉 = 𝔊"
proof(rule cf_eqI)
  from assms(1) have ObjMap: "cf_map 𝔉⦇ObjMap⦈ = cf_map 𝔊⦇ObjMap⦈" 
    and ArrMap: "cf_map 𝔉⦇ArrMap⦈ = cf_map 𝔊⦇ArrMap⦈" 
    by auto
  from ObjMap show "𝔉⦇ObjMap⦈ = 𝔊⦇ObjMap⦈" unfolding cf_map_components by simp
  from ArrMap show "𝔉⦇ArrMap⦈ = 𝔊⦇ArrMap⦈" unfolding cf_map_components by simp
qed (auto intro: assms(2,3))

lemma cf_map_eq_iff[cat_map_cs_simps]: 
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "cf_map 𝔉 = cf_map 𝔊 ⟷ 𝔉 = 𝔊"
  using cf_map_inj[OF _ assms] by auto

lemma cf_map_eqI:
  assumes "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅" 
    and "𝔊 ∈⇩∘ cf_maps α 𝔄 𝔅"
    and "𝔉⦇ObjMap⦈ = 𝔊⦇ObjMap⦈"
    and "𝔉⦇ArrMap⦈ = 𝔊⦇ArrMap⦈"
  shows "𝔉 = 𝔊"
proof-
  from assms(1) obtain 𝔉' 
    where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉': "𝔉' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by auto
  from assms(2) obtain 𝔊'
    where 𝔊_def: "𝔊 = cf_map 𝔊'" and 𝔊': "𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by auto
  show ?thesis
  proof(rule vsv_eqI, unfold 𝔉_def 𝔊_def)
    show "a ∈⇩∘ 𝒟⇩∘ (cf_map 𝔉') ⟹ cf_map 𝔉'⦇a⦈ = cf_map 𝔊'⦇a⦈" for a
      by 
        (
          unfold cf_map_vdomain,
          elim_in_numeral,
          insert assms(3,4),
          unfold 𝔉_def 𝔊_def
        )
        (auto simp: dghm_field_simps)
  qed (auto simp: cat_map_cs_simps intro: cat_map_cs_intros)
qed



subsection‹Conversion of a functor map to a functor›


subsubsection‹Definition and elementary properties›

definition cf_of_cf_map :: "V ⇒ V ⇒ V ⇒ V"
  where "cf_of_cf_map 𝔄 𝔅 𝔉 = [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔄, 𝔅]⇩∘"


text‹Components.›

lemma cf_of_cf_map_components:
  shows "cf_of_cf_map 𝔄 𝔅 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
    and "cf_of_cf_map 𝔄 𝔅 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
    and "cf_of_cf_map 𝔄 𝔅 𝔉⦇HomDom⦈ = 𝔄"
    and "cf_of_cf_map 𝔄 𝔅 𝔉⦇HomCod⦈ = 𝔅"
  unfolding cf_of_cf_map_def dghm_field_simps by (simp_all add: nat_omega_simps)

lemmas [cat_map_extra_cs_simps] = cf_of_cf_map_components(1-2)
lemmas [cat_map_cs_simps] = cf_of_cf_map_components(3-4)


subsubsection‹The conversion of a functor map to a functor is a functor›

lemma (in is_functor) cf_of_cf_map_is_functor: 
  "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉) : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof(rule is_functorI')
  show "vfsequence (cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉))"
    unfolding cf_of_cf_map_def by simp
  show "vcard (cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)) = 4⇩ℕ"
    unfolding cf_of_cf_map_def by (simp add: nat_omega_simps)
  show
    "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇f⦈ :
      cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙
      cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇b⦈"
    if "f : a ↦⇘𝔄⇙ b" for a b f 
    unfolding cf_of_cf_map_components cf_map_components
    using is_functor_axioms that 
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show 
    "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ =
      cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙
      cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇f⦈"
    if "g : b ↦⇘𝔄⇙ c" and "f : a ↦⇘𝔄⇙ b" for b c g a f
    using is_functor_axioms that 
    unfolding cf_of_cf_map_components cf_map_components
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  show 
    "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = 
      𝔅⦇CId⦈⦇cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇c⦈⦈"
    if "c ∈⇩∘ 𝔄⦇Obj⦈" for c
    using is_functor_axioms that 
    unfolding cf_of_cf_map_components cf_map_components
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
qed 
  (
    auto simp: 
      cat_cs_simps 
      cf_of_cf_map_components 
      cf_map_components 
      cf_ObjMap_vrange
      intro: cat_cs_intros
  )

lemma (in is_functor) cf_of_cf_map_is_functor': 
  assumes "𝔉' = cf_map 𝔉"
    and "𝔄' = 𝔄"
    and "𝔅' = 𝔅"
  shows "cf_of_cf_map 𝔄 𝔅 𝔉' : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
  unfolding assms by (rule cf_of_cf_map_is_functor)

lemmas [cat_map_cs_intros] = is_functor.cf_of_cf_map_is_functor'


subsubsection‹The value of the conversion of a functor map to a functor›

lemma (in is_functor) cf_of_cf_map_of_cf_map[cat_map_cs_simps]:
  "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉) = 𝔉"
proof(rule cf_eqI)
  show "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉) : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  proof(rule is_functorI')
    show "vfsequence (cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉))"
      unfolding cf_of_cf_map_def by auto
    show "vcard (cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)) = 4⇩ℕ"
      unfolding cf_of_cf_map_def by (simp add: nat_omega_simps)
    show
      "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇f⦈ :
        cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙
        cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇b⦈"
      if "f : a ↦⇘𝔄⇙ b" for a b f 
      unfolding cf_of_cf_map_components cf_map_components
      using is_functor_axioms that 
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    show 
      "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ =
        cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙
        cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇f⦈"
      if "g : b ↦⇘𝔄⇙ c" and "f : a ↦⇘𝔄⇙ b" for b c g a f
      unfolding cf_of_cf_map_components cf_map_components
      using is_functor_axioms that 
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    show 
      "cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ =
        𝔅⦇CId⦈⦇cf_of_cf_map 𝔄 𝔅 (cf_map 𝔉)⦇ObjMap⦈⦇c⦈⦈"
      if "c ∈⇩∘ 𝔄⦇Obj⦈" for c
      unfolding cf_of_cf_map_components cf_map_components
      using is_functor_axioms that 
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  qed 
    (
      auto simp: 
        cat_cs_simps 
        cf_of_cf_map_components 
        cf_map_components 
        cf_ObjMap_vrange 
        intro: cat_cs_intros
    )
qed (auto simp: cf_of_cf_map_components cf_map_components intro: cat_cs_intros)

lemmas [cat_map_cs_simps] = is_functor.cf_of_cf_map_of_cf_map



subsection‹Natural transformation arrow›


subsubsection‹Definition and elementary properties›

definition ntcf_arrow :: "V ⇒ V"
  where "ntcf_arrow 𝔑 = [𝔑⦇NTMap⦈, cf_map (𝔑⦇NTDom⦈), cf_map (𝔑⦇NTCod⦈)]⇩∘"

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

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

lemma tm_ntcf_arrows_subset_ntcf_arrows:
  "{ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅} ⊆
    {ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
  by auto


text‹Components.›

lemma ntcf_arrow_components:
  shows [cat_map_cs_simps]: "ntcf_arrow 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
    and "ntcf_arrow 𝔑⦇NTDom⦈ = cf_map (𝔑⦇NTDom⦈)"
    and "ntcf_arrow 𝔑⦇NTCod⦈ = cf_map (𝔑⦇NTCod⦈)"
  unfolding ntcf_arrow_def nt_field_simps by (simp_all add: nat_omega_simps)

lemma (in is_ntcf) ntcf_arrow_components':
  shows "ntcf_arrow 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
    and "ntcf_arrow 𝔑⦇NTDom⦈ = cf_map 𝔉"
    and "ntcf_arrow 𝔑⦇NTCod⦈ = cf_map 𝔊"
  unfolding ntcf_arrow_components ntcf_NTDom ntcf_NTCod by simp_all

lemmas [cat_map_cs_simps] = is_ntcf.ntcf_arrow_components'(2,3)


text‹Elementary properties.›

lemma dg_FUNCT_Arr_components:
  shows "[NTM, NTD, NTC]⇩∘⦇NTMap⦈ = NTM"
    and "[NTM, NTD, NTC]⇩∘⦇NTDom⦈ = NTD"
    and "[NTM, NTD, NTC]⇩∘⦇NTCod⦈ = NTC"
  unfolding nt_field_simps by (simp_all add: nat_omega_simps)

lemma ntcf_arrow_vfsequence[cat_map_cs_intros]: "vfsequence (ntcf_arrow 𝔑)"
  unfolding ntcf_arrow_def by simp

lemma ntcf_arrow_vdomain[cat_map_cs_simps]: "𝒟⇩∘ (ntcf_arrow 𝔑) = 3⇩ℕ"
  unfolding ntcf_arrow_def by (simp add: nat_omega_simps)


text‹Size.›

lemma (in is_ntcf) ntcf_arrow_NTMap_in_Vset:
  assumes "α ∈⇩∘ β"
  shows "ntcf_arrow 𝔑⦇NTMap⦈ ∈⇩∘ Vset β"
  using assms unfolding ntcf_arrow_components by (intro ntcf_NTMap_in_Vset)

lemma (in is_tm_ntcf) tm_ntcf_arrow_NTMap_in_Vset:
  "ntcf_arrow 𝔑⦇NTMap⦈ ∈⇩∘ Vset α"
  unfolding ntcf_arrow_components by (rule tm_ntcf_NTMap_in_Vset)

lemma (in is_ntcf) ntcf_arrow_NTDom_in_Vset:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "ntcf_arrow 𝔑⦇NTDom⦈ ∈⇩∘ Vset β"
  using assms unfolding ntcf_arrow_components' by (rule NTDom.cf_map_in_Vset)

lemma (in is_tm_ntcf) tm_ntcf_arrow_NTDom_in_Vset: 
  "ntcf_arrow 𝔑⦇NTDom⦈ ∈⇩∘ Vset α"
  unfolding ntcf_arrow_components' by (rule NTDom.tm_cf_map_in_Vset)

lemma (in is_ntcf) ntcf_arrow_NTCod_in_Vset:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "ntcf_arrow 𝔑⦇NTCod⦈ ∈⇩∘ Vset β"
  using assms unfolding ntcf_arrow_components' by (rule NTCod.cf_map_in_Vset)

lemma (in is_tm_ntcf) tm_ntcf_arrow_NTCod_in_Vset: 
  "ntcf_arrow 𝔑⦇NTCod⦈ ∈⇩∘ Vset α"
  unfolding ntcf_arrow_components' by (rule NTCod.tm_cf_map_in_Vset)

lemma (in is_ntcf) ntcf_arrow_in_Vset:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "ntcf_arrow 𝔑 ∈⇩∘ Vset β"
proof-
  interpret ntcf_arrow: vfsequence ‹ntcf_arrow 𝔑› 
    by (auto intro: cat_map_cs_intros)
  interpret β: 𝒵 β by (rule assms(1))
  show ?thesis
  proof(rule vsv.vsv_Limit_vsv_in_VsetI)
    from assms show "𝒟⇩∘ (ntcf_arrow 𝔑) ∈⇩∘ Vset β" 
      by (auto simp: cat_map_cs_simps)
    have "n ∈⇩∘ 𝒟⇩∘ (ntcf_arrow 𝔑) ⟹ ntcf_arrow 𝔑⦇n⦈ ∈⇩∘ Vset β" for n
      by
        (
          unfold ntcf_arrow_vdomain,
          elim_in_numeral, 
          all‹rewrite in "⌑ ∈⇩∘ _" nt_field_simps[symmetric]›, 
          insert assms,
          unfold ntcf_arrow_components'
        )
        (
          auto intro: 
            ntcf_NTMap_in_Vset NTDom.cf_map_in_Vset NTCod.cf_map_in_Vset
        )
    with ntcf_arrow.vsv_vrange_vsubset show "ℛ⇩∘ (ntcf_arrow 𝔑) ⊆⇩∘ Vset β"  
      by simp
  qed (auto simp: cat_map_cs_simps)
qed

lemma (in is_tm_ntcf) tm_ntcf_arrow_in_Vset: "ntcf_arrow 𝔑 ∈⇩∘ Vset α"
proof-
  interpret tm_ntcf_arrow: vfsequence ‹ntcf_arrow 𝔑› 
    by (auto intro: cat_map_cs_intros)
  show ?thesis
  proof(rule vsv.vsv_Limit_vsv_in_VsetI)
    have "n ∈⇩∘ 𝒟⇩∘ (ntcf_arrow 𝔑) ⟹ ntcf_arrow 𝔑⦇n⦈ ∈⇩∘ Vset α" for n
      by 
        (
          unfold ntcf_arrow_vdomain,
          elim_in_numeral, 
          all‹rewrite in "⌑ ∈⇩∘ _" nt_field_simps[symmetric]›
        )
        (
          intro tm_ntcf_arrow_NTMap_in_Vset
          tm_ntcf_arrow_NTDom_in_Vset
          tm_ntcf_arrow_NTCod_in_Vset
        )+
    with tm_ntcf_arrow.vsv_vrange_vsubset show "ℛ⇩∘ (ntcf_arrow 𝔑) ⊆⇩∘ Vset α"  
      by auto
  qed (auto simp: cat_map_cs_simps)
qed

lemma ntcf_arrows_subset_Vset:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows 
    "{ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅} ⊆ elts (Vset β)"
proof(intro subsetI, unfold mem_Collect_eq, elim exE conjE)
  fix x 𝔑 𝔉 𝔊 assume x_def: "x = ntcf_arrow 𝔑" 
    and 𝔑: "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  interpret is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑  by (rule 𝔑)
  show "x ∈⇩∘ Vset β" unfolding x_def by (rule ntcf_arrow_in_Vset[OF assms])
qed

lemma tm_ntcf_arrows_subset_Vset:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows 
    "{ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅} ⊆
      elts (Vset β)"
proof(intro subsetI, unfold mem_Collect_eq, elim exE conjE)
  fix x 𝔑 𝔉 𝔊 assume x_def: "x = ntcf_arrow 𝔑" 
    and 𝔑: "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  interpret is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑  by (rule 𝔑)
  show "x ∈⇩∘ Vset β" unfolding x_def by (rule ntcf_arrow_in_Vset[OF assms])
qed

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

lemma small_tm_ntcf_arrows[simp]: 
  "small {ntcf_arrow 𝔑 | 𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅}"
  by 
    ( 
      rule smaller_than_small[
        OF small_ntcf_arrows tm_ntcf_arrows_subset_ntcf_arrows
        ]
    )

lemma (in is_ntcf) ntcf_arrow_in_Vset_7: "ntcf_arrow 𝔑 ∈⇩∘ Vset (α + 7⇩ℕ)"
proof-
  note [folded VPow_iff, folded Vset_succ[OF Ord_α], cat_cs_intros] =
    ntcf_NTMap_vsubset_Vset 
  from NTDom.cf_map_in_Vset_4 have [cat_cs_intros]:
    "cf_map 𝔉 ∈⇩∘ Vset (succ (succ (succ (succ α))))"
    by succ_of_numeral 
      (cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
  from NTCod.cf_map_in_Vset_4 have [cat_cs_intros]:
    "cf_map 𝔊 ∈⇩∘ Vset (succ (succ (succ (succ α))))"
    by succ_of_numeral 
      (cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
  show ?thesis
    by (subst ntcf_arrow_def, succ_of_numeral, unfold cat_cs_simps)
      (
        cs_concl 
          cs_simp: plus_V_succ_right V_cs_simps 
          cs_intro: V_cs_intros cat_cs_intros
      )
qed

lemma (in 𝒵) ntcf_arrows_in_Vset:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "ntcf_arrows α 𝔄 𝔅 ∈⇩∘ Vset β"
proof(rule vsubset_in_VsetI)
  interpret β: 𝒵 β by (rule assms(1))
  show "ntcf_arrows α 𝔄 𝔅 ⊆⇩∘ Vset (α + 7⇩ℕ)"
  proof(intro vsubsetI)
    fix 𝔑 assume "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
    then obtain 𝔑' 𝔉 𝔊 
      where 𝔑_def: "𝔑 = ntcf_arrow 𝔑'" 
        and 𝔑': "𝔑' : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
      by clarsimp
    interpret is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑' using 𝔑' by simp
    show "𝔑 ∈⇩∘ Vset (α + 7⇩ℕ)" unfolding 𝔑_def by (rule ntcf_arrow_in_Vset_7)
  qed
  from assms(2) show "Vset (α + 7⇩ℕ) ∈⇩∘ Vset β"
    by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed
  
lemma (in 𝒵) tm_ntcf_arrows_vsubset_Vset: "tm_ntcf_arrows α 𝔄 𝔅 ⊆⇩∘ Vset α"
  by (clarsimp simp: is_tm_ntcf.tm_ntcf_arrow_in_Vset)


text‹Rules.›

lemma (in is_ntcf) ntcf_arrowsI: "ntcf_arrow 𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
  using is_ntcf_axioms by auto

lemma (in is_tm_ntcf) tm_ntcf_arrowsI: "ntcf_arrow 𝔑 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
  using is_ntcf_axioms by (auto intro: cat_small_cs_intros)

lemma (in is_ntcf) ntcf_arrowsI': 
  assumes "𝔑' = ntcf_arrow 𝔑"
  shows "𝔑' ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
  unfolding assms(1) by (rule ntcf_arrowsI)

lemma (in is_tm_ntcf) tm_ntcf_arrowsI': 
  assumes "𝔑' = ntcf_arrow 𝔑"
  shows "𝔑' ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
  unfolding assms(1) by (rule tm_ntcf_arrowsI)

lemmas [cat_map_cs_intros] =
  is_ntcf.ntcf_arrowsI

lemmas ntcf_arrowsI'[cat_map_cs_intros] =
  is_ntcf.ntcf_arrowsI'[rotated]

lemmas [cat_map_cs_intros] =
  is_tm_ntcf.tm_ntcf_arrowsI

lemmas tm_ntcf_arrowsI'[cat_map_cs_intros] =
  is_tm_ntcf.tm_ntcf_arrowsI'[rotated]

lemma ntcf_arrowsE[elim]:
  assumes "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
  obtains 𝔐 𝔉 𝔊 where "𝔑 = ntcf_arrow 𝔐" and "𝔐 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  using assms by auto

lemma tm_ntcf_arrowsE[elim]:
  assumes "𝔑 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
  obtains 𝔐 𝔉 𝔊 where "𝔑 = ntcf_arrow 𝔐" 
    and "𝔐 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  using assms by auto


text‹Elementary properties.›

lemma tm_ntcf_arrows_vsubset_ntcf_arrows: 
  "tm_ntcf_arrows α 𝔄 𝔅 ⊆⇩∘ ntcf_arrows α 𝔄 𝔅"
  using tm_ntcf_arrows_subset_ntcf_arrows by auto

lemma tm_ntcf_arrows_in_cf_arrows[cat_map_cs_intros]:
  assumes "𝔑 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
  shows "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
  using assms tm_ntcf_arrows_vsubset_ntcf_arrows[of α 𝔄 𝔅] by blast

lemma ntcf_arrow_inj:
  assumes "ntcf_arrow 𝔐 = ntcf_arrow 𝔑"
    and "𝔐 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔐 = 𝔑"
proof(rule ntcf_eqI)
  interpret 𝔐: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔐 by (rule assms(2))
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉' 𝔊' 𝔑 by (rule assms(3))
  from assms(1) have NTMap: "ntcf_arrow 𝔐⦇NTMap⦈ = ntcf_arrow 𝔑⦇NTMap⦈" 
    and NTDom: "ntcf_arrow 𝔐⦇NTDom⦈ = ntcf_arrow 𝔑⦇NTDom⦈"
    and NTCod: "ntcf_arrow 𝔐⦇NTCod⦈ = ntcf_arrow 𝔑⦇NTCod⦈"
    by auto
  from NTMap show "𝔐⦇NTMap⦈ = 𝔑⦇NTMap⦈" unfolding ntcf_arrow_components by simp
  from NTDom NTCod show "𝔐⦇NTDom⦈ = 𝔑⦇NTDom⦈" "𝔐⦇NTCod⦈ = 𝔑⦇NTCod⦈" 
    unfolding ntcf_arrow_components cf_map_components
    by 
      (
        auto simp: 
          cat_cs_simps 
          cf_map_eq_iff[OF 𝔐.NTDom.is_functor_axioms 𝔑.NTDom.is_functor_axioms]
          cf_map_eq_iff[OF 𝔐.NTCod.is_functor_axioms 𝔑.NTCod.is_functor_axioms]
      )
  from assms(2,3) show 
    "𝔐 : 𝔐⦇NTDom⦈ ↦⇩C⇩F 𝔐⦇NTCod⦈ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    "𝔑 : 𝔑⦇NTDom⦈ ↦⇩C⇩F 𝔑⦇NTCod⦈ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (auto simp: cat_cs_simps)
qed auto

lemma ntcf_arrow_eq_iff[cat_map_cs_simps]:
  assumes "𝔐 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔑 : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "ntcf_arrow 𝔐 = ntcf_arrow 𝔑 ⟷ 𝔐 = 𝔑"
  using ntcf_arrow_inj[OF _ assms] by auto

lemma ntcf_arrow_eqI:
  assumes "𝔐 ∈⇩∘ ntcf_arrows α 𝔄 𝔅" 
    and "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
    and "𝔐⦇NTMap⦈ = 𝔑⦇NTMap⦈"
    and "𝔐⦇NTDom⦈ = 𝔑⦇NTDom⦈"
    and "𝔐⦇NTCod⦈ = 𝔑⦇NTCod⦈"
  shows "𝔐 = 𝔑"
proof-
  from assms(1) obtain 𝔐' 𝔉 𝔊
    where 𝔐_def: "𝔐 = ntcf_arrow 𝔐'" and 𝔐': "𝔐' : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by auto
  from assms(2) obtain 𝔑' 𝔉' 𝔊'
    where 𝔑_def: "𝔑 = ntcf_arrow 𝔑'" and 𝔑': "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by auto
  show ?thesis
  proof(rule vsv_eqI, unfold 𝔐_def 𝔑_def)
    show "a ∈⇩∘ 𝒟⇩∘ (ntcf_arrow 𝔐') ⟹ ntcf_arrow 𝔐'⦇a⦈ = ntcf_arrow 𝔑'⦇a⦈" 
      for a
      by  
        (
          unfold ntcf_arrow_vdomain, 
          elim_in_numeral, 
          insert assms(3-5), 
          unfold 𝔐_def 𝔑_def,
          fold nt_field_simps
        )
        simp_all
  qed (auto intro: cat_map_cs_intros simp: cat_map_cs_simps)
qed



subsection‹
Conversion of a natural transformation arrow to a natural transformation
›


subsubsection‹Definition and elementary properties›

definition ntcf_of_ntcf_arrow :: "V ⇒ V ⇒ V ⇒ V"
  where "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 =
    [
      𝔑⦇NTMap⦈,
      cf_of_cf_map 𝔄 𝔅 (𝔑⦇NTDom⦈),
      cf_of_cf_map 𝔄 𝔅 (𝔑⦇NTCod⦈),
      𝔄,
      𝔅
    ]⇩∘"


text‹Components.›

lemma ntcf_of_ntcf_arrow_components:
  shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
    and "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTDom⦈ = cf_of_cf_map 𝔄 𝔅 (𝔑⦇NTDom⦈)"
    and "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTCod⦈ = cf_of_cf_map 𝔄 𝔅 (𝔑⦇NTCod⦈)"
    and "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTDGDom⦈ = 𝔄"
    and "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTDGCod⦈ = 𝔅"
  unfolding ntcf_of_ntcf_arrow_def nt_field_simps 
  by (simp_all add: nat_omega_simps)

lemmas [cat_map_extra_cs_simps] = ntcf_of_ntcf_arrow_components(1)
lemmas [cat_map_cs_simps] = ntcf_of_ntcf_arrow_components(2-5)


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

lemma (in is_ntcf) ntcf_of_ntcf_arrow_is_ntcf: 
  "ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑) : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof(rule is_ntcfI')
  show "vfsequence (ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑))"
    unfolding ntcf_of_ntcf_arrow_def by auto
  show "vcard (ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑)) = 5⇩ℕ"
    unfolding ntcf_of_ntcf_arrow_def by (simp add: nat_omega_simps)
  show "ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑)⦇NTMap⦈⦇a⦈ :
    𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"
    if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
    using is_ntcf_axioms that
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_map_cs_simps cat_map_extra_cs_simps 
          cs_intro: cat_cs_intros
      )
  show "ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑)⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ =
    𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑)⦇NTMap⦈⦇a⦈"
    if "f : a ↦⇘𝔄⇙ b" for a b f
    using is_ntcf_axioms that
    by 
      (
        cs_concl cs_shallow 
          cs_simp: ntcf_Comp_commute cat_map_cs_simps cat_map_extra_cs_simps 
          cs_intro: cat_cs_intros
      )
qed 
  (
    use is_ntcf_axioms in 
      ‹auto simp: cat_cs_simps cat_map_cs_simps cat_map_extra_cs_simps›
  )

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

lemmas [cat_map_cs_intros] = is_ntcf.ntcf_of_ntcf_arrow_is_ntcf'


subsubsection‹
The composition of the conversion of a natural transformation arrow 
to a natural transformation
›

lemma (in is_ntcf) ntcf_of_ntcf_arrow[cat_map_cs_simps]:
  "ntcf_of_ntcf_arrow 𝔄 𝔅 (ntcf_arrow 𝔑) = 𝔑"
  by (rule ntcf_eqI) 
    (
      auto 
        simp: cat_map_cs_simps cat_map_extra_cs_simps 
        intro: cat_cs_intros ntcf_of_ntcf_arrow_is_ntcf
    )

lemmas [cat_map_cs_simps] = is_ntcf.ntcf_of_ntcf_arrow



subsection‹Composition of the natural transformation arrows›

definition ntcf_arrow_vcomp :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "ntcf_arrow_vcomp 𝔄 𝔅 𝔐 𝔑 =
    ntcf_arrow (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔐 ∙⇩N⇩T⇩C⇩F ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑)"

syntax "_ntcf_arrow_vcomp" :: "V ⇒ V ⇒ V ⇒ V ⇒ V" 
  (‹(_/ ∙⇩N⇩T⇩C⇩F⇘_,_⇙ _)› [55, 56, 57, 58] 55)
translations "𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ 𝔑" ⇌ "CONST ntcf_arrow_vcomp 𝔄 𝔅 𝔐 𝔑"


text‹Components.›

lemma (in is_ntcf) ntcf_arrow_vcomp_components:
  "(ntcf_arrow 𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ ntcf_arrow 𝔑)⦇NTMap⦈ = (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTMap⦈"
  "(ntcf_arrow 𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ ntcf_arrow 𝔑)⦇NTDom⦈ = cf_map ((𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)⦇NTDom⦈)"
  "(ntcf_arrow 𝔑 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ ntcf_arrow 𝔐)⦇NTCod⦈ = cf_map ((𝔑 ∙⇩N⇩T⇩C⇩F 𝔐)⦇NTCod⦈)"
  unfolding 
    ntcf_arrow_vcomp_def
    ntsmcf_vcomp_components 
    ntcf_arrow_components 
    ntcf_of_ntcf_arrow_components
  by (simp_all add: cat_cs_simps cat_map_cs_simps)

lemmas [cat_map_cs_simps] = is_ntcf.ntcf_arrow_vcomp_components


text‹Elementary properties.›

lemma ntcf_arrow_vcomp_ntcf_vcomp[cat_map_cs_simps]:
  assumes "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
  shows "ntcf_arrow 𝔐 ∙⇩N⇩T⇩C⇩F⇘𝔄,𝔅⇙ ntcf_arrow 𝔑 = ntcf_arrow (𝔐 ∙⇩N⇩T⇩C⇩F 𝔑)"
  by (rule ntcf_arrow_eqI, insert assms)
    (
      cs_concl 
        cs_simp: ntcf_arrow_vcomp_def cat_map_cs_simps cat_cs_simps
        cs_intro: cat_map_cs_intros cat_cs_intros
    )+


subsection‹Identity natural transformation arrow›

definition ntcf_arrow_id :: "V ⇒ V ⇒ V ⇒ V"
  where "ntcf_arrow_id 𝔄 𝔅 𝔉 = ntcf_arrow (ntcf_id (cf_of_cf_map 𝔄 𝔅 𝔉))"


text‹Components.›

lemma (in is_functor) ntcf_arrow_id_components:
  "(ntcf_arrow_id 𝔄 𝔅 (cf_map 𝔉))⦇NTMap⦈ = ntcf_id 𝔉⦇NTMap⦈"
  "(ntcf_arrow_id 𝔄 𝔅 (cf_map 𝔉))⦇NTDom⦈ = cf_map (ntcf_id 𝔉⦇NTDom⦈)"
  "(ntcf_arrow_id 𝔄 𝔅 (cf_map 𝔉))⦇NTCod⦈ = cf_map (ntcf_id 𝔉⦇NTCod⦈)"
  unfolding ntcf_arrow_id_def ntcf_arrow_components 
  by (simp_all add: cat_map_cs_simps)

lemmas [cat_map_cs_simps] = is_functor.ntcf_arrow_id_components


text‹Identity natural transformation arrow is a natural transformation arrow.›

lemma ntcf_arrow_id_ntcf_id[cat_map_cs_simps]:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
  shows "ntcf_arrow_id 𝔄 𝔅 (cf_map 𝔉) = ntcf_arrow (ntcf_id 𝔉)"
  by (rule ntcf_arrow_eqI, insert assms, unfold ntcf_arrow_id_def)
    (
      cs_concl 
        cs_simp: cat_map_cs_simps cat_cs_simps 
        cs_intro: cat_map_cs_intros cat_cs_intros
    )



subsection‹‹FUNCT››


subsubsection‹Definition and elementary properties›

definition dg_FUNCT :: "V ⇒ V ⇒ V ⇒ V"
  where "dg_FUNCT α 𝔄 𝔅 =
    [
      cf_maps α 𝔄 𝔅,
      ntcf_arrows α 𝔄 𝔅,
      (λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈),
      (λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈)
    ]⇩∘"

lemmas [dg_FUNCT_cs_simps] = cat_map_cs_simps
lemmas [dg_FUNCT_cs_intros] = cat_map_cs_intros


text‹Components.›

lemma dg_FUNCT_components: 
  shows "dg_FUNCT α 𝔄 𝔅⦇Obj⦈ = cf_maps α 𝔄 𝔅"
    and "dg_FUNCT α 𝔄 𝔅⦇Arr⦈ = ntcf_arrows α 𝔄 𝔅"
    and "dg_FUNCT α 𝔄 𝔅⦇Dom⦈ = (λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈)"
    and "dg_FUNCT α 𝔄 𝔅⦇Cod⦈ = (λ𝔑∈⇩∘ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈)"
  unfolding dg_FUNCT_def dg_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Objects›

lemma (in is_functor) dg_FUNCT_ObjI: "cf_map 𝔉 ∈⇩∘ dg_FUNCT α 𝔄 𝔅⦇Obj⦈"
  unfolding dg_FUNCT_components by (auto intro: cat_cs_intros)


subsubsection‹Domain and codomain›

mk_VLambda dg_FUNCT_components(3)
  |vsv dg_FUNCT_Dom_vsv[dg_FUNCT_cs_intros]|
  |vdomain dg_FUNCT_Dom_vdomain[dg_FUNCT_cs_simps]|

mk_VLambda dg_FUNCT_components(4)
  |vsv dg_FUNCT_Cod_vsv[dg_FUNCT_cs_intros]|
  |vdomain dg_FUNCT_Cod_vdomain[dg_FUNCT_cs_simps]|

lemma (in is_ntcf)
  shows dg_FUNCT_Dom_app: "dg_FUNCT α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"
    and dg_FUNCT_Cod_app: "dg_FUNCT α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
proof-
  from is_ntcf_axioms show 
    "dg_FUNCT α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"  
    "dg_FUNCT α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
    unfolding dg_FUNCT_components 
    by 
      ( 
        cs_concl 
          cs_simp: dg_FUNCT_cs_simps V_cs_simps cs_intro: dg_FUNCT_cs_intros
      )+
qed

lemma (in is_ntcf)
  assumes "𝔑' = ntcf_arrow 𝔑"
  shows dg_FUNCT_Dom_app': "dg_FUNCT α 𝔄 𝔅⦇Dom⦈⦇𝔑'⦈ = cf_map 𝔉"
    and dg_FUNCT_Cod_app': "dg_FUNCT α 𝔄 𝔅⦇Cod⦈⦇𝔑'⦈ = cf_map 𝔊"
  unfolding assms by (intro dg_FUNCT_Dom_app dg_FUNCT_Cod_app)+

lemmas [dg_FUNCT_cs_simps] = 
  is_ntcf.dg_FUNCT_Dom_app'
  is_ntcf.dg_FUNCT_Cod_app'

lemma 
  shows dg_FUNCT_Dom_vrange: "ℛ⇩∘ (dg_FUNCT α 𝔄 𝔅⦇Dom⦈) ⊆⇩∘ dg_FUNCT α 𝔄 𝔅⦇Obj⦈"
    and dg_FUNCT_Cod_vrange: "ℛ⇩∘ (dg_FUNCT α 𝔄 𝔅⦇Cod⦈) ⊆⇩∘ dg_FUNCT α 𝔄 𝔅⦇Obj⦈"
  unfolding dg_FUNCT_components
proof(all‹intro vrange_VLambda_vsubset›)
  fix 𝔑 assume "𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅"
  then obtain 𝔐 𝔉 𝔊 where 𝔑_def[dg_FUNCT_cs_simps]: "𝔑 = ntcf_arrow 𝔐" 
    and 𝔐: "𝔐 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by auto
  from 𝔐 show "𝔑⦇NTDom⦈ ∈⇩∘ cf_maps α 𝔄 𝔅"
    by (cs_concl cs_simp: dg_FUNCT_cs_simps cs_intro: dg_FUNCT_cs_intros cat_cs_intros)
  from 𝔐 show "𝔑⦇NTCod⦈ ∈⇩∘ cf_maps α 𝔄 𝔅"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: dg_FUNCT_cs_simps cs_intro: dg_FUNCT_cs_intros cat_cs_intros
      )
qed


subsubsection‹‹FUNCT› is a tiny digraph›

lemma (in 𝒵) tiny_digraph_dg_FUNCT:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "tiny_digraph β (dg_FUNCT α 𝔄 𝔅)"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  show ?thesis
  proof(intro tiny_digraphI)
    show "vfsequence (dg_FUNCT α 𝔄 𝔅)" unfolding dg_FUNCT_def by simp
    show "vcard (dg_FUNCT α 𝔄 𝔅) = 4⇩ℕ"
      unfolding dg_FUNCT_def by (simp add: nat_omega_simps)
    show "ℛ⇩∘ (dg_FUNCT α 𝔄 𝔅⦇Dom⦈) ⊆⇩∘ dg_FUNCT α 𝔄 𝔅⦇Obj⦈"
      by (simp add: dg_FUNCT_Dom_vrange dg_FUNCT_Cod_vrange)
    show "ℛ⇩∘ (dg_FUNCT α 𝔄 𝔅⦇Cod⦈) ⊆⇩∘ dg_FUNCT α 𝔄 𝔅⦇Obj⦈"
      by (simp add: dg_FUNCT_Dom_vrange dg_FUNCT_Cod_vrange)
    from assms show "dg_FUNCT α 𝔄 𝔅⦇Obj⦈ ∈⇩∘ Vset β"
      unfolding dg_FUNCT_components(1) by (rule cf_maps_in_Vset)
    show "dg_FUNCT α 𝔄 𝔅⦇Arr⦈ ∈⇩∘ Vset β"
      unfolding dg_FUNCT_components(2) by (rule ntcf_arrows_in_Vset[OF assms])
  qed (auto simp: dg_FUNCT_cs_simps dg_FUNCT_components(1,2) intro: dg_FUNCT_cs_intros)
qed


subsubsection‹Arrow with a domain and a codomain›

lemma dg_FUNCT_is_arrI:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
  shows "ntcf_arrow 𝔑 : cf_map 𝔉 ↦⇘dg_FUNCT α 𝔄 𝔅⇙ cf_map 𝔊"
proof(intro is_arrI, unfold dg_FUNCT_components(1,2))
  interpret is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms)
  from assms show "ntcf_arrow 𝔑 ∈⇩∘ ntcf_arrows α 𝔄 𝔅" by auto
  from assms show 
    "dg_FUNCT α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"
    "dg_FUNCT α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
    by (cs_concl cs_shallow cs_simp: dg_FUNCT_cs_simps)+
qed

lemma dg_FUNCT_is_arrI':
  assumes "𝔑' = ntcf_arrow 𝔑"
    and "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔉' = cf_map 𝔉"
    and "𝔊' = cf_map 𝔊"
  shows "𝔑' : 𝔉' ↦⇘dg_FUNCT α 𝔄 𝔅⇙ 𝔊'"
  using assms(2) unfolding assms(1,3,4) by (rule dg_FUNCT_is_arrI)

lemmas [dg_FUNCT_cs_intros] = dg_FUNCT_is_arrI'

lemma dg_FUNCT_is_arrD[dest]:
  assumes "𝔑 : 𝔉 ↦⇘dg_FUNCT α 𝔄 𝔅⇙ 𝔊"
  shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
    cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F 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-
  note 𝔑 = is_arrD[OF assms, unfolded dg_FUNCT_components(2)]
  obtain 𝔑' 𝔉' 𝔊' where 𝔑_def: "𝔑 = ntcf_arrow 𝔑'"
    and 𝔑': "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    by (elim ntcf_arrowsE[OF 𝔑(1)])
  from 𝔑(2) 𝔑' have 𝔉_def: "𝔉 = cf_map 𝔉'"
    by (cs_prems cs_simp: 𝔑_def dg_FUNCT_cs_simps) simp
  from 𝔑(3) 𝔑' have 𝔊_def: "𝔊 = cf_map 𝔊'"
    by (cs_prems cs_simp: 𝔑_def dg_FUNCT_cs_simps) simp
  from 𝔑' have 𝔑'_def: "𝔑' = ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑"
    unfolding 𝔑_def by (cs_concl cs_shallow cs_simp: dg_FUNCT_cs_simps)
  from 𝔑' have 𝔉'_def: "𝔉' = cf_of_cf_map 𝔄 𝔅 𝔉"
    and 𝔊'_def: "𝔊' = cf_of_cf_map 𝔄 𝔅 𝔊"
    unfolding 𝔉_def 𝔊_def 
    by (cs_concl cs_simp: dg_FUNCT_cs_simps cs_intro: cat_cs_intros)+
  from 𝔑' show "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
    cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F 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 𝔄 𝔅 𝔊)"
    by (fold 𝔉'_def 𝔊'_def 𝔑'_def 𝔉_def 𝔊_def 𝔑_def) simp_all
qed

lemma dg_FUNCT_is_arrE[elim]:
  assumes "𝔑 : 𝔉 ↦⇘dg_FUNCT α 𝔄 𝔅⇙ 𝔊"
  obtains 𝔑' 𝔉' 𝔊' 
    where "𝔑' : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
      and "𝔑 = ntcf_arrow 𝔑'"
      and "𝔉 = cf_map 𝔉'" 
      and "𝔊 = cf_map 𝔊'"
  using dg_FUNCT_is_arrD[OF assms] by auto



subsection‹‹Funct››


subsubsection‹Definition and elementary properties›

definition dg_Funct :: "V ⇒ V ⇒ V ⇒ V"
  where "dg_Funct α 𝔄 𝔅 =
    [
      tm_cf_maps α 𝔄 𝔅,
      tm_ntcf_arrows α 𝔄 𝔅,
      (λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈),
      (λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈)
    ]⇩∘"


text‹Components.›

lemma dg_Funct_components: 
  shows "dg_Funct α 𝔄 𝔅⦇Obj⦈ = tm_cf_maps α 𝔄 𝔅"
    and "dg_Funct α 𝔄 𝔅⦇Arr⦈ = tm_ntcf_arrows α 𝔄 𝔅"
    and "dg_Funct α 𝔄 𝔅⦇Dom⦈ = (λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTDom⦈)"
    and "dg_Funct α 𝔄 𝔅⦇Cod⦈ = (λ𝔑∈⇩∘tm_ntcf_arrows α 𝔄 𝔅. 𝔑⦇NTCod⦈)"
  unfolding dg_Funct_def dg_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Objects›

lemma (in is_tm_functor) dg_Funct_ObjI: "cf_map 𝔉 ∈⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
  unfolding dg_Funct_components by (auto simp: cat_small_cs_intros)


subsubsection‹Domain and codomain›

mk_VLambda dg_Funct_components(3)
  |vsv dg_Funct_Dom_vsv[dg_FUNCT_cs_intros]|
  |vdomain dg_Funct_Dom_vdomain[dg_FUNCT_cs_simps]|

mk_VLambda dg_Funct_components(4)
  |vsv dg_Funct_Cod_vsv[dg_FUNCT_cs_intros]|
  |vdomain dg_Funct_Cod_vdomain[dg_FUNCT_cs_simps]|

lemma (in is_tm_ntcf)
  shows dg_Funct_Dom_app: "dg_Funct α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"
    and dg_Funct_Cod_app: "dg_Funct α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
proof-
  from is_tm_ntcf_axioms show 
    "dg_Funct α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"  
    "dg_Funct α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
    unfolding dg_Funct_components 
    by 
      (
        cs_concl cs_shallow
          cs_simp: dg_FUNCT_cs_simps V_cs_simps 
          cs_intro: dg_FUNCT_cs_intros cat_cs_intros
      )+
qed

lemma (in is_tm_ntcf)
  assumes "𝔑' = ntcf_arrow 𝔑"
  shows dg_Funct_Dom_app': "dg_Funct α 𝔄 𝔅⦇Dom⦈⦇𝔑'⦈ = cf_map 𝔉"
    and dg_Funct_Cod_app': "dg_Funct α 𝔄 𝔅⦇Cod⦈⦇𝔑'⦈ = cf_map 𝔊"
  unfolding assms by (intro dg_Funct_Dom_app dg_Funct_Cod_app)+

lemmas [dg_FUNCT_cs_simps] = 
  is_tm_ntcf.dg_Funct_Dom_app'
  is_tm_ntcf.dg_Funct_Cod_app'

lemma 
  shows dg_Funct_Dom_vrange: "ℛ⇩∘ (dg_Funct α 𝔄 𝔅⦇Dom⦈) ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
    and dg_Funct_Cod_vrange: "ℛ⇩∘ (dg_Funct α 𝔄 𝔅⦇Cod⦈) ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
  unfolding dg_Funct_components
proof(all‹intro vrange_VLambda_vsubset›)
  fix 𝔑 assume "𝔑 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅"
  then obtain 𝔐 𝔉 𝔊 where 𝔑_def[dg_FUNCT_cs_simps]: "𝔑 = ntcf_arrow 𝔐" 
    and 𝔐: "𝔐 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    by auto
  from 𝔐 show "𝔑⦇NTDom⦈ ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
    by 
      ( 
        cs_concl  
          cs_simp: dg_FUNCT_cs_simps 
          cs_intro: dg_FUNCT_cs_intros cat_small_cs_intros
      )
  from 𝔐 show "𝔑⦇NTCod⦈ ∈⇩∘ tm_cf_maps α 𝔄 𝔅"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: dg_FUNCT_cs_simps 
          cs_intro: dg_FUNCT_cs_intros cat_small_cs_intros
      )
qed


subsubsection‹Arrow with a domain and a codomain›

lemma dg_Funct_is_arrI:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" 
  shows "ntcf_arrow 𝔑 : cf_map 𝔉 ↦⇘dg_Funct α 𝔄 𝔅⇙ cf_map 𝔊"
proof(intro is_arrI, unfold dg_Funct_components(1,2))
  interpret is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms)
  from assms show "ntcf_arrow 𝔑 ∈⇩∘ tm_ntcf_arrows α 𝔄 𝔅" by auto
  from assms show 
    "dg_Funct α 𝔄 𝔅⦇Dom⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔉"
    "dg_Funct α 𝔄 𝔅⦇Cod⦈⦇ntcf_arrow 𝔑⦈ = cf_map 𝔊"
    by (cs_concl cs_shallow cs_simp: dg_FUNCT_cs_simps)+
qed

lemma dg_Funct_is_arrI':
  assumes "𝔑' = ntcf_arrow 𝔑"
    and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" 
    and "𝔉' = cf_map 𝔉"
    and "𝔊' = cf_map 𝔊"
  shows "𝔑' : 𝔉' ↦⇘dg_Funct α 𝔄 𝔅⇙ 𝔊'"
  using assms(2) unfolding assms(1,3,4) by (rule dg_Funct_is_arrI)

lemmas [dg_FUNCT_cs_intros] = dg_Funct_is_arrI'

lemma dg_Funct_is_arrD[dest]:
  assumes "𝔑 : 𝔉 ↦⇘dg_Funct α 𝔄 𝔅⇙ 𝔊"
  shows "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
    cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 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-
  note 𝔑 = is_arrD[OF assms, unfolded dg_Funct_components(2)]
  obtain 𝔑' 𝔉' 𝔊' where 𝔑_def: "𝔑 = ntcf_arrow 𝔑'"
    and 𝔑': "𝔑' : 𝔉' ↦⇩C⇩F⇩.⇩t⇩m 𝔊' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    by (elim tm_ntcf_arrowsE[OF 𝔑(1)])
  from 𝔑(2) 𝔑' have 𝔉_def: "𝔉 = cf_map 𝔉'"
    by (cs_prems cs_simp: 𝔑_def dg_FUNCT_cs_simps) simp
  from 𝔑(3) 𝔑' have 𝔊_def: "𝔊 = cf_map 𝔊'"
    by (cs_prems cs_simp: 𝔑_def dg_FUNCT_cs_simps) simp
  from 𝔑' have 𝔑'_def: "𝔑' = ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑"
    unfolding 𝔑_def 
    by 
      (
        cs_concl cs_shallow
          cs_simp: dg_FUNCT_cs_simps cs_intro: cat_small_cs_intros cat_cs_intros
      )
  from 𝔑' have 𝔉'_def: "𝔉' = cf_of_cf_map 𝔄 𝔅 𝔉"
    and 𝔊'_def: "𝔊' = cf_of_cf_map 𝔄 𝔅 𝔊"
    unfolding 𝔉_def 𝔊_def 
    by 
      (
        cs_concl 
          cs_simp: dg_FUNCT_cs_simps cs_intro: cat_small_cs_intros cat_cs_intros
      )+
  from 𝔑' show "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑 :
    cf_of_cf_map 𝔄 𝔅 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 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 𝔄 𝔅 𝔊)"
    by (fold 𝔉'_def 𝔊'_def 𝔑'_def 𝔉_def 𝔊_def 𝔑_def) simp_all
qed

lemma dg_Funct_is_arrE[elim]:
  assumes "𝔑 : 𝔉 ↦⇘dg_Funct α 𝔄 𝔅⇙ 𝔊"
  obtains 𝔑' 𝔉' 𝔊' where "𝔑' : 𝔉' ↦⇩C⇩F⇩.⇩t⇩m 𝔊' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" 
    and "𝔑 = ntcf_arrow 𝔑'"
    and "𝔉 = cf_map 𝔉'" 
    and "𝔊 = cf_map 𝔊'"
  using dg_Funct_is_arrD[OF assms] by auto


subsubsection‹‹Funct› is a digraph›

lemma digraph_dg_Funct: 
  assumes "tiny_category α 𝔄" and "category α 𝔅"
  shows "digraph α (dg_Funct α 𝔄 𝔅)"
proof-

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

  show ?thesis

  proof(intro digraphI)
  
    show "vfsequence (dg_Funct α 𝔄 𝔅)" unfolding dg_Funct_def by simp
    show "vcard (dg_Funct α 𝔄 𝔅) = 4⇩ℕ"
      unfolding dg_Funct_def by (simp add: nat_omega_simps)
    show "ℛ⇩∘ (dg_Funct α 𝔄 𝔅⦇Dom⦈) ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
      by (simp add: dg_Funct_Dom_vrange dg_Funct_Cod_vrange)
    show "ℛ⇩∘ (dg_Funct α 𝔄 𝔅⦇Cod⦈) ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
      by (simp add: dg_Funct_Dom_vrange dg_Funct_Cod_vrange)
    show "dg_Funct α 𝔄 𝔅⦇Obj⦈ ⊆⇩∘ Vset α"
      unfolding dg_Funct_components(1,2) by (rule tm_cf_maps_vsubset_Vset)
    
    have RA: 
      "(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ∈⇩∘ Vset α"
      "(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ⊆⇩∘ 𝔅⦇Obj⦈"
      if "A ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈" and "A ∈⇩∘ Vset α" for A
    proof-
      have "(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ⊆⇩∘ 𝔅⦇Obj⦈" 
        and "(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ⊆⇩∘ ⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘A)))))"
      proof(all‹intro vsubsetI›)
        fix f assume "f ∈⇩∘ (⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈))"
        then obtain 𝔉 where 𝔉: "𝔉 ∈⇩∘ A" and f: "f ∈⇩∘ ℛ⇩∘ (𝔉⦇ObjMap⦈)" by auto
        with that(1) have "𝔉 ∈⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈" by (elim vsubsetE)
        then obtain 𝔉'
          where 𝔉_def: "𝔉 = cf_map 𝔉'" and 𝔉': "𝔉' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
          unfolding dg_Funct_components by auto
        interpret 𝔉': is_tm_functor α 𝔄 𝔅 𝔉' by (rule 𝔉')
        from f obtain a where "a ∈⇩∘ 𝒟⇩∘ (𝔉'⦇ObjMap⦈)" and af: "⟨a, f⟩ ∈⇩∘ 𝔉'⦇ObjMap⦈"
          unfolding 𝔉_def cf_map_components vdomain_iff by force
        then show "f ∈⇩∘ 𝔅⦇Obj⦈"
          using 𝔉'.cf_ObjMap_vrange 𝔉_def cf_map_components(1) f vsubsetE by auto
        show "f ∈⇩∘ ⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘A)))))"
        proof(intro VUnionI)
          show "𝔉 ∈⇩∘ A" by (rule 𝔉)
          show "set {0, 𝔉⦇ObjMap⦈} ∈⇩∘ ⟨[]⇩∘, 𝔉⦇ObjMap⦈⟩" unfolding vpair_def by simp
          show "⟨a, f⟩ ∈⇩∘ 𝔉⦇ObjMap⦈"
            unfolding 𝔉_def cf_map_components by (intro af)
          show "set {a, f} ∈⇩∘ ⟨a, f⟩" unfolding vpair_def by clarsimp
        qed (clarsimp simp: 𝔉_def cf_map_def dg_FUNCT_Obj_components)+
      qed
      moreover have "⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘(⋃⇩∘A))))) ∈⇩∘ Vset α"
        by (intro VUnion_in_VsetI that(2))
      ultimately show 
        "(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ∈⇩∘ Vset α" 
        "(⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈)) ⊆⇩∘ 𝔅⦇Obj⦈" 
        by blast+
    qed
  
    fix A B assume prems:
      "A ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
      "B ⊆⇩∘ dg_Funct α 𝔄 𝔅⦇Obj⦈"
      "A ∈⇩∘ Vset α"
      "B ∈⇩∘ Vset α"
  
    define ARs where "ARs = (⋃⇩∘𝔉∈⇩∘A. ℛ⇩∘ (𝔉⦇ObjMap⦈))"
    define BRs where "BRs = (⋃⇩∘𝔊∈⇩∘B. ℛ⇩∘ (𝔊⦇ObjMap⦈))"
    define Hom_AB where "Hom_AB = (⋃⇩∘a∈⇩∘ARs. ⋃⇩∘b∈⇩∘BRs. Hom 𝔅 a b)"
  
    define Q where
      "Q i = (if i = 0 then VPow (𝔄⦇Obj⦈ ×⇩∘ Hom_AB) else if i = 1⇩ℕ then A else B)" 
      for i
    have 
      "{[𝔑, 𝔉, 𝔊]⇩∘ |𝔑 𝔉 𝔊. 𝔑 ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB ∧ 𝔉 ∈⇩∘ A ∧ 𝔊 ∈⇩∘ B} ⊆
        elts (∏⇩∘i∈⇩∘set {0, 1⇩ℕ, 2⇩ℕ}. Q i)"
    proof(intro subsetI, unfold mem_Collect_eq, elim exE conjE)
      fix 𝔑𝔉𝔊 𝔑 𝔉 𝔊 assume prems': 
        "𝔑𝔉𝔊 = [𝔑, 𝔉, 𝔊]⇩∘" "𝔑 ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB" "𝔉 ∈⇩∘ A" "𝔊 ∈⇩∘ B"
      show "𝔑𝔉𝔊 ∈⇩∘ (∏⇩∘i∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}. Q i)"
      proof(intro vproductI, unfold Ball_def; (intro allI impI)?)
        fix i assume "i ∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}"
        then consider ‹i = 0› | ‹i = 1⇩ℕ› | ‹i = 2⇩ℕ› by auto
        then show "𝔑𝔉𝔊⦇i⦈ ∈⇩∘ Q i"
          by cases (auto simp: Q_def prems' nat_omega_simps)
      qed (auto simp: prems'(1) three nat_omega_simps)
    qed
    moreover then have small[simp]: 
      "small {[r, a, b]⇩∘ | r a b. r ⊆⇩∘𝔄⦇Obj⦈ ×⇩∘ Hom_AB ∧ a ∈⇩∘ A ∧ b ∈⇩∘ B}"
      by (rule down)
    ultimately have
      "set {[r, a, b]⇩∘ |r a b. r ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB ∧ a ∈⇩∘ A ∧ b ∈⇩∘ B} ⊆⇩∘
        (∏⇩∘i∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}. Q i)"
      by auto
    moreover have "(∏⇩∘i∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}. Q i) ∈⇩∘ Vset α"
    proof(rule Limit_vproduct_in_VsetI)
      show "set {0, 1⇩ℕ, 2⇩ℕ} ∈⇩∘ Vset α"
        by (cs_concl cs_intro: V_cs_intros cat_cs_intros cs_simp: V_cs_simps)
      have "Hom_AB ∈⇩∘ Vset α"
        unfolding Hom_AB_def
        by 
          (
            intro 𝔅.cat_Hom_vifunion_in_Vset prems(3,4), 
            unfold ARs_def BRs_def; 
            intro RA prems
          )
      moreover have "𝔄⦇Obj⦈ ∈⇩∘ Vset α" by (intro tiny_cat_Obj_in_Vset)
      ultimately have "VPow (𝔄⦇Obj⦈ ×⇩∘ Hom_AB) ∈⇩∘ Vset α"
        by (cs_concl cs_shallow cs_intro: V_cs_intros)
      with prems(3,4) show "Q i ∈⇩∘ Vset α" if "i ∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}" for i
        unfolding Q_def by (simp_all add: nat_omega_simps)
    qed auto
    moreover have
      "(⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom (dg_Funct α 𝔄 𝔅) a b) ⊆⇩∘
        set {[r, a, b]⇩∘ | r a b. r ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB ∧ a ∈⇩∘ A ∧ b ∈⇩∘ B}"
    proof(rule vsubsetI)
      fix 𝔑 assume "𝔑 ∈⇩∘ (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom (dg_Funct α 𝔄 𝔅) a b)"
      then obtain 𝔉 𝔊 
        where 𝔉: "𝔉 ∈⇩∘ A"
          and 𝔊: "𝔊 ∈⇩∘ B"
          and 𝔑_ab: "𝔑 ∈⇩∘ Hom (dg_Funct α 𝔄 𝔅) 𝔉 𝔊"
        by auto
      then have "𝔑 : 𝔉 ↦⇘dg_Funct α 𝔄 𝔅⇙ 𝔊" by simp
      note 𝔑 = dg_Funct_is_arrD[OF this]
      show 
        "𝔑 ∈⇩∘ set {[r, a, b]⇩∘ | r a b. r ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB ∧ a ∈⇩∘ A ∧ b ∈⇩∘ B}"
      proof(intro in_set_CollectI small exI conjI)
        show "𝔑 =
          [
            ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTMap⦈,
            cf_map (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTDom⦈),
            cf_map (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTCod⦈)
          ]⇩∘"
          by (rule 𝔑(2)[unfolded ntcf_arrow_def])
        interpret 𝔑: is_tm_ntcf α 
          𝔄 𝔅 
          ‹cf_of_cf_map 𝔄 𝔅 𝔉› ‹cf_of_cf_map 𝔄 𝔅 𝔊› 
          ‹ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑›
          rewrites "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTMap⦈ = 𝔑⦇NTMap⦈"
            and "cf_of_cf_map 𝔄 𝔅 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
            and "cf_of_cf_map 𝔄 𝔅 𝔊⦇ObjMap⦈ = 𝔊⦇ObjMap⦈"
          by
            (
              rule 𝔑(1), 
              unfold ntcf_of_ntcf_arrow_components cf_of_cf_map_components
            ) 
            simp_all
        show "ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTMap⦈ ⊆⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB"
        proof(intro vsubsetI, unfold ntcf_of_ntcf_arrow_components)
          fix af assume prems'': "af ∈⇩∘ 𝔑⦇NTMap⦈"
          then obtain a f where af_def: "af = ⟨a, f⟩" 
            and a: "a ∈⇩∘ 𝔄⦇Obj⦈"
            and f: "f ∈⇩∘ ℛ⇩∘ (𝔑⦇NTMap⦈)" 
            by (elim 𝔑.NTMap.vbrelation_vinE)
          from prems'' have f_def: "f = 𝔑⦇NTMap⦈⦇a⦈" 
            unfolding af_def 𝔑.NTMap.vsv_ex1_app1[OF a] .
          have 𝔑a: "𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈"
            by (rule 𝔑.ntcf_NTMap_is_arr[OF a])
          have "f ∈⇩∘ Hom_AB"
            unfolding f_def Hom_AB_def ARs_def BRs_def
          proof(intro vifunionI, unfold in_Hom_iff)
            show "𝔉 ∈⇩∘ A" by (intro 𝔉)
            from a show "𝔉⦇ObjMap⦈⦇a⦈ ∈⇩∘ ℛ⇩∘ (𝔉⦇ObjMap⦈)" 
              by (metis 𝔑.NTDom.ObjMap.vdomain_atD 𝔑.NTDom.cf_ObjMap_vdomain)
            show "𝔊 ∈⇩∘ B" by (intro 𝔊)
            from a show "𝔊⦇ObjMap⦈⦇a⦈ ∈⇩∘ ℛ⇩∘ (𝔊⦇ObjMap⦈)" 
              by (metis 𝔑.NTCod.ObjMap.vdomain_atD 𝔑.NTCod.cf_ObjMap_vdomain)
            show "𝔑⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔊⦇ObjMap⦈⦇a⦈" by (intro 𝔑a)
          qed
          with a show "af ∈⇩∘ 𝔄⦇Obj⦈ ×⇩∘ Hom_AB" unfolding af_def f_def by simp
        qed
        show "cf_map (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTDom⦈) ∈⇩∘ A"
          unfolding 𝔑.ntcf_NTDom 𝔑(3)[symmetric] by (rule 𝔉)
        show "cf_map (ntcf_of_ntcf_arrow 𝔄 𝔅 𝔑⦇NTCod⦈) ∈⇩∘ B"
          unfolding 𝔑.ntcf_NTCod 𝔑(4)[symmetric] by (rule 𝔊)
      qed
    qed
    ultimately show "(⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom (dg_Funct α 𝔄 𝔅) a b) ∈⇩∘ Vset α"
      by blast
  qed (auto simp: dg_Funct_components)

qed


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

lemma subdigraph_dg_Funct_dg_FUNCT:
  assumes "𝒵 β" and "α ∈⇩∘ β" and "tiny_category α 𝔄" and "category α 𝔅"
  shows "dg_Funct α 𝔄 𝔅 ⊆⇩D⇩G⇘β⇙ dg_FUNCT α 𝔄 𝔅"
proof(intro subdigraphI, unfold dg_FUNCT_components(1) dg_Funct_components(1))
  interpret 𝔄: tiny_category α 𝔄 by (rule assms(3))
  interpret β: 𝒵 β by (rule assms(1))
  show "digraph β (dg_Funct α 𝔄 𝔅)"
    by (intro digraph.dg_digraph_if_ge_Limit[OF digraph_dg_Funct] assms)
  from assms show "digraph β (dg_FUNCT α 𝔄 𝔅)"    
    by (cs_concl cs_shallow cs_intro: dg_small_cs_intros 𝔄.tiny_digraph_dg_FUNCT)
  show "𝔉 ∈⇩∘ cf_maps α 𝔄 𝔅" if "𝔉 ∈⇩∘ tm_cf_maps α 𝔄 𝔅" for 𝔉
    using that 
    by (cs_concl cs_shallow cs_intro: dg_FUNCT_cs_intros tm_cf_maps_in_cf_maps)
  show "𝔑 : 𝔉 ↦⇘dg_FUNCT α 𝔄 𝔅⇙ 𝔊" if "𝔑 : 𝔉 ↦⇘dg_Funct α 𝔄 𝔅⇙ 𝔊" 
    for 𝔑 𝔉 𝔊
  proof-
    note f = dg_Funct_is_arrD[OF that]
    from f(1) show ?thesis
      by (subst f(2), use nothing in ‹subst f(3), subst f(4)›)
        (cs_concl cs_shallow cs_intro: dg_FUNCT_cs_intros cat_small_cs_intros)
  qed
qed

text‹\newpage›

end