Theory CZH_UCAT_Limit

(* Copyright 2021 (C) Mihails Milehins *)

section‹Limits and colimits›
theory CZH_UCAT_Limit
  imports 
    CZH_UCAT_Universal
    CZH_Elementary_Categories.CZH_ECAT_Cone
    CZH_Elementary_Categories.CZH_ECAT_Small_Cone
begin



subsection‹Background›

named_theorems cat_lim_cs_simps
named_theorems cat_lim_cs_intros



subsection‹Limit and colimit›


subsubsection‹Definition and elementary properties›


text‹
The concept of a limit is introduced in Chapter III-4 in
cite‹"mac_lane_categories_2010"›; the concept of a colimit is introduced in
Chapter III-3 in cite‹"mac_lane_categories_2010"›.
›

locale is_cat_limit = is_cat_cone α r 𝔍 ℭ 𝔉 u for α 𝔍 ℭ 𝔉 r u + 
  assumes cat_lim_ua_fo: "⋀u' r'. u' : r' <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ ⟹
    ∃!f'. f' : r' ↦⇘ℭ⇙ r ∧ u' = u ∙NTCF ntcf_const 𝔍 ℭ f'"

syntax "_is_cat_limit" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ <CF.lim _ :/ _ ↦↦Cı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_cat_limit" ⇌ is_cat_limit
translations "u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ" ⇌ 
  "CONST is_cat_limit α 𝔍 ℭ 𝔉 r u"

locale is_cat_colimit = is_cat_cocone α r 𝔍 ℭ 𝔉 u for α 𝔍 ℭ 𝔉 r u +
  assumes cat_colim_ua_of: "⋀u' r'. u' : 𝔉 >CF.cocone r' : 𝔍 ↦↦C⇘α⇙ ℭ ⟹
    ∃!f'. f' : r ↦⇘ℭ⇙ r' ∧ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"

syntax "_is_cat_colimit" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ >CF.colim _ :/ _ ↦↦Cı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_cat_colimit" ⇌ is_cat_colimit
translations "u : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ ℭ" ⇌
  "CONST is_cat_colimit α 𝔍 ℭ 𝔉 r u"


text‹Rules.›

lemma (in is_cat_limit) is_cat_limit_axioms'[cat_lim_cs_intros]:
  assumes "α' = α" and "r' = r" and "𝔍' = 𝔍" and "ℭ' = ℭ" and "𝔉' = 𝔉"
  shows "u : r' <CF.lim 𝔉' : 𝔍' ↦↦C⇘α'⇙ ℭ'"
  unfolding assms by (rule is_cat_limit_axioms)

mk_ide rf is_cat_limit_def[unfolded is_cat_limit_axioms_def]
  |intro is_cat_limitI|
  |dest is_cat_limitD[dest]|
  |elim is_cat_limitE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_limitD(1)

lemma (in is_cat_colimit) is_cat_colimit_axioms'[cat_lim_cs_intros]:
  assumes "α' = α" and "r' = r" and "𝔍' = 𝔍" and "ℭ' = ℭ" and "𝔉' = 𝔉"
  shows "u : 𝔉' >CF.colim r' : 𝔍' ↦↦C⇘α'⇙ ℭ'"
  unfolding assms by (rule is_cat_colimit_axioms)

mk_ide rf is_cat_colimit_def[unfolded is_cat_colimit_axioms_def]
  |intro is_cat_colimitI|
  |dest is_cat_colimitD[dest]|
  |elim is_cat_colimitE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_colimitD(1)


text‹Limits, colimits and universal arrows.›

lemma (in is_cat_limit) cat_lim_is_universal_arrow_fo:
  "universal_arrow_fo (ΔCF α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u)"
proof(intro is_functor.universal_arrow_foI)

  define β where "β = α + ω"
  have β: "𝒵 β" and αβ: "α ∈∘ β"
    by (simp_all add: β_def 𝒵_Limit_αω 𝒵_ω_αω 𝒵_def 𝒵_α_αω)
  then interpret β: 𝒵 β by simp 

  show "ΔCF α 𝔍 ℭ : ℭ ↦↦C⇘β⇙ cat_FUNCT α 𝔍 ℭ"
    by 
      (
        intro 
          β αβ
          cf_diagonal_is_functor 
          NTDom.HomDom.category_axioms 
          NTDom.HomCod.category_axioms
      )

  show "r ∈∘ ℭ⦇Obj⦈" by (intro cat_cone_obj)
  then show "ntcf_arrow u : ΔCF α 𝔍 ℭ⦇ObjMap⦈⦇r⦈ ↦⇘cat_FUNCT α 𝔍 ℭ⇙ cf_map 𝔉"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_FUNCT_cs_intros
      )

  fix r' u' assume prems: 
    "r' ∈∘ ℭ⦇Obj⦈" "u' : ΔCF α 𝔍 ℭ⦇ObjMap⦈⦇r'⦈ ↦⇘cat_FUNCT α 𝔍 ℭ⇙ cf_map 𝔉"
  from prems(1) have [cat_cs_simps]: 
    "cf_of_cf_map 𝔍 ℭ (cf_map 𝔉) = 𝔉"
    "cf_of_cf_map 𝔍 ℭ (cf_map (cf_const 𝔍 ℭ r')) = cf_const 𝔍 ℭ r'"
    by (cs_concl cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros)+
  from prems(2,1) have
    "u' : cf_map (cf_const 𝔍 ℭ r') ↦⇘cat_FUNCT α 𝔍 ℭ⇙ cf_map 𝔉"
    by (cs_prems cs_shallow cs_simp: cat_cs_simps)
  note u'[unfolded cat_cs_simps] = cat_FUNCT_is_arrD[OF this]

  from cat_lim_ua_fo[OF is_cat_coneI[OF u'(1) prems(1)]] obtain f 
    where f: "f : r' ↦⇘ℭ⇙ r"
      and [symmetric, cat_cs_simps]: 
        "ntcf_of_ntcf_arrow 𝔍 ℭ u' = u ∙NTCF ntcf_const 𝔍 ℭ f"
      and f_unique: 
        "⟦
          f' : r' ↦⇘ℭ⇙ r;
          ntcf_of_ntcf_arrow 𝔍 ℭ u' = u ∙NTCF ntcf_const 𝔍 ℭ f'
         ⟧ ⟹ f' = f"
    for f'
    by metis

  show "∃!f'.
    f' : r' ↦⇘ℭ⇙ r ∧
    u' = umap_fo (ΔCF α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f'⦈"
  proof(intro ex1I conjI; (elim conjE)?)
    show "f : r' ↦⇘ℭ⇙ r" by (rule f)
    with αβ cat_cone_obj show u'_def: 
      "u' = umap_fo (ΔCF α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f⦈"
      by 
        (
          cs_concl
            cs_simp: u'(2)[symmetric] cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    fix f' assume prems': 
      "f' : r' ↦⇘ℭ⇙ r"
      "u' = umap_fo (ΔCF α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f'⦈"
    from prems'(2) αβ f prems' cat_cone_obj have u'_def':
      "u' = ntcf_arrow (u ∙NTCF ntcf_const 𝔍 ℭ f')"
      by
        (
          cs_prems
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    from prems'(1) have "ntcf_of_ntcf_arrow 𝔍 ℭ u' = u ∙NTCF ntcf_const 𝔍 ℭ f'"
      by 
        (
          cs_concl 
            cs_simp: cat_FUNCT_cs_simps u'_def' cs_intro: cat_cs_intros
        )
    from f_unique[OF prems'(1) this] show "f' = f" .

  qed

qed

lemma (in is_cat_cone) cat_cone_is_cat_limit:
  assumes "universal_arrow_fo (ΔCF α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑)"
  shows "𝔑 : c <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
proof-

  define β where "β = α + ω"
  have β: "𝒵 β" and αβ: "α ∈∘ β"
    by (simp_all add: β_def 𝒵_Limit_αω 𝒵_ω_αω 𝒵_def 𝒵_α_αω)
  then interpret β: 𝒵 β by simp 

  show ?thesis
  proof(intro is_cat_limitI is_cat_cone_axioms)
    fix u' c' assume prems: "u' : c' <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"

    interpret u': is_cat_cone α c' 𝔍 ℭ 𝔉 u' by (rule prems)

    from u'.cat_cone_obj have u'_is_arr:
      "ntcf_arrow u' : ΔCF α 𝔍 ℭ⦇ObjMap⦈⦇c'⦈ ↦⇘cat_FUNCT α 𝔍 ℭ⇙ cf_map 𝔉"
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    
    from is_functor.universal_arrow_foD(3)
      [
        OF
          cf_diagonal_is_functor[
            OF β αβ NTDom.HomDom.category_axioms NTDom.HomCod.category_axioms
            ]
          assms
          u'.cat_cone_obj
          u'_is_arr
      ]
    obtain f where f: "f : c' ↦⇘ℭ⇙ c"
      and u'_def': "ntcf_arrow u' =
        umap_fo (ΔCF α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f⦈"
      and f'_unique:
        "⟦
          f' : c' ↦⇘ℭ⇙ c;
          ntcf_arrow u' =
            umap_fo (ΔCF α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f'⦈
         ⟧ ⟹ f' = f"
      for f'
      by metis

    from u'_def' αβ f cat_cone_obj have u'_def: 
      "u' = 𝔑 ∙NTCF ntcf_const 𝔍 ℭ f"
      by
        (
          cs_prems
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    
    show "∃!f'. f' : c' ↦⇘ℭ⇙ c ∧ u' = 𝔑 ∙NTCF ntcf_const 𝔍 ℭ f'"
    proof(intro ex1I conjI; (elim conjE)?, (rule f)?, (rule u'_def)?)
      fix f'' assume prems': 
        "f'' : c' ↦⇘ℭ⇙ c" "u' = 𝔑 ∙NTCF ntcf_const 𝔍 ℭ f''"
      from αβ prems' have 
        "ntcf_arrow u' = 
          umap_fo (ΔCF α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f''⦈"
        by
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
      from f'_unique[OF prems'(1) this] show "f'' = f".
    qed

  qed
  
qed

lemma (in is_cat_colimit) cat_colim_is_universal_arrow_of:
  "universal_arrow_of (ΔCF α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u)"
proof(intro is_functor.universal_arrow_ofI)

  define β where "β = α + ω"
  have β: "𝒵 β" and αβ: "α ∈∘ β"
    by (simp_all add: β_def 𝒵_Limit_αω 𝒵_ω_αω 𝒵_def 𝒵_α_αω)
  then interpret β: 𝒵 β by simp 

  show "ΔCF α 𝔍 ℭ : ℭ ↦↦C⇘β⇙ cat_FUNCT α 𝔍 ℭ"
    by 
      (
        intro 
          β αβ
          cf_diagonal_is_functor 
          NTDom.HomDom.category_axioms 
          NTDom.HomCod.category_axioms
      )

  show "r ∈∘ ℭ⦇Obj⦈" by (intro cat_cocone_obj)

  then show "ntcf_arrow u : cf_map 𝔉 ↦⇘cat_FUNCT α 𝔍 ℭ⇙ ΔCF α 𝔍 ℭ⦇ObjMap⦈⦇r⦈"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_FUNCT_cs_intros
      )

  fix r' u' assume prems: 
    "r' ∈∘ ℭ⦇Obj⦈" "u' : cf_map 𝔉 ↦⇘cat_FUNCT α 𝔍 ℭ⇙ ΔCF α 𝔍 ℭ⦇ObjMap⦈⦇r'⦈"
  from prems(1) have [cat_cs_simps]: 
    "cf_of_cf_map 𝔍 ℭ (cf_map 𝔉) = 𝔉"
    "cf_of_cf_map 𝔍 ℭ (cf_map (cf_const 𝔍 ℭ r')) = cf_const 𝔍 ℭ r'"
    by (cs_concl cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros)+
  from prems(2,1) have
    "u' : cf_map 𝔉 ↦⇘cat_FUNCT α 𝔍 ℭ⇙ cf_map (cf_const 𝔍 ℭ r')"
    by (cs_prems cs_shallow cs_simp: cat_cs_simps)
  note u'[unfolded cat_cs_simps] = cat_FUNCT_is_arrD[OF this]

  from cat_colim_ua_of[OF is_cat_coconeI[OF u'(1) prems(1)]] obtain f 
    where f: "f : r ↦⇘ℭ⇙ r'"
      and [symmetric, cat_cs_simps]: 
        "ntcf_of_ntcf_arrow 𝔍 ℭ u' = ntcf_const 𝔍 ℭ f ∙NTCF u"
      and f_unique: 
        "⟦
          f' : r ↦⇘ℭ⇙ r';
          ntcf_of_ntcf_arrow 𝔍 ℭ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u
         ⟧ ⟹ f' = f"
    for f'
    by metis

  show " ∃!f'. 
    f' : r ↦⇘ℭ⇙ r' ∧ 
    u' = umap_of (ΔCF α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f'⦈"
  proof(intro ex1I conjI; (elim conjE)?)
  
    show "f : r ↦⇘ℭ⇙ r'" by (rule f)
    with αβ cat_cocone_obj show u'_def: 
      "u' = umap_of (ΔCF α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f⦈"
      by 
        (
          cs_concl
            cs_simp: u'(2)[symmetric] cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
  
    fix f' assume prems':
      "f' : r ↦⇘ℭ⇙ r'"
      "u' = umap_of (ΔCF α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f'⦈"
    from prems'(2) αβ f prems' cat_cocone_obj have u'_def':
      "u' = ntcf_arrow (ntcf_const 𝔍 ℭ f' ∙NTCF u)"
      by
        (
          cs_prems
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    from prems'(1) have "ntcf_of_ntcf_arrow 𝔍 ℭ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_FUNCT_cs_simps u'_def' cs_intro: cat_cs_intros
        )
    from f_unique[OF prems'(1) this] show "f' = f" .

  qed

qed

lemma (in is_cat_cocone) cat_cocone_is_cat_colimit:
  assumes "universal_arrow_of (ΔCF α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑)"
  shows "𝔑 : 𝔉 >CF.colim c : 𝔍 ↦↦C⇘α⇙ ℭ"
proof-

  define β where "β = α + ω"
  have β: "𝒵 β" and αβ: "α ∈∘ β"
    by (simp_all add: β_def 𝒵_Limit_αω 𝒵_ω_αω 𝒵_def 𝒵_α_αω)
  then interpret β: 𝒵 β by simp 

  show ?thesis
  proof(intro is_cat_colimitI is_cat_cocone_axioms)
  
    fix u' c' assume prems: "u' : 𝔉 >CF.cocone c' : 𝔍 ↦↦C⇘α⇙ ℭ"

    interpret u': is_cat_cocone α c' 𝔍 ℭ 𝔉 u' by (rule prems)

    from u'.cat_cocone_obj have u'_is_arr:
      "ntcf_arrow u' : cf_map 𝔉 ↦⇘cat_FUNCT α 𝔍 ℭ⇙ ΔCF α 𝔍 ℭ⦇ObjMap⦈⦇c'⦈"
      by
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )

    from is_functor.universal_arrow_ofD(3)
      [
        OF
          cf_diagonal_is_functor[
            OF β αβ NTDom.HomDom.category_axioms NTDom.HomCod.category_axioms
            ]
          assms
          u'.cat_cocone_obj
          u'_is_arr
      ]
    obtain f where f: "f : c ↦⇘ℭ⇙ c'"
      and u'_def': "ntcf_arrow u' =
        umap_of (ΔCF α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f⦈"
      and f'_unique:
        "⟦
          f' : c ↦⇘ℭ⇙ c';
          ntcf_arrow u' =
            umap_of (ΔCF α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f'⦈
         ⟧ ⟹ f' = f"
      for f'
      by metis

    from u'_def' αβ f cat_cocone_obj have u'_def: 
      "u' = ntcf_const 𝔍 ℭ f ∙NTCF 𝔑"
      by
        (
          cs_prems
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
    
    show "∃!f'. f' : c ↦⇘ℭ⇙ c' ∧ u' = ntcf_const 𝔍 ℭ f' ∙NTCF 𝔑"
    proof(intro ex1I conjI; (elim conjE)?, (rule f)?, (rule u'_def)?)
      fix f'' assume prems': 
        "f'' : c ↦⇘ℭ⇙ c'" "u' = ntcf_const 𝔍 ℭ f'' ∙NTCF 𝔑"
      from αβ prems' have 
        "ntcf_arrow u' = 
          umap_of (ΔCF α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f''⦈"
        by
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_FUNCT_cs_simps
              cs_intro: cat_cs_intros cat_FUNCT_cs_intros
          )
      from f'_unique[OF prems'(1) this] show "f'' = f".
    qed

  qed
  
qed


text‹Duality.›

lemma (in is_cat_limit) is_cat_colimit_op:
  "op_ntcf u : op_cf 𝔉 >CF.colim r : op_cat 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
proof(intro is_cat_colimitI)
  show "op_ntcf u : op_cf 𝔉 >CF.cocone r : op_cat 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
    by (cs_concl cs_shallow cs_simp: cs_intro: cat_op_intros)
  fix u' r' assume prems: 
    "u' : op_cf 𝔉 >CF.cocone r' : op_cat 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
  interpret u': is_cat_cocone α r' ‹op_cat 𝔍› ‹op_cat ℭ› ‹op_cf 𝔉› u' 
    by (rule prems)
  from cat_lim_ua_fo[OF u'.is_cat_cone_op[unfolded cat_op_simps]] obtain f 
    where f: "f : r' ↦⇘ℭ⇙ r"
      and op_u'_def: "op_ntcf u' = u ∙NTCF ntcf_const 𝔍 ℭ f"
      and f_unique: 
        "⟦ f' : r' ↦⇘ℭ⇙ r; op_ntcf u' = u ∙NTCF ntcf_const 𝔍 ℭ f' ⟧ ⟹
          f' = f"
    for f'
    by metis
  from op_u'_def have "op_ntcf (op_ntcf u') = op_ntcf (u ∙NTCF ntcf_const 𝔍 ℭ f)"
    by simp
  from this f have u'_def: 
    "u' = ntcf_const (op_cat 𝔍) (op_cat ℭ) f ∙NTCF op_ntcf u"
    by (cs_prems cs_simp: cat_op_simps cs_intro: cat_cs_intros)
  show "∃!f'. 
    f' : r ↦⇘op_cat ℭ⇙ r' ∧ 
    u' = ntcf_const (op_cat 𝔍) (op_cat ℭ) f' ∙NTCF op_ntcf u"
  proof(intro ex1I conjI; (elim conjE)?, (unfold cat_op_simps)?)
    fix f' assume prems': 
      "f' : r' ↦⇘ℭ⇙ r"
      "u' = ntcf_const (op_cat 𝔍) (op_cat ℭ) f' ∙NTCF op_ntcf u"
    from prems'(2) have 
      "op_ntcf u' = op_ntcf (ntcf_const (op_cat 𝔍) (op_cat ℭ) f' ∙NTCF op_ntcf u)"
      by simp
    from this prems'(1) have "op_ntcf u' = u ∙NTCF ntcf_const 𝔍 ℭ f'"
      by 
        (
          cs_prems
            cs_simp: cat_cs_simps cat_op_simps 
            cs_intro: cat_cs_intros cat_op_intros
        )
    from f_unique[OF prems'(1) this] show "f' = f". 
  qed (intro u'_def f)+
qed

lemma (in is_cat_limit) is_cat_colimit_op'[cat_op_intros]:
  assumes "𝔉' = op_cf 𝔉" and "𝔍' = op_cat 𝔍" and "ℭ' = op_cat ℭ"
  shows "op_ntcf u : 𝔉' >CF.colim r : 𝔍' ↦↦C⇘α⇙ ℭ'"
  unfolding assms by (rule is_cat_colimit_op)

lemmas [cat_op_intros] = is_cat_limit.is_cat_colimit_op'

lemma (in is_cat_colimit) is_cat_limit_op:
  "op_ntcf u : r <CF.lim op_cf 𝔉 : op_cat 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
proof(intro is_cat_limitI)
  show "op_ntcf u : r <CF.cone op_cf 𝔉 : op_cat 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
    by (cs_concl cs_shallow cs_simp: cs_intro: cat_op_intros)
  fix u' r' assume prems: 
    "u' : r' <CF.cone op_cf 𝔉 : op_cat 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
  interpret u': is_cat_cone α r' ‹op_cat 𝔍› ‹op_cat ℭ› ‹op_cf 𝔉› u' 
    by (rule prems)
  from cat_colim_ua_of[OF u'.is_cat_cocone_op[unfolded cat_op_simps]] obtain f 
    where f: "f : r ↦⇘ℭ⇙ r'"
      and op_u'_def: "op_ntcf u' = ntcf_const 𝔍 ℭ f ∙NTCF u"
      and f_unique: 
        "⟦ f' : r ↦⇘ℭ⇙ r'; op_ntcf u' = ntcf_const 𝔍 ℭ f' ∙NTCF u ⟧ ⟹
          f' = f"
    for f'
    by metis
  from op_u'_def have "op_ntcf (op_ntcf u') = op_ntcf (ntcf_const 𝔍 ℭ f ∙NTCF u)"
    by simp
  from this f have u'_def: 
    "u' = op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f"
    by (cs_prems cs_simp: cat_op_simps cs_intro: cat_cs_intros)
  show "∃!f'. 
    f' : r' ↦⇘op_cat ℭ⇙ r ∧ 
    u' = op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f'"
  proof(intro ex1I conjI; (elim conjE)?, (unfold cat_op_simps)?)
    fix f' assume prems': 
      "f' : r ↦⇘ℭ⇙ r'"
      "u' = op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f'"
    from prems'(2) have 
      "op_ntcf u' = op_ntcf (op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f')"
      by simp
    from this prems'(1) have "op_ntcf u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"
      by
        (
          cs_prems
            cs_simp: cat_cs_simps cat_op_simps 
            cs_intro: cat_cs_intros cat_op_intros
        )
    from f_unique[OF prems'(1) this] show "f' = f". 
  qed (intro u'_def f)+
qed

lemma (in is_cat_colimit) is_cat_colimit_op'[cat_op_intros]:
  assumes "𝔉' = op_cf 𝔉" and "𝔍' = op_cat 𝔍" and "ℭ' = op_cat ℭ"
  shows "op_ntcf u : r <CF.lim 𝔉' : 𝔍' ↦↦C⇘α⇙ ℭ'"
  unfolding assms by (rule is_cat_limit_op)

lemmas [cat_op_intros] = is_cat_colimit.is_cat_colimit_op'


subsubsection‹Universal property›

lemma (in is_cat_limit) cat_lim_unique_cone':
  assumes "u' : r' <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  shows 
    "∃!f'. f' : r' ↦⇘ℭ⇙ r ∧ (∀j∈∘𝔍⦇Obj⦈. u'⦇NTMap⦈⦇j⦈ = u⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ f')"
  by (fold helper_cat_cone_Comp_ntcf_vcomp_iff[OF assms(1)])
    (intro cat_lim_ua_fo assms)

lemma (in is_cat_limit) cat_lim_unique:
  assumes "u' : r' <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  shows "∃!f'. f' : r' ↦⇘ℭ⇙ r ∧ u' = u ∙NTCF ntcf_const 𝔍 ℭ f'"
  by (intro cat_lim_ua_fo[OF is_cat_limitD(1)[OF assms]])

lemma (in is_cat_limit) cat_lim_unique':
  assumes "u' : r' <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  shows 
    "∃!f'. f' : r' ↦⇘ℭ⇙ r ∧ (∀j∈∘𝔍⦇Obj⦈. u'⦇NTMap⦈⦇j⦈ = u⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ f')"
  by (intro cat_lim_unique_cone'[OF is_cat_limitD(1)[OF assms]])

lemma (in is_cat_colimit) cat_colim_unique_cocone:
  assumes "u' : 𝔉 >CF.cocone r' : 𝔍 ↦↦C⇘α⇙ ℭ"
  shows "∃!f'. f' : r ↦⇘ℭ⇙ r' ∧ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"
proof-
  interpret u': is_cat_cocone α r' 𝔍 ℭ 𝔉 u' by (rule assms(1))
  from u'.cat_cocone_obj have op_r': "r' ∈∘ op_cat ℭ⦇Obj⦈"
    unfolding cat_op_simps by simp
  from 
    is_cat_limit.cat_lim_ua_fo[
      OF is_cat_limit_op u'.is_cat_cone_op, folded op_ntcf_ntcf_const
      ]
  obtain f' where f': "f' : r' ↦⇘op_cat ℭ⇙ r"
    and [cat_cs_simps]: 
      "op_ntcf u' = op_ntcf u ∙NTCF op_ntcf (ntcf_const 𝔍 ℭ f')"
    and unique: 
      "⟦
        f'' : r' ↦⇘op_cat ℭ⇙ r;
        op_ntcf u' = op_ntcf u ∙NTCF op_ntcf (ntcf_const 𝔍 ℭ f'')
       ⟧ ⟹ f'' = f'" 
    for f''
    by metis
  show ?thesis
  proof(intro ex1I conjI; (elim conjE)?)
    from f' show f': "f' : r ↦⇘ℭ⇙ r'" unfolding cat_op_simps by simp
    show "u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"
      by (rule eq_op_ntcf_iff[THEN iffD1], insert f')
        (cs_concl cs_intro: cat_cs_intros cs_simp: cat_cs_simps cat_op_simps)+
    fix f'' assume prems: "f'' : r ↦⇘ℭ⇙ r'" "u' = ntcf_const 𝔍 ℭ f'' ∙NTCF u"
    from prems(1) have "f'' : r' ↦⇘op_cat ℭ⇙ r" unfolding cat_op_simps by simp
    moreover from prems(1) have 
      "op_ntcf u' = op_ntcf u ∙NTCF op_ntcf (ntcf_const 𝔍 ℭ f'')"
      unfolding prems(2)
      by (cs_concl cs_intro: cat_cs_intros cs_simp: cat_cs_simps cat_op_simps)
    ultimately show "f'' = f'" by (rule unique)
  qed
qed

lemma (in is_cat_colimit) cat_colim_unique_cocone':
  assumes "u' : 𝔉 >CF.cocone r' : 𝔍 ↦↦C⇘α⇙ ℭ"
  shows 
    "∃!f'. f' : r ↦⇘ℭ⇙ r' ∧ (∀j∈∘𝔍⦇Obj⦈. u'⦇NTMap⦈⦇j⦈ = f' ∘A⇘ℭ⇙ u⦇NTMap⦈⦇j⦈)"
  by (fold helper_cat_cocone_Comp_ntcf_vcomp_iff[OF assms(1)])
    (intro cat_colim_unique_cocone assms)

lemma (in is_cat_colimit) cat_colim_unique:
  assumes "u' : 𝔉 >CF.colim r' : 𝔍 ↦↦C⇘α⇙ ℭ"
  shows "∃!f'. f' : r ↦⇘ℭ⇙ r' ∧ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"
  by (intro cat_colim_unique_cocone[OF is_cat_colimitD(1)[OF assms]])

lemma (in is_cat_colimit) cat_colim_unique':
  assumes "u' : 𝔉 >CF.colim r' : 𝔍 ↦↦C⇘α⇙ ℭ"
  shows
    "∃!f'. f' : r ↦⇘ℭ⇙ r' ∧ (∀j∈∘𝔍⦇Obj⦈. u'⦇NTMap⦈⦇j⦈ = f' ∘A⇘ℭ⇙ u⦇NTMap⦈⦇j⦈)"
proof-
  interpret u': is_cat_colimit α 𝔍 ℭ 𝔉 r' u' by (rule assms(1))
  show ?thesis
    by (fold helper_cat_cocone_Comp_ntcf_vcomp_iff[OF u'.is_cat_cocone_axioms])
      (intro cat_colim_unique assms)
qed

lemma cat_lim_ex_is_iso_arr:
  assumes "u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ" and "u' : r' <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  obtains f where "f : r' ↦iso⇘ℭ⇙ r" and "u' = u ∙NTCF ntcf_const 𝔍 ℭ f"
proof-
  interpret u: is_cat_limit α 𝔍 ℭ 𝔉 r u by (rule assms(1))
  interpret u': is_cat_limit α 𝔍 ℭ 𝔉 r' u' by (rule assms(2))
  define β where "β = α + ω"
  have β: "𝒵 β" and αβ: "α ∈∘ β"
    by (simp_all add: β_def u.𝒵_Limit_αω u.𝒵_ω_αω 𝒵_def u.𝒵_α_αω)
  then interpret β: 𝒵 β by simp 
  have Δ: "ΔCF α 𝔍 ℭ : ℭ ↦↦C⇘β⇙ cat_FUNCT α 𝔍 ℭ"
    by 
      (
        intro 
          β αβ
          cf_diagonal_is_functor 
          u.NTDom.HomDom.category_axioms 
          u.NTDom.HomCod.category_axioms
      )
  then interpret Δ: is_functor β ℭ ‹cat_FUNCT α 𝔍 ℭ› ‹ΔCF α 𝔍 ℭ› by simp
  from is_functor.cf_universal_arrow_fo_ex_is_iso_arr[
    OF Δ u.cat_lim_is_universal_arrow_fo u'.cat_lim_is_universal_arrow_fo
    ]
  obtain f where f: "f : r' ↦iso⇘ℭ⇙ r"
    and u': "ntcf_arrow u' =
    umap_fo (ΔCF α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f⦈"
    by auto
  from f have "f : r' ↦⇘ℭ⇙ r" by auto
  from u' this have "u' = u ∙NTCF ntcf_const 𝔍 ℭ f"
    by
      (
        cs_prems  
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros
      )
  with f that show ?thesis by simp
qed

lemma cat_lim_ex_is_iso_arr':
  assumes "u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ" and "u' : r' <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  obtains f where "f : r' ↦iso⇘ℭ⇙ r" 
    and "⋀j. j ∈∘ 𝔍⦇Obj⦈ ⟹ u'⦇NTMap⦈⦇j⦈ = u⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ f"
proof-
  interpret u: is_cat_limit α 𝔍 ℭ 𝔉 r u by (rule assms(1))
  interpret u': is_cat_limit α 𝔍 ℭ 𝔉 r' u' by (rule assms(2))
  from assms obtain f 
    where iso_f: "f : r' ↦iso⇘ℭ⇙ r" and u'_def: "u' = u ∙NTCF ntcf_const 𝔍 ℭ f"
    by (rule cat_lim_ex_is_iso_arr)
  then have f: "f : r' ↦⇘ℭ⇙ r" by auto
  then have "u'⦇NTMap⦈⦇j⦈ = u⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ f" if "j ∈∘ 𝔍⦇Obj⦈" for j
    by 
      (
        intro u.helper_cat_cone_ntcf_vcomp_Comp[
          OF u'.is_cat_cone_axioms f u'_def that
          ]
      )
  with iso_f that show ?thesis by simp
qed

lemma cat_colim_ex_is_iso_arr:
  assumes "u : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ ℭ" 
    and "u' : 𝔉 >CF.colim r' : 𝔍 ↦↦C⇘α⇙ ℭ"
  obtains f where "f : r ↦iso⇘ℭ⇙ r'" and "u' = ntcf_const 𝔍 ℭ f ∙NTCF u"
proof-
  interpret u: is_cat_colimit α 𝔍 ℭ 𝔉 r u by (rule assms(1))
  interpret u': is_cat_colimit α 𝔍 ℭ 𝔉 r' u' by (rule assms(2))
  obtain f where f: "f : r' ↦iso⇘op_cat ℭ⇙ r"
    and [cat_cs_simps]: 
      "op_ntcf u' = op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f"
    by 
      (
        elim cat_lim_ex_is_iso_arr[
          OF u.is_cat_limit_op u'.is_cat_limit_op
          ]
      )
  from f have iso_f: "f : r ↦iso⇘ℭ⇙ r'" unfolding cat_op_simps by simp
  then have f: "f : r ↦⇘ℭ⇙ r'" by auto
  have "u' = ntcf_const 𝔍 ℭ f ∙NTCF u"
    by (rule eq_op_ntcf_iff[THEN iffD1], insert f)
      (cs_concl cs_intro: cat_cs_intros cs_simp: cat_cs_simps cat_op_simps)+
  from iso_f this that show ?thesis by simp
qed

lemma cat_colim_ex_is_iso_arr':
  assumes "u : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ ℭ" 
    and "u' : 𝔉 >CF.colim r' : 𝔍 ↦↦C⇘α⇙ ℭ"
  obtains f where "f : r ↦iso⇘ℭ⇙ r'"
    and "⋀j. j ∈∘ 𝔍⦇Obj⦈ ⟹ u'⦇NTMap⦈⦇j⦈ = f ∘A⇘ℭ⇙ u⦇NTMap⦈⦇j⦈"
proof-
  interpret u: is_cat_colimit α 𝔍 ℭ 𝔉 r u by (rule assms(1))
  interpret u': is_cat_colimit α 𝔍 ℭ 𝔉 r' u' by (rule assms(2))
  from assms obtain f 
    where iso_f: "f : r ↦iso⇘ℭ⇙ r'" and u'_def: "u' = ntcf_const 𝔍 ℭ f ∙NTCF u"
    by (rule cat_colim_ex_is_iso_arr)
  then have f: "f : r ↦⇘ℭ⇙ r'" by auto
  then have "u'⦇NTMap⦈⦇j⦈ = f ∘A⇘ℭ⇙ u⦇NTMap⦈⦇j⦈" if "j ∈∘ 𝔍⦇Obj⦈" for j
    by 
      (
        intro u.helper_cat_cocone_ntcf_vcomp_Comp[
          OF u'.is_cat_cocone_axioms f u'_def that
          ]
      )
  with iso_f that show ?thesis by simp
qed


subsubsection‹Further properties›

lemma (in is_cat_limit) cat_lim_is_cat_limit_if_is_iso_arr:
  assumes "f : r' ↦iso⇘ℭ⇙ r"
  shows "u ∙NTCF ntcf_const 𝔍 ℭ f : r' <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
proof-
  note f = is_iso_arrD(1)[OF assms(1)]
  from f(1) interpret u': is_cat_cone α r' 𝔍 ℭ 𝔉 ‹u ∙NTCF ntcf_const 𝔍 ℭ f› 
    by (cs_concl cs_intro: cat_lim_cs_intros cat_cs_intros)
  define β where "β = α + ω"
  have β: "𝒵 β" and αβ: "α ∈∘ β"
    by (simp_all add: β_def 𝒵_Limit_αω 𝒵_ω_αω 𝒵_def 𝒵_α_αω)
  then interpret β: 𝒵 β by simp 
  show ?thesis
  proof
    (
      intro u'.cat_cone_is_cat_limit, 
      rule is_functor.universal_arrow_fo_if_universal_arrow_fo,
      rule cf_diagonal_is_functor[OF β αβ],
      rule NTDom.HomDom.category_axioms,
      rule NTDom.HomCod.category_axioms,
      rule cat_lim_is_universal_arrow_fo
    )
    show "f : r' ↦iso⇘ℭ⇙ r" by (rule assms(1))
    from αβ f show
      "ntcf_arrow (u ∙NTCF ntcf_const 𝔍 ℭ f) =
        umap_fo (ΔCF α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
  qed
qed

lemma (in is_cat_colimit) cat_colim_is_cat_colimit_if_is_iso_arr:
  assumes "f : r ↦iso⇘ℭ⇙ r'" 
  shows "ntcf_const 𝔍 ℭ f ∙NTCF u : 𝔉 >CF.colim r' : 𝔍 ↦↦C⇘α⇙ ℭ"
proof-
  note f = is_iso_arrD[OF assms(1)]
  from f(1) interpret u': is_cat_cocone α r' 𝔍 ℭ 𝔉 ‹ntcf_const 𝔍 ℭ f ∙NTCF u› 
    by (cs_concl cs_intro: cat_lim_cs_intros cat_cs_intros)
  from f have [symmetric, cat_op_simps]:
    "op_ntcf (ntcf_const 𝔍 ℭ f ∙NTCF u) =
      op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f"
    by
      (
        cs_concl cs_shallow 
          cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros
      )
  show ?thesis
    by 
      (
        rule is_cat_limit.is_cat_colimit_op
          [
            OF is_cat_limit.cat_lim_is_cat_limit_if_is_iso_arr[
              OF is_cat_limit_op, unfolded cat_op_simps, OF assms(1)
              ],
            unfolded cat_op_simps
          ]
      )
qed

lemma ntcf_cf_comp_is_cat_limit_if_is_iso_functor:
  assumes "u : r <CF.lim 𝔉 : 𝔅 ↦↦C⇘α⇙ ℭ" and "𝔊 : 𝔄 ↦↦C.iso⇘α⇙ 𝔅"
  shows "u ∘NTCF-CF 𝔊 : r <CF.lim 𝔉 ∘CF 𝔊 : 𝔄 ↦↦C⇘α⇙ ℭ"
proof(intro is_cat_limitI)
  interpret u: is_cat_limit α 𝔅 ℭ 𝔉 r u by (rule assms(1)) 
  interpret 𝔊: is_iso_functor α 𝔄 𝔅 𝔊 by (rule assms(2))
  note [cf_cs_simps] = is_iso_functor_is_iso_arr(2,3)
  show u𝔊: "u ∘NTCF-CF 𝔊 : r <CF.cone 𝔉 ∘CF 𝔊 : 𝔄 ↦↦C⇘α⇙ ℭ"
    by (intro is_cat_coneI)
      (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  fix u' r' assume prems: "u' : r' <CF.cone 𝔉 ∘CF 𝔊 : 𝔄 ↦↦C⇘α⇙ ℭ"
  then interpret u': is_cat_cone α r' 𝔄 ℭ ‹𝔉 ∘CF 𝔊› u' by simp
  have "u' ∘NTCF-CF inv_cf 𝔊 : r' <CF.cone 𝔉 : 𝔅 ↦↦C⇘α⇙ ℭ"
    by (intro is_cat_coneI)
      (
        cs_concl
          cs_simp: cat_cs_simps cf_cs_simps
          cs_intro: cat_cs_intros cf_cs_intros
      )
  from is_cat_limit.cat_lim_ua_fo[OF assms(1) this] obtain f 
    where f: "f : r' ↦⇘ℭ⇙ r"
      and u'_𝔊: "u' ∘NTCF-CF inv_cf 𝔊 = u ∙NTCF ntcf_const 𝔅 ℭ f"
      and f'f:
        "⟦
          f' : r' ↦⇘ℭ⇙ r; 
          u' ∘NTCF-CF inv_cf 𝔊 = u ∙NTCF ntcf_const 𝔅 ℭ f' 
         ⟧ ⟹ f' = f"
    for f'
    by metis
  from u'_𝔊 have u'_inv𝔊_𝔊:
    "(u' ∘NTCF-CF inv_cf 𝔊) ∘NTCF-CF 𝔊 = (u ∙NTCF ntcf_const 𝔅 ℭ f) ∘NTCF-CF 𝔊"
    by simp
  show "∃!f'. f' : r' ↦⇘ℭ⇙ r ∧ u' = u ∘NTCF-CF 𝔊 ∙NTCF ntcf_const 𝔄 ℭ f'"
  proof(intro ex1I conjI; (elim conjE)?)
    show "f : r' ↦⇘ℭ⇙ r" by (rule f)
    from u'_inv𝔊_𝔊 f show "u' = u ∘NTCF-CF 𝔊 ∙NTCF ntcf_const 𝔄 ℭ f"
      by
        (
          cs_prems 
            cs_simp:
              cf_cs_simps cat_cs_simps
              ntcf_cf_comp_ntcf_cf_comp_assoc 
              ntcf_vcomp_ntcf_cf_comp[symmetric]
            cs_intro: cat_cs_intros cf_cs_intros
        )
    fix f' assume prems:
      "f' : r' ↦⇘ℭ⇙ r" "u' = u ∘NTCF-CF 𝔊 ∙NTCF ntcf_const 𝔄 ℭ f'"
    from prems(2) have 
      "u' ∘NTCF-CF inv_cf 𝔊 = 
        (u ∘NTCF-CF 𝔊 ∙NTCF ntcf_const 𝔄 ℭ f') ∘NTCF-CF inv_cf 𝔊"
      by simp
    from this f prems(1) have "u' ∘NTCF-CF inv_cf 𝔊 = u ∙NTCF ntcf_const 𝔅 ℭ f'"
      by
        (
          cs_prems 
            cs_simp:
              cat_cs_simps cf_cs_simps
              ntcf_vcomp_ntcf_cf_comp[symmetric]
              ntcf_cf_comp_ntcf_cf_comp_assoc
            cs_intro: cf_cs_intros cat_cs_intros
        )
    then show "f' = f" by (intro f'f prems(1))
  qed
qed

lemma ntcf_cf_comp_is_cat_limit_if_is_iso_functor'[cat_lim_cs_intros]:
  assumes "u : r <CF.lim 𝔉 : 𝔅 ↦↦C⇘α⇙ ℭ" 
    and "𝔊 : 𝔄 ↦↦C.iso⇘α⇙ 𝔅"
    and "𝔄' = 𝔉 ∘CF 𝔊"
  shows "u ∘NTCF-CF 𝔊 : r <CF.lim 𝔄' : 𝔄 ↦↦C⇘α⇙ ℭ"
  using assms(1,2) 
  unfolding assms(3)
  by (rule ntcf_cf_comp_is_cat_limit_if_is_iso_functor)



subsection‹Small limit and small colimit›


subsubsection‹Definition and elementary properties›


text‹
The concept of a limit is introduced in Chapter III-4 in
cite‹"mac_lane_categories_2010"›; the concept of a colimit is introduced in
Chapter III-3 in cite‹"mac_lane_categories_2010"›. The definitions of small
limits were tailored for ZFC in HOL.
›

locale is_tm_cat_limit = is_tm_cat_cone α r 𝔍 ℭ 𝔉 u for α 𝔍 ℭ 𝔉 r u + 
  assumes tm_cat_lim_ua_fo: 
    "⋀u' r'. u' : r' <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ ⟹
      ∃!f'. f' : r' ↦⇘ℭ⇙ r ∧ u' = u ∙NTCF ntcf_const 𝔍 ℭ f'"

syntax "_is_tm_cat_limit" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ <CF.tm.lim _ :/ _ ↦↦C.tmı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_tm_cat_limit" ⇌ is_tm_cat_limit
translations "u : r <CF.tm.lim 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ" ⇌ 
  "CONST is_tm_cat_limit α 𝔍 ℭ 𝔉 r u"

locale is_tm_cat_colimit = is_tm_cat_cocone α r 𝔍 ℭ 𝔉 u for α 𝔍 ℭ 𝔉 r u +
  assumes tm_cat_colim_ua_of: 
    "⋀u' r'. u' : 𝔉 >CF.cocone r' : 𝔍 ↦↦C⇘α⇙ ℭ ⟹
      ∃!f'. f' : r ↦⇘ℭ⇙ r' ∧ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"

syntax "_is_tm_cat_colimit" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ >CF.tm.colim _ :/ _ ↦↦C.tmı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_tm_cat_colimit" ⇌ is_tm_cat_colimit
translations "u : 𝔉 >CF.tm.colim r : 𝔍 ↦↦C.tm⇘α⇙ ℭ" ⇌ 
  "CONST is_tm_cat_colimit α 𝔍 ℭ 𝔉 r u"


text‹Rules.›

lemma (in is_tm_cat_limit) is_tm_cat_limit_axioms'[cat_lim_cs_intros]:
  assumes "α' = α" and "r' = r" and "𝔍' = 𝔍" and "ℭ' = ℭ" and "𝔉' = 𝔉"
  shows "u : r' <CF.tm.lim 𝔉' : 𝔍' ↦↦C.tm⇘α'⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_limit_axioms)

mk_ide rf is_tm_cat_limit_def[unfolded is_tm_cat_limit_axioms_def]
  |intro is_tm_cat_limitI|
  |dest is_tm_cat_limitD[dest]|
  |elim is_tm_cat_limitE[elim]|

lemmas [cat_lim_cs_intros] = is_tm_cat_limitD(1)

lemma (in is_tm_cat_colimit) is_tm_cat_colimit_axioms'[cat_lim_cs_intros]:
  assumes "α' = α" and "r' = r" and "𝔍' = 𝔍" and "ℭ' = ℭ" and "𝔉' = 𝔉"
  shows "u : 𝔉' >CF.tm.colim r' : 𝔍' ↦↦C.tm⇘α'⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_colimit_axioms)

mk_ide rf is_tm_cat_colimit_def[unfolded is_tm_cat_colimit_axioms_def]
  |intro is_tm_cat_colimitI|
  |dest is_tm_cat_colimitD[dest]|
  |elim is_tm_cat_colimitE[elim]|

lemmas [cat_lim_cs_intros] = is_tm_cat_colimitD(1)

lemma is_tm_cat_limitI':
  assumes "u : r <CF.tm.cone 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
    and "⋀u' r'. u' : r' <CF.tm.cone 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ ⟹
      ∃!f'. f' : r' ↦⇘ℭ⇙ r ∧ u' = u ∙NTCF ntcf_const 𝔍 ℭ f'"
  shows "u : r <CF.tm.lim 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
proof(rule is_tm_cat_limitI, rule assms(1))
  interpret is_tm_cat_cone α r 𝔍 ℭ 𝔉 u by (rule assms(1))  
  fix r' u' assume prems: "u' : r' <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  then interpret u': is_cat_cone α r' 𝔍 ℭ 𝔉 u' . 
  have "u' : r' <CF.tm.cone 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
    by
      (
        intro
          is_tm_cat_coneI 
          NTCod.is_tm_functor_axioms
          u'.cat_cone_obj 
          u'.is_ntcf_axioms
      )
  then show "∃!f'. f' : r' ↦⇘ℭ⇙ r ∧ u' = u ∙NTCF ntcf_const 𝔍 ℭ f'"
    by (rule assms(2))
qed

lemma is_tm_cat_colimitI':
  assumes "u : 𝔉 >CF.tm.cocone r : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
    and "⋀u' r'. u' : 𝔉 >CF.tm.cocone r' : 𝔍 ↦↦C.tm⇘α⇙ ℭ ⟹
      ∃!f'. f' : r ↦⇘ℭ⇙ r' ∧ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"
  shows "u : 𝔉 >CF.tm.colim r : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
proof(intro is_tm_cat_colimitI, rule assms(1))
  interpret is_tm_cat_cocone α r 𝔍 ℭ 𝔉 u by (rule assms(1))
  fix r' u' assume prems: "u' : 𝔉 >CF.cocone r' : 𝔍 ↦↦C⇘α⇙ ℭ"
  then interpret u': is_cat_cocone α r' 𝔍 ℭ 𝔉 u' . 
  have "u' : 𝔉 >CF.tm.cocone r' : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
    by
      (
        intro
          is_tm_cat_coconeI 
          NTDom.is_tm_functor_axioms
          u'.cat_cocone_obj 
          u'.is_ntcf_axioms
      )
  then show "∃!f'. f' : r ↦⇘ℭ⇙ r' ∧ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"
    by (rule assms(2))
qed


text‹Elementary properties.›

sublocale is_tm_cat_limit ⊆ is_cat_limit
  by (intro is_cat_limitI, rule is_cat_cone_axioms, rule tm_cat_lim_ua_fo)

sublocale is_tm_cat_colimit ⊆ is_cat_colimit
  by (intro is_cat_colimitI, rule is_cat_cocone_axioms, rule tm_cat_colim_ua_of)

lemma (in is_cat_limit) cat_lim_is_tm_cat_limit:
  assumes "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
  shows "u : r <CF.tm.lim 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ" 
proof(intro is_tm_cat_limitI)
  interpret 𝔉: is_tm_functor α 𝔍 ℭ 𝔉 by (rule assms) 
  show "u : r <CF.tm.cone 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
    by (intro is_tm_cat_coneI assms is_ntcf_axioms cat_cone_obj)
  fix u' r' assume prems: "u' : r' <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  show "∃!f'. f' : r' ↦⇘ℭ⇙ r ∧ u' = u ∙NTCF ntcf_const 𝔍 ℭ f'"
    by (rule cat_lim_ua_fo[OF prems])
qed

lemma (in is_cat_colimit) cat_colim_is_tm_cat_colimit:
  assumes "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
  shows "u : 𝔉 >CF.tm.colim r : 𝔍 ↦↦C.tm⇘α⇙ ℭ" 
proof(intro is_tm_cat_colimitI)
  interpret 𝔉: is_tm_functor α 𝔍 ℭ 𝔉 by (rule assms) 
  show "u : 𝔉 >CF.tm.cocone r : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
    by (intro is_tm_cat_coconeI assms is_ntcf_axioms cat_cocone_obj)
  fix u' r' assume prems: "u' : 𝔉 >CF.cocone r' : 𝔍 ↦↦C⇘α⇙ ℭ"
  show "∃!f'. f' : r ↦⇘ℭ⇙ r' ∧ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"
    by (rule cat_colim_ua_of[OF prems])
qed


text‹Limits, colimits and universal arrows.›

lemma (in is_tm_cat_limit) tm_cat_lim_is_universal_arrow_fo:
  "universal_arrow_fo (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u)"
proof(intro is_functor.universal_arrow_foI)

  show "ΔCF.tm α 𝔍 ℭ : ℭ ↦↦C⇘α⇙ cat_Funct α 𝔍 ℭ"
    by 
      (
        intro 
          tm_cf_diagonal_is_functor 
          NTCod.HomDom.tiny_category_axioms
          NTDom.HomCod.category_axioms
      )

  show "r ∈∘ ℭ⦇Obj⦈" by (intro cat_cone_obj)
  then show "ntcf_arrow u : ΔCF.tm α 𝔍 ℭ⦇ObjMap⦈⦇r⦈ ↦⇘cat_Funct α 𝔍 ℭ⇙ cf_map 𝔉"
    by 
      (
        cs_concl
          cs_simp: cat_cs_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )

  fix r' u' assume prems: 
    "r' ∈∘ ℭ⦇Obj⦈" "u' : ΔCF.tm α 𝔍 ℭ⦇ObjMap⦈⦇r'⦈ ↦⇘cat_Funct α 𝔍 ℭ⇙ cf_map 𝔉"
  from prems(1) have [cat_cs_simps]: 
    "cf_of_cf_map 𝔍 ℭ (cf_map 𝔉) = 𝔉"
    "cf_of_cf_map 𝔍 ℭ (cf_map (cf_const 𝔍 ℭ r')) = cf_const 𝔍 ℭ r'"
    by (cs_concl cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros)+
  from prems(2,1) have 
    "u' : cf_map (cf_const 𝔍 ℭ r') ↦⇘cat_Funct α 𝔍 ℭ⇙ cf_map 𝔉"
    by (cs_prems cs_shallow cs_simp: cat_cs_simps)
  note u'[unfolded cat_cs_simps] = cat_Funct_is_arrD[OF this]

  from 
    tm_cat_lim_ua_fo[
      OF is_cat_coneI[OF is_tm_ntcfD(1)[OF u'(1)] prems(1)]
      ] 
  obtain f 
    where f: "f : r' ↦⇘ℭ⇙ r"
      and [symmetric, cat_cs_simps]: 
        "ntcf_of_ntcf_arrow 𝔍 ℭ u' = u ∙NTCF ntcf_const 𝔍 ℭ f"
      and f_unique: 
        "⟦
          f' : r' ↦⇘ℭ⇙ r;
          ntcf_of_ntcf_arrow 𝔍 ℭ u' = u ∙NTCF ntcf_const 𝔍 ℭ f'
         ⟧ ⟹ f' = f"
    for f'
    by metis

  show "∃!f'.
    f' : r' ↦⇘ℭ⇙ r ∧
    u' = umap_fo (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f'⦈"
  proof(intro ex1I conjI; (elim conjE)?)
    show "f : r' ↦⇘ℭ⇙ r" by (rule f)
    with cat_cone_obj show u'_def: 
      "u' = umap_fo (ΔCF.tm  α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f⦈"
      by 
        (
          cs_concl 
            cs_simp: u'(2)[symmetric] cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    fix f' assume prems': 
      "f' : r' ↦⇘ℭ⇙ r"
      "u' = umap_fo (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f'⦈"
    from prems'(2) f prems' cat_cone_obj have u'_def':
      "u' = ntcf_arrow (u ∙NTCF ntcf_const 𝔍 ℭ f')"
      by
        (
          cs_prems
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from prems'(1) have "ntcf_of_ntcf_arrow 𝔍 ℭ u' = u ∙NTCF ntcf_const 𝔍 ℭ f'"
      by (cs_concl cs_simp: cat_FUNCT_cs_simps u'_def' cs_intro: cat_cs_intros)
    from f_unique[OF prems'(1) this] show "f' = f" .

  qed

qed

lemma (in is_tm_cat_cone) tm_cat_cone_is_tm_cat_limit:
  assumes "universal_arrow_fo (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑)"
  shows "𝔑 : c <CF.tm.lim 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
proof(intro is_tm_cat_limitI' is_tm_cat_cone_axioms)

  fix u' c' assume prems: "u' : c' <CF.tm.cone 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"

  interpret u': is_tm_cat_cone α c' 𝔍 ℭ 𝔉 u' by (rule prems)

  from u'.tm_cat_cone_obj have u'_is_arr:
    "ntcf_arrow u' : ΔCF.tm α 𝔍 ℭ⦇ObjMap⦈⦇c'⦈ ↦⇘cat_Funct α 𝔍 ℭ⇙ cf_map 𝔉"
    by
      (
        cs_concl
          cs_simp: cat_cs_simps
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )

  from is_functor.universal_arrow_foD(3)
    [
      OF
        tm_cf_diagonal_is_functor[
          OF NTCod.HomDom.tiny_category_axioms NTDom.HomCod.category_axioms
          ]
        assms
        u'.cat_cone_obj
        u'_is_arr
    ]
  obtain f where f: "f : c' ↦⇘ℭ⇙ c"
    and u'_def': "ntcf_arrow u' =
      umap_fo (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f⦈"
    and f'_unique:
      "⟦
        f' : c' ↦⇘ℭ⇙ c;
        ntcf_arrow u' =
          umap_fo (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f'⦈
       ⟧ ⟹ f' = f"
    for f'
    by metis

  from u'_def' f cat_cone_obj have u'_def: "u' = 𝔑 ∙NTCF ntcf_const 𝔍 ℭ f"
    by
      (
        cs_prems 
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )

  show "∃!f'. f' : c' ↦⇘ℭ⇙ c ∧ u' = 𝔑 ∙NTCF ntcf_const 𝔍 ℭ f'"
  proof(intro ex1I conjI; (elim conjE)?, (rule f)?, (rule u'_def)?)
    fix f'' assume prems': 
      "f'' : c' ↦⇘ℭ⇙ c" "u' = 𝔑 ∙NTCF ntcf_const 𝔍 ℭ f''"
    from prems' have 
      "ntcf_arrow u' =
        umap_fo (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f''⦈"
      by
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from f'_unique[OF prems'(1) this] show "f'' = f".
  qed

qed

lemma (in is_tm_cat_colimit) tm_cat_colim_is_universal_arrow_of:
  "universal_arrow_of (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u)"
proof(intro is_functor.universal_arrow_ofI)

  show "ΔCF.tm α 𝔍 ℭ : ℭ ↦↦C⇘α⇙ cat_Funct α 𝔍 ℭ"
    by 
      (
        intro 
          tm_cf_diagonal_is_functor 
          NTDom.HomDom.tiny_category_axioms 
          NTDom.HomCod.category_axioms
      )

  show "r ∈∘ ℭ⦇Obj⦈" by (intro cat_cocone_obj)

  then show "ntcf_arrow u : cf_map 𝔉 ↦⇘cat_Funct α 𝔍 ℭ⇙ ΔCF.tm α 𝔍 ℭ⦇ObjMap⦈⦇r⦈"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )

  fix r' u' assume prems: 
    "r' ∈∘ ℭ⦇Obj⦈" "u' : cf_map 𝔉 ↦⇘cat_Funct α 𝔍 ℭ⇙ ΔCF.tm α 𝔍 ℭ⦇ObjMap⦈⦇r'⦈"
  from prems(1) have [cat_cs_simps]: 
    "cf_of_cf_map 𝔍 ℭ (cf_map 𝔉) = 𝔉"
    "cf_of_cf_map 𝔍 ℭ (cf_map (cf_const 𝔍 ℭ r')) = cf_const 𝔍 ℭ r'"
    by (cs_concl cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros)+
  from prems(2,1) have
    "u' : cf_map 𝔉 ↦⇘cat_Funct α 𝔍 ℭ⇙ cf_map (cf_const 𝔍 ℭ r')"
    by (cs_prems cs_shallow cs_simp: cat_cs_simps)
  note u'[unfolded cat_cs_simps] = cat_Funct_is_arrD[OF this]

  from cat_colim_ua_of[OF is_cat_coconeI[OF is_tm_ntcfD(1)[OF u'(1)] prems(1)]]
  obtain f 
    where f: "f : r ↦⇘ℭ⇙ r'"
      and [symmetric, cat_cs_simps]: 
        "ntcf_of_ntcf_arrow 𝔍 ℭ u' = ntcf_const 𝔍 ℭ f ∙NTCF u"
      and f_unique:
        "⟦
          f' : r ↦⇘ℭ⇙ r';
          ntcf_of_ntcf_arrow 𝔍 ℭ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u
         ⟧ ⟹ f' = f"
    for f'
    by metis

  show " ∃!f'.
    f' : r ↦⇘ℭ⇙ r' ∧
    u' = umap_of (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f'⦈"
  proof(intro ex1I conjI; (elim conjE)?)
  
    show "f : r ↦⇘ℭ⇙ r'" by (rule f)

    with cat_cocone_obj show u'_def:
      "u' = umap_of (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f⦈"
      by 
        (
          cs_concl
            cs_simp: u'(2)[symmetric] cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
  
    fix f' assume prems':
      "f' : r ↦⇘ℭ⇙ r'"
      "u' = umap_of (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f'⦈"
    from prems'(2) f prems' cat_cocone_obj have u'_def':
      "u' = ntcf_arrow (ntcf_const 𝔍 ℭ f' ∙NTCF u)"
      by
        (
          cs_prems
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from prems'(1) have "ntcf_of_ntcf_arrow 𝔍 ℭ u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_FUNCT_cs_simps u'_def' cs_intro: cat_cs_intros
        )
    from f_unique[OF prems'(1) this] show "f' = f" .

  qed

qed

lemma (in is_tm_cat_cocone) tm_cat_cocone_is_tm_cat_colimit:
  assumes "universal_arrow_of (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑)"
  shows "𝔑 : 𝔉 >CF.tm.colim c : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
proof(intro is_tm_cat_colimitI' is_tm_cat_cocone_axioms)
  
  fix u' c' assume prems: "u' : 𝔉 >CF.tm.cocone c' : 𝔍 ↦↦C.tm⇘α⇙ ℭ"

  interpret u': is_tm_cat_cocone α c' 𝔍 ℭ 𝔉 u' by (rule prems)

  from u'.tm_cat_cocone_obj have u'_is_arr:
    "ntcf_arrow u' : cf_map 𝔉 ↦⇘cat_Funct α 𝔍 ℭ⇙ ΔCF.tm α 𝔍 ℭ⦇ObjMap⦈⦇c'⦈"
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )

  from is_functor.universal_arrow_ofD(3)
    [
      OF
        tm_cf_diagonal_is_functor[
          OF NTDom.HomDom.tiny_category_axioms NTDom.HomCod.category_axioms
          ]
        assms
        u'.cat_cocone_obj
        u'_is_arr
    ]
  obtain f where f: "f : c ↦⇘ℭ⇙ c'"
    and u'_def': "ntcf_arrow u' =
      umap_of (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f⦈"
    and f'_unique:
      "⟦
        f' : c ↦⇘ℭ⇙ c';
        ntcf_arrow u' =
          umap_of (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f'⦈
       ⟧ ⟹ f' = f"
    for f'
    by metis

  from u'_def' f cat_cocone_obj have u'_def: "u' = ntcf_const 𝔍 ℭ f ∙NTCF 𝔑"
    by
      (
        cs_prems
          cs_simp: cat_cs_simps cat_FUNCT_cs_simps
          cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
      )
  
  show "∃!f'. f' : c ↦⇘ℭ⇙ c' ∧ u' = ntcf_const 𝔍 ℭ f' ∙NTCF 𝔑"
  proof(intro ex1I conjI; (elim conjE)?, (rule f)?, (rule u'_def)?)
    fix f'' assume prems': 
      "f'' : c ↦⇘ℭ⇙ c'" "u' = ntcf_const 𝔍 ℭ f'' ∙NTCF 𝔑"
    from prems' have 
      "ntcf_arrow u' =
        umap_of (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) c (ntcf_arrow 𝔑) c'⦇ArrVal⦈⦇f''⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
    from f'_unique[OF prems'(1) this] show "f'' = f".
  qed

qed
  

text‹Duality.›

lemma (in is_tm_cat_limit) is_tm_cat_colimit_op:
  "op_ntcf u : op_cf 𝔉 >CF.tm.colim r : op_cat 𝔍 ↦↦C.tm⇘α⇙ op_cat ℭ"
proof(intro is_tm_cat_colimitI')
  show "op_ntcf u : op_cf 𝔉 >CF.tm.cocone r : op_cat 𝔍 ↦↦C.tm⇘α⇙ op_cat ℭ"
    by (cs_concl cs_shallow cs_simp: cs_intro: cat_op_intros)
  fix u' r' assume prems: 
    "u' : op_cf 𝔉 >CF.tm.cocone r' : op_cat 𝔍 ↦↦C.tm⇘α⇙ op_cat ℭ"
  interpret u': is_tm_cat_cocone α r' ‹op_cat 𝔍› ‹op_cat ℭ› ‹op_cf 𝔉› u' 
    by (rule prems)
  from tm_cat_lim_ua_fo[OF u'.is_cat_cone_op[unfolded cat_op_simps]] obtain f 
    where f: "f : r' ↦⇘ℭ⇙ r"
      and op_u'_def: "op_ntcf u' = u ∙NTCF ntcf_const 𝔍 ℭ f"
      and f_unique: 
        "⟦ f' : r' ↦⇘ℭ⇙ r; op_ntcf u' = u ∙NTCF ntcf_const 𝔍 ℭ f' ⟧ ⟹
          f' = f"
    for f'
    by metis
  from op_u'_def have "op_ntcf (op_ntcf u') = op_ntcf (u ∙NTCF ntcf_const 𝔍 ℭ f)"
    by simp
  from this f have u'_def: 
    "u' = ntcf_const (op_cat 𝔍) (op_cat ℭ) f ∙NTCF op_ntcf u"
    by (cs_prems cs_simp: cat_op_simps cs_intro: cat_cs_intros)
  show "∃!f'. 
    f' : r ↦⇘op_cat ℭ⇙ r' ∧ 
    u' = ntcf_const (op_cat 𝔍) (op_cat ℭ) f' ∙NTCF op_ntcf u"
  proof(intro ex1I conjI; (elim conjE)?, (unfold cat_op_simps)?)
    fix f' assume prems': 
      "f' : r' ↦⇘ℭ⇙ r"
      "u' = ntcf_const (op_cat 𝔍) (op_cat ℭ) f' ∙NTCF op_ntcf u"
    from prems'(2) have "op_ntcf u' =
      op_ntcf (ntcf_const (op_cat 𝔍) (op_cat ℭ) f' ∙NTCF op_ntcf u)"
      by simp
    from this prems'(1) have "op_ntcf u' = u ∙NTCF ntcf_const 𝔍 ℭ f'"
      by
        (
          cs_prems
            cs_simp: cat_cs_simps cat_op_simps 
            cs_intro: cat_cs_intros cat_op_intros
        )
    from f_unique[OF prems'(1) this] show "f' = f". 
  qed (intro u'_def f)+
qed

lemma (in is_tm_cat_limit) is_tm_cat_colimit_op'[cat_op_intros]:
  assumes "𝔉' = op_cf 𝔉" and "𝔍' = op_cat 𝔍" and "ℭ' = op_cat ℭ"
  shows "op_ntcf u : 𝔉' >CF.tm.colim r : 𝔍' ↦↦C.tm⇘α⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_colimit_op)

lemmas [cat_op_intros] = is_tm_cat_limit.is_tm_cat_colimit_op'

lemma (in is_tm_cat_colimit) is_tm_cat_limit_op:
  "op_ntcf u : r <CF.tm.lim op_cf 𝔉 : op_cat 𝔍 ↦↦C.tm⇘α⇙ op_cat ℭ"
proof(intro is_tm_cat_limitI')
  show "op_ntcf u : r <CF.tm.cone op_cf 𝔉 : op_cat 𝔍 ↦↦C.tm⇘α⇙ op_cat ℭ"
    by (cs_concl cs_shallow cs_simp: cs_intro: cat_op_intros)
  fix u' r' assume prems: 
    "u' : r' <CF.tm.cone op_cf 𝔉 : op_cat 𝔍 ↦↦C.tm⇘α⇙ op_cat ℭ"
  interpret u': is_tm_cat_cone α r' ‹op_cat 𝔍› ‹op_cat ℭ› ‹op_cf 𝔉› u' 
    by (rule prems)
  from tm_cat_colim_ua_of[OF u'.is_cat_cocone_op[unfolded cat_op_simps]] obtain f 
    where f: "f : r ↦⇘ℭ⇙ r'"
      and op_u'_def: "op_ntcf u' = ntcf_const 𝔍 ℭ f ∙NTCF u"
      and f_unique: 
        "⟦ f' : r ↦⇘ℭ⇙ r'; op_ntcf u' = ntcf_const 𝔍 ℭ f' ∙NTCF u ⟧ ⟹ f' = f"
    for f'
    by metis
  from op_u'_def have "op_ntcf (op_ntcf u') = op_ntcf (ntcf_const 𝔍 ℭ f ∙NTCF u)"
    by simp
  from this f have u'_def: 
    "u' = op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f"
    by (cs_prems cs_simp: cat_op_simps cs_intro: cat_cs_intros)
  show "∃!f'. 
    f' : r' ↦⇘op_cat ℭ⇙ r ∧ 
    u' = op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f'"
  proof(intro ex1I conjI; (elim conjE)?, (unfold cat_op_simps)?)
    fix f' assume prems': 
      "f' : r ↦⇘ℭ⇙ r'"
      "u' = op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f'"
    from prems'(2) have "op_ntcf u' =
      op_ntcf (op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f')"
      by simp
    from this prems'(1) have "op_ntcf u' = ntcf_const 𝔍 ℭ f' ∙NTCF u"
      by
        (
          cs_prems
            cs_simp: cat_cs_simps cat_op_simps 
            cs_intro: cat_cs_intros cat_op_intros
        )
    from f_unique[OF prems'(1) this] show "f' = f". 
  qed (intro u'_def f)+
qed

lemma (in is_tm_cat_colimit) is_tm_cat_colimit_op'[cat_op_intros]:
  assumes "𝔉' = op_cf 𝔉" and "𝔍' = op_cat 𝔍" and "ℭ' = op_cat ℭ"
  shows "op_ntcf u : r <CF.tm.lim 𝔉' : 𝔍' ↦↦C.tm⇘α⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_limit_op)

lemmas [cat_op_intros] = is_tm_cat_colimit.is_tm_cat_colimit_op'


subsubsection‹Further properties›

lemma (in is_tm_cat_limit) tm_cat_lim_is_tm_cat_limit_if_iso_arr:
  assumes "f : r' ↦iso⇘ℭ⇙ r"
  shows "u ∙NTCF ntcf_const 𝔍 ℭ f : r' <CF.tm.lim 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
proof-
  note f = is_iso_arrD(1)[OF assms]
  from f(1) interpret u': is_tm_cat_cone α r' 𝔍 ℭ 𝔉 ‹u ∙NTCF ntcf_const 𝔍 ℭ f› 
    by (cs_concl cs_intro: cat_small_cs_intros cat_cs_intros)
  show ?thesis
  proof
    (
      intro u'.tm_cat_cone_is_tm_cat_limit,
      rule is_functor.universal_arrow_fo_if_universal_arrow_fo,
      rule tm_cf_diagonal_is_functor,
      rule NTCod.HomDom.tiny_category_axioms,
      rule NTDom.HomCod.category_axioms,
      rule tm_cat_lim_is_universal_arrow_fo
    )
    show "f : r' ↦iso⇘ℭ⇙ r" by (rule assms)
    from f show "ntcf_arrow (u ∙NTCF ntcf_const 𝔍 ℭ f) =
      umap_fo (ΔCF.tm α 𝔍 ℭ) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrVal⦈⦇f⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
        )
  qed
qed

lemma (in is_tm_cat_colimit) tm_cat_colim_is_tm_cat_colimit_if_iso_arr:
  assumes "f : r ↦iso⇘ℭ⇙ r'"
  shows "ntcf_const 𝔍 ℭ f ∙NTCF u : 𝔉 >CF.tm.colim r' : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
proof-
  note f = is_iso_arrD(1)[OF assms]
  from f(1) interpret u': 
    is_tm_cat_cocone α r' 𝔍 ℭ 𝔉 ‹ntcf_const 𝔍 ℭ f ∙NTCF u› 
    by (cs_concl cs_intro: cat_small_cs_intros cat_cs_intros)
  from f have [symmetric, cat_op_simps]:
    "op_ntcf (ntcf_const 𝔍 ℭ f ∙NTCF u) =
      op_ntcf u ∙NTCF ntcf_const (op_cat 𝔍) (op_cat ℭ) f"
    by
      (
        cs_concl cs_shallow 
          cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros
      )
  show ?thesis
    by 
      (
        rule is_tm_cat_limit.is_tm_cat_colimit_op
          [
            OF is_tm_cat_limit.tm_cat_lim_is_tm_cat_limit_if_iso_arr[
              OF is_tm_cat_limit_op, unfolded cat_op_simps, OF assms(1)
              ],
            unfolded cat_op_simps
          ]
      )
qed



subsection‹Finite limit and finite colimit›

locale is_cat_finite_limit = 
  is_cat_limit α 𝔍 ℭ 𝔉 r u + NTDom.HomDom: finite_category α 𝔍
  for α 𝔍 ℭ 𝔉 r u

syntax "_is_cat_finite_limit" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ <CF.lim.fin _ :/ _ ↦↦Cı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_cat_finite_limit" ⇌ is_cat_finite_limit
translations "u : r <CF.lim.fin 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ" ⇌ 
  "CONST is_cat_finite_limit α 𝔍 ℭ 𝔉 r u"

locale is_cat_finite_colimit = 
  is_cat_colimit α 𝔍 ℭ 𝔉 r u + NTDom.HomDom: finite_category α 𝔍
  for α 𝔍 ℭ 𝔉 r u

syntax "_is_cat_finite_colimit" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ >CF.colim.fin _ :/ _ ↦↦Cı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_cat_finite_colimit" ⇌ is_cat_finite_colimit
translations "u : 𝔉 >CF.colim.fin r : 𝔍 ↦↦C⇘α⇙ ℭ" ⇌ 
  "CONST is_cat_finite_colimit α 𝔍 ℭ 𝔉 r u"


text‹Rules.›

lemma (in is_cat_finite_limit) is_cat_finite_limit_axioms'[cat_lim_cs_intros]:
  assumes "α' = α" and "r' = r" and "𝔍' = 𝔍" and "ℭ' = ℭ" and "𝔉' = 𝔉"
  shows "u : r' <CF.lim.fin 𝔉' : 𝔍' ↦↦C⇘α'⇙ ℭ'"
  unfolding assms by (rule is_cat_finite_limit_axioms)

mk_ide rf is_cat_finite_limit_def
  |intro is_cat_finite_limitI|
  |dest is_cat_finite_limitD[dest]|
  |elim is_cat_finite_limitE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_finite_limitD

lemma (in is_cat_finite_colimit) 
  is_cat_finite_colimit_axioms'[cat_lim_cs_intros]:
  assumes "α' = α" and "r' = r" and "𝔍' = 𝔍" and "ℭ' = ℭ" and "𝔉' = 𝔉"
  shows "u : 𝔉' >CF.colim.fin r' : 𝔍' ↦↦C⇘α'⇙ ℭ'"
  unfolding assms by (rule is_cat_finite_colimit_axioms)

mk_ide rf is_cat_finite_colimit_def[unfolded is_cat_colimit_axioms_def]
  |intro is_cat_finite_colimitI|
  |dest is_cat_finite_colimitD[dest]|
  |elim is_cat_finite_colimitE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_finite_colimitD


text‹Duality.›

lemma (in is_cat_finite_limit) is_cat_finite_colimit_op:
  "op_ntcf u : op_cf 𝔉 >CF.colim.fin r : op_cat 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
  by
    (
      cs_concl cs_shallow
        cs_intro: is_cat_finite_colimitI cat_op_intros cat_small_cs_intros
    )

lemma (in is_cat_finite_limit) is_cat_finite_colimit_op'[cat_op_intros]:
  assumes "𝔉' = op_cf 𝔉" and "𝔍' = op_cat 𝔍" and "ℭ' = op_cat ℭ"
  shows "op_ntcf u : 𝔉' >CF.colim.fin r : 𝔍' ↦↦C⇘α⇙ ℭ'"
  unfolding assms by (rule is_cat_finite_colimit_op)

lemmas [cat_op_intros] = is_cat_finite_limit.is_cat_finite_colimit_op'

lemma (in is_cat_finite_colimit) is_cat_finite_limit_op:
  "op_ntcf u : r <CF.lim.fin op_cf 𝔉 : op_cat 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
  by 
    (
      cs_concl cs_shallow 
        cs_intro: is_cat_finite_limitI cat_op_intros cat_small_cs_intros
    )

lemma (in is_cat_finite_colimit) is_cat_finite_colimit_op'[cat_op_intros]:
  assumes "𝔉' = op_cf 𝔉" and "𝔍' = op_cat 𝔍" and "ℭ' = op_cat ℭ"
  shows "op_ntcf u : r <CF.lim.fin 𝔉' : 𝔍' ↦↦C⇘α⇙ ℭ'"
  unfolding assms by (rule is_cat_finite_limit_op)

lemmas [cat_op_intros] = is_cat_finite_colimit.is_cat_finite_colimit_op'


text‹Elementary properties.›

sublocale is_cat_finite_limit ⊆ is_tm_cat_limit
  by
    (
      intro 
        is_tm_cat_limitI 
        is_tm_cat_coneI 
        is_ntcf_axioms 
        cat_lim_ua_fo 
        cat_cone_obj 
        NTCod.cf_is_tm_functor_if_HomDom_finite_category[
          OF NTDom.HomDom.finite_category_axioms
          ]
    )

sublocale is_cat_finite_colimit ⊆ is_tm_cat_colimit
  by
    (
      intro 
        is_tm_cat_colimitI 
        is_tm_cat_coconeI 
        is_ntcf_axioms 
        cat_colim_ua_of 
        cat_cocone_obj 
        NTDom.cf_is_tm_functor_if_HomDom_finite_category[
          OF NTDom.HomDom.finite_category_axioms
          ]
    )



subsection‹Creation of limits›


text‹See Chapter V-1 in cite‹"mac_lane_categories_2010"›.›

definition cf_creates_limits :: "V ⇒ V ⇒ V ⇒ bool"
  where "cf_creates_limits α 𝔊 𝔉 =
    (
      ∀τ b.
        τ : b <CF.lim 𝔊 ∘CF 𝔉 : 𝔉⦇HomDom⦈ ↦↦C⇘α⇙ 𝔊⦇HomCod⦈ ⟶
        (
          (
            ∃!σa. ∃σ a. σa = ⟨σ, a⟩ ∧
              σ : a <CF.cone 𝔉 : 𝔉⦇HomDom⦈ ↦↦C⇘α⇙ 𝔉⦇HomCod⦈ ∧
              τ = 𝔊 ∘CF-NTCF σ ∧
              b = 𝔊⦇ObjMap⦈⦇a⦈
          ) ∧
          (
            ∀σ a.
              σ : a <CF.cone 𝔉 : 𝔉⦇HomDom⦈ ↦↦C⇘α⇙ 𝔉⦇HomCod⦈ ⟶
              τ = 𝔊 ∘CF-NTCF σ ⟶
              b = 𝔊⦇ObjMap⦈⦇a⦈ ⟶
              σ : a <CF.lim 𝔉 : 𝔉⦇HomDom⦈ ↦↦C⇘α⇙ 𝔉⦇HomCod⦈
          )
        )
    )"


text‹Rules.›

context
  fixes α 𝔍 𝔄 𝔅 𝔊 𝔉
  assumes 𝔉: "𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    and 𝔊: "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
begin

interpretation 𝔉: is_functor α 𝔍 𝔄 𝔉 by (rule 𝔉)
interpretation 𝔊: is_functor α 𝔄 𝔅 𝔊 by (rule 𝔊)

mk_ide rf cf_creates_limits_def[
  where α=α and 𝔉=𝔉 and 𝔊=𝔊, unfolded cat_cs_simps
  ]
  |intro cf_creates_limitsI|
  |dest cf_creates_limitsD'|
  |elim cf_creates_limitsE'|

end

lemmas cf_creates_limitsD[dest!] = cf_creates_limitsD'[rotated 2]
  and cf_creates_limitsE[elim!] = cf_creates_limitsE'[rotated 2]

lemma cf_creates_limitsE'':
  assumes "cf_creates_limits α 𝔊 𝔉"
    and "τ : b <CF.lim 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔅"
    and "𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    and "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
  obtains σ r where "σ : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    and "τ = 𝔊 ∘CF-NTCF σ"
    and "b = 𝔊⦇ObjMap⦈⦇r⦈"
proof-
  note cflD = cf_creates_limitsD[OF assms]
  from conjunct1[OF cflD] obtain σ r
    where σ: "σ : r <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
      and τ_def: "τ = 𝔊 ∘CF-NTCF σ"
      and b_def: "b = 𝔊⦇ObjMap⦈⦇r⦈"
    by metis
  moreover have "σ : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    by (rule conjunct2[OF cflD, rule_format, OF σ τ_def b_def])
  ultimately show ?thesis using that by auto
qed



subsection‹Preservation of limits and colimits›


subsubsection‹Definitions and elementary properties›


text‹See Chapter V-4 in cite‹"mac_lane_categories_2010"›.›

definition cf_preserves_limits :: "V ⇒ V ⇒ V ⇒ bool"
  where "cf_preserves_limits α 𝔊 𝔉 =
    (
      ∀σ a.
        σ : a <CF.lim 𝔉 : 𝔉⦇HomDom⦈ ↦↦C⇘α⇙ 𝔉⦇HomCod⦈ ⟶
        𝔊 ∘CF-NTCF σ : 𝔊⦇ObjMap⦈⦇a⦈ <CF.lim 𝔊 ∘CF 𝔉 : 𝔉⦇HomDom⦈ ↦↦C⇘α⇙ 𝔊⦇HomCod⦈
    )"

definition cf_preserves_colimits :: "V ⇒ V ⇒ V ⇒ bool"
  where "cf_preserves_colimits α 𝔊 𝔉 =
    (
      ∀σ a.
        σ : 𝔉 >CF.colim a : 𝔉⦇HomDom⦈ ↦↦C⇘α⇙ 𝔉⦇HomCod⦈ ⟶
        𝔊 ∘CF-NTCF σ : 𝔊 ∘CF 𝔉 >CF.colim 𝔊⦇ObjMap⦈⦇a⦈ : 𝔉⦇HomDom⦈ ↦↦C⇘α⇙ 𝔊⦇HomCod⦈
    )"


text‹Rules.›

context
  fixes α 𝔍 𝔄 𝔅 𝔊 𝔉
  assumes 𝔉: "𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    and 𝔊: "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
begin

interpretation 𝔉: is_functor α 𝔍 𝔄 𝔉 by (rule 𝔉)
interpretation 𝔊: is_functor α 𝔄 𝔅 𝔊 by (rule 𝔊)

mk_ide rf cf_preserves_limits_def[
  where α=α and 𝔉=𝔉 and 𝔊=𝔊, unfolded cat_cs_simps
  ]
  |intro cf_preserves_limitsI|
  |dest cf_preserves_limitsD'|
  |elim cf_preserves_limitsE'|

mk_ide rf cf_preserves_colimits_def[
  where α=α and 𝔉=𝔉 and 𝔊=𝔊, unfolded cat_cs_simps
  ]
  |intro cf_preserves_colimitsI|
  |dest cf_preserves_colimitsD'|
  |elim cf_preserves_colimitsE'|

end

lemmas cf_preserves_limitsD[dest!] = cf_preserves_limitsD'[rotated 2]
  and cf_preserves_limitsE[elim!] = cf_preserves_limitsE'[rotated 2]

lemmas cf_preserves_colimitsD[dest!] = cf_preserves_colimitsD'[rotated 2]
  and cf_preserves_colimitsE[elim!] = cf_preserves_colimitsE'[rotated 2]


text‹Duality.›

lemma cf_preserves_colimits_op[cat_op_simps]:
  assumes "𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄" and "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
  shows 
    "cf_preserves_colimits α (op_cf 𝔊) (op_cf 𝔉) ⟷
      cf_preserves_limits α 𝔊 𝔉"
proof

  interpret 𝔉: is_functor α 𝔍 𝔄 𝔉 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔄 𝔅 𝔊 by (rule assms(2))

  show "cf_preserves_limits α 𝔊 𝔉"
    if "cf_preserves_colimits α (op_cf 𝔊) (op_cf 𝔉)"
  proof(rule cf_preserves_limitsI, rule assms(1), rule assms(2))
    fix σ r assume "σ : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    then interpret σ: is_cat_limit α 𝔍 𝔄 𝔉 r σ .
    show "𝔊 ∘CF-NTCF σ : 𝔊⦇ObjMap⦈⦇r⦈ <CF.lim 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔅"
      by 
        (
          rule is_cat_colimit.is_cat_limit_op
            [
              OF cf_preserves_colimitsD
                [
                  OF that σ.is_cat_colimit_op 𝔉.is_functor_op 𝔊.is_functor_op,
                  folded op_cf_cf_comp op_ntcf_cf_ntcf_comp
                ],
              unfolded cat_op_simps
            ]
        )
  qed

  show "cf_preserves_colimits α (op_cf 𝔊) (op_cf 𝔉)"
    if "cf_preserves_limits α 𝔊 𝔉"
  proof
    (
      rule cf_preserves_colimitsI, 
      rule 𝔉.is_functor_op, 
      rule 𝔊.is_functor_op, 
      unfold cat_op_simps
    )
    fix σ r assume "σ : op_cf 𝔉 >CF.colim r : op_cat 𝔍 ↦↦C⇘α⇙ op_cat 𝔄"
    then interpret σ: is_cat_colimit α ‹op_cat 𝔍› ‹op_cat 𝔄› ‹op_cf 𝔉› r σ . 
    show "op_cf 𝔊 ∘CF-NTCF σ :
      op_cf 𝔊 ∘CF op_cf 𝔉 >CF.colim 𝔊⦇ObjMap⦈⦇r⦈ : op_cat 𝔍 ↦↦C⇘α⇙ op_cat 𝔅"
      by 
        (
          rule is_cat_limit.is_cat_colimit_op
            [
              OF cf_preserves_limitsD[
                OF that σ.is_cat_limit_op[unfolded cat_op_simps] assms(1,2)
                ],
              unfolded cat_op_simps
            ]
        )
  qed

qed

lemma cf_preserves_limits_op[cat_op_simps]:
  assumes "𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄" and "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
  shows 
    "cf_preserves_limits α (op_cf 𝔊) (op_cf 𝔉) ⟷
      cf_preserves_colimits α 𝔊 𝔉"
proof

  interpret 𝔉: is_functor α 𝔍 𝔄 𝔉 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔄 𝔅 𝔊 by (rule assms(2))

  show "cf_preserves_colimits α 𝔊 𝔉" 
    if "cf_preserves_limits α (op_cf 𝔊) (op_cf 𝔉)"
  proof(rule cf_preserves_colimitsI, rule assms(1), rule assms(2))
    fix σ r assume "σ : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ 𝔄" 
    then interpret σ: is_cat_colimit α 𝔍 𝔄 𝔉 r σ .
    show "𝔊 ∘CF-NTCF σ : 𝔊 ∘CF 𝔉 >CF.colim 𝔊⦇ObjMap⦈⦇r⦈ : 𝔍 ↦↦C⇘α⇙ 𝔅"
      by 
        (
          rule is_cat_limit.is_cat_colimit_op
            [
              OF cf_preserves_limitsD
                [
                  OF that σ.is_cat_limit_op 𝔉.is_functor_op 𝔊.is_functor_op,
                  folded op_cf_cf_comp op_ntcf_cf_ntcf_comp
                ],
              unfolded cat_op_simps
            ]
        )
  qed

  show "cf_preserves_limits α (op_cf 𝔊) (op_cf 𝔉)"
    if "cf_preserves_colimits α 𝔊 𝔉"
  proof
    (
      rule cf_preserves_limitsI, 
      rule 𝔉.is_functor_op, 
      rule 𝔊.is_functor_op, 
      unfold cat_op_simps
    )
    fix σ r assume "σ : r <CF.lim op_cf 𝔉 : op_cat 𝔍 ↦↦C⇘α⇙ op_cat 𝔄"
    then interpret σ: is_cat_limit α ‹op_cat 𝔍› ‹op_cat 𝔄› ‹op_cf 𝔉› r σ . 
    show "op_cf 𝔊 ∘CF-NTCF σ :
      𝔊⦇ObjMap⦈⦇r⦈ <CF.lim op_cf 𝔊 ∘CF op_cf 𝔉 : op_cat 𝔍 ↦↦C⇘α⇙ op_cat 𝔅"
      by 
        (
          rule is_cat_colimit.is_cat_limit_op
            [
              OF cf_preserves_colimitsD[
                OF that σ.is_cat_colimit_op[unfolded cat_op_simps] assms(1,2)
                ],
              unfolded cat_op_simps
            ]
        )
  qed
  
qed


subsubsection‹Further properties›

lemma cf_preserves_limits_if_cf_creates_limits:
  ―‹See Theorem 2 in Chapter V-4 in \cite{mac_lane_categories_2010}.›
  assumes "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
    and "𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    and "ψ : b <CF.lim 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔅"
    and "cf_creates_limits α 𝔊 𝔉"
  shows "cf_preserves_limits α 𝔊 𝔉"
proof-

  interpret 𝔊: is_functor α 𝔄 𝔅 𝔊 by (rule assms(1))
  interpret 𝔉: is_functor α 𝔍 𝔄 𝔉 by (rule assms(2))
  interpret ψ: is_cat_limit α 𝔍 𝔅 ‹𝔊 ∘CF 𝔉› b ψ
    by (intro is_cat_limit.cat_lim_is_tm_cat_limit assms(3,4))

  show ?thesis
  proof
    (
      intro cf_preserves_limitsI,
      rule 𝔉.is_functor_axioms,
      rule 𝔊.is_functor_axioms
    )

    fix σ a assume prems: "σ : a <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    then interpret σ: is_cat_limit α 𝔍 𝔄 𝔉 a σ .

    obtain τ A
      where τ: "τ : A <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
        and ψ_def: "ψ = 𝔊 ∘CF-NTCF τ"
        and b_def: "b = 𝔊⦇ObjMap⦈⦇A⦈"
      by 
        (
          rule cf_creates_limitsE''
            [
              OF 
                assms(4)  
                ψ.is_cat_limit_axioms
                𝔉.is_functor_axioms
                𝔊.is_functor_axioms
            ]  
        )
    from τ interpret τ: is_cat_limit α 𝔍 𝔄 𝔉 A τ .

    from cat_lim_ex_is_iso_arr[OF τ.is_cat_limit_axioms prems] obtain f
      where f: "f : a ↦iso⇘𝔄⇙ A" and σ_def: "σ = τ ∙NTCF ntcf_const 𝔍 𝔄 f"
      by auto

    note f = f is_iso_arrD(1)[OF f]

    from f(2) have "𝔊 ∘CF-NTCF σ : 𝔊⦇ObjMap⦈⦇a⦈ <CF.cone 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔅"
      by (intro is_cat_coneI)
        (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

    from σ_def have "𝔊 ∘CF-NTCF σ = 𝔊 ∘CF-NTCF (τ ∙NTCF ntcf_const 𝔍 𝔄 f)" 
      by simp
    also from f(2) have "… = ψ ∙NTCF ntcf_const 𝔍 𝔅 (𝔊⦇ArrMap⦈⦇f⦈)"
      by (cs_concl_step cf_ntcf_comp_ntcf_vcomp)
        (
          cs_concl
            cs_simp: cat_cs_simps ψ_def[symmetric] cs_intro: cat_cs_intros
        )
    finally have 𝔊σ: "𝔊 ∘CF-NTCF σ = ψ ∙NTCF ntcf_const 𝔍 𝔅 (𝔊⦇ArrMap⦈⦇f⦈)" .

    show "𝔊 ∘CF-NTCF σ : 𝔊⦇ObjMap⦈⦇a⦈ <CF.lim 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔅"
      by 
        (
          rule ψ.cat_lim_is_cat_limit_if_is_iso_arr
            [
              OF 𝔊.cf_ArrMap_is_iso_arr[OF f(1), folded b_def], 
              folded 𝔊σ
            ]
        )
    
  qed
  
qed



subsection‹Continuous and cocontinuous functor›


subsubsection‹Definition and elementary properties›

definition is_cf_continuous :: "V ⇒ V ⇒ bool"
  where "is_cf_continuous α 𝔊 ⟷
    (∀𝔉 𝔍. 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔊⦇HomDom⦈ ⟶ cf_preserves_limits α 𝔊 𝔉)"

definition is_cf_cocontinuous :: "V ⇒ V ⇒ bool"
  where "is_cf_cocontinuous α 𝔊 ⟷
    (∀𝔉 𝔍. 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔊⦇HomDom⦈ ⟶ cf_preserves_colimits α 𝔊 𝔉)"


text‹Rules.›

context
  fixes α 𝔍 𝔄 𝔅 𝔊 𝔉
  assumes 𝔊: "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
begin

interpretation 𝔊: is_functor α 𝔄 𝔅 𝔊 by (rule 𝔊)

mk_ide rf is_cf_continuous_def[where α=α and 𝔊=𝔊, unfolded cat_cs_simps]
  |intro is_cf_continuousI|
  |dest is_cf_continuousD'|
  |elim is_cf_continuousE'|

mk_ide rf is_cf_cocontinuous_def[where α=α and 𝔊=𝔊, unfolded cat_cs_simps]
  |intro is_cf_cocontinuousI|
  |dest is_cf_cocontinuousD'|
  |elim is_cf_cocontinuousE'|

end

lemmas is_cf_continuousD[dest!] = is_cf_continuousD'[rotated]
  and is_cf_continuousE[elim!] = is_cf_continuousE'[rotated]

lemmas is_cf_cocontinuousD[dest!] = is_cf_cocontinuousD'[rotated]
  and is_cf_cocontinuousE[elim!] = is_cf_cocontinuousE'[rotated]


text‹Duality.›

lemma is_cf_continuous_op[cat_op_simps]:
  assumes "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
  shows "is_cf_continuous α (op_cf 𝔊) ⟷ is_cf_cocontinuous α 𝔊"
proof
  interpret 𝔊: is_functor α 𝔄 𝔅 𝔊 by (rule assms(1))
  show "is_cf_cocontinuous α 𝔊" if "is_cf_continuous α (op_cf 𝔊)"
  proof(intro is_cf_cocontinuousI, rule assms)
    fix 𝔉 𝔍 assume prems': "𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    then interpret 𝔉: is_functor α 𝔍 𝔄 𝔉 .
    show "cf_preserves_colimits α 𝔊 𝔉"
      by 
        (
          rule cf_preserves_limits_op
            [
              THEN iffD1, 
              OF
                prems' 
                assms(1) 
                is_cf_continuousD[OF that 𝔉.is_functor_op 𝔊.is_functor_op] 
            ]
        )
  qed
  show "is_cf_continuous α (op_cf 𝔊)" if "is_cf_cocontinuous α 𝔊"
  proof(intro is_cf_continuousI, rule 𝔊.is_functor_op)
    fix 𝔉 𝔍 assume prems': "𝔉 : 𝔍 ↦↦C⇘α⇙ op_cat 𝔄"
    then interpret 𝔉: is_functor α 𝔍 ‹op_cat 𝔄› 𝔉 .
    from that assms have op_op_bundle:
      "is_cf_cocontinuous α (op_cf (op_cf 𝔊))"
      "op_cf (op_cf 𝔊) : 𝔄 ↦↦C⇘α⇙ 𝔅"
      unfolding cat_op_simps .
    show "cf_preserves_limits α (op_cf 𝔊) 𝔉"
      by 
        (
          rule cf_preserves_colimits_op
            [
              THEN iffD1, 
              OF
                𝔉.is_functor_axioms 
                𝔊.is_functor_op 
                is_cf_cocontinuousD
                  [
                    OF
                      op_op_bundle(1) 
                      𝔉.is_functor_op[unfolded cat_op_simps] 
                      op_op_bundle(2)
                  ]
            ]
        )
  qed
qed

lemma is_cf_cocontinuous_op[cat_op_simps]:
  assumes "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
  shows "is_cf_cocontinuous α (op_cf 𝔊) ⟷ is_cf_continuous α 𝔊"
proof
  interpret 𝔊: is_functor α 𝔄 𝔅 𝔊 by (rule assms(1))
  show "is_cf_continuous α 𝔊" if "is_cf_cocontinuous α (op_cf 𝔊)"
  proof(intro is_cf_continuousI, rule assms)
    fix 𝔉 𝔍 assume prems': "𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    then interpret 𝔉: is_functor α 𝔍 𝔄 𝔉 .
    show "cf_preserves_limits α 𝔊 𝔉"
      by 
        (
          rule cf_preserves_colimits_op
            [
              THEN iffD1, 
              OF
                prems' 
                assms(1) 
                is_cf_cocontinuousD[OF that 𝔉.is_functor_op 𝔊.is_functor_op] 
            ]
        )
  qed
  show "is_cf_cocontinuous α (op_cf 𝔊)" if "is_cf_continuous α 𝔊"
  proof(intro is_cf_cocontinuousI, rule 𝔊.is_functor_op)
    fix 𝔉 𝔍 assume prems': "𝔉 : 𝔍 ↦↦C⇘α⇙ op_cat 𝔄"
    then interpret 𝔉: is_functor α 𝔍 ‹op_cat 𝔄› 𝔉 .
    from that assms have op_op_bundle:
      "is_cf_continuous α (op_cf (op_cf 𝔊))"
      "op_cf (op_cf 𝔊) : 𝔄 ↦↦C⇘α⇙ 𝔅"
      unfolding cat_op_simps .
    show "cf_preserves_colimits α (op_cf 𝔊) 𝔉"
      by 
        (
          rule cf_preserves_limits_op
            [
              THEN iffD1, 
              OF
                𝔉.is_functor_axioms 
                𝔊.is_functor_op 
                is_cf_continuousD
                  [
                    OF
                      op_op_bundle(1) 
                      𝔉.is_functor_op[unfolded cat_op_simps] 
                      op_op_bundle(2)
                  ]
            ]
        )
  qed
qed


subsubsection‹Category isomorphisms are continuous and cocontinuous›

lemma (in is_iso_functor) iso_cf_is_cf_continuous: "is_cf_continuous α 𝔉"
proof(intro is_cf_continuousI)
  fix 𝔍 𝔊 assume prems: "𝔊 : 𝔍 ↦↦C⇘α⇙ 𝔄"
  then interpret 𝔊: is_functor α 𝔍 𝔄 𝔊 .
  show "cf_preserves_limits α 𝔉 𝔊"
  proof(intro cf_preserves_limitsI)
    fix a σ assume "σ : a <CF.lim 𝔊 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    then interpret σ: is_cat_limit α 𝔍 𝔄 𝔊 a σ .
    show "𝔉 ∘CF-NTCF σ : 𝔉⦇ObjMap⦈⦇a⦈ <CF.lim 𝔉 ∘CF 𝔊 : 𝔍 ↦↦C⇘α⇙ 𝔅"
    proof(intro is_cat_limitI)
      fix r' τ assume "τ : r' <CF.cone 𝔉 ∘CF 𝔊 : 𝔍 ↦↦C⇘α⇙ 𝔅"
      then interpret τ: is_cat_cone α r' 𝔍 𝔅 ‹𝔉 ∘CF 𝔊› τ .
      note [cat_cs_simps] = cf_comp_assoc_helper[
          where ℌ=‹inv_cf 𝔉› and 𝔊=𝔉 and 𝔉=𝔊 and 𝒬=‹cf_id 𝔄›
          ]
      have inv_τ: "inv_cf 𝔉 ∘CF-NTCF τ :
        inv_cf 𝔉⦇ObjMap⦈⦇r'⦈ <CF.cone 𝔊 : 𝔍 ↦↦C⇘α⇙ 𝔄"
        by
          (
            cs_concl
              cs_simp: cat_cs_simps cf_cs_simps
              cs_intro: cat_cs_intros cf_cs_intros
          )
      from is_cat_limit.cat_lim_unique_cone'[OF σ.is_cat_limit_axioms inv_τ]
      obtain f where f: "f : inv_cf 𝔉⦇ObjMap⦈⦇r'⦈ ↦⇘𝔄⇙ a"
        and f_up: "⋀j. j ∈∘ 𝔍⦇Obj⦈ ⟹
          (inv_cf 𝔉 ∘CF-NTCF τ)⦇NTMap⦈⦇j⦈ = σ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ f"
        and f_unique:
          "⟦
            f' : inv_cf 𝔉⦇ObjMap⦈⦇r'⦈ ↦⇘𝔄⇙ a;
            ⋀j. j ∈∘ 𝔍⦇Obj⦈ ⟹ 
              (inv_cf 𝔉 ∘CF-NTCF τ)⦇NTMap⦈⦇j⦈ = σ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ f'
          ⟧ ⟹ f' = f"
        for f'
        by metis
      have [cat_cs_simps]: "𝔉⦇ArrMap⦈⦇σ⦇NTMap⦈⦇j⦈⦈ ∘A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = τ⦇NTMap⦈⦇j⦈"
        if "j ∈∘ 𝔍⦇Obj⦈" for j
      proof-
        from f_up[OF that] that have 
          "inv_cf 𝔉⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈⦈ = σ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ f"
          by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        then have 
          "𝔉⦇ArrMap⦈⦇inv_cf 𝔉⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈⦈⦈ =
            𝔉⦇ArrMap⦈⦇σ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ f⦈"
          by simp
        from this that f show ?thesis 
          by 
            (
              cs_prems cs_shallow 
                cs_simp: cat_cs_simps cf_cs_simps cs_intro: cat_cs_intros
            ) 
            simp
      qed
      show "∃!f'.
        f' : r' ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈ ∧ τ = 𝔉 ∘CF-NTCF σ ∙NTCF ntcf_const 𝔍 𝔅 f'"
      proof(intro ex1I conjI; (elim conjE)?)
        from f have 
          "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇inv_cf 𝔉⦇ObjMap⦈⦇r'⦈⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
          by (cs_concl cs_shallow cs_intro: cat_cs_intros)
        then show "𝔉⦇ArrMap⦈⦇f⦈ : r' ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
          by (cs_prems cs_shallow cs_simp: cf_cs_simps cs_intro: cat_cs_intros)
        show "τ = 𝔉 ∘CF-NTCF σ ∙NTCF ntcf_const 𝔍 𝔅 (𝔉⦇ArrMap⦈⦇f⦈)"
        proof(rule ntcf_eqI, rule τ.is_ntcf_axioms)
          from f show "𝔉 ∘CF-NTCF σ ∙NTCF ntcf_const 𝔍 𝔅 (𝔉⦇ArrMap⦈⦇f⦈) :
            cf_const 𝔍 𝔅 r' ↦CF 𝔉 ∘CF 𝔊 : 𝔍 ↦↦C⇘α⇙ 𝔅"
            by
              (
                cs_concl
                  cs_simp: cat_cs_simps cf_cs_simps cs_intro: cat_cs_intros
              )
          then have dom_rhs:
            "𝒟∘ ((𝔉 ∘CF-NTCF σ ∙NTCF ntcf_const 𝔍 𝔅 (𝔉⦇ArrMap⦈⦇f⦈))⦇NTMap⦈) = 
              𝔍⦇Obj⦈"
            by (cs_concl cs_simp: cat_cs_simps)
          show 
            "τ⦇NTMap⦈ = (𝔉 ∘CF-NTCF σ ∙NTCF ntcf_const 𝔍 𝔅 (𝔉⦇ArrMap⦈⦇f⦈))⦇NTMap⦈"
          proof(rule vsv_eqI, unfold τ.ntcf_NTMap_vdomain dom_rhs)
            fix j assume "j ∈∘ 𝔍⦇Obj⦈"
            with f show "τ⦇NTMap⦈⦇j⦈ =
              (𝔉 ∘CF-NTCF σ ∙NTCF ntcf_const 𝔍 𝔅 (𝔉⦇ArrMap⦈⦇f⦈))⦇NTMap⦈⦇j⦈"
              by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
          qed (cs_concl cs_intro: V_cs_intros cat_cs_intros)+
        qed simp_all
        fix f' assume prems': 
          "f' : r' ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
          "τ = 𝔉 ∘CF-NTCF σ ∙NTCF ntcf_const 𝔍 𝔅 f'"
        have τj_def: "τ⦇NTMap⦈⦇j⦈ = 𝔉⦇ArrMap⦈⦇σ⦇NTMap⦈⦇j⦈⦈ ∘A⇘𝔅⇙ f'"
          if "j ∈∘ 𝔍⦇Obj⦈" for j
        proof-
          from prems'(2) have
            "τ⦇NTMap⦈⦇j⦈ = (𝔉 ∘CF-NTCF σ ∙NTCF ntcf_const 𝔍 𝔅 f')⦇NTMap⦈⦇j⦈"
            by simp
          from this prems'(1) that show ?thesis
            by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        qed
        have "inv_cf 𝔉⦇ArrMap⦈⦇f'⦈ = f"
        proof(rule f_unique)
          from prems'(1) show 
            "inv_cf 𝔉⦇ArrMap⦈⦇f'⦈ : inv_cf 𝔉⦇ObjMap⦈⦇r'⦈ ↦⇘𝔄⇙ a"
            by
              (
                cs_concl 
                  cs_simp: cf_cs_simps cs_intro: cat_cs_intros cf_cs_intros
              )
          fix j assume "j ∈∘ 𝔍⦇Obj⦈"
          from this prems'(1) show 
            "(inv_cf 𝔉 ∘CF-NTCF τ)⦇NTMap⦈⦇j⦈ = 
              σ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ inv_cf 𝔉⦇ArrMap⦈⦇f'⦈"
            by
              (
                cs_concl 
                  cs_simp: cat_cs_simps cf_cs_simps τj_def
                  cs_intro: cat_cs_intros cf_cs_intros
              )
        qed
        then have "𝔉⦇ArrMap⦈⦇inv_cf 𝔉⦇ArrMap⦈⦇f'⦈⦈ = 𝔉⦇ArrMap⦈⦇f⦈" by simp
        from this prems'(1) show "f' = 𝔉⦇ArrMap⦈⦇f⦈"
          by 
            (
              cs_prems cs_shallow 
                cs_simp: cat_cs_simps cf_cs_simps cs_intro: cat_cs_intros
            )
      qed
    qed (cs_concl cs_intro: cat_cs_intros cat_lim_cs_intros)
  qed (intro prems is_functor_axioms)+
qed (rule is_functor_axioms)

lemma (in is_iso_functor) iso_cf_is_cf_cocontinuous: "is_cf_cocontinuous α 𝔉"
  using is_iso_functor.iso_cf_is_cf_continuous[OF is_iso_functor_op] 
  by (cs_prems cs_shallow cs_simp: cat_op_simps cs_intro: cat_cs_intros)



subsection‹Tiny-continuous and tiny-cocontinuous functor›


subsubsection‹Definition and elementary properties›

definition is_tm_cf_continuous :: "V ⇒ V ⇒ bool"
  where "is_tm_cf_continuous α 𝔊 =
    (∀𝔉 𝔍. 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ 𝔊⦇HomDom⦈ ⟶ cf_preserves_limits α 𝔊 𝔉)"


text‹Rules.›

context
  fixes α 𝔍 𝔄 𝔅 𝔊 𝔉
  assumes 𝔊: "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
begin

interpretation 𝔊: is_functor α 𝔄 𝔅 𝔊 by (rule 𝔊)

mk_ide rf is_tm_cf_continuous_def[where α=α and 𝔊=𝔊, unfolded cat_cs_simps]
  |intro is_tm_cf_continuousI|
  |dest is_tm_cf_continuousD'|
  |elim is_tm_cf_continuousE'|

end

lemmas is_tm_cf_continuousD[dest!] = is_tm_cf_continuousD'[rotated]
  and is_tm_cf_continuousE[elim!] = is_tm_cf_continuousE'[rotated]


text‹Elementary properties.›

lemma (in is_functor) cf_continuous_is_tm_cf_continuous:
  assumes "is_cf_continuous α 𝔉"
  shows "is_tm_cf_continuous α 𝔉"
proof(intro is_tm_cf_continuousI, rule is_functor_axioms)
  fix 𝔉' 𝔍 assume "𝔉' : 𝔍 ↦↦C.tm⇘α⇙ 𝔄"
  then interpret 𝔉': is_tm_functor α 𝔍 𝔄 𝔉'.
  show "cf_preserves_limits α 𝔉 𝔉'"
    by 
      (
        intro is_cf_continuousD[OF assms(1) _ is_functor_axioms], 
        rule 𝔉'.is_functor_axioms
      )
qed

text‹\newpage›

end