Theory CZH_SMC_Small_Semifunctor

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for semifunctors›
theory CZH_SMC_Small_Semifunctor
  imports 
    CZH_DG_Small_DGHM
    CZH_SMC_Semifunctor
    CZH_SMC_Small_Semicategory
begin



subsection‹Semifunctor with tiny maps›


subsubsection‹Definition and elementary properties›

locale is_tm_semifunctor = is_semifunctor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
  assumes tm_smcf_is_tm_dghm[slicing_intros]: 
    "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ smc_dg 𝔅" 

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

abbreviation (input) is_cn_tm_semifunctor :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_cn_tm_semifunctor α 𝔄 𝔅 𝔉 ≡ 𝔉 : op_dg 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"

syntax "_is_cn_tm_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" 
  (‹(_ :/ _ ⇩S⇩M⇩C⇩.⇩t⇩m↦↦ı _)› [51, 51, 51] 51)
syntax_consts "_is_cn_tm_semifunctor" ⇌ is_cn_tm_semifunctor
translations "𝔉 : 𝔄 ⇩S⇩M⇩C⇩.⇩t⇩m↦↦⇘α⇙ 𝔅" ⇀ "CONST is_cn_tm_semifunctor α 𝔄 𝔅 𝔉"

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

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

lemma (in is_tm_semifunctor) tm_smcf_is_tm_dghm':
  assumes "α' = α"
    and "𝔄' = smc_dg 𝔄"
    and "𝔅' = smc_dg 𝔅"
  shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩t⇩m⇘α'⇙ 𝔅'"
  unfolding assms by (rule tm_smcf_is_tm_dghm)

lemmas [slicing_intros] = is_tm_semifunctor.tm_smcf_is_tm_dghm'


text‹Rules.›

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

mk_ide rf is_tm_semifunctor_def[unfolded is_tm_semifunctor_axioms_def]
  |intro is_tm_semifunctorI|
  |dest is_tm_semifunctorD[dest]|
  |elim is_tm_semifunctorE[elim]|

lemmas [smc_small_cs_intros] = is_tm_semifunctorD(1)


text‹Slicing.›

context is_tm_semifunctor
begin

interpretation dghm: is_tm_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
  by (rule tm_smcf_is_tm_dghm)

lemmas_with [unfolded slicing_simps]:
  tm_smcf_ObjMap_in_Vset[smc_small_cs_intros] = dghm.tm_dghm_ObjMap_in_Vset
  and tm_smcf_ArrMap_in_Vset[smc_small_cs_intros] = dghm.tm_dghm_ArrMap_in_Vset

end


text‹Elementary properties.›

sublocale is_tm_semifunctor ⊆ HomDom: tiny_semicategory α 𝔄 
proof(rule tiny_semicategoryI')
  show "𝔄⦇Obj⦈ ∈⇩∘ Vset α"
    by (rule vdomain_in_VsetI[OF tm_smcf_ObjMap_in_Vset, unfolded smc_cs_simps])
  show "𝔄⦇Arr⦈ ∈⇩∘ Vset α"
    by (rule vdomain_in_VsetI[OF tm_smcf_ArrMap_in_Vset, unfolded smc_cs_simps])
qed (simp add: smc_cs_intros)


text‹Further rules.›

lemma is_tm_semifunctorI':
  assumes [simp]: "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and [simp]: "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
    and [simp]: "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
    and [simp]: "semicategory α 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof(intro is_tm_semifunctorI)
  interpret is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(1))
  show "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ smc_dg 𝔅"
    by (intro is_tm_dghmI', unfold slicing_simps) (auto simp: slicing_intros)
qed simp_all

lemma is_tm_semifunctorD':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "semicategory α 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
    and "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
proof-
  interpret is_tm_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(1))    
  show "semicategory α 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
    and "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
    by (auto intro: smc_cs_intros smc_small_cs_intros)
qed

lemmas [smc_small_cs_intros] = is_tm_semifunctorD'(1)

lemma is_tm_semifunctorE':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  obtains "semicategory α 𝔅"
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
    and "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
  using is_tm_semifunctorD'[OF assms] by simp


text‹Size.›

lemma small_all_tm_smcfs[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅}"
proof(rule down)
  show 
    "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅} ⊆
      elts (set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_smcfs if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔉 assume "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    then obtain 𝔄 𝔅 where "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" by clarsimp
    then interpret is_tm_semifunctor α 𝔄 𝔅 𝔉 by simp
    show "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" by (auto intro: is_semifunctor_axioms)
  qed
qed


subsubsection‹Opposite semifunctor with tiny maps›

lemma (in is_tm_semifunctor) is_tm_semifunctor_op: 
  "op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ op_smc 𝔅"
  by (intro is_tm_semifunctorI', unfold smc_op_simps)
    (cs_concl cs_intro: smc_cs_intros smc_op_intros smc_small_cs_intros)

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

lemmas is_tm_semifunctor_op[smc_op_intros] = is_tm_semifunctor.is_tm_semifunctor_op'


subsubsection‹Composition of semifunctors with tiny maps›

lemma smcf_comp_is_tm_semifunctor[smc_small_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof(rule is_tm_semifunctorI)
  interpret 𝔉: is_tm_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tm_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
  show "smcf_dghm (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ smc_dg ℭ"
    unfolding slicing_commute[symmetric] 
    using 𝔉.tm_smcf_is_tm_dghm 𝔊.tm_smcf_is_tm_dghm  
    by (auto simp: dg_small_cs_intros)
  show "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" by (auto intro: smc_cs_intros)
qed


subsubsection‹Finite semicategories and semifunctors with tiny maps›

lemma (in is_semifunctor) smcf_is_tm_semifunctor_if_HomDom_finite_semicategory:
  assumes "finite_semicategory α 𝔄"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof(intro is_tm_semifunctorI)
  interpret 𝔄: finite_semicategory α 𝔄 by (rule assms(1))
  show "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ smc_dg 𝔅"
    by 
      (
        rule is_dghm.dghm_is_tm_dghm_if_HomDom_finite_digraph[
          OF smcf_is_dghm 𝔄.fin_smc_finite_digraph
          ]
      )
qed (auto intro: smc_cs_intros)


subsubsection‹Constant semifunctor with tiny maps›

lemma smcf_const_is_tm_semifunctor: 
  assumes "tiny_semicategory α ℭ"
    and "semicategory α 𝔇" 
    and "f : a ↦⇘𝔇⇙ a"
    and "f ∘⇩A⇘𝔇⇙ f = f"
  shows "smcf_const ℭ 𝔇 a f : ℭ ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔇"
proof(intro is_tm_semifunctorI)
  interpret ℭ: tiny_semicategory α ℭ by (rule assms(1))
  interpret 𝔇: semicategory α 𝔇 by (rule assms(2))
  show "smcf_dghm (smcf_const ℭ 𝔇 a f) : smc_dg ℭ ↦↦⇩D⇩G⇩.⇩t⇩m⇘α⇙ smc_dg 𝔇"
    unfolding slicing_commute[symmetric]
    by (rule dghm_const_is_tm_dghm) 
      (auto simp: slicing_simps ℭ.tiny_smc_tiny_digraph assms(3) 𝔇.smc_digraph)
  from assms show "smcf_const ℭ 𝔇 a f : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
    by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
qed

lemma smcf_const_is_tm_semifunctor':
  assumes "tiny_semicategory α ℭ"
    and "semicategory α 𝔇" 
    and "f : a ↦⇘𝔇⇙ a"
    and "f ∘⇩A⇘𝔇⇙ f = f"
    and "ℭ' = ℭ"
    and "𝔇' = 𝔇"
  shows "smcf_const ℭ 𝔇 a f : ℭ' ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ 𝔇'"
  using assms(1-4) unfolding assms(5,6) by (rule smcf_const_is_tm_semifunctor)

lemmas [smc_small_cs_intros] = smcf_const_is_tm_semifunctor'



subsection‹Tiny semifunctor›


subsubsection‹Definition and elementary properties›

locale is_tiny_semifunctor = is_semifunctor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 + 
  assumes tiny_smcf_is_tiny_dghm[slicing_intros]: 
    "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘α⇙ smc_dg 𝔅"

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

abbreviation (input) is_cn_tiny_smcf :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_cn_tiny_smcf α 𝔄 𝔅 𝔉 ≡ 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"

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

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

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

lemmas [slicing_intros] = is_tiny_semifunctor.tiny_smcf_is_tiny_dghm


text‹Rules.›

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

mk_ide rf is_tiny_semifunctor_def[unfolded is_tiny_semifunctor_axioms_def]
  |intro is_tiny_semifunctorI|
  |dest is_tiny_semifunctorD[dest]|
  |elim is_tiny_semifunctorE[elim]|

lemmas [smc_small_cs_intros] = is_tiny_semifunctorD(1)


text‹Elementary properties.›

sublocale is_tiny_semifunctor ⊆ HomDom: tiny_semicategory α 𝔄
proof(intro tiny_semicategoryI')
  interpret dghm: is_tiny_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
    by (rule tiny_smcf_is_tiny_dghm)
  show "𝔄⦇Obj⦈ ∈⇩∘ Vset α"
    by (rule dghm.HomDom.tiny_dg_Obj_in_Vset[unfolded slicing_simps])    
  show "𝔄⦇Arr⦈ ∈⇩∘ Vset α"
    by (rule dghm.HomDom.tiny_dg_Arr_in_Vset[unfolded slicing_simps])    
qed (auto simp: smc_cs_intros)

sublocale is_tiny_semifunctor ⊆ HomCod: tiny_semicategory α 𝔅
proof(intro tiny_semicategoryI')
  interpret dghm: is_tiny_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
    by (rule tiny_smcf_is_tiny_dghm)
  show "𝔅⦇Obj⦈ ∈⇩∘ Vset α"
    by (rule dghm.HomCod.tiny_dg_Obj_in_Vset[unfolded slicing_simps])    
  show "𝔅⦇Arr⦈ ∈⇩∘ Vset α"
    by (rule dghm.HomCod.tiny_dg_Arr_in_Vset[unfolded slicing_simps])    
qed (auto simp: smc_cs_intros)

sublocale is_tiny_semifunctor ⊆ is_tm_semifunctor
proof(intro is_tm_semifunctorI')
  interpret dghm: is_tiny_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
    by (rule tiny_smcf_is_tiny_dghm)
  note Vset[unfolded slicing_simps] = 
    dghm.tiny_dghm_ObjMap_in_Vset
    dghm.tiny_dghm_ArrMap_in_Vset
  show "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α" "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α" by (intro Vset)+
qed (auto simp: smc_cs_intros)


text‹Further rules.›

lemma is_tiny_semifunctorI':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "tiny_semicategory α 𝔄"
    and "tiny_semicategory α 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  using assms 
  by 
    (
      auto simp: 
        smc_cs_simps 
        smc_cs_intros 
        is_semifunctor.smcf_is_dghm 
        is_tiny_dghm.intro 
        is_tiny_semifunctorI 
        tiny_semicategory.tiny_smc_tiny_digraph
    )

lemma is_tiny_semifunctorD':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "tiny_semicategory α 𝔄"
    and "tiny_semicategory α 𝔅"
proof-
  interpret is_tiny_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(1))
  show "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "tiny_semicategory α 𝔄" 
    and "tiny_semicategory α 𝔅"
    by (auto intro: smc_small_cs_intros)
qed

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

lemma is_tiny_semifunctorE':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "tiny_semicategory α 𝔄"
    and "tiny_semicategory α 𝔅"
  using is_tiny_semifunctorD'[OF assms] by auto

lemma is_tiny_semifunctor_iff:
  "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅 ⟷
    (𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅 ∧ tiny_semicategory α 𝔄 ∧ tiny_semicategory α 𝔅)"
  by (auto intro: is_tiny_semifunctorI' dest: is_tiny_semifunctorD'(2,3))


text‹Size.›

lemma (in is_tiny_semifunctor) tiny_smcf_in_Vset: "𝔉 ∈⇩∘ Vset α"
proof-
  note [smc_cs_intros] = 
    tm_smcf_ObjMap_in_Vset 
    tm_smcf_ArrMap_in_Vset
    HomDom.tiny_smc_in_Vset 
    HomCod.tiny_smc_in_Vset 
  show ?thesis
    by (subst smcf_def) 
      (
        cs_concl cs_shallow 
          cs_simp: smc_cs_simps cs_intro: smc_cs_intros V_cs_intros
      )
qed

lemma small_all_tiny_smcfs[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅}"
proof(rule down)
  show 
    "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅} ⊆ 
      elts (set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_smcfs if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔉 assume "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    then obtain 𝔄 𝔅 where "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅" by clarsimp
    then interpret is_tiny_semifunctor α 𝔄 𝔅 𝔉 by simp
    show "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" using is_semifunctor_axioms by auto
  qed
qed

lemma tiny_smcfs_vsubset_Vset[simp]: 
  "set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅} ⊆⇩∘ Vset α"
proof(rule vsubsetI)
  fix 𝔉 assume "𝔉 ∈⇩∘ all_tiny_smcfs α"
  then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅" by clarsimp
  then show "𝔉 ∈⇩∘ Vset α" by (auto simp: is_tiny_semifunctor.tiny_smcf_in_Vset)
qed

lemma (in is_semifunctor) smcf_is_tiny_semifunctor_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ 𝔅"
proof(intro is_tiny_semifunctorI)
  show "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩t⇩i⇩n⇩y⇘β⇙ smc_dg 𝔅"
    by 
      (
        rule is_dghm.dghm_is_tiny_dghm_if_ge_Limit, 
        rule smcf_is_dghm; 
        intro assms
      )
qed (simp add: smcf_is_semifunctor_if_ge_Limit assms)


subsubsection‹Opposite tiny semifunctor›

lemma (in is_tiny_semifunctor) is_tiny_semifunctor_op: 
  "op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ op_smc 𝔅"
  by (intro is_tiny_semifunctorI') 
    (cs_concl cs_shallow cs_intro: smc_small_cs_intros smc_op_intros)+

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

lemmas is_tiny_semifunctor_op[smc_op_intros] = 
  is_tiny_semifunctor.is_tiny_semifunctor_op'


subsubsection‹Composition of tiny semifunctors›

lemma smcf_comp_is_tiny_semifunctor[smc_small_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ ℭ"
proof-
  interpret 𝔉: is_tiny_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tiny_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
  show ?thesis 
    by (rule is_tiny_semifunctorI') 
      (cs_concl cs_intro: smc_cs_intros smc_small_cs_intros)
qed


subsubsection‹Tiny constant semifunctor›

lemma smcf_const_is_tiny_semifunctor:
  assumes "tiny_semicategory α ℭ" 
    and "tiny_semicategory α 𝔇" 
    and "f : a ↦⇘𝔇⇙ a"
    and "f ∘⇩A⇘𝔇⇙ f = f"
  shows "smcf_const ℭ 𝔇 a f : ℭ ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔇"
proof(intro is_tiny_semifunctorI')
  from assms show "smcf_const ℭ 𝔇 a f : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
    by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_small_cs_intros)
qed (auto simp: assms(1,2))

lemma smcf_const_is_tiny_semifunctor'[smc_small_cs_intros]:
  assumes "tiny_semicategory α ℭ"
    and "tiny_semicategory α 𝔇" 
    and "f : a ↦⇘𝔇⇙ a"
    and "f ∘⇩A⇘𝔇⇙ f = f"
    and "ℭ' = ℭ"
    and "𝔇' = 𝔇"
  shows "smcf_const ℭ 𝔇 a f : ℭ' ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔇'"
  using assms(1-4) unfolding assms(5,6) by (rule smcf_const_is_tiny_semifunctor)

text‹\newpage›

end