Theory CZH_ECAT_Small_NTCF

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for natural transformations›
theory CZH_ECAT_Small_NTCF
  imports 
    CZH_Foundations.CZH_SMC_Small_NTSMCF
    CZH_ECAT_Small_Functor
    CZH_ECAT_NTCF
begin



subsection‹Natural transformation of functors with tiny maps›


subsubsection‹Definition and elementary properties›

locale is_tm_ntcf = is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 for α 𝔄 𝔅 𝔉 𝔊 𝔑 +
  assumes tm_ntcf_is_tm_ntsmcf: "ntcf_ntsmcf 𝔑 :
    cf_smcf 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m cf_smcf 𝔊 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ cat_smc 𝔅"

syntax "_is_tm_ntcf" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦⇩C⇩F⇩.⇩t⇩m _ :/ _ ↦↦⇩C⇩.⇩t⇩mı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_tm_ntcf" ⇌ is_tm_ntcf
translations "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" ⇌
  "CONST is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑"

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

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

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

lemma (in is_tm_ntcf) tm_ntcf_is_tm_ntsmcf':
  assumes "𝔉' = cf_smcf 𝔉"
    and "𝔊' = cf_smcf 𝔊"
    and "𝔄' = cat_smc 𝔄"
    and "𝔅' = cat_smc 𝔅"
  shows "ntcf_ntsmcf 𝔑 : 𝔉' ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m 𝔊' : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅'"
  unfolding assms by (rule tm_ntcf_is_tm_ntsmcf)

lemmas [slicing_intros] = is_tm_ntcf.tm_ntcf_is_tm_ntsmcf'


text‹Rules.›

lemma (in is_tm_ntcf) is_tm_ntcf_axioms'[cat_small_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅" and "𝔉' = 𝔉" and "𝔊' = 𝔊"
  shows "𝔑 : 𝔉' ↦⇩C⇩F⇩.⇩t⇩m 𝔊' : 𝔄' ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅'"
  unfolding assms by (rule is_tm_ntcf_axioms)

mk_ide rf is_tm_ntcf_def[unfolded is_tm_ntcf_axioms_def]
  |intro is_tm_ntcfI|
  |dest is_tm_ntcfD[dest]|
  |elim is_tm_ntcfE[elim]|

lemmas [cat_small_cs_intros] = is_tm_ntcfD(1)

context is_tm_ntcf
begin

interpretation ntsmcf: is_tm_ntsmcf
  α ‹cat_smc 𝔄› ‹cat_smc 𝔅› ‹cf_smcf 𝔉› ‹cf_smcf 𝔊› ‹ntcf_ntsmcf 𝔑›
  by (rule tm_ntcf_is_tm_ntsmcf)

lemmas_with [unfolded slicing_simps]:
  tm_ntcf_NTMap_in_Vset = ntsmcf.tm_ntsmcf_NTMap_in_Vset

end

sublocale is_tm_ntcf ⊆ NTDom: is_tm_functor α 𝔄 𝔅 𝔉
  using tm_ntcf_is_tm_ntsmcf 
  by (intro is_tm_functorI) (auto intro: cat_cs_intros is_tm_ntsmcfD')

sublocale is_tm_ntcf ⊆ NTCod: is_tm_functor α 𝔄 𝔅 𝔊
  using tm_ntcf_is_tm_ntsmcf 
  by (intro is_tm_functorI) (auto intro: cat_cs_intros is_tm_ntsmcfD')


text‹Further rules.›

lemma is_tm_ntcfI':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof-
  interpret is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret 𝔉: is_tm_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tm_functor α 𝔄 𝔅 𝔊 by (rule assms(3))
  show ?thesis
  proof(intro is_tm_ntcfI)
    show "ntcf_ntsmcf 𝔑 : 
      cf_smcf 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m cf_smcf 𝔊 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ cat_smc 𝔅"
      by (intro is_tm_ntsmcfI') (auto intro: slicing_intros)
  qed (auto intro: cat_cs_intros)
qed

lemma is_tm_ntcfD':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof-
  interpret is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  show "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    by (auto simp: cat_small_cs_intros)
qed

lemmas [cat_small_cs_intros] = is_tm_ntcfD'(2,3)

lemma is_tm_ntcfE':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  obtains "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  using is_tm_ntcfD'[OF assms] by auto


text‹The set of all natural transformations with tiny maps is small.›

lemma small_all_tm_ntcfs[simp]: 
  "small {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅}"
proof(rule down)
  show 
    "{𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅} ⊆
      elts (set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_ntcfs if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔑 assume "∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    then obtain 𝔉 𝔊 𝔄 𝔅 where "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
      by clarsimp
    then interpret is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by simp
    have "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by (auto simp: cat_cs_intros)
    then show "∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by auto
  qed
qed

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

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


text‹Further elementary results.›

lemma these_tm_ntcfs_iff: (*not simp*)
  "𝔑 ∈⇩∘ these_tm_ntcfs α 𝔄 𝔅 𝔉 𝔊 ⟷ 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  by auto


subsubsection‹Opposite natural transformation of functors with tiny maps›

lemma (in is_tm_ntcf) is_tm_ntcf_op: "op_ntcf 𝔑 :
  op_cf 𝔊 ↦⇩C⇩F⇩.⇩t⇩m op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ op_cat 𝔅"
  by (intro is_tm_ntcfI')
    (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+

lemma (in is_tm_ntcf) is_tm_ntcf_op'[cat_op_intros]: 
  assumes "𝔊' = op_cf 𝔊"
    and "𝔉' = op_cf 𝔉"
    and "𝔄' = op_cat 𝔄"
    and "𝔅' = op_cat 𝔅"
  shows "op_ntcf 𝔑 : 𝔊' ↦⇩C⇩F⇩.⇩t⇩m 𝔉' : 𝔄' ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅'"
  unfolding assms by (rule is_tm_ntcf_op)

lemmas is_tm_ntcf_op[cat_op_intros] = is_tm_ntcf.is_tm_ntcf_op'


subsubsection‹
Vertical composition of natural transformations of 
functors with tiny maps
›

lemma ntcf_vcomp_is_tm_ntcf[cat_small_cs_intros]:
  assumes "𝔐 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩m ℌ : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m ℌ : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof-
  interpret 𝔐: is_tm_ntcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(1))
  interpret 𝔑: is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis 
    by (rule is_tm_ntcfI') (auto intro: cat_cs_intros cat_small_cs_intros) 
qed


subsubsection‹Identity natural transformation of a functor with tiny maps›

lemma (in is_tm_functor) tm_cf_ntcf_id_is_tm_ntcf:
  "ntcf_id 𝔉 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  by (intro is_tm_ntcfI') (auto intro: cat_cs_intros cat_small_cs_intros)

lemma (in is_tm_functor) tm_cf_ntcf_id_is_tm_ntcf':
  assumes "𝔉' = 𝔉" and "𝔊' = 𝔉"
  shows "ntcf_id 𝔉 : 𝔉' ↦⇩C⇩F⇩.⇩t⇩m 𝔊': 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  unfolding assms(1,2) by (rule tm_cf_ntcf_id_is_tm_ntcf)

lemmas [cat_small_cs_intros] = is_tm_functor.tm_cf_ntcf_id_is_tm_ntcf'


subsubsection‹Constant natural transformation of functors with tiny maps›

lemma ntcf_const_is_tm_ntcf:
  assumes "tiny_category α 𝔍" and "category α ℭ" and "f : a ↦⇘ℭ⇙ b"
  shows "ntcf_const 𝔍 ℭ f : 
    cf_const 𝔍 ℭ a ↦⇩C⇩F⇩.⇩t⇩m cf_const 𝔍 ℭ b : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
    (is ‹?Cf : ?Ca ↦⇩C⇩F⇩.⇩t⇩m ?Cb : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ›)
proof(intro is_tm_ntcfI')
  interpret 𝔍: tiny_category α 𝔍 by (rule assms(1))
  interpret ℭ: category α ℭ by (rule assms(2))
  from assms show 
    "?Cf : ?Ca ↦⇩C⇩F ?Cb : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
    "cf_const 𝔍 ℭ a : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
    "cf_const 𝔍 ℭ b : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
    by (cs_concl cs_intro: cat_small_cs_intros cat_cs_intros)+
qed

lemma ntcf_const_is_tm_ntcf'[cat_small_cs_intros]:
  assumes "tiny_category α 𝔍" 
    and "category α ℭ"
    and "f : a ↦⇘ℭ⇙ b"
    and "𝔄 = cf_const 𝔍 ℭ a"
    and "𝔅 = cf_const 𝔍 ℭ b"
    and "𝔍' = 𝔍"
    and "ℭ' = ℭ"
  shows "ntcf_const 𝔍 ℭ f : 𝔄 ↦⇩C⇩F⇩.⇩t⇩m 𝔅 : 𝔍' ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ'"
  using assms(1-3) unfolding assms(4-7) by (rule ntcf_const_is_tm_ntcf)


subsubsection‹Natural isomorphisms of functors with tiny maps›

locale is_tm_iso_ntcf = is_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 + is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 
  for α 𝔄 𝔅 𝔉 𝔊 𝔑

syntax "_is_tm_iso_ntcf" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ : _ ↦⇩C⇩F⇩.⇩t⇩m⇩.⇩i⇩s⇩o _ : _ ↦↦⇩C⇩.⇩t⇩mı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_tm_iso_ntcf" ⇌ is_tm_iso_ntcf
translations "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" ⇌
  "CONST is_tm_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑"


text‹Rules.›

mk_ide rf is_tm_iso_ntcf_def
  |intro is_tm_iso_ntcfI|
  |dest is_tm_iso_ntcfD[dest]|
  |elim is_tm_iso_ntcfE[elim]|

lemmas [ntcf_cs_intros] = is_tm_iso_ntcfD

lemma iso_tm_ntcf_is_iso_arr:
  assumes "category α 𝔅" and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows [ntcf_cs_intros]: "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩m⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔑 = ntcf_id 𝔊"
    and "inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F 𝔑 = ntcf_id 𝔉"
proof-
  interpret 𝔅: category α 𝔅 by (rule assms(1))
  interpret 𝔑: is_tm_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms)
  note inv_𝔑 = iso_ntcf_is_iso_arr[OF 𝔑.is_iso_ntcf_axioms]
  show "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩m⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  proof(intro is_tm_iso_ntcfI)
    show "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by (intro inv_𝔑(1))
    interpret inv_𝔑: is_iso_ntcf α 𝔄 𝔅 𝔊 𝔉 ‹inv_ntcf 𝔑› by (rule inv_𝔑(1))
    show "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩m 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
      by (intro is_tm_ntcfI') (auto intro: cat_cs_intros cat_small_cs_intros)
  qed
  show "𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔑 = ntcf_id 𝔊" "inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F 𝔑 = ntcf_id 𝔉" 
    by (intro inv_𝔑(2,3))+
qed

lemma is_iso_arr_is_tm_iso_ntcf:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔐 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩m 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and [simp]: "𝔑 ∙⇩N⇩T⇩C⇩F 𝔐 = ntcf_id 𝔊"
    and [simp]: "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 = ntcf_id 𝔉"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof-
  interpret 𝔑: is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret 𝔐: is_tm_ntcf α 𝔄 𝔅 𝔊 𝔉 𝔐 by (rule assms(2))
  show ?thesis
  proof(rule is_tm_iso_ntcfI)
    show "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
      by (rule is_iso_arr_is_iso_ntcf) (auto intro: cat_small_cs_intros)
    show "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
      by (rule is_tm_ntcfI')
        (auto simp: 𝔑.tm_ntcf_NTMap_in_Vset intro: cat_small_cs_intros)
  qed
qed


subsubsection‹
Composition of a natural transformation 
of functors with tiny maps and a functor with tiny maps
›

lemma ntcf_cf_comp_is_tm_ntcf:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔅 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ" and "ℌ : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ : 𝔉 ∘⇩C⇩F ℌ ↦⇩C⇩F⇩.⇩t⇩m 𝔊 ∘⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof-
  interpret 𝔑: is_tm_ntcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_tm_functor α 𝔄 𝔅 ℌ by (rule assms(2))
  from assms show ?thesis
    by (intro is_tm_ntcfI)
      (
        cs_concl cs_shallow
          cs_simp: slicing_commute[symmetric] 
          cs_intro: cat_cs_intros smc_small_cs_intros slicing_intros
      )+
qed

lemma ntcf_cf_comp_is_tm_ntcf'[cat_small_cs_intros]:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔅 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ" 
    and "ℌ : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔉' = 𝔉 ∘⇩C⇩F ℌ"
    and "𝔊' = 𝔊 ∘⇩C⇩F ℌ"
  shows "𝔑 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F ℌ : 𝔉' ↦⇩C⇩F⇩.⇩t⇩m 𝔊' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (rule ntcf_cf_comp_is_tm_ntcf)


subsubsection‹
Composition of a functor with tiny maps 
and a natural transformation of functors with tiny maps
›

lemma cf_ntcf_comp_is_tm_ntcf:
  assumes "ℌ : 𝔅 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : ℌ ∘⇩C⇩F 𝔉 ↦⇩C⇩F⇩.⇩t⇩m ℌ ∘⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof-
  interpret ℌ: is_tm_functor α 𝔅 ℭ ℌ by (rule assms(1))
  interpret 𝔑: is_tm_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  from assms show ?thesis
    by (intro is_tm_ntcfI)
      (
        cs_concl cs_shallow
          cs_simp: slicing_commute[symmetric] 
          cs_intro: cat_cs_intros smc_small_cs_intros slicing_intros
      )+
qed

lemma cf_ntcf_comp_is_tm_ntcf'[cat_small_cs_intros]:
  assumes "ℌ : 𝔅 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ" 
    and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔉' = ℌ ∘⇩C⇩F 𝔉"
    and "𝔊' = ℌ ∘⇩C⇩F 𝔊"
  shows "ℌ ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : 𝔉' ↦⇩C⇩F⇩.⇩t⇩m 𝔊' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
  using assms(1,2) unfolding assms(3,4) by (rule cf_ntcf_comp_is_tm_ntcf)



subsection‹Tiny natural transformation of functors›


subsubsection‹Definition and elementary properties›

locale is_tiny_ntcf = is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 for α 𝔄 𝔅 𝔉 𝔊 𝔑 +
  assumes tiny_ntcf_is_tiny_ntsmcf: 
    "ntcf_ntsmcf 𝔑 :
      cf_smcf 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩i⇩n⇩y cf_smcf 𝔊 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ cat_smc 𝔅"

syntax "_is_tiny_ntcf" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y _ :/ _ ↦↦⇩C⇩.⇩t⇩i⇩n⇩yı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_tiny_ntcf" ⇌ is_tiny_ntcf
translations "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅" ⇌ 
  "CONST is_tiny_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑"

abbreviation all_tiny_ntcfs :: "V ⇒ V"
  where "all_tiny_ntcfs α ≡
    set {𝔑. ∃𝔄 𝔅 𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅}"

abbreviation tiny_ntcfs :: "V ⇒ V ⇒ V ⇒ V"
  where "tiny_ntcfs α 𝔄 𝔅 ≡
    set {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅}"

abbreviation these_tiny_ntcfs :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "these_tiny_ntcfs α 𝔄 𝔅 𝔉 𝔊 ≡
    set {𝔑. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅}"

lemma (in is_tiny_ntcf) tiny_ntcf_is_tiny_ntsmcf':
  assumes "α' = α"
    and "𝔉' = cf_smcf 𝔉"
    and "𝔊' = cf_smcf 𝔊"
    and "𝔄' = cat_smc 𝔄"
    and "𝔅' = cat_smc 𝔅"
  shows "ntcf_ntsmcf 𝔑 : 𝔉' ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊' : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α'⇙ 𝔅'"
  unfolding assms by (rule tiny_ntcf_is_tiny_ntsmcf)

lemmas [slicing_intros] = is_tiny_ntcf.tiny_ntcf_is_tiny_ntsmcf'


text‹Rules.›

lemma (in is_tiny_ntcf) is_tiny_ntcf_axioms'[cat_small_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅" and "𝔉' = 𝔉" and "𝔊' = 𝔊"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  unfolding assms by (rule is_tiny_ntcf_axioms)

mk_ide rf is_tiny_ntcf_def[unfolded is_tiny_ntcf_axioms_def]
  |intro is_tiny_ntcfI|
  |dest is_tiny_ntcfD[dest]|
  |elim is_tiny_ntcfE[elim]|


text‹Elementary properties.›

sublocale is_tiny_ntcf ⊆ NTDom: is_tiny_functor α 𝔄 𝔅 𝔉 
  using tiny_ntcf_is_tiny_ntsmcf 
  by (intro is_tiny_functorI) 
    (auto intro: cat_cs_intros simp: is_tiny_ntsmcf_iff)

sublocale is_tiny_ntcf ⊆ NTCod: is_tiny_functor α 𝔄 𝔅 𝔊
  using tiny_ntcf_is_tiny_ntsmcf 
  by (intro is_tiny_functorI) 
    (auto intro: cat_cs_intros simp: is_tiny_ntsmcf_iff)

sublocale is_tiny_ntcf ⊆ is_tm_ntcf 
  by (rule is_tm_ntcfI') (auto intro: cat_cs_intros cat_small_cs_intros)

lemmas (in is_tiny_ntcf) tiny_ntcf_is_tm_ntcf[cat_small_cs_intros] = 
  is_tm_ntcf_axioms

lemmas [cat_small_cs_intros] = is_tiny_ntcf.tiny_ntcf_is_tm_ntcf


text‹Further rules.›

lemma is_tiny_ntcfI':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
proof-
  interpret 𝔑: is_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret 𝔉: is_tiny_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tiny_functor α 𝔄 𝔅 𝔊 by (rule assms(3))
  show "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    by (intro is_tiny_ntcfI is_tiny_ntsmcfI') 
      (auto intro: cat_cs_intros slicing_intros)
qed

lemma is_tiny_ntcfD':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
proof-
  interpret 𝔑: is_tiny_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  show "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    by (auto intro: cat_small_cs_intros)
qed

lemmas [cat_small_cs_intros] = is_tiny_ntcfD'(2,3)

lemma is_tiny_ntcfE':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  obtains "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  using assms by (auto dest: is_tiny_ntcfD'(2,3))

lemma is_tiny_ntcf_iff:
  "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅 ⟷ 
    (
      𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅 ∧ 
      𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅 ∧ 
      𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅
    )"
   by (auto intro: is_tiny_ntcfI' dest: is_tiny_ntcfD'(2,3))

lemma (in is_tiny_ntcf) tiny_ntcf_in_Vset: "𝔑 ∈⇩∘ Vset α"
proof-
  note [cat_cs_intros] =
    tm_ntcf_NTMap_in_Vset
    NTDom.tiny_cf_in_Vset
    NTCod.tiny_cf_in_Vset
    NTDom.HomDom.tiny_cat_in_Vset
    NTDom.HomCod.tiny_cat_in_Vset
  show ?thesis
    by (subst ntcf_def) 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros V_cs_intros
      )
qed

lemma small_all_tiny_ntcfs[simp]: 
  "small {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅}"
proof(rule down)
  show "{𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅} ⊆ 
    elts (set {𝔑. ∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_ntcfs if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔑 assume "∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    then obtain 𝔉 𝔊 𝔄 𝔅 where "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
      by clarsimp
    then interpret is_tiny_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 .
    have "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by (auto intro: cat_cs_intros)
    then show "∃𝔉 𝔊 𝔄 𝔅. 𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by auto
  qed
qed

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

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

lemma tiny_ntcfs_vsubset_Vset[simp]: 
  "set {𝔑. ∃𝔉 𝔊. 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅} ⊆⇩∘ Vset α"
  (is ‹set ?ntcfs ⊆⇩∘ _›)
proof(cases ‹tiny_category α 𝔄 ∧ tiny_category α 𝔅›)
  case True
  then have "tiny_category α 𝔄" and "tiny_category α 𝔅" by auto
  show ?thesis 
  proof(rule vsubsetI)
    fix 𝔑 assume "𝔑 ∈⇩∘ set ?ntcfs"
    then obtain 𝔉 𝔊 where "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅" by auto
    then interpret is_tiny_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by simp
    from tiny_ntcf_in_Vset show "𝔑 ∈⇩∘ Vset α" by simp
  qed
next
  case False
  then have "set ?ntcfs = 0" 
    unfolding is_tiny_ntcf_iff is_tiny_functor_iff by auto
  then show ?thesis by simp
qed


text‹Further elementary results.›

lemma these_tiny_ntcfs_iff: (*not simp*) 
  "𝔑 ∈⇩∘ these_tiny_ntcfs α 𝔄 𝔅 𝔉 𝔊 ⟷ 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  by auto


text‹Size.›

lemma (in is_ntcf) ntcf_is_tiny_ntcf_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ 𝔅" 
proof(intro is_tiny_ntcfI)
  interpret β: 𝒵 β by (rule assms(1))
  show "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘β⇙ 𝔅"
    by (intro ntcf_is_ntcf_if_ge_Limit)
      (use assms(2) in ‹cs_concl cs_shallow cs_intro: dg_cs_intros›)+
  show "ntcf_ntsmcf 𝔑 : 
    cf_smcf 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩i⇩n⇩y cf_smcf 𝔊 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ cat_smc 𝔅"
    by 
      ( 
        rule is_ntsmcf.ntsmcf_is_tiny_ntsmcf_if_ge_Limit, 
        rule ntcf_is_ntsmcf;
        intro assms
     )
qed


subsubsection‹Opposite natural transformation of tiny functors›

lemma (in is_tiny_ntcf) is_tm_ntcf_op: "op_ntcf 𝔑 :
  op_cf 𝔊 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ op_cat 𝔅"
  by (intro is_tiny_ntcfI')
   (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+

lemma (in is_tiny_ntcf) is_tiny_ntcf_op'[cat_op_intros]: 
  assumes "𝔊' = op_cf 𝔊"
    and "𝔉' = op_cf 𝔉"
    and "𝔄' = op_cat 𝔄"
    and "𝔅' = op_cat 𝔅"
  shows "op_ntcf 𝔑 : 𝔊' ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔉' : 𝔄' ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅'"
  unfolding assms by (rule is_tm_ntcf_op)

lemmas is_tiny_ntcf_op[cat_op_intros] = is_tiny_ntcf.is_tiny_ntcf_op'


subsubsection‹Vertical composition of tiny natural transformations›

lemma ntsmcf_vcomp_is_tiny_ntsmcf[cat_small_cs_intros]:
  assumes "𝔐 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y ℌ : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y ℌ : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
proof-
  interpret 𝔐: is_tiny_ntcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(1))
  interpret 𝔑: is_tiny_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis by (rule is_tiny_ntcfI') (auto intro: cat_small_cs_intros)
qed


subsubsection‹Tiny identity natural transformation›

lemma (in is_tiny_functor) tiny_cf_ntcf_id_is_tiny_ntcf:
  "ntcf_id 𝔉 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  by (intro is_tiny_ntcfI') (auto intro: cat_small_cs_intros)

lemma (in is_tiny_functor) tiny_cf_ntcf_id_is_tiny_ntcf'[cat_small_cs_intros]:
  assumes "𝔉' = 𝔉" and "𝔊' = 𝔉"
  shows "ntcf_id 𝔉 : 𝔉' ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊' : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  unfolding assms by (rule tiny_cf_ntcf_id_is_tiny_ntcf)

lemmas [cat_small_cs_intros] = is_tiny_functor.tiny_cf_ntcf_id_is_tiny_ntcf'



subsection‹Tiny natural isomorphisms›


subsubsection‹Definition and elementary properties›

locale is_tiny_iso_ntcf = is_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 + is_tiny_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 
  for α 𝔄 𝔅 𝔉 𝔊 𝔑

syntax "_is_tiny_iso_ntcf" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ : _ ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o _ : _ ↦↦⇩C⇩.⇩t⇩i⇩n⇩yı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_tiny_iso_ntcf" ⇌ is_tiny_iso_ntcf
translations "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅" ⇌
  "CONST is_tiny_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑"


text‹Rules.›

mk_ide rf is_tiny_iso_ntcf_def
  |intro is_tiny_iso_ntcfI|
  |dest is_tiny_iso_ntcfD[dest]|
  |elim is_tiny_iso_ntcfE[elim]|

lemmas [ntcf_cs_intros] = is_tiny_iso_ntcfD(2)


text‹Elementary properties.›

sublocale is_tiny_iso_ntcf ⊆ is_tm_iso_ntcf 
  by (rule is_tm_iso_ntcfI) (auto intro: cat_cs_intros cat_small_cs_intros)

lemmas (in is_tiny_iso_ntcf) is_tm_iso_ntcf_axioms' = is_tm_iso_ntcf_axioms

lemmas [ntcf_cs_intros] = is_tiny_iso_ntcf.is_tm_iso_ntcf_axioms'


text‹Further rules.›

lemma is_tiny_iso_ntcfI':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
proof-
  interpret 𝔑: is_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret 𝔉: is_tiny_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tiny_functor α 𝔄 𝔅 𝔊 by (rule assms(3))
  show "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    by (intro is_tiny_iso_ntcfI is_tiny_ntcfI') 
     (auto intro: cat_cs_intros cat_small_cs_intros)
qed

lemma is_tiny_iso_ntcfD':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
proof-
  interpret 𝔑: is_tiny_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  show "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    by (auto intro: cat_cs_intros cat_small_cs_intros)
qed

lemma is_tiny_iso_ntcfE':
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  obtains "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  using assms by (auto dest: is_tiny_ntcfD'(2,3))

lemma is_tiny_iso_ntcf_iff:
  "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅 ⟷ 
    (
      𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅 ∧ 
      𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅 ∧ 
      𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅
    )"
  by (auto intro: is_tiny_iso_ntcfI' dest: is_tiny_ntcfD'(2,3))


subsubsection‹Further properties›

lemma iso_tiny_ntcf_is_iso_arr:
  assumes "category α 𝔅" and "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows [ntcf_cs_intros]: "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔑 = ntcf_id 𝔊"
    and "inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F 𝔑 = ntcf_id 𝔉"
proof-
  interpret 𝔅: category α 𝔅 by (rule assms(1))
  interpret 𝔑: is_tiny_iso_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms)
  note inv_𝔑 = iso_ntcf_is_iso_arr[OF 𝔑.is_iso_ntcf_axioms]
  show "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  proof(intro is_tiny_iso_ntcfI)
    show "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by (intro inv_𝔑(1))
    interpret inv_𝔑: is_iso_ntcf α 𝔄 𝔅 𝔊 𝔉 ‹inv_ntcf 𝔑› by (rule inv_𝔑(1))
    show "inv_ntcf 𝔑 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
      by (intro is_tiny_ntcfI') (auto intro: cat_small_cs_intros cat_cs_intros)
  qed
  show "𝔑 ∙⇩N⇩T⇩C⇩F inv_ntcf 𝔑 = ntcf_id 𝔊" "inv_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F 𝔑 = ntcf_id 𝔉" 
    by (intro inv_𝔑(2,3))+
qed

lemma is_iso_arr_is_tiny_iso_ntcf:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔐 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and [simp]: "𝔑 ∙⇩N⇩T⇩C⇩F 𝔐 = ntcf_id 𝔊"
    and [simp]: "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 = ntcf_id 𝔉"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
proof-
  interpret 𝔑: is_tiny_ntcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret 𝔐: is_tiny_ntcf α 𝔄 𝔅 𝔊 𝔉 𝔐 by (rule assms(2))
  show ?thesis
  proof(rule is_tiny_iso_ntcfI)
    show "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
      by (rule is_iso_arr_is_iso_ntcf) (auto intro: cat_small_cs_intros)
    show "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
      by (rule is_tiny_ntcfI') (auto intro: cat_small_cs_intros)
  qed
qed

text‹\newpage›

end