Session CZH_Universal_Constructions

Theory CZH_UCAT_Introduction

(* Copyright 2021 (C) Mihails Milehins *)

sectionβ€ΉIntroductionβ€Ί
theory CZH_UCAT_Introduction
  imports CZH_Elementary_Categories.CZH_ECAT_Introduction
begin

textβ€Ή
This article provides a formalization of further elements of the 
theory of 1-categories without an additional structure.
More specifically, this article explores canonical universal
constructions \cite{noauthor_nlab_nodate}\footnote{
\url{https://ncatlab.org/nlab/show/universal+construction}
} and their properties.
β€Ί

textβ€Ή\newpageβ€Ί

end

Theory CZH_UCAT_Universal

(* Copyright 2021 (C) Mihails Milehins *)

sectionβ€ΉUniversal arrowβ€Ί
theory CZH_UCAT_Universal
  imports 
    CZH_UCAT_Introduction
    CZH_Elementary_Categories.CZH_ECAT_FUNCT
    CZH_Elementary_Categories.CZH_ECAT_Set
    CZH_Elementary_Categories.CZH_ECAT_Hom
begin



subsectionβ€ΉBackgroundβ€Ί


textβ€Ή
The following section is based, primarily, on the elements of the content 
of Chapter III-1 in \cite{mac_lane_categories_2010}.
β€Ί



subsectionβ€ΉUniversal mapβ€Ί


textβ€Ή
The universal map is a convenience utility that allows treating 
a part of the definition of the universal arrow as an arrow in the
category β€ΉSetβ€Ί.
β€Ί


subsubsectionβ€ΉDefinition and elementary propertiesβ€Ί

definition umap_of :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V"
  where "umap_of 𝔉 c r u d =
    [
      (Ξ»f'∈∘Hom (𝔉⦇HomDom⦈) r d. 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘A𝔉⦇HomCod⦈ u),
      Hom (𝔉⦇HomDom⦈) r d,
      Hom (𝔉⦇HomCod⦈) c (𝔉⦇ObjMapβ¦ˆβ¦‡d⦈)
    ]∘"

definition umap_fo :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V"
  where "umap_fo 𝔉 c r u d = umap_of (op_cf 𝔉) c r u d"


textβ€ΉComponents.β€Ί

lemma (in is_functor) umap_of_components:
  assumes "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈" (*do not remove*)
  shows "umap_of 𝔉 c r u d⦇ArrVal⦈ = (Ξ»f'∈∘Hom 𝔄 r d. 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘A𝔅 u)"
    and "umap_of 𝔉 c r u d⦇ArrDom⦈ = Hom 𝔄 r d"
    and "umap_of 𝔉 c r u d⦇ArrCod⦈ = Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡d⦈)"
  unfolding umap_of_def arr_field_simps
  by (simp_all add: cat_cs_simps nat_omega_simps)

lemma (in is_functor) umap_fo_components:
  assumes "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c"
  shows "umap_fo 𝔉 c r u d⦇ArrVal⦈ = (Ξ»f'∈∘Hom 𝔄 d r. u ∘A𝔅 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈)"
    and "umap_fo 𝔉 c r u d⦇ArrDom⦈ = Hom 𝔄 d r"
    and "umap_fo 𝔉 c r u d⦇ArrCod⦈ = Hom 𝔅 (𝔉⦇ObjMapβ¦ˆβ¦‡d⦈) c"
  unfolding 
    umap_fo_def 
    is_functor.umap_of_components[
      OF is_functor_op, unfolded cat_op_simps, OF assms
      ] 
proof(rule vsv_eqI)
  fix f' assume "f' ∈∘ π’Ÿβˆ˜ (Ξ»f'∈∘Hom 𝔄 d r. 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘Aop_cat 𝔅 u)"
  then have f': "f' : d ↦𝔄 r" by simp
  then have 𝔉f': "𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ : 𝔉⦇ObjMapβ¦ˆβ¦‡d⦈ ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈" 
    by (auto intro: cat_cs_intros)
  from f' show 
    "(Ξ»f'∈∘Hom 𝔄 d r. 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘Aop_cat 𝔅 u)⦇f'⦈ = 
      (Ξ»f'∈∘Hom 𝔄 d r. u ∘A𝔅 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈)⦇f'⦈"
    by (simp add: HomCod.op_cat_Comp[OF assms 𝔉f'])
qed simp_all


textβ€ΉUniversal maps for the opposite functor.β€Ί

lemma (in is_functor) op_umap_of[cat_op_simps]: "umap_of (op_cf 𝔉) = umap_fo 𝔉"
  unfolding umap_fo_def by simp 

lemma (in is_functor) op_umap_fo[cat_op_simps]: "umap_fo (op_cf 𝔉) = umap_of 𝔉"
  unfolding umap_fo_def by (simp add: cat_op_simps)

lemmas [cat_op_simps] = 
  is_functor.op_umap_of
  is_functor.op_umap_fo


subsubsectionβ€ΉArrow valueβ€Ί

lemma umap_of_ArrVal_vsv[cat_cs_intros]: "vsv (umap_of 𝔉 c r u d⦇ArrVal⦈)"
  unfolding umap_of_def arr_field_simps by (simp add: nat_omega_simps)

lemma umap_fo_ArrVal_vsv[cat_cs_intros]: "vsv (umap_fo 𝔉 c r u d⦇ArrVal⦈)"
  unfolding umap_fo_def by (rule umap_of_ArrVal_vsv)

lemma (in is_functor) umap_of_ArrVal_vdomain: 
  assumes "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
  shows "π’Ÿβˆ˜ (umap_of 𝔉 c r u d⦇ArrVal⦈) = Hom 𝔄 r d"
  unfolding umap_of_components[OF assms] by simp

lemmas [cat_cs_simps] = is_functor.umap_of_ArrVal_vdomain

lemma (in is_functor) umap_fo_ArrVal_vdomain:
  assumes "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c"
  shows "π’Ÿβˆ˜ (umap_fo 𝔉 c r u d⦇ArrVal⦈) = Hom 𝔄 d r"
  unfolding umap_fo_components[OF assms] by simp

lemmas [cat_cs_simps] = is_functor.umap_fo_ArrVal_vdomain

lemma (in is_functor) umap_of_ArrVal_app: 
  assumes "f' : r ↦𝔄 d" and "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
  shows "umap_of 𝔉 c r u d⦇ArrValβ¦ˆβ¦‡f'⦈ = 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘A𝔅 u"
  using assms(1) unfolding umap_of_components[OF assms(2)] by simp

lemmas [cat_cs_simps] = is_functor.umap_of_ArrVal_app

lemma (in is_functor) umap_fo_ArrVal_app: 
  assumes "f' : d ↦𝔄 r" and "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c"
  shows "umap_fo 𝔉 c r u d⦇ArrValβ¦ˆβ¦‡f'⦈ = u ∘A𝔅 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈"
proof-
  from assms have "𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ : 𝔉⦇ObjMapβ¦ˆβ¦‡d⦈ ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈" 
    by (auto intro: cat_cs_intros)
  from this assms(2) have 𝔉f'[simp]:
    "𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘Aop_cat 𝔅 u = u ∘A𝔅 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈"
    by (simp add: cat_op_simps)
  from
    is_functor_axioms
    is_functor.umap_of_ArrVal_app[
      OF is_functor_op, unfolded cat_op_simps, 
      OF assms
      ] 
  show ?thesis
    by (simp add: cat_op_simps cat_cs_simps)
qed

lemmas [cat_cs_simps] = is_functor.umap_fo_ArrVal_app

lemma (in is_functor) umap_of_ArrVal_vrange: 
  assumes "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
  shows "β„›βˆ˜ (umap_of 𝔉 c r u d⦇ArrVal⦈) βŠ†βˆ˜ Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡d⦈)"
proof(intro vsubset_antisym vsubsetI)
  interpret vsv β€Ήumap_of 𝔉 c r u d⦇ArrValβ¦ˆβ€Ί 
    unfolding umap_of_components[OF assms] by simp
  fix g assume "g ∈∘ β„›βˆ˜ (umap_of 𝔉 c r u d⦇ArrVal⦈)"
  then obtain f' 
    where g_def: "g = umap_of 𝔉 c r u d⦇ArrValβ¦ˆβ¦‡f'⦈" 
      and f': "f' ∈∘ π’Ÿβˆ˜ (umap_of 𝔉 c r u d⦇ArrVal⦈)"
    unfolding umap_of_components[OF assms] by auto
  then have f': "f' : r ↦𝔄 d" 
    unfolding umap_of_ArrVal_vdomain[OF assms] by simp
  then have 𝔉f': "𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡d⦈" 
    by (auto intro!: cat_cs_intros)
  have g_def: "g = 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘A𝔅 u"
    unfolding g_def umap_of_ArrVal_app[OF f' assms]..
  from 𝔉f' assms show "g ∈∘ Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡d⦈)" 
    unfolding g_def by (auto intro: cat_cs_intros)
qed

lemma (in is_functor) umap_fo_ArrVal_vrange: 
  assumes "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c"
  shows "β„›βˆ˜ (umap_fo 𝔉 c r u d⦇ArrVal⦈) βŠ†βˆ˜ Hom 𝔅 (𝔉⦇ObjMapβ¦ˆβ¦‡d⦈) c"
  by 
    (
      rule is_functor.umap_of_ArrVal_vrange[
        OF is_functor_op, unfolded cat_op_simps, OF assms, folded umap_fo_def
        ]
    )


subsubsectionβ€ΉUniversal map is an arrow in the category β€ΉSetβ€Ίβ€Ί

lemma (in is_functor) cf_arr_Set_umap_of: 
  assumes "category Ξ± 𝔄" 
    and "category Ξ± 𝔅" 
    and r: "r ∈∘ 𝔄⦇Obj⦈" 
    and d: "d ∈∘ 𝔄⦇Obj⦈"
    and u: "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
  shows "arr_Set Ξ± (umap_of 𝔉 c r u d)"
proof(intro arr_SetI)
  interpret HomDom: category Ξ± 𝔄 by (rule assms(1))
  interpret HomCod: category Ξ± 𝔅 by (rule assms(2))
  note umap_of_components = umap_of_components[OF u]
  from u d have c: "c ∈∘ 𝔅⦇Obj⦈" and 𝔉d: "(𝔉⦇ObjMapβ¦ˆβ¦‡d⦈) ∈∘ 𝔅⦇Obj⦈" 
    by (auto intro: cat_cs_intros)
  show "vfsequence (umap_of 𝔉 c r u d)" unfolding umap_of_def by simp
  show "vcard (umap_of 𝔉 c r u d) = 3β„•"
    unfolding umap_of_def by (simp add: nat_omega_simps)
  from umap_of_ArrVal_vrange[OF u] show 
    "β„›βˆ˜ (umap_of 𝔉 c r u d⦇ArrVal⦈) βŠ†βˆ˜ umap_of 𝔉 c r u d⦇ArrCod⦈"
    unfolding umap_of_components by simp
  from r d show "umap_of 𝔉 c r u d⦇ArrDom⦈ ∈∘ Vset Ξ±"
    unfolding umap_of_components by (intro HomDom.cat_Hom_in_Vset)
  from c 𝔉d show "umap_of 𝔉 c r u d⦇ArrCod⦈ ∈∘ Vset Ξ±"
    unfolding umap_of_components by (intro HomCod.cat_Hom_in_Vset)
qed (auto simp: umap_of_components[OF u])

lemma (in is_functor) cf_arr_Set_umap_fo: 
  assumes "category Ξ± 𝔄" 
    and "category Ξ± 𝔅" 
    and r: "r ∈∘ 𝔄⦇Obj⦈" 
    and d: "d ∈∘ 𝔄⦇Obj⦈"
    and u: "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c"
  shows "arr_Set Ξ± (umap_fo 𝔉 c r u d)"
proof-
  from assms(1) have 𝔄: "category Ξ± (op_cat 𝔄)" 
    by (auto intro: cat_cs_intros)
  from assms(2) have 𝔅: "category Ξ± (op_cat 𝔅)" 
    by (auto intro: cat_cs_intros)
  show ?thesis
    by 
      (
        rule 
          is_functor.cf_arr_Set_umap_of[
            OF is_functor_op, unfolded cat_op_simps, OF 𝔄 𝔅 r d u
            ]
      )
qed

lemma (in is_functor) cf_umap_of_is_arr:
  assumes "category Ξ± 𝔄" 
    and "category Ξ± 𝔅" 
    and "r ∈∘ 𝔄⦇Obj⦈" 
    and "d ∈∘ 𝔄⦇Obj⦈"
    and "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
  shows "umap_of 𝔉 c r u d : Hom 𝔄 r d ↦cat_Set Ξ± Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡d⦈)"
proof(intro cat_Set_is_arrI)
  show "arr_Set Ξ± (umap_of 𝔉 c r u d)" 
    by (rule cf_arr_Set_umap_of[OF assms])
qed (simp_all add: umap_of_components[OF assms(5)])

lemma (in is_functor) cf_umap_of_is_arr':
  assumes "category Ξ± 𝔄" 
    and "category Ξ± 𝔅" 
    and "r ∈∘ 𝔄⦇Obj⦈" 
    and "d ∈∘ 𝔄⦇Obj⦈"
    and "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
    and "A = Hom 𝔄 r d"
    and "B = Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡d⦈)"
    and "β„­ = cat_Set Ξ±"
  shows "umap_of 𝔉 c r u d : A ↦ℭ B"
  using assms(1-5) unfolding assms(6-8) by (rule cf_umap_of_is_arr)

lemmas [cat_cs_intros] = is_functor.cf_umap_of_is_arr'

lemma (in is_functor) cf_umap_fo_is_arr:
  assumes "category Ξ± 𝔄" 
    and "category Ξ± 𝔅" 
    and "r ∈∘ 𝔄⦇Obj⦈" 
    and "d ∈∘ 𝔄⦇Obj⦈"
    and "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c"
  shows "umap_fo 𝔉 c r u d : Hom 𝔄 d r ↦cat_Set Ξ± Hom 𝔅 (𝔉⦇ObjMapβ¦ˆβ¦‡d⦈) c"
proof(intro cat_Set_is_arrI)
  show "arr_Set Ξ± (umap_fo 𝔉 c r u d)" 
    by (rule cf_arr_Set_umap_fo[OF assms])
qed (simp_all add: umap_fo_components[OF assms(5)])

lemma (in is_functor) cf_umap_fo_is_arr':
  assumes "category Ξ± 𝔄" 
    and "category Ξ± 𝔅" 
    and "r ∈∘ 𝔄⦇Obj⦈" 
    and "d ∈∘ 𝔄⦇Obj⦈"
    and "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c"
    and "A = Hom 𝔄 d r"
    and "B = Hom 𝔅 (𝔉⦇ObjMapβ¦ˆβ¦‡d⦈) c"
    and "β„­ = cat_Set Ξ±"
  shows "umap_fo 𝔉 c r u d : A ↦ℭ B"
  using assms(1-5) unfolding assms(6-8) by (rule cf_umap_fo_is_arr)

lemmas [cat_cs_intros] = is_functor.cf_umap_fo_is_arr'



subsectionβ€ΉUniversal arrow: definition and elementary propertiesβ€Ί


textβ€ΉSee Chapter III-1 in \cite{mac_lane_categories_2010}.β€Ί

definition universal_arrow_of :: "V β‡’ V β‡’ V β‡’ V β‡’ bool"
  where "universal_arrow_of 𝔉 c r u ⟷
    (
      r ∈∘ 𝔉⦇HomDomβ¦ˆβ¦‡Obj⦈ ∧
      u : c ↦𝔉⦇HomCod⦈ 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ∧
      (
        βˆ€r' u'.
          r' ∈∘ 𝔉⦇HomDomβ¦ˆβ¦‡Obj⦈ ⟢
          u' : c ↦𝔉⦇HomCod⦈ 𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈ ⟢
          (βˆƒ!f'. f' : r ↦𝔉⦇HomDom⦈ r' ∧ u' = umap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f'⦈)
      )
    )"

definition universal_arrow_fo :: "V β‡’ V β‡’ V β‡’ V β‡’ bool"
  where "universal_arrow_fo 𝔉 c r u ≑ universal_arrow_of (op_cf 𝔉) c r u"


textβ€ΉRules.β€Ί

mk_ide (in is_functor) rf 
  universal_arrow_of_def[where 𝔉=𝔉, unfolded cf_HomDom cf_HomCod]
  |intro universal_arrow_ofI|
  |dest universal_arrow_ofD[dest]|
  |elim universal_arrow_ofE[elim]|

lemma (in is_functor) universal_arrow_foI:
  assumes "r ∈∘ 𝔄⦇Obj⦈" 
    and "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c" 
    and "β‹€r' u'. ⟦ r' ∈∘ 𝔄⦇Obj⦈; u' : 𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈ ↦𝔅 c ⟧ ⟹ 
      βˆƒ!f'. f' : r' ↦𝔄 r ∧ u' = umap_fo 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f'⦈"
  shows "universal_arrow_fo 𝔉 c r u"
  by 
    (
      simp add: 
        is_functor.universal_arrow_ofI
          [
            OF is_functor_op, 
            folded universal_arrow_fo_def, 
            unfolded cat_op_simps, 
            OF assms
          ]
    )

lemma (in is_functor) universal_arrow_foD[dest]:
  assumes "universal_arrow_fo 𝔉 c r u"
  shows "r ∈∘ 𝔄⦇Obj⦈" 
    and "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c" 
    and "β‹€r' u'. ⟦ r' ∈∘ 𝔄⦇Obj⦈; u' : 𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈ ↦𝔅 c ⟧ ⟹ 
      βˆƒ!f'. f' : r' ↦𝔄 r ∧ u' = umap_fo 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f'⦈"
  by
    (
      auto simp: 
        is_functor.universal_arrow_ofD
          [
            OF is_functor_op, 
            folded universal_arrow_fo_def, 
            unfolded cat_op_simps,
            OF assms
          ]
    )

lemma (in is_functor) universal_arrow_foE[elim]:
  assumes "universal_arrow_fo 𝔉 c r u"
  obtains "r ∈∘ 𝔄⦇Obj⦈" 
    and "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c" 
    and "β‹€r' u'. ⟦ r' ∈∘ 𝔄⦇Obj⦈; u' : 𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈ ↦𝔅 c ⟧ ⟹ 
      βˆƒ!f'. f' : r' ↦𝔄 r ∧ u' = umap_fo 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f'⦈"
  using assms by (auto simp: universal_arrow_foD)


textβ€ΉElementary properties.β€Ί

lemma (in is_functor) op_cf_universal_arrow_of[cat_op_simps]: 
  "universal_arrow_of (op_cf 𝔉) c r u ⟷ universal_arrow_fo 𝔉 c r u"
  unfolding universal_arrow_fo_def ..

lemma (in is_functor) op_cf_universal_arrow_fo[cat_op_simps]: 
  "universal_arrow_fo (op_cf 𝔉) c r u ⟷ universal_arrow_of 𝔉 c r u"
  unfolding universal_arrow_fo_def cat_op_simps ..

lemmas (in is_functor) [cat_op_simps] = 
  is_functor.op_cf_universal_arrow_of
  is_functor.op_cf_universal_arrow_fo



subsectionβ€ΉUniquenessβ€Ί


textβ€Ή
The following properties are related to the uniqueness of the 
universal arrow. These properties can be inferred from the content of
Chapter III-1 in \cite{mac_lane_categories_2010}.
β€Ί

lemma (in is_functor) cf_universal_arrow_of_ex_is_arr_isomorphism:
  ―‹The proof is based on the ideas expressed in the proof of Theorem 5.2 
  in Chapter Introduction in \cite{hungerford_algebra_2003}.β€Ί
  assumes "universal_arrow_of 𝔉 c r u" and "universal_arrow_of 𝔉 c r' u'"
  obtains f where "f : r ↦iso𝔄 r'" and "u' = umap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f⦈"
proof-

  note ua1 = universal_arrow_ofD[OF assms(1)]
  note ua2 = universal_arrow_ofD[OF assms(2)]

  from ua1(1) have 𝔄r: "𝔄⦇CIdβ¦ˆβ¦‡r⦈ : r ↦𝔄 r" by (auto intro: cat_cs_intros)
  from ua1(1) have "𝔉⦇ArrMapβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈ = 𝔅⦇CIdβ¦ˆβ¦‡π”‰β¦‡ObjMapβ¦ˆβ¦‡r⦈⦈"
    by (auto intro: cat_cs_intros)
  with ua1(1,2) have u_def: "u = umap_of 𝔉 c r u r⦇ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈"
    unfolding umap_of_ArrVal_app[OF 𝔄r ua1(2)] by (auto simp: cat_cs_simps)

  from ua2(1) have 𝔄r': "𝔄⦇CIdβ¦ˆβ¦‡r'⦈ : r' ↦𝔄 r'" by (auto intro: cat_cs_intros)
  from ua2(1) have "𝔉⦇ArrMapβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r'⦈⦈ = 𝔅⦇CIdβ¦ˆβ¦‡π”‰β¦‡ObjMapβ¦ˆβ¦‡r'⦈⦈" 
    by (auto intro: cat_cs_intros)
  with ua2(1,2) have u'_def: "u' = umap_of 𝔉 c r' u' r'⦇ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r'⦈⦈"
    unfolding umap_of_ArrVal_app[OF 𝔄r' ua2(2)] by (auto simp: cat_cs_simps)

  from 𝔄r u_def universal_arrow_ofD(3)[OF assms(1) ua1(1,2)] have eq_CId_rI: 
    "⟦ f' : r ↦𝔄 r; u = umap_of 𝔉 c r u r⦇ArrValβ¦ˆβ¦‡f'⦈ ⟧ ⟹ f' = 𝔄⦇CIdβ¦ˆβ¦‡r⦈" 
    for f'
    by blast
  from 𝔄r' u'_def universal_arrow_ofD(3)[OF assms(2) ua2(1,2)] have eq_CId_r'I: 
    "⟦ f' : r' ↦𝔄 r'; u' = umap_of 𝔉 c r' u' r'⦇ArrValβ¦ˆβ¦‡f'⦈ ⟧ ⟹
      f' = 𝔄⦇CIdβ¦ˆβ¦‡r'⦈" 
    for f'
    by blast

  from ua1(3)[OF ua2(1,2)] obtain f 
    where f: "f : r ↦𝔄 r'" 
      and u'_def: "u' = umap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f⦈"
      and "g : r ↦𝔄 r' ⟹ u' = umap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡g⦈ ⟹ f = g" 
    for g
    by metis
  from ua2(3)[OF ua1(1,2)] obtain f' 
    where f': "f' : r' ↦𝔄 r" 
      and u_def: "u = umap_of 𝔉 c r' u' r⦇ArrValβ¦ˆβ¦‡f'⦈"
      and "g : r' ↦𝔄 r ⟹ u = umap_of 𝔉 c r' u' r⦇ArrValβ¦ˆβ¦‡g⦈ ⟹ f' = g" 
    for g
    by metis

  have "f : r ↦iso𝔄 r'"
  proof(intro is_arr_isomorphismI is_inverseI)
    show f: "f : r ↦𝔄 r'" by (rule f)
    show f': "f' : r' ↦𝔄 r" by (rule f')
    show "f : r ↦𝔄 r'" by (rule f)
    from f' have 𝔉f': "𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ : 𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈ ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈" 
      by (auto intro: cat_cs_intros)
    from f have 𝔉f: "𝔉⦇ArrMapβ¦ˆβ¦‡f⦈ : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈" 
      by (auto intro: cat_cs_intros)
    note u'_def' = u'_def[symmetric, unfolded umap_of_ArrVal_app[OF f ua1(2)]] 
      and u_def' = u_def[symmetric, unfolded umap_of_ArrVal_app[OF f' ua2(2)]]
    show "f' ∘A𝔄 f = 𝔄⦇CIdβ¦ˆβ¦‡r⦈"
    proof(rule eq_CId_rI)
      from f f' show f'f: "f' ∘A𝔄 f : r ↦𝔄 r" 
        by (auto intro: cat_cs_intros)
      from ua1(2) 𝔉f' 𝔉f show "u = umap_of 𝔉 c r u r⦇ArrValβ¦ˆβ¦‡f' ∘A𝔄 f⦈"
        unfolding umap_of_ArrVal_app[OF f'f ua1(2)] cf_ArrMap_Comp[OF f' f]
        by (simp add: HomCod.cat_Comp_assoc u'_def' u_def')
    qed
    show "f ∘A𝔄 f' = 𝔄⦇CIdβ¦ˆβ¦‡r'⦈"
    proof(rule eq_CId_r'I)
      from f f' show ff': "f ∘A𝔄 f' : r' ↦𝔄 r'" 
        by (auto intro: cat_cs_intros)
      from ua2(2) 𝔉f' 𝔉f show "u' = umap_of 𝔉 c r' u' r'⦇ArrValβ¦ˆβ¦‡f ∘A𝔄 f'⦈"
        unfolding umap_of_ArrVal_app[OF ff' ua2(2)] cf_ArrMap_Comp[OF f f']
        by (simp add: HomCod.cat_Comp_assoc u'_def' u_def')
    qed
  qed
  
  with u'_def that show ?thesis by auto

qed

lemma (in is_functor) cf_universal_arrow_fo_ex_is_arr_isomorphism:
  assumes "universal_arrow_fo 𝔉 c r u"
    and "universal_arrow_fo 𝔉 c r' u'"
  obtains f where "f : r' ↦iso𝔄 r" and "u' = umap_fo 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f⦈"
  by 
    (
      elim 
        is_functor.cf_universal_arrow_of_ex_is_arr_isomorphism[
          OF is_functor_op, unfolded cat_op_simps, OF assms
          ]
    )

lemma (in is_functor) cf_universal_arrow_of_unique:
  assumes "universal_arrow_of 𝔉 c r u"
    and "universal_arrow_of 𝔉 c r' u'"
  shows "βˆƒ!f'. f' : r ↦𝔄 r' ∧ u' = umap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f'⦈"
proof-
  note ua1 = universal_arrow_ofD[OF assms(1)]
  note ua2 = universal_arrow_ofD[OF assms(2)]
  from ua1(3)[OF ua2(1,2)] show ?thesis .
qed

lemma (in is_functor) cf_universal_arrow_fo_unique:
  assumes "universal_arrow_fo 𝔉 c r u"
    and "universal_arrow_fo 𝔉 c r' u'"
  shows "βˆƒ!f'. f' : r' ↦𝔄 r ∧ u' = umap_fo 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f'⦈"
proof-
  note ua1 = universal_arrow_foD[OF assms(1)]
  note ua2 = universal_arrow_foD[OF assms(2)]
  from ua1(3)[OF ua2(1,2)] show ?thesis .
qed

lemma (in is_functor) cf_universal_arrow_of_is_arr_isomorphism:
  assumes "universal_arrow_of 𝔉 c r u"
    and "universal_arrow_of 𝔉 c r' u'"
    and "f : r ↦𝔄 r'" 
    and "u' = umap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f⦈"
  shows "f : r ↦iso𝔄 r'"
proof-
  from assms(3,4) cf_universal_arrow_of_unique[OF assms(1,2)] have eq: 
    "g : r ↦𝔄 r' ⟹ u' = umap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡g⦈ ⟹ f = g" for g
    by blast
  from assms(1,2) obtain f' 
    where iso_f': "f' : r ↦iso𝔄 r'" 
      and u'_def: "u' = umap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f'⦈"
    by (auto elim: cf_universal_arrow_of_ex_is_arr_isomorphism)
  then have f': "f' : r ↦𝔄 r'" by auto
  from iso_f' show ?thesis unfolding eq[OF f' u'_def, symmetric].
qed

lemma (in is_functor) cf_universal_arrow_fo_is_arr_isomorphism:
  assumes "universal_arrow_fo 𝔉 c r u"
    and "universal_arrow_fo 𝔉 c r' u'"
    and "f : r' ↦𝔄 r" 
    and "u' = umap_fo 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f⦈"
  shows "f : r' ↦iso𝔄 r"
  by 
    (
      rule 
        is_functor.cf_universal_arrow_of_is_arr_isomorphism[
          OF is_functor_op, unfolded cat_op_simps, OF assms
          ]
    )



subsectionβ€ΉUniversal natural transformationβ€Ί


subsubsectionβ€ΉDefinition and elementary propertiesβ€Ί


textβ€Ή
The concept of the universal natural transformation is introduced for the 
statement of the elements of a variant of Proposition 1 in Chapter III-2
in \cite{mac_lane_categories_2010}.
β€Ί

definition ntcf_ua_of :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V"
  where "ntcf_ua_of Ξ± 𝔉 c r u =
    [
      (Ξ»dβˆˆβˆ˜π”‰β¦‡HomDomβ¦ˆβ¦‡Obj⦈. umap_of 𝔉 c r u d),
      HomO.Cα𝔉⦇HomDom⦈(r,-),
      HomO.Cα𝔉⦇HomCod⦈(c,-) ∘CF 𝔉,
      𝔉⦇HomDom⦈,
      cat_Set Ξ±
    ]∘"

definition ntcf_ua_fo :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V"
  where "ntcf_ua_fo Ξ± 𝔉 c r u = ntcf_ua_of Ξ± (op_cf 𝔉) c r u"


textβ€ΉComponents.β€Ί

lemma ntcf_ua_of_components:
  shows "ntcf_ua_of Ξ± 𝔉 c r u⦇NTMap⦈ = (Ξ»dβˆˆβˆ˜π”‰β¦‡HomDomβ¦ˆβ¦‡Obj⦈. umap_of 𝔉 c r u d)"
    and "ntcf_ua_of Ξ± 𝔉 c r u⦇NTDom⦈ = HomO.Cα𝔉⦇HomDom⦈(r,-)"
    and "ntcf_ua_of Ξ± 𝔉 c r u⦇NTCod⦈ = HomO.Cα𝔉⦇HomCod⦈(c,-) ∘CF 𝔉"
    and "ntcf_ua_of Ξ± 𝔉 c r u⦇NTDGDom⦈ = 𝔉⦇HomDom⦈"
    and "ntcf_ua_of Ξ± 𝔉 c r u⦇NTDGCod⦈ = cat_Set Ξ±"
  unfolding ntcf_ua_of_def nt_field_simps by (simp_all add: nat_omega_simps) 

lemma ntcf_ua_fo_components:
  shows "ntcf_ua_fo Ξ± 𝔉 c r u⦇NTMap⦈ = (Ξ»dβˆˆβˆ˜π”‰β¦‡HomDomβ¦ˆβ¦‡Obj⦈. umap_fo 𝔉 c r u d)"
    and "ntcf_ua_fo Ξ± 𝔉 c r u⦇NTDom⦈ = HomO.CΞ±op_cat (𝔉⦇HomDom⦈)(r,-)"
    and "ntcf_ua_fo Ξ± 𝔉 c r u⦇NTCod⦈ =
      HomO.CΞ±op_cat (𝔉⦇HomCod⦈)(c,-) ∘CF op_cf 𝔉"
    and "ntcf_ua_fo Ξ± 𝔉 c r u⦇NTDGDom⦈ = op_cat (𝔉⦇HomDom⦈)"
    and "ntcf_ua_fo Ξ± 𝔉 c r u⦇NTDGCod⦈ = cat_Set Ξ±"
  unfolding ntcf_ua_fo_def ntcf_ua_of_components umap_fo_def cat_op_simps 
  by simp_all

context is_functor
begin

lemmas ntcf_ua_of_components' = 
  ntcf_ua_of_components[where Ξ±=Ξ± and 𝔉=𝔉, unfolded cat_cs_simps]

lemmas [cat_cs_simps] = ntcf_ua_of_components'(2-5)

lemma ntcf_ua_fo_components':
  assumes "c ∈∘ 𝔅⦇Obj⦈" and "r ∈∘ 𝔄⦇Obj⦈" 
  shows "ntcf_ua_fo Ξ± 𝔉 c r u⦇NTMap⦈ = (Ξ»dβˆˆβˆ˜π”„β¦‡Obj⦈. umap_fo 𝔉 c r u d)"
    and [cat_cs_simps]: 
      "ntcf_ua_fo Ξ± 𝔉 c r u⦇NTDom⦈ = HomO.Cα𝔄(-,r)"
    and [cat_cs_simps]: 
      "ntcf_ua_fo Ξ± 𝔉 c r u⦇NTCod⦈ = HomO.Cα𝔅(-,c) ∘CF op_cf 𝔉"
    and [cat_cs_simps]: "ntcf_ua_fo Ξ± 𝔉 c r u⦇NTDGDom⦈ = op_cat 𝔄"
    and [cat_cs_simps]: "ntcf_ua_fo Ξ± 𝔉 c r u⦇NTDGCod⦈ = cat_Set Ξ±"
  unfolding
    ntcf_ua_fo_components cat_cs_simps
    HomDom.cat_op_cat_cf_Hom_snd[OF assms(2)] 
    HomCod.cat_op_cat_cf_Hom_snd[OF assms(1)]
  by simp_all

end

lemmas [cat_cs_simps] = 
  is_functor.ntcf_ua_of_components'(2-5)
  is_functor.ntcf_ua_fo_components'(2-5)


subsubsectionβ€ΉNatural transformation mapβ€Ί

mk_VLambda (in is_functor) 
  ntcf_ua_of_components(1)[where Ξ±=Ξ± and 𝔉=𝔉, unfolded cf_HomDom]
  |vsv ntcf_ua_of_NTMap_vsv|
  |vdomain ntcf_ua_of_NTMap_vdomain|
  |app ntcf_ua_of_NTMap_app|

context is_functor
begin

context
  fixes c r
  assumes r: "r ∈∘ 𝔄⦇Obj⦈" and c: "c ∈∘ 𝔅⦇Obj⦈" 
begin

mk_VLambda ntcf_ua_fo_components'(1)[OF c r]
  |vsv ntcf_ua_fo_NTMap_vsv|
  |vdomain ntcf_ua_fo_NTMap_vdomain|
  |app ntcf_ua_fo_NTMap_app|

end

end

lemmas [cat_cs_intros] = 
  is_functor.ntcf_ua_fo_NTMap_vsv
  is_functor.ntcf_ua_of_NTMap_vsv

lemmas [cat_cs_simps] = 
  is_functor.ntcf_ua_fo_NTMap_vdomain
  is_functor.ntcf_ua_fo_NTMap_app
  is_functor.ntcf_ua_of_NTMap_vdomain
  is_functor.ntcf_ua_of_NTMap_app

lemma (in is_functor) ntcf_ua_of_NTMap_vrange:
  assumes "category Ξ± 𝔄" 
    and "category Ξ± 𝔅" 
    and "r ∈∘ 𝔄⦇Obj⦈" 
    and "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
  shows "β„›βˆ˜ (ntcf_ua_of Ξ± 𝔉 c r u⦇NTMap⦈) βŠ†βˆ˜ cat_Set α⦇Arr⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold ntcf_ua_of_NTMap_vdomain)
  show "vsv (ntcf_ua_of Ξ± 𝔉 c r u⦇NTMap⦈)" by (rule ntcf_ua_of_NTMap_vsv)
  fix d assume prems: "d ∈∘ 𝔄⦇Obj⦈"
  with category_cat_Set is_functor_axioms assms show 
    "ntcf_ua_of Ξ± 𝔉 c r u⦇NTMapβ¦ˆβ¦‡d⦈ ∈∘ cat_Set α⦇Arr⦈"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed


subsubsectionβ€ΉCommutativity of the universal maps and β€Ήhomβ€Ί-functionsβ€Ί

lemma (in is_functor) cf_umap_of_cf_hom_commute: 
  assumes "category Ξ± 𝔄"
    and "category Ξ± 𝔅"
    and "c ∈∘ 𝔅⦇Obj⦈"
    and "r ∈∘ 𝔄⦇Obj⦈"
    and "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
    and "f : a ↦𝔄 b"
  shows 
    "umap_of 𝔉 c r u b ∘Acat_Set Ξ± cf_hom 𝔄 [𝔄⦇CIdβ¦ˆβ¦‡r⦈, f]∘ =
      cf_hom 𝔅 [𝔅⦇CIdβ¦ˆβ¦‡c⦈, 𝔉⦇ArrMapβ¦ˆβ¦‡f⦈]∘ ∘Acat_Set Ξ± umap_of 𝔉 c r u a"
  (is β€Ή?uof_b ∘Acat_Set Ξ± ?rf = ?cf ∘Acat_Set Ξ± ?uof_aβ€Ί)
proof-

  from is_functor_axioms category_cat_Set assms(1,2,4-6) have b_rf: 
    "?uof_b ∘Acat_Set Ξ± ?rf : Hom 𝔄 r a ↦cat_Set Ξ± Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡b⦈)"
    by (cs_concl cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros)
  from is_functor_axioms category_cat_Set assms(1,2,4-6) have cf_a: 
    "?cf ∘Acat_Set Ξ± ?uof_a : Hom 𝔄 r a ↦cat_Set Ξ± Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡b⦈)"
    by (cs_concl cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros)

  show ?thesis
  proof(rule arr_Set_eqI[of Ξ±])
    from b_rf show arr_Set_b_rf: "arr_Set α (?uof_b ∘Acat_Set α ?rf)"
      by (auto dest: cat_Set_is_arrD(1))
    from b_rf have dom_lhs: 
      "π’Ÿβˆ˜ ((?uof_b ∘Acat_Set Ξ± ?rf)⦇ArrVal⦈) = Hom 𝔄 r a"
      by (cs_concl cs_simp: cat_cs_simps)+
    from cf_a show arr_Set_cf_a: "arr_Set α (?cf ∘Acat_Set α ?uof_a)"
      by (auto dest: cat_Set_is_arrD(1))
    from cf_a have dom_rhs: 
      "π’Ÿβˆ˜ ((?cf ∘Acat_Set Ξ± ?uof_a)⦇ArrVal⦈) = Hom 𝔄 r a"
      by (cs_concl cs_simp: cat_cs_simps)
    show "(?uof_b ∘Acat_Set Ξ± ?rf)⦇ArrVal⦈ = (?cf ∘Acat_Set Ξ± ?uof_a)⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
      fix q assume "q : r ↦𝔄 a"
      with is_functor_axioms category_cat_Set assms show 
        "(?uof_b ∘Acat_Set Ξ± ?rf)⦇ArrValβ¦ˆβ¦‡q⦈ =
          (?cf ∘Acat_Set Ξ± ?uof_a)⦇ArrValβ¦ˆβ¦‡q⦈"
        by (*slow*)
          (
            cs_concl
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
         )
    qed (use arr_Set_b_rf arr_Set_cf_a in auto)
  
  qed (use b_rf cf_a in β€Ήcs_concl cs_simp: cat_cs_simpsβ€Ί)+

qed

lemma cf_umap_of_cf_hom_unit_commute:
  assumes "category Ξ± β„­"
    and "category Ξ± 𝔇"
    and "𝔉 : β„­ ↦↦CΞ± 𝔇"
    and "π”Š : 𝔇 ↦↦CΞ± β„­"
    and "Ξ· : cf_id β„­ ↦CF π”Š ∘CF 𝔉 : β„­ ↦↦CΞ± β„­"
    and "g : c' ↦ℭ c" 
    and "f : d ↦𝔇 d'"
  shows 
    "umap_of π”Š c' (𝔉⦇ObjMapβ¦ˆβ¦‡c'⦈) (η⦇NTMapβ¦ˆβ¦‡c'⦈) d' ∘Acat_Set Ξ±
      cf_hom 𝔇 [𝔉⦇ArrMapβ¦ˆβ¦‡g⦈, f]∘ =
        cf_hom β„­ [g, π”Šβ¦‡ArrMapβ¦ˆβ¦‡f⦈]∘ ∘Acat_Set Ξ±
          umap_of π”Š c (𝔉⦇ObjMapβ¦ˆβ¦‡c⦈) (η⦇NTMapβ¦ˆβ¦‡c⦈) d"
  (is β€Ή?uof_c'd' ∘Acat_Set Ξ± ?𝔉gf = ?gπ”Šf ∘Acat_Set Ξ± ?uof_cdβ€Ί)
proof-

  interpret Ξ·: is_ntcf Ξ± β„­ β„­ β€Ήcf_id β„­β€Ί β€Ήπ”Š ∘CF 𝔉› Ξ· by (rule assms(5))

  from assms have c'd'_𝔉gf: "?uof_c'd' ∘Acat_Set Ξ± ?𝔉gf :
    Hom 𝔇 (𝔉⦇ObjMapβ¦ˆβ¦‡c⦈) d ↦cat_Set Ξ± Hom β„­ c' (π”Šβ¦‡ObjMapβ¦ˆβ¦‡d'⦈)"
    by
      (
        cs_concl
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
      )
  then have dom_lhs:
    "π’Ÿβˆ˜ ((?uof_c'd' ∘Acat_Set Ξ± ?𝔉gf)⦇ArrVal⦈) = Hom 𝔇 (𝔉⦇ObjMapβ¦ˆβ¦‡c⦈) d"
    by (cs_concl cs_simp: cat_cs_simps)
  from assms have gπ”Šf_cd: "?gπ”Šf ∘Acat_Set Ξ± ?uof_cd :
    Hom 𝔇 (𝔉⦇ObjMapβ¦ˆβ¦‡c⦈) d ↦cat_Set Ξ± Hom β„­ c' (π”Šβ¦‡ObjMapβ¦ˆβ¦‡d'⦈)"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
      )
  then have dom_rhs: 
    "π’Ÿβˆ˜ ((?gπ”Šf ∘Acat_Set Ξ± ?uof_cd)⦇ArrVal⦈) = Hom 𝔇 (𝔉⦇ObjMapβ¦ˆβ¦‡c⦈) d"
    by (cs_concl cs_simp: cat_cs_simps)

  show ?thesis
  proof(rule arr_Set_eqI[of Ξ±])
    from c'd'_𝔉gf show arr_Set_c'd'_𝔉gf: 
      "arr_Set Ξ± (?uof_c'd' ∘Acat_Set Ξ± ?𝔉gf)"
      by (auto dest: cat_Set_is_arrD(1))
    from gπ”Šf_cd show arr_Set_gπ”Šf_cd:
      "arr_Set Ξ± (?gπ”Šf ∘Acat_Set Ξ± ?uof_cd)"
      by (auto dest: cat_Set_is_arrD(1))
    show 
      "(?uof_c'd' ∘Acat_Set Ξ± ?𝔉gf)⦇ArrVal⦈ =
        (?gπ”Šf ∘Acat_Set Ξ± ?uof_cd)⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
      fix h assume prems: "h : 𝔉⦇ObjMapβ¦ˆβ¦‡c⦈ ↦𝔇 d"
      from Ξ·.ntcf_Comp_commute[OF assms(6)] assms have [cat_cs_simps]:
        "η⦇NTMapβ¦ˆβ¦‡c⦈ ∘Aβ„­ g = π”Šβ¦‡ArrMapβ¦ˆβ¦‡π”‰β¦‡ArrMapβ¦ˆβ¦‡g⦈⦈ ∘Aβ„­ η⦇NTMapβ¦ˆβ¦‡c'⦈"
        by (cs_prems cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros)
      from assms prems show 
        "(?uof_c'd' ∘Acat_Set Ξ± ?𝔉gf)⦇ArrValβ¦ˆβ¦‡h⦈ =
          (?gπ”Šf ∘Acat_Set Ξ± ?uof_cd)⦇ArrValβ¦ˆβ¦‡h⦈"
        by 
          (
            cs_concl
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros  
              cs_simp: cat_cs_simps
          )
    qed (use arr_Set_c'd'_𝔉gf arr_Set_gπ”Šf_cd in auto)
 
  qed (use c'd'_𝔉gf gπ”Šf_cd in β€Ήcs_concl cs_simp: cat_cs_simpsβ€Ί)+

qed


subsubsectionβ€ΉUniversal natural transformation is a natural transformationβ€Ί

lemma (in is_functor) cf_ntcf_ua_of_is_ntcf:
  assumes "r ∈∘ 𝔄⦇Obj⦈"
    and "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
  shows "ntcf_ua_of Ξ± 𝔉 c r u :
    HomO.Cα𝔄(r,-) ↦CF HomO.Cα𝔅(c,-) ∘CF 𝔉 : 𝔄 ↦↦CΞ± cat_Set Ξ±"
proof(intro is_ntcfI')
  let ?ua = β€Ήntcf_ua_of Ξ± 𝔉 c r uβ€Ί
  show "vfsequence (ntcf_ua_of Ξ± 𝔉 c r u)" unfolding ntcf_ua_of_def by simp
  show "vcard ?ua = 5β„•" unfolding ntcf_ua_of_def by (simp add: nat_omega_simps)
  from assms(1) show "HomO.Cα𝔄(r,-) : 𝔄 ↦↦CΞ± cat_Set Ξ±"
    by (cs_concl cs_intro: cat_cs_intros)
  from is_functor_axioms assms(2) show 
    "HomO.Cα𝔅(c,-) ∘CF 𝔉 : 𝔄 ↦↦CΞ± cat_Set Ξ±"
    by (cs_concl cs_intro: cat_cs_intros)
  from is_functor_axioms assms show "π’Ÿβˆ˜ (?ua⦇NTMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  show "?ua⦇NTMapβ¦ˆβ¦‡a⦈ :
    HomO.Cα𝔄(r,-)⦇ObjMapβ¦ˆβ¦‡a⦈ ↦cat_Set Ξ± (HomO.Cα𝔅(c,-) ∘CF 𝔉)⦇ObjMapβ¦ˆβ¦‡a⦈"
    if "a ∈∘ 𝔄⦇Obj⦈" for a
    using is_functor_axioms assms that 
    by (cs_concl cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros)
  show "?ua⦇NTMapβ¦ˆβ¦‡b⦈ ∘Acat_Set Ξ± HomO.Cα𝔄(r,-)⦇ArrMapβ¦ˆβ¦‡f⦈ =
    (HomO.Cα𝔅(c,-) ∘CF 𝔉)⦇ArrMapβ¦ˆβ¦‡f⦈ ∘Acat_Set Ξ± ?ua⦇NTMapβ¦ˆβ¦‡a⦈"
    if "f : a ↦𝔄 b" for a b f
    using is_functor_axioms assms that 
    by 
      ( 
        cs_concl 
          cs_simp: cf_umap_of_cf_hom_commute cat_cs_simps cat_op_simps 
          cs_intro: cat_cs_intros cat_op_intros
      )
qed (auto simp: ntcf_ua_of_components cat_cs_simps)

lemma (in is_functor) cf_ntcf_ua_fo_is_ntcf:
  assumes "r ∈∘ 𝔄⦇Obj⦈" and "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c"
  shows "ntcf_ua_fo Ξ± 𝔉 c r u :
    HomO.Cα𝔄(-,r) ↦CF HomO.Cα𝔅(-,c) ∘CF op_cf 𝔉 :
    op_cat 𝔄 ↦↦CΞ± cat_Set Ξ±"
proof-
  from assms(2) have c: "c ∈∘ 𝔅⦇Obj⦈" by auto
  show ?thesis
    by 
      (
        rule is_functor.cf_ntcf_ua_of_is_ntcf
          [
            OF is_functor_op, 
            unfolded cat_op_simps, 
            OF assms(1,2),
            unfolded 
              HomDom.cat_op_cat_cf_Hom_snd[OF assms(1)] 
              HomCod.cat_op_cat_cf_Hom_snd[OF c]
              ntcf_ua_fo_def[symmetric]
          ]
      )
qed


subsubsectionβ€ΉUniversal natural transformation and universal arrowβ€Ί


textβ€Ή
The lemmas in this subsection correspond to 
variants of elements of Proposition 1 in Chapter III-2 in 
\cite{mac_lane_categories_2010}.
β€Ί

lemma (in is_functor) cf_ntcf_ua_of_is_iso_ntcf:
  assumes "universal_arrow_of 𝔉 c r u"
  shows "ntcf_ua_of Ξ± 𝔉 c r u :
    HomO.Cα𝔄(r,-) ↦CF.iso HomO.Cα𝔅(c,-) ∘CF 𝔉 : 𝔄 ↦↦CΞ± cat_Set Ξ±"
proof-

  have r: "r ∈∘ 𝔄⦇Obj⦈"
    and u: "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
    and bij: "β‹€r' u'.
      ⟦
        r' ∈∘ 𝔄⦇Obj⦈; 
        u' : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈
      ⟧ ⟹ βˆƒ!f'. f' : r ↦𝔄 r' ∧ u' = umap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f'⦈"
    by (auto intro!: universal_arrow_ofD[OF assms(1)])

  show ?thesis
  proof(intro is_iso_ntcfI)
    show "ntcf_ua_of Ξ± 𝔉 c r u :
      HomO.Cα𝔄(r,-) ↦CF HomO.Cα𝔅(c,-) ∘CF 𝔉 : 𝔄 ↦↦CΞ± cat_Set Ξ±"
      by (rule cf_ntcf_ua_of_is_ntcf[OF r u])
    fix a assume prems: "a ∈∘ 𝔄⦇Obj⦈"
    from is_functor_axioms prems r u have [simp]:
      "umap_of 𝔉 c r u a : Hom 𝔄 r a ↦cat_Set Ξ± Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡a⦈)"
      by (cs_concl cs_intro: cat_cs_intros)
    then have dom: "π’Ÿβˆ˜ (umap_of 𝔉 c r u a⦇ArrVal⦈) = Hom 𝔄 r a"
      by (cs_concl cs_simp: cat_cs_simps)
    have "umap_of 𝔉 c r u a : Hom 𝔄 r a ↦isocat_Set Ξ± Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡a⦈)"
    proof(intro cat_Set_is_arr_isomorphismI, unfold dom)
 
      show umof_a: "v11 (umap_of 𝔉 c r u a⦇ArrVal⦈)"
      proof(intro vsv.vsv_valeq_v11I, unfold dom in_Hom_iff)
        fix g f assume prems': 
          "g : r ↦𝔄 a"
          "f : r ↦𝔄 a" 
          "umap_of 𝔉 c r u a⦇ArrValβ¦ˆβ¦‡g⦈ = umap_of 𝔉 c r u a⦇ArrValβ¦ˆβ¦‡f⦈"
        from is_functor_axioms r u prems'(1) have 𝔉g:
          "𝔉⦇ArrMapβ¦ˆβ¦‡g⦈ ∘A𝔅 u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡a⦈"
          by (cs_concl cs_intro: cat_cs_intros)
        from bij[OF prems 𝔉g] have unique:
          "⟦
            f' : r ↦𝔄 a;
            𝔉⦇ArrMapβ¦ˆβ¦‡g⦈ ∘A𝔅 u = umap_of 𝔉 c r u a⦇ArrValβ¦ˆβ¦‡f'⦈ 
           ⟧ ⟹ g = f'"
          for f' by (metis prems'(1) u umap_of_ArrVal_app)
        from is_functor_axioms prems'(1,2) u have 𝔉g_u:
          "𝔉⦇ArrMapβ¦ˆβ¦‡g⦈ ∘A𝔅 u = umap_of 𝔉 c r u a⦇ArrValβ¦ˆβ¦‡f⦈"
          by (cs_concl cs_simp: prems'(3)[symmetric] cat_cs_simps)
        show "g = f" by (rule unique[OF prems'(2) 𝔉g_u])
      qed (auto simp: cat_cs_simps cat_cs_intros)

      interpret umof_a: v11 β€Ήumap_of 𝔉 c r u a⦇ArrValβ¦ˆβ€Ί by (rule umof_a)

      show "β„›βˆ˜ (umap_of 𝔉 c r u a⦇ArrVal⦈) = Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡a⦈)"
      proof(intro vsubset_antisym)
        from u show "β„›βˆ˜ (umap_of 𝔉 c r u a⦇ArrVal⦈) βŠ†βˆ˜ Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡a⦈)"
          by (rule umap_of_ArrVal_vrange)
        show "Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡a⦈) βŠ†βˆ˜ β„›βˆ˜ (umap_of 𝔉 c r u a⦇ArrVal⦈)"
        proof(rule vsubsetI, unfold in_Hom_iff )
          fix f assume prems': "f : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡a⦈"
          from bij[OF prems prems'] obtain f' 
            where f': "f' : r ↦𝔄 a" 
              and f_def: "f = umap_of 𝔉 c r u a⦇ArrValβ¦ˆβ¦‡f'⦈"
            by auto
          from is_functor_axioms prems prems' u f' have 
            "f' ∈∘ π’Ÿβˆ˜ (umap_of 𝔉 c r u a⦇ArrVal⦈)"
            by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
          from this show "f ∈∘ β„›βˆ˜ (umap_of 𝔉 c r u a⦇ArrVal⦈)"
            unfolding f_def by (rule umof_a.vsv_vimageI2)
        qed

      qed

    qed simp_all

    from is_functor_axioms prems r u this show 
      "ntcf_ua_of Ξ± 𝔉 c r u⦇NTMapβ¦ˆβ¦‡a⦈ :
        HomO.Cα𝔄(r,-)⦇ObjMapβ¦ˆβ¦‡a⦈ ↦isocat_Set Ξ±
        (HomO.Cα𝔅(c,-) ∘CF 𝔉)⦇ObjMapβ¦ˆβ¦‡a⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_op_simps 
            cs_intro: cat_cs_intros cat_op_intros
        )
  qed

qed

lemmas [cat_cs_intros] = is_functor.cf_ntcf_ua_of_is_iso_ntcf

lemma (in is_functor) cf_ntcf_ua_fo_is_iso_ntcf:
  assumes "universal_arrow_fo 𝔉 c r u"
  shows "ntcf_ua_fo Ξ± 𝔉 c r u :
    HomO.Cα𝔄(-,r) ↦CF.iso HomO.Cα𝔅(-,c) ∘CF op_cf 𝔉 :
    op_cat 𝔄 ↦↦CΞ± cat_Set Ξ±"
proof-
  from universal_arrow_foD[OF assms] have r: "r ∈∘ 𝔄⦇Obj⦈" and c: "c ∈∘ 𝔅⦇Obj⦈"
    by auto
  show ?thesis
    by 
      (
        rule is_functor.cf_ntcf_ua_of_is_iso_ntcf
          [
            OF is_functor_op, 
            unfolded cat_op_simps, 
            OF assms,
            unfolded 
              HomDom.cat_op_cat_cf_Hom_snd[OF r] 
              HomCod.cat_op_cat_cf_Hom_snd[OF c]
              ntcf_ua_fo_def[symmetric]
          ]
      ) 
qed

lemmas [cat_cs_intros] = is_functor.cf_ntcf_ua_fo_is_iso_ntcf

lemma (in is_functor) cf_ua_of_if_ntcf_ua_of_is_iso_ntcf:
  assumes "r ∈∘ 𝔄⦇Obj⦈"
    and "u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
    and "ntcf_ua_of Ξ± 𝔉 c r u :
      HomO.Cα𝔄(r,-) ↦CF.iso HomO.Cα𝔅(c,-) ∘CF 𝔉 : 𝔄 ↦↦CΞ± cat_Set Ξ±"
  shows "universal_arrow_of 𝔉 c r u"
proof(rule universal_arrow_ofI)
  interpret ua_of_u: is_iso_ntcf 
    Ξ± 
    𝔄 
    β€Ήcat_Set Ξ±β€Ί
    β€ΉHomO.Cα𝔄(r,-)β€Ί 
    β€ΉHomO.Cα𝔅(c,-) ∘CF 𝔉› 
    β€Ήntcf_ua_of Ξ± 𝔉 c r uβ€Ί
    by (rule assms(3))
  fix r' u' assume prems: "r' ∈∘ 𝔄⦇Obj⦈" "u' : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈"  
  have "ntcf_ua_of Ξ± 𝔉 c r u⦇NTMapβ¦ˆβ¦‡r'⦈ :
    HomO.Cα𝔄(r,-)⦇ObjMapβ¦ˆβ¦‡r'⦈ ↦isocat_Set Ξ±
    (HomO.Cα𝔅(c,-) ∘CF 𝔉)⦇ObjMapβ¦ˆβ¦‡r'⦈"
    by (rule is_iso_ntcf.iso_ntcf_is_arr_isomorphism[OF assms(3) prems(1)])
  from this is_functor_axioms assms(1-2) prems have uof_r':
    "umap_of 𝔉 c r u r' : Hom 𝔄 r r' ↦isocat_Set Ξ± Hom 𝔅 c (𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈)"
    by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros)
  note uof_r' = cat_Set_is_arr_isomorphismD[OF uof_r']  
  interpret uof_r': v11 β€Ήumap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ€Ί by (rule uof_r'(2))  
  from 
    uof_r'.v11_vrange_ex1_eq[
      THEN iffD1, unfolded uof_r'(3,4) in_Hom_iff, OF prems(2)
      ] 
  show "βˆƒ!f'. f' : r ↦𝔄 r' ∧ u' = umap_of 𝔉 c r u r'⦇ArrValβ¦ˆβ¦‡f'⦈"
    by metis
qed (intro assms)+

lemma (in is_functor) cf_ua_fo_if_ntcf_ua_fo_is_iso_ntcf:
  assumes "r ∈∘ 𝔄⦇Obj⦈"
    and "u : 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈ ↦𝔅 c"
    and "ntcf_ua_fo Ξ± 𝔉 c r u :
      HomO.Cα𝔄(-,r) ↦CF.iso HomO.Cα𝔅(-,c) ∘CF op_cf 𝔉 :
      op_cat 𝔄 ↦↦CΞ± cat_Set Ξ±"
  shows "universal_arrow_fo 𝔉 c r u"
proof-
  from assms(2) have c: "c ∈∘ 𝔅⦇Obj⦈" by auto
  show ?thesis
    by 
      (
        rule is_functor.cf_ua_of_if_ntcf_ua_of_is_iso_ntcf
          [
            OF is_functor_op, 
            unfolded cat_op_simps,
            OF assms(1,2),
            unfolded 
              HomDom.cat_op_cat_cf_Hom_snd[OF assms(1)] 
              HomCod.cat_op_cat_cf_Hom_snd[OF c]
              ntcf_ua_fo_def[symmetric],
            OF assms(3)
          ]
      )
qed

lemma (in is_functor) cf_universal_arrow_of_if_is_iso_ntcf:
  assumes "r ∈∘ 𝔄⦇Obj⦈"
    and "c ∈∘ 𝔅⦇Obj⦈"
    and "Ο† :
      HomO.Cα𝔄(r,-) ↦CF.iso HomO.Cα𝔅(c,-) ∘CF 𝔉 :
      𝔄 ↦↦CΞ± cat_Set Ξ±"
  shows "universal_arrow_of 𝔉 c r (φ⦇NTMapβ¦ˆβ¦‡rβ¦ˆβ¦‡ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈)"
    (is β€Ήuniversal_arrow_of 𝔉 c r ?uβ€Ί)
proof-

  interpret Ο†: is_iso_ntcf 
    Ξ± 𝔄 β€Ήcat_Set Ξ±β€Ί β€ΉHomO.Cα𝔄(r,-)β€Ί β€ΉHomO.Cα𝔅(c,-) ∘CF 𝔉› Ο†
    by (rule assms(3))

  show ?thesis
  proof(intro universal_arrow_ofI assms)
 
    from assms(1,2) show u: "?u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
      by (cs_concl cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros)
    fix r' u' assume prems: "r' ∈∘ 𝔄⦇Obj⦈" "u' : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈"
    have Ο†r'_ArrVal_app[symmetric, cat_cs_simps]:
      "φ⦇NTMapβ¦ˆβ¦‡r'β¦ˆβ¦‡ArrValβ¦ˆβ¦‡f'⦈ =
        𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘A𝔅 φ⦇NTMapβ¦ˆβ¦‡rβ¦ˆβ¦‡ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈"
      if "f' : r ↦𝔄 r'" for f'
    proof-
      have "φ⦇NTMapβ¦ˆβ¦‡r'⦈ ∘Acat_Set Ξ± HomO.Cα𝔄(r,-)⦇ArrMapβ¦ˆβ¦‡f'⦈ =
        (HomO.Cα𝔅(c,-) ∘CF 𝔉)⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘Acat_Set Ξ± φ⦇NTMapβ¦ˆβ¦‡r⦈"
        using that by (intro Ο†.ntcf_Comp_commute)
      then have 
        "φ⦇NTMapβ¦ˆβ¦‡r'⦈ ∘Acat_Set Ξ± cf_hom 𝔄 [𝔄⦇CIdβ¦ˆβ¦‡r⦈, f']∘ =
          cf_hom 𝔅 [𝔅⦇CIdβ¦ˆβ¦‡c⦈, 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈]∘ ∘Acat_Set Ξ± φ⦇NTMapβ¦ˆβ¦‡r⦈" 
        using assms(1,2) that prems
        by (cs_prems cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros)
      then have
        "(φ⦇NTMapβ¦ˆβ¦‡r'⦈ ∘Acat_Set Ξ±
        cf_hom 𝔄 [𝔄⦇CIdβ¦ˆβ¦‡r⦈, f']∘)⦇ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈ =
          (cf_hom 𝔅 [𝔅⦇CIdβ¦ˆβ¦‡c⦈, 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈]∘ ∘Acat_Set Ξ±
          φ⦇NTMapβ¦ˆβ¦‡r⦈)⦇ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈"
         by simp
      from this assms(1,2) u that show ?thesis
        by
          (
            cs_prems
              cs_simp: cat_cs_simps cat_op_simps 
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed 
    
    show "βˆƒ!f'. f' : r ↦𝔄 r' ∧ u' = umap_of 𝔉 c r ?u r'⦇ArrValβ¦ˆβ¦‡f'⦈"
    proof(intro ex1I conjI; (elim conjE)?)
      from assms prems show 
        "(φ⦇NTMapβ¦ˆβ¦‡r'⦈)Β―Ccat_Set α⦇ArrValβ¦ˆβ¦‡u'⦈ : r ↦𝔄 r'"
        by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_cs_intros cat_arrow_cs_intros
          )
      with assms(1,2) prems show "u' =
        umap_of 𝔉 c r ?u r'⦇ArrValβ¦ˆβ¦‡(φ⦇NTMapβ¦ˆβ¦‡r'⦈)Β―Ccat_Set α⦇ArrValβ¦ˆβ¦‡u'⦈⦈"
        by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_arrow_cs_intros cat_cs_intros cat_op_intros
          )
      fix f' assume prems': 
        "f' : r ↦𝔄 r'"
        "u' = umap_of 𝔉 c r (φ⦇NTMapβ¦ˆβ¦‡rβ¦ˆβ¦‡ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈) r'⦇ArrValβ¦ˆβ¦‡f'⦈"
      from prems'(2,1) assms(1,2) have u'_def: 
        "u' = 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘A𝔅 φ⦇NTMapβ¦ˆβ¦‡rβ¦ˆβ¦‡ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈"
        by
          (
            cs_prems
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_cs_intros cat_op_intros
          )
      from prems' show "f' = (φ⦇NTMapβ¦ˆβ¦‡r'⦈)Β―Ccat_Set α⦇ArrValβ¦ˆβ¦‡u'⦈"
        unfolding u'_def Ο†r'_ArrVal_app[OF prems'(1)]
        by
          (
            cs_concl
              cs_simp: cat_cs_simps
              cs_intro: cat_arrow_cs_intros cat_cs_intros cat_op_intros
          )

    qed

  qed

qed

lemma (in is_functor) cf_universal_arrow_fo_if_is_iso_ntcf:
  assumes "r ∈∘ 𝔄⦇Obj⦈"
    and "c ∈∘ 𝔅⦇Obj⦈"
    and "Ο† :
      HomO.Cα𝔄(-,r) ↦CF.iso HomO.Cα𝔅(-,c) ∘CF op_cf 𝔉 :
      op_cat 𝔄 ↦↦CΞ± cat_Set Ξ±"
  shows "universal_arrow_fo 𝔉 c r (φ⦇NTMapβ¦ˆβ¦‡rβ¦ˆβ¦‡ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈)"
  by
    (
      rule is_functor.cf_universal_arrow_of_if_is_iso_ntcf
        [
          OF is_functor_op,
          unfolded cat_op_simps,
          OF assms(1,2),
          unfolded 
            HomDom.cat_op_cat_cf_Hom_snd[OF assms(1)] 
            HomCod.cat_op_cat_cf_Hom_snd[OF assms(2)]
            ntcf_ua_fo_def[symmetric],
          OF assms(3)
        ]
  )

lemma (in is_functor) cf_universal_arrow_of_if_is_iso_ntcf_if_ge_Limit:
  assumes "𝒡 Ξ²"
    and "α ∈∘ β"
    and "r ∈∘ 𝔄⦇Obj⦈"
    and "c ∈∘ 𝔅⦇Obj⦈"
    and "Ο† :
      HomO.Cβ𝔄(r,-) ↦CF.iso HomO.Cβ𝔅(c,-) ∘CF 𝔉 :
      𝔄 ↦↦CΞ² cat_Set Ξ²"
  shows "universal_arrow_of 𝔉 c r (φ⦇NTMapβ¦ˆβ¦‡rβ¦ˆβ¦‡ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈)"
    (is β€Ήuniversal_arrow_of 𝔉 c r ?uβ€Ί)
proof-

  interpret Ξ²: 𝒡 Ξ² by (rule assms(1))
  interpret cat_Set_Ξ±Ξ²: subcategory Ξ² β€Ήcat_Set Ξ±β€Ί β€Ήcat_Set Ξ²β€Ί
    by (rule subcategory_cat_Set_cat_Set[OF assms(1,2)])
  interpret Ο†: is_iso_ntcf 
    Ξ² 𝔄 β€Ήcat_Set Ξ²β€Ί β€ΉHomO.Cβ𝔄(r,-)β€Ί β€ΉHomO.Cβ𝔅(c,-) ∘CF 𝔉› Ο†
    by (rule assms(5))
  interpret β𝔄: category Ξ² 𝔄
    by (rule category.cat_category_if_ge_Limit)
      (use assms(2) in β€Ήcs_concl cs_simp: cs_intro: cat_cs_introsβ€Ί)+
  interpret β𝔅: category Ξ² 𝔅
    by (rule category.cat_category_if_ge_Limit)
      (use assms(2) in β€Ήcs_concl cs_simp: cs_intro: cat_cs_introsβ€Ί)+
  interpret β𝔉: is_functor Ξ² 𝔄 𝔅 𝔉
    by (rule cf_is_functor_if_ge_Limit)
      (use assms(2) in β€Ήcs_concl cs_simp: cs_intro: cat_cs_introsβ€Ί)+

  show ?thesis
  proof(intro universal_arrow_ofI assms)
 
    from assms(3,4) show u: "?u : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r⦈"
      by (cs_concl cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros)
    fix r' u' assume prems: "r' ∈∘ 𝔄⦇Obj⦈" "u' : c ↦𝔅 𝔉⦇ObjMapβ¦ˆβ¦‡r'⦈"
    have Ο†r'_ArrVal_app[symmetric, cat_cs_simps]:
      "φ⦇NTMapβ¦ˆβ¦‡r'β¦ˆβ¦‡ArrValβ¦ˆβ¦‡f'⦈ =
        𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘A𝔅 φ⦇NTMapβ¦ˆβ¦‡rβ¦ˆβ¦‡ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈"
      if "f' : r ↦𝔄 r'" for f'
    proof-
      have "φ⦇NTMapβ¦ˆβ¦‡r'⦈ ∘Acat_Set Ξ² HomO.Cβ𝔄(r,-)⦇ArrMapβ¦ˆβ¦‡f'⦈ =
        (HomO.Cβ𝔅(c,-) ∘CF 𝔉)⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘Acat_Set Ξ² φ⦇NTMapβ¦ˆβ¦‡r⦈"
        using that by (intro Ο†.ntcf_Comp_commute)
      then have 
        "φ⦇NTMapβ¦ˆβ¦‡r'⦈ ∘Acat_Set Ξ² cf_hom 𝔄 [𝔄⦇CIdβ¦ˆβ¦‡r⦈, f']∘ =
          cf_hom 𝔅 [𝔅⦇CIdβ¦ˆβ¦‡c⦈, 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈]∘ ∘Acat_Set Ξ² φ⦇NTMapβ¦ˆβ¦‡r⦈" 
        using assms(3,4) assms(1,2) that prems
        by (cs_prems cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros)
      then have
        "(φ⦇NTMapβ¦ˆβ¦‡r'⦈ ∘Acat_Set Ξ²
        cf_hom 𝔄 [𝔄⦇CIdβ¦ˆβ¦‡r⦈, f']∘)⦇ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈ =
          (cf_hom 𝔅 [𝔅⦇CIdβ¦ˆβ¦‡c⦈, 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈]∘ ∘Acat_Set Ξ²
          φ⦇NTMapβ¦ˆβ¦‡r⦈)⦇ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈"
        by simp
      from 
        this assms(3,4,2) u that HomDom.category_axioms HomCod.category_axioms
      show ?thesis
        by
          (
            cs_prems
              cs_simp: cat_cs_simps cat_op_simps 
              cs_intro:
                cat_cs_intros
                cat_op_intros
                cat_prod_cs_intros
                cat_Set_Ξ±Ξ².subcat_is_arrD
          )
    qed 
    
    show "βˆƒ!f'. f' : r ↦𝔄 r' ∧ u' = umap_of 𝔉 c r ?u r'⦇ArrValβ¦ˆβ¦‡f'⦈"
    proof(intro ex1I conjI; (elim conjE)?)
      from assms prems HomDom.category_axioms show 
        "(φ⦇NTMapβ¦ˆβ¦‡r'⦈)Β―Ccat_Set β⦇ArrValβ¦ˆβ¦‡u'⦈ : r ↦𝔄 r'"
        by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_cs_intros cat_arrow_cs_intros
          )
      with assms(3,4) prems show "u' =
        umap_of 𝔉 c r ?u r'⦇ArrValβ¦ˆβ¦‡(φ⦇NTMapβ¦ˆβ¦‡r'⦈)Β―Ccat_Set β⦇ArrValβ¦ˆβ¦‡u'⦈⦈"
        by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_arrow_cs_intros cat_cs_intros cat_op_intros
          )
      fix f' assume prems': 
        "f' : r ↦𝔄 r'"
        "u' = umap_of 𝔉 c r (φ⦇NTMapβ¦ˆβ¦‡rβ¦ˆβ¦‡ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈) r'⦇ArrValβ¦ˆβ¦‡f'⦈"
      from prems'(2,1) assms(3,4) have u'_def: 
        "u' = 𝔉⦇ArrMapβ¦ˆβ¦‡f'⦈ ∘A𝔅 φ⦇NTMapβ¦ˆβ¦‡rβ¦ˆβ¦‡ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈"
        by
          (
            cs_prems
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_cs_intros cat_op_intros
          )
      from prems' show "f' = (φ⦇NTMapβ¦ˆβ¦‡r'⦈)Β―Ccat_Set β⦇ArrValβ¦ˆβ¦‡u'⦈"
        unfolding u'_def Ο†r'_ArrVal_app[OF prems'(1)]
        by
          (
            cs_concl
              cs_simp: cat_cs_simps
              cs_intro: cat_arrow_cs_intros cat_cs_intros cat_op_intros
          )

    qed

  qed

qed

lemma (in is_functor) cf_universal_arrow_fo_if_is_iso_ntcf_if_ge_Limit:
  assumes "𝒡 Ξ²"
    and "α ∈∘ β"
    and  "r ∈∘ 𝔄⦇Obj⦈"
    and "c ∈∘ 𝔅⦇Obj⦈"
    and "Ο† :
      HomO.Cβ𝔄(-,r) ↦CF.iso HomO.Cβ𝔅(-,c) ∘CF op_cf 𝔉 :
      op_cat 𝔄 ↦↦CΞ² cat_Set Ξ²"
  shows "universal_arrow_fo 𝔉 c r (φ⦇NTMapβ¦ˆβ¦‡rβ¦ˆβ¦‡ArrValβ¦ˆβ¦‡π”„β¦‡CIdβ¦ˆβ¦‡r⦈⦈)"
proof-
  interpret Ξ²: 𝒡 Ξ² by (rule assms(1))
  interpret β𝔉: is_functor Ξ² 𝔄 𝔅 𝔉
    by (rule cf_is_functor_if_ge_Limit)
      (use assms(2) in β€Ήcs_concl cs_intro: cat_cs_introsβ€Ί)+
  show ?thesis 
    by 
      (
        rule is_functor.cf_universal_arrow_of_if_is_iso_ntcf_if_ge_Limit
          [
            OF is_functor_op,
            OF assms(1,2),
            unfolded cat_op_simps,
            OF assms(3,4),
            unfolded 
              β𝔉.HomDom.cat_op_cat_cf_Hom_snd[OF assms(3)] 
              β𝔉.HomCod.cat_op_cat_cf_Hom_snd[OF assms(4)]
              ntcf_ua_fo_def[symmetric],
            OF assms(5)
          ]
      )
qed

textβ€Ή\newpageβ€Ί

end

Theory CZH_UCAT_Limit

(* Copyright 2021 (C) Mihails Milehins *)

sectionβ€ΉLimitsβ€Ί
theory CZH_UCAT_Limit
  imports 
    CZH_UCAT_Universal
    CZH_Elementary_Categories.CZH_ECAT_Discrete 
    CZH_Elementary_Categories.CZH_ECAT_SS
    CZH_Elementary_Categories.CZH_ECAT_Parallel
begin



subsectionβ€ΉBackgroundβ€Ί

named_theorems cat_lim_cs_simps
named_theorems cat_lim_cs_intros



subsectionβ€ΉCone and coconeβ€Ί


textβ€Ή
In the context of this work, the concept of a cone corresponds to that of a cone
to the base of a functor from a vertex, as defined in Chapter III-4 in
\cite{mac_lane_categories_2010}; the concept of a cocone corresponds to that
of a cone from the base of a functor to a vertex, as defined in Chapter III-3
in \cite{mac_lane_categories_2010}.

In this body of work, only limits and colimits of functors with tiny maps 
are considered. The definitions of a cone and a cocone also reflect this.
However, this restriction may be removed in the future.
β€Ί

(*TODO: remove the size limitation; see TODO in the next subsection*)
locale is_cat_cone = is_tm_ntcf Ξ± 𝔍 β„­ β€Ήcf_const 𝔍 β„­ cβ€Ί 𝔉 𝔑 for Ξ± c 𝔍 β„­ 𝔉 𝔑 +
  assumes cat_cone_obj[cat_lim_cs_intros]: "c ∈∘ ℭ⦇Obj⦈"

syntax "_is_cat_cone" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ <CF.cone _ :/ _ ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51] 51)
translations "𝔑 : c <CF.cone 𝔉 : 𝔍 ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_cone Ξ± c 𝔍 β„­ 𝔉 𝔑"

locale is_cat_cocone = is_tm_ntcf Ξ± 𝔍 β„­ 𝔉 β€Ήcf_const 𝔍 β„­ cβ€Ί 𝔑 for Ξ± c 𝔍 β„­ 𝔉 𝔑 +
  assumes cat_cocone_obj[cat_lim_cs_intros]: "c ∈∘ ℭ⦇Obj⦈"

syntax "_is_cat_cocone" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ >CF.cocone _ :/ _ ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51] 51)
translations "𝔑 : 𝔉 >CF.cocone c : 𝔍 ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_cocone Ξ± c 𝔍 β„­ 𝔉 𝔑"


textβ€ΉRules.β€Ί

lemma (in is_cat_cone) is_cat_cone_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±" and "c' = c" and "𝔍' = 𝔍" and "β„­' = β„­" and "𝔉' = 𝔉"
  shows "𝔑 : c' <CF.cone 𝔉' : 𝔍' ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_cone_axioms)

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

lemma (in is_cat_cone) is_cat_coneD'[cat_lim_cs_intros]:
  assumes "c' = cf_const 𝔍 β„­ c"
  shows "𝔑 : c' ↦CF.tm 𝔉 : 𝔍 ↦↦C.tmΞ± β„­"
  unfolding assms by (cs_concl cs_intro: cat_small_cs_intros)

lemmas [cat_lim_cs_intros] = is_cat_cone.is_cat_coneD'

lemma (in is_cat_cocone) is_cat_cocone_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±" and "c' = c" and "𝔍' = 𝔍" and "β„­' = β„­" and "𝔉' = 𝔉"
  shows "𝔑 : 𝔉' >CF.cocone c' : 𝔍' ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_cocone_axioms)

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

lemma (in is_cat_cocone) is_cat_coconeD'[cat_lim_cs_intros]:
  assumes "c' = cf_const 𝔍 β„­ c"
  shows "𝔑 : 𝔉 ↦CF.tm c' : 𝔍 ↦↦C.tmΞ± β„­"
  unfolding assms by (cs_concl cs_intro: cat_small_cs_intros)

lemmas [cat_lim_cs_intros] = is_cat_cocone.is_cat_coconeD'


textβ€ΉDuality.β€Ί

lemma (in is_cat_cone) is_cat_cocone_op:
  "op_ntcf 𝔑 : op_cf 𝔉 >CF.cocone c : op_cat 𝔍 ↦↦CΞ± op_cat β„­"
  by (intro is_cat_coconeI)
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_lim_cs_intros cat_op_intros)+

lemma (in is_cat_cone) is_cat_cocone_op'[cat_op_intros]:
  assumes "Ξ±' = Ξ±" and "𝔍' = op_cat 𝔍" and "β„­' = op_cat β„­" and "𝔉' = op_cf 𝔉"
  shows "op_ntcf 𝔑 : 𝔉' >CF.cocone c : 𝔍' ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_cocone_op)

lemmas [cat_op_intros] = is_cat_cone.is_cat_cocone_op'

lemma (in is_cat_cocone) is_cat_cone_op:
  "op_ntcf 𝔑 : c <CF.cone op_cf 𝔉 : op_cat 𝔍 ↦↦CΞ± op_cat β„­"
  by (intro is_cat_coneI)
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_lim_cs_intros cat_op_intros)

lemma (in is_cat_cocone) is_cat_cone_op'[cat_op_intros]:
  assumes "Ξ±' = Ξ±" and "𝔍' = op_cat 𝔍" and "β„­' = op_cat β„­" and "𝔉' = op_cf 𝔉"
  shows "op_ntcf 𝔑 : c <CF.cone 𝔉' : 𝔍' ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_cone_op)

lemmas [cat_op_intros] = is_cat_cocone.is_cat_cone_op'


textβ€ΉElementary properties.β€Ί

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

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

lemmas [cat_lim_cs_intros] = is_cat_cone.cat_cone_LArr_app_is_arr'

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

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

lemmas [cat_lim_cs_intros] = is_cat_cocone.cat_cocone_LArr_app_is_arr'

lemma (in is_cat_cone) cat_cone_Comp_commute[cat_lim_cs_simps]:
  assumes "f : a ↦𝔍 b"
  shows "𝔉⦇ArrMapβ¦ˆβ¦‡f⦈ ∘Aβ„­ 𝔑⦇NTMapβ¦ˆβ¦‡a⦈ = 𝔑⦇NTMapβ¦ˆβ¦‡b⦈"
  using ntcf_Comp_commute[symmetric, OF assms] assms 
  by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

lemmas [cat_lim_cs_simps] = is_cat_cone.cat_cone_Comp_commute

lemma (in is_cat_cocone) cat_cocone_Comp_commute[cat_lim_cs_simps]:
  assumes "f : a ↦𝔍 b"
  shows "𝔑⦇NTMapβ¦ˆβ¦‡b⦈ ∘Aβ„­ 𝔉⦇ArrMapβ¦ˆβ¦‡f⦈ = 𝔑⦇NTMapβ¦ˆβ¦‡a⦈"
  using ntcf_Comp_commute[OF assms] assms 
  by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

lemmas [cat_lim_cs_simps] = is_cat_cocone.cat_cocone_Comp_commute


textβ€ΉUtilities/helper lemmas.β€Ί

lemma (in is_cat_cone) helper_cat_cone_ntcf_vcomp_Comp:
  assumes "𝔑' : c' <CF.cone 𝔉 : 𝔍 ↦↦CΞ± β„­"
    and "f' : c' ↦ℭ c" 
    and "𝔑' = 𝔑 βˆ™NTCF ntcf_const 𝔍 β„­ f'" 
    and "j ∈∘ 𝔍⦇Obj⦈"
  shows "𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = 𝔑⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aβ„­ f'"
proof-
  from assms(3) have "𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = (𝔑 βˆ™NTCF ntcf_const 𝔍 β„­ f')⦇NTMapβ¦ˆβ¦‡j⦈"
    by simp
  from this assms(1,2,4) show "𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = 𝔑⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aβ„­ f'"
    by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed

lemma (in is_cat_cone) helper_cat_cone_Comp_ntcf_vcomp:
  assumes "𝔑' : c' <CF.cone 𝔉 : 𝔍 ↦↦CΞ± β„­"
    and "f' : c' ↦ℭ c" 
    and "β‹€j. j ∈∘ 𝔍⦇Obj⦈ ⟹ 𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = 𝔑⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aβ„­ f'" 
  shows "𝔑' = 𝔑 βˆ™NTCF ntcf_const 𝔍 β„­ f'"
proof-
  interpret 𝔑': is_cat_cone Ξ± c' 𝔍 β„­ 𝔉 𝔑' by (rule assms(1))
  show ?thesis
  proof(rule ntcf_eqI[OF 𝔑'.is_ntcf_axioms])
    from assms(2) show 
      "𝔑 βˆ™NTCF ntcf_const 𝔍 β„­ f' : cf_const 𝔍 β„­ c' ↦CF 𝔉 : 𝔍 ↦↦CΞ± β„­"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show "𝔑'⦇NTMap⦈ = (𝔑 βˆ™NTCF ntcf_const 𝔍 β„­ f')⦇NTMap⦈"
    proof(rule vsv_eqI, unfold cat_cs_simps)
      show "vsv ((𝔑 βˆ™NTCF ntcf_const 𝔍 β„­ f')⦇NTMap⦈)"
        by (cs_concl cs_intro: cat_cs_intros)
      from assms show "𝔍⦇Obj⦈ = π’Ÿβˆ˜ ((𝔑 βˆ™NTCF ntcf_const 𝔍 β„­ f')⦇NTMap⦈)"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      fix j assume prems': "j ∈∘ 𝔍⦇Obj⦈"
      with assms(1,2) show "𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = (𝔑 βˆ™NTCF ntcf_const 𝔍 β„­ f')⦇NTMapβ¦ˆβ¦‡j⦈"
        by (cs_concl cs_simp: cat_cs_simps assms(3) cs_intro: cat_cs_intros)
    qed auto
  qed simp_all
qed

lemma (in is_cat_cone) helper_cat_cone_Comp_ntcf_vcomp_iff:
  assumes "𝔑' : c' <CF.cone 𝔉 : 𝔍 ↦↦CΞ± β„­"
  shows "f' : c' ↦ℭ c ∧ 𝔑' = 𝔑 βˆ™NTCF ntcf_const 𝔍 β„­ f' ⟷
    f' : c' ↦ℭ c ∧ (βˆ€jβˆˆβˆ˜π”β¦‡Obj⦈. 𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = 𝔑⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aβ„­ f')"
  using 
    helper_cat_cone_ntcf_vcomp_Comp[OF assms]
    helper_cat_cone_Comp_ntcf_vcomp[OF assms]
  by (intro iffI; elim conjE; intro conjI) metis+

lemma (in is_cat_cocone) helper_cat_cocone_ntcf_vcomp_Comp:
  assumes "𝔑' : 𝔉 >CF.cocone c' : 𝔍 ↦↦CΞ± β„­"
    and "f' : c ↦ℭ c'" 
    and "𝔑' = ntcf_const 𝔍 β„­ f' βˆ™NTCF 𝔑" 
    and "j ∈∘ 𝔍⦇Obj⦈"
  shows "𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = f' ∘Aβ„­ 𝔑⦇NTMapβ¦ˆβ¦‡j⦈"
proof-
  interpret 𝔑': is_cat_cocone Ξ± c' 𝔍 β„­ 𝔉 𝔑' by (rule assms(1))
  from assms(3) have "op_ntcf 𝔑' = op_ntcf (ntcf_const 𝔍 β„­ f' βˆ™NTCF 𝔑)" by simp
  from this assms(2) have op_𝔑':
    "op_ntcf 𝔑' = op_ntcf 𝔑 βˆ™NTCF ntcf_const (op_cat 𝔍) (op_cat β„­) f'"
    by (cs_prems cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros)
  have "𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = 𝔑⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aop_cat β„­ f'"
    by 
      (
        rule is_cat_cone.helper_cat_cone_ntcf_vcomp_Comp[
          OF is_cat_cone_op 𝔑'.is_cat_cone_op, 
          unfolded cat_op_simps, 
          OF assms(2) op_𝔑' assms(4)
          ]
      )
  from this assms(2,4) show "𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = f' ∘Aβ„­ 𝔑⦇NTMapβ¦ˆβ¦‡j⦈"
    by (cs_prems cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros)
qed

lemma (in is_cat_cocone) helper_cat_cocone_Comp_ntcf_vcomp:
  assumes "𝔑' : 𝔉 >CF.cocone c' : 𝔍 ↦↦CΞ± β„­"
    and "f' : c ↦ℭ c'" 
    and "β‹€j. j ∈∘ 𝔍⦇Obj⦈ ⟹ 𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = f' ∘Aβ„­ 𝔑⦇NTMapβ¦ˆβ¦‡j⦈" 
  shows "𝔑' = ntcf_const 𝔍 β„­ f' βˆ™NTCF 𝔑"
proof-
  interpret 𝔑': is_cat_cocone Ξ± c' 𝔍 β„­ 𝔉 𝔑' by (rule assms(1))
  from assms(2) have 𝔑'j: "𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = 𝔑⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aop_cat β„­ f'"
    if "j ∈∘ 𝔍⦇Obj⦈" for j
    using that
    unfolding assms(3)[OF that] 
    by (cs_concl cs_simp: cat_op_simps cat_cs_simps cs_intro: cat_cs_intros)
  have op_𝔑': 
    "op_ntcf 𝔑' = op_ntcf 𝔑 βˆ™NTCF ntcf_const (op_cat 𝔍) (op_cat β„­) f'"
    by 
      (
        rule is_cat_cone.helper_cat_cone_Comp_ntcf_vcomp[
          OF is_cat_cone_op 𝔑'.is_cat_cone_op,
          unfolded cat_op_simps, 
          OF assms(2) 𝔑'j, 
          simplified
          ]
      )
  from assms(2) show "𝔑' = (ntcf_const 𝔍 β„­ f' βˆ™NTCF 𝔑)"
    by 
      (
        cs_concl 
          cs_simp: 
            cat_op_simps op_𝔑' eq_op_ntcf_iff[symmetric, OF 𝔑'.is_ntcf_axioms]
          cs_intro: cat_cs_intros
      )
qed

lemma (in is_cat_cocone) helper_cat_cocone_Comp_ntcf_vcomp_iff:
  assumes "𝔑' : 𝔉 >CF.cocone c' : 𝔍 ↦↦CΞ± β„­"
  shows "f' : c ↦ℭ c' ∧ 𝔑' = ntcf_const 𝔍 β„­ f' βˆ™NTCF 𝔑 ⟷
    f' : c ↦ℭ c' ∧ (βˆ€jβˆˆβˆ˜π”β¦‡Obj⦈. 𝔑'⦇NTMapβ¦ˆβ¦‡j⦈ = f' ∘Aβ„­ 𝔑⦇NTMapβ¦ˆβ¦‡j⦈)"
  using 
    helper_cat_cocone_ntcf_vcomp_Comp[OF assms]
    helper_cat_cocone_Comp_ntcf_vcomp[OF assms]
  by (intro iffI; elim conjE; intro conjI) metis+



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}.
β€Ί

(*TODO: remove the size limitation*)
locale is_cat_limit = is_cat_cone Ξ± r 𝔍 β„­ 𝔉 u for Ξ± 𝔍 β„­ 𝔉 r u +
  assumes cat_lim_ua_fo: 
    "universal_arrow_fo (Ξ”C Ξ± 𝔍 β„­) (cf_map 𝔉) r (ntcf_arrow u)"

syntax "_is_cat_limit" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ <CF.lim _ :/ _ ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51] 51)
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_fo: "universal_arrow_fo 
    (Ξ”C Ξ± (op_cat 𝔍) (op_cat β„­)) (cf_map 𝔉) r (ntcf_arrow (op_ntcf u))"

syntax "_is_cat_colimit" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ >CF.colim _ :/ _ ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51] 51)
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β€ΉDualityβ€Ί

lemma (in is_cat_limit) is_cat_colimit_op:
  "op_ntcf u : op_cf 𝔉 >CF.colim r : op_cat 𝔍 ↦↦CΞ± op_cat β„­"
  using cat_lim_ua_fo
  by (intro is_cat_colimitI)
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros)

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 β„­"
  using cat_colim_ua_fo
  by (intro is_cat_limitI)
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros)

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'


textβ€ΉElementary properties of limits and colimits.β€Ί

sublocale is_cat_limit βŠ† Ξ”: is_functor Ξ± β„­ β€Ήcat_Funct Ξ± 𝔍 β„­β€Ί β€ΉΞ”C Ξ± 𝔍 β„­β€Ί
  by (cs_concl cs_intro: cat_cs_intros cat_small_cs_intros)

sublocale is_cat_colimit βŠ† Ξ”: is_functor 
  Ξ± β€Ήop_cat β„­β€Ί β€Ήcat_Funct Ξ± (op_cat 𝔍) (op_cat β„­)β€Ί β€ΉΞ”C Ξ± (op_cat 𝔍) (op_cat β„­)β€Ί
  by (cs_concl cs_intro: cat_small_cs_intros cat_cs_intros cat_op_intros)


subsubsectionβ€ΉUniversal propertyβ€Ί

lemma is_cat_limitI':
  assumes "u : r <CF.cone 𝔉 : 𝔍 ↦↦CΞ± β„­" 
    and "β‹€u' r'. ⟦ u' : r' <CF.cone 𝔉 : 𝔍 ↦↦CΞ± β„­ ⟧ ⟹ 
      βˆƒ!f'. f' : r' ↦ℭ r ∧ u' = u βˆ™NTCF ntcf_const 𝔍 β„­ f'"
  shows "u : r <CF.lim 𝔉 : 𝔍 ↦↦CΞ± β„­"
proof(intro is_cat_limitI is_functor.universal_arrow_foI)
  interpret u: is_cat_cone Ξ± r 𝔍 β„­ 𝔉 u by (rule assms(1))
  show "r ∈∘ ℭ⦇Obj⦈" by (cs_concl cs_intro: cat_lim_cs_intros)
  show "Ξ”C Ξ± 𝔍 β„­ : β„­ ↦↦CΞ± cat_Funct Ξ± 𝔍 β„­"
    by (cs_concl cs_intro: cat_cs_intros cat_small_cs_intros)
  show "ntcf_arrow u : Ξ”C Ξ± 𝔍 ℭ⦇ObjMapβ¦ˆβ¦‡r⦈ ↦cat_Funct Ξ± 𝔍 β„­ cf_map 𝔉"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_lim_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
      )
  fix r' u' assume prems: 
    "r' ∈∘ ℭ⦇Obj⦈" "u' : Ξ”C Ξ± 𝔍 ℭ⦇ObjMapβ¦ˆβ¦‡r'⦈ ↦cat_Funct Ξ± 𝔍 β„­ cf_map 𝔉"
  note u' = cat_Funct_is_arrD[OF prems(2)]
  from u'(1) prems(1) have u'_is_tm_ntcf:
    "ntcf_of_ntcf_arrow 𝔍 β„­ u' : cf_const 𝔍 β„­ r' ↦CF.tm 𝔉 : 𝔍 ↦↦C.tmΞ± β„­"
    by 
      (
        cs_prems 
          cs_simp: cat_cs_simps cat_small_cs_simps cat_FUNCT_cs_simps 
          cs_intro: cat_cs_intros
      )
  from this prems(1) have u'_is_cat_cone: 
    "ntcf_of_ntcf_arrow 𝔍 β„­ u' : r' <CF.cone 𝔉 : 𝔍 ↦↦CΞ± β„­"
    by (intro is_cat_coneI)
  interpret u': is_cat_cone Ξ± r' 𝔍 β„­ 𝔉 β€Ήntcf_of_ntcf_arrow 𝔍 β„­ u'β€Ί
    by (rule u'_is_cat_cone)
  from assms(2)[OF u'_is_cat_cone] obtain f' where f': "f' : r' ↦ℭ r"
    and u'_def: "ntcf_of_ntcf_arrow 𝔍 β„­ u' = u βˆ™NTCF ntcf_const 𝔍 β„­ f'"
    and unique: "β‹€f''.
      ⟦
        f'' : r' ↦ℭ r; 
        ntcf_of_ntcf_arrow 𝔍 β„­ u' = u βˆ™NTCF ntcf_const 𝔍 β„­ f''
      ⟧ ⟹ f'' = f'"
    by (meson prems(1))
  from u'_def have u'_NTMap_app:
    "ntcf_of_ntcf_arrow 𝔍 β„­ u'⦇NTMapβ¦ˆβ¦‡j⦈ = (u βˆ™NTCF ntcf_const 𝔍 β„­ f')⦇NTMapβ¦ˆβ¦‡j⦈"
    if "j ∈∘ 𝔍⦇Obj⦈" for j 
    by simp
  have u'_NTMap_app: "u'⦇NTMapβ¦ˆβ¦‡j⦈ = u⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aβ„­ f'"
    if "j ∈∘ 𝔍⦇Obj⦈" for j 
    using u'_NTMap_app[OF that] that f'
    by (cs_prems cs_simp: cat_cs_simps cat_FUNCT_cs_simps cs_intro: cat_cs_intros)
  show "βˆƒ!f'.
    f' : r' ↦ℭ r ∧
    u' = umap_fo (Ξ”C Ξ± 𝔍 β„­) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrValβ¦ˆβ¦‡f'⦈"
  proof(intro ex1I conjI; (elim conjE)?)
    show "f' : r' ↦ℭ r" by (rule f')
    have u'_def'[symmetric, cat_cs_simps]: 
      "ntcf_of_ntcf_arrow 𝔍 β„­ u' = u βˆ™NTCF ntcf_const 𝔍 β„­ f'"
    proof(rule ntcf_eqI)
      from u'_is_tm_ntcf show 
        "ntcf_of_ntcf_arrow 𝔍 β„­ u' : cf_const 𝔍 β„­ r' ↦CF 𝔉 : 𝔍 ↦↦CΞ± β„­"
        by (cs_concl cs_intro: cat_small_cs_intros)
      from f' show 
        "u βˆ™NTCF ntcf_const 𝔍 β„­ f' : cf_const 𝔍 β„­ r' ↦CF 𝔉 : 𝔍 ↦↦CΞ± β„­"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      show 
        "ntcf_of_ntcf_arrow 𝔍 β„­ u'⦇NTMap⦈ = (u βˆ™NTCF ntcf_const 𝔍 β„­ f')⦇NTMap⦈"
      proof(rule vsv_eqI)
        from f' show "π’Ÿβˆ˜ (ntcf_of_ntcf_arrow 𝔍 β„­ u'⦇NTMap⦈) = 
          π’Ÿβˆ˜ ((u βˆ™NTCF ntcf_const 𝔍 β„­ f')⦇NTMap⦈)"
          by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)    
        show "ntcf_of_ntcf_arrow 𝔍 β„­ u'⦇NTMapβ¦ˆβ¦‡a⦈ = 
          (u βˆ™NTCF ntcf_const 𝔍 β„­ f')⦇NTMapβ¦ˆβ¦‡a⦈"
          if "a ∈∘ π’Ÿβˆ˜ (ntcf_of_ntcf_arrow 𝔍 β„­ u'⦇NTMap⦈)" for a
        proof-
          from that have "a ∈∘ 𝔍⦇Obj⦈" by (cs_prems cs_simp: cat_cs_simps)    
          with f' show 
            "ntcf_of_ntcf_arrow 𝔍 β„­ u'⦇NTMapβ¦ˆβ¦‡a⦈ =
              (u βˆ™NTCF ntcf_const 𝔍 β„­ f')⦇NTMapβ¦ˆβ¦‡a⦈"
            by 
              (
                cs_concl 
                  cs_simp: cat_cs_simps cat_FUNCT_cs_simps u'_NTMap_app 
                  cs_intro: cat_cs_intros
              )
        qed
      qed (auto intro: cat_cs_intros)
    qed simp_all
    from f' u'(1) show 
      "u' = umap_fo (Ξ”C Ξ± 𝔍 β„­) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrValβ¦ˆβ¦‡f'⦈"
      by (subst u'(2))
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_small_cs_intros
        )
    fix f'' assume prems': 
      "f'' : r' ↦ℭ r"
      "u' = umap_fo (Ξ”C Ξ± 𝔍 β„­) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrValβ¦ˆβ¦‡f''⦈"  
    from prems'(2,1) u'(1) have 
      "ntcf_of_ntcf_arrow 𝔍 β„­ u' = u βˆ™NTCF ntcf_const 𝔍 β„­ f''"
      by (subst (asm) u'(2))
        (
          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 unique[OF prems'(1) this] show "f'' = f'" .
  qed
qed (intro assms)+

lemma (in is_cat_limit) cat_lim_unique_cone:
  assumes "u' : r' <CF.cone 𝔉 : 𝔍 ↦↦CΞ± β„­" 
  shows "βˆƒ!f'. f' : r' ↦ℭ r ∧ u' = u βˆ™NTCF ntcf_const 𝔍 β„­ f'"
proof-
  interpret u': is_cat_cone Ξ± r' 𝔍 β„­ 𝔉 u' by (rule assms(1))
  have "ntcf_arrow u' : Ξ”C Ξ± 𝔍 ℭ⦇ObjMapβ¦ˆβ¦‡r'⦈ ↦cat_Funct Ξ± 𝔍 β„­ cf_map 𝔉"
    by 
      (
        cs_concl 
          cs_intro: cat_lim_cs_intros cat_FUNCT_cs_intros cs_simp: cat_cs_simps
      )
  from Ξ”.universal_arrow_foD(3)[OF cat_lim_ua_fo u'.cat_cone_obj this] obtain f'
    where f': "f' : r' ↦ℭ r" 
      and u': "ntcf_arrow u' =
      umap_fo (Ξ”C Ξ± 𝔍 β„­) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrValβ¦ˆβ¦‡f'⦈"
      and unique:
        "⟦
          f'' : r' ↦ℭ r;
          ntcf_arrow u' =
            umap_fo (Ξ”C Ξ± 𝔍 β„­) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrValβ¦ˆβ¦‡f''⦈
         ⟧ ⟹ f'' = f'"
    for f''
    by metis
  show "βˆƒ!f'. f' : r' ↦ℭ r ∧ u' = u βˆ™NTCF ntcf_const 𝔍 β„­ f'"
  proof(intro ex1I conjI; (elim conjE)?)
    show "f' : r' ↦ℭ r" by (rule f')
    with u' show "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 cat_small_cs_intros
        )
    fix f'' assume prems: "f'' : r' ↦ℭ r"  "u' = u βˆ™NTCF ntcf_const 𝔍 β„­ f''"
    from prems(1) have "ntcf_arrow u' =
      umap_fo (Ξ”C Ξ± 𝔍 β„­) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrValβ¦ˆβ¦‡f''⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps prems(2)[symmetric] 
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_small_cs_intros
        )
    from prems(1) this show "f'' = f'" by (intro unique)
  qed
qed  

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_unique_cone 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_unique_cone[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_unique_cone[
      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_arr_isomorphism:
  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))
  obtain f where f: "f : r' ↦isoβ„­ r"
    and u': "ntcf_arrow u' =
    umap_fo (Ξ”C Ξ± 𝔍 β„­) (cf_map 𝔉) r (ntcf_arrow u) r'⦇ArrValβ¦ˆβ¦‡f⦈"
    by 
      (
        elim u.Ξ”.cf_universal_arrow_fo_ex_is_arr_isomorphism[
          OF u.cat_lim_ua_fo u'.cat_lim_ua_fo
          ]
      )
  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 cat_small_cs_simps
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros cat_small_cs_intros
      )
  with f that show ?thesis by simp
qed

lemma cat_lim_ex_is_arr_isomorphism':
  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_arr_isomorphism)
  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_arr_isomorphism:
  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' ↦isoop_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_arr_isomorphism[
          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_arr_isomorphism':
  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_arr_isomorphism)
  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



subsectionβ€ΉFinite limit and finite colimitβ€Ί

locale is_cat_finite_limit = is_cat_limit Ξ± 𝔍 β„­ 𝔉 r u + 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)
translations "u : r <CF.lim.fin 𝔉 : 𝔍 ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_finite_limit Ξ± 𝔍 β„­ 𝔉 r u"

locale is_cat_finite_colimit = is_cat_colimit Ξ± 𝔍 β„­ 𝔉 r u + 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)
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_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_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'



subsectionβ€ΉProduct and coproductβ€Ί


subsubsectionβ€ΉDefinition and elementary propertiesβ€Ί


textβ€Ή
The definition of the product object is a specialization of the 
definition presented in Chapter III-4 in \cite{mac_lane_categories_2010}.
In the definition presented below, the discrete category that is used in the 
definition presented in \cite{mac_lane_categories_2010} is parameterized by
an index set and the functor from the discrete category is 
parameterized by a function from the index set to the set of 
the objects of the category.
β€Ί

locale is_cat_obj_prod = 
  is_cat_limit Ξ± β€Ή:C Iβ€Ί β„­ β€Ή:β†’: I A β„­β€Ί P Ο€ + cf_discrete Ξ± I A β„­
  for Ξ± I A β„­ P Ο€

syntax "_is_cat_obj_prod" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ <CF.∏ _ :/ _ ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51] 51)
translations "Ο€ : P <CF.∏ A : I ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_obj_prod Ξ± I A β„­ P Ο€"

locale is_cat_obj_coprod = 
  is_cat_colimit Ξ± β€Ή:C Iβ€Ί β„­ β€Ή:β†’: I A β„­β€Ί U Ο€ + cf_discrete Ξ± I A β„­
  for Ξ± I A β„­ U Ο€

syntax "_is_cat_obj_coprod" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ >CF.∐ _ :/ _ ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51] 51)
translations "Ο€ : A >CF.∐ U : I ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_obj_coprod Ξ± I A β„­ U Ο€"


textβ€ΉRules.β€Ί

lemma (in is_cat_obj_prod) is_cat_obj_prod_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±" and "P' = P" and "A' = A" and "I' = I" and "β„­' = β„­" 
  shows "Ο€ : P' <CF.∏ A' : I' ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_obj_prod_axioms)

mk_ide rf is_cat_obj_prod_def
  |intro is_cat_obj_prodI|
  |dest is_cat_obj_prodD[dest]|
  |elim is_cat_obj_prodE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_obj_prodD

lemma (in is_cat_obj_coprod) is_cat_obj_coprod_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±" and "U' = U" and "A' = A" and "I' = I" and "β„­' = β„­" 
  shows "Ο€ : A' >CF.∐ U' : I' ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_obj_coprod_axioms)

mk_ide rf is_cat_obj_coprod_def
  |intro is_cat_obj_coprodI|
  |dest is_cat_obj_coprodD[dest]|
  |elim is_cat_obj_coprodE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_obj_coprodD


textβ€ΉDuality.β€Ί

lemma (in is_cat_obj_prod) is_cat_obj_coprod_op:
  "op_ntcf Ο€ : A >CF.∐ P : I ↦↦CΞ± op_cat β„­"
  using cf_discrete_vdomain_vsubset_Vset
  by (intro is_cat_obj_coprodI)
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros)

lemma (in is_cat_obj_prod) is_cat_obj_coprod_op'[cat_op_intros]:
  assumes "β„­' = op_cat β„­"
  shows "op_ntcf Ο€ : A >CF.∐ P : I ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_obj_coprod_op)

lemmas [cat_op_intros] = is_cat_obj_prod.is_cat_obj_coprod_op'

lemma (in is_cat_obj_coprod) is_cat_obj_prod_op:
  "op_ntcf Ο€ : U <CF.∏ A : I ↦↦CΞ± op_cat β„­"
  using cf_discrete_vdomain_vsubset_Vset
  by (intro is_cat_obj_prodI)
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros)

lemma (in is_cat_obj_coprod) is_cat_obj_prod_op'[cat_op_intros]:
  assumes "β„­' = op_cat β„­"
  shows "op_ntcf Ο€ : U <CF.∏ A : I ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_obj_prod_op)

lemmas [cat_op_intros] = is_cat_obj_coprod.is_cat_obj_prod_op'


subsubsectionβ€ΉUniversal propertyβ€Ί

(*cat_obj_prod_unique_cone already proven*)
lemma (in is_cat_obj_prod) cat_obj_prod_unique_cone':
  assumes "Ο€' : P' <CF.cone :β†’: I A β„­ : :C I ↦↦CΞ± β„­"
  shows "βˆƒ!f'. f' : P' ↦ℭ P ∧ (βˆ€j∈∘I. Ο€'⦇NTMapβ¦ˆβ¦‡j⦈ = π⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aβ„­ f')"
  by 
    (
      rule cat_lim_unique_cone'[
        OF assms, unfolded the_cat_discrete_components(1)
        ]
    )

lemma (in is_cat_obj_prod) cat_obj_prod_unique:
  assumes "Ο€' : P' <CF.∏ A : I ↦↦CΞ± β„­"
  shows "βˆƒ!f'. f' : P' ↦ℭ P ∧ Ο€' = Ο€ βˆ™NTCF ntcf_const (:C I) β„­ f'"
  by (intro cat_lim_unique[OF is_cat_obj_prodD(1)[OF assms]])

lemma (in is_cat_obj_prod) cat_obj_prod_unique':
  assumes "Ο€' : P' <CF.∏ A : I ↦↦CΞ± β„­"
  shows "βˆƒ!f'. f' : P' ↦ℭ P ∧ (βˆ€i∈∘I. Ο€'⦇NTMapβ¦ˆβ¦‡i⦈ = π⦇NTMapβ¦ˆβ¦‡i⦈ ∘Aβ„­ f')"
proof-
  interpret Ο€': is_cat_obj_prod Ξ± I A β„­ P' Ο€' by (rule assms(1))
  show ?thesis
    by 
      (
        rule cat_lim_unique'[
          OF Ο€'.is_cat_limit_axioms, unfolded the_cat_discrete_components(1)
          ]
      )
qed

lemma (in is_cat_obj_coprod) cat_obj_coprod_unique_cocone':
  assumes "Ο€' : :β†’: I A β„­ >CF.cocone U' : :C I ↦↦CΞ± β„­"
  shows "βˆƒ!f'. f' : U ↦ℭ U' ∧ (βˆ€j∈∘I. Ο€'⦇NTMapβ¦ˆβ¦‡j⦈ = f' ∘Aβ„­ π⦇NTMapβ¦ˆβ¦‡j⦈)"
  by 
    (
      rule cat_colim_unique_cocone'[
        OF assms, unfolded the_cat_discrete_components(1)
        ]
    )

lemma (in is_cat_obj_coprod) cat_obj_coprod_unique:
  assumes "Ο€' : A >CF.∐ U' : I ↦↦CΞ± β„­"
  shows "βˆƒ!f'. f' : U ↦ℭ U' ∧ Ο€' = ntcf_const (:C I) β„­ f' βˆ™NTCF Ο€"
  by (intro cat_colim_unique[OF is_cat_obj_coprodD(1)[OF assms]])

lemma (in is_cat_obj_coprod) cat_obj_coprod_unique':
  assumes "Ο€' : A >CF.∐ U' : I ↦↦CΞ± β„­"
  shows "βˆƒ!f'. f' : U ↦ℭ U' ∧ (βˆ€j∈∘I. Ο€'⦇NTMapβ¦ˆβ¦‡j⦈ = f' ∘Aβ„­ π⦇NTMapβ¦ˆβ¦‡j⦈)"
  by 
    (
      rule cat_colim_unique'[
        OF is_cat_obj_coprodD(1)[OF assms], unfolded the_cat_discrete_components
        ]
    )

lemma cat_obj_prod_ex_is_arr_isomorphism:
  assumes "Ο€ : P <CF.∏ A : I ↦↦CΞ± β„­" and "Ο€' : P' <CF.∏ A : I ↦↦CΞ± β„­"
  obtains f where "f : P' ↦isoβ„­ P" and "Ο€' = Ο€ βˆ™NTCF ntcf_const (:C I) β„­ f"
proof-
  interpret Ο€: is_cat_obj_prod Ξ± I A β„­ P Ο€ by (rule assms(1))
  interpret Ο€': is_cat_obj_prod Ξ± I A β„­ P' Ο€' by (rule assms(2))
  from that show ?thesis
    by 
      (
        elim cat_lim_ex_is_arr_isomorphism[
          OF Ο€.is_cat_limit_axioms Ο€'.is_cat_limit_axioms
          ]
      )
qed

lemma cat_obj_prod_ex_is_arr_isomorphism':
  assumes "Ο€ : P <CF.∏ A : I ↦↦CΞ± β„­" and "Ο€' : P' <CF.∏ A : I ↦↦CΞ± β„­"
  obtains f where "f : P' ↦isoβ„­ P" 
    and "β‹€j. j ∈∘ I ⟹ Ο€'⦇NTMapβ¦ˆβ¦‡j⦈ = π⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aβ„­ f"
proof-
  interpret Ο€: is_cat_obj_prod Ξ± I A β„­ P Ο€ by (rule assms(1))
  interpret Ο€': is_cat_obj_prod Ξ± I A β„­ P' Ο€' by (rule assms(2))
  from that show ?thesis
    by 
      (
        elim cat_lim_ex_is_arr_isomorphism'[
          OF Ο€.is_cat_limit_axioms Ο€'.is_cat_limit_axioms,
          unfolded the_cat_discrete_components(1)
          ]
      )
qed

lemma cat_obj_coprod_ex_is_arr_isomorphism:
  assumes "Ο€ : A >CF.∐ U : I ↦↦CΞ± β„­" and "Ο€' : A >CF.∐ U' : I ↦↦CΞ± β„­"
  obtains f where "f : U ↦isoβ„­ U'" and "Ο€' = ntcf_const (:C I) β„­ f βˆ™NTCF Ο€"
proof-
  interpret Ο€: is_cat_obj_coprod Ξ± I A β„­ U Ο€ by (rule assms(1))
  interpret Ο€': is_cat_obj_coprod Ξ± I A β„­ U' Ο€' by (rule assms(2))
  from that show ?thesis
    by 
      (
        elim cat_colim_ex_is_arr_isomorphism[
          OF Ο€.is_cat_colimit_axioms Ο€'.is_cat_colimit_axioms
          ]
      )
qed

lemma cat_obj_coprod_ex_is_arr_isomorphism':
  assumes "Ο€ : A >CF.∐ U : I ↦↦CΞ± β„­" and "Ο€' : A >CF.∐ U' : I ↦↦CΞ± β„­"
  obtains f where "f : U ↦isoβ„­ U'" 
    and "β‹€j. j ∈∘ I ⟹ Ο€'⦇NTMapβ¦ˆβ¦‡j⦈ = f ∘Aβ„­ π⦇NTMapβ¦ˆβ¦‡j⦈"
proof-
  interpret Ο€: is_cat_obj_coprod Ξ± I A β„­ U Ο€ by (rule assms(1))
  interpret Ο€': is_cat_obj_coprod Ξ± I A β„­ U' Ο€' by (rule assms(2))
  from that show ?thesis
    by 
      (
        elim cat_colim_ex_is_arr_isomorphism'[
          OF Ο€.is_cat_colimit_axioms Ο€'.is_cat_colimit_axioms,
          unfolded the_cat_discrete_components(1)
          ]
      )
qed



subsectionβ€ΉFinite product and finite coproductβ€Ί

locale is_cat_finite_obj_prod = is_cat_obj_prod Ξ± I A β„­ P Ο€ 
  for Ξ± I A β„­ P Ο€ +
  assumes cat_fin_obj_prod_index_in_Ο‰: "I ∈∘ Ο‰" 

syntax "_is_cat_finite_obj_prod" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ <CF.∏.fin _ :/ _ ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51] 51)
translations "Ο€ : P <CF.∏.fin A : I ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_finite_obj_prod Ξ± I A β„­ P Ο€"

locale is_cat_finite_obj_coprod = is_cat_obj_coprod Ξ± I A β„­ U Ο€ 
  for Ξ± I A β„­ U Ο€ +
  assumes cat_fin_obj_coprod_index_in_Ο‰: "I ∈∘ Ο‰" 

syntax "_is_cat_finite_obj_coprod" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ >CF.∐.fin _ :/ _ ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51] 51)
translations "Ο€ : A >CF.∐.fin U : I ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_finite_obj_coprod Ξ± I A β„­ U Ο€"

lemma (in is_cat_finite_obj_prod) cat_fin_obj_prod_index_vfinite: "vfinite I"
  using cat_fin_obj_prod_index_in_Ο‰ by auto

sublocale is_cat_finite_obj_prod βŠ† I: finite_category Ξ± β€Ή:C Iβ€Ί
  by (intro finite_categoryI')
    (
      auto
        simp: NTDom.HomDom.tiny_dg_category the_cat_discrete_components
        intro!: cat_fin_obj_prod_index_vfinite
    )

lemma (in is_cat_finite_obj_coprod) cat_fin_obj_coprod_index_vfinite:
  "vfinite I"
  using cat_fin_obj_coprod_index_in_Ο‰ by auto

sublocale is_cat_finite_obj_coprod βŠ† I: finite_category Ξ± β€Ή:C Iβ€Ί
  by (intro finite_categoryI')
    (
      auto 
        simp: NTDom.HomDom.tiny_dg_category the_cat_discrete_components 
        intro!: cat_fin_obj_coprod_index_vfinite
    )


textβ€ΉRules.β€Ί

lemma (in is_cat_finite_obj_prod) 
  is_cat_finite_obj_prod_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±" and "P' = P" and "A' = A" and "I' = I" and "β„­' = β„­" 
  shows "Ο€ : P' <CF.∏.fin A' : I' ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_finite_obj_prod_axioms)

mk_ide rf 
  is_cat_finite_obj_prod_def[unfolded is_cat_finite_obj_prod_axioms_def]
  |intro is_cat_finite_obj_prodI|
  |dest is_cat_finite_obj_prodD[dest]|
  |elim is_cat_finite_obj_prodE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_finite_obj_prodD

lemma (in is_cat_finite_obj_coprod) 
  is_cat_finite_obj_coprod_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±" and "U' = U" and "A' = A" and "I' = I" and "β„­' = β„­" 
  shows "Ο€ : A' >CF.∐.fin U' : I' ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_finite_obj_coprod_axioms)

mk_ide rf 
  is_cat_finite_obj_coprod_def[unfolded is_cat_finite_obj_coprod_axioms_def]
  |intro is_cat_finite_obj_coprodI|
  |dest is_cat_finite_obj_coprodD[dest]|
  |elim is_cat_finite_obj_coprodE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_finite_obj_coprodD


textβ€ΉDuality.β€Ί

lemma (in is_cat_finite_obj_prod) is_cat_finite_obj_coprod_op:
  "op_ntcf Ο€ : A >CF.∐.fin P : I ↦↦CΞ± op_cat β„­"
  by (intro is_cat_finite_obj_coprodI)
    (
      cs_concl 
        cs_simp: cat_op_simps 
        cs_intro: cat_fin_obj_prod_index_in_Ο‰ cat_cs_intros cat_op_intros
    )

lemma (in is_cat_finite_obj_prod) is_cat_finite_obj_coprod_op'[cat_op_intros]:
  assumes "β„­' = op_cat β„­"
  shows "op_ntcf Ο€ : A >CF.∐.fin P : I ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_finite_obj_coprod_op)

lemmas [cat_op_intros] = is_cat_finite_obj_prod.is_cat_finite_obj_coprod_op'

lemma (in is_cat_finite_obj_coprod) is_cat_finite_obj_prod_op:
  "op_ntcf Ο€ : U <CF.∏.fin A : I ↦↦CΞ± op_cat β„­"
  by (intro is_cat_finite_obj_prodI)
    (
      cs_concl 
        cs_simp: cat_op_simps 
        cs_intro: cat_fin_obj_coprod_index_in_Ο‰ cat_cs_intros cat_op_intros
    )

lemma (in is_cat_finite_obj_coprod) is_cat_finite_obj_prod_op'[cat_op_intros]:
  assumes "β„­' = op_cat β„­"
  shows "op_ntcf Ο€ : U <CF.∏.fin A : I ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_finite_obj_prod_op)

lemmas [cat_op_intros] = is_cat_finite_obj_coprod.is_cat_finite_obj_prod_op'



subsectionβ€ΉProduct and coproduct of two objectsβ€Ί


subsubsectionβ€ΉDefinition and elementary propertiesβ€Ί

locale is_cat_obj_prod_2 = is_cat_obj_prod Ξ± β€Ή2β„•β€Ί β€Ήif2 a bβ€Ί β„­ P Ο€
  for Ξ± a b β„­ P Ο€

syntax "_is_cat_obj_prod_2" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ <CF.Γ— {_,_} :/ 2C ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51] 51)
translations "Ο€ : P <CF.Γ— {a,b} : 2C ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_obj_prod_2 Ξ± a b β„­ P Ο€"

locale is_cat_obj_coprod_2 = is_cat_obj_coprod Ξ± β€Ή2β„•β€Ί β€Ήif2 a bβ€Ί β„­ P Ο€
  for Ξ± a b β„­ P Ο€

syntax "_is_cat_obj_coprod_2" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ {_,_} >CF.⊎ _ :/ 2C ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51] 51)
translations "Ο€ : {a,b} >CF.⊎ U : 2C ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_obj_coprod_2 Ξ± a b β„­ U Ο€"

abbreviation proj_fst where "proj_fst Ο€ ≑ vpfst (π⦇NTMap⦈)"
abbreviation proj_snd where "proj_snd Ο€ ≑ vpsnd (π⦇NTMap⦈)"


textβ€ΉRules.β€Ί

lemma (in is_cat_obj_prod_2) is_cat_obj_prod_2_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±" and "P' = P" and "a' = a" and "b' = b" and "β„­' = β„­" 
  shows "Ο€ : P' <CF.Γ— {a',b'} : 2C ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_obj_prod_2_axioms)

mk_ide rf is_cat_obj_prod_2_def
  |intro is_cat_obj_prod_2I|
  |dest is_cat_obj_prod_2D[dest]|
  |elim is_cat_obj_prod_2E[elim]|

lemmas [cat_lim_cs_intros] = is_cat_obj_prod_2D

lemma (in is_cat_obj_coprod_2) is_cat_obj_coprod_2_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±" and "P' = P" and "a' = a" and "b' = b" and "β„­' = β„­" 
  shows "Ο€ : {a',b'} >CF.⊎ P' : 2C ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_obj_coprod_2_axioms)

mk_ide rf is_cat_obj_coprod_2_def
  |intro is_cat_obj_coprod_2I|
  |dest is_cat_obj_coprod_2D[dest]|
  |elim is_cat_obj_coprod_2E[elim]|

lemmas [cat_lim_cs_intros] = is_cat_obj_coprod_2D


textβ€ΉDuality.β€Ί

lemma (in is_cat_obj_prod_2) is_cat_obj_coprod_2_op:
  "op_ntcf Ο€ : {a,b} >CF.⊎ P : 2C ↦↦CΞ± op_cat β„­"
  by (rule is_cat_obj_coprod_2I[OF is_cat_obj_coprod_op])

lemma (in is_cat_obj_prod_2) is_cat_obj_coprod_2_op'[cat_op_intros]:
  assumes "β„­' = op_cat β„­"
  shows "op_ntcf Ο€ : {a,b} >CF.⊎ P : 2C ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_obj_coprod_2_op)

lemmas [cat_op_intros] = is_cat_obj_prod_2.is_cat_obj_coprod_2_op'

lemma (in is_cat_obj_coprod_2) is_cat_obj_prod_2_op:
  "op_ntcf Ο€ : P <CF.Γ— {a,b} : 2C ↦↦CΞ± op_cat β„­"
  by (rule is_cat_obj_prod_2I[OF is_cat_obj_prod_op])

lemma (in is_cat_obj_coprod_2) is_cat_obj_prod_2_op'[cat_op_intros]:
  assumes "β„­' = op_cat β„­"
  shows "op_ntcf Ο€ : P <CF.Γ— {a,b} : 2C ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_obj_prod_2_op)

lemmas [cat_op_intros] = is_cat_obj_coprod_2.is_cat_obj_prod_2_op'


textβ€ΉProduct/coproduct of two objects is a finite product/coproduct.β€Ί

sublocale is_cat_obj_prod_2 βŠ† is_cat_finite_obj_prod Ξ± β€Ή2β„•β€Ί β€Ήif2 a bβ€Ί β„­ P Ο€
proof(intro is_cat_finite_obj_prodI)
  show "2β„• ∈∘ Ο‰" by simp
qed (cs_concl cs_simp: two[symmetric] cs_intro: cat_lim_cs_intros)

sublocale is_cat_obj_coprod_2 βŠ† is_cat_finite_obj_coprod Ξ± β€Ή2β„•β€Ί β€Ήif2 a bβ€Ί β„­ P Ο€
proof(intro is_cat_finite_obj_coprodI)
  show "2β„• ∈∘ Ο‰" by simp
qed (cs_concl cs_simp: two[symmetric] cs_intro: cat_lim_cs_intros)


textβ€ΉElementary properties.β€Ί

lemma (in is_cat_obj_prod_2) cat_obj_prod_2_lr_in_Obj:
  shows cat_obj_prod_2_left_in_Obj[cat_lim_cs_intros]: "a ∈∘ ℭ⦇Obj⦈" 
    and cat_obj_prod_2_right_in_Obj[cat_lim_cs_intros]: "b ∈∘ ℭ⦇Obj⦈"
proof-
  have 0: "0 ∈∘ 2β„•" and 1: "1β„• ∈∘ 2β„•" by simp_all
  show "a ∈∘ ℭ⦇Obj⦈" and "b ∈∘ ℭ⦇Obj⦈"
    by 
      (
        intro 
          cf_discrete_selector_vrange[OF 0, simplified]
          cf_discrete_selector_vrange[OF 1, simplified]
      )+
qed

lemmas [cat_lim_cs_intros] = is_cat_obj_prod_2.cat_obj_prod_2_lr_in_Obj

lemma (in is_cat_obj_coprod_2) cat_obj_coprod_2_lr_in_Obj:
  shows cat_obj_coprod_2_left_in_Obj[cat_lim_cs_intros]: "a ∈∘ ℭ⦇Obj⦈" 
    and cat_obj_coprod_2_right_in_Obj[cat_lim_cs_intros]: "b ∈∘ ℭ⦇Obj⦈"
  by 
    (
      intro is_cat_obj_prod_2.cat_obj_prod_2_lr_in_Obj[
        OF is_cat_obj_prod_2_op, unfolded cat_op_simps
        ]
    )+

lemmas [cat_lim_cs_intros] = is_cat_obj_coprod_2.cat_obj_coprod_2_lr_in_Obj


textβ€ΉUtilities/help lemmas.β€Ί

lemma helper_I2_proj_fst_proj_snd_iff: 
  "(βˆ€j∈∘2β„•. Ο€'⦇NTMapβ¦ˆβ¦‡j⦈ = π⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aβ„­ f') ⟷
    (proj_fst Ο€' = proj_fst Ο€ ∘Aβ„­ f' ∧ proj_snd Ο€' = proj_snd Ο€ ∘Aβ„­ f')" 
  unfolding two by auto

lemma helper_I2_proj_fst_proj_snd_iff': 
  "(βˆ€j∈∘2β„•. Ο€'⦇NTMapβ¦ˆβ¦‡j⦈ = f' ∘Aβ„­ π⦇NTMapβ¦ˆβ¦‡j⦈) ⟷
    (proj_fst Ο€' = f' ∘Aβ„­ proj_fst Ο€ ∧ proj_snd Ο€' = f' ∘Aβ„­ proj_snd Ο€)" 
  unfolding two by auto


subsubsectionβ€ΉUniversal propertyβ€Ί

lemma (in is_cat_obj_prod_2) cat_obj_prod_2_unique_cone':
  assumes "Ο€' : P' <CF.cone :β†’: (2β„•) (if2 a b) β„­ : :C (2β„•) ↦↦CΞ± β„­"
  shows
    "βˆƒ!f'. f' : P' ↦ℭ P ∧
      proj_fst Ο€' = proj_fst Ο€ ∘Aβ„­ f' ∧
      proj_snd Ο€' = proj_snd Ο€ ∘Aβ„­ f'"
  by 
    (
      rule cat_obj_prod_unique_cone'[
        OF assms, unfolded helper_I2_proj_fst_proj_snd_iff
        ]
    )

lemma (in is_cat_obj_prod_2) cat_obj_prod_2_unique:
  assumes "Ο€' : P' <CF.Γ— {a,b} : 2C ↦↦CΞ± β„­"
  shows "βˆƒ!f'. f' : P' ↦ℭ P ∧ Ο€' = Ο€ βˆ™NTCF ntcf_const (:C (2β„•)) β„­ f'"
  by (rule cat_obj_prod_unique[OF is_cat_obj_prod_2D[OF assms]])

lemma (in is_cat_obj_prod_2) cat_obj_prod_2_unique':
  assumes "Ο€' : P' <CF.Γ— {a,b} : 2C ↦↦CΞ± β„­"
  shows
    "βˆƒ!f'. f' : P' ↦ℭ P ∧
      proj_fst Ο€' = proj_fst Ο€ ∘Aβ„­ f' ∧
      proj_snd Ο€' = proj_snd Ο€ ∘Aβ„­ f'"
  by 
    (
      rule cat_obj_prod_unique'[
        OF is_cat_obj_prod_2D[OF assms], 
        unfolded helper_I2_proj_fst_proj_snd_iff
        ]
    )

lemma (in is_cat_obj_coprod_2) cat_obj_coprod_2_unique_cocone':
  assumes "Ο€' : :β†’: (2β„•) (if2 a b) β„­ >CF.cocone P' : :C (2β„•) ↦↦CΞ± β„­"
  shows
    "βˆƒ!f'. f' : P ↦ℭ P' ∧
      proj_fst Ο€' = f' ∘Aβ„­ proj_fst Ο€ ∧
      proj_snd Ο€' = f' ∘Aβ„­ proj_snd Ο€"
  by 
    (
      rule cat_obj_coprod_unique_cocone'[
        OF assms, unfolded helper_I2_proj_fst_proj_snd_iff'
        ]
    )

lemma (in is_cat_obj_coprod_2) cat_obj_coprod_2_unique:
  assumes "Ο€' : {a,b} >CF.⊎ P' : 2C ↦↦CΞ± β„­"
  shows "βˆƒ!f'. f' : P ↦ℭ P' ∧ Ο€' = ntcf_const (:C (2β„•)) β„­ f' βˆ™NTCF Ο€"
  by (rule cat_obj_coprod_unique[OF is_cat_obj_coprod_2D[OF assms]])

lemma (in is_cat_obj_coprod_2) cat_obj_coprod_2_unique':
  assumes "Ο€' : {a,b} >CF.⊎ P' : 2C ↦↦CΞ± β„­"
  shows
    "βˆƒ!f'. f' : P ↦ℭ P' ∧
      proj_fst Ο€' = f' ∘Aβ„­ proj_fst Ο€ ∧
      proj_snd Ο€' = f' ∘Aβ„­ proj_snd Ο€"
  by 
    (
      rule cat_obj_coprod_unique'[
        OF is_cat_obj_coprod_2D[OF assms], 
        unfolded helper_I2_proj_fst_proj_snd_iff'
        ]
    )

lemma cat_obj_prod_2_ex_is_arr_isomorphism:
  assumes "Ο€ : P <CF.Γ— {a,b} : 2C ↦↦CΞ± β„­" 
    and "Ο€' : P' <CF.Γ— {a,b} : 2C ↦↦CΞ± β„­"
  obtains f where "f : P' ↦isoβ„­ P" and "Ο€' = Ο€ βˆ™NTCF ntcf_const (:C (2β„•)) β„­ f"
proof-
  interpret Ο€: is_cat_obj_prod_2 Ξ± a b β„­ P Ο€ by (rule assms(1))
  interpret Ο€': is_cat_obj_prod_2 Ξ± a b β„­ P' Ο€' by (rule assms(2))
  from that show ?thesis
    by 
      (
        elim cat_obj_prod_ex_is_arr_isomorphism[
          OF Ο€.is_cat_obj_prod_axioms Ο€'.is_cat_obj_prod_axioms
          ]
      )
qed

lemma cat_obj_coprod_2_ex_is_arr_isomorphism:
  assumes "Ο€ : {a,b} >CF.⊎ U : 2C ↦↦CΞ± β„­" 
    and "Ο€' : {a,b} >CF.⊎ U' : 2C ↦↦CΞ± β„­"
  obtains f where "f : U ↦isoβ„­ U'" and "Ο€' = ntcf_const (:C (2β„•)) β„­ f βˆ™NTCF Ο€"
proof-
  interpret Ο€: is_cat_obj_coprod_2 Ξ± a b β„­ U Ο€ by (rule assms(1))
  interpret Ο€': is_cat_obj_coprod_2 Ξ± a b β„­ U' Ο€' by (rule assms(2))
  from that show ?thesis
    by 
      (
        elim cat_obj_coprod_ex_is_arr_isomorphism[
          OF Ο€.is_cat_obj_coprod_axioms Ο€'.is_cat_obj_coprod_axioms
          ]
      )
qed



subsectionβ€ΉPullbacks and pushoutsβ€Ί


subsubsectionβ€ΉDefinition and elementary propertiesβ€Ί


textβ€Ή
The definitions and the elementary properties of the pullbacks and the 
pushouts can be found, for example, in Chapter III-3 and Chapter III-4 in 
\cite{mac_lane_categories_2010}. 
β€Ί

locale is_cat_pullback =
  is_cat_limit Ξ± β€Ήβ†’βˆ™β†Cβ€Ί β„­ β€ΉβŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­β€Ί X x + 
  cf_scospan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­
  for Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X x 

syntax "_is_cat_pullback" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ <CF.pb _β†’_β†’_←_←_ ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51, 51, 51, 51] 51)
translations "x : X <CF.pb π”žβ†’π”€β†’π”¬β†π”£β†π”Ÿ ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_pullback Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X x"
                        
locale is_cat_pushout =
  is_cat_colimit Ξ± β€Ήβ†βˆ™β†’Cβ€Ί β„­ β€ΉβŸ¨π”žβ†π”€β†π”¬β†’π”£β†’π”ŸβŸ©CFβ„­β€Ί X x +
  cf_sspan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­
  for Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X x

syntax "_is_cat_pushout" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _←_←_β†’_β†’_ >CF.po _ ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51, 51, 51, 51] 51)
translations "x : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_pushout Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X x"


textβ€ΉRules.β€Ί

lemma (in is_cat_pullback) is_cat_pullback_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±"
    and "π”ž' = π”ž"
    and "𝔀' = 𝔀"
    and "𝔬' = 𝔬"
    and "𝔣' = 𝔣"
    and "π”Ÿ' = π”Ÿ"
    and "β„­' = β„­"
    and "X' = X"
  shows "x : X' <CF.pb π”ž'→𝔀'→𝔬'←𝔣'β†π”Ÿ' ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_pullback_axioms)

mk_ide rf is_cat_pullback_def
  |intro is_cat_pullbackI|
  |dest is_cat_pullbackD[dest]|
  |elim is_cat_pullbackE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_pullbackD

lemma (in is_cat_pushout) is_cat_pushout_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±"
    and "π”ž' = π”ž"
    and "𝔀' = 𝔀"
    and "𝔬' = 𝔬"
    and "𝔣' = 𝔣"
    and "π”Ÿ' = π”Ÿ"
    and "β„­' = β„­"
    and "X' = X"
  shows "x : π”ž'←𝔀'←𝔬'→𝔣'β†’π”Ÿ' >CF.po X' ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_pushout_axioms)

mk_ide rf is_cat_pushout_def
  |intro is_cat_pushoutI|
  |dest is_cat_pushoutD[dest]|
  |elim is_cat_pushoutE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_pushoutD


textβ€ΉDuality.β€Ί

lemma (in is_cat_pullback) is_cat_pushout_op:
  "op_ntcf x : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X ↦↦CΞ± op_cat β„­"
  by (intro is_cat_pushoutI) 
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_op_intros)+

lemma (in is_cat_pullback) is_cat_pushout_op'[cat_op_intros]:
  assumes "β„­' = op_cat β„­"
  shows "op_ntcf x : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_pushout_op)

lemmas [cat_op_intros] = is_cat_pullback.is_cat_pushout_op'

lemma (in is_cat_pushout) is_cat_pullback_op:
  "op_ntcf x : X <CF.pb π”žβ†’π”€β†’π”¬β†π”£β†π”Ÿ ↦↦CΞ± op_cat β„­"
  by (intro is_cat_pullbackI) 
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_op_intros)+

lemma (in is_cat_pushout) is_cat_pullback_op'[cat_op_intros]:
  assumes "β„­' = op_cat β„­"
  shows "op_ntcf x : X <CF.pb π”žβ†’π”€β†’π”¬β†π”£β†π”Ÿ ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_pullback_op)

lemmas [cat_op_intros] = is_cat_pushout.is_cat_pullback_op'


textβ€ΉElementary properties.β€Ί

lemma cat_cone_cospan:
  assumes "x : X <CF.cone βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­ : β†’βˆ™β†C ↦↦CΞ± β„­"
    and "cf_scospan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­"
  shows "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = 𝔀 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈"
    and "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = 𝔣 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈"
    and "𝔀 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = 𝔣 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈"
proof-
  interpret x: is_cat_cone Ξ± X β€Ήβ†’βˆ™β†Cβ€Ί β„­ β€ΉβŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­β€Ί x 
    by (rule assms(1))
  interpret cospan: cf_scospan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ by (rule assms(2))
  have 𝔀SS: "𝔀SS : π”žSS β†¦β†’βˆ™β†C 𝔬SS" and 𝔣SS: "𝔣SS : π”ŸSS β†¦β†’βˆ™β†C 𝔬SS" 
    by (cs_concl cs_simp: cs_intro: cat_ss_cs_intros)+
  from x.ntcf_Comp_commute[OF 𝔀SS] 𝔀SS 𝔣SS show
    "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = 𝔀 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈"
    by (cs_prems cs_simp: cat_ss_cs_simps cat_cs_simps cs_intro: cat_cs_intros)
  moreover from x.ntcf_Comp_commute[OF 𝔣SS] 𝔀SS 𝔣SS show 
    "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = 𝔣 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈"
    by (cs_prems cs_simp: cat_ss_cs_simps cat_cs_simps cs_intro: cat_cs_intros)
  ultimately show "𝔀 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = 𝔣 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈" by simp
qed

lemma (in is_cat_pullback) cat_pb_cone_cospan:
  shows "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = 𝔀 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈"
    and "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = 𝔣 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈"
    and "𝔀 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = 𝔣 ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈"
  by (allβ€Ήrule cat_cone_cospan[OF is_cat_cone_axioms cf_scospan_axioms]β€Ί)

lemma cat_cocone_span:
  assumes "x : βŸ¨π”žβ†π”€β†π”¬β†’π”£β†’π”ŸβŸ©CFβ„­ >CF.cocone X : β†βˆ™β†’C ↦↦CΞ± β„­"
    and "cf_sspan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­"
  shows "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ 𝔀"
    and "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ 𝔣"
    and "x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ 𝔀 = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ 𝔣"
proof-
  interpret x: is_cat_cocone Ξ± X β€Ήβ†βˆ™β†’Cβ€Ί β„­ β€ΉβŸ¨π”žβ†π”€β†π”¬β†’π”£β†’π”ŸβŸ©CFβ„­β€Ί x
    by (rule assms(1))
  interpret span: cf_sspan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ by (rule assms(2))
  note op = 
    cat_cone_cospan
      [
        OF 
          x.is_cat_cone_op[unfolded cat_op_simps] 
          span.cf_scospan_op, 
          unfolded cat_op_simps
      ]
  from op(1) show "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ 𝔀"
    by 
      (
        cs_prems 
          cs_simp: cat_ss_cs_simps cat_op_simps 
          cs_intro: cat_cs_intros cat_ss_cs_intros
      )
  moreover from op(2) show "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ 𝔣"
    by 
      (
        cs_prems 
          cs_simp: cat_ss_cs_simps cat_op_simps 
          cs_intro: cat_cs_intros cat_ss_cs_intros
      )
  ultimately show "x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ 𝔀 = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ 𝔣" by auto
qed

lemma (in is_cat_pushout) cat_po_cocone_span:
  shows "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ 𝔀"
    and "x⦇NTMapβ¦ˆβ¦‡π”¬SS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ 𝔣"
    and "x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ 𝔀 = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ 𝔣"
  by (allβ€Ήrule cat_cocone_span[OF is_cat_cocone_axioms cf_sspan_axioms]β€Ί)


subsubsectionβ€ΉUniversal propertyβ€Ί

lemma is_cat_pullbackI':
  assumes "x : X <CF.cone βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­ : β†’βˆ™β†C ↦↦CΞ± β„­"
    and "cf_scospan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­"
    and "β‹€x' X'.
      x' : X' <CF.cone βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­ : β†’βˆ™β†C ↦↦CΞ± β„­ ⟹
        βˆƒ!f'.
          f' : X' ↦ℭ X ∧
          x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ f' ∧
          x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ f'"
  shows "x : X <CF.pb π”žβ†’π”€β†’π”¬β†π”£β†π”Ÿ ↦↦CΞ± β„­"
proof(intro is_cat_pullbackI is_cat_limitI')

  show "x : X <CF.cone βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­ : β†’βˆ™β†C ↦↦CΞ± β„­" 
    by (rule assms(1))
  interpret x: is_cat_cone Ξ± X β€Ήβ†’βˆ™β†Cβ€Ί β„­ β€ΉβŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­β€Ί x 
    by (rule assms(1))
  show "cf_scospan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­" by (rule assms(2))
  interpret cospan: cf_scospan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ by (rule assms(2))

  fix u' r' assume prems:
    "u' : r' <CF.cone βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­ : β†’βˆ™β†C ↦↦CΞ± β„­"

  interpret u': is_cat_cone Ξ± r' β€Ήβ†’βˆ™β†Cβ€Ί β„­ β€ΉβŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­β€Ί u' 
    by (rule prems)

  from assms(3)[OF prems] obtain f' 
    where f': "f' : r' ↦ℭ X"
      and u'_π”žSS: "u'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ f'"
      and u'_π”ŸSS: "u'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ f'"
      and unique_f': "β‹€f''.
        ⟦
          f'' : r' ↦ℭ X;
          u'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ f'';
          u'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ f''
        ⟧ ⟹ f'' = f'"
    by metis

  show "βˆƒ!f'. f' : r' ↦ℭ X ∧ u' = x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f'"
  proof(intro ex1I conjI; (elim conjE)?)

    show "u' = x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f'"
    proof(rule ntcf_eqI)
      show "u' : cf_const β†’βˆ™β†C β„­ r' ↦CF βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­ : β†’βˆ™β†C ↦↦CΞ± β„­"
        by (rule u'.is_ntcf_axioms)
      from f' show 
        "x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f' :
          cf_const β†’βˆ™β†C β„­ r' ↦CF βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­ :
          β†’βˆ™β†C ↦↦CΞ± β„­"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      from f' have dom_rhs: 
        "π’Ÿβˆ˜ ((x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f')⦇NTMap⦈) = β†’βˆ™β†C⦇Obj⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      show "u'⦇NTMap⦈ = (x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f')⦇NTMap⦈"
      proof(rule vsv_eqI, unfold cat_cs_simps dom_rhs)
        fix a assume prems': "a ∈∘ β†’βˆ™β†C⦇Obj⦈"
        from this f' x.is_ntcf_axioms show
          "u'⦇NTMapβ¦ˆβ¦‡a⦈ = (x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f')⦇NTMapβ¦ˆβ¦‡a⦈"
          by (elim the_cat_scospan_ObjE; simp only:)
            (
              cs_concl
                cs_simp:
                  cat_cs_simps cat_ss_cs_simps 
                  u'_π”ŸSS u'_π”žSS 
                  cat_cone_cospan(1)[OF assms(1,2)] 
                  cat_cone_cospan(1)[OF prems assms(2)] 
                cs_intro: cat_cs_intros cat_ss_cs_intros
            )+
      qed (cs_concl cs_intro: cat_cs_intros | auto)+
    qed simp_all

    fix f'' assume prems: 
      "f'' : r' ↦ℭ X" "u' = x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f''"
    have π”žSS: "π”žSS ∈∘ β†’βˆ™β†C⦇Obj⦈" and π”ŸSS: "π”ŸSS ∈∘ β†’βˆ™β†C⦇Obj⦈" 
      by (cs_concl cs_simp: cs_intro: cat_ss_cs_intros)+
    have "u'⦇NTMapβ¦ˆβ¦‡a⦈ = x⦇NTMapβ¦ˆβ¦‡a⦈ ∘Aβ„­ f''" if "a ∈∘ β†’βˆ™β†C⦇Obj⦈" for a
    proof-
      from prems(2) have 
        "u'⦇NTMapβ¦ˆβ¦‡a⦈ = (x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f'')⦇NTMapβ¦ˆβ¦‡a⦈"
        by simp
      from this that prems(1) show "u'⦇NTMapβ¦ˆβ¦‡a⦈ = x⦇NTMapβ¦ˆβ¦‡a⦈ ∘Aβ„­ f''"
        by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed
    from unique_f'[OF prems(1) this[OF π”žSS] this[OF π”ŸSS]] show "f'' = f'".

  qed (intro f')

qed

lemma is_cat_pushoutI':
  assumes "x : βŸ¨π”žβ†π”€β†π”¬β†’π”£β†’π”ŸβŸ©CFβ„­ >CF.cocone X : β†βˆ™β†’C ↦↦CΞ± β„­"
    and "cf_sspan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­"
    and "β‹€x' X'. x' : βŸ¨π”žβ†π”€β†π”¬β†’π”£β†’π”ŸβŸ©CFβ„­ >CF.cocone X' : β†βˆ™β†’C ↦↦CΞ± β„­ ⟹
      βˆƒ!f'.
        f' : X ↦ℭ X' ∧
        x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = f' ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∧
        x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = f' ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈"
  shows "x : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X ↦↦CΞ± β„­"
proof-
  interpret x: is_cat_cocone Ξ± X β€Ήβ†βˆ™β†’Cβ€Ί β„­ β€ΉβŸ¨π”žβ†π”€β†π”¬β†’π”£β†’π”ŸβŸ©CFβ„­β€Ί x 
    by (rule assms(1))
  interpret span: cf_sspan Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ by (rule assms(2))
  have assms_3': 
    "βˆƒ!f'.
      f' : X ↦ℭ X' ∧
      x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aop_cat β„­ f' ∧
      x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aop_cat β„­ f'"
    if "x' : X' <CF.cone βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFop_cat β„­ : β†’βˆ™β†C ↦↦CΞ± op_cat β„­"
    for x' X'
  proof-
    from that(1) have [cat_op_simps]:
      "f' : X ↦ℭ X' ∧ 
      x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aop_cat β„­ f' ∧
      x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aop_cat β„­ f' ⟷
        f' : X ↦ℭ X' ∧
        x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = f' ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∧
        x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = f' ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈" 
      for f'
      by (intro iffI conjI; (elim conjE)?)
        (
          cs_concl 
            cs_simp: category.op_cat_Comp[symmetric] cat_op_simps cat_cs_simps 
            cs_intro: cat_cs_intros cat_ss_cs_intros
        )+
    interpret x': 
      is_cat_cone Ξ± X' β€Ήβ†’βˆ™β†Cβ€Ί β€Ήop_cat β„­β€Ί β€ΉβŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFop_cat β„­β€Ί x'
      by (rule that)
    show ?thesis
      unfolding cat_op_simps
      by 
        (
          rule assms(3)[
            OF x'.is_cat_cocone_op[unfolded cat_op_simps], 
            unfolded cat_op_simps
            ]
        )
  qed
  interpret op_x: is_cat_pullback Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β€Ήop_cat β„­β€Ί X β€Ήop_ntcf xβ€Ί 
    using 
      is_cat_pullbackI'
        [
          OF x.is_cat_cone_op[unfolded cat_op_simps] 
          span.cf_scospan_op, 
          unfolded cat_op_simps, 
          OF assms_3'
        ]
    by simp
  show "x : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X ↦↦CΞ± β„­"
    by (rule op_x.is_cat_pushout_op[unfolded cat_op_simps])
qed
                   
lemma (in is_cat_pullback) cat_pb_unique_cone:
  assumes "x' : X' <CF.cone βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­ : β†’βˆ™β†C ↦↦CΞ± β„­"
  shows "βˆƒ!f'.
    f' : X' ↦ℭ X ∧
    x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ f' ∧
    x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ f'"
proof-
  interpret x': is_cat_cone Ξ± X' β€Ήβ†’βˆ™β†Cβ€Ί β„­ β€ΉβŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­β€Ί x' 
    by (rule assms)
  from cat_lim_unique_cone[OF assms] obtain f'
    where f': "f' : X' ↦ℭ X" 
      and x'_def: "x' = x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f'"
      and unique_f': "β‹€f''.
        ⟦ f'' : X' ↦ℭ X; x' = x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f'' ⟧ ⟹
        f'' = f'"
    by auto
  have π”žSS: "π”žSS ∈∘ β†’βˆ™β†C⦇Obj⦈" and π”ŸSS: "π”ŸSS ∈∘ β†’βˆ™β†C⦇Obj⦈"
    by (cs_concl cs_intro: cat_ss_cs_intros)+
  show ?thesis
  proof(intro ex1I conjI; (elim conjE)?)
    show "f' : X' ↦ℭ X" by (rule f')
    have "x'⦇NTMapβ¦ˆβ¦‡a⦈ = x⦇NTMapβ¦ˆβ¦‡a⦈ ∘Aβ„­ f'" if "a ∈∘ β†’βˆ™β†C⦇Obj⦈" for a
    proof-
      from x'_def have 
        "x'⦇NTMapβ¦ˆβ¦‡a⦈ = (x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f')⦇NTMapβ¦ˆβ¦‡a⦈"
        by simp
      from this that f' show "x'⦇NTMapβ¦ˆβ¦‡a⦈ = x⦇NTMapβ¦ˆβ¦‡a⦈ ∘Aβ„­ f'"
        by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed
    from this[OF π”žSS] this[OF π”ŸSS] show 
      "x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ f'"
      "x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ f'"
      by auto
    fix f'' assume prems': 
      "f'' : X' ↦ℭ X"
      "x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ f''"
      "x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ f''"
    have "x' = x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f''"
    proof(rule ntcf_eqI)
      show "x' : cf_const β†’βˆ™β†C β„­ X' ↦CF βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­ : β†’βˆ™β†C ↦↦CΞ± β„­"
        by (rule x'.is_ntcf_axioms)
      from prems'(1) show
        "x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f'' :
          cf_const β†’βˆ™β†C β„­ X' ↦CF βŸ¨π”žβ†’π”€β†’π”¬β†π”£β†π”ŸβŸ©CFβ„­ :
          β†’βˆ™β†C ↦↦CΞ± β„­"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      have dom_lhs: "π’Ÿβˆ˜ (x'⦇NTMap⦈) = β†’βˆ™β†C⦇Obj⦈" 
        by (cs_concl cs_simp: cat_cs_simps)
      from prems'(1) have dom_rhs:
        "π’Ÿβˆ˜ ((x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f'')⦇NTMap⦈) = β†’βˆ™β†C⦇Obj⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      show "x'⦇NTMap⦈ = (x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f'')⦇NTMap⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix a assume prems'': "a ∈∘ β†’βˆ™β†C⦇Obj⦈"
        from this prems'(1) show 
          "x'⦇NTMapβ¦ˆβ¦‡a⦈ = (x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f'')⦇NTMapβ¦ˆβ¦‡a⦈"
          by (elim the_cat_scospan_ObjE; simp only:)
            (
              cs_concl 
                cs_simp: 
                  prems'(2,3)
                  cat_cone_cospan(1,2)[OF assms cf_scospan_axioms] 
                  cat_pb_cone_cospan 
                  cat_ss_cs_simps cat_cs_simps 
                cs_intro: cat_ss_cs_intros cat_cs_intros
            )+
      qed (auto simp: cat_cs_intros)
    qed simp_all
    from unique_f'[OF prems'(1) this] show "f'' = f'".
  qed
qed

lemma (in is_cat_pullback) cat_pb_unique:
  assumes "x' : X' <CF.pb π”žβ†’π”€β†’π”¬β†π”£β†π”Ÿ ↦↦CΞ± β„­"
  shows "βˆƒ!f'. f' : X' ↦ℭ X ∧ x' = x βˆ™NTCF ntcf_const β†’βˆ™β†C β„­ f'"
  by (rule cat_lim_unique[OF is_cat_pullbackD(1)[OF assms]])

lemma (in is_cat_pullback) cat_pb_unique':
  assumes "x' : X' <CF.pb π”žβ†’π”€β†’π”¬β†π”£β†π”Ÿ ↦↦CΞ± β„­"
  shows "βˆƒ!f'.
    f' : X' ↦ℭ X ∧
    x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ f' ∧
    x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ f'"
proof-
  interpret x': is_cat_pullback Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X' x' by (rule assms(1))
  show ?thesis by (rule cat_pb_unique_cone[OF x'.is_cat_cone_axioms])
qed

lemma (in is_cat_pushout) cat_po_unique_cocone:
  assumes "x' : βŸ¨π”žβ†π”€β†π”¬β†’π”£β†’π”ŸβŸ©CFβ„­ >CF.cocone X' : β†βˆ™β†’C ↦↦CΞ± β„­"
  shows "βˆƒ!f'.
    f' : X ↦ℭ X' ∧
    x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = f' ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∧
    x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = f' ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈"
proof-
  interpret x': is_cat_cocone Ξ± X' β€Ήβ†βˆ™β†’Cβ€Ί β„­ β€ΉβŸ¨π”žβ†π”€β†π”¬β†’π”£β†’π”ŸβŸ©CFβ„­β€Ί x'
    by (rule assms(1))
  have [cat_op_simps]:
    "f' : X ↦ℭ X' ∧
    x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aop_cat β„­ f' ∧
    x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aop_cat β„­ f' ⟷
      f' : X ↦ℭ X' ∧
      x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = f' ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∧
      x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = f' ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈" 
    for f'
    by (intro iffI conjI; (elim conjE)?)
      (
        cs_concl 
          cs_simp: category.op_cat_Comp[symmetric] cat_op_simps cat_cs_simps  
          cs_intro: cat_cs_intros cat_ss_cs_intros
      )+
  show ?thesis
    by 
      (
        rule is_cat_pullback.cat_pb_unique_cone[
          OF is_cat_pullback_op x'.is_cat_cone_op[unfolded cat_op_simps], 
          unfolded cat_op_simps
          ]
     )
qed

lemma (in is_cat_pushout) cat_po_unique:
  assumes "x' : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X' ↦↦CΞ± β„­"
  shows "βˆƒ!f'. f' : X ↦ℭ X' ∧ x' = ntcf_const β†βˆ™β†’C β„­ f' βˆ™NTCF x"
  by (rule cat_colim_unique[OF is_cat_pushoutD(1)[OF assms]])

lemma (in is_cat_pushout) cat_po_unique':
  assumes "x' : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X' ↦↦CΞ± β„­"
  shows "βˆƒ!f'.
    f' : X ↦ℭ X' ∧
    x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = f' ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∧
    x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = f' ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈"
proof-
  interpret x': is_cat_pushout Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X' x' by (rule assms(1))
  show ?thesis by (rule cat_po_unique_cocone[OF x'.is_cat_cocone_axioms])
qed

lemma cat_pullback_ex_is_arr_isomorphism:
  assumes "x : X <CF.pb π”žβ†’π”€β†’π”¬β†π”£β†π”Ÿ ↦↦CΞ± β„­"
    and "x' : X' <CF.pb π”žβ†’π”€β†’π”¬β†π”£β†π”Ÿ ↦↦CΞ± β„­"
  obtains f where "f : X' ↦isoβ„­ X" 
    and "x' = x βˆ™NTCF ntcf_const β†’βˆ™β†C  β„­ f"
proof-
  interpret x: is_cat_pullback Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X x by (rule assms(1))
  interpret x': is_cat_pullback Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X' x' by (rule assms(2))
  from that show ?thesis
    by 
      (
        elim cat_lim_ex_is_arr_isomorphism[
          OF x.is_cat_limit_axioms x'.is_cat_limit_axioms
          ]
      )
qed

lemma cat_pullback_ex_is_arr_isomorphism':
  assumes "x : X <CF.pb π”žβ†’π”€β†’π”¬β†π”£β†π”Ÿ ↦↦CΞ± β„­"
    and "x' : X' <CF.pb π”žβ†’π”€β†’π”¬β†π”£β†π”Ÿ ↦↦CΞ± β„­"
  obtains f where "f : X' ↦isoβ„­ X" 
    and "x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ f"
    and "x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ f"
proof-
  interpret x: is_cat_pullback Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X x by (rule assms(1))
  interpret x': is_cat_pullback Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X' x' by (rule assms(2))
  obtain f where f: "f : X' ↦isoβ„­ X"
    and "j ∈∘ β†’βˆ™β†C⦇Obj⦈ ⟹ x'⦇NTMapβ¦ˆβ¦‡j⦈ = x⦇NTMapβ¦ˆβ¦‡j⦈ ∘Aβ„­ f" for j
    by 
      (
        elim cat_lim_ex_is_arr_isomorphism'[
          OF x.is_cat_limit_axioms x'.is_cat_limit_axioms
          ]
      )
  then have 
    "x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”žSS⦈ ∘Aβ„­ f" 
    "x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ ∘Aβ„­ f"
    by (auto simp: cat_ss_cs_intros)
  with f show ?thesis using that by simp
qed

lemma cat_pushout_ex_is_arr_isomorphism:
  assumes "x : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X ↦↦CΞ± β„­"
    and "x' : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X' ↦↦CΞ± β„­"
  obtains f where "f : X ↦isoβ„­ X'" 
    and "x' = ntcf_const β†βˆ™β†’C β„­ f βˆ™NTCF x"
proof-
  interpret x: is_cat_pushout Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X x by (rule assms(1))
  interpret x': is_cat_pushout Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X' x' by (rule assms(2))
  from that show ?thesis
    by 
      (
        elim cat_colim_ex_is_arr_isomorphism[
          OF x.is_cat_colimit_axioms x'.is_cat_colimit_axioms
          ]
      )
qed

lemma cat_pushout_ex_is_arr_isomorphism':
  assumes "x : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X ↦↦CΞ± β„­"
    and "x' : π”žβ†π”€β†π”¬β†’π”£β†’π”Ÿ >CF.po X' ↦↦CΞ± β„­"
  obtains f where "f : X ↦isoβ„­ X'" 
    and "x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = f ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈"
    and "x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = f ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈"
proof-
  interpret x: is_cat_pushout Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X x by (rule assms(1))
  interpret x': is_cat_pushout Ξ± π”ž 𝔀 𝔬 𝔣 π”Ÿ β„­ X' x' by (rule assms(2))
  obtain f where f: "f : X ↦isoβ„­ X'"
    and "j ∈∘ β†βˆ™β†’C⦇Obj⦈ ⟹ x'⦇NTMapβ¦ˆβ¦‡j⦈ = f ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡j⦈" for j
    by 
      (
        elim cat_colim_ex_is_arr_isomorphism'[
          OF x.is_cat_colimit_axioms x'.is_cat_colimit_axioms,
          unfolded the_cat_parallel_components(1)
          ]
      )
  then have "x'⦇NTMapβ¦ˆβ¦‡π”žSS⦈ = f ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”žSS⦈"
    and "x'⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈ = f ∘Aβ„­ x⦇NTMapβ¦ˆβ¦‡π”ŸSS⦈"
    by (auto simp: cat_ss_cs_intros)
  with f show ?thesis using that by simp
qed



subsectionβ€ΉEqualizers and coequalizersβ€Ί


subsubsectionβ€ΉDefinition and elementary propertiesβ€Ί


textβ€Ή
See \cite{noauthor_wikipedia_2001}\footnote{
\url{https://en.wikipedia.org/wiki/Equaliser_(mathematics)}
}.
β€Ί

locale is_cat_equalizer =
  is_cat_limit Ξ± ‹↑↑C π”žPL π”ŸPL 𝔀PL 𝔣PLβ€Ί β„­ ‹↑↑→↑↑ β„­ π”žPL π”ŸPL 𝔀PL 𝔣PL π”ž π”Ÿ 𝔀 𝔣› E Ξ΅ 
  for Ξ± π”ž π”Ÿ 𝔀 𝔣 β„­ E Ξ΅ +
  assumes cat_eq_𝔀[cat_lim_cs_intros]: "𝔀 : π”ž ↦ℭ π”Ÿ"
    and cat_eq_𝔣[cat_lim_cs_intros]: "𝔣 : π”ž ↦ℭ π”Ÿ"

syntax "_is_cat_equalizer" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ _ <CF.eq '(_,_,_,_') :/ ↑↑2C ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51, 51] 51)
translations "Ξ΅ : E <CF.eq (π”ž,π”Ÿ,𝔀,𝔣) : ↑↑2C ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_equalizer Ξ± π”ž π”Ÿ 𝔀 𝔣 β„­ E Ξ΅"

locale is_cat_coequalizer =
  is_cat_colimit Ξ± ‹↑↑C π”ŸPL π”žPL 𝔣PL 𝔀PLβ€Ί β„­ ‹↑↑→↑↑ β„­ π”ŸPL π”žPL 𝔣PL 𝔀PL π”Ÿ π”ž 𝔣 𝔀› E Ξ΅ 
  for Ξ± π”ž π”Ÿ 𝔀 𝔣 β„­ E Ξ΅ +
  assumes cat_coeq_𝔀[cat_lim_cs_intros]: "𝔀 : π”Ÿ ↦ℭ π”ž"
    and cat_coeq_𝔣[cat_lim_cs_intros]: "𝔣 : π”Ÿ ↦ℭ π”ž"

syntax "_is_cat_coequalizer" :: "V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ V β‡’ bool"
  (β€Ή(_ :/ '(_,_,_,_') >CF.coeq _ :/ ↑↑2C ↦↦CΔ± _)β€Ί [51, 51, 51, 51, 51, 51] 51)
translations "Ξ΅ : (π”ž,π”Ÿ,𝔀,𝔣) >CF.coeq E : ↑↑2C ↦↦CΞ± β„­" β‡Œ 
  "CONST is_cat_coequalizer Ξ± π”ž π”Ÿ 𝔀 𝔣 β„­ E Ξ΅"


textβ€ΉRules.β€Ί

lemma (in is_cat_equalizer) is_cat_equalizer_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±"
    and "E' = E"
    and "π”ž' = π”ž"
    and "π”Ÿ' = π”Ÿ"
    and "𝔀' = 𝔀"
    and "𝔣' = 𝔣"
    and "β„­' = β„­"
  shows "Ξ΅ : E' <CF.eq (π”ž',π”Ÿ',𝔀',𝔣') : ↑↑2C ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_equalizer_axioms)

mk_ide rf is_cat_equalizer_def[unfolded is_cat_equalizer_axioms_def]
  |intro is_cat_equalizerI|
  |dest is_cat_equalizerD[dest]|
  |elim is_cat_equalizerE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_equalizerD(1)

lemma (in is_cat_coequalizer) is_cat_coequalizer_axioms'[cat_lim_cs_intros]:
  assumes "Ξ±' = Ξ±"
    and "E' = E"
    and "π”ž' = π”ž"
    and "π”Ÿ' = π”Ÿ"
    and "𝔀' = 𝔀"
    and "𝔣' = 𝔣"
    and "β„­' = β„­"
  shows "Ξ΅ : (π”ž',π”Ÿ',𝔀',𝔣') >CF.coeq E' : ↑↑2C ↦↦CΞ±' β„­'"
  unfolding assms by (rule is_cat_coequalizer_axioms)

mk_ide rf is_cat_coequalizer_def[unfolded is_cat_coequalizer_axioms_def]
  |intro is_cat_coequalizerI|
  |dest is_cat_coequalizerD[dest]|
  |elim is_cat_coequalizerE[elim]|

lemmas [cat_lim_cs_intros] = is_cat_coequalizerD(1)


textβ€ΉElementary properties.β€Ί

sublocale is_cat_equalizer βŠ† cf_parallel Ξ± π”žPL π”ŸPL 𝔀PL 𝔣PL π”ž π”Ÿ 𝔀 𝔣 β„­ 
  by (intro cf_parallelI cat_parallelI)
    (simp_all add: cat_parallel_cs_intros cat_lim_cs_intros cat_cs_intros)

sublocale is_cat_coequalizer βŠ† cf_parallel Ξ± π”ŸPL π”žPL 𝔣PL 𝔀PL π”Ÿ π”ž 𝔣 𝔀 β„­
  by (intro cf_parallelI cat_parallelI)
    (
      simp_all add: 
        cat_parallel_cs_intros cat_lim_cs_intros cat_cs_intros 
        cat_PL_ineq[symmetric]
    )


textβ€ΉDuality.β€Ί

lemma (in is_cat_equalizer) is_cat_coequalizer_op:
  "op_ntcf Ξ΅ : (π”ž,π”Ÿ,𝔀,𝔣) >CF.coeq E : ↑↑2C ↦↦CΞ± op_cat β„­"
  by (intro is_cat_coequalizerI)
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_op_intros cat_lim_cs_intros)+

lemma (in is_cat_equalizer) is_cat_coequalizer_op'[cat_op_intros]:
  assumes "β„­' = op_cat β„­"
  shows "op_ntcf Ξ΅ : (π”ž,π”Ÿ,𝔀,𝔣) >CF.coeq E : ↑↑2C ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_coequalizer_op)

lemmas [cat_op_intros] = is_cat_equalizer.is_cat_coequalizer_op'

lemma (in is_cat_coequalizer) is_cat_equalizer_op:
  "op_ntcf Ξ΅ : E <CF.eq (π”ž,π”Ÿ,𝔀,𝔣) : ↑↑2C ↦↦CΞ± op_cat β„­"
  by (intro is_cat_equalizerI)
    (
      cs_concl
        cs_simp: cat_op_simps
        cs_intro: cat_cs_intros cat_op_intros cat_lim_cs_intros
    )+

lemma (in is_cat_coequalizer) is_cat_equalizer_op'[cat_op_intros]:
  assumes "β„­' = op_cat β„­"
  shows "op_ntcf Ξ΅ : E <CF.eq (π”ž,π”Ÿ,𝔀,𝔣) : ↑↑2C ↦↦CΞ± β„­'"
  unfolding assms by (rule is_cat_equalizer_op)

lemmas [cat_op_intros] = is_cat_coequalizer.is_cat_equalizer_op'


textβ€ΉElementary properties.β€Ί

lemma cf_parallel_if_is_cat_cone:
  assumes "Ξ΅ :
    E <CF.cone ↑↑→↑↑ β„­ π”žPL π”ŸPL 𝔀PL 𝔣PL π”ž π”Ÿ 𝔀 𝔣 : ↑↑C π”žPL π”ŸPL 𝔀PL 𝔣PL ↦↦CΞ± β„­"
    and "𝔀 : π”ž ↦ℭ π”Ÿ"
    and "𝔣 : π”ž ↦ℭ π”Ÿ"
  shows "cf_parallel Ξ± π”žPL π”ŸPL 𝔀PL 𝔣PL π”ž π”Ÿ 𝔀 𝔣 β„­"
proof-
  let ?II = ‹↑↑C π”žPL π”ŸPL 𝔀PL 𝔣PLβ€Ί and ?II_II = ‹↑↑→↑↑ β„­ π”žPL π”ŸPL 𝔀PL 𝔣PL π”ž π”Ÿ 𝔀 𝔣›
  interpret is_cat_cone Ξ± E ?II β„­ ?II_II Ξ΅ by (rule assms(1))
  show ?thesis
    by (intro cf_parallelI cat_parallelI)
      (
        simp_all add: 
          assms cat_parallel_cs_intros cat_lim_cs_intros cat_cs_intros
      )
qed

lemma cf_parallel_if_is_cat_cocone:
  assumes "Ξ΅' :
    ↑↑→↑↑ β„­ π”ŸPL π”žPL 𝔣PL 𝔀PL π”Ÿ π”ž 𝔣 𝔀 >CF.cocone E' : ↑↑C π”ŸPL π”žPL 𝔣PL 𝔀PL ↦↦CΞ± β„­"
    and "𝔀 : π”Ÿ ↦ℭ π”ž"
    and "𝔣 : π”Ÿ ↦ℭ π”ž"
  shows "cf_parallel Ξ± π”ŸPL π”žPL 𝔣PL 𝔀PL π”Ÿ π”ž 𝔣 𝔀 β„­"
proof-
  let ?II = ‹↑↑C π”ŸPL π”žPL 𝔣PL 𝔀PLβ€Ί and ?II_II = ‹↑↑→↑↑ β„­ π”ŸPL π”žPL 𝔣PL 𝔀PL π”Ÿ π”ž 𝔣 𝔀›
  interpret is_cat_cocone Ξ± E' ?II β„­ ?II_II Ξ΅' by (rule assms(1))
  show ?thesis
    by (intro cf_parallelI cat_parallelI)
      (
        simp_all add: 
          assms 
          cat_parallel_cs_intros 
          cat_lim_cs_intros 
          cat_cs_intros
          cat_PL_ineq[symmetric]
      )
qed

lemma (in category) cat_cf_parallel_cat_equalizer: 
  assumes "𝔀 : π”ž ↦ℭ π”Ÿ" and "𝔣 : π”ž ↦ℭ π”Ÿ"
  shows "cf_parallel Ξ± π”žPL π”ŸPL 𝔀PL 𝔣PL π”ž π”Ÿ 𝔀 𝔣 β„­"
  using assms 
  by (intro cf_parallelI cat_parallelI)
    (auto simp: cat_parallel_cs_intros cat_cs_intros)

lemma (in category) cat_cf_parallel_cat_coequalizer: 
  assumes "𝔀 : π”Ÿ ↦ℭ π”ž" and "𝔣 : π”Ÿ ↦ℭ π”ž"
  shows "cf_parallel Ξ± π”ŸPL π”žPL 𝔣PL 𝔀PL π”Ÿ π”ž 𝔣 𝔀 β„­"
  using assms 
  by (intro cf_parallelI cat_parallelI)
    (simp_all add: cat_parallel_cs_intros cat_cs_intros cat_PL_ineq[symmetric])

lemma cat_cone_cf_par_eps_NTMap_app:
  assumes "Ξ΅ :
    E <CF.cone ↑↑→↑↑ β„­ π”žPL π”ŸPL 𝔀PL 𝔣PL π”ž π”Ÿ 𝔀 𝔣 : ↑↑C π”žPL π”ŸPL 𝔀PL 𝔣PL ↦↦CΞ± β„­"
    and "𝔀 : π”ž ↦ℭ π”Ÿ" 
    and "𝔣 : π”ž ↦ℭ π”Ÿ"
  shows 
    "Ρ⦇NTMapβ¦ˆβ¦‡π”ŸPL⦈ = 𝔀 ∘Aβ„­ Ρ⦇NTMapβ¦ˆβ¦‡π”žPL⦈" 
    "Ρ⦇NTMapβ¦ˆβ¦‡π”ŸPL⦈ = 𝔣 ∘Aβ„­ Ρ⦇NTMapβ¦ˆβ¦‡π”žPL⦈"
proof-
  let ?II = ‹↑↑C π”žPL π”ŸPL 𝔀PL 𝔣PLβ€Ί and ?II_II = ‹↑↑→↑↑ β„­ π”žPL π”ŸPL 𝔀PL 𝔣PL π”ž π”Ÿ 𝔀 𝔣›
  interpret Ξ΅: is_cat_cone Ξ± E ?II β„­ ?II_II Ξ΅ by (rule assms(1))
  from assms(2,3) have π”ž: "π”ž ∈∘ ℭ⦇Obj⦈" and π”Ÿ: "π”Ÿ ∈∘ ℭ⦇Obj⦈" by auto
  interpret par: cf_parallel Ξ± π”žPL π”ŸPL 𝔀PL 𝔣PL π”ž π”Ÿ 𝔀 𝔣 β„­ 
    by (intro cf_parallel_if_is_cat_cone, rule assms) (auto intro: assms π”ž π”Ÿ)
  have 𝔀PL: "𝔀PL : π”žPL ↦↑↑C π”žPL π”ŸPL 𝔀PL 𝔣PL π”ŸPL" 
    and 𝔣PL: "𝔣PL : π”žPL ↦↑↑C π”žPL π”ŸPL 𝔀PL 𝔣PL π”ŸPL"
    by 
      (
        simp_all add: 
          par.the_cat_parallel_is_arr_π”žπ”Ÿπ”€ par.the_cat_parallel_is_arr_π”žπ”Ÿπ”£
      )
  from Ξ΅.ntcf_Comp_commute[OF 𝔀PL] show "Ρ⦇NTMapβ¦ˆβ¦‡π”ŸPL⦈ = 𝔀 ∘Aβ„­ Ρ⦇NTMapβ¦ˆβ¦‡π”žPL⦈"
    by (*slow*)
      (
        cs_prems 
          cs_simp: cat_parallel_cs_simps cat_cs_simps 
          cs_intro: cat_cs_intros cat_parallel_cs_intros 
      )
  from Ξ΅.ntcf_Comp_commute[OF 𝔣PL] show "Ρ⦇NTMapβ¦ˆβ¦‡π”ŸPL⦈ = 𝔣 ∘Aβ„­ Ρ⦇NTMapβ¦ˆβ¦‡π”žPL⦈"
    by (*slow*)
      (
        cs_prems 
          cs_simp: cat_parallel_cs_simps cat_cs_simps 
          cs_intro: cat_cs_intros cat_parallel_cs_intros 
      )
qed

lemma cat_cocone_cf_par_eps_NTMap_app:
  assumes "Ξ΅ :
    ↑↑→↑↑ β„­ π”ŸPL π”žPL 𝔣PL 𝔀PL π”Ÿ π”ž 𝔣 𝔀 >CF.cocone E : ↑↑C π”ŸPL π”žPL 𝔣PL 𝔀PL ↦↦CΞ± β„­"
    and "𝔀 : π”Ÿ ↦ℭ π”ž" 
    and "𝔣 : π”Ÿ ↦ℭ π”ž"
  shows 
    "Ρ⦇NTMapβ¦ˆβ¦‡π”ŸPL⦈ = Ρ⦇NTMapβ¦ˆβ¦‡π”žPL⦈ ∘Aβ„­ 𝔀" 
    "Ρ⦇NTMapβ¦ˆβ¦‡π”ŸPL⦈ = Ρ⦇NTMapβ¦ˆβ¦‡π”žPL⦈ ∘Aβ„­ 𝔣"    
proof-
  let ?II = ‹↑↑C π”ŸPL π”žPL 𝔣PL 𝔀PLβ€Ί and ?II_II = ‹↑↑→↑↑ β„­ π”ŸPL π”žPL 𝔣PL 𝔀PL π”Ÿ π”ž 𝔣 𝔀›
  interpret Ξ΅: is_cat_cocone Ξ± E ?II β„­ ?II_II Ξ΅ by (rule assms(1))
  from assms(2,3) have π”ž: "π”ž ∈∘ ℭ⦇Obj⦈" and π”Ÿ: "π”Ÿ ∈∘ ℭ⦇Obj⦈" by auto
  interpret par: cf_parallel Ξ± π”ŸPL π”žPL 𝔣PL 𝔀PL π”Ÿ π”ž 𝔣 𝔀 β„­ 
    by (intro cf_parallel_if_is_cat_cocone, rule assms) (auto intro: assms π”ž π”Ÿ)
  note Ξ΅_NTMap_app = 
    cat_cone_cf_par_eps_NTMap_app[
      OF Ξ΅.is_cat_cone_op[unfolded cat_op_simps],
      unfolded cat_op_simps,  
      OF assms(2,3)
      ]
  from Ξ΅_NTMap_app show Ξ΅_NTMap_app:
    "Ρ⦇NTMapβ¦ˆβ¦‡π”ŸPL⦈ = Ρ⦇NTMapβ¦ˆβ¦‡π”žPL⦈ ∘Aβ„­ 𝔀"
    "Ρ⦇NTMapβ¦ˆβ¦‡π”ŸPL⦈ = Ρ⦇NTMapβ¦ˆβ¦‡π”žPL⦈ ∘Aβ„­ 𝔣"
    by 
      (
        cs_concl