Theory CZH_SMC_Small_NTSMCF

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for natural transformations of semifunctors›
theory CZH_SMC_Small_NTSMCF
  imports 
    CZH_DG_Small_TDGHM
    CZH_SMC_Small_Semifunctor
    CZH_SMC_NTSMCF
begin



subsection‹Natural transformation of semifunctors with tiny maps›


subsubsection‹Definition and elementary properties›

locale is_tm_ntsmcf = is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 for α 𝔄 𝔅 𝔉 𝔊 𝔑 +
  assumes tm_ntsmcf_is_tm_tdghm[slicing_intros]: "ntsmcf_tdghm 𝔑 :
    smcf_dghm 𝔉 ↦⇩D⇩G⇩H⇩M⇩.⇩t⇩m smcf_dghm 𝔊 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ smc_dg 𝔅"

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

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

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

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

lemma (in is_tm_ntsmcf) tm_ntsmcf_is_tm_tdghm':
  assumes "α' = α"
    and "𝔉' = smcf_dghm 𝔉"
    and "𝔊' = smcf_dghm 𝔊"
    and "𝔄' = smc_dg 𝔄"
    and "𝔅' = smc_dg 𝔅"
  shows "ntsmcf_tdghm 𝔑 :
    𝔉' ↦⇩D⇩G⇩H⇩M⇩.⇩t⇩m 𝔊' : 𝔄' ↦↦⇩D⇩G⇩.⇩t⇩m⇘α'⇙ 𝔅'"
  unfolding assms by (rule tm_ntsmcf_is_tm_tdghm)

lemmas [slicing_intros] = is_tm_ntsmcf.tm_ntsmcf_is_tm_tdghm'


text‹Rules.›

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

mk_ide rf is_tm_ntsmcf_def[unfolded is_tm_ntsmcf_axioms_def]
  |intro is_tm_ntsmcfI|
  |dest is_tm_ntsmcfD[dest]|
  |elim is_tm_ntsmcfE[elim]|

lemmas [smc_small_cs_intros] = is_tm_ntsmcfD(1)


text‹Slicing.›

context is_tm_ntsmcf
begin

interpretation tdghm: is_tm_tdghm
  α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉› ‹smcf_dghm 𝔊› ‹ntsmcf_tdghm 𝔑›
  by (rule tm_ntsmcf_is_tm_tdghm)

lemmas_with [unfolded slicing_simps]:
  tm_ntsmcf_NTMap_in_Vset = tdghm.tm_tdghm_NTMap_in_Vset

end


text‹Elementary properties.›

sublocale is_tm_ntsmcf ⊆ NTDom: is_tm_semifunctor α 𝔄 𝔅 𝔉 
  using tm_ntsmcf_is_tm_tdghm 
  by (intro is_tm_semifunctorI) (auto simp: smc_cs_intros)

sublocale is_tm_ntsmcf ⊆ NTCod: is_tm_semifunctor α 𝔄 𝔅 𝔊
  using tm_ntsmcf_is_tm_tdghm 
  by (intro is_tm_semifunctorI) (auto simp: smc_cs_intros)


text‹Further rules.›

lemma is_tm_ntsmcfI':
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof-
  interpret is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret 𝔉: is_tm_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tm_semifunctor α 𝔄 𝔅 𝔊 by (rule assms(3))
  show ?thesis
  proof(intro is_tm_ntsmcfI)
    show "ntsmcf_tdghm 𝔑 :
      smcf_dghm 𝔉 ↦⇩D⇩G⇩H⇩M⇩.⇩t⇩m smcf_dghm 𝔊 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ smc_dg 𝔅"
      by (intro is_tm_tdghmI) (auto simp: slicing_intros)
  qed (auto simp: assms(2,3) vfsequence_axioms smc_cs_intros)
qed

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

lemmas [smc_small_cs_intros] = is_tm_ntsmcfD'(2,3)


text‹Size.›

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

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

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


text‹Further elementary results.›

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


subsubsection‹
Opposite natural transformation of semifunctors with tiny maps
›

lemma (in is_tm_ntsmcf) is_tm_ntsmcf_op: "op_ntsmcf 𝔑 : 
  op_smcf 𝔊 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ op_smc 𝔅"
  by (intro is_tm_ntsmcfI') 
    (cs_concl cs_shallow cs_intro: smc_cs_intros smc_op_intros)+

lemma (in is_tm_ntsmcf) is_tm_ntsmcf_op'[smc_op_intros]: 
  assumes "𝔊' = op_smcf 𝔊"
    and "𝔉' = op_smcf 𝔉"
    and "𝔄' = op_smc 𝔄"
    and "𝔅' = op_smc 𝔅"
  shows "op_ntsmcf 𝔑 : 𝔊' ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m 𝔉' : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅'"
  unfolding assms by (rule is_tm_ntsmcf_op)

lemmas is_tm_ntsmcf_op[smc_op_intros] = is_tm_ntsmcf.is_tm_ntsmcf_op'


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

lemma ntsmcf_vcomp_is_tm_ntsmcf[smc_small_cs_intros]:
  assumes "𝔐 : 𝔊 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔐 ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof-
  interpret 𝔐: is_tm_ntsmcf α 𝔄 𝔅 𝔊 ℌ 𝔐 by (rule assms(1))
  interpret 𝔑: is_tm_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  show ?thesis 
    by (rule is_tm_ntsmcfI') (auto intro: smc_cs_intros smc_small_cs_intros)
qed 


subsubsection‹
Composition of a natural transformation of semifunctors and a semifunctor
›

lemma ntsmcf_smcf_comp_is_tm_ntsmcf:
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ ℭ" and "ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔑 ∘⇩N⇩T⇩S⇩M⇩C⇩F⇩-⇩S⇩M⇩C⇩F ℌ : 𝔉 ∘⇩S⇩M⇩C⇩F ℌ ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m 𝔊 ∘⇩S⇩M⇩C⇩F ℌ : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof-
  interpret 𝔑: is_tm_ntsmcf α 𝔅 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  interpret ℌ: is_tm_semifunctor α 𝔄 𝔅 ℌ by (rule assms(2))
  from assms show ?thesis
    by (intro is_tm_ntsmcfI)
      (
        cs_concl 
          cs_simp: slicing_commute[symmetric] 
          cs_intro: smc_cs_intros dg_small_cs_intros slicing_intros
      )+
qed

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


subsubsection‹
Composition of a semifunctor and a natural transformation of semifunctors
›

lemma smcf_ntsmcf_comp_is_tm_ntsmcf:
  assumes "ℌ : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ ℭ" and "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "ℌ ∘⇩S⇩M⇩C⇩F⇩-⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 : ℌ ∘⇩S⇩M⇩C⇩F 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩m ℌ ∘⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof-
  interpret ℌ: is_tm_semifunctor α 𝔅 ℭ ℌ by (rule assms(1))
  interpret 𝔑: is_tm_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(2))
  from assms show ?thesis
    by (intro is_tm_ntsmcfI)
      (
        cs_concl 
          cs_simp: slicing_commute[symmetric] 
          cs_intro: smc_cs_intros dg_small_cs_intros slicing_intros
      )+
qed

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



subsection‹Tiny natural transformation of semifunctors›


subsubsection‹Definition and elementary properties›

locale is_tiny_ntsmcf = is_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 for α 𝔄 𝔅 𝔉 𝔊 𝔑 +
  assumes tiny_ntsmcf_is_tdghm[slicing_intros]: "ntsmcf_tdghm 𝔑 :
    smcf_dghm 𝔉 ↦⇩D⇩G⇩H⇩M⇩.⇩t⇩i⇩n⇩y smcf_dghm 𝔊 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ smc_dg 𝔅" 

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

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

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

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

lemma (in is_tiny_ntsmcf) tiny_ntsmcf_is_tdghm':
  assumes "α' = α"
    and "𝔉' = smcf_dghm 𝔉"
    and "𝔊' = smcf_dghm 𝔊"
    and "𝔄' = smc_dg 𝔄"
    and "𝔅' = smc_dg 𝔅"
  shows "ntsmcf_tdghm 𝔑 : 𝔉' ↦⇩D⇩G⇩H⇩M⇩.⇩t⇩i⇩n⇩y 𝔊' : 𝔄' ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α'⇙ 𝔅'"
  unfolding assms by (rule tiny_ntsmcf_is_tdghm)

lemmas [slicing_intros] = is_tiny_ntsmcf.tiny_ntsmcf_is_tdghm'


text‹Rules.›

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

mk_ide rf is_tiny_ntsmcf_def[unfolded is_tiny_ntsmcf_axioms_def]
  |intro is_tiny_ntsmcfI|
  |dest is_tiny_ntsmcfD[dest]|
  |elim is_tiny_ntsmcfE[elim]|


text‹Elementary properties.›

sublocale is_tiny_ntsmcf ⊆ NTDom: is_tiny_semifunctor α 𝔄 𝔅 𝔉 
  using tiny_ntsmcf_is_tdghm 
  by (intro is_tiny_semifunctorI) (auto simp: smc_cs_intros)

sublocale is_tiny_ntsmcf ⊆ NTCod: is_tiny_semifunctor α 𝔄 𝔅 𝔊
  using tiny_ntsmcf_is_tdghm 
  by (intro is_tiny_semifunctorI) (auto simp: smc_cs_intros)

sublocale is_tiny_ntsmcf ⊆ is_tm_ntsmcf
  by (rule is_tm_ntsmcfI')
    (auto simp: tiny_ntsmcf_is_tdghm smc_small_cs_intros smc_cs_intros)


text‹Further rules.›

lemma is_tiny_ntsmcfI':
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  using assms by (auto intro: is_tiny_ntsmcfI)

lemma is_tiny_ntsmcfD':
  assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
proof-
  interpret is_tiny_ntsmcf α 𝔄 𝔅 𝔉 𝔊 𝔑 by (rule assms(1))
  show "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    and "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    by 
      (
        auto 
          simp: is_ntsmcf_axioms 
          intro:  
            NTDom.is_tiny_semifunctor_axioms 
            NTCod.is_tiny_semifunctor_axioms
      )
qed

lemmas [smc_small_cs_intros] = is_tiny_ntsmcfD'(2,3)

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

lemma is_tiny_ntsmcf_iff:
  "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅 ⟷
    (
      𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅 ∧
      𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅 ∧
      𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅
    )"
  using is_tiny_ntsmcfI' is_tiny_ntsmcfD' by (intro iffI) auto


text‹Size.›

lemma (in is_tiny_ntsmcf) tiny_ntsmcf_in_Vset: "𝔑 ∈⇩∘ Vset α"
proof-
  note [smc_cs_intros] =
    tm_ntsmcf_NTMap_in_Vset
    NTDom.tiny_smcf_in_Vset
    NTCod.tiny_smcf_in_Vset
    NTDom.HomDom.tiny_smc_in_Vset
    NTDom.HomCod.tiny_smc_in_Vset
  show ?thesis
    by (subst ntsmcf_def) 
      (
        cs_concl cs_shallow 
          cs_simp: smc_cs_simps cs_intro: smc_cs_intros V_cs_intros
      )
qed

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

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

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

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

lemma (in is_ntsmcf) ntsmcf_is_tiny_ntsmcf_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ 𝔅" 
proof(intro is_tiny_ntsmcfI)
  interpret β: 𝒵 β by (rule assms(1))
  show "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘β⇙ 𝔅"
    by (intro ntsmcf_is_ntsmcf_if_ge_Limit)
      (use assms(2) in ‹cs_concl cs_shallow cs_intro: dg_cs_intros›)+
  show "ntsmcf_tdghm 𝔑 :
    smcf_dghm 𝔉 ↦⇩D⇩G⇩H⇩M⇩.⇩t⇩i⇩n⇩y smcf_dghm 𝔊 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘β⇙ smc_dg 𝔅"
    by 
      ( 
        rule is_tdghm.tdghm_is_tiny_tdghm_if_ge_Limit, 
        rule ntsmcf_is_tdghm;
        intro assms
     )
qed


text‹Further elementary results.›

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


subsubsection‹Opposite natural transformation of tiny semifunctors›

lemma (in is_tiny_ntsmcf) is_tm_ntsmcf_op: "op_ntsmcf 𝔑 :
  op_smcf 𝔊 ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩i⇩n⇩y op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ op_smc 𝔅"
  by (intro is_tiny_ntsmcfI')
    (cs_concl cs_shallow cs_intro: smc_cs_intros smc_op_intros)+

lemma (in is_tiny_ntsmcf) is_tiny_ntsmcf_op'[smc_op_intros]: 
  assumes "𝔊' = op_smcf 𝔊"
    and "𝔉' = op_smcf 𝔉"
    and "𝔄' = op_smc 𝔄"
    and "𝔅' = op_smc 𝔅"
  shows "op_ntsmcf 𝔑 : 𝔊' ↦⇩S⇩M⇩C⇩F⇩.⇩t⇩i⇩n⇩y 𝔉' : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅'"
  unfolding assms by (rule is_tm_ntsmcf_op)

lemmas is_tiny_ntsmcf_op[smc_op_intros] = is_tiny_ntsmcf.is_tiny_ntsmcf_op'


subsubsection‹
Vertical composition of tiny natural transformations of 
semifunctors
›

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

text‹\newpage›

end