Theory CZH_UCAT_Complete

(* Copyright 2021 (C) Mihails Milehins *)

section‹Completeness and cocompleteness›
theory CZH_UCAT_Complete
  imports 
    CZH_UCAT_Limit
    CZH_UCAT_Limit_Product
    CZH_UCAT_Limit_Equalizer
begin



subsection‹Limits by products and equalizers›

lemma cat_limit_of_cat_prod_obj_and_cat_equalizer:
  ―‹See Theorem 1 in Chapter V-2 in \cite{mac_lane_categories_2010}.›
  assumes "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
    and "⋀𝔞 𝔟 𝔤 𝔣. ⟦ 𝔣 : 𝔞 ↦⇘ℭ⇙ 𝔟; 𝔤 : 𝔞 ↦⇘ℭ⇙ 𝔟 ⟧ ⟹
      ∃E ε. ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ"
    and "⋀A. tm_cf_discrete α (𝔍⦇Obj⦈) A ℭ ⟹
      ∃P π. π : P <CF.∏ A : 𝔍⦇Obj⦈ ↦↦C⇘α⇙ ℭ"
    and "⋀A. tm_cf_discrete α (𝔍⦇Arr⦈) A ℭ ⟹
      ∃P π. π : P <CF.∏ A : 𝔍⦇Arr⦈ ↦↦C⇘α⇙ ℭ"
  obtains r u where "u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
proof-

  let ?L =‹λu. 𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇u⦈⦈› and ?R =‹λi. 𝔉⦇ObjMap⦈⦇i⦈›
  
  interpret 𝔉: is_tm_functor α 𝔍 ℭ 𝔉 by (rule assms(1))

  have "?R j ∈∘ ℭ⦇Obj⦈" if "j ∈∘ 𝔍⦇Obj⦈" for j
    by (cs_concl cs_shallow cs_intro: cat_cs_intros that)

  have "tm_cf_discrete α (𝔍⦇Obj⦈) ?R ℭ"
  proof(intro tm_cf_discreteI)
    show "𝔉⦇ObjMap⦈⦇i⦈ ∈∘ ℭ⦇Obj⦈" if "i ∈∘ 𝔍⦇Obj⦈" for i
      by (cs_concl cs_shallow cs_intro: cat_cs_intros that)
    show "VLambda (𝔍⦇Obj⦈) ?R ∈∘ Vset α"
    proof(rule vbrelation.vbrelation_Limit_in_VsetI)
      show "ℛ∘ (VLambda (𝔍⦇Obj⦈) ?R) ∈∘ Vset α"
      proof-
        have "ℛ∘ (VLambda (𝔍⦇Obj⦈) ?R) ⊆∘ ℛ∘ (𝔉⦇ObjMap⦈)"
          by (auto simp: 𝔉.cf_ObjMap_vdomain)
        moreover have "ℛ∘ (𝔉⦇ObjMap⦈) ∈∘ Vset α"
          by (force intro: vrange_in_VsetI 𝔉.tm_cf_ObjMap_in_Vset)
        ultimately show ?thesis by auto
      qed
    qed (auto simp: cat_small_cs_intros)
    show "(λi∈∘𝔍⦇Obj⦈. ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇i⦈⦈) ∈∘ Vset α"
    proof(rule vbrelation.vbrelation_Limit_in_VsetI)
      show "ℛ∘ (λi∈∘𝔍⦇Obj⦈. ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇i⦈⦈) ∈∘ Vset α"
      proof-
        have "ℛ∘ (λi∈∘𝔍⦇Obj⦈. ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇i⦈⦈) ⊆∘ ℛ∘ (𝔉⦇ArrMap⦈)"
        proof(rule vrange_VLambda_vsubset)
          fix x assume x: "x ∈∘ 𝔍⦇Obj⦈"
          then have "𝔍⦇CId⦈⦇x⦈ ∈∘ 𝒟∘ (𝔉⦇ArrMap⦈)"
            by (auto intro: cat_cs_intros simp: cat_cs_simps)
          moreover from x have "ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈ = 𝔉⦇ArrMap⦈⦇𝔍⦇CId⦈⦇x⦈⦈"
            by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
          ultimately show "ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈ ∈∘ ℛ∘ (𝔉⦇ArrMap⦈)"
            by (simp add: 𝔉.ArrMap.vsv_vimageI2)
        qed
        moreover have "ℛ∘ (𝔉⦇ArrMap⦈) ∈∘ Vset α"
          by (force intro: vrange_in_VsetI 𝔉.tm_cf_ArrMap_in_Vset)
        ultimately show ?thesis by auto
      qed
    qed (auto simp: cat_small_cs_intros)
  qed (auto intro: cat_cs_intros)

  from assms(3)[where A=‹?R›, OF this] obtain PO πO
    where πO: "πO : PO <CF.∏ ?R : 𝔍⦇Obj⦈ ↦↦C⇘α⇙ ℭ"
    by clarsimp

  interpret πO: is_cat_obj_prod α ‹𝔍⦇Obj⦈› ?R ℭ PO πO by (rule πO)

  have PO: "PO ∈∘ ℭ⦇Obj⦈" by (intro πO.cat_cone_obj)

  have "?L u ∈∘ ℭ⦇Obj⦈" if "u ∈∘ 𝔍⦇Arr⦈" for u
  proof-
    from that obtain a b where "u : a ↦⇘𝔍⇙ b" by auto
    then show ?thesis 
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed

  have tm_cf_discrete: "tm_cf_discrete α (𝔍⦇Arr⦈) ?L ℭ"
  proof(intro tm_cf_discreteI)
    show "𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇f⦈⦈ ∈∘ ℭ⦇Obj⦈" if "f ∈∘ 𝔍⦇Arr⦈" for f
    proof-
      from that obtain a b where "f : a ↦⇘𝔍⇙ b" by auto
      then show ?thesis 
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed
 
    show "(λu∈∘𝔍⦇Arr⦈. 𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇u⦈⦈) ∈∘ Vset α"
    proof(rule vbrelation.vbrelation_Limit_in_VsetI)
      show "ℛ∘ (λu∈∘𝔍⦇Arr⦈. ?L u) ∈∘ Vset α"
      proof-
        have "ℛ∘ (λu∈∘𝔍⦇Arr⦈. ?L u) ⊆∘ ℛ∘ (𝔉⦇ObjMap⦈)"
        proof(rule vrange_VLambda_vsubset)
          fix f assume "f ∈∘ 𝔍⦇Arr⦈"
          then obtain a b where "f : a ↦⇘𝔍⇙ b" by auto
          then show "𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇f⦈⦈ ∈∘ ℛ∘ (𝔉⦇ObjMap⦈)"
            by 
              (
                cs_concl cs_shallow
                  cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros
              )
        qed
        moreover have "ℛ∘ (𝔉⦇ObjMap⦈) ∈∘ Vset α"
          by (auto intro: vrange_in_VsetI 𝔉.tm_cf_ObjMap_in_Vset)
        ultimately show ?thesis by auto
      qed
    qed (auto simp: cat_small_cs_intros)

    show "(λi∈∘𝔍⦇Arr⦈. ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇i⦈⦈⦈) ∈∘ Vset α"
    proof(rule vbrelation.vbrelation_Limit_in_VsetI)
      show "ℛ∘ (λi∈∘𝔍⦇Arr⦈. ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇i⦈⦈⦈) ∈∘ Vset α"
      proof-
        have "ℛ∘ (λi∈∘𝔍⦇Arr⦈. ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇i⦈⦈⦈) ⊆∘ ℛ∘ (𝔉⦇ArrMap⦈)"
        proof(rule vrange_VLambda_vsubset)
          fix f assume "f ∈∘ 𝔍⦇Arr⦈"
          then obtain a b where f: "f : a ↦⇘𝔍⇙ b" by auto
          then have "𝔍⦇CId⦈⦇b⦈ ∈∘ 𝒟∘ (𝔉⦇ArrMap⦈)"
            by (auto intro: cat_cs_intros simp: cat_cs_simps)
          moreover from f have 
            "ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇f⦈⦈⦈ = 𝔉⦇ArrMap⦈⦇𝔍⦇CId⦈⦇b⦈⦈"
            by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
          ultimately show "ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇f⦈⦈⦈ ∈∘ ℛ∘ (𝔉⦇ArrMap⦈)"
            by (simp add: 𝔉.ArrMap.vsv_vimageI2)
        qed
        moreover have "ℛ∘ (𝔉⦇ArrMap⦈) ∈∘ Vset α"
          by (force intro: vrange_in_VsetI 𝔉.tm_cf_ArrMap_in_Vset)
        ultimately show ?thesis by auto
      qed
    qed (auto simp: cat_small_cs_intros)
  qed (auto intro: cat_cs_intros)

  from assms(4)[where A=‹?L›, OF this, simplified] obtain PA πA
    where πA: "πA : PA <CF.∏ ?L : 𝔍⦇Arr⦈ ↦↦C⇘α⇙ ℭ"
    by auto

  interpret πA: is_cat_obj_prod α ‹𝔍⦇Arr⦈› ?L ℭ PA πA by (rule πA)

  let ?F = ‹λu. 𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇u⦈⦈› and ?f = ‹λu. πO⦇NTMap⦈⦇𝔍⦇Cod⦈⦇u⦈⦈› 
  let ?πO' = ‹ntcf_obj_prod_base ℭ (:C (𝔍⦇Arr⦈)⦇Obj⦈) ?F PO ?f›

  have πO': "?πO' :
    PO <CF.cone :→: (𝔍⦇Arr⦈) (λu. 𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇u⦈⦈) ℭ :
    :C (𝔍⦇Arr⦈) ↦↦C⇘α⇙ ℭ"
    unfolding the_cat_discrete_components(1)
  proof
    (
      intro 
        tm_cf_discrete.tm_cf_discrete_ntcf_obj_prod_base_is_cat_cone 
        tm_cf_discrete
    )
    fix f assume "f ∈∘ 𝔍⦇Arr⦈"
    then obtain a b where "f : a ↦⇘𝔍⇙ b" by auto
    then show "πO⦇NTMap⦈⦇𝔍⦇Cod⦈⦇f⦈⦈ : PO ↦⇘ℭ⇙ 𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇f⦈⦈"
      by 
        (
          cs_concl cs_shallow
            cs_simp:
              the_cat_discrete_components(1) cat_discrete_cs_simps cat_cs_simps
            cs_intro: cat_cs_intros
        )
  qed (intro PO)

  from πA.cat_obj_prod_unique_cone'[OF πO'] obtain f' 
    where f': "f' : PO ↦⇘ℭ⇙ PA"
      and πO'_NTMap_app: 
        "⋀j. j ∈∘ 𝔍⦇Arr⦈ ⟹ ?πO'⦇NTMap⦈⦇j⦈ = πA⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ f'"
      and unique_f':
        "⟦
          f'' : PO ↦⇘ℭ⇙ PA;
          ⋀j. j ∈∘ 𝔍⦇Arr⦈ ⟹ ?πO'⦇NTMap⦈⦇j⦈ = πA⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ f''
         ⟧ ⟹ f'' = f'"
      for f''
    by metis

  have πO_NTMap_app_Cod: 
    "πO⦇NTMap⦈⦇b⦈ = πA⦇NTMap⦈⦇f⦈ ∘A⇘ℭ⇙ f'" if "f : a ↦⇘𝔍⇙ b" for f a b 
  proof-
    from that have "f ∈∘ 𝔍⦇Arr⦈" by auto
    from πO'_NTMap_app[OF this] that show ?thesis
      by 
        (
          cs_prems cs_shallow
            cs_simp: cat_cs_simps the_cat_discrete_components(1)
            cs_intro: cat_cs_intros
        )
  qed

  from this[symmetric] have πA_NTMap_Comp_app: 
    "πA⦇NTMap⦈⦇f⦈ ∘A⇘ℭ⇙ (f' ∘A⇘ℭ⇙ q) = πO⦇NTMap⦈⦇b⦈ ∘A⇘ℭ⇙ q" 
    if "f : a ↦⇘𝔍⇙ b" and "q : c ↦⇘ℭ⇙ PO" for q f a b c 
    using that f'
    by (intro 𝔉.HomCod.cat_assoc_helper)
      (
        cs_concl cs_shallow
          cs_simp: 
            cat_cs_simps cat_discrete_cs_simps the_cat_discrete_components(1)
          cs_intro: cat_cs_intros
      )+

  let ?g = ‹λu. 𝔉⦇ArrMap⦈⦇u⦈ ∘A⇘ℭ⇙ πO⦇NTMap⦈⦇𝔍⦇Dom⦈⦇u⦈⦈› 
  let ?πO'' = ‹ntcf_obj_prod_base ℭ (:C (𝔍⦇Arr⦈)⦇Obj⦈) ?F PO ?g›
  
  have πO'': "?πO'' : PO <CF.cone :→: (𝔍⦇Arr⦈) ?L ℭ : :C (𝔍⦇Arr⦈) ↦↦C⇘α⇙ ℭ"
    unfolding the_cat_discrete_components(1)
  proof
    (
      intro 
        tm_cf_discrete.tm_cf_discrete_ntcf_obj_prod_base_is_cat_cone  
        tm_cf_discrete
    )
    show "𝔉⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ πO⦇NTMap⦈⦇𝔍⦇Dom⦈⦇f⦈⦈ : PO ↦⇘ℭ⇙ 𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇f⦈⦈"
      if "f ∈∘ 𝔍⦇Arr⦈" for f
    proof-
      from that obtain a b where "f : a ↦⇘𝔍⇙ b"  by auto
      then show ?thesis
        by  
          (
            cs_concl 
              cs_simp: 
                cat_cs_simps cat_discrete_cs_simps 
                the_cat_discrete_components(1) 
              cs_intro: cat_cs_intros
          )
    qed
  qed (intro PO)

  from πA.cat_obj_prod_unique_cone'[OF πO''] obtain g' 
    where g': "g' : PO ↦⇘ℭ⇙ PA"
      and πO''_NTMap_app: 
        "⋀j. j ∈∘ 𝔍⦇Arr⦈ ⟹ ?πO''⦇NTMap⦈⦇j⦈ = πA⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ g'"
      and unique_g':
        "⟦
          g'' : PO ↦⇘ℭ⇙ PA;
          ⋀j. j ∈∘ 𝔍⦇Arr⦈ ⟹ ?πO''⦇NTMap⦈⦇j⦈ = πA⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ g''
         ⟧ ⟹ g'' = g'"
      for g''
    by (metis (lifting))

  have "𝔉⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ πO⦇NTMap⦈⦇a⦈ = πA⦇NTMap⦈⦇f⦈ ∘A⇘ℭ⇙ g'" 
    if "f : a ↦⇘𝔍⇙ b" for f a b 
  proof-
    from that have "f ∈∘ 𝔍⦇Arr⦈" by auto
    from πO''_NTMap_app[OF this] that show ?thesis
      by 
        (
          cs_prems cs_shallow
            cs_simp: cat_cs_simps the_cat_discrete_components(1)
            cs_intro: cat_cs_intros
        )
  qed
  then have πO_NTMap_app_Dom: 
    "𝔉⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ (πO⦇NTMap⦈⦇a⦈ ∘A⇘ℭ⇙ q) =
      (πA⦇NTMap⦈⦇f⦈ ∘A⇘ℭ⇙ g') ∘A⇘ℭ⇙ q" 
    if "f : a ↦⇘𝔍⇙ b" and "q : c ↦⇘ℭ⇙  PO" for q f a b c 
    using that g' 
    by (intro 𝔉.HomCod.cat_assoc_helper)
      (
        cs_concl 
          cs_simp: 
            cat_cs_simps cat_discrete_cs_simps the_cat_discrete_components(1)
          cs_intro: cat_cs_intros
      )

  from assms(2)[OF f' g'] obtain E ε where ε: 
    "ε : E <CF.eq (PO,PA,g',f') : ↑↑C ↦↦C⇘α⇙ ℭ"
    by clarsimp

  interpret ε: is_cat_equalizer_2 α PO PA g' f' ℭ E ε by (rule ε)

  define μ where "μ =
    [(λi∈∘𝔍⦇Obj⦈. πO⦇NTMap⦈⦇i⦈ ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈), cf_const 𝔍 ℭ E, 𝔉, 𝔍, ℭ]∘"

  have μ_components:
    "μ⦇NTMap⦈ = (λi∈∘𝔍⦇Obj⦈. πO⦇NTMap⦈⦇i⦈ ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈)"
    "μ⦇NTDom⦈ = cf_const 𝔍 ℭ E"
    "μ⦇NTCod⦈ = 𝔉"
    "μ⦇NTDGDom⦈ = 𝔍"
    "μ⦇NTDGCod⦈ = ℭ"
    unfolding μ_def nt_field_simps by (simp_all add: nat_omega_simps)

  have [cat_cs_simps]: 
    "μ⦇NTMap⦈⦇i⦈ = πO⦇NTMap⦈⦇i⦈ ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈" if "i ∈∘ 𝔍⦇Obj⦈" 
    for i
    using that unfolding μ_components by simp

  have "μ : E <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  proof(intro is_cat_limitI)

    show μ: "μ : E <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ" 
    proof(intro is_cat_coneI is_tm_ntcfI' is_ntcfI')
      show "vfsequence μ" unfolding μ_def by simp 
      show "vcard μ = 5ℕ" unfolding μ_def by (simp add: nat_omega_simps)
      show "cf_const 𝔍 ℭ E : 𝔍 ↦↦C⇘α⇙ ℭ"
        by (cs_concl cs_intro: cat_cs_intros cat_lim_cs_intros)
      show "𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ" by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      show "μ⦇NTMap⦈⦇a⦈ : cf_const 𝔍 ℭ E⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ 𝔉⦇ObjMap⦈⦇a⦈"
        if "a ∈∘ 𝔍⦇Obj⦈" for a
        using that
        by 
          (
            cs_concl 
              cs_simp: 
                cat_cs_simps 
                cat_discrete_cs_simps 
                cat_parallel_cs_simps 
                the_cat_discrete_components(1) 
              cs_intro: cat_cs_intros cat_lim_cs_intros cat_parallel_cs_intros
          )
      show 
        "μ⦇NTMap⦈⦇b⦈ ∘A⇘ℭ⇙ cf_const 𝔍 ℭ E⦇ArrMap⦈⦇f⦈ =
          𝔉⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ μ⦇NTMap⦈⦇a⦈"
        if "f : a ↦⇘𝔍⇙ b" for a b f
        using that ε g' f' 
        by 
          (
            cs_concl 
              cs_simp:
                cat_parallel_cs_simps
                cat_cs_simps 
                the_cat_discrete_components(1) 
                πO_NTMap_app_Cod 
                πO_NTMap_app_Dom 
                ε.cat_eq_2_Comp_eq(1) 
              cs_intro: cat_lim_cs_intros cat_cs_intros cat_parallel_cs_intros
          )

    qed (auto simp: μ_components cat_cs_intros)

    interpret μ: is_cat_cone α E 𝔍 ℭ 𝔉 μ by (rule μ)

    show "∃!f'. f' : r' ↦⇘ℭ⇙ E ∧ u' = μ ∙NTCF ntcf_const 𝔍 ℭ f'"
      if "u' : r' <CF.cone 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ" for u' r'
    proof-

      interpret u': is_cat_cone α r' 𝔍 ℭ 𝔉 u' by (rule that)

      let ?u' = ‹λj. u'⦇NTMap⦈⦇j⦈› 
      let ?π' = ‹ntcf_obj_prod_base ℭ (𝔍⦇Obj⦈) ?R r' ?u'›

      have π'_NTMap_app: "?π'⦇NTMap⦈⦇j⦈ = u'⦇NTMap⦈⦇j⦈" if "j ∈∘ 𝔍⦇Obj⦈" for j
        using that 
        unfolding ntcf_obj_prod_base_components the_cat_discrete_components 
        by auto

      have π': "?π' : r' <CF.cone :→: (𝔍⦇Obj⦈) ?R ℭ : :C (𝔍⦇Obj⦈) ↦↦C⇘α⇙ ℭ"
        unfolding the_cat_discrete_components(1)
      proof(intro tm_cf_discrete.tm_cf_discrete_ntcf_obj_prod_base_is_cat_cone)
        show "tm_cf_discrete α (𝔍⦇Obj⦈) ?R ℭ"
        proof(intro tm_cf_discreteI)
          show "𝔉⦇ObjMap⦈⦇i⦈ ∈∘ ℭ⦇Obj⦈" if "i ∈∘ 𝔍⦇Obj⦈" for i
            by (cs_concl cs_simp: cat_cs_simps cs_intro: that cat_cs_intros)
          show "category α ℭ" by (auto intro: cat_cs_intros)
          from 𝔉.tm_cf_ObjMap_in_Vset show "(λx∈∘𝔍⦇Obj⦈. 𝔉⦇ObjMap⦈⦇x⦈) ∈∘ Vset α"
            by (auto simp: 𝔉.cf_ObjMap_vdomain)
          show "(λi∈∘𝔍⦇Obj⦈. ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇i⦈⦈) ∈∘ Vset α"
          proof(rule vbrelation.vbrelation_Limit_in_VsetI)
            have "ℛ∘ (λi∈∘𝔍⦇Obj⦈. ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇i⦈⦈) ⊆∘ ℛ∘ (𝔉⦇ArrMap⦈)"
            proof(intro vsubsetI)
              fix x assume "x ∈∘ ℛ∘ (λi∈∘𝔍⦇Obj⦈. ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇i⦈⦈)"
              then obtain i where i: "i ∈∘ 𝔍⦇Obj⦈" 
                and x_def: "x = ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇i⦈⦈"
                by auto
              from i have "x = 𝔉⦇ArrMap⦈⦇𝔍⦇CId⦈⦇i⦈⦈"
                by (simp add: x_def 𝔉.cf_ObjMap_CId)
              moreover from i have "𝔍⦇CId⦈⦇i⦈ ∈∘ 𝒟∘ (𝔉⦇ArrMap⦈)"
                by 
                  (
                    cs_concl cs_shallow 
                      cs_simp: cat_cs_simps cs_intro: cat_cs_intros
                  )
              ultimately show "x ∈∘ ℛ∘ (𝔉⦇ArrMap⦈)"
                by (auto intro: 𝔉.ArrMap.vsv_vimageI2)
            qed
            then show "ℛ∘ (λi∈∘𝔍⦇Obj⦈. ℭ⦇CId⦈⦇𝔉⦇ObjMap⦈⦇i⦈⦈) ∈∘ Vset α"  
              by
                (
                  auto simp: 
                    𝔉.tm_cf_ArrMap_in_Vset vrange_in_VsetI vsubset_in_VsetI
                )
          qed (auto intro: 𝔉.HomDom.tiny_cat_Obj_in_Vset)
        qed
        show "u'⦇NTMap⦈⦇j⦈ : r' ↦⇘ℭ⇙ 𝔉⦇ObjMap⦈⦇j⦈" if "j ∈∘ 𝔍⦇Obj⦈" for j
          using that 
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      qed (auto simp: cat_cs_intros)

      from πO.cat_obj_prod_unique_cone'[OF this] obtain h' 
        where h': "h' : r' ↦⇘ℭ⇙ PO"
          and π'_NTMap_app': 
            "⋀j. j ∈∘ (𝔍⦇Obj⦈) ⟹ ?π'⦇NTMap⦈⦇j⦈ = πO⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ h'"
          and unique_h': "⋀h''.
            ⟦ 
              h'' : r' ↦⇘ℭ⇙ PO;
              ⋀j. j ∈∘ (𝔍⦇Obj⦈) ⟹ ?π'⦇NTMap⦈⦇j⦈ = πO⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ h'' 
            ⟧ ⟹ h'' = h'"
        by metis

      interpret π':
        is_cat_cone α r' ‹:C (𝔍⦇Obj⦈)› ℭ ‹:→: (𝔍⦇Obj⦈) (app (𝔉⦇ObjMap⦈)) ℭ› ?π'
        by (rule π')

      let ?u'' = ‹λu. u'⦇NTMap⦈⦇𝔍⦇Cod⦈⦇u⦈⦈› 
      let ?π'' = ‹ntcf_obj_prod_base ℭ (𝔍⦇Arr⦈) ?L r' ?u''›

      have π''_NTMap_app: "?π''⦇NTMap⦈⦇f⦈ = u'⦇NTMap⦈⦇b⦈"
        if "f : a ↦⇘𝔍⇙ b" for f a b 
        using that 
        unfolding ntcf_obj_prod_base_components the_cat_discrete_components 
        by 
          (
            cs_concl cs_shallow
              cs_simp: V_cs_simps cat_cs_simps cs_intro: cat_cs_intros
          )
      
      have π'': "?π'' : r' <CF.cone :→: (𝔍⦇Arr⦈) ?L ℭ : :C (𝔍⦇Arr⦈) ↦↦C⇘α⇙ ℭ"
        unfolding the_cat_discrete_components(1)
      proof
        (
          intro 
            tm_cf_discrete.tm_cf_discrete_ntcf_obj_prod_base_is_cat_cone 
            tm_cf_discrete
        )
        fix f assume "f ∈∘ 𝔍⦇Arr⦈"
        then obtain a b where "f : a ↦⇘𝔍⇙ b" by auto
        then show "u'⦇NTMap⦈⦇𝔍⦇Cod⦈⦇f⦈⦈ : r' ↦⇘ℭ⇙ 𝔉⦇ObjMap⦈⦇𝔍⦇Cod⦈⦇f⦈⦈"
          by 
            (
              cs_concl cs_shallow
                cs_simp: cat_cs_simps cs_intro: cat_cs_intros
            )
      qed (simp add: cat_cs_intros)

      from πA.cat_obj_prod_unique_cone'[OF this] obtain h'' 
        where h'': "h'' : r' ↦⇘ℭ⇙ PA"
          and π''_NTMap_app': 
            "⋀j. j ∈∘ 𝔍⦇Arr⦈ ⟹ ?π''⦇NTMap⦈⦇j⦈ = πA⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ h''"
          and unique_h'': "⋀h'''.
            ⟦ 
              h''' : r' ↦⇘ℭ⇙ PA;
              ⋀j. j ∈∘ 𝔍⦇Arr⦈ ⟹ ?π''⦇NTMap⦈⦇j⦈ = πA⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ h''' 
            ⟧ ⟹ h''' = h''"
        by metis

      interpret π'': is_cat_cone α r' ‹:C (𝔍⦇Arr⦈)› ℭ ‹:→: (𝔍⦇Arr⦈) ?L ℭ› ?π''
        by (rule π'')

      have g'h'_f'h': "g' ∘A⇘ℭ⇙ h' = f' ∘A⇘ℭ⇙ h'"  
      proof-

        from g' h' have g'h': "g' ∘A⇘ℭ⇙ h' : r' ↦⇘ℭ⇙ PA"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        from f' h' have f'h': "f' ∘A⇘ℭ⇙ h' : r' ↦⇘ℭ⇙ PA"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

        have "?π''⦇NTMap⦈⦇f⦈ = πA⦇NTMap⦈⦇f⦈ ∘A⇘ℭ⇙ (g' ∘A⇘ℭ⇙ h')"
          if "f ∈∘ 𝔍⦇Arr⦈" for f
        proof-
          from that obtain a b where f: "f : a ↦⇘𝔍⇙ b" by auto
          then have "?π''⦇NTMap⦈⦇f⦈ = u'⦇NTMap⦈⦇b⦈"
            by (cs_concl cs_simp: π''_NTMap_app cat_cs_simps)
          also from f have "… = 𝔉⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ ?π'⦇NTMap⦈⦇a⦈"
            by 
              (
                cs_concl  
                  cs_simp: π'_NTMap_app cat_cs_simps cat_lim_cs_simps 
                  cs_intro: cat_cs_intros
              )
          also from f g' h' have "… = πA⦇NTMap⦈⦇f⦈ ∘A⇘ℭ⇙ (g' ∘A⇘ℭ⇙ h')" 
            by 
              (
                cs_concl 
                  cs_simp: 
                    cat_cs_simps 
                    cat_discrete_cs_simps
                    the_cat_discrete_components(1) 
                    π'_NTMap_app'
                    πO_NTMap_app_Dom 
                  cs_intro: cat_cs_intros
              )
          finally show ?thesis by simp
        qed
          
        from unique_h''[OF g'h' this, simplified] have g'h'_h'': 
          "g' ∘A⇘ℭ⇙ h' = h''".
        have "?π''⦇NTMap⦈⦇f⦈ = πA⦇NTMap⦈⦇f⦈ ∘A⇘ℭ⇙ (f' ∘A⇘ℭ⇙ h')"
          if "f ∈∘ 𝔍⦇Arr⦈" for f
        proof-
          from that obtain a b where f: "f : a ↦⇘𝔍⇙ b" by auto
          then have "?π''⦇NTMap⦈⦇f⦈ = u'⦇NTMap⦈⦇b⦈"
            by (cs_concl cs_simp: π''_NTMap_app cat_cs_simps)
          also from f have "… = ?π'⦇NTMap⦈⦇b⦈"
            by 
              (
                cs_concl cs_shallow 
                  cs_simp: π'_NTMap_app cs_intro: cat_cs_intros
              )
          also from f have "… = πO⦇NTMap⦈⦇b⦈ ∘A⇘ℭ⇙ h'"
            by 
              (
                cs_concl cs_shallow 
                  cs_simp: π'_NTMap_app' cs_intro: cat_cs_intros
              )
          also from f g' h' have "… = (πA⦇NTMap⦈⦇f⦈ ∘A⇘ℭ⇙ f') ∘A⇘ℭ⇙ h'"
            by 
              (
                cs_concl cs_shallow 
                  cs_simp: πO_NTMap_app_Cod cs_intro: cat_cs_intros
              )
          also from that f' h' have "… = πA⦇NTMap⦈⦇f⦈ ∘A⇘ℭ⇙ (f' ∘A⇘ℭ⇙ h')"
            by 
              (
                cs_concl cs_shallow
                  cs_simp: cat_cs_simps the_cat_discrete_components(1) 
                  cs_intro: cat_cs_intros
               )
          finally show ?thesis by simp
        qed
        from unique_h''[OF f'h' this, simplified] have f'h'_h'': 
          "f' ∘A⇘ℭ⇙ h' = h''".
        from g'h'_h'' f'h'_h'' show ?thesis by simp
      qed

      let ?II = ‹↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL› 
        and ?II_II = ‹↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL PO PA g' f'›

    define ε' where "ε' =
      [
        (λf∈∘?II⦇Obj⦈. (f = 𝔞PL2 ? h' : (f' ∘A⇘ℭ⇙ h'))),
        cf_const ?II ℭ r',
        ?II_II,
        ?II,
        ℭ
      ]∘"

    have ε'_components: 
      "ε'⦇NTMap⦈ = (λf∈∘?II⦇Obj⦈. (f = 𝔞PL2 ? h' : (f' ∘A⇘ℭ⇙ h')))"
      "ε'⦇NTDom⦈ = cf_const ?II ℭ r'"
      "ε'⦇NTCod⦈ = ?II_II"
      "ε'⦇NTDGDom⦈ = ?II"
      "ε'⦇NTDGCod⦈ = ℭ"
      unfolding ε'_def nt_field_simps by (simp_all add: nat_omega_simps)

    have ε'_NTMap_app_I2: "ε'⦇NTMap⦈⦇x⦈ = h'" if "x = 𝔞PL2" for x 
    proof-
      have "x ∈∘ ?II⦇Obj⦈"
        unfolding that by (cs_concl cs_intro: cat_parallel_cs_intros)
      then show ?thesis unfolding ε'_components that by simp
    qed

    have ε'_NTMap_app_sI2: "ε'⦇NTMap⦈⦇x⦈ = f' ∘A⇘ℭ⇙ h'" if "x = 𝔟PL2" for x 
    proof-
      have "x ∈∘ ?II⦇Obj⦈"
        unfolding that by (cs_concl cs_shallow cs_intro: cat_parallel_cs_intros)
      with ε.cat_parallel_𝔞𝔟 show ?thesis
        unfolding ε'_components by (cs_concl cs_simp: V_cs_simps that)
    qed

    interpret par: cf_parallel_2 α 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL PO PA g' f' ℭ
      by (intro cf_parallel_2I cat_parallel_2I)
        (simp_all add: cat_cs_intros cat_parallel_cs_intros)

    have "ε' : r' <CF.cone ?II_II : ?II ↦↦C⇘α⇙ ℭ"
    proof(intro is_cat_coneI is_tm_ntcfI' is_ntcfI')
      show "vfsequence ε'" unfolding ε'_def by auto
      show "vcard ε' = 5ℕ" unfolding ε'_def by (simp add: nat_omega_simps)
      from h' show "cf_const (?II) ℭ r' : ?II ↦↦C⇘α⇙ ℭ"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      show "?II_II : ?II ↦↦C⇘α⇙ ℭ"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_parallel_cs_simps cs_intro: cat_cs_intros
          )
      from h' show "ε'⦇NTMap⦈⦇a⦈ : 
        cf_const ?II ℭ r'⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ ?II_II⦇ObjMap⦈⦇a⦈"
        if "a ∈∘ ?II⦇Obj⦈" for a 
        using that
        by (elim the_cat_parallel_2_ObjE; simp only:)
          (
            cs_concl 
              cs_simp: 
                ε'_NTMap_app_I2 ε'_NTMap_app_sI2 
                cat_cs_simps cat_parallel_cs_simps 
              cs_intro: cat_cs_intros cat_parallel_cs_intros
          )
      from h' f' g'h'_f'h' show 
        "ε'⦇NTMap⦈⦇b⦈ ∘A⇘ℭ⇙ cf_const ?II ℭ r'⦇ArrMap⦈⦇f⦈ =
          ?II_II⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ ε'⦇NTMap⦈⦇a⦈"
          if "f : a ↦⇘?II⇙ b" for a b f
          using that
          by (elim ε.the_cat_parallel_2_is_arrE; simp only:)
            (
              cs_concl 
                cs_intro: cat_cs_intros cat_parallel_cs_intros 
                cs_simp:
                  cat_cs_simps
                  cat_parallel_cs_simps
                  ε'_NTMap_app_I2 
                  ε'_NTMap_app_sI2
            )+
      qed 
        (
          simp add: ε'_components | 
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_lim_cs_intros cat_cs_intros cat_small_cs_intros 
        )+
    from ε.cat_eq_2_unique_cone[OF this] obtain t'
      where t': "t' : r' ↦⇘ℭ⇙ E"
        and ε'_NTMap_app: "ε'⦇NTMap⦈⦇𝔞PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ t'"
        and unique_t':
          "⟦ t'' : r' ↦⇘ℭ⇙ E; ε'⦇NTMap⦈⦇𝔞PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ t''⟧ ⟹ 
            t'' = t'" 
        for t''
      by metis

    show "∃!f'. f' : r' ↦⇘ℭ⇙ E ∧ u' = μ ∙NTCF ntcf_const 𝔍 ℭ f'"
    proof(intro ex1I conjI; (elim conjE)?, (rule t')?)
      show [symmetric, cat_cs_simps]: "u' = μ ∙NTCF ntcf_const 𝔍 ℭ t'"
      proof(rule ntcf_eqI[OF u'.is_ntcf_axioms])
        from t' show 
          "μ ∙NTCF ntcf_const 𝔍 ℭ t' : cf_const 𝔍 ℭ r' ↦CF 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        show "u'⦇NTMap⦈ = (μ ∙NTCF ntcf_const 𝔍 ℭ t')⦇NTMap⦈"
        proof(rule vsv_eqI)
          show "vsv ((μ ∙NTCF ntcf_const 𝔍 ℭ t')⦇NTMap⦈)"
            by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
          from t' show 
            "𝒟∘ (u'⦇NTMap⦈) = 𝒟∘ ((μ ∙NTCF ntcf_const 𝔍 ℭ t')⦇NTMap⦈)"
            by 
              (
                cs_concl cs_shallow 
                  cs_simp: cat_cs_simps cs_intro: cat_cs_intros
              )
          show "u'⦇NTMap⦈⦇a⦈ = (μ ∙NTCF ntcf_const 𝔍 ℭ t')⦇NTMap⦈⦇a⦈"
            if "a ∈∘ 𝒟∘ (u'⦇NTMap⦈)" for a
          proof-
            from that have "a ∈∘ 𝔍⦇Obj⦈" 
              by (cs_prems cs_shallow cs_simp: cat_cs_simps)
            with t' show "u'⦇NTMap⦈⦇a⦈ = (μ ∙NTCF ntcf_const 𝔍 ℭ t')⦇NTMap⦈⦇a⦈"
              by 
                (
                  cs_concl 
                    cs_simp:
                      cat_cs_simps 
                      π'_NTMap_app
                      cat_parallel_cs_simps
                      the_cat_discrete_components(1)
                      ε'_NTMap_app[symmetric]
                      ε'_NTMap_app_I2
                      π'_NTMap_app'[symmetric]
                    cs_intro: cat_cs_intros cat_parallel_cs_intros
                )
          qed
        qed auto
      qed simp_all

      fix t'' assume prems': "t'' : r' ↦⇘ℭ⇙ E" "u' = μ ∙NTCF ntcf_const 𝔍 ℭ t''"
      then have u'_NTMap_app_x:
        "u'⦇NTMap⦈⦇x⦈ = (μ ∙NTCF ntcf_const 𝔍 ℭ t'')⦇NTMap⦈⦇x⦈"
        for x 
        by simp
      have "?π'⦇NTMap⦈⦇j⦈ = πO⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ (ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ t'')" 
        if "j ∈∘ 𝔍⦇Obj⦈" for j
        using u'_NTMap_app_x[of j] prems'(1) that
        by 
          (
            cs_prems 
              cs_simp:
                cat_cs_simps 
                cat_discrete_cs_simps 
                cat_parallel_cs_simps 
                the_cat_discrete_components(1) 
              cs_intro: cat_cs_intros cat_parallel_cs_intros
          ) 
          (simp add: π'_NTMap_app[OF that, symmetric])
      moreover from prems'(1) have "ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ t'' : r' ↦⇘ℭ⇙ PO"
        by 
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_parallel_cs_simps 
              cs_intro: cat_cs_intros cat_parallel_cs_intros
          )
      ultimately have [cat_cs_simps]: "ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ t'' = h'" 
        by (intro unique_h') simp
      show "t'' = t'"
        by (rule unique_t', intro prems'(1)) 
          (cs_concl cs_shallow cs_simp: ε'_NTMap_app_I2 cat_cs_simps)
      qed
    qed
 
  qed
  
  then show ?thesis using that by clarsimp

qed

lemma cat_colimit_of_cat_prod_obj_and_cat_coequalizer:
  ―‹See Theorem 1 in Chapter V-2 in \cite{mac_lane_categories_2010}.›
  assumes "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
    and "⋀𝔞 𝔟 𝔤 𝔣. ⟦ 𝔣 : 𝔟 ↦⇘ℭ⇙ 𝔞; 𝔤 : 𝔟 ↦⇘ℭ⇙ 𝔞 ⟧ ⟹
      ∃E ε. ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ"
    and "⋀A. tm_cf_discrete α (𝔍⦇Obj⦈) A ℭ ⟹
      ∃P π. π : A >CF.∐ P : 𝔍⦇Obj⦈ ↦↦C⇘α⇙ ℭ"
    and "⋀A. tm_cf_discrete α (𝔍⦇Arr⦈) A ℭ ⟹
      ∃P π. π : A >CF.∐ P : 𝔍⦇Arr⦈ ↦↦C⇘α⇙ ℭ"
  obtains r u where "u : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ ℭ"
proof-
  interpret 𝔉: is_tm_functor α 𝔍 ℭ 𝔉 by (rule assms(1))
  have "∃E ε. ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ op_cat ℭ"
    if "𝔣 : 𝔟 ↦⇘ℭ⇙ 𝔞" "𝔤 : 𝔟 ↦⇘ℭ⇙ 𝔞" for 𝔞 𝔟 𝔤 𝔣
  proof-
    from assms(2)[OF that(1,2)] obtain E ε 
      where ε: "ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ"
      by clarsimp
    interpret ε: is_cat_coequalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E ε by (rule ε)
    from ε.is_cat_equalizer_2_op[unfolded cat_op_simps] show ?thesis by auto
  qed
  moreover have "∃P π. π : P <CF.∏ A : 𝔍⦇Obj⦈ ↦↦C⇘α⇙ op_cat ℭ"
    if "tm_cf_discrete α (𝔍⦇Obj⦈) A (op_cat ℭ)" for A
  proof-
    interpret tm_cf_discrete α ‹𝔍⦇Obj⦈› A ‹op_cat ℭ› by (rule that)
    from assms(3)[OF tm_cf_discrete_op[unfolded cat_op_simps]] obtain P π 
      where π: "π : A >CF.∐ P : 𝔍⦇Obj⦈ ↦↦C⇘α⇙ ℭ"
      by clarsimp 
    interpret π: is_cat_obj_coprod α ‹𝔍⦇Obj⦈› A ℭ P π by (rule π)
    from π.is_cat_obj_prod_op show ?thesis by auto
  qed
  moreover have "∃P π. π : P <CF.∏ A : 𝔍⦇Arr⦈ ↦↦C⇘α⇙ op_cat ℭ"
    if "tm_cf_discrete α (𝔍⦇Arr⦈) A (op_cat ℭ)" for A 
  proof-
    interpret tm_cf_discrete α ‹𝔍⦇Arr⦈› A ‹op_cat ℭ› by (rule that)
    from assms(4)[OF tm_cf_discrete_op[unfolded cat_op_simps]] obtain P π 
      where π: "π : A >CF.∐ P : 𝔍⦇Arr⦈ ↦↦C⇘α⇙ ℭ"
      by clarsimp 
    interpret π: is_cat_obj_coprod α ‹𝔍⦇Arr⦈› A ℭ P π by (rule π)
    from π.is_cat_obj_prod_op show ?thesis by auto
  qed
  ultimately obtain u r where u: 
    "u : r <CF.lim op_cf 𝔉 : op_cat 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
    by 
      (
        rule cat_limit_of_cat_prod_obj_and_cat_equalizer[
          OF 𝔉.is_tm_functor_op, unfolded cat_op_simps
          ]
      )
  interpret u: is_cat_limit α ‹op_cat 𝔍› ‹op_cat ℭ› ‹op_cf 𝔉› r u by (rule u)
  from u.is_cat_colimit_op[unfolded cat_op_simps] that show ?thesis by simp
qed



subsection‹Small-complete and small-cocomplete category›


subsubsection‹Definition and elementary properties›

locale cat_small_complete = category α ℭ for α ℭ + 
  assumes cat_small_complete: 
    "⋀𝔉 𝔍. 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ ⟹ ∃u r. u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"

locale cat_small_cocomplete = category α ℭ for α ℭ + 
  assumes cat_small_cocomplete: 
    "⋀𝔉 𝔍. 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ ⟹ ∃u r. u : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ ℭ"


text‹Rules.›

mk_ide rf cat_small_complete_def[unfolded cat_small_complete_axioms_def]
  |intro cat_small_completeI|
  |dest cat_small_completeD[dest]|
  |elim cat_small_completeE[elim]|

lemma cat_small_completeE'[elim]:
  assumes "cat_small_complete α ℭ" and "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
  obtains u r where "u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  using assms by auto

mk_ide rf cat_small_cocomplete_def[unfolded cat_small_cocomplete_axioms_def]
  |intro cat_small_cocompleteI|
  |dest cat_small_cocompleteD[dest]|
  |elim cat_small_cocompleteE[elim]|

lemma cat_small_cocompleteE'[elim]:
  assumes "cat_small_cocomplete α ℭ" and "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
  obtains u r where "u : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ ℭ"
  using assms by auto


subsubsection‹Duality›

lemma (in cat_small_complete) cat_small_cocomplete_op[cat_op_intros]:
  "cat_small_cocomplete α (op_cat ℭ)"
proof(intro cat_small_cocompleteI)
  fix 𝔉 𝔍 assume "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ op_cat ℭ"
  then interpret 𝔉: is_tm_functor α 𝔍 ‹op_cat ℭ› 𝔉 .
  from cat_small_complete[OF 𝔉.is_tm_functor_op[unfolded cat_op_simps]]
  obtain u r where u: "u : r <CF.lim op_cf 𝔉 : op_cat 𝔍 ↦↦C⇘α⇙ ℭ"
    by auto
  then interpret u: is_cat_limit α ‹op_cat 𝔍› ℭ ‹op_cf 𝔉› r u .
  from u.is_cat_colimit_op[unfolded cat_op_simps] show 
    "∃u r. u : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
    by auto
qed (auto intro: cat_cs_intros)

lemmas [cat_op_intros] = cat_small_complete.cat_small_cocomplete_op

lemma (in cat_small_cocomplete) cat_small_complete_op[cat_op_intros]:
  "cat_small_complete α (op_cat ℭ)"
proof(intro cat_small_completeI)
  fix 𝔉 𝔍 assume prems: "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ op_cat ℭ"
  then interpret 𝔉: is_tm_functor α 𝔍 ‹op_cat ℭ› 𝔉 .
  from cat_small_cocomplete[OF 𝔉.is_tm_functor_op[unfolded cat_op_simps]]
  obtain u r where u: "u : op_cf 𝔉 >CF.colim r : op_cat 𝔍 ↦↦C⇘α⇙ ℭ"
    by auto
  interpret u: is_cat_colimit α ‹op_cat 𝔍› ℭ ‹op_cf 𝔉› r u by (rule u)
  from u.is_cat_limit_op[unfolded cat_op_simps] show 
    "∃u r. u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ op_cat ℭ"
    by auto
qed (auto intro: cat_cs_intros)

lemmas [cat_op_intros] = cat_small_cocomplete.cat_small_complete_op


subsubsection‹A category with equalizers and small products is small-complete›

lemma (in category) cat_small_complete_if_eq_and_obj_prod:
  ―‹See Corollary 2 in Chapter V-2 in \cite{mac_lane_categories_2010}›
  assumes "⋀𝔞 𝔟 𝔤 𝔣. ⟦ 𝔣 : 𝔞 ↦⇘ℭ⇙ 𝔟; 𝔤 : 𝔞 ↦⇘ℭ⇙ 𝔟 ⟧ ⟹
      ∃E ε. ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ"
    and "⋀A I. tm_cf_discrete α I A ℭ ⟹ ∃P π. π : P <CF.∏ A : I ↦↦C⇘α⇙ ℭ"
  shows "cat_small_complete α ℭ"
proof(intro cat_small_completeI)
  fix 𝔉 𝔍 assume prems: "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ ℭ"
  then interpret 𝔉: is_tm_functor α 𝔍 ℭ 𝔉 .
  show "∃u r. u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
    by (rule cat_limit_of_cat_prod_obj_and_cat_equalizer[OF prems assms(1)])
      (auto intro: assms(2))
qed (auto simp: cat_cs_intros)

lemma (in category) cat_small_cocomplete_if_eq_and_obj_prod:
  assumes "⋀𝔞 𝔟 𝔤 𝔣. ⟦ 𝔣 : 𝔟 ↦⇘ℭ⇙ 𝔞; 𝔤 : 𝔟 ↦⇘ℭ⇙ 𝔞 ⟧ ⟹
    ∃E ε. ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ"
    and "⋀A I. tm_cf_discrete α I A ℭ ⟹ ∃P π. π : A >CF.∐ P : I ↦↦C⇘α⇙ ℭ"
  shows "cat_small_cocomplete α ℭ"
proof-
  have "∃E ε. ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ op_cat ℭ"
    if "𝔣 : 𝔟 ↦⇘ℭ⇙ 𝔞" and "𝔤 : 𝔟 ↦⇘ℭ⇙ 𝔞" for 𝔞 𝔟 𝔤 𝔣
  proof-
    from assms(1)[OF that] obtain ε E where 
      ε: "ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ"
      by clarsimp
    interpret ε: is_cat_coequalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E ε by (rule ε)
    from ε.is_cat_equalizer_2_op show ?thesis by auto
  qed
  moreover have "∃P π. π : P <CF.∏ A : I ↦↦C⇘α⇙ op_cat ℭ"
    if "tm_cf_discrete α I A (op_cat ℭ)" for A I
  proof-
    interpret tm_cf_discrete α I A ‹op_cat ℭ› by (rule that)
    from assms(2)[OF tm_cf_discrete_op[unfolded cat_op_simps]] obtain P π 
      where π: "π : A >CF.∐ P : I ↦↦C⇘α⇙ ℭ"
      by auto
    interpret π: is_cat_obj_coprod α I A ℭ P π by (rule π)
    from π.is_cat_obj_prod_op show ?thesis by auto
  qed
  ultimately interpret cat_small_complete α ‹op_cat ℭ›
    by 
      (
        rule category.cat_small_complete_if_eq_and_obj_prod[
          OF category_op, unfolded cat_op_simps
          ]
      )
  show ?thesis by (rule cat_small_cocomplete_op[unfolded cat_op_simps])
qed


subsubsection‹
Existence of the initial and terminal objects in 
small-complete and small-cocomplete categories
›

lemma (in cat_small_complete) cat_sc_ex_obj_initial:
  ―‹See Theorem 1 in Chapter V-6 in \cite{mac_lane_categories_2010}.›
  assumes "A ⊆∘ ℭ⦇Obj⦈"
    and "A ∈∘ Vset α"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ ∃f a. a ∈∘ A ∧ f : a ↦⇘ℭ⇙ c"
  obtains z where "obj_initial ℭ z"
proof-
  
  interpret tcd: tm_cf_discrete α A id ℭ
  proof(intro tm_cf_discreteI)
    show "(λi∈∘A. ℭ⦇CId⦈⦇id i⦈) ∈∘ Vset α"
      unfolding id_def
    proof(rule vbrelation.vbrelation_Limit_in_VsetI)
      from assms(1) have "A ⊆∘ 𝒟∘ (ℭ⦇CId⦈)" by (simp add: cat_CId_vdomain)
      then have "ℛ∘ (VLambda A (app (ℭ⦇CId⦈))) = ℭ⦇CId⦈ `∘ A" by auto
      moreover have "(⋃∘a∈∘A. ⋃∘b∈∘A. Hom ℭ a b) ∈∘ Vset α"
        by (rule cat_Hom_vifunion_in_Vset[OF assms(1,1,2,2)])
      moreover have "ℭ⦇CId⦈ `∘ A ⊆∘ (⋃∘a∈∘A. ⋃∘b∈∘A. Hom ℭ a b)"
      proof(intro vsubsetI)
        fix f assume "f ∈∘ ℭ⦇CId⦈ `∘ A"
        then obtain a where a: "a ∈∘ A" and f_def: "f = ℭ⦇CId⦈⦇a⦈" by auto
        from assms(1) a show "f ∈∘ (⋃∘a∈∘A. ⋃∘b∈∘A. Hom ℭ a b)"
          unfolding f_def by (intro vifunionI) (auto simp: cat_CId_is_arr)
      qed
      ultimately show "ℛ∘ (VLambda A (app (ℭ⦇CId⦈))) ∈∘ Vset α" by auto
    qed (simp_all add: assms(2))
  qed 
    (
      use assms in 
        ‹auto simp: assms(2) Limit_vid_on_in_Vset intro: cat_cs_intros›
    )

  have tcd: ":→: A id ℭ : :C A ↦↦C.tm⇘α⇙ ℭ"
    by 
      (
        cs_concl cs_shallow cs_intro: 
          cat_small_cs_intros 
          cat_cs_intros 
          cat_small_discrete_cs_intros
          cat_discrete_cs_intros
      )
  from cat_small_complete[OF this] obtain π w 
    where "π : w <CF.lim :→: A id ℭ : :C A ↦↦C⇘α⇙ ℭ"
    by auto
  then interpret π: is_cat_obj_prod α A id ℭ w π
    by (intro is_cat_obj_prodI tcd.cf_discrete_axioms)

  let ?ww = ‹Hom ℭ w w›

  have CId_w: "ℭ⦇CId⦈⦇w⦈ ∈∘ ?ww"
    by (cs_concl cs_intro: cat_cs_intros cat_lim_cs_intros)
  then have ww_neq_vempty: "?ww ≠ 0" by force

  have wd: "∃h. h : w ↦⇘ℭ⇙ d" if "d ∈∘ ℭ⦇Obj⦈" for d
  proof-
    from assms(3)[OF that] obtain g a where a: "a ∈∘ A" and g: "g : a ↦⇘ℭ⇙ d"
      by clarsimp
    from π.ntcf_NTMap_is_arr[unfolded the_cat_discrete_components, OF a] a g 
    have "π⦇NTMap⦈⦇a⦈ : w ↦⇘ℭ⇙ a"
      by
        (
          cs_prems cs_shallow cs_simp:
            id_apply the_cat_discrete_components(1) 
            cat_discrete_cs_simps cat_cs_simps
        )
    with g have "g ∘A⇘ℭ⇙ π⦇NTMap⦈⦇a⦈ : w ↦⇘ℭ⇙ d"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    then show ?thesis by (intro exI)
  qed

  have "cf_parallel α (𝔞PL ?ww) (𝔟PL ?ww) ?ww w w (vid_on ?ww) ℭ"
    by (intro cat_cf_parallel_𝔞𝔟 π.cat_cone_obj cat_Hom_in_Vset) simp_all
  then have "⇑→⇑CF ℭ (𝔞PL ?ww) (𝔟PL ?ww) ?ww w w (vid_on ?ww) :
    ⇑C (𝔞PL ?ww) (𝔟PL ?ww) ?ww ↦↦C.tm⇘α⇙ ℭ"
    by (intro cf_parallel.cf_parallel_the_cf_parallel_is_tm_functor)
  from cat_small_complete[OF this] obtain ε v where ε: "ε :
    v <CF.lim ⇑→⇑CF ℭ (𝔞PL ?ww) (𝔟PL ?ww) ?ww w w (vid_on ?ww) :
    ⇑C (𝔞PL ?ww) (𝔟PL ?ww) ?ww ↦↦C⇘α⇙ ℭ"
    by clarsimp
  from is_cat_equalizerI[
      OF
        this
        _ 
        cat_Hom_in_Vset[OF π.cat_cone_obj π.cat_cone_obj]
        ww_neq_vempty
      ]
  interpret ε: is_cat_equalizer α w w ?ww ‹vid_on ?ww› ℭ v ε by auto
  note ε_is_monic_arr = 
    is_cat_equalizer.cat_eq_is_monic_arr[OF ε.is_cat_equalizer_axioms]
  note ε_is_monic_arrD = is_monic_arrD[OF ε_is_monic_arr]

  show ?thesis
  proof(rule, intro obj_initialI)

    show "v ∈∘ ℭ⦇Obj⦈" by (rule ε.cat_cone_obj)
    then have CId_v: "ℭ⦇CId⦈⦇v⦈ : v ↦⇘ℭ⇙ v" 
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)

    fix d assume prems: "d ∈∘ ℭ⦇Obj⦈"
    from wd[OF prems] obtain h where h: "h : w ↦⇘ℭ⇙ d" by auto

    show "∃!f. f : v ↦⇘ℭ⇙ d"
    proof(rule ex1I)
      define f where "f = h ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL ?ww⦈"
      from ε_is_monic_arrD(1) h show f: "f : v ↦⇘ℭ⇙ d"
        unfolding f_def by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      fix g assume prems': "g : v ↦⇘ℭ⇙ d"
      have "cf_parallel_2 α 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL v d g f ℭ"
        by (intro cat_cf_parallel_2_cat_equalizer prems' f)
      then have "↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL v d g f :
        ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL ↦↦C.tm⇘α⇙ ℭ"
        by (intro cf_parallel_2.cf_parallel_2_the_cf_parallel_2_is_tm_functor)
      from cat_small_complete[OF this] obtain ε' u 
        where "ε' :
          u <CF.lim ↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL v d g f :
          ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL ↦↦C⇘α⇙ ℭ"
        by clarsimp
      from is_cat_equalizer_2I[OF this prems' f] interpret ε': 
        is_cat_equalizer_2 α v d g f ℭ u ε'.
      note ε'_is_monic_arr = is_cat_equalizer_2.cat_eq_2_is_monic_arr[
        OF ε'.is_cat_equalizer_2_axioms
        ]
      note ε'_is_monic_arrD = is_monic_arrD[OF ε'_is_monic_arr]
      then have "u ∈∘ ℭ⦇Obj⦈" by auto
      from wd[OF this] obtain s where s: "s : w ↦⇘ℭ⇙ u" by clarsimp
      from s ε'_is_monic_arrD(1) ε_is_monic_arrD(1) have εε's:
        "ε⦇NTMap⦈⦇𝔞PL ?ww⦈ ∘A⇘ℭ⇙ ε'⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ s : w ↦⇘ℭ⇙ w"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      from s ε'_is_monic_arrD(1) ε_is_monic_arrD(1) have ε'sε:
        "ε'⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ s ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL ?ww⦈ : v ↦⇘ℭ⇙ v"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      from ε_is_monic_arrD(1) ε'_is_monic_arrD(1) s have 
        "ε⦇NTMap⦈⦇𝔞PL ?ww⦈ ∘A⇘ℭ⇙ (ε'⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ s ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL ?ww⦈) =
          ε⦇NTMap⦈⦇𝔞PL ?ww⦈ ∘A⇘ℭ⇙ ε'⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ s ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL ?ww⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      also from
        ε.cat_eq_Comp_eq
          [
            unfolded in_Hom_iff, OF cat_CId_is_arr[OF π.cat_cone_obj] εε's,
            symmetric
          ]
        εε's π.cat_cone_obj ε_is_monic_arr(1)
      have "… = ℭ⦇CId⦈⦇w⦈ ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL ?ww⦈"
        by (cs_prems cs_shallow cs_simp: vid_on_atI cs_intro:  cat_cs_intros)
      also from ε.cf_parallel_𝔞' ε_is_monic_arrD(1) have 
        "… = ε⦇NTMap⦈⦇𝔞PL ?ww⦈ ∘A⇘ℭ⇙ ℭ⦇CId⦈⦇v⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro:  cat_cs_intros)
      finally have
        "ε⦇NTMap⦈⦇𝔞PL ?ww⦈ ∘A⇘ℭ⇙ (ε'⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ s ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL ?ww⦈) =
          ε⦇NTMap⦈⦇𝔞PL ?ww⦈ ∘A⇘ℭ⇙ ℭ⦇CId⦈⦇v⦈".      
      from 
        is_monic_arrD(2)[OF ε_is_monic_arr ε'sε CId_v this] 
        ε'_is_monic_arrD(1) s ε_is_monic_arrD(1) 
      have ε'sε_is_CId: 
        "ε'⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ (s ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL ?ww⦈) = ℭ⦇CId⦈⦇v⦈"
        by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      have ε'_is_iso_arr: "ε'⦇NTMap⦈⦇𝔞PL2⦈ : u ↦iso⇘ℭ⇙ v"
        by 
        (
          intro 
            cat_is_iso_arr_if_is_monic_arr_is_right_inverse 
            ε'_is_monic_arr,
          rule is_right_inverseI[OF _ ε'_is_monic_arrD(1) ε'sε_is_CId]
        )
        (
          use s ε_is_monic_arrD(1) in 
            ‹cs_concl cs_shallow cs_intro: cat_cs_intros›
        )
      from ε'.cat_eq_2_Comp_eq(1) have 
        "g ∘A⇘ℭ⇙ ε'⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ (ε'⦇NTMap⦈⦇𝔞PL2⦈)¯C⇘ℭ⇙ =
          f ∘A⇘ℭ⇙ ε'⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ (ε'⦇NTMap⦈⦇𝔞PL2⦈)¯C⇘ℭ⇙"
        by simp      
      from this f ε'_is_monic_arrD(1) ε'_is_iso_arr prems' show "g = f"
        by
          (
            cs_prems cs_shallow
              cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_arrow_cs_intros
          )
    qed

  qed

qed

lemma (in cat_small_cocomplete) cat_sc_ex_obj_terminal:
  ―‹See Theorem 1 in Chapter V-6 in \cite{mac_lane_categories_2010}.›
  assumes "A ⊆∘ ℭ⦇Obj⦈"
    and "A ∈∘ Vset α"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ ∃f a. a ∈∘ A ∧ f : c ↦⇘ℭ⇙ a"
  obtains z where "obj_terminal ℭ z"
  using that 
  by 
    (
      rule cat_small_complete.cat_sc_ex_obj_initial[
        OF cat_small_complete_op, unfolded cat_op_simps, OF assms, simplified
        ]
    )


subsubsection‹Creation of limits, continuity and completeness›

lemma
  ―‹See Theorem 2 in Chapter V-4 in \cite{mac_lane_categories_2010}.›
  assumes "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔅"
    and "cat_small_complete α 𝔅"
    and "⋀𝔉 𝔍. 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ 𝔄 ⟹ 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ 𝔅"
    and "⋀𝔉 𝔍. 𝔉 : 𝔍 ↦↦C.tm⇘α⇙ 𝔄 ⟹ cf_creates_limits α 𝔊 𝔉"
  shows is_tm_cf_continuous_if_cf_creates_limits: "is_tm_cf_continuous α 𝔊"
    and cat_small_complete_if_cf_creates_limits: "cat_small_complete α 𝔄"
proof-

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

  show "is_tm_cf_continuous α 𝔊"
  proof(intro is_tm_cf_continuousI, rule assms)
    fix 𝔉 𝔍 assume prems: "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ 𝔄"
    then interpret 𝔉: is_tm_functor α 𝔍 𝔄 𝔉 .
    from cat_small_completeD(2)[OF assms(2) assms(3)[OF prems]] obtain ψ r
      where ψ: "ψ : r <CF.lim 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔅"
      by clarsimp
    show "cf_preserves_limits α 𝔊 𝔉"
      by 
        (
          rule cf_preserves_limits_if_cf_creates_limits, 
          rule assms(1),
          rule 𝔉.is_functor_axioms,
          rule ψ,
          rule assms(4)[OF prems]
        )
  qed

  show "cat_small_complete α 𝔄"
  proof(intro cat_small_completeI 𝔊.HomDom.category_axioms)
    fix 𝔉 𝔍 assume prems: "𝔉 : 𝔍 ↦↦C.tm⇘α⇙ 𝔄"
    then interpret 𝔉: is_tm_functor α 𝔍 𝔄 𝔉 .
    from cat_small_completeD(2)[OF assms(2) assms(3)[OF prems]] obtain ψ r
      where ψ: "ψ : r <CF.lim 𝔊 ∘CF 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔅"
      by clarsimp
    from cf_creates_limitsE''[
        OF assms(4)[OF prems] ψ 𝔉.is_functor_axioms assms(1)
        ]
    show "∃u r. u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ 𝔄"
      by metis
  qed

qed



subsection‹Finite-complete and finite-cocomplete category›

locale cat_finite_complete = category α ℭ for α ℭ + 
  assumes cat_finite_complete: 
    "⋀𝔉 𝔍. ⟦ finite_category α 𝔍; 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ ⟧ ⟹ 
      ∃u r. u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"

locale cat_finite_cocomplete = category α ℭ for α ℭ + 
  assumes cat_finite_cocomplete: 
    "⋀𝔉 𝔍. ⟦ finite_category α 𝔍; 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ ⟧ ⟹ 
      ∃u r. u : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ ℭ"


text‹Rules.›

mk_ide rf cat_finite_complete_def[unfolded cat_finite_complete_axioms_def]
  |intro cat_finite_completeI|
  |dest cat_finite_completeD[dest]|
  |elim cat_finite_completeE[elim]|

lemma cat_finite_completeE'[elim]:
  assumes "cat_finite_complete α ℭ" 
    and "finite_category α 𝔍" 
    and "𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  obtains u r where "u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  using assms by auto

mk_ide rf cat_finite_cocomplete_def[unfolded cat_finite_cocomplete_axioms_def]
  |intro cat_finite_cocompleteI|
  |dest cat_finite_cocompleteD[dest]|
  |elim cat_finite_cocompleteE[elim]|

lemma cat_finite_cocompleteE'[elim]:
  assumes "cat_finite_cocomplete α ℭ" 
    and "finite_category α 𝔍" 
    and "𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  obtains u r where "u : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ ℭ"
  using assms by auto


text‹Elementary properties.›

sublocale cat_small_complete ⊆ cat_finite_complete
proof(intro cat_finite_completeI)
  fix 𝔉 𝔍 assume prems: "finite_category α 𝔍" "𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  interpret 𝔉: is_functor α 𝔍 ℭ 𝔉 by (rule prems(2))
  from cat_small_complete_axioms show "∃u r. u : r <CF.lim 𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ" 
    by (auto intro: 𝔉.cf_is_tm_functor_if_HomDom_finite_category[OF prems(1)])
qed (auto intro: cat_cs_intros)

sublocale cat_small_cocomplete ⊆ cat_finite_cocomplete
proof(intro cat_finite_cocompleteI)
  fix 𝔉 𝔍 assume prems: "finite_category α 𝔍" "𝔉 : 𝔍 ↦↦C⇘α⇙ ℭ"
  interpret 𝔉: is_functor α 𝔍 ℭ 𝔉 by (rule prems(2))
  from cat_small_cocomplete_axioms show "∃u r. u : 𝔉 >CF.colim r : 𝔍 ↦↦C⇘α⇙ ℭ" 
    by (auto intro: 𝔉.cf_is_tm_functor_if_HomDom_finite_category[OF prems(1)])
qed (auto intro: cat_cs_intros)

text‹\newpage›

end