Theory CZH_UCAT_Limit_Product

(* Copyright 2021 (C) Mihails Milehins *)

section‹Products and coproducts as limits and colimits›
theory CZH_UCAT_Limit_Product
  imports 
    CZH_UCAT_Limit
    CZH_Elementary_Categories.CZH_ECAT_Discrete 
begin



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)
syntax_consts "_is_cat_obj_prod" ⇌ is_cat_obj_prod
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)
syntax_consts "_is_cat_obj_coprod" ⇌ is_cat_obj_coprod
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_shallow 
        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_shallow 
        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›

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_iso_arr:
  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_iso_arr[
          OF π.is_cat_limit_axioms π'.is_cat_limit_axioms
          ]
      )
qed

lemma cat_obj_prod_ex_is_iso_arr':
  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_iso_arr'[
          OF π.is_cat_limit_axioms π'.is_cat_limit_axioms,
          unfolded the_cat_discrete_components(1)
          ]
      )
qed

lemma cat_obj_coprod_ex_is_iso_arr:
  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_iso_arr[
          OF π.is_cat_colimit_axioms π'.is_cat_colimit_axioms
          ]
      )
qed

lemma cat_obj_coprod_ex_is_iso_arr':
  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_iso_arr'[
          OF π.is_cat_colimit_axioms π'.is_cat_colimit_axioms,
          unfolded the_cat_discrete_components(1)
          ]
      )
qed



subsection‹Small product and small coproduct›


subsubsection‹Definition and elementary properties›

locale is_tm_cat_obj_prod = 
  is_cat_limit α ‹:C I› ℭ ‹:→: I A ℭ› P π + tm_cf_discrete α I A ℭ
  for α I A ℭ P π

syntax "_is_tm_cat_obj_prod" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ <CF.tm.∏ _ :/ _ ↦↦C.tmı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_tm_cat_obj_prod" ⇌ is_tm_cat_obj_prod
translations "π : P <CF.tm.∏ A : I ↦↦C.tm⇘α⇙ ℭ" ⇌ 
  "CONST is_tm_cat_obj_prod α I A ℭ P π"

locale is_tm_cat_obj_coprod = 
  is_cat_colimit α ‹:C I› ℭ ‹:→: I A ℭ› U π + tm_cf_discrete α I A ℭ
  for α I A ℭ U π

syntax "_is_tm_cat_obj_coprod" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ >CF.tm.∐ _ :/ _ ↦↦C.tmı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_tm_cat_obj_coprod" ⇌ is_tm_cat_obj_coprod
translations "π : A >CF.tm.∐ U : I ↦↦C.tm⇘α⇙ ℭ" ⇌ 
  "CONST is_tm_cat_obj_coprod α I A ℭ U π"


text‹Rules.›

lemma (in is_tm_cat_obj_prod) is_tm_cat_obj_prod_axioms'[cat_lim_cs_intros]:
  assumes "α' = α" and "P' = P" and "A' = A" and "I' = I" and "ℭ' = ℭ" 
  shows "π : P' <CF.tm.∏ A' : I' ↦↦C.tm⇘α'⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_obj_prod_axioms)

mk_ide rf is_tm_cat_obj_prod_def
  |intro is_tm_cat_obj_prodI|
  |dest is_tm_cat_obj_prodD[dest]|
  |elim is_tm_cat_obj_prodE[elim]|

lemmas [cat_lim_cs_intros] = is_tm_cat_obj_prodD

lemma (in is_tm_cat_obj_coprod) 
  is_tm_cat_obj_coprod_axioms'[cat_lim_cs_intros]:
  assumes "α' = α" and "U' = U" and "A' = A" and "I' = I" and "ℭ' = ℭ" 
  shows "π : A' >CF.tm.∐ U' : I' ↦↦C.tm⇘α'⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_obj_coprod_axioms)

mk_ide rf is_tm_cat_obj_coprod_def
  |intro is_tm_cat_obj_coprodI|
  |dest is_tm_cat_obj_coprodD[dest]|
  |elim is_tm_cat_obj_coprodE[elim]|

lemmas [cat_lim_cs_intros] = is_tm_cat_obj_coprodD


text‹Elementary properties.›

sublocale is_tm_cat_obj_prod ⊆ is_cat_obj_prod
  by
    (
      intro is_cat_obj_prodI,
      rule is_cat_limit_axioms,
      rule cf_discrete_axioms
    )

lemmas (in is_tm_cat_obj_prod) tm_cat_obj_prod_is_cat_obj_prod = 
  is_cat_obj_prod_axioms

sublocale is_tm_cat_obj_coprod ⊆ is_cat_obj_coprod
  by 
    ( 
      intro is_cat_obj_coprodI, 
      rule is_cat_colimit_axioms, 
      rule cf_discrete_axioms
    )

lemmas (in is_tm_cat_obj_coprod) tm_cat_obj_coprod_is_cat_obj_coprod = 
  is_cat_obj_coprod_axioms

sublocale is_tm_cat_obj_prod ⊆ is_tm_cat_limit α ‹:C I› ℭ ‹:→: I A ℭ› P π
  by
    (
      intro
        is_tm_cat_limitI 
        is_tm_cat_coneI 
        is_ntcf_axioms 
        tm_cf_discrete_the_cf_discrete_is_tm_functor 
        cat_cone_obj 
        cat_lim_ua_fo
    )

lemmas (in is_tm_cat_obj_prod) tm_cat_obj_prod_is_tm_cat_limit =
  is_tm_cat_limit_axioms

sublocale is_tm_cat_obj_coprod ⊆ is_tm_cat_colimit α ‹:C I› ℭ ‹:→: I A ℭ› U π
  by
    (
      intro
        is_tm_cat_colimitI 
        is_tm_cat_coconeI 
        is_ntcf_axioms 
        tm_cf_discrete_the_cf_discrete_is_tm_functor 
        cat_cocone_obj 
        cat_colim_ua_of
    )

lemmas (in is_tm_cat_obj_coprod) tm_cat_obj_coprod_is_tm_cat_colimit =
  is_tm_cat_colimit_axioms


text‹Duality.›

lemma (in is_tm_cat_obj_prod) is_tm_cat_obj_coprod_op:
  "op_ntcf π : A >CF.tm.∐ P : I ↦↦C.tm⇘α⇙ op_cat ℭ"
  using cf_discrete_vdomain_vsubset_Vset
  by (intro is_tm_cat_obj_coprodI) 
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_op_intros)

lemma (in is_tm_cat_obj_prod) is_tm_cat_obj_coprod_op'[cat_op_intros]:
  assumes "ℭ' = op_cat ℭ"
  shows "op_ntcf π : A >CF.tm.∐ P : I ↦↦C.tm⇘α⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_obj_coprod_op)

lemmas [cat_op_intros] = is_tm_cat_obj_prod.is_tm_cat_obj_coprod_op'

lemma (in is_tm_cat_obj_coprod) is_tm_cat_obj_coprod_op:
  "op_ntcf π : U <CF.tm.∏ A : I ↦↦C.tm⇘α⇙ op_cat ℭ"
  using cf_discrete_vdomain_vsubset_Vset
  by (intro is_tm_cat_obj_prodI)
    (cs_concl cs_simp: cat_op_simps cs_intro: cat_op_intros)

lemma (in is_tm_cat_obj_coprod) is_tm_cat_obj_prod_op'[cat_op_intros]:
  assumes "ℭ' = op_cat ℭ"
  shows "op_ntcf π : U <CF.tm.∏ A : I ↦↦C.tm⇘α⇙ ℭ'"
  unfolding assms by (rule is_tm_cat_obj_coprod_op)

lemmas [cat_op_intros] = is_tm_cat_obj_coprod.is_tm_cat_obj_prod_op'



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)
syntax_consts "_is_cat_finite_obj_prod" ⇌ is_cat_finite_obj_prod
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)
syntax_consts "_is_cat_finite_obj_coprod" ⇌ is_cat_finite_obj_coprod
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.category_axioms 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.category_axioms 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_shallow
        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_shallow
        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)
syntax_consts "_is_cat_obj_prod_2" ⇌ is_cat_obj_prod_2
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)
syntax_consts "_is_cat_obj_coprod_2" ⇌ is_cat_obj_coprod_2
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_shallow 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_shallow 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_iso_arr:
  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_iso_arr[
          OF π.is_cat_obj_prod_axioms π'.is_cat_obj_prod_axioms
          ]
      )
qed

lemma cat_obj_coprod_2_ex_is_iso_arr:
  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_iso_arr[
          OF π.is_cat_obj_coprod_axioms π'.is_cat_obj_coprod_axioms
          ]
      )
qed



subsection‹Projection cone›


subsubsection‹Definition and elementary properties›

definition ntcf_obj_prod_base :: "V ⇒ V ⇒ (V ⇒ V) ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "ntcf_obj_prod_base ℭ I F P f =
    [(λj∈∘:C I⦇Obj⦈. f j), cf_const (:C I) ℭ P, :→: I F ℭ, :C I, ℭ]∘"

definition ntcf_obj_coprod_base :: "V ⇒ V ⇒ (V ⇒ V) ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "ntcf_obj_coprod_base ℭ I F P f =
    [(λj∈∘:C I⦇Obj⦈. f j), :→: I F ℭ, cf_const (:C I) ℭ P, :C I, ℭ]∘"


text‹Components.›

lemma ntcf_obj_prod_base_components:
  shows "ntcf_obj_prod_base ℭ I F P f⦇NTMap⦈ = (λj∈∘:C I⦇Obj⦈. f j)"
    and "ntcf_obj_prod_base ℭ I F P f⦇NTDom⦈ = cf_const (:C I) ℭ P"
    and "ntcf_obj_prod_base ℭ I F P f⦇NTCod⦈ = :→: I F ℭ"
    and "ntcf_obj_prod_base ℭ I F P f⦇NTDGDom⦈ = :C I"
    and "ntcf_obj_prod_base ℭ I F P f⦇NTDGCod⦈ = ℭ"
  unfolding ntcf_obj_prod_base_def nt_field_simps 
  by (simp_all add: nat_omega_simps)

lemma ntcf_obj_coprod_base_components:
  shows "ntcf_obj_coprod_base ℭ I F P f⦇NTMap⦈ = (λj∈∘:C I⦇Obj⦈. f j)"
    and "ntcf_obj_coprod_base ℭ I F P f⦇NTDom⦈ = :→: I F ℭ"
    and "ntcf_obj_coprod_base ℭ I F P f⦇NTCod⦈ = cf_const (:C I) ℭ P"
    and "ntcf_obj_coprod_base ℭ I F P f⦇NTDGDom⦈ = :C I"
    and "ntcf_obj_coprod_base ℭ I F P f⦇NTDGCod⦈ = ℭ"
  unfolding ntcf_obj_coprod_base_def nt_field_simps 
  by (simp_all add: nat_omega_simps)


text‹Duality.›

lemma (in cf_discrete) op_ntcf_ntcf_obj_coprod_base[cat_op_simps]:
  "op_ntcf (ntcf_obj_coprod_base ℭ I F P f) =
    ntcf_obj_prod_base (op_cat ℭ) I F P f"
proof-
  note [cat_op_simps] = the_cat_discrete_op[OF cf_discrete_vdomain_vsubset_Vset]
  show ?thesis
    unfolding 
      ntcf_obj_prod_base_def ntcf_obj_coprod_base_def op_ntcf_def nt_field_simps
    by (simp add: nat_omega_simps cat_op_simps) 
qed

lemma (in cf_discrete) op_ntcf_ntcf_obj_prod_base[cat_op_simps]:
  "op_ntcf (ntcf_obj_prod_base ℭ I F P f) =
    ntcf_obj_coprod_base (op_cat ℭ) I F P f"
proof-
  note [cat_op_simps] = the_cat_discrete_op[OF cf_discrete_vdomain_vsubset_Vset]
  show ?thesis
    unfolding 
      ntcf_obj_prod_base_def ntcf_obj_coprod_base_def op_ntcf_def nt_field_simps
    by (simp add: nat_omega_simps cat_op_simps) 
qed


subsubsection‹Natural transformation map›

mk_VLambda ntcf_obj_prod_base_components(1)
  |vsv ntcf_obj_prod_base_NTMap_vsv[cat_cs_intros]|
  |vdomain ntcf_obj_prod_base_NTMap_vdomain[cat_cs_simps]|
  |app ntcf_obj_prod_base_NTMap_app[cat_cs_simps]|

mk_VLambda ntcf_obj_coprod_base_components(1)
  |vsv ntcf_obj_coprod_base_NTMap_vsv[cat_cs_intros]|
  |vdomain ntcf_obj_coprod_base_NTMap_vdomain[cat_cs_simps]|
  |app ntcf_obj_coprod_base_NTMap_app[cat_cs_simps]|


subsubsection‹Projection natural transformation is a cone›

lemma (in tm_cf_discrete) tm_cf_discrete_ntcf_obj_prod_base_is_cat_cone:
  assumes "P ∈∘ ℭ⦇Obj⦈" and "⋀a. a ∈∘ I ⟹ f a : P ↦⇘ℭ⇙ F a"
  shows "ntcf_obj_prod_base ℭ I F P f : P <CF.cone :→: I F ℭ : :C I ↦↦C⇘α⇙ ℭ"
proof(intro is_cat_coneI is_tm_ntcfI' is_ntcfI')
  from assms(2) have [cat_cs_intros]: 
    "⟦ a ∈∘ I; P' = P; Fa = F a ⟧ ⟹ f a : P' ↦⇘ℭ⇙ Fa" for a P' Fa 
    by simp
  show "vfsequence (ntcf_obj_prod_base ℭ I F P f)"
    unfolding ntcf_obj_prod_base_def by auto
  show "vcard (ntcf_obj_prod_base ℭ I F P f) = 5ℕ"
    unfolding ntcf_obj_prod_base_def by (auto simp: nat_omega_simps)
  from assms show "cf_const (:C I) ℭ P : :C I ↦↦C⇘α⇙ ℭ"
    by 
      (
        cs_concl 
          cs_intro: 
            cf_discrete_vdomain_vsubset_Vset 
            cat_discrete_cs_intros 
            cat_cs_intros
      )
  show ":→: I F ℭ : :C I ↦↦C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_intro: cat_discrete_cs_intros)
  show "ntcf_obj_prod_base ℭ I F P f⦇NTMap⦈⦇a⦈ :
    cf_const (:C I) ℭ P⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ :→: I F ℭ⦇ObjMap⦈⦇a⦈"
    if "a ∈∘ :C I⦇Obj⦈" for a
  proof-
    from that have "a ∈∘ I" unfolding the_cat_discrete_components by simp
    from that this show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_discrete_cs_simps cs_intro: cat_cs_intros
        )
  qed
  show 
    "ntcf_obj_prod_base ℭ I F P f⦇NTMap⦈⦇b⦈ ∘A⇘ℭ⇙
      cf_const (:C I) ℭ P⦇ArrMap⦈⦇g⦈ =
      :→: I F ℭ⦇ArrMap⦈⦇g⦈ ∘A⇘ℭ⇙ ntcf_obj_prod_base ℭ I F P f⦇NTMap⦈⦇a⦈"
    if "g : a ↦⇘:C I⇙ b" for a b g
  proof-
    note g = the_cat_discrete_is_arrD[OF that]
    from that g(4)[unfolded g(7-9)] g(1)[unfolded g(7-9)] show ?thesis
      unfolding g(7-9)
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_discrete_cs_simps 
            cs_intro: 
              cf_discrete_vdomain_vsubset_Vset 
              cat_cs_intros cat_discrete_cs_intros
        )
  qed
qed 
  (
    auto simp: 
      assms 
      ntcf_obj_prod_base_components 
      tm_cf_discrete_the_cf_discrete_is_tm_functor
  )

lemma (in tm_cf_discrete) tm_cf_discrete_ntcf_obj_coprod_base_is_cat_cocone:
  assumes "P ∈∘ ℭ⦇Obj⦈" and "⋀a. a ∈∘ I ⟹ f a : F a ↦⇘ℭ⇙ P"
  shows "ntcf_obj_coprod_base ℭ I F P f :
    :→: I F ℭ >CF.cocone P : :C I ↦↦C⇘α⇙ ℭ"
proof-
  note [cat_op_simps] =
    the_cat_discrete_op[OF cf_discrete_vdomain_vsubset_Vset]
    cf_discrete.op_ntcf_ntcf_obj_prod_base[OF cf_discrete_op]
    cf_discrete.cf_discrete_the_cf_discrete_op[OF cf_discrete_op]
  have "op_ntcf (ntcf_obj_coprod_base ℭ I F P f) :
    P <CF.cone op_cf (:→: I F ℭ) : op_cat (:C I) ↦↦C⇘α⇙ op_cat ℭ"
    unfolding cat_op_simps
    by
      (
        rule tm_cf_discrete.tm_cf_discrete_ntcf_obj_prod_base_is_cat_cone[
          OF tm_cf_discrete_op, unfolded cat_op_simps, OF assms
          ]
      )
  from is_cat_cone.is_cat_cocone_op[OF this, unfolded cat_op_simps] 
  show ?thesis .
qed

lemma (in tm_cf_discrete) tm_cf_discrete_ntcf_obj_prod_base_is_cat_obj_prod:
  assumes "P ∈∘ ℭ⦇Obj⦈" 
    and "⋀a. a ∈∘ I ⟹ f a : P ↦⇘ℭ⇙ F a"
    and "⋀u' r'.
      ⟦ u' : r' <CF.cone :→: I F ℭ : :C I ↦↦C⇘α⇙ ℭ ⟧ ⟹ 
        ∃!f'.
          f' : r' ↦⇘ℭ⇙ P ∧
          u' = ntcf_obj_prod_base ℭ I F P f ∙NTCF ntcf_const (:C I) ℭ f'"
  shows "ntcf_obj_prod_base ℭ I F P f : P <CF.∏ F : I ↦↦C⇘α⇙ ℭ"
proof
  (
    intro 
      is_cat_obj_prodI 
      is_cat_limitI 
      tm_cf_discrete_ntcf_obj_prod_base_is_cat_cone[OF assms(1,2), simplified] 
      assms(1,3)
  )
  show "cf_discrete α I F ℭ"
    by (cs_concl cs_shallow cs_intro: cat_small_discrete_cs_intros)
qed

lemma (in tm_cf_discrete) tm_cf_discrete_ntcf_obj_coprod_base_is_cat_obj_coprod:
  assumes "P ∈∘ ℭ⦇Obj⦈" 
    and "⋀a. a ∈∘ I ⟹ f a : F a ↦⇘ℭ⇙ P"
    and "⋀u' r'. ⟦ u' : :→: I F ℭ >CF.cocone r' : :C I ↦↦C⇘α⇙ ℭ ⟧ ⟹
      ∃!f'.
        f' : P ↦⇘ℭ⇙ r' ∧
        u' = ntcf_const (:C I) ℭ f' ∙NTCF ntcf_obj_coprod_base ℭ I F P f"
  shows "ntcf_obj_coprod_base ℭ I F P f : F >CF.∐ P : I ↦↦C⇘α⇙ ℭ"
    (is ‹?nc : F >CF.∐ P : I ↦↦C⇘α⇙ ℭ›)
proof-
  let ?np = ‹ntcf_obj_prod_base (op_cat ℭ) I F P f›
  interpret is_cat_cocone α P ‹:C I› ℭ ‹:→: I F ℭ› ?nc
    by (intro tm_cf_discrete_ntcf_obj_coprod_base_is_cat_cocone[OF assms(1,2)])
  note [cat_op_simps] =
    the_cat_discrete_op[OF cf_discrete_vdomain_vsubset_Vset]
    cf_discrete.op_ntcf_ntcf_obj_prod_base[OF cf_discrete_op]
    cf_discrete.cf_discrete_the_cf_discrete_op[OF cf_discrete_op]
  have "∃!f'.
    f' : P ↦⇘ℭ⇙ r ∧
    u = ?np ∙NTCF ntcf_const (:C I) (op_cat ℭ) f'"
    if "u : r <CF.cone :→: I F (op_cat ℭ) : :C I ↦↦C⇘α⇙ op_cat ℭ" for u r
  proof-
    interpret u: is_cat_cone α r ‹:C I› ‹op_cat ℭ› ‹:→: I F (op_cat ℭ)› u
      by (rule that)
    from assms(3)[OF u.is_cat_cocone_op[unfolded cat_op_simps]] obtain g 
      where g: "g : P ↦⇘ℭ⇙ r"
        and op_u: "op_ntcf u = ntcf_const (:C I) ℭ g ∙NTCF ?nc"
        and g_unique: 
          "⟦ g' : P ↦⇘ℭ⇙ r; op_ntcf u = ntcf_const (:C I) ℭ g' ∙NTCF ?nc ⟧ ⟹
            g' = g"
      for g'
      by metis
    show ?thesis
    proof(intro ex1I conjI; (elim conjE)?)
      from op_u have 
        "op_ntcf (op_ntcf u) = op_ntcf (ntcf_const (:C I) ℭ g ∙NTCF ?nc)"
        by simp
      from this g show "u = ?np ∙NTCF ntcf_const (:C I) (op_cat ℭ) g"
        by (cs_prems cs_simp: cat_op_simps cs_intro: cat_cs_intros)
      fix g' assume prems:
        "g' : P ↦⇘ℭ⇙ r"
        "u = ?np ∙NTCF ntcf_const (:C I) (op_cat ℭ) g'"
      from prems(2) have 
        "op_ntcf u = op_ntcf (?np ∙NTCF ntcf_const (:C I) (op_cat ℭ) g')"
        by simp
      from this prems(1) g have "op_ntcf u = ntcf_const (:C I) ℭ g' ∙NTCF ?nc"
        by 
          (
            subst (asm) 
              the_cat_discrete_op[OF cf_discrete_vdomain_vsubset_Vset, symmetric]
          )
          (
            cs_prems 
              cs_simp: 
                cat_op_simps 
                op_ntcf_ntcf_vcomp[symmetric] 
                is_ntcf.ntcf_op_ntcf_op_ntcf 
                op_ntcf_ntcf_obj_coprod_base[symmetric] 
                op_ntcf_ntcf_const[symmetric]
              cs_intro: cat_cs_intros cat_op_intros
          )
      from g_unique[OF prems(1) this] show "g' = g" .
    qed (rule g)
  qed
  from is_cat_obj_prod.is_cat_obj_coprod_op
    [
      OF tm_cf_discrete.tm_cf_discrete_ntcf_obj_prod_base_is_cat_obj_prod
        [
          OF tm_cf_discrete_op, 
          unfolded cat_op_simps,
          OF assms(1,2) this, 
          folded op_ntcf_ntcf_obj_coprod_base
        ],
      unfolded cat_op_simps
    ]
  show "?nc : F >CF.∐ P : I ↦↦C⇘α⇙ ℭ".
qed

text‹\newpage›

end