Theory CZH_UCAT_Limit_Equalizer

(* Copyright 2021 (C) Mihails Milehins *)

section‹Equalizers and coequalizers as limits and colimits›
theory CZH_UCAT_Limit_Equalizer
  imports 
    CZH_UCAT_Limit
    CZH_Elementary_Categories.CZH_ECAT_Parallel
begin



subsection‹Equalizer and coequalizer›


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 F) (𝔟PL F) F› ℭ ‹⇑→⇑CF ℭ (𝔞PL F) (𝔟PL F) F 𝔞 𝔟 F'› E ε +
  F': vsv F'
  for α 𝔞 𝔟 F F' ℭ E ε +
  assumes cat_eq_F_in_Vset[cat_lim_cs_intros]: "F ∈∘ Vset α"
    and cat_eq_F_ne[cat_lim_cs_intros]: "F ≠ 0"
    and cat_eq_F'_vdomain[cat_lim_cs_simps]: "𝒟∘ F' = F"
    and cat_eq_F'_app_is_arr[cat_lim_cs_intros]: "𝔣 ∈∘ F ⟹ F'⦇𝔣⦈ : 𝔞 ↦⇘ℭ⇙ 𝔟"

syntax "_is_cat_equalizer" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ <CF.eq '(_,_,_,_') :/ ⇑C ↦↦Cı _)› [51, 51, 51, 51, 51, 51] 51)
syntax_consts "_is_cat_equalizer" ⇌ is_cat_equalizer
translations "ε : E <CF.eq (𝔞,𝔟,F,F') : ⇑C ↦↦C⇘α⇙ ℭ" ⇌
  "CONST is_cat_equalizer α 𝔞 𝔟 F F' ℭ E ε"

locale is_cat_coequalizer =
  is_cat_colimit α ‹⇑C (𝔟PL F) (𝔞PL F) F› ℭ ‹⇑→⇑CF ℭ (𝔟PL F) (𝔞PL F) F 𝔟 𝔞 F'› E ε +
  F': vsv F'
  for α 𝔞 𝔟 F F' ℭ E ε +
  assumes cat_coeq_F_in_Vset[cat_lim_cs_intros]: "F ∈∘ Vset α" 
    and cat_coeq_F_ne[cat_lim_cs_intros]: "F ≠ 0"
    and cat_coeq_F'_vdomain[cat_lim_cs_simps]: "𝒟∘ F' = F"
    and cat_coeq_F'_app_is_arr[cat_lim_cs_intros]: "𝔣 ∈∘ F ⟹ F'⦇𝔣⦈ : 𝔟 ↦⇘ℭ⇙ 𝔞"

syntax "_is_cat_coequalizer" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ '(_,_,_,_') >CF.coeq _ :/ ⇑C ↦↦Cı _)› [51, 51, 51, 51, 51, 51] 51)
syntax_consts "_is_cat_coequalizer" ⇌ is_cat_coequalizer
translations "ε : (𝔞,𝔟,F,F') >CF.coeq E : ⇑C ↦↦C⇘α⇙ ℭ" ⇌
  "CONST is_cat_coequalizer α 𝔞 𝔟 F F' ℭ E ε"


text‹Rules.›

lemma (in is_cat_equalizer) is_cat_equalizer_axioms'[cat_lim_cs_intros]:
  assumes "α' = α"
    and "E' = E"
    and "𝔞' = 𝔞"
    and "𝔟' = 𝔟"
    and "F'' = F"
    and "F''' = F'"
    and "ℭ' = ℭ"
  shows "ε : E' <CF.eq (𝔞',𝔟',F'',F''') : ⇑C ↦↦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 "F'' = F"
    and "F''' = F'"
    and "ℭ' = ℭ"
  shows "ε : (𝔞',𝔟',F'',F''') >CF.coeq E' : ⇑C ↦↦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.›

lemma (in is_cat_equalizer) 
  cat_eq_𝔞[cat_lim_cs_intros]: "𝔞 ∈∘ ℭ⦇Obj⦈"
  and cat_eq_𝔟[cat_lim_cs_intros]: "𝔟 ∈∘ ℭ⦇Obj⦈"
proof-
  from cat_eq_F_ne obtain 𝔣 where 𝔣: "𝔣 ∈∘ F" by force
  have "F'⦇𝔣⦈ : 𝔞 ↦⇘ℭ⇙ 𝔟" by (rule cat_eq_F'_app_is_arr[OF 𝔣])
  then show "𝔞 ∈∘ ℭ⦇Obj⦈" "𝔟 ∈∘ ℭ⦇Obj⦈" by auto
qed

lemma (in is_cat_coequalizer) 
  cat_coeq_𝔞[cat_lim_cs_intros]: "𝔞 ∈∘ ℭ⦇Obj⦈"
  and cat_coeq_𝔟[cat_lim_cs_intros]: "𝔟 ∈∘ ℭ⦇Obj⦈"
proof-
  from cat_coeq_F_ne obtain 𝔣 where 𝔣: "𝔣 ∈∘ F" by force
  have "F'⦇𝔣⦈ : 𝔟 ↦⇘ℭ⇙ 𝔞" by (rule cat_coeq_F'_app_is_arr[OF 𝔣])
  then show "𝔞 ∈∘ ℭ⦇Obj⦈" "𝔟 ∈∘ ℭ⦇Obj⦈" by auto
qed

sublocale is_cat_equalizer ⊆ cf_parallel α ‹𝔞PL F› ‹𝔟PL F› F 𝔞 𝔟 F' ℭ
  by (intro cf_parallelI cat_parallelI)
    (
      auto simp:
        cat_lim_cs_simps cat_parallel_cs_intros cat_lim_cs_intros cat_cs_intros
    )

sublocale is_cat_coequalizer ⊆ cf_parallel α ‹𝔟PL F› ‹𝔞PL F› F 𝔟 𝔞 F' ℭ
  by (intro cf_parallelI cat_parallelI)
    (
      auto simp:
        cat_lim_cs_simps cat_parallel_cs_intros cat_lim_cs_intros cat_cs_intros
    )


text‹Duality.›

lemma (in is_cat_equalizer) is_cat_coequalizer_op:
  "op_ntcf ε : (𝔞,𝔟,F,F') >CF.coeq E : ⇑C ↦↦C⇘α⇙ op_cat ℭ"
  by (intro is_cat_coequalizerI)
    (
      cs_concl 
        cs_simp: cat_lim_cs_simps cat_op_simps 
        cs_intro: V_cs_intros 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 ε : (𝔞,𝔟,F,F') >CF.coeq E : ⇑C ↦↦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 (𝔞,𝔟,F,F') : ⇑C ↦↦C⇘α⇙ op_cat ℭ"
  by (intro is_cat_equalizerI)
    (
      cs_concl 
        cs_simp: cat_lim_cs_simps cat_op_simps
        cs_intro: V_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 (𝔞,𝔟,F,F') : ⇑C ↦↦C⇘α⇙ ℭ'"
  unfolding assms by (rule is_cat_equalizer_op)

lemmas [cat_op_intros] = is_cat_coequalizer.is_cat_equalizer_op'


text‹Further properties.›

lemma (in category) cat_cf_parallel_𝔞𝔟:
  assumes "vsv F'"
    and "F ∈∘ Vset α" 
    and "𝒟∘ F' = F"
    and "⋀𝔣. 𝔣 ∈∘ F ⟹ F'⦇𝔣⦈ : 𝔞 ↦⇘ℭ⇙ 𝔟"
    and "𝔞 ∈∘ ℭ⦇Obj⦈"
    and "𝔟 ∈∘ ℭ⦇Obj⦈"
  shows "cf_parallel α (𝔞PL F) (𝔟PL F) F 𝔞 𝔟 F' ℭ"
proof-
  have "𝔞PL F ∈∘ Vset α" "𝔟PL F ∈∘ Vset α"
    by (simp_all add: Axiom_of_Pairing 𝔟PL_def 𝔞PL_def assms(2))
  then show ?thesis
    by (intro cf_parallelI cat_parallelI)
      (simp_all add: assms cat_parallel_cs_intros cat_cs_intros)
qed

lemma (in category) cat_cf_parallel_𝔟𝔞:
  assumes "vsv F'"
    and "F ∈∘ Vset α" 
    and "𝒟∘ F' = F"
    and "⋀𝔣. 𝔣 ∈∘ F ⟹ F'⦇𝔣⦈ : 𝔟 ↦⇘ℭ⇙ 𝔞"
    and "𝔞 ∈∘ ℭ⦇Obj⦈"
    and "𝔟 ∈∘ ℭ⦇Obj⦈"
  shows "cf_parallel α (𝔟PL F) (𝔞PL F) F 𝔟 𝔞 F' ℭ"
proof-
  have "𝔞PL F ∈∘ Vset α" "𝔟PL F ∈∘ Vset α"
    by (simp_all add: Axiom_of_Pairing 𝔟PL_def 𝔞PL_def assms(2))
  then show ?thesis
    by (intro cf_parallelI cat_parallelI)
      (simp_all add: assms cat_parallel_cs_intros cat_cs_intros)
qed

lemma cat_cone_cf_par_eps_NTMap_app:
  assumes "ε :
    E <CF.cone ⇑→⇑CF ℭ (𝔞PL F) (𝔟PL F) F 𝔞 𝔟 F' :
    ⇑C (𝔞PL F) (𝔟PL F) F ↦↦C⇘α⇙ ℭ"
    and "vsv F'"
    and "F ∈∘ Vset α" 
    and "𝒟∘ F' = F"
    and "⋀𝔣. 𝔣 ∈∘ F ⟹ F'⦇𝔣⦈ : 𝔞 ↦⇘ℭ⇙ 𝔟"
    and "𝔣 ∈∘ F"
  shows "ε⦇NTMap⦈⦇𝔟PL F⦈ = F'⦇𝔣⦈ ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈" 
proof-
  let ?II = ‹⇑C (𝔞PL F) (𝔟PL F) F› 
    and ?II_II = ‹⇑→⇑CF ℭ (𝔞PL F) (𝔟PL F) F 𝔞 𝔟 F'›
  interpret ε: is_cat_cone α E ?II ℭ ?II_II ε by (rule assms(1))
  from assms(5,6) have 𝔞: "𝔞 ∈∘ ℭ⦇Obj⦈" and 𝔟: "𝔟 ∈∘ ℭ⦇Obj⦈" by auto
  interpret par: cf_parallel α ‹𝔞PL F› ‹𝔟PL F› F 𝔞 𝔟 F' ℭ 
    by (intro ε.NTDom.HomCod.cat_cf_parallel_𝔞𝔟 assms 𝔞 𝔟)
  from assms(6) have 𝔣: "𝔣 : 𝔞PL F ↦⇘⇑C (𝔞PL F) (𝔟PL F) F⇙ 𝔟PL F" 
    by (simp_all add: par.the_cat_parallel_is_arr_𝔞𝔟F)
  note ε.cat_cone_Comp_commute[cat_cs_simps del]
  from ε.ntcf_Comp_commute[OF 𝔣] assms(6) show ?thesis
    by
      (
        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 "ε :
    ⇑→⇑CF ℭ (𝔟PL F) (𝔞PL F) F 𝔟 𝔞 F' >CF.cocone E :
    ⇑C (𝔟PL F) (𝔞PL F) F ↦↦C⇘α⇙ ℭ"
    and "vsv F'"
    and "F ∈∘ Vset α"
    and "𝒟∘ F' = F"
    and "⋀𝔣. 𝔣 ∈∘ F ⟹ F'⦇𝔣⦈ : 𝔟 ↦⇘ℭ⇙ 𝔞"
    and "𝔣 ∈∘ F"
  shows "ε⦇NTMap⦈⦇𝔟PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ F'⦇𝔣⦈"
proof-
  let ?II = ‹⇑C (𝔟PL F) (𝔞PL F) F› 
    and ?II_II = ‹⇑→⇑CF ℭ (𝔟PL F) (𝔞PL F) F 𝔟 𝔞 F'›
  interpret ε: is_cat_cocone α E ?II ℭ ?II_II ε by (rule assms(1))
  from assms(5,6) 
  have 𝔞: "𝔞 ∈∘ ℭ⦇Obj⦈" and 𝔟: "𝔟 ∈∘ ℭ⦇Obj⦈" and F'𝔣: "F'⦇𝔣⦈ : 𝔟 ↦⇘ℭ⇙ 𝔞" 
    by auto
  interpret par: cf_parallel α ‹𝔟PL F› ‹𝔞PL F› F 𝔟 𝔞 F' ℭ
    by (intro ε.NTDom.HomCod.cat_cf_parallel_𝔟𝔞 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-6),
      simplified
      ]
  from ε_NTMap_app F'𝔣 show ?thesis
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_parallel_cs_simps category.op_cat_Comp[symmetric] 
          cs_intro: cat_cs_intros cat_parallel_cs_intros
      )
qed

lemma (in is_cat_equalizer) cat_eq_eps_NTMap_app:
  assumes "𝔣 ∈∘ F"
  shows "ε⦇NTMap⦈⦇𝔟PL F⦈ = F'⦇𝔣⦈ ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈" 
  by 
    (
      intro cat_cone_cf_par_eps_NTMap_app[
        OF 
          is_cat_cone_axioms 
          F'.vsv_axioms 
          cat_eq_F_in_Vset 
          cat_eq_F'_vdomain
          cat_eq_F'_app_is_arr
          assms
        ]
    )+

lemma (in is_cat_coequalizer) cat_coeq_eps_NTMap_app:
  assumes "𝔣 ∈∘ F"
  shows "ε⦇NTMap⦈⦇𝔟PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ F'⦇𝔣⦈" 
  by 
    (
      intro cat_cocone_cf_par_eps_NTMap_app[
        OF is_cat_cocone_axioms
          F'.vsv_axioms 
          cat_coeq_F_in_Vset 
          cat_coeq_F'_vdomain
          cat_coeq_F'_app_is_arr
          assms
        ]
    )+

lemma (in is_cat_equalizer) cat_eq_Comp_eq: 
  assumes "𝔤 ∈∘ F" and "𝔣 ∈∘ F"
  shows "F'⦇𝔤⦈ ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈ = F'⦇𝔣⦈ ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈"
  using cat_eq_eps_NTMap_app[OF assms(1)] cat_eq_eps_NTMap_app[OF assms(2)]
  by auto

lemma (in is_cat_coequalizer) cat_coeq_Comp_eq: 
  assumes "𝔤 ∈∘ F" and "𝔣 ∈∘ F"
  shows "ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ F'⦇𝔤⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ F'⦇𝔣⦈"
  using cat_coeq_eps_NTMap_app[OF assms(1)] cat_coeq_eps_NTMap_app[OF assms(2)]
  by auto


subsubsection‹Universal property›

lemma is_cat_equalizerI':
  assumes "ε :
    E <CF.cone ⇑→⇑CF ℭ (𝔞PL F) (𝔟PL F) F 𝔞 𝔟 F' :
    ⇑C (𝔞PL F) (𝔟PL F) F ↦↦C⇘α⇙ ℭ"
    and "vsv F'"
    and "F ∈∘ Vset α" 
    and "𝒟∘ F' = F"
    and "⋀𝔣. 𝔣 ∈∘ F ⟹ F'⦇𝔣⦈ : 𝔞 ↦⇘ℭ⇙ 𝔟"
    and "𝔣 ∈∘ F" 
    and "⋀ε' E'. ε' :
      E' <CF.cone ⇑→⇑CF ℭ (𝔞PL F) (𝔟PL F) F 𝔞 𝔟 F' :
      ⇑C (𝔞PL F) (𝔟PL F) F ↦↦C⇘α⇙ ℭ ⟹
      ∃!f'. f' : E' ↦⇘ℭ⇙ E ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f'"
  shows "ε : E <CF.eq (𝔞,𝔟,F,F') : ⇑C ↦↦C⇘α⇙ ℭ"
proof-

  let ?II = ‹⇑C (𝔞PL F) (𝔟PL F) F› 
    and ?II_II = ‹⇑→⇑CF ℭ (𝔞PL F) (𝔟PL F) F 𝔞 𝔟 F'›
  interpret ε: is_cat_cone α E ?II ℭ ?II_II ε by (rule assms(1))
  from assms(5,6) have 𝔞: "𝔞 ∈∘ ℭ⦇Obj⦈" and 𝔟: "𝔟 ∈∘ ℭ⦇Obj⦈" by auto
  interpret par: cf_parallel α ‹𝔞PL F› ‹𝔟PL F› F 𝔞 𝔟 F' ℭ
    by (intro ε.NTDom.HomCod.cat_cf_parallel_𝔞𝔟 assms 𝔞 𝔟) simp
  
  show ?thesis
  proof(intro is_cat_equalizerI is_cat_limitI assms(1-3))
    fix u' r' assume prems: "u' : r' <CF.cone ?II_II : ?II ↦↦C⇘α⇙ ℭ"
    interpret u': is_cat_cone α r' ?II ℭ ?II_II u' by (rule prems)
    from assms(7)[OF prems] obtain f'
      where f': "f' : r' ↦⇘ℭ⇙ E"
        and u'_NTMap_app_𝔞: "u'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f'"
        and unique_f': 
          "⋀f''.
            ⟦
              f'' : r' ↦⇘ℭ⇙ E; 
              u'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f''
            ⟧ ⟹ f'' = f'"
      by metis
    show "∃!f'. f' : r' ↦⇘ℭ⇙ E ∧ u' = ε ∙NTCF ntcf_const ?II ℭ f'"
    proof(intro ex1I conjI; (elim conjE)?)
      show "u' = ε ∙NTCF ntcf_const ?II ℭ f'"
      proof(rule ntcf_eqI)
        show "u' : cf_const ?II ℭ r' ↦CF ?II_II : ?II ↦↦C⇘α⇙ ℭ"
          by (rule u'.is_ntcf_axioms)
        from f' show "ε ∙NTCF ntcf_const ?II ℭ f' :
          cf_const ?II ℭ r' ↦CF ?II_II : ?II ↦↦C⇘α⇙ ℭ"
          by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros )
        have dom_lhs: "𝒟∘ (u'⦇NTMap⦈) = ?II⦇Obj⦈"
          unfolding cat_cs_simps by simp
        from f' have dom_rhs:
          "𝒟∘ ((ε ∙NTCF ntcf_const ?II ℭ f')⦇NTMap⦈) = ?II⦇Obj⦈"
          by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        show "u'⦇NTMap⦈ = (ε ∙NTCF ntcf_const ?II ℭ f')⦇NTMap⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix a assume prems': "a ∈∘ ?II⦇Obj⦈"
          note [cat_parallel_cs_simps] = 
            cat_cone_cf_par_eps_NTMap_app[
              OF u'.is_cat_cone_axioms assms(2-5), simplified
              ]
            cat_cone_cf_par_eps_NTMap_app[OF assms(1-5), simplified]
            u'_NTMap_app_𝔞
          from prems' f' assms(6) show 
            "u'⦇NTMap⦈⦇a⦈ = (ε ∙NTCF ntcf_const ?II ℭ f')⦇NTMap⦈⦇a⦈"
            by (elim the_cat_parallel_ObjE; simp only:)
              (
                cs_concl 
                  cs_simp: cat_parallel_cs_simps cat_cs_simps
                  cs_intro: cat_cs_intros cat_parallel_cs_intros
              )
        qed (cs_concl cs_intro: V_cs_intros cat_cs_intros)+
      qed simp_all
      fix f'' assume prems'': 
        "f'' : r' ↦⇘ℭ⇙ E" "u' = ε ∙NTCF ntcf_const ?II ℭ f''"
      from prems''(2) have u'_NTMap_a:
        "u'⦇NTMap⦈⦇a⦈ = (ε ∙NTCF ntcf_const ?II ℭ f'')⦇NTMap⦈⦇a⦈"
        for a 
        by simp
      have "u'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f''"  
        using u'_NTMap_a[of ‹𝔞PL F›] prems''(1) 
        by 
          (
            cs_prems 
              cs_simp: cat_parallel_cs_simps cat_cs_simps 
              cs_intro: cat_parallel_cs_intros cat_cs_intros
          )
      from unique_f'[OF prems''(1) this] show "f'' = f'".
    qed (rule f')
  qed (use assms in fastforce)+

qed

lemma is_cat_coequalizerI':
  assumes "ε :
    ⇑→⇑CF ℭ (𝔟PL F) (𝔞PL F) F 𝔟 𝔞 F' >CF.cocone E : 
    ⇑C (𝔟PL F) (𝔞PL F) F ↦↦C⇘α⇙ ℭ"
    and "vsv F'"
    and "F ∈∘ Vset α" 
    and "𝒟∘ F' = F"
    and "⋀𝔣. 𝔣 ∈∘ F ⟹ F'⦇𝔣⦈ : 𝔟 ↦⇘ℭ⇙ 𝔞"
    and "𝔣 ∈∘ F" 
    and "⋀ε' E'. ε' :
      ⇑→⇑CF ℭ (𝔟PL F) (𝔞PL F) F 𝔟 𝔞 F' >CF.cocone E' : 
      ⇑C (𝔟PL F) (𝔞PL F) F ↦↦C⇘α⇙ ℭ ⟹
      ∃!f'. f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = f' ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈"
  shows "ε : (𝔞,𝔟,F,F') >CF.coeq E : ⇑C ↦↦C⇘α⇙ ℭ"
proof-

  let ?op_II = ‹⇑C (𝔟PL F) (𝔞PL F) F› 
    and ?op_II_II = ‹⇑→⇑CF ℭ (𝔟PL F) (𝔞PL F) F 𝔟 𝔞 F'›
    and ?II = ‹⇑C (𝔞PL F) (𝔟PL F) F›
    and ?II_II = ‹⇑→⇑CF (op_cat ℭ) (𝔞PL F) (𝔟PL F) F 𝔞 𝔟 F'›
  interpret ε: is_cat_cocone α E ?op_II ℭ ?op_II_II ε by (rule assms(1))
  from assms(5,6) have 𝔞: "𝔞 ∈∘ ℭ⦇Obj⦈" and 𝔟: "𝔟 ∈∘ ℭ⦇Obj⦈" by auto
  interpret par: cf_parallel α ‹𝔟PL F› ‹𝔞PL F› F 𝔟 𝔞 F' ℭ
    by (intro ε.NTDom.HomCod.cat_cf_parallel_𝔟𝔞 assms 𝔞 𝔟) simp

  interpret op_par: cf_parallel α ‹𝔞PL F› ‹𝔟PL F› F 𝔞 𝔟 F' ‹op_cat ℭ›
    by (rule par.cf_parallel_op)
  have assms_4':
    "∃!f'. f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘op_cat ℭ⇙ f'"
    if "ε' : E' <CF.cone ?II_II : ?II ↦↦C⇘α⇙ op_cat ℭ" for ε' E'
  proof-
    have [cat_op_simps]:
      "f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘op_cat ℭ⇙ f' ⟷
        f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = f' ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈"
      for f'
      by (intro iffI conjI; (elim conjE)?)
        (
          cs_concl cs_shallow
            cs_simp: category.op_cat_Comp[symmetric] cat_op_simps cat_cs_simps 
            cs_intro: cat_cs_intros cat_parallel_cs_intros
        )+
    interpret ε': is_cat_cone α E' ?II ‹op_cat ℭ› ?II_II ε' by (rule that)
    show ?thesis
      unfolding cat_op_simps
      by 
        (
          rule assms(7)[
            OF ε'.is_cat_cocone_op[unfolded cat_op_simps], 
            unfolded cat_op_simps
            ]
        )
  qed
  interpret op_ε: is_cat_equalizer α 𝔞 𝔟 F F' ‹op_cat ℭ› E ‹op_ntcf ε› 
    by 
      (
        rule 
          is_cat_equalizerI'
            [
              OF ε.is_cat_cone_op[unfolded cat_op_simps], 
              unfolded cat_op_simps, 
              OF assms(2-6) assms_4',
              simplified
            ]
      )
  show ?thesis by (rule op_ε.is_cat_coequalizer_op[unfolded cat_op_simps])

qed

lemma (in is_cat_equalizer) cat_eq_unique_cone:
  assumes "ε' :
    E' <CF.cone ⇑→⇑CF ℭ (𝔞PL F) (𝔟PL F) F 𝔞 𝔟 F' : ⇑C (𝔞PL F) (𝔟PL F) F ↦↦C⇘α⇙ ℭ"
    (is ‹ε' : E' <CF.cone ?II_II : ?II ↦↦C⇘α⇙ ℭ›)
  shows "∃!f'. f' : E' ↦⇘ℭ⇙ E ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f'"
proof-

  interpret ε': is_cat_cone α E' ?II ℭ ?II_II ε' by (rule assms(1))
  from cat_lim_ua_fo[OF assms(1)] obtain f' where f': "f' : E' ↦⇘ℭ⇙ E"
    and ε'_def: "ε' = ε ∙NTCF ntcf_const ?II ℭ f'"
    and unique: 
      "⟦ f'' : E' ↦⇘ℭ⇙ E; ε' = ε ∙NTCF ntcf_const ?II ℭ f'' ⟧ ⟹ f'' = f'" 
    for f''
    by auto
  from cat_eq_F_ne obtain 𝔣 where 𝔣: "𝔣 ∈∘ F" by force

  show ?thesis
  proof(intro ex1I conjI; (elim conjE)?)
    show f': "f' : E' ↦⇘ℭ⇙ E" by (rule f')
    from ε'_def have "ε'⦇NTMap⦈⦇𝔞PL F⦈ = (ε ∙NTCF ntcf_const ?II ℭ f')⦇NTMap⦈⦇𝔞PL F⦈"
      by simp
    from this f' show ε'_NTMap_app_I: "ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f'"
      by 
        (
          cs_prems 
            cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_parallel_cs_intros
        )
    fix f'' assume prems: 
      "f'' : E' ↦⇘ℭ⇙ E" "ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f''"
    have "ε' = ε ∙NTCF ntcf_const ?II ℭ f''"
    proof(rule ntcf_eqI[OF ])
      show "ε' : cf_const ?II ℭ E' ↦CF ?II_II : ?II ↦↦C⇘α⇙ ℭ"
        by (rule ε'.is_ntcf_axioms)
      from f' prems(1) show "ε ∙NTCF ntcf_const ?II ℭ f'' :
        cf_const ?II ℭ E' ↦CF ?II_II : ?II ↦↦C⇘α⇙ ℭ"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      show "ε'⦇NTMap⦈ = (ε ∙NTCF ntcf_const ?II ℭ f'')⦇NTMap⦈"
      proof(rule vsv_eqI, unfold cat_cs_simps)
        show "vsv ((ε ∙NTCF ntcf_const ?II ℭ f'')⦇NTMap⦈)"
          by (cs_concl cs_intro: cat_cs_intros)
        from prems(1) show "?II⦇Obj⦈ = 𝒟∘ ((ε ∙NTCF ntcf_const ?II ℭ f'')⦇NTMap⦈)"
          by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        fix a assume prems': "a ∈∘ ?II⦇Obj⦈"
        note [cat_cs_simps] = 
          cat_eq_eps_NTMap_app[OF 𝔣]
          cat_cone_cf_par_eps_NTMap_app
            [
              OF 
                ε'.is_cat_cone_axioms 
                F'.vsv_axioms 
                cat_eq_F_in_Vset 
                cat_eq_F'_vdomain 
                cat_eq_F'_app_is_arr 𝔣, 
              simplified
            ]
        from prems' prems(1) 𝔣 have [cat_cs_simps]: 
          "ε'⦇NTMap⦈⦇a⦈ = ε⦇NTMap⦈⦇a⦈ ∘A⇘ℭ⇙ f''"
          by (elim the_cat_parallel_ObjE; simp only:)
            (
                cs_concl 
                  cs_simp: cat_cs_simps cat_parallel_cs_simps prems(2)
                  cs_intro: cat_cs_intros cat_parallel_cs_intros
            )+
        from prems' prems show 
          "ε'⦇NTMap⦈⦇a⦈ = (ε ∙NTCF ntcf_const ?II ℭ f'')⦇NTMap⦈⦇a⦈"
          by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      qed auto
    qed simp_all
    from unique[OF prems(1) this] show "f'' = f'" .
  qed

qed

lemma (in is_cat_equalizer) cat_eq_unique:
  assumes "ε' : E' <CF.eq (𝔞,𝔟,F,F') : ⇑C ↦↦C⇘α⇙ ℭ"
  shows 
    "∃!f'. f' : E' ↦⇘ℭ⇙ E ∧ ε' = ε ∙NTCF ntcf_const (⇑C (𝔞PL F) (𝔟PL F) F) ℭ f'"
  by (rule cat_lim_unique[OF is_cat_equalizerD(1)[OF assms]])

lemma (in is_cat_equalizer) cat_eq_unique':
  assumes "ε' : E' <CF.eq (𝔞,𝔟,F,F') : ⇑C ↦↦C⇘α⇙ ℭ"
  shows "∃!f'. f' : E' ↦⇘ℭ⇙ E ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f'"
proof-
  interpret ε': is_cat_equalizer α 𝔞 𝔟 F F' ℭ E' ε' by (rule assms(1))
  show ?thesis by (rule cat_eq_unique_cone[OF ε'.is_cat_cone_axioms])
qed

lemma (in is_cat_coequalizer) cat_coeq_unique_cocone:
  assumes "ε' :
    ⇑→⇑CF ℭ (𝔟PL F) (𝔞PL F) F 𝔟 𝔞 F' >CF.cocone E' : 
    ⇑C (𝔟PL F) (𝔞PL F) F ↦↦C⇘α⇙ ℭ"
    (is ‹ε' : ?II_II >CF.cocone E' : ?II ↦↦C⇘α⇙ ℭ›)
  shows "∃!f'. f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = f' ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈"
proof-
  interpret ε': is_cat_cocone α E' ?II ℭ ?II_II ε' by (rule assms(1))
  have [cat_op_simps]:
    "f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘op_cat ℭ⇙ f' ⟷
      f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = f' ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈" 
    for f'
    by (intro iffI conjI; (elim conjE)?)
      (
        cs_concl cs_shallow
          cs_simp: category.op_cat_Comp[symmetric] cat_op_simps cat_cs_simps 
          cs_intro: cat_cs_intros cat_parallel_cs_intros
      )+
  show ?thesis
    by 
      (
        rule is_cat_equalizer.cat_eq_unique_cone[
          OF is_cat_equalizer_op ε'.is_cat_cone_op[unfolded cat_op_simps],
          unfolded cat_op_simps
          ]
     )
qed

lemma (in is_cat_coequalizer) cat_coeq_unique:
  assumes "ε' : (𝔞,𝔟,F,F') >CF.coeq E' : ⇑C ↦↦C⇘α⇙ ℭ"
  shows "∃!f'.
    f' : E ↦⇘ℭ⇙ E' ∧ ε' = ntcf_const (⇑C (𝔟PL F) (𝔞PL F) F) ℭ f' ∙NTCF ε"
  by (rule cat_colim_unique[OF is_cat_coequalizerD(1)[OF assms]])

lemma (in is_cat_coequalizer) cat_coeq_unique':
  assumes "ε' : (𝔞,𝔟,F,F') >CF.coeq E' : ⇑C ↦↦C⇘α⇙ ℭ"
  shows "∃!f'. f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL F⦈ = f' ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈"
proof-
  interpret ε': is_cat_coequalizer α 𝔞 𝔟 F F' ℭ E' ε' by (rule assms(1))
  show ?thesis by (rule cat_coeq_unique_cocone[OF ε'.is_cat_cocone_axioms])
qed

lemma cat_equalizer_ex_is_iso_arr:
  assumes "ε : E <CF.eq (𝔞,𝔟,F,F') : ⇑C ↦↦C⇘α⇙ ℭ" 
    and "ε' : E' <CF.eq (𝔞,𝔟,F,F') : ⇑C ↦↦C⇘α⇙ ℭ"
  obtains f where "f : E' ↦iso⇘ℭ⇙ E"
    and "ε' = ε ∙NTCF ntcf_const (⇑C (𝔞PL F) (𝔟PL F) F) ℭ f"
proof-
  interpret ε: is_cat_equalizer α 𝔞 𝔟 F F' ℭ E ε by (rule assms(1))
  interpret ε': is_cat_equalizer α 𝔞 𝔟 F F' ℭ E' ε' 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_equalizer_ex_is_iso_arr':
  assumes "ε : E <CF.eq (𝔞,𝔟,F,F') : ⇑C ↦↦C⇘α⇙ ℭ" 
    and "ε' : E' <CF.eq (𝔞,𝔟,F,F') : ⇑C ↦↦C⇘α⇙ ℭ"
  obtains f where "f : E' ↦iso⇘ℭ⇙ E"
    and "ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f"
    and "ε'⦇NTMap⦈⦇𝔟PL F⦈ = ε⦇NTMap⦈⦇𝔟PL F⦈ ∘A⇘ℭ⇙ f"
proof-
  interpret ε: is_cat_equalizer α 𝔞 𝔟 F F' ℭ E ε by (rule assms(1))
  interpret ε': is_cat_equalizer α 𝔞 𝔟 F F' ℭ E' ε' by (rule assms(2))
  obtain f where f: "f : E' ↦iso⇘ℭ⇙ E"
    and "j ∈∘ ⇑C (𝔞PL F) (𝔟PL F) F⦇Obj⦈ ⟹ ε'⦇NTMap⦈⦇j⦈ = ε⦇NTMap⦈⦇j⦈ ∘A⇘ℭ⇙ f" for j
    by 
      (
        elim cat_lim_ex_is_iso_arr'[
          OF ε.is_cat_limit_axioms ε'.is_cat_limit_axioms
          ]
      )
  then have 
    "ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f"
    "ε'⦇NTMap⦈⦇𝔟PL F⦈ = ε⦇NTMap⦈⦇𝔟PL F⦈ ∘A⇘ℭ⇙ f"
    unfolding the_cat_parallel_components by auto
  with f show ?thesis using that by simp
qed

lemma cat_coequalizer_ex_is_iso_arr:
  assumes "ε : (𝔞,𝔟,F,F') >CF.coeq E : ⇑C ↦↦C⇘α⇙ ℭ"
    and "ε' : (𝔞,𝔟,F,F') >CF.coeq E' : ⇑C ↦↦C⇘α⇙ ℭ"
  obtains f where "f : E ↦iso⇘ℭ⇙ E'" 
    and "ε' = ntcf_const (⇑C (𝔟PL F) (𝔞PL F) F)  ℭ f ∙NTCF ε"
proof-
  interpret ε: is_cat_coequalizer α 𝔞 𝔟 F F' ℭ E ε by (rule assms(1))
  interpret ε': is_cat_coequalizer α 𝔞 𝔟 F F' ℭ E' ε' 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_coequalizer_ex_is_iso_arr':
  assumes "ε : (𝔞,𝔟,F,F') >CF.coeq E : ⇑C ↦↦C⇘α⇙ ℭ"
    and "ε' : (𝔞,𝔟,F,F') >CF.coeq E' : ⇑C ↦↦C⇘α⇙ ℭ"
  obtains f where "f : E ↦iso⇘ℭ⇙ E'" 
    and "ε'⦇NTMap⦈⦇𝔞PL F⦈ = f ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈"
    and "ε'⦇NTMap⦈⦇𝔟PL F⦈ = f ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔟PL F⦈"
proof-
  interpret ε: is_cat_coequalizer α 𝔞 𝔟 F F' ℭ E ε by (rule assms(1))
  interpret ε': is_cat_coequalizer α 𝔞 𝔟 F F' ℭ E' ε' by (rule assms(2))
  obtain f where f: "f : E ↦iso⇘ℭ⇙ E'"
    and "j ∈∘ ⇑C (𝔟PL F) (𝔞PL F) F⦇Obj⦈ ⟹ ε'⦇NTMap⦈⦇j⦈ = f ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇j⦈" for j
    by
      (
        elim cat_colim_ex_is_iso_arr'[
          OF ε.is_cat_colimit_axioms ε'.is_cat_colimit_axioms
          ]
      )
  then have 
    "ε'⦇NTMap⦈⦇𝔞PL F⦈ = f ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL F⦈"
    "ε'⦇NTMap⦈⦇𝔟PL F⦈ = f ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔟PL F⦈"
    unfolding the_cat_parallel_components by auto
  with f show ?thesis using that by simp
qed


subsubsection‹Further properties›

lemma (in is_cat_equalizer) cat_eq_is_monic_arr: 
  ―‹See subsection 3.3 in \cite{awodey_category_2010}.›
  "ε⦇NTMap⦈⦇𝔞PL F⦈ : E ↦mon⇘ℭ⇙ 𝔞"
proof(intro is_monic_arrI)
  show "ε⦇NTMap⦈⦇𝔞PL F⦈ : E ↦⇘ℭ⇙ 𝔞"
    by
      (
        cs_concl
          cs_simp: cat_cs_simps cat_parallel_cs_simps 
          cs_intro: cat_cs_intros cat_parallel_cs_intros
      )
  fix f g a
  assume prems:
    "f : a ↦⇘ℭ⇙ E"
    "g : a ↦⇘ℭ⇙ E"
    "ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ g"
  define ε' where "ε' = ε ∙NTCF ntcf_const (⇑C (𝔞PL F) (𝔟PL F) F) ℭ f"
  from prems(1) have "ε' :
    a <CF.cone ⇑→⇑CF ℭ (𝔞PL F) (𝔟PL F) F 𝔞 𝔟 F' :
    ⇑C (𝔞PL F) (𝔟PL F) F ↦↦C⇘α⇙ ℭ"
    unfolding ε'_def 
    by (cs_concl cs_shallow cs_intro: is_cat_coneI cat_cs_intros)    
  from cat_eq_unique_cone[OF this] obtain f' 
    where f': "f' : a ↦⇘ℭ⇙ E"
      and ε'_𝔞: "ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f'"
      and unique_f': "⋀f''.
        ⟦ f'' : a ↦⇘ℭ⇙ E; ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f'' ⟧ ⟹
          f'' = f'"
    by meson
  from prems(1) have unique_f: "ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ f"
    unfolding ε'_def
    by
      (
        cs_concl 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_parallel_cs_intros
      )
  from prems(1) have unique_g: "ε'⦇NTMap⦈⦇𝔞PL F⦈ = ε⦇NTMap⦈⦇𝔞PL F⦈ ∘A⇘ℭ⇙ g"
    unfolding ε'_def
    by
      (
        cs_concl
          cs_simp: prems(3) cat_cs_simps
          cs_intro: cat_cs_intros cat_parallel_cs_intros
      )
  show "f = g"
    by 
      (
        rule unique_f'
          [
            OF prems(1) unique_f,
            unfolded unique_f'[OF prems(2) unique_g, symmetric]
          ]
      )
qed

lemma (in is_cat_coequalizer) cat_coeq_is_epic_arr: 
  "ε⦇NTMap⦈⦇𝔞PL F⦈ : 𝔞 ↦epi⇘ℭ⇙ E"
  by
    (
      rule is_cat_equalizer.cat_eq_is_monic_arr[
        OF is_cat_equalizer_op, unfolded cat_op_simps
        ]
    )



subsection‹Equalizer and coequalizer for two arrows›


subsubsection‹Definition and elementary properties›


text‹
See cite‹"noauthor_wikipedia_2001"›\footnote{
\url{https://en.wikipedia.org/wiki/Equaliser_(mathematics)}
}.
›

locale is_cat_equalizer_2 =
  is_cat_limit α ‹↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL› ℭ ‹↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣› E ε 
  for α 𝔞 𝔟 𝔤 𝔣 ℭ E ε +
  assumes cat_eq_𝔤[cat_lim_cs_intros]: "𝔤 : 𝔞 ↦⇘ℭ⇙ 𝔟"
    and cat_eq_𝔣[cat_lim_cs_intros]: "𝔣 : 𝔞 ↦⇘ℭ⇙ 𝔟"

syntax "_is_cat_equalizer_2" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ <CF.eq '(_,_,_,_') :/ ↑↑C ↦↦Cı _)› [51, 51, 51, 51, 51, 51] 51)
syntax_consts "_is_cat_equalizer_2" ⇌ is_cat_equalizer_2
translations "ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ" ⇌
  "CONST is_cat_equalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E ε"

locale is_cat_coequalizer_2 =
  is_cat_colimit 
    α ‹↑↑C 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL› ℭ ‹↑↑→↑↑CF ℭ 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL 𝔟 𝔞 𝔣 𝔤› E ε 
  for α 𝔞 𝔟 𝔤 𝔣 ℭ E ε +
  assumes cat_coeq_𝔤[cat_lim_cs_intros]: "𝔤 : 𝔟 ↦⇘ℭ⇙ 𝔞"
    and cat_coeq_𝔣[cat_lim_cs_intros]: "𝔣 : 𝔟 ↦⇘ℭ⇙ 𝔞"

syntax "_is_cat_coequalizer_2" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ '(_,_,_,_') >CF.coeq _ :/ ↑↑C ↦↦Cı _)› [51, 51, 51, 51, 51, 51] 51)
syntax_consts "_is_cat_coequalizer_2" ⇌ is_cat_coequalizer_2
translations "ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ" ⇌
  "CONST is_cat_coequalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E ε"


text‹Rules.›

lemma (in is_cat_equalizer_2) is_cat_equalizer_2_axioms'[cat_lim_cs_intros]:
  assumes "α' = α"
    and "E' = E"
    and "𝔞' = 𝔞"
    and "𝔟' = 𝔟"
    and "𝔤' = 𝔤"
    and "𝔣' = 𝔣"
    and "ℭ' = ℭ"
  shows "ε : E' <CF.eq (𝔞',𝔟',𝔤',𝔣') : ↑↑C ↦↦C⇘α'⇙ ℭ'"
  unfolding assms by (rule is_cat_equalizer_2_axioms)

mk_ide rf is_cat_equalizer_2_def[unfolded is_cat_equalizer_2_axioms_def]
  |intro is_cat_equalizer_2I|
  |dest is_cat_equalizer_2D[dest]|
  |elim is_cat_equalizer_2E[elim]|

lemmas [cat_lim_cs_intros] = is_cat_equalizer_2D(1)

lemma (in is_cat_coequalizer_2) is_cat_coequalizer_2_axioms'[cat_lim_cs_intros]:
  assumes "α' = α"
    and "E' = E"
    and "𝔞' = 𝔞"
    and "𝔟' = 𝔟"
    and "𝔤' = 𝔤"
    and "𝔣' = 𝔣"
    and "ℭ' = ℭ"
  shows "ε : (𝔞',𝔟',𝔤',𝔣') >CF.coeq E' : ↑↑C ↦↦C⇘α'⇙ ℭ'"
  unfolding assms by (rule is_cat_coequalizer_2_axioms)

mk_ide rf is_cat_coequalizer_2_def[unfolded is_cat_coequalizer_2_axioms_def]
  |intro is_cat_coequalizer_2I|
  |dest is_cat_coequalizer_2D[dest]|
  |elim is_cat_coequalizer_2E[elim]|

lemmas [cat_lim_cs_intros] = is_cat_coequalizer_2D(1)


text‹Helper lemmas.›

(*FIXME*)
lemma cat_eq_F'_helper:
  "(λf∈∘set {𝔣PL, 𝔤PL}. (f = 𝔤PL ? 𝔤 : 𝔣)) =
    (λf∈∘set {𝔣PL, 𝔤PL}. (f = 𝔣PL ? 𝔣 : 𝔤))"
  using cat_PL2_𝔤𝔣 by (simp add: VLambda_vdoubleton)


text‹Elementary properties.›

sublocale is_cat_equalizer_2 ⊆ cf_parallel_2 α 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣 ℭ 
  by (intro cf_parallel_2I cat_parallel_2I)
    (simp_all add: cat_parallel_cs_intros cat_lim_cs_intros cat_cs_intros)

sublocale is_cat_coequalizer_2 ⊆ cf_parallel_2 α 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL 𝔟 𝔞 𝔣 𝔤 ℭ
  by (intro cf_parallel_2I cat_parallel_2I)
    (
      auto simp: 
        cat_parallel_cs_intros cat_lim_cs_intros cat_cs_intros 
        cat_PL2_ineq[symmetric]
    )

lemma (in is_cat_equalizer_2) cat_equalizer_2_is_cat_equalizer:
  "ε :
    E <CF.eq (𝔞,𝔟,set {𝔤PL, 𝔣PL},(λf∈∘set {𝔤PL, 𝔣PL}. (f = 𝔣PL ? 𝔣 : 𝔤))) : 
    ⇑C ↦↦C⇘α⇙ ℭ"
  by 
    (
      intro is_cat_equalizerI, 
      rule is_cat_limit_axioms[
        unfolded the_cf_parallel_2_def the_cat_parallel_2_def 𝔞PL2_def 𝔟PL2_def
        ]
    ) 
    (auto simp: Limit_vdoubleton_in_VsetI cat_parallel_cs_intros)

lemma (in is_cat_coequalizer_2) cat_coequalizer_2_is_cat_coequalizer:
  "ε :
    (𝔞,𝔟,set {𝔤PL, 𝔣PL},(λf∈∘set {𝔤PL, 𝔣PL}. (f = 𝔣PL ? 𝔣 : 𝔤))) >CF.coeq E :
    ⇑C ↦↦C⇘α⇙ ℭ"
proof
  (
    intro is_cat_coequalizerI, 
    fold the_cf_parallel_2_def the_cat_parallel_2_def 𝔞PL2_def 𝔟PL2_def
  )
  show "ε :
    ↑↑→↑↑CF ℭ 𝔟PL2 𝔞PL2 𝔤PL 𝔣PL 𝔟 𝔞 𝔤 𝔣 >CF.colim E :
    ↑↑C 𝔟PL2 𝔞PL2 𝔤PL 𝔣PL ↦↦C⇘α⇙ ℭ"
    by 
      (
        subst the_cat_parallel_2_commute, 
        subst cf_parallel_2_the_cf_parallel_2_commute[symmetric]
      )
      (intro is_cat_colimit_axioms)
qed (auto simp: Limit_vdoubleton_in_VsetI cat_parallel_cs_intros)

lemma cat_equalizer_is_cat_equalizer_2:
  assumes "ε :
    E <CF.eq (𝔞,𝔟,set {𝔤PL, 𝔣PL},(λf∈∘set {𝔤PL, 𝔣PL}. (f = 𝔣PL ? 𝔣 : 𝔤))) :
    ⇑C ↦↦C⇘α⇙ ℭ"
  shows "ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ"
proof-
  interpret ε: is_cat_equalizer 
    α 𝔞 𝔟 ‹set {𝔤PL, 𝔣PL}› ‹(λf∈∘set {𝔤PL, 𝔣PL}. (f = 𝔣PL ? 𝔣 : 𝔤))› ℭ E ε
    by (rule assms)
  have 𝔣PL: "𝔣PL ∈∘ set {𝔤PL, 𝔣PL}" and 𝔤PL: "𝔤PL ∈∘ set {𝔤PL, 𝔣PL}" by auto
  show ?thesis
    using ε.cat_eq_F'_app_is_arr[OF 𝔤PL] ε.cat_eq_F'_app_is_arr[OF 𝔣PL] 
    by 
      (
        intro 
          is_cat_equalizer_2I 
          ε.is_cat_limit_axioms
            [
              folded 
                the_cf_parallel_2_def the_cat_parallel_2_def 𝔞PL2_def 𝔟PL2_def
            ]
      )
      (auto simp: cat_PL2_𝔤𝔣)
qed

lemma cat_coequalizer_is_cat_coequalizer_2:
  assumes "ε :
    (𝔞,𝔟,set {𝔤PL, 𝔣PL},(λf∈∘set {𝔤PL, 𝔣PL}. (f = 𝔣PL ? 𝔣 : 𝔤))) >CF.coeq E :
    ⇑C ↦↦C⇘α⇙ ℭ"
  shows "ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ"
proof-
  interpret is_cat_coequalizer 
    α 𝔞 𝔟 ‹set {𝔤PL, 𝔣PL}› ‹(λf∈∘set {𝔤PL, 𝔣PL}. (f = 𝔣PL ? 𝔣 : 𝔤))› ℭ E ε
    by (rule assms)
  interpret cf_parallel_2 α 𝔟PL2 𝔞PL2 𝔤PL 𝔣PL 𝔟 𝔞 𝔤 𝔣 ℭ
    by 
      (
        rule cf_parallel_is_cf_parallel_2[
          OF cf_parallel_axioms cat_PL2_𝔤𝔣, folded 𝔞PL2_def 𝔟PL2_def
          ]
      )
  show "ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ"
    by
      (
        intro is_cat_coequalizer_2I, 
        subst the_cat_parallel_2_commute, 
        subst cf_parallel_2_the_cf_parallel_2_commute[symmetric], 
        rule is_cat_colimit_axioms[
          folded 𝔞PL2_def 𝔟PL2_def the_cat_parallel_2_def the_cf_parallel_2_def
          ]
      )
      (simp_all add: cf_parallel_𝔣' cf_parallel_𝔤')
qed


text‹Duality.›

lemma (in is_cat_equalizer_2) is_cat_coequalizer_2_op:
  "op_ntcf ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ op_cat ℭ"
  unfolding is_cat_equalizer_def
  by 
    (
      rule cat_coequalizer_is_cat_coequalizer_2
        [
          OF is_cat_equalizer.is_cat_coequalizer_op[
            OF cat_equalizer_2_is_cat_equalizer
          ]
        ]
    )

lemma (in is_cat_equalizer_2) is_cat_coequalizer_2_op'[cat_op_intros]:
  assumes "ℭ' = op_cat ℭ"
  shows "op_ntcf ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ'"
  unfolding assms by (rule is_cat_coequalizer_2_op)

lemmas [cat_op_intros] = is_cat_equalizer_2.is_cat_coequalizer_2_op'

lemma (in is_cat_coequalizer_2) is_cat_equalizer_2_op:
  "op_ntcf ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ op_cat ℭ"
  unfolding is_cat_coequalizer_def
  by 
    (
      rule cat_equalizer_is_cat_equalizer_2
        [
          OF is_cat_coequalizer.is_cat_equalizer_op[
            OF cat_coequalizer_2_is_cat_coequalizer
          ]
        ]
    )

lemma (in is_cat_coequalizer_2) is_cat_equalizer_2_op'[cat_op_intros]:
  assumes "ℭ' = op_cat ℭ"
  shows "op_ntcf ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ'"
  unfolding assms by (rule is_cat_equalizer_2_op)

lemmas [cat_op_intros] = is_cat_coequalizer_2.is_cat_equalizer_2_op'


text‹Further properties.›

lemma (in category) cat_cf_parallel_2_cat_equalizer: 
  assumes "𝔤 : 𝔞 ↦⇘ℭ⇙ 𝔟" and "𝔣 : 𝔞 ↦⇘ℭ⇙ 𝔟"
  shows "cf_parallel_2 α 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣 ℭ"
  using assms 
  by (intro cf_parallel_2I cat_parallel_2I)
    (auto simp: cat_parallel_cs_intros cat_cs_intros)

lemma (in category) cat_cf_parallel_2_cat_coequalizer: 
  assumes "𝔤 : 𝔟 ↦⇘ℭ⇙ 𝔞" and "𝔣 : 𝔟 ↦⇘ℭ⇙ 𝔞"
  shows "cf_parallel_2 α 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL 𝔟 𝔞 𝔣 𝔤 ℭ"
  using assms 
  by (intro cf_parallel_2I cat_parallel_2I)
    (simp_all add: cat_parallel_cs_intros cat_cs_intros cat_PL2_ineq[symmetric])

lemma cat_cone_cf_par_2_eps_NTMap_app:
  assumes "ε :
    E <CF.cone ↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣 : ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL ↦↦C⇘α⇙ ℭ"
    and "𝔤 : 𝔞 ↦⇘ℭ⇙ 𝔟" 
    and "𝔣 : 𝔞 ↦⇘ℭ⇙ 𝔟"
  shows 
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = 𝔤 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈" 
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = 𝔣 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
proof-
  let ?II = ‹↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL› 
    and ?II_II = ‹↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣›
    and ?F = ‹set {𝔤PL, 𝔣PL}›
  interpret ε: is_cat_cone α E ?II ℭ ?II_II ε by (rule assms(1))
  from ε.cat_PL2_𝔣 ε.cat_PL2_𝔤 have 𝔤𝔣: "?F ∈∘ Vset α"
    by (intro Limit_vdoubleton_in_VsetI)  auto
  from assms(2,3) have
    "(⋀𝔣'. 𝔣' ∈∘ ?F ⟹ (λf∈∘?F. (f = 𝔣PL ? 𝔣 : 𝔤))⦇𝔣'⦈ : 𝔞 ↦⇘ℭ⇙ 𝔟)"
    by auto
  note cat_cone_cf_par_eps_NTMap_app = cat_cone_cf_par_eps_NTMap_app
      [
        OF 
          assms(1)[
            unfolded 
              the_cat_parallel_2_def the_cf_parallel_2_def 𝔞PL2_def 𝔟PL2_def
            ], 
        folded 𝔞PL2_def 𝔟PL2_def, OF _ 𝔤𝔣 _ this,
        simplified
      ]
  from
    cat_cone_cf_par_eps_NTMap_app[of 𝔤PL, simplified]
    cat_cone_cf_par_eps_NTMap_app[of 𝔣PL, simplified]
    cat_PL2_𝔤𝔣
  show 
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = 𝔤 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈" 
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = 𝔣 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
    by fastforce+
qed

lemma cat_cocone_cf_par_2_eps_NTMap_app:
  assumes "ε :
    ↑↑→↑↑CF ℭ 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL 𝔟 𝔞 𝔣 𝔤 >CF.cocone E :
    ↑↑C 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL ↦↦C⇘α⇙ ℭ"
    and "𝔤 : 𝔟 ↦⇘ℭ⇙ 𝔞" 
    and "𝔣 : 𝔟 ↦⇘ℭ⇙ 𝔞"
  shows 
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔤" 
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔣"    
proof-
  let ?II = ‹↑↑C 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL› 
    and ?II_II = ‹↑↑→↑↑CF ℭ 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL 𝔟 𝔞 𝔣 𝔤›
    and ?F = ‹set {𝔤PL, 𝔣PL}›
  have 𝔣𝔤_𝔤𝔣: "{𝔣PL, 𝔤PL} = {𝔤PL, 𝔣PL}" by auto
  interpret ε: is_cat_cocone α E ?II ℭ ?II_II ε by (rule assms(1))
  from ε.cat_PL2_𝔣 ε.cat_PL2_𝔤 have 𝔤𝔣: "?F ∈∘ Vset α"
    by (intro Limit_vdoubleton_in_VsetI) auto
  from assms(2,3) have
    "(⋀𝔣'. 𝔣' ∈∘ ?F ⟹ (λf∈∘?F. (f = 𝔤PL ? 𝔤 : 𝔣))⦇𝔣'⦈ : 𝔟 ↦⇘ℭ⇙ 𝔞)"
    by auto
  note cat_cocone_cf_par_eps_NTMap_app = cat_cocone_cf_par_eps_NTMap_app
    [
      OF assms(1)
        [
          unfolded 
            the_cat_parallel_2_def 
            the_cf_parallel_2_def 
            𝔞PL2_def 𝔟PL2_def 
            insert_commute,
          unfolded 𝔣𝔤_𝔤𝔣
        ],
      folded 𝔞PL2_def 𝔟PL2_def,
      OF _ 𝔤𝔣 _ this,
      simplified
    ]
  from
    cat_cocone_cf_par_eps_NTMap_app[of 𝔤PL, simplified]
    cat_cocone_cf_par_eps_NTMap_app[of 𝔣PL, simplified]
    cat_PL2_𝔤𝔣
  show
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔤" 
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔣"
    by fastforce+
qed

lemma (in is_cat_equalizer_2) cat_eq_2_eps_NTMap_app:
  "ε⦇NTMap⦈⦇𝔟PL2⦈ = 𝔤 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
  "ε⦇NTMap⦈⦇𝔟PL2⦈ = 𝔣 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
proof-
  have 𝔤PL: "𝔤PL ∈∘ set {𝔤PL, 𝔣PL}" and 𝔣PL: "𝔣PL ∈∘ set {𝔤PL, 𝔣PL}" by auto
  note cat_eq_eps_NTMap_app = is_cat_equalizer.cat_eq_eps_NTMap_app
    [
      OF cat_equalizer_2_is_cat_equalizer,
      folded 𝔞PL2_def 𝔟PL2_def
    ]
  from cat_eq_eps_NTMap_app[OF 𝔤PL] cat_eq_eps_NTMap_app[OF 𝔣PL] cat_PL2_𝔤𝔣 show 
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = 𝔤 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = 𝔣 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
    by auto
qed

lemma (in is_cat_coequalizer_2) cat_coeq_2_eps_NTMap_app:
  "ε⦇NTMap⦈⦇𝔟PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔤"
  "ε⦇NTMap⦈⦇𝔟PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔣"
proof-
  have 𝔤PL: "𝔤PL ∈∘ set {𝔤PL, 𝔣PL}" and 𝔣PL: "𝔣PL ∈∘ set {𝔤PL, 𝔣PL}" by auto
  note cat_eq_eps_NTMap_app = is_cat_coequalizer.cat_coeq_eps_NTMap_app
    [
      OF cat_coequalizer_2_is_cat_coequalizer,
      folded 𝔞PL2_def 𝔟PL2_def
    ]
  from cat_eq_eps_NTMap_app[OF 𝔤PL] cat_eq_eps_NTMap_app[OF 𝔣PL] cat_PL2_𝔤𝔣 show 
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔤"
    "ε⦇NTMap⦈⦇𝔟PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔣"
    by auto
qed

lemma (in is_cat_equalizer_2) cat_eq_2_Comp_eq: 
  "𝔤 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈ = 𝔣 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
  "𝔣 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈ = 𝔤 ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
  unfolding cat_eq_2_eps_NTMap_app[symmetric] by simp_all

lemma (in is_cat_coequalizer_2) cat_coeq_2_Comp_eq: 
  "ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔤 = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔣"
  "ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔣 = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ 𝔤"
  unfolding cat_coeq_2_eps_NTMap_app[symmetric] by simp_all


subsubsection‹Universal property›

lemma is_cat_equalizer_2I':
  assumes "ε :
    E <CF.cone ↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣 : ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL ↦↦C⇘α⇙ ℭ"
    and "𝔤 : 𝔞 ↦⇘ℭ⇙ 𝔟"
    and "𝔣 : 𝔞 ↦⇘ℭ⇙ 𝔟"
    and "⋀ε' E'. ε' :
      E' <CF.cone ↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣 :
      ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL ↦↦C⇘α⇙ ℭ ⟹
      ∃!f'. f' : E' ↦⇘ℭ⇙ E ∧ ε'⦇NTMap⦈⦇𝔞PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ f'"
  shows "ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ"
proof-
  let ?II = ‹↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL› 
    and ?II_II = ‹↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣›
    and ?F = ‹set {𝔤PL, 𝔣PL}›
  interpret ε: is_cat_cone α E ?II ℭ ?II_II ε by (rule assms(1))
  from ε.cat_PL2_𝔣 ε.cat_PL2_𝔤 have 𝔤𝔣: "?F ∈∘ Vset α"
    by (intro Limit_vdoubleton_in_VsetI) auto
  from assms(2,3) have "(λf∈∘?F. (f = 𝔣PL ? 𝔣 : 𝔤))⦇𝔣'⦈ : 𝔞 ↦⇘ℭ⇙ 𝔟" 
    if "𝔣' ∈∘ ?F" for 𝔣'
    using that by simp
  note is_cat_equalizerI' = is_cat_equalizerI'
      [
        OF 
          assms(1)[
            unfolded 
              the_cat_parallel_2_def the_cf_parallel_2_def 𝔞PL2_def 𝔟PL2_def
            ], 
        folded 𝔞PL2_def 𝔟PL2_def, 
        OF 
          _ 
          𝔤𝔣 
          _ 
          this 
          _ 
          assms(4)[unfolded the_cf_parallel_2_def the_cat_parallel_2_def], 
        of 𝔤PL,
        simplified
      ]
  show ?thesis by (rule cat_equalizer_is_cat_equalizer_2[OF is_cat_equalizerI'])
qed

lemma is_cat_coequalizer_2I':
  assumes "ε :
    ↑↑→↑↑CF ℭ 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL 𝔟 𝔞 𝔣 𝔤 >CF.cocone E :
    ↑↑C 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL ↦↦C⇘α⇙ ℭ"
    and "𝔤 : 𝔟 ↦⇘ℭ⇙ 𝔞"
    and "𝔣 : 𝔟 ↦⇘ℭ⇙ 𝔞"
    and "⋀ε' E'. ε' :
      ↑↑→↑↑CF ℭ 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL 𝔟 𝔞 𝔣 𝔤 >CF.cocone E' :
      ↑↑C 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL ↦↦C⇘α⇙ ℭ ⟹
      ∃!f'. f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL2⦈ = f' ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
  shows "ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ"
proof-
  let ?II = ‹↑↑C 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL› 
    and ?II_II = ‹↑↑→↑↑CF ℭ 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL 𝔟 𝔞 𝔣 𝔤›
    and ?F = ‹set {𝔤PL, 𝔣PL}›
  have 𝔣𝔤_𝔤𝔣: "{𝔣PL, 𝔤PL} = {𝔤PL, 𝔣PL}" by auto
  interpret ε: is_cat_cocone α E ?II ℭ ?II_II ε by (rule assms(1))
  from ε.cat_PL2_𝔣 ε.cat_PL2_𝔤 have 𝔤𝔣: "?F ∈∘ Vset α"
    by (intro Limit_vdoubleton_in_VsetI) auto
  from assms(2,3) have "(λf∈∘set {𝔤PL, 𝔣PL}. (f = 𝔤PL ? 𝔤 : 𝔣))⦇𝔣'⦈ : 𝔟 ↦⇘ℭ⇙ 𝔞"
    if "𝔣' ∈∘ set {𝔤PL, 𝔣PL}" for 𝔣'
    using that by simp
  note is_cat_coequalizerI'
    [
      OF assms(1)[
        unfolded 
          the_cat_parallel_2_def the_cf_parallel_2_def 𝔞PL2_def 𝔟PL2_def 𝔣𝔤_𝔤𝔣
          ],
      folded 𝔞PL2_def 𝔟PL2_def,
      OF 
        _ 
        𝔤𝔣
        _ 
        this
        _
        assms(4)[unfolded the_cf_parallel_2_def the_cat_parallel_2_def 𝔣𝔤_𝔤𝔣],
      of 𝔤PL,
      simplified
    ]
  with cat_PL2_𝔤𝔣 have
    "ε : (𝔞,𝔟,?F,(λf∈∘?F. (f = 𝔣PL ? 𝔣 : 𝔤))) >CF.coeq E : ⇑C ↦↦C⇘α⇙ ℭ"
    by (auto simp: VLambda_vdoubleton)
  from cat_coequalizer_is_cat_coequalizer_2[OF this] show ?thesis by simp
qed

lemma (in is_cat_equalizer_2) cat_eq_2_unique_cone:
  assumes "ε' :
    E' <CF.cone ↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣 : 
    ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL ↦↦C⇘α⇙ ℭ"
  shows "∃!f'. f' : E' ↦⇘ℭ⇙ E ∧ ε'⦇NTMap⦈⦇𝔞PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ f'"
  by 
    (
      rule is_cat_equalizer.cat_eq_unique_cone
        [
          OF cat_equalizer_2_is_cat_equalizer, 
          folded 𝔞PL2_def 𝔟PL2_def,
          OF assms[unfolded the_cf_parallel_2_def the_cat_parallel_2_def]
        ]
    )

lemma (in is_cat_equalizer_2) cat_eq_2_unique:
  assumes "ε' : E' <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ"
  shows
    "∃!f'. f' : E' ↦⇘ℭ⇙ E ∧ ε' = ε ∙NTCF ntcf_const (↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL) ℭ f'"
proof-  
  interpret ε': is_cat_equalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E' ε' by (rule assms)
  show ?thesis
    by 
      (
        rule is_cat_equalizer.cat_eq_unique
          [
            OF cat_equalizer_2_is_cat_equalizer,
            folded 𝔞PL2_def 𝔟PL2_def,
            OF ε'.cat_equalizer_2_is_cat_equalizer,
            folded the_cat_parallel_2_def
          ]
      )
qed

lemma (in is_cat_equalizer_2) cat_eq_2_unique':
  assumes "ε' : E' <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ"
  shows "∃!f'. f' : E' ↦⇘ℭ⇙ E ∧ ε'⦇NTMap⦈⦇𝔞PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ f'"
proof-
  interpret ε': is_cat_equalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E' ε' by (rule assms)
  show ?thesis
    by 
      (
        rule is_cat_equalizer.cat_eq_unique'
          [
            OF cat_equalizer_2_is_cat_equalizer,
            folded 𝔞PL2_def 𝔟PL2_def,
            OF ε'.cat_equalizer_2_is_cat_equalizer,
            folded the_cat_parallel_2_def
          ]
      )
qed

lemma (in is_cat_coequalizer_2) cat_coeq_2_unique_cocone:
  assumes "ε' :
    ↑↑→↑↑CF ℭ 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL 𝔟 𝔞 𝔣 𝔤 >CF.cocone E' :
    ↑↑C 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL ↦↦C⇘α⇙ ℭ"
  shows "∃!f'. f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL2⦈ = f' ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
  by 
    (
      rule is_cat_coequalizer.cat_coeq_unique_cocone
        [
          OF cat_coequalizer_2_is_cat_coequalizer,
          folded 𝔞PL2_def 𝔟PL2_def insert_commute,
          OF assms[
            unfolded 
              the_cf_parallel_2_def the_cat_parallel_2_def cat_eq_F'_helper
            ]
        ]
    )

lemma (in is_cat_coequalizer_2) cat_coeq_2_unique:
  assumes "ε' : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E' : ↑↑C ↦↦C⇘α⇙ ℭ"
  shows "∃!f'.
    f' : E ↦⇘ℭ⇙ E' ∧
    ε' = ntcf_const (↑↑C 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL) ℭ f' ∙NTCF ε"
proof-
  interpret ε': is_cat_coequalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E' ε' by (rule assms)
  show ?thesis  
    by 
      (
        rule is_cat_coequalizer.cat_coeq_unique
          [
            OF cat_coequalizer_2_is_cat_coequalizer,
            folded 𝔞PL2_def 𝔟PL2_def,
            OF ε'.cat_coequalizer_2_is_cat_coequalizer,
            folded the_cat_parallel_2_def the_cat_parallel_2_commute
          ]
      )
qed

lemma (in is_cat_coequalizer_2) cat_coeq_2_unique':
  assumes "ε' : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E' : ↑↑C ↦↦C⇘α⇙ ℭ"
  shows "∃!f'. f' : E ↦⇘ℭ⇙ E' ∧ ε'⦇NTMap⦈⦇𝔞PL2⦈ = f' ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
proof-
  interpret ε': is_cat_coequalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E' ε' by (rule assms)
  show ?thesis
    by 
      (
        rule is_cat_coequalizer.cat_coeq_unique'
          [
            OF cat_coequalizer_2_is_cat_coequalizer,
            folded 𝔞PL2_def 𝔟PL2_def,
            OF ε'.cat_coequalizer_2_is_cat_coequalizer,
            folded the_cat_parallel_2_def
          ]
      )
qed

lemma cat_equalizer_2_ex_is_iso_arr:
  assumes "ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ" 
    and "ε' : E' <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ"
  obtains f where "f : E' ↦iso⇘ℭ⇙ E"
    and "ε' = ε ∙NTCF ntcf_const (↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL) ℭ f"
proof-
  interpret ε: is_cat_equalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E ε by (rule assms(1))
  interpret ε': is_cat_equalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E' ε' by (rule assms(2))
  show ?thesis
    using that 
    by 
      (
        rule cat_equalizer_ex_is_iso_arr
          [
            OF 
              ε.cat_equalizer_2_is_cat_equalizer 
              ε'.cat_equalizer_2_is_cat_equalizer,
            folded 𝔞PL2_def 𝔟PL2_def the_cat_parallel_2_def
          ]
      )  
qed

lemma cat_equalizer_2_ex_is_iso_arr':
  assumes "ε : E <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ" 
    and "ε' : E' <CF.eq (𝔞,𝔟,𝔤,𝔣) : ↑↑C ↦↦C⇘α⇙ ℭ"
  obtains f where "f : E' ↦iso⇘ℭ⇙ E"
    and "ε'⦇NTMap⦈⦇𝔞PL2⦈ = ε⦇NTMap⦈⦇𝔞PL2⦈ ∘A⇘ℭ⇙ f"
    and "ε'⦇NTMap⦈⦇𝔟PL2⦈ = ε⦇NTMap⦈⦇𝔟PL2⦈ ∘A⇘ℭ⇙ f"
proof-
  interpret ε: is_cat_equalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E ε by (rule assms(1))
  interpret ε': is_cat_equalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E' ε' by (rule assms(2))
  show ?thesis
    using that 
    by 
      (
        rule cat_equalizer_ex_is_iso_arr'
          [
            OF 
              ε.cat_equalizer_2_is_cat_equalizer 
              ε'.cat_equalizer_2_is_cat_equalizer,
            folded 𝔞PL2_def 𝔟PL2_def the_cat_parallel_2_def
          ]
      )
qed

lemma cat_coequalizer_2_ex_is_iso_arr:
  assumes "ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ"
    and "ε' : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E' : ↑↑C ↦↦C⇘α⇙ ℭ"
  obtains f where "f : E ↦iso⇘ℭ⇙ E'" 
    and "ε' = ntcf_const (↑↑C 𝔟PL2 𝔞PL2 𝔣PL 𝔤PL) ℭ f ∙NTCF ε"
proof-
  interpret ε: is_cat_coequalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E ε by (rule assms(1))
  interpret ε': is_cat_coequalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E' ε' by (rule assms(2))
  show ?thesis
    using that 
    by 
      (
        rule cat_coequalizer_ex_is_iso_arr
          [
            OF 
              ε.cat_coequalizer_2_is_cat_coequalizer 
              ε'.cat_coequalizer_2_is_cat_coequalizer,
            folded 
              𝔞PL2_def 𝔟PL2_def the_cat_parallel_2_def the_cat_parallel_2_commute
          ]
      )
qed

lemma cat_coequalizer_2_ex_is_iso_arr':
  assumes "ε : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E : ↑↑C ↦↦C⇘α⇙ ℭ"
    and "ε' : (𝔞,𝔟,𝔤,𝔣) >CF.coeq E' : ↑↑C ↦↦C⇘α⇙ ℭ"
  obtains f where "f : E ↦iso⇘ℭ⇙ E'" 
    and "ε'⦇NTMap⦈⦇𝔞PL2⦈ = f ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔞PL2⦈"
    and "ε'⦇NTMap⦈⦇𝔟PL2⦈ = f ∘A⇘ℭ⇙ ε⦇NTMap⦈⦇𝔟PL2⦈"
proof-
  interpret ε: is_cat_coequalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E ε by (rule assms(1))
  interpret ε': is_cat_coequalizer_2 α 𝔞 𝔟 𝔤 𝔣 ℭ E' ε' by (rule assms(2))
  show ?thesis
    using that 
    by 
      (
        rule cat_coequalizer_ex_is_iso_arr'
          [
            OF
              ε.cat_coequalizer_2_is_cat_coequalizer
              ε'.cat_coequalizer_2_is_cat_coequalizer,
            folded 
              𝔞PL2_def 𝔟PL2_def the_cat_parallel_2_def the_cat_parallel_2_commute
          ]
      )
qed


subsubsection‹Further properties›

lemma (in is_cat_equalizer_2) cat_eq_2_is_monic_arr: 
  "ε⦇NTMap⦈⦇𝔞PL2⦈ : E ↦mon⇘ℭ⇙ 𝔞"
  by
    (
      rule is_cat_equalizer.cat_eq_is_monic_arr[
        OF cat_equalizer_2_is_cat_equalizer, folded 𝔞PL2_def
        ]
    )

lemma (in is_cat_coequalizer_2) cat_coeq_2_is_epic_arr:
  "ε⦇NTMap⦈⦇𝔞PL2⦈ : 𝔞 ↦epi⇘ℭ⇙ E"
  by
    (
      rule is_cat_coequalizer.cat_coeq_is_epic_arr[
        OF cat_coequalizer_2_is_cat_coequalizer, folded 𝔞PL2_def
        ]
    )



subsection‹Equalizer cone›


subsubsection‹Definition and elementary properties›

definition ntcf_equalizer_base :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e =
    [
      (λx∈∘↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL⦇Obj⦈. e x),
      cf_const (↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL) ℭ E,
      ↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣,
      ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL,
      ℭ
    ]∘"


text‹Components.›

lemma ntcf_equalizer_base_components:
  shows "ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e⦇NTMap⦈ =
    (λx∈∘↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL⦇Obj⦈. e x)"
    and [cat_lim_cs_simps]: "ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e⦇NTDom⦈ =
      cf_const (↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL) ℭ E"
    and [cat_lim_cs_simps]: "ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e⦇NTCod⦈ =
      ↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣"
    and [cat_lim_cs_simps]: 
      "ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e⦇NTDGDom⦈ = ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL"
    and [cat_lim_cs_simps]: 
      "ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e⦇NTDGCod⦈ = ℭ"
  unfolding ntcf_equalizer_base_def nt_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Natural transformation map›

mk_VLambda ntcf_equalizer_base_components(1)
  |vsv ntcf_equalizer_base_NTMap_vsv[cat_lim_cs_intros]|
  |vdomain ntcf_equalizer_base_NTMap_vdomain[cat_lim_cs_simps]|
  |app ntcf_equalizer_base_NTMap_app[cat_lim_cs_simps]|


subsubsection‹Equalizer cone is a cone›

lemma (in category) cat_ntcf_equalizer_base_is_cat_cone:
  assumes "e 𝔞PL2 : E ↦⇘ℭ⇙ 𝔞"
    and "e 𝔟PL2 : E ↦⇘ℭ⇙ 𝔟"
    and "e 𝔟PL2 = 𝔤 ∘A⇘ℭ⇙ e 𝔞PL2"
    and "e 𝔟PL2 = 𝔣 ∘A⇘ℭ⇙ e 𝔞PL2"
    and "𝔤 : 𝔞 ↦⇘ℭ⇙ 𝔟"
    and "𝔣 : 𝔞 ↦⇘ℭ⇙ 𝔟"
  shows "ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e :
    E <CF.cone ↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣 :
    ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL ↦↦C⇘α⇙ ℭ"
proof-
  interpret par: cf_parallel_2 α 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣 ℭ 
    by (intro cf_parallel_2I cat_parallel_2I assms(5,6))
      (simp_all add: cat_parallel_cs_intros cat_cs_intros)
  show ?thesis
  proof(intro is_cat_coneI is_tm_ntcfI' is_ntcfI')
    show "vfsequence (ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e)"
      unfolding ntcf_equalizer_base_def by auto
    show "vcard (ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e) = 5ℕ"
      unfolding ntcf_equalizer_base_def by (simp add: nat_omega_simps)
    from assms(2) show 
      "cf_const (↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL) ℭ E : ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL ↦↦C⇘α⇙ ℭ"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps 
            cs_intro: cat_small_cs_intros cat_parallel_cs_intros cat_cs_intros
        )
    from assms show 
      "↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣 : ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL ↦↦C⇘α⇙ ℭ"
      by (cs_concl cs_intro: cat_parallel_cs_intros cat_small_cs_intros)
    show 
      "ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e⦇NTMap⦈⦇i⦈ :
        cf_const (↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL) ℭ E⦇ObjMap⦈⦇i⦈ ↦⇘ℭ⇙
        ↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣⦇ObjMap⦈⦇i⦈"
      if "i ∈∘ ↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL⦇Obj⦈" for i 
    proof-
      from that assms(1,2,5,6) show ?thesis
        by (elim the_cat_parallel_2_ObjE; simp only:)
          ( 
            cs_concl 
              cs_simp: cat_lim_cs_simps cat_cs_simps cat_parallel_cs_simps 
              cs_intro: cat_cs_intros cat_parallel_cs_intros
          )
    qed
    show 
      "ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e⦇NTMap⦈⦇b'⦈ ∘A⇘ℭ⇙
        cf_const (↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL) ℭ E⦇ArrMap⦈⦇f'⦈ =
          ↑↑→↑↑CF ℭ 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL 𝔞 𝔟 𝔤 𝔣⦇ArrMap⦈⦇f'⦈ ∘A⇘ℭ⇙
          ntcf_equalizer_base ℭ 𝔞 𝔟 𝔤 𝔣 E e⦇NTMap⦈⦇a'⦈"
      if "f' : a' ↦⇘↑↑C 𝔞PL2 𝔟PL2 𝔤PL 𝔣PL⇙ b'" for a' b' f'
      using that assms(1,2,5,6)
      by (elim par.the_cat_parallel_2_is_arrE; simp only:)
        (
          cs_concl 
            cs_simp: 
              cat_cs_simps 
              cat_lim_cs_simps 
              cat_parallel_cs_simps 
              assms(3,4)[symmetric]
            cs_intro: cat_parallel_cs_intros
        )+
  qed 
    (
      use assms(2) in 
        ‹
          cs_concl 
            cs_intro: cat_lim_cs_intros cat_cs_intros 
            cs_simp: cat_lim_cs_simps
        ›
    )+
qed

text‹\newpage›

end