Theory CZH_ECAT_Small_Functor

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for functors›
theory CZH_ECAT_Small_Functor
  imports 
    CZH_Foundations.CZH_SMC_Small_Semifunctor
    CZH_ECAT_Functor
    CZH_ECAT_Small_Category
begin



subsection‹Functor with tiny maps›


subsubsection‹Definition and elementary properties›

locale is_tm_functor = is_functor α 𝔄 𝔅 𝔉  for α 𝔄 𝔅 𝔉 +
  assumes tm_cf_is_semifunctor[slicing_intros]: 
    "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ cat_smc 𝔅" 

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

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

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

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

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

lemma (in is_tm_functor) tm_cf_is_semifunctor':
  assumes "α' = α"
    and "𝔄' = cat_smc 𝔄"
    and "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α'⇙ 𝔅'"
  unfolding assms by (rule tm_cf_is_semifunctor)

lemmas [slicing_intros] = is_tm_functor.tm_cf_is_semifunctor'


text‹Rules.›

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

mk_ide rf is_tm_functor_def[unfolded is_tm_functor_axioms_def]
  |intro is_tm_functorI|
  |dest is_tm_functorD[dest]|
  |elim is_tm_functorE[elim]|

lemmas [cat_small_cs_intros] = is_tm_functorD(1)


text‹Slicing.›

context is_tm_functor
begin

interpretation smcf: is_tm_semifunctor α ‹cat_smc 𝔄› ‹cat_smc 𝔅› ‹cf_smcf 𝔉›
  by (rule tm_cf_is_semifunctor)

lemmas_with [unfolded slicing_simps]:
  tm_cf_ObjMap_in_Vset[cat_cs_intros] = smcf.tm_smcf_ObjMap_in_Vset
  and tm_cf_ArrMap_in_Vset[cat_cs_intros] = smcf.tm_smcf_ArrMap_in_Vset

end

sublocale is_tm_functor ⊆ HomDom: tiny_category α 𝔄
proof(rule tiny_categoryI')
  show "𝔄⦇Obj⦈ ∈⇩∘ Vset α"
    by (rule vdomain_in_VsetI[OF tm_cf_ObjMap_in_Vset, unfolded cat_cs_simps])
  show "𝔄⦇Arr⦈ ∈⇩∘ Vset α"
    by (rule vdomain_in_VsetI[OF tm_cf_ArrMap_in_Vset, unfolded cat_cs_simps])
qed (simp add: cat_cs_intros)


text‹Further rules.›

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

lemma is_tm_functorD':
  assumes "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
    and "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
proof-
  interpret is_tm_functor α 𝔄 𝔅 𝔉 by (rule assms(1))    
  show "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α"
    and "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α"
    by (auto intro: cat_cs_intros)
qed

lemmas [cat_small_cs_intros] = is_tm_functorD'(1)

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


text‹Size.›

lemma small_all_tm_cfs[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅}"
proof(rule down)
  show 
    "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅} ⊆
      elts (set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_cfs if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔉 assume "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    then obtain 𝔄 𝔅 where "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" by clarsimp
    then interpret is_tm_functor α 𝔄 𝔅 𝔉 .
    show "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by (blast intro: is_functor_axioms')
  qed
qed


subsubsection‹Opposite functor with tiny maps›

lemma (in is_tm_functor) is_tm_functor_op: 
  "op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ op_cat 𝔅"
  by (intro is_tm_functorI', unfold cat_op_simps)
    (cs_concl cs_intro: cat_cs_intros cat_op_intros)

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

lemmas is_tm_functor_op[cat_op_intros] = is_tm_functor.is_tm_functor_op'


subsubsection‹Composition of functors with tiny maps›

lemma cf_comp_is_tm_functor[cat_small_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof(rule is_tm_functorI)
  interpret 𝔉: is_tm_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tm_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
  from 𝔉.tm_cf_is_semifunctor 𝔊.tm_cf_is_semifunctor show 
    "cf_smcf (𝔊 ∘⇩C⇩F 𝔉) : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ cat_smc ℭ"   
    by (auto simp: smc_small_cs_intros slicing_commute[symmetric])
  show "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" by (auto intro: cat_cs_intros)
qed


subsubsection‹Finite categories and functors with tiny maps›

lemma (in is_functor) cf_is_tm_functor_if_HomDom_finite_category:
  assumes "finite_category α 𝔄"
  shows "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof(intro is_tm_functorI)
  interpret 𝔄: finite_category α 𝔄 by (rule assms(1))
  show "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ cat_smc 𝔅"
    by 
      (
        rule 
          is_semifunctor.smcf_is_tm_semifunctor_if_HomDom_finite_semicategory[
            OF cf_is_semifunctor 𝔄.fin_cat_finite_semicategory
            ]
      )
qed (auto intro: cat_cs_intros)


subsubsection‹Constant functor with tiny maps›

lemma cf_const_is_tm_functor: 
  assumes "tiny_category α ℭ" and "category α 𝔇" and "a ∈⇩∘ 𝔇⦇Obj⦈"
  shows "cf_const ℭ 𝔇 a : ℭ ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔇"
proof(intro is_tm_functorI)
  from assms show "cf_smcf (cf_const ℭ 𝔇 a) : cat_smc ℭ ↦↦⇩S⇩M⇩C⇩.⇩t⇩m⇘α⇙ cat_smc 𝔇"
    by 
      (
        cs_concl 
          cs_simp: slicing_commute[symmetric] slicing_simps cat_cs_simps 
          cs_intro: slicing_intros cat_cs_intros smc_small_cs_intros
      )+
  from assms show "cf_const ℭ 𝔇 a : ℭ ↦↦⇩C⇘α⇙ 𝔇"
    by (cs_concl cs_intro: cat_cs_intros cat_small_cs_intros)
qed

lemma cf_const_is_tm_functor'[cat_small_cs_intros]:
  assumes "tiny_category α ℭ"
    and "category α 𝔇" 
    and "a ∈⇩∘ 𝔇⦇Obj⦈"
    and "ℭ' = ℭ"
    and "𝔇' = 𝔇"
  shows "cf_const ℭ 𝔇 a : ℭ' ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔇'"
  using assms(1-3) unfolding assms(4,5) by (rule cf_const_is_tm_functor)



subsection‹Tiny functor›


subsubsection‹Definition and elementary properties›

locale is_tiny_functor = is_functor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
  assumes tiny_cf_is_tiny_semifunctor[slicing_intros]: 
    "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ cat_smc 𝔅" 

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

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

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

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

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

lemmas [slicing_intros] = is_tiny_functor.tiny_cf_is_tiny_semifunctor


text‹Rules.›

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

mk_ide rf is_tiny_functor_def[unfolded is_tiny_functor_axioms_def]
  |intro is_tiny_functorI|
  |dest is_tiny_functorD[dest]|
  |elim is_tiny_functorE[elim]|

lemmas [cat_small_cs_intros] = is_tiny_functorD(1)


text‹Elementary properties.›

sublocale is_tiny_functor ⊆ HomDom: tiny_category α 𝔄
proof(intro tiny_categoryI')
  interpret smcf: is_tiny_semifunctor α ‹cat_smc 𝔄› ‹cat_smc 𝔅› ‹cf_smcf 𝔉›
    by (rule tiny_cf_is_tiny_semifunctor)
  show "𝔄⦇Obj⦈ ∈⇩∘ Vset α"
    by (rule smcf.HomDom.tiny_smc_Obj_in_Vset[unfolded slicing_simps])    
  show "𝔄⦇Arr⦈ ∈⇩∘ Vset α"
    by (rule smcf.HomDom.tiny_smc_Arr_in_Vset[unfolded slicing_simps])    
qed (auto simp: cat_cs_intros)

sublocale is_tiny_functor ⊆ HomCod: tiny_category α 𝔅
proof(intro tiny_categoryI')
  interpret smcf: is_tiny_semifunctor α ‹cat_smc 𝔄› ‹cat_smc 𝔅› ‹cf_smcf 𝔉›
    by (rule tiny_cf_is_tiny_semifunctor)
  show "𝔅⦇Obj⦈ ∈⇩∘ Vset α"
    by (rule smcf.HomCod.tiny_smc_Obj_in_Vset[unfolded slicing_simps])    
  show "𝔅⦇Arr⦈ ∈⇩∘ Vset α"
    by (rule smcf.HomCod.tiny_smc_Arr_in_Vset[unfolded slicing_simps])    
qed (auto simp: cat_cs_intros)

sublocale is_tiny_functor ⊆ is_tm_functor
proof(intro is_tm_functorI')
  interpret smcf: is_tiny_semifunctor α ‹cat_smc 𝔄› ‹cat_smc 𝔅› ‹cf_smcf 𝔉›
    by (rule tiny_cf_is_tiny_semifunctor)
  note Vset[unfolded slicing_simps] = 
    smcf.tm_smcf_ObjMap_in_Vset
    smcf.tm_smcf_ArrMap_in_Vset
  show "𝔉⦇ObjMap⦈ ∈⇩∘ Vset α" "𝔉⦇ArrMap⦈ ∈⇩∘ Vset α" by (intro Vset)+
qed (auto simp: cat_cs_intros)


text‹Further rules.›

lemma is_tiny_functorI':
  assumes [simp]: "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "tiny_category α 𝔄"
    and "tiny_category α 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
proof(intro is_tiny_functorI)
  interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(1))
  interpret 𝔄: tiny_category α 𝔄 by (rule assms(2))
  interpret 𝔅: tiny_category α 𝔅 by (rule assms(3))
  show "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ cat_smc 𝔅"
    by (intro is_tiny_semifunctorI') (auto intro: slicing_intros)
qed (rule assms(1))

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

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

lemma is_tiny_functorE':
  assumes "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" 
    and "tiny_category α 𝔄"
    and "tiny_category α 𝔅"
  using is_tiny_functorD'[OF assms] by auto

lemma is_tiny_functor_iff:
  "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅 ⟷ 
    (𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅 ∧ tiny_category α 𝔄 ∧ tiny_category α 𝔅)"
  by (auto intro: is_tiny_functorI' dest: is_tiny_functorD'(2,3))


text‹Size.›

lemma (in is_tiny_functor) tiny_cf_in_Vset: "𝔉 ∈⇩∘ Vset α"
proof-
  note [cat_cs_intros] = 
    tm_cf_ObjMap_in_Vset 
    tm_cf_ArrMap_in_Vset
    HomDom.tiny_cat_in_Vset 
    HomCod.tiny_cat_in_Vset 
  show ?thesis
    by (subst cf_def) 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros V_cs_intros
      )
qed

lemma small_all_tiny_cfs[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅}"
proof(rule down)
  show 
    "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅} ⊆ 
      elts (set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_cfs if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔉 assume "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
    then obtain 𝔄 𝔅 where "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅" by clarsimp
    then interpret is_tiny_functor α 𝔄 𝔅 𝔉 by simp
    show "∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by (meson is_functor_axioms)
  qed
qed

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

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

lemma (in is_functor) cf_is_tiny_functor_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ 𝔅"
proof(intro is_tiny_functorI)
  show "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩t⇩i⇩n⇩y⇘β⇙ cat_smc 𝔅"
    by 
      (
        rule is_semifunctor.smcf_is_tiny_semifunctor_if_ge_Limit, 
        rule cf_is_semifunctor; 
        intro assms
      )
qed (simp add: cf_is_functor_if_ge_Limit assms)


subsubsection‹Opposite tiny semifunctor›

lemma (in is_tiny_functor) is_tiny_functor_op: 
  "op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ op_cat 𝔅"
  by (intro is_tiny_functorI') 
    (cs_concl cs_intro: cat_op_intros cat_small_cs_intros)+

lemma (in is_tiny_functor) is_tiny_functor_op'[cat_op_intros]:  
  assumes "𝔄' = op_cat 𝔄" and "𝔅' = op_cat 𝔅" and "α' = α"
  shows "op_cf 𝔉 : 𝔄' ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_tiny_functor_op)

lemmas is_tiny_functor_op[cat_op_intros] = 
  is_tiny_functor.is_tiny_functor_op'


subsubsection‹Composition of tiny functors›

lemma cf_comp_is_tiny_functor[cat_small_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ ℭ"
proof-
  interpret 𝔉: is_tiny_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  interpret 𝔊: is_tiny_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
  show ?thesis by (rule is_tiny_functorI') (auto intro: cat_small_cs_intros)
qed


subsubsection‹Tiny constant functor›

lemma cf_const_is_tiny_functor:
  assumes "tiny_category α ℭ" and "tiny_category α 𝔇" and "a ∈⇩∘ 𝔇⦇Obj⦈"
  shows "cf_const ℭ 𝔇 a : ℭ ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔇"
proof(intro is_tiny_functorI')
  from assms show "cf_const ℭ 𝔇 a : ℭ ↦↦⇩C⇘α⇙ 𝔇"
    by (cs_concl cs_intro: cat_small_cs_intros)
qed (auto simp: assms(1,2))

lemma cf_const_is_tiny_functor':
  assumes "tiny_category α ℭ"
    and "tiny_category α 𝔇" 
    and "a ∈⇩∘ 𝔇⦇Obj⦈"
    and "ℭ' = ℭ"
    and "𝔇' = 𝔇"
  shows "cf_const ℭ 𝔇 a : ℭ' ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔇'"
  using assms(1-3) unfolding assms(4,5) by (rule cf_const_is_tiny_functor)

lemmas [cat_small_cs_intros] = cf_const_is_tiny_functor'

text‹\newpage›

end