Theory CZH_UCAT_Limit_Pullback

(* Copyright 2021 (C) Mihails Milehins *)

section‹Pullbacks and pushouts as limits and colimits›
theory CZH_UCAT_Limit_Pullback
  imports 
    CZH_UCAT_Limit
    CZH_Elementary_Categories.CZH_ECAT_SS
begin



subsection‹Pullback and pushout›


subsubsection‹Definition and elementary properties›


text‹
The definitions and the elementary properties of the pullbacks and the 
pushouts can be found, for example, in Chapter III-3 and Chapter III-4 in 
\<^cite>‹"mac_lane_categories_2010"›. 
›

locale is_cat_pullback =
  is_cat_limit α ‹→∙←⇩C› ℭ ‹⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙› X x + 
  cf_scospan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ
  for α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X x 

syntax "_is_cat_pullback" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ <⇩C⇩F⇩.⇩p⇩b _→_→_←_←_ ↦↦⇩Cı _)› [51, 51, 51, 51, 51, 51, 51, 51] 51)
translations "x : X <⇩C⇩F⇩.⇩p⇩b 𝔞→𝔤→𝔬←𝔣←𝔟 ↦↦⇩C⇘α⇙ ℭ" ⇌ 
  "CONST is_cat_pullback α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X x"
                        
locale is_cat_pushout =
  is_cat_colimit α ‹←∙→⇩C› ℭ ‹⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙› X x +
  cf_sspan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ
  for α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X x

syntax "_is_cat_pushout" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _←_←_→_→_ >⇩C⇩F⇩.⇩p⇩o _ ↦↦⇩Cı _)› [51, 51, 51, 51, 51, 51, 51, 51] 51)
translations "x : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X ↦↦⇩C⇘α⇙ ℭ" ⇌ 
  "CONST is_cat_pushout α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X x"


text‹Rules.›

lemma (in is_cat_pullback) is_cat_pullback_axioms'[cat_lim_cs_intros]:
  assumes "α' = α"
    and "𝔞' = 𝔞"
    and "𝔤' = 𝔤"
    and "𝔬' = 𝔬"
    and "𝔣' = 𝔣"
    and "𝔟' = 𝔟"
    and "ℭ' = ℭ"
    and "X' = X"
  shows "x : X' <⇩C⇩F⇩.⇩p⇩b 𝔞'→𝔤'→𝔬'←𝔣'←𝔟' ↦↦⇩C⇘α'⇙ ℭ'"
  unfolding assms by (rule is_cat_pullback_axioms)

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

lemmas [cat_lim_cs_intros] = is_cat_pullbackD

lemma (in is_cat_pushout) is_cat_pushout_axioms'[cat_lim_cs_intros]:
  assumes "α' = α"
    and "𝔞' = 𝔞"
    and "𝔤' = 𝔤"
    and "𝔬' = 𝔬"
    and "𝔣' = 𝔣"
    and "𝔟' = 𝔟"
    and "ℭ' = ℭ"
    and "X' = X"
  shows "x : 𝔞'←𝔤'←𝔬'→𝔣'→𝔟' >⇩C⇩F⇩.⇩p⇩o X' ↦↦⇩C⇘α'⇙ ℭ'"
  unfolding assms by (rule is_cat_pushout_axioms)

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

lemmas [cat_lim_cs_intros] = is_cat_pushoutD


text‹Duality.›

lemma (in is_cat_pullback) is_cat_pushout_op:
  "op_ntcf x : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X ↦↦⇩C⇘α⇙ op_cat ℭ"
  by (intro is_cat_pushoutI) 
    (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)+

lemma (in is_cat_pullback) is_cat_pushout_op'[cat_op_intros]:
  assumes "ℭ' = op_cat ℭ"
  shows "op_ntcf x : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X ↦↦⇩C⇘α⇙ ℭ'"
  unfolding assms by (rule is_cat_pushout_op)

lemmas [cat_op_intros] = is_cat_pullback.is_cat_pushout_op'

lemma (in is_cat_pushout) is_cat_pullback_op:
  "op_ntcf x : X <⇩C⇩F⇩.⇩p⇩b 𝔞→𝔤→𝔬←𝔣←𝔟 ↦↦⇩C⇘α⇙ op_cat ℭ"
  by (intro is_cat_pullbackI) 
    (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)+

lemma (in is_cat_pushout) is_cat_pullback_op'[cat_op_intros]:
  assumes "ℭ' = op_cat ℭ"
  shows "op_ntcf x : X <⇩C⇩F⇩.⇩p⇩b 𝔞→𝔤→𝔬←𝔣←𝔟 ↦↦⇩C⇘α⇙ ℭ'"
  unfolding assms by (rule is_cat_pullback_op)

lemmas [cat_op_intros] = is_cat_pushout.is_cat_pullback_op'


text‹Elementary properties.›

lemma cat_cone_cospan:
  assumes "x : X <⇩C⇩F⇩.⇩c⇩o⇩n⇩e ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ : →∙←⇩C ↦↦⇩C⇘α⇙ ℭ"
    and "cf_scospan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ"
  shows "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = 𝔤 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈"
    and "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = 𝔣 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈"
    and "𝔤 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = 𝔣 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈"
proof-
  interpret x: is_cat_cone α X ‹→∙←⇩C› ℭ ‹⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙› x 
    by (rule assms(1))
  interpret cospan: cf_scospan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ by (rule assms(2))
  have 𝔤⇩S⇩S: "𝔤⇩S⇩S : 𝔞⇩S⇩S ↦⇘→∙←⇩C⇙ 𝔬⇩S⇩S" and 𝔣⇩S⇩S: "𝔣⇩S⇩S : 𝔟⇩S⇩S ↦⇘→∙←⇩C⇙ 𝔬⇩S⇩S" 
    by (cs_concl cs_intro: cat_ss_cs_intros)+
  note x.cat_cone_Comp_commute[cat_cs_simps del]
  from x.ntcf_Comp_commute[OF 𝔤⇩S⇩S] 𝔤⇩S⇩S 𝔣⇩S⇩S show
    "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = 𝔤 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈"
    by 
      (
        cs_prems cs_shallow
          cs_simp: cat_ss_cs_simps cat_cs_simps cs_intro: cat_cs_intros
      )
  moreover from x.ntcf_Comp_commute[OF 𝔣⇩S⇩S] 𝔤⇩S⇩S 𝔣⇩S⇩S show 
    "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = 𝔣 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈"
    by 
      (
        cs_prems cs_shallow 
          cs_simp: cat_ss_cs_simps cat_cs_simps cs_intro: cat_cs_intros
      )
  ultimately show "𝔤 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = 𝔣 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈" by simp
qed

lemma (in is_cat_pullback) cat_pb_cone_cospan:
  shows "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = 𝔤 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈"
    and "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = 𝔣 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈"
    and "𝔤 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = 𝔣 ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈"
  by (all‹rule cat_cone_cospan[OF is_cat_cone_axioms cf_scospan_axioms]›)

lemma cat_cocone_span:
  assumes "x : ⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙ >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e X : ←∙→⇩C ↦↦⇩C⇘α⇙ ℭ"
    and "cf_sspan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ"
  shows "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔤"
    and "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔣"
    and "x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔤 = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔣"
proof-
  interpret x: is_cat_cocone α X ‹←∙→⇩C› ℭ ‹⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙› x
    by (rule assms(1))
  interpret span: cf_sspan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ by (rule assms(2))
  note op = 
    cat_cone_cospan
      [
        OF 
          x.is_cat_cone_op[unfolded cat_op_simps] 
          span.cf_scospan_op, 
          unfolded cat_op_simps
      ]
  from op(1) show "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔤"
    by 
      (
        cs_prems  
          cs_simp: cat_ss_cs_simps cat_op_simps 
          cs_intro: cat_cs_intros cat_ss_cs_intros
      )
  moreover from op(2) show "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔣"
    by 
      (
        cs_prems 
          cs_simp: cat_ss_cs_simps cat_op_simps 
          cs_intro: cat_cs_intros cat_ss_cs_intros
      )
  ultimately show "x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔤 = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔣" by auto
qed

lemma (in is_cat_pushout) cat_po_cocone_span:
  shows "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔤"
    and "x⦇NTMap⦈⦇𝔬⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔣"
    and "x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔤 = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ 𝔣"
  by (all‹rule cat_cocone_span[OF is_cat_cocone_axioms cf_sspan_axioms]›)


subsubsection‹Universal property›

lemma is_cat_pullbackI':
  assumes "x : X <⇩C⇩F⇩.⇩c⇩o⇩n⇩e ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ : →∙←⇩C ↦↦⇩C⇘α⇙ ℭ"
    and "cf_scospan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ"
    and "⋀x' X'. x' : X' <⇩C⇩F⇩.⇩c⇩o⇩n⇩e ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ : →∙←⇩C ↦↦⇩C⇘α⇙ ℭ ⟹
      ∃!f'.
        f' : X' ↦⇘ℭ⇙ X ∧
        x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f' ∧
        x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f'"
  shows "x : X <⇩C⇩F⇩.⇩p⇩b 𝔞→𝔤→𝔬←𝔣←𝔟 ↦↦⇩C⇘α⇙ ℭ"
proof(intro is_cat_pullbackI is_cat_limitI)

  show "x : X <⇩C⇩F⇩.⇩c⇩o⇩n⇩e ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ : →∙←⇩C ↦↦⇩C⇘α⇙ ℭ" 
    by (rule assms(1))
  interpret x: is_cat_cone α X ‹→∙←⇩C› ℭ ‹⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙› x 
    by (rule assms(1))
  show "cf_scospan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ" by (rule assms(2))
  interpret cospan: cf_scospan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ by (rule assms(2))

  fix u' r' assume prems:
    "u' : r' <⇩C⇩F⇩.⇩c⇩o⇩n⇩e ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ : →∙←⇩C ↦↦⇩C⇘α⇙ ℭ"

  interpret u': is_cat_cone α r' ‹→∙←⇩C› ℭ ‹⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙› u' 
    by (rule prems)

  from assms(3)[OF prems] obtain f' 
    where f': "f' : r' ↦⇘ℭ⇙ X"
      and u'_𝔞⇩S⇩S: "u'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f'"
      and u'_𝔟⇩S⇩S: "u'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f'"
      and unique_f': "⋀f''.
        ⟦
          f'' : r' ↦⇘ℭ⇙ X;
          u'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f'';
          u'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f''
        ⟧ ⟹ f'' = f'"
    by metis

  show "∃!f'. f' : r' ↦⇘ℭ⇙ X ∧ u' = x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f'"
  proof(intro ex1I conjI; (elim conjE)?)

    show "u' = x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f'"
    proof(rule ntcf_eqI)
      show "u' : cf_const →∙←⇩C ℭ r' ↦⇩C⇩F ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ : →∙←⇩C ↦↦⇩C⇘α⇙ ℭ"
        by (rule u'.is_ntcf_axioms)
      from f' show 
        "x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f' :
          cf_const →∙←⇩C ℭ r' ↦⇩C⇩F ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ :
          →∙←⇩C ↦↦⇩C⇘α⇙ ℭ"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      from f' have dom_rhs: 
        "𝒟⇩∘ ((x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f')⦇NTMap⦈) = →∙←⇩C⦇Obj⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      show "u'⦇NTMap⦈ = (x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f')⦇NTMap⦈"
      proof(rule vsv_eqI, unfold cat_cs_simps dom_rhs)
        fix a assume prems': "a ∈⇩∘ →∙←⇩C⦇Obj⦈"
        from this f' x.is_ntcf_axioms show
          "u'⦇NTMap⦈⦇a⦈ = (x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f')⦇NTMap⦈⦇a⦈"
          by (elim the_cat_scospan_ObjE; simp only:)
            (
              cs_concl 
                cs_simp:
                  cat_cs_simps cat_ss_cs_simps 
                  u'_𝔟⇩S⇩S u'_𝔞⇩S⇩S 
                  cat_cone_cospan(1)[OF assms(1,2)] 
                  cat_cone_cospan(1)[OF prems assms(2)] 
                cs_intro: cat_cs_intros cat_ss_cs_intros
            )+
      qed (cs_concl cs_intro: cat_cs_intros | auto)+
    qed simp_all

    fix f'' assume prems: 
      "f'' : r' ↦⇘ℭ⇙ X" "u' = x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f''"
    have 𝔞⇩S⇩S: "𝔞⇩S⇩S ∈⇩∘ →∙←⇩C⦇Obj⦈" and 𝔟⇩S⇩S: "𝔟⇩S⇩S ∈⇩∘ →∙←⇩C⦇Obj⦈" 
      by (cs_concl cs_intro: cat_ss_cs_intros)+
    have "u'⦇NTMap⦈⦇a⦈ = x⦇NTMap⦈⦇a⦈ ∘⇩A⇘ℭ⇙ f''" if "a ∈⇩∘ →∙←⇩C⦇Obj⦈" for a
    proof-
      from prems(2) have 
        "u'⦇NTMap⦈⦇a⦈ = (x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f'')⦇NTMap⦈⦇a⦈"
        by simp
      from this that prems(1) show "u'⦇NTMap⦈⦇a⦈ = x⦇NTMap⦈⦇a⦈ ∘⇩A⇘ℭ⇙ f''"
        by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed
    from unique_f'[OF prems(1) this[OF 𝔞⇩S⇩S] this[OF 𝔟⇩S⇩S]] show "f'' = f'".

  qed (intro f')

qed

lemma is_cat_pushoutI':
  assumes "x : ⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙ >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e X : ←∙→⇩C ↦↦⇩C⇘α⇙ ℭ"
    and "cf_sspan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ"
    and "⋀x' X'. x' : ⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙ >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e X' : ←∙→⇩C ↦↦⇩C⇘α⇙ ℭ ⟹
      ∃!f'.
        f' : X ↦⇘ℭ⇙ X' ∧
        x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = f' ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∧
        x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = f' ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈"
  shows "x : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X ↦↦⇩C⇘α⇙ ℭ"
proof-
  interpret x: is_cat_cocone α X ‹←∙→⇩C› ℭ ‹⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙› x 
    by (rule assms(1))
  interpret span: cf_sspan α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ by (rule assms(2))
  have assms_3': 
    "∃!f'.
      f' : X ↦⇘ℭ⇙ X' ∧
      x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘op_cat ℭ⇙ f' ∧
      x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘op_cat ℭ⇙ f'"
    if "x' : X' <⇩C⇩F⇩.⇩c⇩o⇩n⇩e ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘op_cat ℭ⇙ : →∙←⇩C ↦↦⇩C⇘α⇙ op_cat ℭ"
    for x' X'
  proof-
    from that(1) have [cat_op_simps]:
      "f' : X ↦⇘ℭ⇙ X' ∧ 
      x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘op_cat ℭ⇙ f' ∧
      x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘op_cat ℭ⇙ f' ⟷
        f' : X ↦⇘ℭ⇙ X' ∧
        x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = f' ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∧
        x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = f' ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈" 
      for f'
      by (intro iffI conjI; (elim conjE)?)
        (
          cs_concl 
            cs_simp: category.op_cat_Comp[symmetric] cat_op_simps cat_cs_simps 
            cs_intro: cat_cs_intros cat_ss_cs_intros
        )+
    interpret x': 
      is_cat_cone α X' ‹→∙←⇩C› ‹op_cat ℭ› ‹⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘op_cat ℭ⇙› x'
      by (rule that)
    show ?thesis
      unfolding cat_op_simps
      by 
        (
          rule assms(3)[
            OF x'.is_cat_cocone_op[unfolded cat_op_simps], 
            unfolded cat_op_simps
            ]
        )
  qed
  interpret op_x: is_cat_pullback α 𝔞 𝔤 𝔬 𝔣 𝔟 ‹op_cat ℭ› X ‹op_ntcf x› 
    using 
      is_cat_pullbackI'
        [
          OF x.is_cat_cone_op[unfolded cat_op_simps] 
          span.cf_scospan_op, 
          unfolded cat_op_simps, 
          OF assms_3'
        ]
    by simp
  show "x : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X ↦↦⇩C⇘α⇙ ℭ"
    by (rule op_x.is_cat_pushout_op[unfolded cat_op_simps])
qed
                   
lemma (in is_cat_pullback) cat_pb_unique_cone:
  assumes "x' : X' <⇩C⇩F⇩.⇩c⇩o⇩n⇩e ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ : →∙←⇩C ↦↦⇩C⇘α⇙ ℭ"
  shows "∃!f'.
    f' : X' ↦⇘ℭ⇙ X ∧
    x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f' ∧
    x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f'"
proof-
  interpret x': is_cat_cone α X' ‹→∙←⇩C› ℭ ‹⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙› x' 
    by (rule assms)
  from cat_lim_ua_fo[OF assms] obtain f'
    where f': "f' : X' ↦⇘ℭ⇙ X" 
      and x'_def: "x' = x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f'"
      and unique_f': "⋀f''.
        ⟦ f'' : X' ↦⇘ℭ⇙ X; x' = x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f'' ⟧ ⟹
        f'' = f'"
    by auto
  have 𝔞⇩S⇩S: "𝔞⇩S⇩S ∈⇩∘ →∙←⇩C⦇Obj⦈" and 𝔟⇩S⇩S: "𝔟⇩S⇩S ∈⇩∘ →∙←⇩C⦇Obj⦈"
    by (cs_concl cs_intro: cat_ss_cs_intros)+
  show ?thesis
  proof(intro ex1I conjI; (elim conjE)?)
    show "f' : X' ↦⇘ℭ⇙ X" by (rule f')
    have "x'⦇NTMap⦈⦇a⦈ = x⦇NTMap⦈⦇a⦈ ∘⇩A⇘ℭ⇙ f'" if "a ∈⇩∘ →∙←⇩C⦇Obj⦈" for a
    proof-
      from x'_def have 
        "x'⦇NTMap⦈⦇a⦈ = (x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f')⦇NTMap⦈⦇a⦈"
        by simp
      from this that f' show "x'⦇NTMap⦈⦇a⦈ = x⦇NTMap⦈⦇a⦈ ∘⇩A⇘ℭ⇙ f'"
        by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed
    from this[OF 𝔞⇩S⇩S] this[OF 𝔟⇩S⇩S] show 
      "x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f'"
      "x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f'"
      by auto
    fix f'' assume prems': 
      "f'' : X' ↦⇘ℭ⇙ X"
      "x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f''"
      "x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f''"
    have "x' = x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f''"
    proof(rule ntcf_eqI)
      show "x' : cf_const →∙←⇩C ℭ X' ↦⇩C⇩F ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ : →∙←⇩C ↦↦⇩C⇘α⇙ ℭ"
        by (rule x'.is_ntcf_axioms)
      from prems'(1) show
        "x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f'' :
          cf_const →∙←⇩C ℭ X' ↦⇩C⇩F ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ :
          →∙←⇩C ↦↦⇩C⇘α⇙ ℭ"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      have dom_lhs: "𝒟⇩∘ (x'⦇NTMap⦈) = →∙←⇩C⦇Obj⦈" 
        by (cs_concl cs_shallow cs_simp: cat_cs_simps)
      from prems'(1) have dom_rhs:
        "𝒟⇩∘ ((x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f'')⦇NTMap⦈) = →∙←⇩C⦇Obj⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      show "x'⦇NTMap⦈ = (x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f'')⦇NTMap⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix a assume prems'': "a ∈⇩∘ →∙←⇩C⦇Obj⦈"
        from this prems'(1) show 
          "x'⦇NTMap⦈⦇a⦈ = (x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f'')⦇NTMap⦈⦇a⦈"
          by (elim the_cat_scospan_ObjE; simp only:)
            (
              cs_concl 
                cs_simp: 
                  prems'(2,3)
                  cat_cone_cospan(1,2)[OF assms cf_scospan_axioms] 
                  cat_pb_cone_cospan 
                  cat_ss_cs_simps cat_cs_simps 
                cs_intro: cat_ss_cs_intros cat_cs_intros
            )+
      qed (auto simp: cat_cs_intros)
    qed simp_all
    from unique_f'[OF prems'(1) this] show "f'' = f'".
  qed
qed

lemma (in is_cat_pullback) cat_pb_unique:
  assumes "x' : X' <⇩C⇩F⇩.⇩p⇩b 𝔞→𝔤→𝔬←𝔣←𝔟 ↦↦⇩C⇘α⇙ ℭ"
  shows "∃!f'. f' : X' ↦⇘ℭ⇙ X ∧ x' = x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C ℭ f'"
  by (rule cat_lim_unique[OF is_cat_pullbackD(1)[OF assms]])

lemma (in is_cat_pullback) cat_pb_unique':
  assumes "x' : X' <⇩C⇩F⇩.⇩p⇩b 𝔞→𝔤→𝔬←𝔣←𝔟 ↦↦⇩C⇘α⇙ ℭ"
  shows "∃!f'.
    f' : X' ↦⇘ℭ⇙ X ∧
    x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f' ∧
    x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f'"
proof-
  interpret x': is_cat_pullback α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X' x' by (rule assms(1))
  show ?thesis by (rule cat_pb_unique_cone[OF x'.is_cat_cone_axioms])
qed

lemma (in is_cat_pushout) cat_po_unique_cocone:
  assumes "x' : ⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙ >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e X' : ←∙→⇩C ↦↦⇩C⇘α⇙ ℭ"
  shows "∃!f'.
    f' : X ↦⇘ℭ⇙ X' ∧
    x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = f' ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∧
    x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = f' ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈"
proof-
  interpret x': is_cat_cocone α X' ‹←∙→⇩C› ℭ ‹⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙› x'
    by (rule assms(1))
  have [cat_op_simps]:
    "f' : X ↦⇘ℭ⇙ X' ∧
    x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘op_cat ℭ⇙ f' ∧
    x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘op_cat ℭ⇙ f' ⟷
      f' : X ↦⇘ℭ⇙ X' ∧
      x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = f' ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∧
      x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = f' ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈" 
    for f'
    by (intro iffI conjI; (elim conjE)?)
      (
        cs_concl 
          cs_simp: category.op_cat_Comp[symmetric] cat_op_simps cat_cs_simps  
          cs_intro: cat_cs_intros cat_ss_cs_intros
      )+
  show ?thesis
    by 
      (
        rule is_cat_pullback.cat_pb_unique_cone[
          OF is_cat_pullback_op x'.is_cat_cone_op[unfolded cat_op_simps], 
          unfolded cat_op_simps
          ]
     )
qed

lemma (in is_cat_pushout) cat_po_unique:
  assumes "x' : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X' ↦↦⇩C⇘α⇙ ℭ"
  shows "∃!f'. f' : X ↦⇘ℭ⇙ X' ∧ x' = ntcf_const ←∙→⇩C ℭ f' ∙⇩N⇩T⇩C⇩F x"
  by (rule cat_colim_unique[OF is_cat_pushoutD(1)[OF assms]])

lemma (in is_cat_pushout) cat_po_unique':
  assumes "x' : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X' ↦↦⇩C⇘α⇙ ℭ"
  shows "∃!f'.
    f' : X ↦⇘ℭ⇙ X' ∧
    x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = f' ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∧
    x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = f' ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈"
proof-
  interpret x': is_cat_pushout α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X' x' by (rule assms(1))
  show ?thesis by (rule cat_po_unique_cocone[OF x'.is_cat_cocone_axioms])
qed

lemma cat_pullback_ex_is_iso_arr:
  assumes "x : X <⇩C⇩F⇩.⇩p⇩b 𝔞→𝔤→𝔬←𝔣←𝔟 ↦↦⇩C⇘α⇙ ℭ"
    and "x' : X' <⇩C⇩F⇩.⇩p⇩b 𝔞→𝔤→𝔬←𝔣←𝔟 ↦↦⇩C⇘α⇙ ℭ"
  obtains f where "f : X' ↦⇩i⇩s⇩o⇘ℭ⇙ X" 
    and "x' = x ∙⇩N⇩T⇩C⇩F ntcf_const →∙←⇩C  ℭ f"
proof-
  interpret x: is_cat_pullback α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X x by (rule assms(1))
  interpret x': is_cat_pullback α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X' x' by (rule assms(2))
  from that show ?thesis
    by 
      (
        elim cat_lim_ex_is_iso_arr[
          OF x.is_cat_limit_axioms x'.is_cat_limit_axioms
          ]
      )
qed

lemma cat_pullback_ex_is_iso_arr':
  assumes "x : X <⇩C⇩F⇩.⇩p⇩b 𝔞→𝔤→𝔬←𝔣←𝔟 ↦↦⇩C⇘α⇙ ℭ"
    and "x' : X' <⇩C⇩F⇩.⇩p⇩b 𝔞→𝔤→𝔬←𝔣←𝔟 ↦↦⇩C⇘α⇙ ℭ"
  obtains f where "f : X' ↦⇩i⇩s⇩o⇘ℭ⇙ X" 
    and "x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f"
    and "x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f"
proof-
  interpret x: is_cat_pullback α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X x by (rule assms(1))
  interpret x': is_cat_pullback α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X' x' by (rule assms(2))
  obtain f where f: "f : X' ↦⇩i⇩s⇩o⇘ℭ⇙ X"
    and "j ∈⇩∘ →∙←⇩C⦇Obj⦈ ⟹ x'⦇NTMap⦈⦇j⦈ = x⦇NTMap⦈⦇j⦈ ∘⇩A⇘ℭ⇙ f" for j
    by 
      (
        elim cat_lim_ex_is_iso_arr'[
          OF x.is_cat_limit_axioms x'.is_cat_limit_axioms
          ]
      )
  then have 
    "x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔞⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f" 
    "x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = x⦇NTMap⦈⦇𝔟⇩S⇩S⦈ ∘⇩A⇘ℭ⇙ f"
    by (auto simp: cat_ss_cs_intros)
  with f show ?thesis using that by simp
qed

lemma cat_pushout_ex_is_iso_arr:
  assumes "x : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X ↦↦⇩C⇘α⇙ ℭ"
    and "x' : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X' ↦↦⇩C⇘α⇙ ℭ"
  obtains f where "f : X ↦⇩i⇩s⇩o⇘ℭ⇙ X'" 
    and "x' = ntcf_const ←∙→⇩C ℭ f ∙⇩N⇩T⇩C⇩F x"
proof-
  interpret x: is_cat_pushout α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X x by (rule assms(1))
  interpret x': is_cat_pushout α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X' x' by (rule assms(2))
  from that show ?thesis
    by 
      (
        elim cat_colim_ex_is_iso_arr[
          OF x.is_cat_colimit_axioms x'.is_cat_colimit_axioms
          ]
      )
qed

lemma cat_pushout_ex_is_iso_arr':
  assumes "x : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X ↦↦⇩C⇘α⇙ ℭ"
    and "x' : 𝔞←𝔤←𝔬→𝔣→𝔟 >⇩C⇩F⇩.⇩p⇩o X' ↦↦⇩C⇘α⇙ ℭ"
  obtains f where "f : X ↦⇩i⇩s⇩o⇘ℭ⇙ X'" 
    and "x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = f ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈"
    and "x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = f ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈"
proof-
  interpret x: is_cat_pushout α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X x by (rule assms(1))
  interpret x': is_cat_pushout α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ X' x' by (rule assms(2))
  obtain f where f: "f : X ↦⇩i⇩s⇩o⇘ℭ⇙ X'"
    and "j ∈⇩∘ ←∙→⇩C⦇Obj⦈ ⟹ x'⦇NTMap⦈⦇j⦈ = f ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇j⦈" for j
    by 
      (
        elim cat_colim_ex_is_iso_arr'[
          OF x.is_cat_colimit_axioms x'.is_cat_colimit_axioms
          ]
      )
  then have "x'⦇NTMap⦈⦇𝔞⇩S⇩S⦈ = f ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔞⇩S⇩S⦈"
    and "x'⦇NTMap⦈⦇𝔟⇩S⇩S⦈ = f ∘⇩A⇘ℭ⇙ x⦇NTMap⦈⦇𝔟⇩S⇩S⦈"
    by (auto simp: cat_ss_cs_intros)
  with f show ?thesis using that by simp
qed

text‹\newpage›

end