Theory CZH_UCAT_Set

(* Copyright 2021 (C) Mihails Milehins *)

section‹Category ‹Set› and universal constructions›
theory CZH_UCAT_Set
  imports CZH_UCAT_Complete
begin



subsection‹Discrete functor with tiny maps to the category ‹Set››

lemma (in 𝒵) tm_cf_discrete_cat_Set_if_VLambda_in_Vset:
  assumes "VLambda I F ∈∘ Vset α"
  shows "tm_cf_discrete α I F (cat_Set α)"
proof(intro tm_cf_discreteI)
  from assms have vrange_F_in_Vset: "ℛ∘ (VLambda I F) ∈∘ Vset α"
    by (auto intro: vrange_in_VsetI)
  show "(λi∈∘I. cat_Set α⦇CId⦈⦇F i⦈) ∈∘ Vset α"
  proof(rule vbrelation.vbrelation_Limit_in_VsetI)
    from assms show "𝒟∘ (λi∈∘I. cat_Set α⦇CId⦈⦇F i⦈) ∈∘ Vset α"
      by (metis vdomain_VLambda vdomain_in_VsetI)
    define Q where
      "Q i =
        (
          if i = 0
          then VPow ((⋃∘i∈∘I. F i) ×∘ (⋃∘i∈∘I. F i)) 
          else set (F ` elts I)
        )" 
      for i :: V
    have "ℛ∘ (λi∈∘I. cat_Set α⦇CId⦈⦇F i⦈) ⊆∘ (∏∘i∈∘ set {0, 1ℕ, 2ℕ}. Q i)"
    proof(intro vsubsetI, unfold cat_Set_components)
      fix y assume "y ∈∘ ℛ∘ (λi∈∘I. VLambda (Vset α) id_Set⦇F i⦈)"
      then obtain i where i: "i ∈∘ I" 
        and y_def: "y = VLambda (Vset α) id_Set⦇F i⦈" 
        by auto
      from i have "F i ∈∘ ℛ∘ (VLambda I F)" by auto
      with vrange_F_in_Vset have "F i ∈∘ Vset α" by auto
      then have y_def: "y = id_Set (F i)" unfolding y_def by auto
      show "y ∈∘ (∏∘i∈∘set {0, 1ℕ, 2ℕ}. Q i)"
        unfolding y_def
      proof(intro vproductI, unfold Ball_def; (intro allI impI)?)
        show "𝒟∘ (id_Rel (F i)) = set {0, 1ℕ, 2ℕ}"  
          by (simp add: id_Rel_def incl_Rel_def three nat_omega_simps)
        fix j assume "j ∈∘ set {0, 1ℕ, 2ℕ}"
        then consider ‹j = 0› | ‹j = 1ℕ› | ‹j = 2ℕ› by auto
        then show "id_Rel (F i)⦇j⦈ ∈∘ Q j"
        proof cases
          case 1
          from i show ?thesis
            unfolding 1
            by 
              (
                subst arr_field_simps(1)[symmetric], 
                unfold id_Rel_components Q_def
              )
              force
        next
          case 2
          from i show ?thesis
            unfolding 2
            by 
              (
                subst arr_field_simps(2)[symmetric], 
                unfold id_Rel_components Q_def
              ) 
              auto
        next
          case 3
          from i show ?thesis
            unfolding 3
            by 
              (
                subst arr_field_simps(3)[symmetric], 
                unfold id_Rel_components Q_def
              ) 
              auto
        qed
      qed (auto simp: id_Rel_def cat_Set_cs_intros)
    qed
    moreover have "(∏∘i∈∘ set {0, 1ℕ, 2ℕ}. Q i) ∈∘ Vset α"
    proof(rule Limit_vproduct_in_VsetI)
      show "set {0, 1ℕ, 2ℕ} ∈∘ Vset α" unfolding three[symmetric] by simp
      from assms have "VPow ((⋃∘i∈∘I. F i) ×∘ (⋃∘i∈∘I. F i)) ∈∘ Vset α"
        by 
          (
            intro 
              Limit_VPow_in_VsetI 
              Limit_vtimes_in_VsetI 
              Limit_vifunion_in_Vset_if_VLambda_in_VsetI
          )
          auto
      then show "Q i ∈∘ Vset α" if "i ∈∘ set {0, 1ℕ, 2ℕ}" for i
        using that vrange_VLambda
        by (auto intro!: vrange_F_in_Vset simp: Q_def nat_omega_simps)
    qed auto
    ultimately show "ℛ∘ (λi∈∘I. cat_Set α⦇CId⦈⦇F i⦈) ∈∘ Vset α"
      by (meson vsubset_in_VsetI) 
  qed auto
  fix i assume prems: "i ∈∘ I"
  from assms have "ℛ∘ (VLambda I F) ∈∘ Vset α" by (auto simp: vrange_in_VsetI)
  moreover from prems have "F i ∈∘ ℛ∘ (VLambda I F)" by auto
  ultimately show "F i ∈∘ cat_Set α⦇Obj⦈" unfolding cat_Set_components by auto    
qed (cs_concl cs_shallow cs_intro: cat_cs_intros assms)+



subsection‹Product cone and coproduct cocone for the category ‹Set››


subsubsection‹Definition and elementary properties›

definition ntcf_Set_obj_prod :: "V ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "ntcf_Set_obj_prod α I F = ntcf_obj_prod_base 
    (cat_Set α) I F (∏∘i∈∘I. F i) (λi. vprojection_arrow I F i)"

definition ntcf_Set_obj_coprod :: "V ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "ntcf_Set_obj_coprod α I F = ntcf_obj_coprod_base 
    (cat_Set α) I F (∐∘i∈∘I. F i) (λi. vcinjection_arrow I F i)"


text‹Components.›

lemma ntcf_Set_obj_prod_components:
  shows "ntcf_Set_obj_prod α I F⦇NTMap⦈ =
    (λi∈∘:C I⦇Obj⦈. vprojection_arrow I F i)"
    and "ntcf_Set_obj_prod α I F⦇NTDom⦈ =
    cf_const (:C I) (cat_Set α) (∏∘i∈∘I. F i)"
    and "ntcf_Set_obj_prod α I F⦇NTCod⦈ = :→: I F (cat_Set α)"
    and "ntcf_Set_obj_prod α I F⦇NTDGDom⦈ = :C I"
    and "ntcf_Set_obj_prod α I F⦇NTDGCod⦈ = cat_Set α"
  unfolding ntcf_Set_obj_prod_def ntcf_obj_prod_base_components by simp_all

lemma ntcf_Set_obj_coprod_components:
  shows "ntcf_Set_obj_coprod α I F⦇NTMap⦈ =
      (λi∈∘:C I⦇Obj⦈. vcinjection_arrow I F i)"
    and "ntcf_Set_obj_coprod α I F⦇NTDom⦈ = :→: I F (cat_Set α)"
    and "ntcf_Set_obj_coprod α I F⦇NTCod⦈ =
      cf_const (:C I) (cat_Set α) (∐∘i∈∘I. F i)"
    and "ntcf_Set_obj_coprod α I F⦇NTDGDom⦈ = :C I"
    and "ntcf_Set_obj_coprod α I F⦇NTDGCod⦈ = cat_Set α"
  unfolding ntcf_Set_obj_coprod_def ntcf_obj_coprod_base_components by simp_all


subsubsection‹Natural transformation map›

mk_VLambda ntcf_Set_obj_prod_components(1)
  |vsv ntcf_Set_obj_prod_NTMap_vsv[cat_cs_intros]|
  |vdomain ntcf_Set_obj_prod_NTMap_vdomain[cat_cs_simps]|
  |app ntcf_Set_obj_prod_NTMap_app[cat_cs_simps]|

mk_VLambda ntcf_Set_obj_coprod_components(1)
  |vsv ntcf_Set_obj_coprod_NTMap_vsv[cat_cs_intros]|
  |vdomain ntcf_Set_obj_coprod_NTMap_vdomain[cat_cs_simps]|
  |app ntcf_Set_obj_coprod_NTMap_app[cat_cs_simps]|


subsubsection‹
Product cone for the category ‹Set› is a universal cone and product cocone
for the category ‹Set› is a universal cocone
›

lemma (in 𝒵) tm_cf_discrete_ntcf_obj_prod_base_is_cat_obj_prod:
  ―‹See Theorem 5.2 in Chapter Introduction in \cite{hungerford_algebra_2003}.›
  assumes "VLambda I F ∈∘ Vset α"
  shows "ntcf_Set_obj_prod α I F : 
    (∏∘i∈∘I. F i) <CF.∏ F : I ↦↦C⇘α⇙ cat_Set α"
proof(intro is_cat_obj_prodI is_cat_limitI)

  interpret Set: tm_cf_discrete α I F ‹cat_Set α› 
    by (rule tm_cf_discrete_cat_Set_if_VLambda_in_Vset[OF assms])

  let ?F = ‹ntcf_Set_obj_prod α I F›

  show "cf_discrete α I F (cat_Set α)"
    by (auto simp: cat_small_discrete_cs_intros)
  show F_is_cat_cone: "?F :
    (∏∘i∈∘I. F i) <CF.cone :→: I F (cat_Set α) : :C I ↦↦C⇘α⇙ cat_Set α"
      unfolding ntcf_Set_obj_prod_def
  proof(rule Set.tm_cf_discrete_ntcf_obj_prod_base_is_cat_cone)
    show "(∏∘i∈∘I. F i) ∈∘ cat_Set α⦇Obj⦈"
      unfolding cat_Set_components
      by 
        (
          intro 
            Limit_vproduct_in_Vset_if_VLambda_in_VsetI 
            Set.tm_cf_discrete_ObjMap_in_Vset
        ) 
        auto
  qed (intro vprojection_arrow_is_arr Set.tm_cf_discrete_ObjMap_in_Vset)

  interpret F: is_cat_cone 
    α ‹∏∘i∈∘I. F i› ‹:C I› ‹cat_Set α› ‹:→: I F (cat_Set α)› ‹?F›
    by (rule F_is_cat_cone)

  fix π' P' assume prems:
    "π' : P' <CF.cone :→: I F (cat_Set α) : :C I ↦↦C⇘α⇙ cat_Set α"

  let ?π'i = ‹λi. π'⦇NTMap⦈⦇i⦈›
  let ?up' = ‹cat_Set_obj_prod_up I F P' ?π'i›

  interpret π': is_cat_cone α P' ‹:C I› ‹cat_Set α› ‹:→: I F (cat_Set α)› π'
    by (rule prems(1))

  show "∃!f'.
    f' : P' ↦⇘cat_Set α⇙ (∏∘i∈∘I. F i) ∧
    π' = ?F ∙NTCF ntcf_const (:C I) (cat_Set α) f'"
  proof(intro ex1I conjI; (elim conjE)?)
    show up': "?up' : P' ↦⇘cat_Set α⇙ (∏∘i∈∘I. F i)" 
    proof(rule cat_Set_obj_prod_up_cat_Set_is_arr)
      show "P' ∈∘ cat_Set α⦇Obj⦈" by (auto intro: cat_cs_intros cat_lim_cs_intros)
      fix i assume "i ∈∘ I"
      then show "π'⦇NTMap⦈⦇i⦈ : P' ↦⇘cat_Set α⇙ F i"
        by 
          (
            cs_concl cs_shallow
              cs_simp: 
                the_cat_discrete_components(1) 
                cat_cs_simps cat_discrete_cs_simps 
              cs_intro: cat_cs_intros
          )
    qed (rule assms)

    then have P': "P' ∈∘ cat_Set α⦇Obj⦈" 
      by (auto intro: cat_cs_intros cat_lim_cs_intros)

    have π'i_i: "?π'i i : P' ↦⇘cat_Set α⇙ F i" if "i ∈∘ I" for i
      using 
        π'.ntcf_NTMap_is_arr[unfolded the_cat_discrete_components(1), OF that]
        that
      by 
        (
          cs_prems cs_shallow cs_simp:
            cat_cs_simps cat_discrete_cs_simps the_cat_discrete_components(1)
        )

    from cat_Set_obj_prod_up_cat_Set_is_arr[OF P' assms(1) π'i_i] have π'i: 
      "cat_Set_obj_prod_up I F P' ?π'i : P' ↦⇘cat_Set α⇙ (∏∘i∈∘I. F i)". 

    show "π' = ?F ∙NTCF ntcf_const (:C I) (cat_Set α) ?up'"
    proof(rule ntcf_eqI, rule π'.is_ntcf_axioms)

      from F_is_cat_cone π'i show 
        "?F ∙NTCF ntcf_const (:C I) (cat_Set α) ?up' :
          cf_const (:C I) (cat_Set α) P' ↦CF :→: I F (cat_Set α) : 
          :C I ↦↦C⇘α⇙ cat_Set α"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)

      have dom_lhs: "𝒟∘ (π'⦇NTMap⦈) = :C I⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps)
      from F_is_cat_cone π'i have dom_rhs: 
        "𝒟∘ ((?F ∙NTCF ntcf_const (:C I) (cat_Set α) ?up')⦇NTMap⦈) = :C I⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

      show "π'⦇NTMap⦈ = (?F ∙NTCF ntcf_const (:C I) (cat_Set α) ?up')⦇NTMap⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix i assume prems': "i ∈∘ :C I⦇Obj⦈"
        then have i: "i ∈∘ I" unfolding the_cat_discrete_components by simp
        have [cat_cs_simps]: 
          "vprojection_arrow I F i ∘A⇘cat_Set α⇙ ?up' = π'⦇NTMap⦈⦇i⦈"
          by 
            (
              rule cat_Set_cf_comp_proj_obj_prod_up[
                OF P' assms π'i_i i, symmetric
                ]
            ) 
            auto
        from π'i prems' show "π'⦇NTMap⦈⦇i⦈ =
          (?F ∙NTCF ntcf_const (:C I) (cat_Set α) ?up')⦇NTMap⦈⦇i⦈"
          by 
            (
              cs_concl cs_shallow
                cs_simp: cat_cs_simps cat_Rel_cs_simps cs_intro: cat_cs_intros
            )
      qed (auto simp: cat_cs_intros)

    qed simp_all

    fix f' assume prems:
      "f' : P' ↦⇘cat_Set α⇙ (∏∘i∈∘I. F i)"
      "π' = ?F ∙NTCF ntcf_const (:C I) (cat_Set α) f'"
    from prems(2) have π'_eq_F_f': "π'⦇NTMap⦈⦇i⦈⦇ArrVal⦈⦇a⦈ = 
      (?F ∙NTCF ntcf_const (:C I) (cat_Set α) f')⦇NTMap⦈⦇i⦈⦇ArrVal⦈⦇a⦈"
      if "i ∈∘ I" and "a ∈∘ P'" for i a
      by simp
    have [cat_Set_cs_simps]: "π'⦇NTMap⦈⦇i⦈⦇ArrVal⦈⦇a⦈ = f'⦇ArrVal⦈⦇a⦈⦇i⦈"
      if "i ∈∘ I" and "a ∈∘ P'" for i a
      using 
        π'_eq_F_f'[OF that] 
        assms prems that 
        vprojection_arrow_is_arr[OF that(1) assms]
      by 
        (
          cs_prems cs_shallow
            cs_simp: 
              cat_Set_cs_simps 
              cat_cs_simps 
              vprojection_arrow_ArrVal_app 
              the_cat_discrete_components(1) 
            cs_intro: cat_Set_cs_intros cat_cs_intros
        )

    note f' = cat_Set_is_arrD[OF prems(1)]
    note up' = cat_Set_is_arrD[OF up']

    interpret f': arr_Set α f' by (rule f'(1))
    interpret u': arr_Set α ‹(cat_Set_obj_prod_up I F P' (app (π'⦇NTMap⦈)))› 
      by (rule up'(1))

    show "f' = ?up'"
    proof(rule arr_Set_eqI[of α])
      have dom_lhs: "𝒟∘ (f'⦇ArrVal⦈) = P'" by (simp add: cat_Set_cs_simps f')
      have dom_rhs: 
        "𝒟∘ (cat_Set_obj_prod_up I F P' (app (π'⦇NTMap⦈))⦇ArrVal⦈) = P'"
        by (simp add: cat_Set_cs_simps up')
      show "f'⦇ArrVal⦈ = cat_Set_obj_prod_up I F P' (app (π'⦇NTMap⦈))⦇ArrVal⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix a assume prems': "a ∈∘ P'"
        from prems(1) prems' have "f'⦇ArrVal⦈⦇a⦈ ∈∘ (∏∘i∈∘I. F i)"
          by (cs_concl cs_shallow cs_intro: cat_Set_cs_intros)
        note f'a = vproductD[OF this]
        from prems' have dom_rhs: 
          "𝒟∘ (cat_Set_obj_prod_up I F P' (app (π'⦇NTMap⦈))⦇ArrVal⦈⦇a⦈) = I"
          by (cs_concl cs_shallow cs_simp: cat_Set_cs_simps)
        show "f'⦇ArrVal⦈⦇a⦈ =
          cat_Set_obj_prod_up I F P' (app (π'⦇NTMap⦈))⦇ArrVal⦈⦇a⦈"
        proof(rule vsv_eqI, unfold f'a dom_rhs)
          fix i assume "i ∈∘ I"
          with prems' show "f'⦇ArrVal⦈⦇a⦈⦇i⦈ =
            cat_Set_obj_prod_up I F P' (app (π'⦇NTMap⦈))⦇ArrVal⦈⦇a⦈⦇i⦈"
            by (cs_concl cs_shallow cs_simp: cat_Set_cs_simps)
        qed (simp_all add: prems' f'a(1) cat_Set_obj_prod_up_ArrVal_app)
      qed auto
    qed (simp_all add: cat_Set_obj_prod_up_components f' up'(1))

  qed

qed

lemma (in 𝒵) tm_cf_discrete_ntcf_obj_prod_base_is_tm_cat_obj_prod:
  ―‹See Theorem 5.2 in Chapter Introduction in \cite{hungerford_algebra_2003}.›
  assumes "VLambda I F ∈∘ Vset α"
  shows "ntcf_Set_obj_prod α I F :
    (∏∘i∈∘I. F i) <CF.tm.∏ F : I ↦↦C.tm⇘α⇙ cat_Set α"
proof(intro is_tm_cat_obj_prodI)
  from assms show "tm_cf_discrete α I F (cat_Set α)"
    by (rule tm_cf_discrete_cat_Set_if_VLambda_in_Vset)
  show "ntcf_Set_obj_prod α I F :
    vproduct I F <CF.lim  :→: I F (cat_Set α) : :C I ↦↦C⇘α⇙ cat_Set α"
    by 
      (
        rule is_cat_obj_prodD[
          OF tm_cf_discrete_ntcf_obj_prod_base_is_cat_obj_prod[OF assms]
          ]
      )
qed

lemma (in 𝒵) tm_cf_discrete_ntcf_obj_coprod_base_is_cat_obj_coprod:
  ―‹See Theorem 5.2 in Chapter Introduction in \cite{hungerford_algebra_2003}.›
  assumes "VLambda I F ∈∘ Vset α"
  shows "ntcf_Set_obj_coprod α I F :
    F >CF.∐ (∐∘i∈∘I. F i) : I ↦↦C⇘α⇙ cat_Set α"
proof(intro is_cat_obj_coprodI is_cat_colimitI)

  interpret Set: tm_cf_discrete α I F ‹cat_Set α› 
    by (rule tm_cf_discrete_cat_Set_if_VLambda_in_Vset[OF assms])

  let ?F = ‹ntcf_Set_obj_coprod α I F›

  show "cf_discrete α I F (cat_Set α)"
    by (auto simp: cat_small_discrete_cs_intros)
  show F_is_cat_cocone: "?F :
    :→: I F (cat_Set α) >CF.cocone (∐∘i∈∘I. F i) : :C I ↦↦C⇘α⇙ cat_Set α"
    unfolding ntcf_Set_obj_coprod_def
  proof(rule Set.tm_cf_discrete_ntcf_obj_coprod_base_is_cat_cocone)
    show "(∐∘i∈∘I. F i) ∈∘ cat_Set α⦇Obj⦈"
      unfolding cat_Set_components
      by 
        (
          intro 
            Limit_vdunion_in_Vset_if_VLambda_in_VsetI 
            Set.tm_cf_discrete_ObjMap_in_Vset
        ) 
        auto
  qed (intro vcinjection_arrow_is_arr Set.tm_cf_discrete_ObjMap_in_Vset)
  then interpret F: is_cat_cocone 
    α ‹∐∘i∈∘I. F i› ‹:C I› ‹cat_Set α› ‹:→: I F (cat_Set α)› ‹?F› .

  fix π' P' assume prems:
    "π' : :→: I F (cat_Set α) >CF.cocone P' : :C I ↦↦C⇘α⇙ cat_Set α"

  let ?π'i = ‹λi. π'⦇NTMap⦈⦇i⦈›
  let ?up' = ‹cat_Set_obj_coprod_up I F P' ?π'i›

  interpret π': is_cat_cocone α P' ‹:C I› ‹cat_Set α› ‹:→: I F (cat_Set α)› π'
    by (rule prems(1))

  show "∃!f'.
    f' : VSigma I F ↦⇘cat_Set α⇙ P' ∧ 
    π' = ntcf_const (:C I) (cat_Set α) f' ∙NTCF ntcf_Set_obj_coprod α I F"
  proof(intro ex1I conjI; (elim conjE)?)
    show up': "?up' : (∐∘i∈∘I. F i) ↦⇘cat_Set α⇙ P'" 
    proof(rule cat_Set_obj_coprod_up_cat_Set_is_arr)
      show "P' ∈∘ cat_Set α⦇Obj⦈" 
        by (auto intro: cat_cs_intros cat_lim_cs_intros)
      fix i assume "i ∈∘ I"
      then show "π'⦇NTMap⦈⦇i⦈ : F i ↦⇘cat_Set α⇙ P'"
        by 
          (
            cs_concl cs_shallow
              cs_simp: 
                cat_cs_simps cat_discrete_cs_simps 
                the_cat_discrete_components(1) 
              cs_intro: cat_cs_intros
          )
    qed (rule assms)

    then have P': "P' ∈∘ cat_Set α⦇Obj⦈" 
      by (auto intro: cat_cs_intros cat_lim_cs_intros)

    have π'i_i: "?π'i i : F i ↦⇘cat_Set α⇙ P'" if "i ∈∘ I" for i
      using 
        π'.ntcf_NTMap_is_arr[unfolded the_cat_discrete_components(1), OF that]
        that
      by 
        (
          cs_prems cs_shallow cs_simp:
            cat_cs_simps cat_discrete_cs_simps the_cat_discrete_components(1)
        )
    from cat_Set_obj_coprod_up_cat_Set_is_arr[OF P' assms(1) π'i_i] have π'i: 
      "?up' : (∐∘i∈∘I. F i) ↦⇘cat_Set α⇙ P'". 

    show "π' = ntcf_const (:C I) (cat_Set α) ?up' ∙NTCF ?F"
    proof(rule ntcf_eqI, rule π'.is_ntcf_axioms)
      from F_is_cat_cocone π'i show 
        "ntcf_const (:C I) (cat_Set α) ?up' ∙NTCF ?F :
          :→: I F (cat_Set α) ↦CF cf_const (:C I) (cat_Set α) P' : 
          :C I ↦↦C⇘α⇙ cat_Set α"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      have dom_lhs: "𝒟∘ (π'⦇NTMap⦈) = :C I⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps)
      from F_is_cat_cocone π'i have dom_rhs: 
        "𝒟∘ ((?F ∙NTCF ntcf_const (:C I) (cat_Set α) ?up')⦇NTMap⦈) = :C I⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      show "π'⦇NTMap⦈ = (ntcf_const (:C I) (cat_Set α) ?up' ∙NTCF ?F)⦇NTMap⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix i assume prems': "i ∈∘ :C I⦇Obj⦈"
        then have i: "i ∈∘ I" unfolding the_cat_discrete_components by simp
        have [cat_cs_simps]: 
          "?up' ∘A⇘cat_Set α⇙ vcinjection_arrow I F i = π'⦇NTMap⦈⦇i⦈"
          by 
            (
              simp add: cat_Set_cf_comp_coprod_up_vcia[
                OF P' assms π'i_i i, symmetric
                ]
            ) 
        from π'i prems' show "π'⦇NTMap⦈⦇i⦈ =
          (ntcf_const (:C I) (cat_Set α) ?up' ∙NTCF ?F)⦇NTMap⦈⦇i⦈"
          by 
            (
              cs_concl cs_shallow
                cs_simp: cat_cs_simps cat_Rel_cs_simps cs_intro: cat_cs_intros
            )
      qed (cs_concl cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros)+
    qed simp_all

    fix f' assume prems:
      "f' : (∐∘i∈∘I. F i) ↦⇘cat_Set α⇙ P'"
      "π' = ntcf_const (:C I) (cat_Set α) f' ∙NTCF ?F"
    from prems(2) have π'_eq_F_f': "π'⦇NTMap⦈⦇i⦈⦇ArrVal⦈⦇a⦈ =
      (ntcf_const (:C I) (cat_Set α) f' ∙NTCF ?F)⦇NTMap⦈⦇i⦈⦇ArrVal⦈⦇a⦈"
      if "i ∈∘ I" and "a ∈∘ P'" for i a
      by simp
    note f' = cat_Set_is_arrD[OF prems(1)]
    note up' = cat_Set_is_arrD[OF up']
    interpret f': arr_Set α f' by (rule f'(1))
    interpret u': arr_Set α ‹(cat_Set_obj_coprod_up I F P' (app (π'⦇NTMap⦈)))› 
      by (rule up'(1))
    show "f' = ?up'"
    proof(rule arr_Set_eqI[of α])
      have dom_lhs: "𝒟∘ (f'⦇ArrVal⦈) = (∐∘i∈∘I. F i)" 
        by (simp add: cat_Set_cs_simps f')
      have dom_rhs: 
        "𝒟∘ (cat_Set_obj_coprod_up I F P' (app (π'⦇NTMap⦈))⦇ArrVal⦈) = 
          (∐∘i∈∘I. F i)"
        by (simp add: cat_Set_cs_simps up')
      show "f'⦇ArrVal⦈ = cat_Set_obj_coprod_up I F P' (app (π'⦇NTMap⦈))⦇ArrVal⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix ix assume prems': "ix ∈∘ (∐∘i∈∘I. F i)"
        then obtain i x where ix_def: "ix = ⟨i, x⟩" 
          and i: "i ∈∘ I" 
          and x: "x ∈∘ F i" 
          by auto
        from assms prems(1) prems' i x show "f'⦇ArrVal⦈⦇ix⦈ = 
          cat_Set_obj_coprod_up I F P' (app (π'⦇NTMap⦈))⦇ArrVal⦈⦇ix⦈"
          unfolding ix_def prems(2)
          by
            (
              cs_concl cs_shallow
                cs_simp:
                  cat_Set_cs_simps cat_cs_simps the_cat_discrete_components(1)
                cs_intro: cat_cs_intros
            )
      qed auto
    qed (simp_all add: cat_Set_obj_coprod_up_components f' up'(1))

  qed

qed

lemma (in 𝒵) ntcf_Set_obj_coprod_is_tm_cat_obj_coprod:
  ―‹See Theorem 5.2 in Chapter Introduction in \cite{hungerford_algebra_2003}.›
  assumes "VLambda I F ∈∘ Vset α"
  shows "ntcf_Set_obj_coprod α I F :
    F >CF.tm.∐ (∐∘i∈∘I. F i) : I ↦↦C.tm⇘α⇙ cat_Set α"
proof(intro is_tm_cat_obj_coprodI)
  from assms show "tm_cf_discrete α I F (cat_Set α)"
    by (rule tm_cf_discrete_cat_Set_if_VLambda_in_Vset)
  show "ntcf_Set_obj_coprod α I F :
    :→: I F (cat_Set α) >CF.colim VSigma I F : :C I ↦↦C⇘α⇙ cat_Set α"
    by 
      (
        rule is_cat_obj_coprodD[
          OF tm_cf_discrete_ntcf_obj_coprod_base_is_cat_obj_coprod[OF assms]
          ]
      )
qed



subsection‹Equalizer for the category ‹Set››


subsubsection‹Definition and elementary properties›

abbreviation ntcf_Set_equalizer_map :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "ntcf_Set_equalizer_map α a g f i ≡
    (
      i = 𝔞PL2 ?
        incl_Set (vequalizer a g f) a :
        g ∘A⇘cat_Set α⇙ incl_Set (vequalizer a g f) a
    )"

definition ntcf_Set_equalizer :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "ntcf_Set_equalizer α a b g f = ntcf_equalizer_base
    (cat_Set α) a b g f (vequalizer a g f) (ntcf_Set_equalizer_map α a g f)"


text‹Components.›

context
  fixes a g f α :: V
begin

lemmas ntcf_Set_equalizer_components = 
  ntcf_equalizer_base_components[
      where ℭ=‹cat_Set α› 
        and e=‹ntcf_Set_equalizer_map α a g f›
        and E=‹vequalizer a g f›
        and 𝔞=a and 𝔤=g and 𝔣=f,
        folded ntcf_Set_equalizer_def
    ]

end


subsubsection‹Natural transformation map›

mk_VLambda ntcf_Set_equalizer_components(1)
  |vsv ntcf_Set_equalizer_NTMap_vsv[cat_Set_cs_intros]|
  |vdomain ntcf_Set_equalizer_NTMap_vdomain[cat_Set_cs_simps]|
  |app ntcf_Set_equalizer_NTMap_app|

lemma ntcf_Set_equalizer_2_NTMap_app_𝔞[cat_Set_cs_simps]:
  assumes "x = 𝔞PL2"
  shows 
    "ntcf_Set_equalizer α a b g f⦇NTMap⦈⦇x⦈ =
      incl_Set (vequalizer a g f) a"
  unfolding assms the_cat_parallel_2_components(1) ntcf_Set_equalizer_components 
  by simp

lemma ntcf_Set_equalizer_2_NTMap_app_𝔟[cat_Set_cs_simps]:
  assumes "x = 𝔟PL2"
  shows 
    "ntcf_Set_equalizer α a b g f⦇NTMap⦈⦇x⦈ =
      g ∘A⇘cat_Set α⇙ incl_Set (vequalizer a g f) a"
  unfolding assms the_cat_parallel_2_components(1) ntcf_Set_equalizer_components
  using cat_PL2_ineq
  by auto


subsubsection‹Equalizer for the category ‹Set› is an equalizer›

lemma (in 𝒵) ntcf_Set_equalizer_2_is_cat_equalizer_2:
  assumes "𝔤 : 𝔞 ↦⇘cat_Set α⇙ 𝔟" and "𝔣 : 𝔞 ↦⇘cat_Set α⇙ 𝔟" 
  shows "ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 :
    vequalizer 𝔞 𝔤 𝔣 <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ cat_Set α"
proof(intro is_cat_equalizer_2I is_cat_equalizerI is_cat_limitI)
  
  let ?II_II = ‹↑↑→↑↑CF (cat_Set α) 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣›
    and ?II = ‹↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL›

  note 𝔤 = cat_Set_is_arrD[OF assms(1)]
  interpret 𝔤: arr_Set α 𝔤 
    rewrites "𝔤⦇ArrDom⦈ = 𝔞" and "𝔤⦇ArrCod⦈ = 𝔟"
    by (rule 𝔤(1)) (simp_all add: 𝔤)
  note 𝔣 = cat_Set_is_arrD[OF assms(2)]
  interpret 𝔣: arr_Set α 𝔣 
    rewrites "𝔣⦇ArrDom⦈ = 𝔞" and "𝔣⦇ArrCod⦈ = 𝔟"
    by (rule 𝔣(1)) (simp_all add: 𝔣)

  note [cat_Set_cs_intros] = 𝔤.arr_Set_ArrDom_in_Vset 𝔣.arr_Set_ArrCod_in_Vset
  
  let ?incl = ‹incl_Set (vequalizer 𝔞 𝔤 𝔣) 𝔞›

  show 𝔞𝔟𝔤𝔣_is_cat_cone: "ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 :
    vequalizer 𝔞 𝔤 𝔣 <CF.cone ?II_II : ?II ↦↦C⇘α⇙ cat_Set α"
    unfolding ntcf_Set_equalizer_def
  proof
    (
      intro 
        category.cat_ntcf_equalizer_base_is_cat_cone 
        category.cat_cf_parallel_2_cat_equalizer
    )
    from assms show 
      "(𝔟PL2 = 𝔞PL2 ? ?incl : 𝔤 ∘A⇘cat_Set α⇙ ?incl) :
        vequalizer 𝔞 𝔤 𝔣 ↦⇘cat_Set α⇙ 𝔟"
      by 
        (
          cs_concl
            cs_simp: V_cs_simps 
            cs_intro: 
              V_cs_intros cat_Set_cs_intros cat_cs_intros 
              cat_PL2_ineq[symmetric] 
        )
    show 
      "(𝔟PL2 = 𝔞PL2 ? ?incl : 𝔤 ∘A⇘cat_Set α⇙ ?incl) =
        𝔤 ∘A⇘cat_Set α⇙ (𝔞PL2 = 𝔞PL2 ? ?incl : 𝔤 ∘A⇘cat_Set α⇙ ?incl)"
      by 
        (
          cs_concl 
            cs_simp: V_cs_simps 
            cs_intro: 
              V_cs_intros cat_Set_cs_intros cat_cs_intros 
              cat_PL2_ineq[symmetric] 
        )
    from assms show 
      "(𝔟PL2 = 𝔞PL2 ? ?incl : 𝔤 ∘A⇘cat_Set α⇙ ?incl) =
        𝔣 ∘A⇘cat_Set α⇙ (𝔞PL2 = 𝔞PL2 ? ?incl : 𝔤 ∘A⇘cat_Set α⇙ ?incl)"
      by 
        (
          cs_concl 
            cs_simp: V_cs_simps cat_Set_incl_Set_commute 
            cs_intro: V_cs_intros cat_PL2_ineq[symmetric]
        )
  qed
    (
      cs_concl 
        cs_intro: cat_cs_intros V_cs_intros cat_Set_cs_intros assms 
        cs_simp: V_cs_simps cat_cs_simps cat_Set_components(1)
    )+

  interpret 𝔞𝔟𝔤𝔣: is_cat_cone 
    α ‹vequalizer 𝔞 𝔤 𝔣› ?II ‹cat_Set α› ?II_II ‹ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣›
    by (rule 𝔞𝔟𝔤𝔣_is_cat_cone)

  show "∃!f'.
    f' : r' ↦⇘cat_Set α⇙ vequalizer 𝔞 𝔤 𝔣 ∧ 
    u' = ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF ntcf_const ?II (cat_Set α) f'"
    if "u' : r' <CF.cone ?II_II : ?II ↦↦C⇘α⇙ cat_Set α" for u' r'
  proof-
    
    interpret u': is_cat_cone α r' ?II ‹cat_Set α› ?II_II u' by (rule that(1))

    have "𝔞PL2 ∈∘ ?II⦇Obj⦈" 
      unfolding the_cat_parallel_2_components(1) by simp
    from 
      u'.ntcf_NTMap_is_arr[OF this] 
      𝔞𝔟𝔤𝔣.NTDom.HomCod.cat_cf_parallel_2_cat_equalizer[OF assms] 
    have u'_𝔞PL_is_arr: "u'⦇NTMap⦈⦇𝔞PL2⦈ : r' ↦⇘cat_Set α⇙ 𝔞"
      by (cs_prems_atom_step cat_cs_simps)
        (
          cs_prems
            cs_simp: cat_parallel_cs_simps 
            cs_intro: 
              cat_parallel_cs_intros 
              cat_cs_intros
              category.cat_cf_parallel_2_cat_equalizer
        )
    note u'_𝔞PL = cat_Set_is_arrD[OF u'_𝔞PL_is_arr]
    interpret u'_𝔞PL: arr_Set α ‹u'⦇NTMap⦈⦇𝔞PL2⦈› by (rule u'_𝔞PL(1))

    have "𝔟PL2 ∈∘ ?II⦇Obj⦈" 
      by (cs_concl cs_shallow cs_intro: cat_parallel_cs_intros)

    from 
      u'.ntcf_NTMap_is_arr[OF this] 
      𝔞𝔟𝔤𝔣.NTDom.HomCod.cat_cf_parallel_2_cat_equalizer[OF assms]
    have "u'⦇NTMap⦈⦇𝔟PL2⦈ : r' ↦⇘cat_Set α⇙ 𝔟"
      by 
        (
          cs_prems cs_shallow
            cs_simp: cat_cs_simps cat_parallel_cs_simps 
            cs_intro: cat_parallel_cs_intros
        )

    note u'_𝔤u' = cat_cone_cf_par_2_eps_NTMap_app(1)[OF that(1) assms]
    
    define q where "q = [u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈, r', vequalizer 𝔞 𝔤 𝔣]∘"

    have q_components[cat_Set_cs_simps]:  
      "q⦇ArrVal⦈ = u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈" 
      "q⦇ArrDom⦈ = r'" 
      "q⦇ArrCod⦈ = vequalizer 𝔞 𝔤 𝔣"
      unfolding q_def arr_field_simps by (simp_all add: nat_omega_simps)

    from cat_cone_cf_par_2_eps_NTMap_app[OF that(1) assms] have 𝔤u'_eq_𝔣u':
      "(𝔤 ∘A⇘cat_Set α⇙ u'⦇NTMap⦈⦇𝔞PL2⦈)⦇ArrVal⦈⦇x⦈ =
        (𝔣 ∘A⇘cat_Set α⇙ u'⦇NTMap⦈⦇𝔞PL2⦈)⦇ArrVal⦈⦇x⦈"
      for x 
      by simp

    show ?thesis
    proof(intro ex1I conjI; (elim conjE)?)

      have u'_NTMap_vrange: "ℛ∘ (u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈) ⊆∘ vequalizer 𝔞 𝔤 𝔣"
      proof(rule vsubsetI)
        fix y assume prems: "y ∈∘ ℛ∘ (u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈)"
        then obtain x where x: "x ∈∘ 𝒟∘ (u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈)" 
          and y_def: "y = u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈⦇x⦈"
          by (blast dest: u'_𝔞PL.ArrVal.vrange_atD)
        have x: "x ∈∘ r'" 
          by (use x u'_𝔞PL_is_arr in ‹cs_prems cs_shallow cs_simp: cat_cs_simps›)          
        from 𝔤u'_eq_𝔣u'[of x] assms x u'_𝔞PL_is_arr have [simp]: 
          "𝔤⦇ArrVal⦈⦇u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈⦇x⦈⦈ =
            𝔣⦇ArrVal⦈⦇u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈⦇x⦈⦈"
          by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        from prems u'_𝔞PL.arr_Set_ArrVal_vrange[unfolded u'_𝔞PL] show 
          "y ∈∘ vequalizer 𝔞 𝔤 𝔣"
          by (intro vequalizerI, unfold y_def) auto
      qed

      show q_is_arr: "q : r' ↦⇘cat_Set α⇙ vequalizer 𝔞 𝔤 𝔣" 
      proof(intro cat_Set_is_arrI arr_SetI)
        show "q⦇ArrCod⦈ ∈∘ Vset α" 
          by (auto simp: q_components intro: cat_cs_intros cat_lim_cs_intros)
      qed 
        (
          auto 
            simp: 
              cat_Set_cs_simps nat_omega_simps 
              u'_𝔞PL 
              q_def 
              u'_NTMap_vrange
              𝔞𝔟𝔤𝔣.NTDom.HomCod.cat_in_Obj_in_Vset
            intro: cat_cs_intros cat_lim_cs_intros
        )  

      from q_is_arr have 𝔞_q:
        "incl_Set (vequalizer 𝔞 𝔤 𝔣) 𝔞 ∘A⇘cat_Set α⇙ q : r' ↦⇘cat_Set α⇙ 𝔞"
        by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_Set_components(1)
              cs_intro: V_cs_intros cat_cs_intros cat_Set_cs_intros
          )
      interpret arr_Set α ‹incl_Set (vequalizer 𝔞 𝔤 𝔣) 𝔞 ∘A⇘cat_Set α⇙ q›
        using 𝔞_q by (auto dest: cat_Set_is_arrD)

      show "u' = ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF ntcf_const ?II (cat_Set α) q"
      proof(rule ntcf_eqI)
        from q_is_arr show 
          "ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF ntcf_const ?II (cat_Set α) q :
            cf_const ?II (cat_Set α) r' ↦CF 
            ?II_II : ?II ↦↦C⇘α⇙ cat_Set α"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        have dom_lhs: "𝒟∘ (u'⦇NTMap⦈) = ?II⦇Obj⦈" 
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)
        from q_is_arr have dom_rhs:
          "𝒟∘ 
            (
              (ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF 
              ntcf_const ?II (cat_Set α) q
            )⦇NTMap⦈) =  ?II⦇Obj⦈"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        show "u'⦇NTMap⦈ =
          (
            ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF ntcf_const ?II (cat_Set α) q
          )⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          show "vsv ((
            ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF ntcf_const ?II (cat_Set α) q
            )⦇NTMap⦈)"
            by (cs_concl cs_intro: cat_cs_intros)
          fix a assume prems: "a ∈∘ ?II⦇Obj⦈"
          have [symmetric, cat_Set_cs_simps]: 
            "u'⦇NTMap⦈⦇𝔞PL2⦈ = incl_Set (vequalizer 𝔞 𝔤 𝔣) 𝔞 ∘A⇘cat_Set α⇙ q"
          proof(rule arr_Set_eqI[of α])
            from u'_𝔞PL_is_arr have dom_lhs: "𝒟∘ (u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈) = r'"
              by 
                (
                  cs_concl cs_shallow 
                    cs_simp: cat_cs_simps cs_intro: cat_cs_intros
                )
            from 𝔞_q have dom_rhs: 
              "𝒟∘ ((incl_Set (vequalizer 𝔞 𝔤 𝔣) 𝔞 ∘A⇘cat_Set α⇙ q)⦇ArrVal⦈) = r'"
              by 
                (
                  cs_concl cs_shallow 
                    cs_simp: cat_cs_simps cs_intro: cat_cs_intros
                )
            show "u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈ =
              (incl_Set (vequalizer 𝔞 𝔤 𝔣) 𝔞 ∘A⇘cat_Set α⇙ q)⦇ArrVal⦈"
            proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
              fix a assume prems: "a ∈∘ r'"
              with u'_NTMap_vrange dom_lhs u'_𝔞PL.ArrVal.vsv_vimageI2 have 
                "u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈⦇a⦈ ∈∘ vequalizer 𝔞 𝔤 𝔣"
                by blast
              with prems q_is_arr u'_𝔞PL_is_arr show 
                "u'⦇NTMap⦈⦇𝔞PL2⦈⦇ArrVal⦈⦇a⦈ =
                  (incl_Set (vequalizer 𝔞 𝔤 𝔣) 𝔞 ∘A⇘cat_Set α⇙ q)⦇ArrVal⦈⦇a⦈"
                by 
                  (
                    cs_concl cs_shallow
                      cs_simp: cat_Set_cs_simps cat_cs_simps 
                      cs_intro: V_cs_intros cat_cs_intros cat_Set_cs_intros
                  )
            qed auto
          qed 
            (
              use u'_𝔞PL 𝔞_q in ‹
                cs_concl cs_shallow 
                  cs_intro: cat_Set_is_arrD(1) cs_simp: cat_cs_simps
                ›
            )+
          from q_is_arr have u'_NTMap_app_I: "u'⦇NTMap⦈⦇𝔞PL2⦈ =
            (
              ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF ntcf_const ?II (cat_Set α) q
            )⦇NTMap⦈⦇𝔞PL2⦈"
            by 
              (
                cs_concl 
                  cs_intro: cat_cs_intros cat_parallel_cs_intros 
                  cs_simp: cat_Set_cs_simps cat_cs_simps V_cs_simps
              )
          from q_is_arr assms have u'_NTMap_app_sI: "u'⦇NTMap⦈⦇𝔟PL2⦈ =
            (
              ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF ntcf_const ?II (cat_Set α) q
            )⦇NTMap⦈⦇𝔟PL2⦈"
            by 
              (
                cs_concl 
                  cs_simp: cat_Set_cs_simps cat_cs_simps u'_𝔤u' 
                  cs_intro: 
                    V_cs_intros 
                    cat_cs_intros 
                    cat_Set_cs_intros 
                    cat_parallel_cs_intros
              )
          from prems consider ‹a = 𝔞PL2› | ‹a = 𝔟PL2› 
            by (elim the_cat_parallel_2_ObjE)
          then show 
            "u'⦇NTMap⦈⦇a⦈ =
              (
                ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF
                ntcf_const ?II (cat_Set α) q
              )⦇NTMap⦈⦇a⦈"
            by cases (simp_all add: u'_NTMap_app_I u'_NTMap_app_sI)
        qed auto
      qed (simp_all add: u'.is_ntcf_axioms)
        
      fix f' assume prems:
        "f' : r' ↦⇘cat_Set α⇙ vequalizer 𝔞 𝔤 𝔣"
        "u' = ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF ntcf_const ?II (cat_Set α) f'"
      from prems(2) have u'_NTMap_app: 
        "u'⦇NTMap⦈⦇x⦈ =
          (ntcf_Set_equalizer α 𝔞 𝔟 𝔤 𝔣 ∙NTCF
          ntcf_const ?II (cat_Set α) f')⦇NTMap⦈⦇x⦈"
        for x
        by simp
      have u'_f': 
        "u'⦇NTMap⦈⦇𝔞PL2⦈ = incl_Set (vequalizer 𝔞 𝔤 𝔣) 𝔞 ∘A⇘cat_Set α⇙ f'"
        using u'_NTMap_app[of 𝔞PL2] prems(1)
        by 
          (
            cs_prems
              cs_simp: cat_cs_simps 
              cs_intro: cat_cs_intros cat_parallel_cs_intros
          )
          (
            cs_prems cs_shallow 
              cs_simp: cat_Set_cs_simps cs_intro: cat_parallel_cs_intros
          )

      note f' = cat_Set_is_arrD[OF prems(1)]
      note q = cat_Set_is_arrD[OF q_is_arr]

      interpret f': arr_Set α f' using prems(1) by (auto dest: cat_Set_is_arrD)
      interpret q: arr_Set α q using q by (auto dest: cat_Set_is_arrD)

      show "f' = q"
      proof(rule arr_Set_eqI[of α])
        have dom_lhs: "𝒟∘ (f'⦇ArrVal⦈) = r'" by (simp add: cat_Set_cs_simps f')
        from q_is_arr have dom_rhs: "𝒟∘ (q⦇ArrVal⦈) = r'" 
          by 
            (
              cs_concl cs_shallow 
                cs_simp: cat_cs_simps cs_intro: cat_Set_cs_intros
            )
        show "f'⦇ArrVal⦈ = q⦇ArrVal⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix i assume "i ∈∘ r'"
          with prems(1) show "f'⦇ArrVal⦈⦇i⦈ = q⦇ArrVal⦈⦇i⦈"
            by 
              (
                cs_concl
                  cs_simp: 
                    cat_Set_cs_simps cat_cs_simps 
                    q_components u'_f' cat_Set_components(1)
                  cs_intro: V_cs_intros cat_cs_intros cat_Set_cs_intros
              )
        qed auto
      qed 
        (
          use prems(1) q_is_arr in ‹
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cs_intro: q cat_Set_is_arrD
            ›
        )+
    qed
  qed

qed (auto intro: assms)



subsection‹The category ‹Set› is small-complete›

lemma (in 𝒵) cat_small_complete_cat_Set: "cat_small_complete α (cat_Set α)"
  ―‹This lemma appears as a remark on page 113 in
\cite{mac_lane_categories_2010}.›
proof(rule category.cat_small_complete_if_eq_and_obj_prod)
  show "∃E ε. ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ cat_Set α"
    if "𝔣 : 𝔞 ↦⇘cat_Set α⇙ 𝔟" and "𝔤 : 𝔞 ↦⇘cat_Set α⇙ 𝔟" for 𝔞 𝔟 𝔤 𝔣
    using ntcf_Set_equalizer_2_is_cat_equalizer_2[OF that(2,1)] by auto
  show "∃P π. π : P <CF.∏ A : I ↦↦C⇘α⇙ cat_Set α"
    if "tm_cf_discrete α I A (cat_Set α)" for A I
  proof(intro exI, rule tm_cf_discrete_ntcf_obj_prod_base_is_cat_obj_prod)
    interpret tm_cf_discrete α I A ‹cat_Set α› by (rule that)
    show "VLambda I A ∈∘ Vset α" by (rule tm_cf_discrete_ObjMap_in_Vset)
  qed
qed (rule category_cat_Set)

text‹\newpage›

end