Theory CZH_ECAT_Cone

(* Copyright 2021 (C) Mihails Milehins *)

section‹Cones and cocones›
theory CZH_ECAT_Cone
  imports 
    CZH_ECAT_NTCF
    CZH_ECAT_Hom
    CZH_ECAT_FUNCT
begin



subsection‹Cone and cocone›


subsubsection‹Definition and elementary properties›


text‹
In the context of this work, the concept of a cone corresponds to that of a cone
to the base of a functor from a vertex, as defined in Chapter III-4 in
\<^cite>‹"mac_lane_categories_2010"›; the concept of a cocone corresponds to that
of a cone from the base of a functor to a vertex, as defined in Chapter III-3
in \<^cite>‹"mac_lane_categories_2010"›.
›

locale is_cat_cone = is_ntcf α 𝔍 ℭ ‹cf_const 𝔍 ℭ c› 𝔉 𝔑 for α c 𝔍 ℭ 𝔉 𝔑 +
  assumes cat_cone_obj[cat_cs_intros]: "c ∈⇩∘ ℭ⦇Obj⦈"

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

locale is_cat_cocone = is_ntcf α 𝔍 ℭ 𝔉 ‹cf_const 𝔍 ℭ c› 𝔑 for α c 𝔍 ℭ 𝔉 𝔑 +
  assumes cat_cocone_obj[cat_cs_intros]: "c ∈⇩∘ ℭ⦇Obj⦈"

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


text‹Rules.›

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

mk_ide rf is_cat_cone_def[unfolded is_cat_cone_axioms_def]
  |intro is_cat_coneI|
  |dest is_cat_coneD[dest!]|
  |elim is_cat_coneE[elim!]|

lemma (in is_cat_cone) is_cat_coneD'[cat_cs_intros]:
  assumes "c' = cf_const 𝔍 ℭ c"
  shows "𝔑 : c' ↦⇩C⇩F 𝔉 : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
  unfolding assms by (cs_concl cs_shallow cs_intro: cat_cs_intros)

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

mk_ide rf is_cat_cocone_def[unfolded is_cat_cocone_axioms_def]
  |intro is_cat_coconeI|
  |dest is_cat_coconeD[dest!]|
  |elim is_cat_coconeE[elim!]|

lemma (in is_cat_cocone) is_cat_coconeD'[cat_cs_intros]:
  assumes "c' = cf_const 𝔍 ℭ c"
  shows "𝔑 : 𝔉 ↦⇩C⇩F c' : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
  unfolding assms by (cs_concl cs_shallow cs_intro: cat_cs_intros)


text‹Duality.›

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

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

lemmas [cat_op_intros] = is_cat_cone.is_cat_cocone_op'

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

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

lemmas [cat_op_intros] = is_cat_cocone.is_cat_cone_op'


text‹Elementary properties.›

lemma (in is_cat_cone) cat_cone_LArr_app_is_arr: 
  assumes "j ∈⇩∘ 𝔍⦇Obj⦈"
  shows "𝔑⦇NTMap⦈⦇j⦈ : c ↦⇘ℭ⇙ 𝔉⦇ObjMap⦈⦇j⦈"
proof-
  from assms have [simp]: "cf_const 𝔍 ℭ c⦇ObjMap⦈⦇j⦈ = c"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from ntcf_NTMap_is_arr[OF assms] show ?thesis by simp 
qed

lemma (in is_cat_cone) cat_cone_LArr_app_is_arr'[cat_cs_intros]: 
  assumes "j ∈⇩∘ 𝔍⦇Obj⦈" and "𝔉j = 𝔉⦇ObjMap⦈⦇j⦈"
  shows "𝔑⦇NTMap⦈⦇j⦈ : c ↦⇘ℭ⇙ 𝔉j"
  using assms(1) unfolding assms(2) by (rule cat_cone_LArr_app_is_arr)

lemmas [cat_cs_intros] = is_cat_cone.cat_cone_LArr_app_is_arr'

lemma (in is_cat_cocone) cat_cocone_LArr_app_is_arr: 
  assumes "j ∈⇩∘ 𝔍⦇Obj⦈"
  shows "𝔑⦇NTMap⦈⦇j⦈ : 𝔉⦇ObjMap⦈⦇j⦈ ↦⇘ℭ⇙ c"
proof-
  from assms have [simp]: "cf_const 𝔍 ℭ c⦇ObjMap⦈⦇j⦈ = c"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from ntcf_NTMap_is_arr[OF assms] show ?thesis by simp 
qed

lemma (in is_cat_cocone) cat_cocone_LArr_app_is_arr'[cat_cs_intros]: 
  assumes "j ∈⇩∘ 𝔍⦇Obj⦈" and "𝔉j = 𝔉⦇ObjMap⦈⦇j⦈"
  shows "𝔑⦇NTMap⦈⦇j⦈ : 𝔉j ↦⇘ℭ⇙ c"
  using assms(1) unfolding assms(2) by (rule cat_cocone_LArr_app_is_arr)

lemmas [cat_cs_intros] = is_cat_cocone.cat_cocone_LArr_app_is_arr'

lemma (in is_cat_cone) cat_cone_Comp_commute[cat_cs_simps]:
  assumes "f : a ↦⇘𝔍⇙ b"
  shows "𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ 𝔑⦇NTMap⦈⦇a⦈ = 𝔑⦇NTMap⦈⦇b⦈"
  using ntcf_Comp_commute[symmetric, OF assms] assms 
  by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

thm (*not ca_cs_simps*) is_cat_cone.cat_cone_Comp_commute

lemma (in is_cat_cocone) cat_cocone_Comp_commute[cat_cs_simps]:
  assumes "f : a ↦⇘𝔍⇙ b"
  shows "𝔑⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔑⦇NTMap⦈⦇a⦈"
  using ntcf_Comp_commute[OF assms] assms 
  by
    (
      cs_prems 
        cs_simp: cat_cs_simps dghm_const_ArrMap_app cs_intro: cat_cs_intros
    )

thm (*not ca_cs_simps*) is_cat_cocone.cat_cocone_Comp_commute


text‹Utilities/helper lemmas.›

lemma (in is_cat_cone) helper_cat_cone_ntcf_vcomp_Comp:
  assumes "𝔑' : c' <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
    and "f' : c' ↦⇘ℭ⇙ c" 
    and "𝔑' = 𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f'" 
    and "j ∈⇩∘ 𝔍⦇Obj⦈"
  shows "𝔑'⦇NTMap⦈⦇j⦈ = 𝔑⦇NTMap⦈⦇j⦈ ∘⇩A⇘ℭ⇙ f'"
proof-
  from assms(3) have "𝔑'⦇NTMap⦈⦇j⦈ = (𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f')⦇NTMap⦈⦇j⦈"
    by simp
  from this assms(1,2,4) show "𝔑'⦇NTMap⦈⦇j⦈ = 𝔑⦇NTMap⦈⦇j⦈ ∘⇩A⇘ℭ⇙ f'"
    by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed

lemma (in is_cat_cone) helper_cat_cone_Comp_ntcf_vcomp:
  assumes "𝔑' : c' <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
    and "f' : c' ↦⇘ℭ⇙ c" 
    and "⋀j. j ∈⇩∘ 𝔍⦇Obj⦈ ⟹ 𝔑'⦇NTMap⦈⦇j⦈ = 𝔑⦇NTMap⦈⦇j⦈ ∘⇩A⇘ℭ⇙ f'" 
  shows "𝔑' = 𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f'"
proof-
  interpret 𝔑': is_cat_cone α c' 𝔍 ℭ 𝔉 𝔑' by (rule assms(1))
  show ?thesis
  proof(rule ntcf_eqI[OF 𝔑'.is_ntcf_axioms])
    from assms(2) show 
      "𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f' : cf_const 𝔍 ℭ c' ↦⇩C⇩F 𝔉 : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show "𝔑'⦇NTMap⦈ = (𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f')⦇NTMap⦈"
    proof(rule vsv_eqI, unfold cat_cs_simps)
      show "vsv ((𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f')⦇NTMap⦈)"
        by (cs_concl cs_intro: cat_cs_intros)
      from assms show "𝔍⦇Obj⦈ = 𝒟⇩∘ ((𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f')⦇NTMap⦈)"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      fix j assume prems': "j ∈⇩∘ 𝔍⦇Obj⦈"
      with assms(1,2) show "𝔑'⦇NTMap⦈⦇j⦈ = (𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f')⦇NTMap⦈⦇j⦈"
        by (cs_concl cs_simp: cat_cs_simps assms(3) cs_intro: cat_cs_intros)
    qed auto
  qed simp_all
qed

lemma (in is_cat_cone) helper_cat_cone_Comp_ntcf_vcomp_iff:
  assumes "𝔑' : c' <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
  shows "f' : c' ↦⇘ℭ⇙ c ∧ 𝔑' = 𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f' ⟷
    f' : c' ↦⇘ℭ⇙ c ∧ (∀j∈⇩∘𝔍⦇Obj⦈. 𝔑'⦇NTMap⦈⦇j⦈ = 𝔑⦇NTMap⦈⦇j⦈ ∘⇩A⇘ℭ⇙ f')"
  using 
    helper_cat_cone_ntcf_vcomp_Comp[OF assms]
    helper_cat_cone_Comp_ntcf_vcomp[OF assms]
  by (intro iffI; elim conjE; intro conjI) metis+

lemma (in is_cat_cocone) helper_cat_cocone_ntcf_vcomp_Comp:
  assumes "𝔑' : 𝔉 >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e c' : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
    and "f' : c ↦⇘ℭ⇙ c'" 
    and "𝔑' = ntcf_const 𝔍 ℭ f' ∙⇩N⇩T⇩C⇩F 𝔑" 
    and "j ∈⇩∘ 𝔍⦇Obj⦈"
  shows "𝔑'⦇NTMap⦈⦇j⦈ = f' ∘⇩A⇘ℭ⇙ 𝔑⦇NTMap⦈⦇j⦈"
proof-
  interpret 𝔑': is_cat_cocone α c' 𝔍 ℭ 𝔉 𝔑' by (rule assms(1))
  from assms(3) have "op_ntcf 𝔑' = op_ntcf (ntcf_const 𝔍 ℭ f' ∙⇩N⇩T⇩C⇩F 𝔑)" by simp
  from this assms(2) have op_𝔑':
    "op_ntcf 𝔑' = op_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const (op_cat 𝔍) (op_cat ℭ) f'"
    by (cs_prems cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros)
  have "𝔑'⦇NTMap⦈⦇j⦈ = 𝔑⦇NTMap⦈⦇j⦈ ∘⇩A⇘op_cat ℭ⇙ f'"
    by 
      (
        rule is_cat_cone.helper_cat_cone_ntcf_vcomp_Comp[
          OF is_cat_cone_op 𝔑'.is_cat_cone_op, 
          unfolded cat_op_simps, 
          OF assms(2) op_𝔑' assms(4)
          ]
      )
  from this assms(2,4) show "𝔑'⦇NTMap⦈⦇j⦈ = f' ∘⇩A⇘ℭ⇙ 𝔑⦇NTMap⦈⦇j⦈"
    by 
      (
        cs_prems cs_shallow 
          cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
      )
qed

lemma (in is_cat_cocone) helper_cat_cocone_Comp_ntcf_vcomp:
  assumes "𝔑' : 𝔉 >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e c' : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
    and "f' : c ↦⇘ℭ⇙ c'" 
    and "⋀j. j ∈⇩∘ 𝔍⦇Obj⦈ ⟹ 𝔑'⦇NTMap⦈⦇j⦈ = f' ∘⇩A⇘ℭ⇙ 𝔑⦇NTMap⦈⦇j⦈" 
  shows "𝔑' = ntcf_const 𝔍 ℭ f' ∙⇩N⇩T⇩C⇩F 𝔑"
proof-
  interpret 𝔑': is_cat_cocone α c' 𝔍 ℭ 𝔉 𝔑' by (rule assms(1))
  from assms(2) have 𝔑'j: "𝔑'⦇NTMap⦈⦇j⦈ = 𝔑⦇NTMap⦈⦇j⦈ ∘⇩A⇘op_cat ℭ⇙ f'"
    if "j ∈⇩∘ 𝔍⦇Obj⦈" for j
    using that
    unfolding assms(3)[OF that] 
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_op_simps cat_cs_simps cs_intro: cat_cs_intros
      )
  have op_𝔑': 
    "op_ntcf 𝔑' = op_ntcf 𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const (op_cat 𝔍) (op_cat ℭ) f'"
    by 
      (
        rule is_cat_cone.helper_cat_cone_Comp_ntcf_vcomp[
          OF is_cat_cone_op 𝔑'.is_cat_cone_op,
          unfolded cat_op_simps, 
          OF assms(2) 𝔑'j, 
          simplified
          ]
      )
  from assms(2) show "𝔑' = (ntcf_const 𝔍 ℭ f' ∙⇩N⇩T⇩C⇩F 𝔑)"
    by 
      (
        cs_concl  
          cs_simp: 
            cat_op_simps op_𝔑' eq_op_ntcf_iff[symmetric, OF 𝔑'.is_ntcf_axioms]
          cs_intro: cat_cs_intros
      )
qed

lemma (in is_cat_cocone) helper_cat_cocone_Comp_ntcf_vcomp_iff:
  assumes "𝔑' : 𝔉 >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e c' : 𝔍 ↦↦⇩C⇘α⇙ ℭ"
  shows "f' : c ↦⇘ℭ⇙ c' ∧ 𝔑' = ntcf_const 𝔍 ℭ f' ∙⇩N⇩T⇩C⇩F 𝔑 ⟷
    f' : c ↦⇘ℭ⇙ c' ∧ (∀j∈⇩∘𝔍⦇Obj⦈. 𝔑'⦇NTMap⦈⦇j⦈ = f' ∘⇩A⇘ℭ⇙ 𝔑⦇NTMap⦈⦇j⦈)"
  using 
    helper_cat_cocone_ntcf_vcomp_Comp[OF assms]
    helper_cat_cocone_Comp_ntcf_vcomp[OF assms]
  by (intro iffI; elim conjE; intro conjI) metis+


subsubsection‹Vertical composition of a natural transformation and a cone›

lemma ntcf_vcomp_is_cat_cone[cat_cs_intros]:
  assumes "𝔐 : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔑 : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e ℌ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  by 
    (
      intro is_cat_coneI ntcf_vcomp_is_ntcf, rule assms(1); 
      rule is_cat_coneD[OF assms(2)]
    )


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

lemma cf_ntcf_comp_cf_cat_cone: 
  assumes "𝔑 : c <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : 𝔊⦇ObjMap⦈⦇c⦈ <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔑: is_cat_cone α c 𝔄 𝔅 𝔉 𝔑 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))
  show ?thesis
    by (intro is_cat_coneI)
      (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros )+
qed

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

lemma cf_ntcf_comp_cf_cat_cocone:
  assumes "𝔑 : 𝔉 >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e c : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F 𝔑 : 𝔊 ∘⇩C⇩F 𝔉 >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e 𝔊⦇ObjMap⦈⦇c⦈ : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔑: is_cat_cocone α c 𝔄 𝔅 𝔉 𝔑 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))
  show ?thesis
    by
      (
        rule is_cat_cone.is_cat_cocone_op
          [
            OF cf_ntcf_comp_cf_cat_cone[
              OF 𝔑.is_cat_cone_op 𝔊.is_functor_op, unfolded cat_op_simps
              ], 
            unfolded cat_op_simps
          ]
      )
qed

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


subsubsection‹Cones, cocones and constant natural transformations›

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

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

lemma ntcf_vcomp_ntcf_const_is_cat_cocone:
  assumes "𝔑 : 𝔉 >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e a : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "f : a ↦⇘𝔅⇙ b"
  shows "ntcf_const 𝔄 𝔅 f ∙⇩N⇩T⇩C⇩F 𝔑 : 𝔉 >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e b : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
proof-
  interpret 𝔑: is_cat_cocone α a 𝔄 𝔅 𝔉 𝔑 by (rule assms(1))
  from is_cat_cone.is_cat_cocone_op
    [
      OF ntcf_vcomp_ntcf_const_is_cat_cone[
        OF 𝔑.is_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_cat_cocone'[cat_cs_intros]:
  assumes "𝔑 : 𝔉 >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e a : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔐 = ntcf_const 𝔄 𝔅 f"
    and "f : a ↦⇘𝔅⇙ b"
  shows "𝔐 ∙⇩N⇩T⇩C⇩F 𝔑 : 𝔉 >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e b : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  using assms(1,3) 
  unfolding assms(2)
  by (rule ntcf_vcomp_ntcf_const_is_cat_cocone)

lemma ntcf_vcomp_ntcf_const_CId: 
  assumes "𝔑 : b <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  shows "𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔄 𝔅 (𝔅⦇CId⦈⦇b⦈) = 𝔑"
proof-

  interpret 𝔑: is_cat_cone α b 𝔄 𝔅 𝔉 𝔑 by (rule assms) 

  show ?thesis
  proof(rule ntcf_eqI)

    from 𝔑.cat_cone_obj show lhs_is_ntcf: 
      "𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔄 𝔅 (𝔅⦇CId⦈⦇b⦈) :
        cf_const 𝔄 𝔅 b ↦⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    then have dom_lhs: 
      "𝒟⇩∘ ((𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔄 𝔅 (𝔅⦇CId⦈⦇b⦈))⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (simp add: cat_cs_simps)

    from 𝔑.cat_cone_obj show "𝔑 : cf_const 𝔄 𝔅 b ↦⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    then have dom_rhs: "𝒟⇩∘ (𝔑⦇NTMap⦈) = 𝔄⦇Obj⦈"
      by (simp add: cat_cs_simps)

    show "(𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔄 𝔅 (𝔅⦇CId⦈⦇b⦈))⦇NTMap⦈ = 𝔑⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
      from prems 𝔑.cat_cone_obj show 
        "(𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔄 𝔅 (𝔅⦇CId⦈⦇b⦈))⦇NTMap⦈⦇a⦈ = 𝔑⦇NTMap⦈⦇a⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed (use lhs_is_ntcf in ‹cs_concl cs_intro: cat_cs_intros›)+

  qed simp_all

qed

lemma ntcf_vcomp_ntcf_const_CId'[cat_cs_simps]: 
  assumes "𝔑 : b <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔅' = 𝔅"
  shows "𝔑 ∙⇩N⇩T⇩C⇩F ntcf_const 𝔄 𝔅 (𝔅'⦇CId⦈⦇b⦈) = 𝔑"
  using assms(1) unfolding assms(2) by (rule ntcf_vcomp_ntcf_const_CId)



subsection‹Cone and cocone functors›


subsubsection‹Definition and elementary properties›


text‹See Chapter V-1 in \<^cite>‹"mac_lane_categories_2010"›.›

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

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


text‹An alternative form of the definition.›

context is_functor
begin

lemma cf_Cone_def': 
  "cf_Cone α β 𝔉 = Hom⇩O⇩.⇩C⇘β⇙cat_FUNCT α 𝔄 𝔅(-,cf_map 𝔉) ∘⇩C⇩F op_cf (Δ⇩C⇩F α 𝔄 𝔅)"
  unfolding cf_Cone_def cat_cs_simps by simp

lemma cf_Cocone_def': 
  "cf_Cocone α β 𝔉 = Hom⇩O⇩.⇩C⇘β⇙cat_FUNCT α 𝔄 𝔅(cf_map 𝔉,-) ∘⇩C⇩F (Δ⇩C⇩F α 𝔄 𝔅)"
  unfolding cf_Cocone_def cat_cs_simps by simp

end


subsubsection‹Object map›

lemma (in is_functor) cf_Cone_ObjMap_vsv[cat_cs_intros]:
  assumes "𝒵 β" and "α ∈⇩∘ β" 
  shows "vsv (cf_Cone α β 𝔉⦇ObjMap⦈)"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms(2) show ?thesis
    unfolding cf_Cone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps 
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_intros] = is_functor.cf_Cone_ObjMap_vsv

lemma (in is_functor) cf_Cocone_ObjMap_vsv[cat_cs_intros]:
  assumes "𝒵 β" and "α ∈⇩∘ β" 
  shows "vsv (cf_Cocone α β 𝔉⦇ObjMap⦈)"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms(2) show ?thesis
    unfolding cf_Cocone_def'
    by
      (
        cs_concl
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps 
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_intros] = is_functor.cf_Cocone_ObjMap_vsv

lemma (in is_functor) cf_Cone_ObjMap_vdomain[cat_cs_simps]:
  assumes "𝒵 β" and "α ∈⇩∘ β" and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "𝒟⇩∘ (cf_Cone α β 𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms show ?thesis
    unfolding cf_Cone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_simps] = is_functor.cf_Cone_ObjMap_vdomain

lemma (in is_functor) cf_Cocone_ObjMap_vdomain[cat_cs_simps]:
  assumes "𝒵 β" and "α ∈⇩∘ β" and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "𝒟⇩∘ (cf_Cocone α β 𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms show ?thesis
    unfolding cf_Cocone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_simps] = is_functor.cf_Cocone_ObjMap_vdomain

lemma (in is_functor) cf_Cone_ObjMap_app[cat_cs_simps]:
  assumes "𝒵 β" and "α ∈⇩∘ β" and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "cf_Cone α β 𝔉⦇ObjMap⦈⦇b⦈ =
    Hom (cat_FUNCT α 𝔄 𝔅) (cf_map (cf_const 𝔄 𝔅 b)) (cf_map 𝔉)"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms(2,3) show ?thesis
    unfolding cf_Cone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_simps] = is_functor.cf_Cone_ObjMap_app

lemma (in is_functor) cf_Cocone_ObjMap_app[cat_cs_simps]:
  assumes "𝒵 β" and "α ∈⇩∘ β" and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "cf_Cocone α β 𝔉⦇ObjMap⦈⦇b⦈ =
    Hom (cat_FUNCT α 𝔄 𝔅) (cf_map 𝔉) (cf_map (cf_const 𝔄 𝔅 b))"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms(2,3) show ?thesis
    unfolding cf_Cocone_def'
    by
      (
        cs_concl
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_simps] = is_functor.cf_Cocone_ObjMap_app


subsubsection‹Arrow map›

lemma (in is_functor) cf_Cone_ArrMap_vsv[cat_cs_intros]:
  assumes "𝒵 β" and "α ∈⇩∘ β" 
  shows "vsv (cf_Cone α β 𝔉⦇ArrMap⦈)"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms(2) show ?thesis
    unfolding cf_Cone_def
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps 
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_intros] = is_functor.cf_Cone_ArrMap_vsv

lemma (in is_functor) cf_Cocone_ArrMap_vsv[cat_cs_intros]:
  assumes "𝒵 β" and "α ∈⇩∘ β" 
  shows "vsv (cf_Cocone α β 𝔉⦇ArrMap⦈)"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms(2) show ?thesis
    unfolding cf_Cocone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps 
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_intros] = is_functor.cf_Cocone_ArrMap_vsv

lemma (in is_functor) cf_Cone_ArrMap_vdomain[cat_cs_simps]:
  assumes "𝒵 β" and "α ∈⇩∘ β" and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "𝒟⇩∘ (cf_Cone α β 𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms(2) show ?thesis
    unfolding cf_Cone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_simps] = is_functor.cf_Cone_ArrMap_vdomain

lemma (in is_functor) cf_Cocone_ArrMap_vdomain[cat_cs_simps]:
  assumes "𝒵 β" and "α ∈⇩∘ β" and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "𝒟⇩∘ (cf_Cocone α β 𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms(2) show ?thesis
    unfolding cf_Cocone_def'
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_simps] = is_functor.cf_Cocone_ArrMap_vdomain

lemma (in is_functor) cf_Cone_ArrMap_app[cat_cs_simps]:
  assumes "𝒵 β"
    and "α ∈⇩∘ β" 
    and "f : a ↦⇘𝔅⇙ b"
  shows "cf_Cone α β 𝔉⦇ArrMap⦈⦇f⦈ = cf_hom
    (cat_FUNCT α 𝔄 𝔅)
    [ntcf_arrow (ntcf_const 𝔄 𝔅 f), cat_FUNCT α 𝔄 𝔅⦇CId⦈⦇cf_map 𝔉⦈]⇩∘"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms(2,3) show ?thesis
    unfolding cf_Cone_def
    by
      (
        cs_concl 
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps 
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_simps] = is_functor.cf_Cone_ArrMap_app

lemma (in is_functor) cf_Cocone_ArrMap_app[cat_cs_simps]:
  assumes "𝒵 β"
    and "α ∈⇩∘ β" 
    and "f : a ↦⇘𝔅⇙ b"
  shows "cf_Cocone α β 𝔉⦇ArrMap⦈⦇f⦈ = cf_hom
    (cat_FUNCT α 𝔄 𝔅)
    [cat_FUNCT α 𝔄 𝔅⦇CId⦈⦇cf_map 𝔉⦈, ntcf_arrow (ntcf_const 𝔄 𝔅 f)]⇩∘"
proof-
  from assms interpret β: 𝒵 β by simp 
  from assms interpret Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
  from assms(2,3) show ?thesis
    unfolding cf_Cocone_def'
    by
      (
        cs_concl 
          cs_simp: cat_cs_simps cat_FUNCT_components(1) cat_op_simps 
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_op_intros
      )
qed

lemmas [cat_cs_simps] = is_functor.cf_Cocone_ArrMap_app


subsubsection‹The cone functor is a functor›

lemma (in is_functor) tm_cf_cf_Cone_is_functor_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "cf_Cone α β 𝔉 : op_cat 𝔅 ↦↦⇩C⇘β⇙ cat_Set β"
proof-
  from assms interpret FUNCT: category β ‹cat_FUNCT α 𝔄 𝔅›
    by
      (
        cs_concl cs_intro:
          cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  from assms interpret op_Δ: 
    is_functor β ‹op_cat 𝔅› ‹op_cat (cat_FUNCT α 𝔄 𝔅)› ‹op_cf (Δ⇩C⇩F α 𝔄 𝔅)›
    by (cs_concl cs_shallow cs_intro: 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_cs_intros cat_FUNCT_cs_intros
      )
  then show "cf_Cone α β 𝔉 : op_cat 𝔅 ↦↦⇩C⇘β⇙ cat_Set β"
    unfolding cf_Cone_def' by (cs_concl cs_intro: cat_cs_intros)
qed

lemma (in is_functor) tm_cf_cf_Cocone_is_functor_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "cf_Cocone α β 𝔉 : 𝔅 ↦↦⇩C⇘β⇙ cat_Set β"
proof-
  from assms interpret Funct: category β ‹cat_FUNCT α 𝔄 𝔅›
    by
      (
        cs_concl cs_intro:
          cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  from assms interpret op_Δ: is_functor β 𝔅 ‹cat_FUNCT α 𝔄 𝔅› ‹Δ⇩C⇩F α 𝔄 𝔅›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_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_cs_intros cat_FUNCT_cs_intros
      )
  then show "cf_Cocone α β  𝔉 : 𝔅 ↦↦⇩C⇘β⇙ cat_Set β"
    unfolding cf_Cocone_def' by (cs_concl cs_intro: cat_cs_intros)
qed

text‹\newpage›

end