Theory CZH_ECAT_Small_Cone

(* Copyright 2021 (C) Mihails Milehins *)

section‹Smallness for cones and cocones›
theory CZH_ECAT_Small_Cone
  imports 
    CZH_ECAT_Cone
    CZH_ECAT_Small_NTCF
begin



subsection‹Cone with tiny maps and cocone with tiny maps›


subsubsection‹Definition and elementary properties›

locale is_tm_cat_cone =
  is_ntcf α 𝔍 ℭ ‹cf_const 𝔍 ℭ c› 𝔉 𝔑 + NTCod: is_tm_functor α 𝔍 ℭ 𝔉 
  for α c 𝔍 ℭ 𝔉 𝔑 +
  assumes tm_cat_cone_obj[cat_cs_intros, cat_small_cs_intros]: "c ∈⇩∘ ℭ⦇Obj⦈"

syntax "_is_tm_cat_cone" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e _ :/ _ ↦↦⇩C⇩.⇩t⇩mı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_tm_cat_cone" ⇌ is_tm_cat_cone
translations "𝔑 : c <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ" ⇌ 
  "CONST is_tm_cat_cone α c 𝔍 ℭ 𝔉 𝔑"

locale is_tm_cat_cocone = 
  is_ntcf α 𝔍 ℭ 𝔉 ‹cf_const 𝔍 ℭ c› 𝔑 + NTDom: is_tm_functor α 𝔍 ℭ 𝔉
  for α c 𝔍 ℭ 𝔉 𝔑 +
  assumes tm_cat_cocone_obj[cat_cs_intros, cat_small_cs_intros]: "c ∈⇩∘ ℭ⦇Obj⦈"

syntax "_is_tm_cat_cocone" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e _ :/ _ ↦↦⇩C⇩.⇩t⇩mı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_tm_cat_cocone" ⇌ is_tm_cat_cocone
translations "𝔑 : 𝔉 >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e c : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ" ⇌ 
  "CONST is_tm_cat_cocone α c 𝔍 ℭ 𝔉 𝔑"


text‹Rules.›

lemma (in is_tm_cat_cone) is_tm_cat_cone_axioms'[
    cat_cs_intros, cat_small_cs_intros
    ]:
  assumes "α' = α" and "c' = c" and "𝔍' = 𝔍" and "ℭ' = ℭ" and "𝔉' = 𝔉"
  shows "𝔑 : c' <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉' : 𝔍' ↦↦⇩C⇩.⇩t⇩m⇘α'⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_cone_axioms)

mk_ide rf is_tm_cat_cone_def[unfolded is_tm_cat_cone_axioms_def]
  |intro is_tm_cat_coneI|
  |dest is_tm_cat_coneD[dest!]|
  |elim is_tm_cat_coneE[elim!]|

lemma (in is_tm_cat_cocone) is_tm_cat_cocone_axioms'[
    cat_cs_intros, cat_small_cs_intros
    ]:
  assumes "α' = α" and "c' = c" and "𝔍' = 𝔍" and "ℭ' = ℭ" and "𝔉' = 𝔉"
  shows "𝔑 : 𝔉' >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e c' : 𝔍' ↦↦⇩C⇩.⇩t⇩m⇘α'⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_cocone_axioms)

mk_ide rf is_tm_cat_cocone_def[unfolded is_tm_cat_cocone_axioms_def]
  |intro is_tm_cat_coconeI|
  |dest is_tm_cat_coconeD[dest!]|
  |elim is_tm_cat_coconeE[elim!]|


text‹Duality.›

lemma (in is_tm_cat_cone) is_tm_cat_cocone_op:
  "op_ntcf 𝔑 : op_cf 𝔉 >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e c : op_cat 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ op_cat ℭ"
  by (intro is_tm_cat_coconeI)
    (
      cs_concl cs_shallow
        cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros
    )+

lemma (in is_tm_cat_cone) is_tm_cat_cocone_op'[cat_op_intros]:
  assumes "α' = α" and "𝔍' = op_cat 𝔍" and "ℭ' = op_cat ℭ" and "𝔉' = op_cf 𝔉"
  shows "op_ntcf 𝔑 : 𝔉' >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e c : 𝔍' ↦↦⇩C⇩.⇩t⇩m⇘α'⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_cocone_op)

lemmas [cat_op_intros] = is_tm_cat_cone.is_tm_cat_cocone_op'

lemma (in is_tm_cat_cocone) is_tm_cat_cone_op:
  "op_ntcf 𝔑 : c <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e op_cf 𝔉 : op_cat 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ op_cat ℭ"
  by (intro is_tm_cat_coneI)
    (
      cs_concl cs_shallow 
        cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros
    )

lemma (in is_tm_cat_cocone) is_tm_cat_cone_op'[cat_op_intros]:
  assumes "α' = α" and "𝔍' = op_cat 𝔍" and "ℭ' = op_cat ℭ" and "𝔉' = op_cf 𝔉"
  shows "op_ntcf 𝔑 : c <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉' : 𝔍' ↦↦⇩C⇩.⇩t⇩m⇘α'⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_cone_op)

lemmas [cat_op_intros] = is_cat_cocone.is_cat_cone_op'


text‹Elementary properties.›

lemma (in is_tm_cat_cone) tm_cat_cone_is_tm_ntcf'[
    cat_cs_intros, cat_small_cs_intros
    ]:
  assumes "c' = cf_const 𝔍 ℭ c"
  shows "𝔑 : c' ↦⇩C⇩F⇩.⇩t⇩m 𝔉 : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
  unfolding assms
proof(intro is_tm_ntcfI')
  interpret 𝔉: is_tm_functor α 𝔍 ℭ 𝔉 by (rule NTCod.is_tm_functor_axioms)
  show "cf_const 𝔍 ℭ c : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
    by (cs_concl cs_intro: cat_small_cs_intros cat_cs_intros)
qed (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros assms)+

lemmas [cat_small_cs_intros] = is_tm_cat_cone.tm_cat_cone_is_tm_ntcf'

sublocale is_tm_cat_cone ⊆ is_tm_ntcf α 𝔍 ℭ ‹cf_const 𝔍 ℭ c› 𝔉 𝔑 
  by (intro tm_cat_cone_is_tm_ntcf') simp

lemma (in is_tm_cat_cocone) tm_cat_cocone_is_tm_ntcf'[
    cat_cs_intros, cat_small_cs_intros
    ]:
  assumes "c' = cf_const 𝔍 ℭ c"
  shows "𝔑 : 𝔉 ↦⇩C⇩F⇩.⇩t⇩m c' : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
  unfolding assms
proof(intro is_tm_ntcfI')
  interpret 𝔉: is_tm_functor α 𝔍 ℭ 𝔉 by (rule NTDom.is_tm_functor_axioms)
  show "cf_const 𝔍 ℭ c : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
    by (cs_concl cs_intro: cat_small_cs_intros cat_cs_intros)
qed (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros assms)+

lemmas [cat_small_cs_intros, cat_cs_intros] = 
  is_tm_cat_cocone.tm_cat_cocone_is_tm_ntcf'

sublocale is_tm_cat_cocone ⊆ is_tm_ntcf α 𝔍 ℭ 𝔉 ‹cf_const 𝔍 ℭ c› 𝔑 
  by (intro tm_cat_cocone_is_tm_ntcf') simp

sublocale is_tm_cat_cone ⊆ is_cat_cone
  by (intro is_cat_coneI, rule is_ntcf_axioms, rule tm_cat_cone_obj)

lemmas (in is_tm_cat_cone) tm_cat_cone_is_cat_cone = is_cat_cone_axioms
lemmas [cat_small_cs_intros] = is_tm_cat_cone.tm_cat_cone_is_cat_cone

sublocale is_tm_cat_cocone ⊆ is_cat_cocone
  by (intro is_cat_coconeI, rule is_ntcf_axioms, rule tm_cat_cocone_obj)

lemmas (in is_tm_cat_cocone) tm_cat_cocone_is_cat_cocone = is_cat_cocone_axioms
lemmas [cat_small_cs_intros] = is_tm_cat_cocone.tm_cat_cocone_is_cat_cocone


subsubsection‹
Vertical composition of a natural transformation with tiny maps 
and a cone with tiny maps
›

lemma ntcf_vcomp_is_tm_cat_cone[cat_cs_intros]:
  assumes "𝔐 : 𝔊 ↦⇩C⇩F⇩.⇩t⇩m ℌ : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔑 : a <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔊 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  shows "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 : a <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e ℌ : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  by 
    (
      intro is_tm_cat_coneI ntcf_vcomp_is_ntcf; 
      (rule is_tm_ntcfD'[OF assms(1)])?; 
      (intro is_tm_cat_coneD[OF assms(2)])?
    )


subsubsection‹
Composition of a functor and a cone with tiny maps,
composition of a functor and a cocone with tiny maps
›

lemma cf_ntcf_comp_tm_cf_tm_cat_cone: 
  assumes "𝔑 : c <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" 
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
  shows "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : 𝔊⦇ObjMap⦈⦇c⦈ <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof-
  interpret 𝔑: is_tm_cat_cone α c 𝔄 𝔅 𝔉 𝔑 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))
  interpret 𝔊𝔉: is_tm_functor α 𝔄 ℭ ‹𝔊 ∘⇩C⇩F 𝔉› by (rule assms(3))
  show ?thesis
    by (intro is_tm_cat_coneI)
      (cs_concl cs_intro: cat_small_cs_intros cat_cs_intros is_cat_coneD)+
qed

lemma cf_ntcf_comp_tm_cf_tm_cat_cone'[cat_small_cs_intros]: 
  assumes "𝔑 : c <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" 
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
    and "c' = 𝔊⦇ObjMap⦈⦇c⦈"
    and "𝔊𝔉 = 𝔊 ∘⇩C⇩F 𝔉"
  shows "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : c' <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔊𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
  using assms(1,2,3) 
  unfolding assms(4,5) 
  by (rule cf_ntcf_comp_tm_cf_tm_cat_cone)

lemma cf_ntcf_comp_tm_cf_tm_cat_cocone:
  assumes "𝔑 : 𝔉 >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e c : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" 
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
  shows "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : 𝔊 ∘⇩C⇩F 𝔉 >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e 𝔊⦇ObjMap⦈⦇c⦈ : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof-
  interpret 𝔑: is_tm_cat_cocone α c 𝔄 𝔅 𝔉 𝔑 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))
  interpret 𝔊𝔉: is_tm_functor α 𝔄 ℭ ‹𝔊 ∘⇩C⇩F 𝔉› by (rule assms(3))
  show ?thesis
    by
      (
        rule is_tm_cat_cone.is_tm_cat_cocone_op
          [
            OF cf_ntcf_comp_tm_cf_tm_cat_cone[
              OF 𝔑.is_tm_cat_cone_op 𝔊.is_functor_op, unfolded cat_op_simps
              ],
            OF 𝔊𝔉.is_tm_functor_op[unfolded cat_op_simps],
            unfolded cat_op_simps
          ]
      )
qed

lemma cf_ntcf_comp_tm_cf_tm_cat_cocone'[cat_small_cs_intros]: 
  assumes "𝔑 : 𝔉 >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e c : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
    and "c' = 𝔊⦇ObjMap⦈⦇c⦈"
    and "𝔊𝔉 = 𝔊 ∘⇩C⇩F 𝔉"
  shows "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : 𝔊𝔉 >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e c' : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
  using assms(1-3) 
  unfolding assms(4,5) 
  by (rule cf_ntcf_comp_tm_cf_tm_cat_cocone)


subsubsection‹
Cones and cocones with tiny maps and constant natural transformations
›

lemma ntcf_vcomp_ntcf_const_is_tm_cat_cone:
  assumes "𝔑 : b <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" and "f : a ↦⇘𝔅⇙ b"
  shows "𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔄 𝔅 f : a <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof-
  interpret 𝔑: is_tm_cat_cone α b 𝔄 𝔅 𝔉 𝔑 by (rule assms(1))
  from assms(2) show ?thesis
    by (intro is_tm_cat_coneI)
      (cs_concl cs_intro: cat_small_cs_intros cat_cs_intros)
qed

lemma ntcf_vcomp_ntcf_const_is_tm_cat_cone'[cat_small_cs_intros]:
  assumes "𝔑 : b <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
    and "𝔐 = ntcf_const 𝔄 𝔅 f"
    and "f : a ↦⇘𝔅⇙ b"
  shows "𝔑 ∙⇩N⇩T⇩C⇩F 𝔐 : a <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  using assms(1,3)
  unfolding assms(2)
  by (rule ntcf_vcomp_ntcf_const_is_tm_cat_cone)

lemma ntcf_vcomp_ntcf_const_is_tm_cat_cocone:
  assumes "𝔑 : 𝔉 >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e a : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" and "f : a ↦⇘𝔅⇙ b"
  shows "ntcf_const 𝔄 𝔅 f ∙⇩N⇩T⇩C⇩F 𝔑 : 𝔉 >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e b : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
proof-
  interpret 𝔑: is_tm_cat_cocone α a 𝔄 𝔅 𝔉 𝔑 by (rule assms(1))
  from is_tm_cat_cone.is_tm_cat_cocone_op
    [
      OF ntcf_vcomp_ntcf_const_is_tm_cat_cone[
        OF 𝔑.is_tm_cat_cone_op, unfolded cat_op_simps, OF assms(2)
        ],
      unfolded cat_op_simps, 
      folded op_ntcf_ntcf_const
    ]
    assms(2)
  show ?thesis
    by (cs_prems cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros)
qed

lemma ntcf_vcomp_ntcf_const_is_tm_cat_cocone'[cat_cs_intros]:
  assumes "𝔑 : 𝔉 >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e a : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅" 
    and "𝔐 = ntcf_const 𝔄 𝔅 f"
    and "f : a ↦⇘𝔅⇙ b"
  shows "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 : 𝔉 >⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩c⇩o⇩n⇩e b : 𝔄 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ 𝔅"
  using assms(1,3)
  unfolding assms(2)
  by (rule ntcf_vcomp_ntcf_const_is_tm_cat_cocone)



subsection‹Small cone and small cocone functors›(*TODO: duality automation*)


subsubsection‹Definition and elementary properties›

definition tm_cf_Cone :: "V ⇒ V ⇒ V"
  where "tm_cf_Cone α 𝔉 =
    Hom⇩O⇩.⇩C⇘α⇙cat_Funct α (𝔉⦇HomDom⦈) (𝔉⦇HomCod⦈)(-,cf_map 𝔉) ∘⇩C⇩F
    op_cf (Δ⇩C⇩F⇩.⇩t⇩m α (𝔉⦇HomDom⦈) (𝔉⦇HomCod⦈))"

definition tm_cf_Cocone :: "V ⇒ V ⇒ V"
  where "tm_cf_Cocone α 𝔉 =
    Hom⇩O⇩.⇩C⇘α⇙cat_Funct α (𝔉⦇HomDom⦈) (𝔉⦇HomCod⦈)(cf_map 𝔉,-) ∘⇩C⇩F
    (Δ⇩C⇩F⇩.⇩t⇩m α (𝔉⦇HomDom⦈) (𝔉⦇HomCod⦈))"


text‹Alternative definitions.›

context is_tm_functor
begin

lemma tm_cf_Cone_def': 
  "tm_cf_Cone α 𝔉 =
    Hom⇩O⇩.⇩C⇘α⇙cat_Funct α 𝔄 𝔅(-,cf_map 𝔉) ∘⇩C⇩F op_cf (Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅)"
  unfolding tm_cf_Cone_def cat_cs_simps by simp

lemma tm_cf_Cocone_def': 
  "tm_cf_Cocone α 𝔉 =
    Hom⇩O⇩.⇩C⇘α⇙cat_Funct α 𝔄 𝔅(cf_map 𝔉,-) ∘⇩C⇩F (Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅)"
  unfolding tm_cf_Cocone_def cat_cs_simps by simp

end


subsubsection‹Object map›

lemma (in is_tm_functor) tm_cf_Cone_ObjMap_vsv[cat_small_cs_intros]:
  "vsv (tm_cf_Cone α 𝔉⦇ObjMap⦈)"
proof-
  interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  show ?thesis
    unfolding tm_cf_Cone_def
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps
          cs_intro: 
            cat_small_cs_intros 
            cat_cs_intros 
            cat_FUNCT_cs_intros 
            cat_op_intros
      )
qed

lemmas [cat_small_cs_intros] = is_tm_functor.tm_cf_Cone_ObjMap_vsv

lemma (in is_tm_functor) tm_cf_Cocone_ObjMap_vsv[cat_small_cs_intros]:
  "vsv (tm_cf_Cocone α 𝔉⦇ObjMap⦈)"
proof-
  interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  show ?thesis
    unfolding tm_cf_Cocone_def
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros 
       )
qed

lemmas [cat_small_cs_intros] = is_tm_functor.tm_cf_Cocone_ObjMap_vsv

lemma (in is_tm_functor) tm_cf_Cone_ObjMap_vdomain[cat_small_cs_simps]:
  assumes "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "𝒟⇩∘ (tm_cf_Cone α 𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
proof-
  from assms interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  from assms show ?thesis
    unfolding tm_cf_Cone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps
          cs_intro: 
            cat_small_cs_intros 
            cat_cs_intros 
            cat_FUNCT_cs_intros 
            cat_op_intros
      )
qed

lemmas [cat_small_cs_simps] = is_tm_functor.tm_cf_Cone_ObjMap_vdomain

lemma (in is_tm_functor) tm_cf_Cocone_ObjMap_vdomain[cat_small_cs_simps]:
  assumes "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "𝒟⇩∘ (tm_cf_Cocone α 𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
proof-
  from assms interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  from assms show ?thesis
    unfolding tm_cf_Cocone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps
          cs_intro: 
            cat_small_cs_intros 
            cat_cs_intros 
            cat_FUNCT_cs_intros 
            cat_op_intros
      )
qed

lemmas [cat_small_cs_simps] = is_tm_functor.tm_cf_Cocone_ObjMap_vdomain

lemma (in is_tm_functor) tm_cf_Cone_ObjMap_app[cat_small_cs_simps]:
  assumes "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "tm_cf_Cone α 𝔉⦇ObjMap⦈⦇b⦈ =
    Hom (cat_Funct α 𝔄 𝔅) (cf_map (cf_const 𝔄 𝔅 b)) (cf_map 𝔉)"
proof-
  from assms interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  from assms show ?thesis
    unfolding tm_cf_Cone_def
    by
      (
        cs_concl
          cs_simp: 
            cat_small_cs_simps
            cat_cs_simps
            cat_FUNCT_cs_simps
            cat_op_simps
          cs_intro: 
            cat_small_cs_intros
            cat_cs_intros 
            cat_FUNCT_cs_intros
            cat_op_intros
      )
qed

lemmas [cat_small_cs_simps] = is_tm_functor.tm_cf_Cone_ObjMap_app

lemma (in is_tm_functor) tm_cf_Cocone_ObjMap_app[cat_small_cs_simps]:
  assumes "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "tm_cf_Cocone α 𝔉⦇ObjMap⦈⦇b⦈ =
    Hom (cat_Funct α 𝔄 𝔅) (cf_map 𝔉) (cf_map (cf_const 𝔄 𝔅 b))"
proof-
  from assms interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  from assms show ?thesis
    unfolding tm_cf_Cocone_def
    by
      (
        cs_concl cs_shallow
          cs_simp:
            cat_small_cs_simps cat_cs_simps cat_FUNCT_cs_simps cat_op_simps
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
qed

lemmas [cat_small_cs_simps] = is_tm_functor.tm_cf_Cocone_ObjMap_app


subsubsection‹Arrow map›

lemma (in is_tm_functor) tm_cf_Cone_ArrMap_vsv[cat_small_cs_intros]:
  "vsv (tm_cf_Cone α 𝔉⦇ArrMap⦈)"
proof-
  interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  show ?thesis
    unfolding tm_cf_Cone_def
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps 
          cs_intro: 
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_small_cs_intros] = is_tm_functor.tm_cf_Cone_ArrMap_vsv

lemma (in is_tm_functor) tm_cf_Cocone_ArrMap_vsv[cat_small_cs_intros]:
  "vsv (tm_cf_Cocone α 𝔉⦇ArrMap⦈)"
proof-
  interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  show ?thesis
    unfolding tm_cf_Cocone_def
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps
          cs_intro:
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_small_cs_intros] = is_tm_functor.tm_cf_Cocone_ArrMap_vsv

lemma (in is_tm_functor) tm_cf_Cone_ArrMap_vdomain[cat_small_cs_simps]:
  assumes "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "𝒟⇩∘ (tm_cf_Cone α 𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
proof-
  interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  from assms show ?thesis
    unfolding tm_cf_Cone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps
          cs_intro:
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_small_cs_simps] = is_tm_functor.tm_cf_Cone_ArrMap_vdomain

lemma (in is_tm_functor) tm_cf_Cocone_ArrMap_vdomain[cat_small_cs_simps]:
  assumes "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "𝒟⇩∘ (tm_cf_Cocone α 𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
proof-
  interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  from assms show ?thesis
    unfolding tm_cf_Cocone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
qed

lemmas [cat_small_cs_simps] = is_tm_functor.tm_cf_Cocone_ArrMap_vdomain

lemma (in is_tm_functor) tm_cf_Cone_ArrMap_app[cat_small_cs_simps]:
  assumes "f : a ↦⇘𝔅⇙ b"
  shows "tm_cf_Cone α 𝔉⦇ArrMap⦈⦇f⦈ = cf_hom
    (cat_Funct α 𝔄 𝔅)
    [ntcf_arrow (ntcf_const 𝔄 𝔅 f), cat_Funct α 𝔄 𝔅⦇CId⦈⦇cf_map 𝔉⦈]⇩∘"
proof-
  interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  from assms show ?thesis
    unfolding tm_cf_Cone_def
    by
      (
        cs_concl
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps 
          cs_intro:
            cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_small_cs_simps] = is_tm_functor.tm_cf_Cone_ArrMap_app

lemma (in is_tm_functor) tm_cf_Cocone_ArrMap_app[cat_small_cs_simps]:
  assumes "f : a ↦⇘𝔅⇙ b"
  shows "tm_cf_Cocone α 𝔉⦇ArrMap⦈⦇f⦈ = cf_hom
    (cat_Funct α 𝔄 𝔅)
    [cat_Funct α 𝔄 𝔅⦇CId⦈⦇cf_map 𝔉⦈, ntcf_arrow (ntcf_const 𝔄 𝔅 f)]⇩∘"
proof-
  interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  from assms show ?thesis
    unfolding tm_cf_Cocone_def
    by
      (
        cs_concl
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps cat_op_simps
          cs_intro:
            cat_small_cs_intros
            cat_cs_intros
            cat_FUNCT_cs_intros
            cat_op_intros
      )
qed

lemmas [cat_small_cs_simps] = is_tm_functor.tm_cf_Cocone_ArrMap_app


subsubsection‹Small cone functor and small cocone functor are functors›

lemma (in is_tm_functor) tm_cf_cf_Cone_is_functor:
  "tm_cf_Cone α 𝔉 : op_cat 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
proof-
  interpret 𝔄𝔅: category α ‹cat_Funct α 𝔄 𝔅›
    by
      (
        cs_concl cs_shallow cs_intro:
          cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  interpret op_Δ: 
    is_functor α ‹op_cat 𝔅› ‹op_cat (cat_Funct α 𝔄 𝔅)› ‹op_cf (Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅)›
    by 
      (
        cs_concl cs_shallow cs_intro:
          cat_small_cs_intros cat_cs_intros cat_op_intros
      )
  have "Hom⇩O⇩.⇩C⇘α⇙cat_Funct α 𝔄 𝔅(-,cf_map 𝔉) :
    op_cat (cat_Funct α 𝔄 𝔅) ↦↦⇩C⇘α⇙ cat_Set α"
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_FUNCT_cs_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  then show "tm_cf_Cone α 𝔉 : op_cat 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
    unfolding tm_cf_Cone_def' by (cs_concl cs_intro: cat_cs_intros)
qed

lemma (in is_tm_functor) tm_cf_cf_Cone_is_functor'[cat_small_cs_intros]:
  assumes "𝔄' = op_cat 𝔅" and "𝔅' = cat_Set α" and "α' = α"
  shows "tm_cf_Cone α 𝔉 : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
  unfolding assms by (rule tm_cf_cf_Cone_is_functor)

lemmas [cat_small_cs_intros] = is_tm_functor.tm_cf_cf_Cone_is_functor'

lemma (in is_tm_functor) tm_cf_cf_Cocone_is_functor:
  "tm_cf_Cocone α 𝔉 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
proof-
  interpret Funct: category α ‹cat_Funct α 𝔄 𝔅›
    by
      (
        cs_concl cs_shallow cs_intro:
          cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  interpret Δ: is_functor α 𝔅 ‹cat_Funct α 𝔄 𝔅› ‹Δ⇩C⇩F⇩.⇩t⇩m α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_cs_intros)
  have "Hom⇩O⇩.⇩C⇘α⇙cat_Funct α 𝔄 𝔅(cf_map 𝔉,-) :
    cat_Funct α 𝔄 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_FUNCT_cs_simps
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  then show "tm_cf_Cocone α 𝔉 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
    unfolding tm_cf_Cocone_def' by (cs_concl cs_intro: cat_cs_intros)
qed

lemma (in is_tm_functor) tm_cf_cf_Cocone_is_functor'[cat_small_cs_intros]:
  assumes "𝔅' = cat_Set α" and "α' = α"
  shows "tm_cf_Cocone α 𝔉 : 𝔅 ↦↦⇩C⇘α'⇙ 𝔅'"
  unfolding assms by (rule tm_cf_cf_Cocone_is_functor)

lemmas [cat_small_cs_intros] = is_tm_functor.tm_cf_cf_Cocone_is_functor'

text‹\newpage›

end