# Theory CategoryWithPullbacks

(*  Title:       CategoryWithPullbacks
Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2019
Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter "Category with Pullbacks"

theory CategoryWithPullbacks
imports Limit
begin

text ‹
\sloppypar
In this chapter, we give a traditional definition of pullbacks in a category as
limits of cospan diagrams and we define a locale ‹category_with_pullbacks› that
is satisfied by categories in which every cospan diagram has a limit.
These definitions build on the general definition of limit that we gave in
@{theory Category3.Limit}.  We then define a locale ‹elementary_category_with_pullbacks›
that axiomatizes categories equipped with chosen functions that assign to each cospan
a corresponding span of projections'', which enjoy the familiar universal property
of a pullback.  After developing consequences of the axioms, we prove that the two
locales are in agreement, in the sense that every interpretation of
‹category_with_pullbacks› extends to an interpretation of
‹elementary_category_with_pullbacks›, and conversely, the underlying category of
an interpretation of ‹elementary_category_with_pullbacks› always yields an interpretation
of ‹category_with_pullbacks›.
›

section "Commutative Squares"

context category
begin

text ‹
The following provides some useful technology for working with commutative squares.
›

definition commutative_square
where "commutative_square f g h k ≡ cospan f g ∧ span h k ∧ dom f = cod h ∧ f ⋅ h = g ⋅ k"

lemma commutative_squareI [intro, simp]:
assumes "cospan f g" and "span h k" and "dom f = cod h" and "f ⋅ h = g ⋅ k"
shows "commutative_square f g h k"
using assms commutative_square_def by auto

lemma commutative_squareE [elim]:
assumes "commutative_square f g h k"
and "⟦ arr f; arr g; arr h; arr k; cod f = cod g; dom h = dom k; dom f = cod h;
dom g = cod k; f ⋅ h = g ⋅ k ⟧ ⟹ T"
shows T
using assms commutative_square_def
by (metis (mono_tags, lifting) seqE seqI)

lemma commutative_square_comp_arr:
assumes "commutative_square f g h k" and "seq h l"
shows "commutative_square f g (h ⋅ l) (k ⋅ l)"
using assms
apply (elim commutative_squareE, intro commutative_squareI, auto)
using comp_assoc by metis

lemma arr_comp_commutative_square:
assumes "commutative_square f g h k" and "seq l f"
shows "commutative_square (l ⋅ f) (l ⋅ g) h k"
using assms comp_assoc
by (elim commutative_squareE, intro commutative_squareI, auto)

end

section "Cospan Diagrams"

(* TODO: Rework the ugly development of equalizers into this form. *)

text ‹
The shape'' of a cospan diagram is a category having two non-identity arrows
with distinct domains and a common codomain.
›

locale cospan_shape
begin

datatype Arr = Null | AA | BB | TT | AT | BT

fun comp
where "comp AA AA = AA"
| "comp AT AA = AT"
| "comp TT AT = AT"
| "comp BB BB = BB"
| "comp BT BB = BT"
| "comp TT BT = BT"
| "comp TT TT = TT"
| "comp _ _ = Null"

interpretation partial_composition comp
proof
show "∃!n. ∀f. comp n f = n ∧ comp f n = n"
proof
show "∀f. comp Null f = Null ∧ comp f Null = Null" by simp
show "⋀n. ∀f. comp n f = n ∧ comp f n = n ⟹ n = Null"
by (metis comp.simps(8))
qed
qed

lemma null_char:
shows "null = Null"
proof -
have "∀f. comp Null f = Null ∧ comp f Null = Null" by simp
thus ?thesis
using null_def ex_un_null theI [of "λn. ∀f. comp n f = n ∧ comp f n = n"]
by (metis partial_magma.null_is_zero(2) partial_magma_axioms)
qed

lemma ide_char:
shows "ide f ⟷ f = AA ∨ f = BB ∨ f = TT"
proof
show "ide f ⟹ f = AA ∨ f = BB ∨ f = TT"
using ide_def null_char by (cases f, simp_all)
show "f = AA ∨ f = BB ∨ f = TT ⟹ ide f"
proof -
have 1: "⋀f g. f = AA ∨ f = BB ∨ f = TT ⟹
comp f f ≠ Null ∧
(comp g f ≠ Null ⟶ comp g f = g) ∧
(comp f g ≠ Null ⟶ comp f g = g)"
proof -
fix f g
show "f = AA ∨ f = BB ∨ f = TT ⟹
comp f f ≠ Null ∧
(comp g f ≠ Null ⟶ comp g f = g) ∧
(comp f g ≠ Null ⟶ comp f g = g)"
by (cases f; cases g, auto)
qed
assume f: "f = AA ∨ f = BB ∨ f = TT"
show "ide f"
using f 1 ide_def null_char by simp
qed
qed

fun Dom
where "Dom AA = AA"
| "Dom BB = BB"
| "Dom TT = TT"
| "Dom AT = AA"
| "Dom BT = BB"
| "Dom _ = Null"

fun Cod
where "Cod AA = AA"
| "Cod BB = BB"
| "Cod TT = TT"
| "Cod AT = TT"
| "Cod BT = TT"
| "Cod _ = Null"

lemma domains_char':
shows "domains f = (if f = Null then {} else {Dom f})"
using domains_def ide_char null_char
by (cases f, auto)

lemma codomains_char':
shows "codomains f = (if f = Null then {} else {Cod f})"
using codomains_def ide_char null_char
by (cases f, auto)

lemma arr_char:
shows "arr f ⟷ f ≠ Null"
using arr_def domains_char' codomains_char' by simp

lemma seq_char:
shows "seq g f ⟷ (f = AA ∧ (g = AA ∨ g = AT)) ∨
(f = BB ∧ (g = BB ∨ g = BT)) ∨
(f = AT ∧ g = TT) ∨
(f = BT ∧ g = TT) ∨
(f = TT ∧ g = TT)"
using arr_char null_char
by (cases f; cases g, simp_all)

interpretation category comp
proof
fix f g h
show "comp g f ≠ null ⟹ seq g f"
using null_char arr_char seq_char by simp
show "domains f ≠ {} ⟷ codomains f ≠ {}"
using domains_char' codomains_char' by auto
show "seq h g ⟹ seq (comp h g) f ⟹ seq g f"
using seq_char arr_char
by (cases g; cases h; simp_all)
show "seq h (comp g f) ⟹ seq g f ⟹ seq h g"
using seq_char arr_char
by (cases f; cases g; simp_all)
show "seq g f ⟹ seq h g ⟹ seq (comp h g) f"
using seq_char arr_char
by (cases f; simp_all; cases g; simp_all; cases h; auto)
show "seq g f ⟹ seq h g ⟹ comp (comp h g) f = comp h (comp g f)"
using seq_char
by (cases f; simp_all; cases g; simp_all; cases h; auto)
qed

lemma is_category:
shows "category comp"
..

lemma dom_char:
shows "dom = Dom"
using dom_def domains_char domains_char' null_char by fastforce

lemma cod_char:
shows "cod = Cod"
using cod_def codomains_char codomains_char' null_char by fastforce

end

sublocale cospan_shape ⊆ category comp
using is_category by auto

locale cospan_diagram =
J: cospan_shape +
C: category C
for C :: "'c comp"      (infixr "⋅" 55)
and f0 :: 'c
and f1 :: 'c +
assumes is_cospan: "C.cospan f0 f1"
begin

no_notation J.comp   (infixr "⋅" 55)
notation J.comp      (infixr "⋅⇩J" 55)

fun map
where "map J.AA = C.dom f0"
| "map J.BB = C.dom f1"
| "map J.TT = C.cod f0"
| "map J.AT = f0"
| "map J.BT = f1"
| "map _ = C.null"

end

sublocale cospan_diagram ⊆ diagram J.comp C map
proof
show "⋀f. ¬ J.arr f ⟹ map f = C.null"
using J.arr_char by simp
fix f
assume f: "J.arr f"
show "C.arr (map f)"
using f J.arr_char is_cospan by (cases f, simp_all)
show "C.dom (map f) = map (J.dom f)"
using f J.arr_char J.dom_char is_cospan by (cases f, simp_all)
show "C.cod (map f) = map (J.cod f)"
using f J.arr_char J.cod_char is_cospan by (cases f, simp_all)
next
fix f g
assume fg: "J.seq g f"
show "map (g ⋅⇩J f) = map g ⋅ map f"
using fg J.seq_char J.null_char J.not_arr_null is_cospan
apply (cases f; cases g, simp_all)
using C.comp_arr_dom C.comp_cod_arr by auto
qed

section "Category with Pullbacks"

text ‹
A \emph{pullback} in a category @{term C} is a limit of a cospan diagram in @{term C}.
›

context cospan_diagram
begin

definition mkCone
where "mkCone p0 p1 ≡ λj. if j = J.AA then p0
else if j = J.BB then p1
else if j = J.AT then f0 ⋅ p0
else if j = J.BT then f1 ⋅ p1
else if j = J.TT then f0 ⋅ p0
else C.null"

abbreviation is_rendered_commutative_by
where "is_rendered_commutative_by p0 p1 ≡ C.seq f0 p0 ∧ f0 ⋅ p0 = f1 ⋅ p1"

abbreviation has_as_pullback
where "has_as_pullback p0 p1 ≡ limit_cone (C.dom p0) (mkCone p0 p1)"

lemma cone_mkCone:
assumes "is_rendered_commutative_by p0 p1"
shows "cone (C.dom p0) (mkCone p0 p1)"
proof -
interpret E: constant_functor J.comp C ‹C.dom p0›
apply unfold_locales using assms by auto
show "cone (C.dom p0) (mkCone p0 p1)"
proof
fix f
show "¬ J.arr f ⟹ mkCone p0 p1 f = C.null"
using mkCone_def J.arr_char by simp
assume f: "J.arr f"
show "C.dom (mkCone p0 p1 f) = E.map (J.dom f)"
using assms f mkCone_def J.arr_char J.dom_char
apply (cases f, simp_all)
by (metis C.dom_comp)+
show "C.cod (mkCone p0 p1 f) = map (J.cod f)"
using assms f mkCone_def J.arr_char J.cod_char is_cospan
by (cases f, auto)
show "map f ⋅ mkCone p0 p1 (J.dom f) = mkCone p0 p1 f"
using assms f mkCone_def J.arr_char J.dom_char C.comp_ide_arr is_cospan
by (cases f, auto)
show "mkCone p0 p1 (J.cod f) ⋅ E.map f = mkCone p0 p1 f"
using assms f mkCone_def J.arr_char J.cod_char C.comp_arr_dom
apply (cases f, auto)
apply (metis C.dom_comp C.seqE)
by (metis C.dom_comp)+
qed
qed

lemma is_rendered_commutative_by_cone:
assumes "cone a χ"
shows "is_rendered_commutative_by (χ J.AA) (χ J.BB)"
proof -
interpret χ: cone J.comp C map a χ
using assms by auto
show ?thesis
proof
show "C.seq f0 (χ J.AA)"
by (metis C.seqI J.cod_char J.seq_char χ.preserves_cod χ.preserves_reflects_arr
J.seqE is_cospan J.Cod.simps(1) map.simps(1))
show "f0 ⋅ χ J.AA = f1 ⋅ χ J.BB"
by (metis J.cod_char J.dom_char χ.A.map_simp χ.naturality
J.Cod.simps(4-5) J.Dom.simps(4-5) J.comp.simps(2,5) J.seq_char map.simps(4-5))
qed
qed

lemma mkCone_cone:
assumes "cone a χ"
shows "mkCone (χ J.AA) (χ J.BB) = χ"
proof -
interpret χ: cone J.comp C map a χ
using assms by auto
have 1: "is_rendered_commutative_by (χ J.AA) (χ J.BB)"
using assms is_rendered_commutative_by_cone by blast
interpret mkCone_χ: cone J.comp C map ‹C.dom (χ J.AA)› ‹mkCone (χ J.AA) (χ J.BB)›
using assms cone_mkCone 1 by auto
show ?thesis
proof -
have "⋀j. j = J.AA ⟹ mkCone (χ J.AA) (χ J.BB) j = χ j"
using mkCone_def χ.is_extensional by simp
moreover have "⋀j. j = J.BB ⟹ mkCone (χ J.AA) (χ J.BB) j = χ j"
using mkCone_def χ.is_extensional by simp
moreover have "⋀j. j = J.TT ⟹ mkCone (χ J.AA) (χ J.BB) j = χ j"
using 1 mkCone_def χ.is_extensional χ.A.map_simp χ.preserves_comp_1
cospan_shape.seq_char χ.is_natural_2
apply simp
by (metis J.seqE J.comp.simps(5) map.simps(5))
ultimately have "⋀j. J.ide j ⟹ mkCone (χ J.AA) (χ J.BB) j = χ j"
using J.ide_char by auto
thus "mkCone (χ J.AA) (χ J.BB) = χ"
using mkCone_def NaturalTransformation.eqI [of J.comp C]
χ.natural_transformation_axioms mkCone_χ.natural_transformation_axioms
J.ide_char
by simp
qed
qed

lemma cone_iff_commutative_square:
shows "cone (C.dom h) (mkCone h k) ⟷ C.commutative_square f0 f1 h k"
using cone_mkCone mkCone_def J.arr_char J.ide_char is_rendered_commutative_by_cone
is_cospan C.commutative_square_def cospan_shape.Arr.simps(11)
C.dom_comp C.seqE C.seqI
apply (intro iffI)
by (intro C.commutative_squareI) metis+

lemma cones_map_mkCone_eq_iff:
assumes "is_rendered_commutative_by p0 p1" and "is_rendered_commutative_by p0' p1'"
and "«h : C.dom p0' → C.dom p0»"
shows "cones_map h (mkCone p0 p1) = mkCone p0' p1' ⟷ p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
proof -
interpret χ: cone J.comp C map ‹C.dom p0› ‹mkCone p0 p1›
using assms(1) cone_mkCone [of p0 p1] by blast
interpret χ': cone J.comp C map ‹C.dom p0'› ‹mkCone p0' p1'›
using assms(2) cone_mkCone [of p0' p1'] by blast
show ?thesis
proof
assume 3: "cones_map h (mkCone p0 p1) = mkCone p0' p1'"
show "p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
proof
show "p0 ⋅ h = p0'"
proof -
have "p0' = mkCone p0' p1' J.AA"
using mkCone_def J.arr_char by simp
also have "... = cones_map h (mkCone p0 p1) J.AA"
using 3 by simp
also have "... = p0 ⋅ h"
using assms mkCone_def J.arr_char χ.cone_axioms by auto
finally show ?thesis by auto
qed
show "p1 ⋅ h = p1'"
proof -
have "p1' = mkCone p0' p1' J.BB"
using mkCone_def J.arr_char by simp
also have "... = cones_map h (mkCone p0 p1) J.BB"
using 3 by simp
also have "... = p1 ⋅ h"
using assms mkCone_def J.arr_char χ.cone_axioms by auto
finally show ?thesis by auto
qed
qed
next
assume 4: "p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
show "cones_map h (mkCone p0 p1) = mkCone p0' p1'"
proof
fix j
have "¬ J.arr j ⟹ cones_map h (mkCone p0 p1) j = mkCone p0' p1' j"
using assms χ.cone_axioms mkCone_def J.arr_char by auto
moreover have "J.arr j ⟹ cones_map h (mkCone p0 p1) j = mkCone p0' p1' j"
using assms 4 χ.cone_axioms mkCone_def J.arr_char C.comp_assoc
by fastforce
ultimately show "cones_map h (mkCone p0 p1) j = mkCone p0' p1' j"
using J.arr_char J.Dom.cases by blast
qed
qed
qed

end

locale pullback_cone =
J: cospan_shape +
C: category C +
D: cospan_diagram C f0 f1 +
limit_cone J.comp C D.map ‹C.dom p0› ‹D.mkCone p0 p1›
for C :: "'c comp"      (infixr "⋅" 55)
and f0 :: 'c
and f1 :: 'c
and p0 :: 'c
and p1 :: 'c
begin

(* TODO: Equalizer should be simplifiable in the same way. *)
lemma renders_commutative:
shows "D.is_rendered_commutative_by p0 p1"
using D.mkCone_def D.cospan_diagram_axioms cone_axioms
cospan_diagram.is_rendered_commutative_by_cone
by fastforce

lemma is_universal':
assumes "D.is_rendered_commutative_by p0' p1'"
shows "∃!h. «h : C.dom p0' → C.dom p0» ∧ p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
proof -
have "D.cone (C.dom p0') (D.mkCone p0' p1')"
using assms D.cone_mkCone by blast
hence 1: "∃!h. «h : C.dom p0' → C.dom p0» ∧
D.cones_map h (D.mkCone p0 p1) = D.mkCone p0' p1'"
using is_universal by simp
have 2: "⋀h. «h : C.dom p0' → C.dom p0» ⟹
D.cones_map h (D.mkCone p0 p1) = D.mkCone p0' p1' ⟷
p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
using assms D.cones_map_mkCone_eq_iff [of p0 p1 p0' p1'] renders_commutative
by fastforce
thus ?thesis using 1 by blast
qed

lemma induced_arrowI':
assumes "D.is_rendered_commutative_by p0' p1'"
shows "«induced_arrow (C.dom p0') (D.mkCone p0' p1') : C.dom p0' → C.dom p0»"
and "p0 ⋅ induced_arrow (C.dom p0') (D.mkCone p0' p1') = p0'"
and "p1 ⋅ induced_arrow (C.dom p1') (D.mkCone p0' p1') = p1'"
proof -
interpret A': constant_functor J.comp C ‹C.dom p0'›
using assms by (unfold_locales, auto)
have cone: "D.cone (C.dom p0') (D.mkCone p0' p1')"
using assms D.cone_mkCone [of p0' p1'] by blast
show 1: "p0 ⋅ induced_arrow (C.dom p0') (D.mkCone p0' p1') = p0'"
proof -
have "p0 ⋅ induced_arrow (C.dom p0') (D.mkCone p0' p1') =
D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1'))
(D.mkCone p0 p1) J.AA"
using cone induced_arrowI(1) D.mkCone_def J.arr_char is_cone by force
also have "... = p0'"
proof -
have "D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1'))
(D.mkCone p0 p1) =
D.mkCone p0' p1'"
using cone induced_arrowI by blast
thus ?thesis
using J.arr_char D.mkCone_def by simp
qed
finally show ?thesis by auto
qed
show 2: "p1 ⋅ induced_arrow (C.dom p1') (D.mkCone p0' p1') = p1'"
proof -
have "p1 ⋅ induced_arrow (C.dom p1') (D.mkCone p0' p1') =
D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1'))
(D.mkCone p0 p1) J.BB"
proof -
have "C.dom p0' = C.dom p1'"
using assms by (metis C.dom_comp)
thus ?thesis
using cone induced_arrowI(1) D.mkCone_def J.arr_char is_cone by force
qed
also have "... = p1'"
proof -
have "D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1'))
(D.mkCone p0 p1) =
D.mkCone p0' p1'"
using cone induced_arrowI by blast
thus ?thesis
using J.arr_char D.mkCone_def by simp
qed
finally show ?thesis by auto
qed
show "«induced_arrow (C.dom p0') (D.mkCone p0' p1') : C.dom p0' → C.dom p0»"
using 1 cone induced_arrowI by simp
qed

end

context category
begin

definition has_as_pullback
where "has_as_pullback f0 f1 p0 p1 ≡
cospan f0 f1 ∧ cospan_diagram.has_as_pullback C f0 f1 p0 p1"

definition has_pullbacks
where "has_pullbacks = (∀f0 f1. cospan f0 f1 ⟶ (∃p0 p1. has_as_pullback f0 f1 p0 p1))"

lemma has_as_pullbackI [intro]:
assumes "cospan f g" and "commutative_square f g p q"
and "⋀h k. commutative_square f g h k ⟹ ∃!l. p ⋅ l = h ∧ q ⋅ l = k"
shows "has_as_pullback f g p q"
proof (unfold has_as_pullback_def, intro conjI)
show "arr f" and "arr g" and "cod f = cod g"
using assms(1) by auto
interpret J: cospan_shape .
interpret D: cospan_diagram C f g
using assms(1-2) by unfold_locales auto
show "D.has_as_pullback p q"
proof -
have 1: "D.is_rendered_commutative_by p q"
using assms ide_in_hom by blast
let ?χ = "D.mkCone p q"
let ?a = "dom p"
interpret χ: cone J.comp C D.map ?a ?χ
using assms(2) D.cone_mkCone 1 by auto
interpret χ: limit_cone J.comp C D.map ?a ?χ
proof
fix x χ'
assume χ': "D.cone x χ'"
interpret χ': cone J.comp C D.map x χ'
using χ' by simp
have 2: "D.is_rendered_commutative_by (χ' J.AA) (χ' J.BB)"
using χ' D.is_rendered_commutative_by_cone [of x χ'] by blast
have 3: "∃!l. p ⋅ l = χ' J.AA ∧ q ⋅ l = χ' J.BB"
using assms(1,3) 2 χ'.preserves_hom J.arr_char J.ide_char by simp
obtain l where l: "p ⋅ l = χ' J.AA ∧ q ⋅ l = χ' J.BB"
using 3 by blast
have "«l : x → ?a»"
using l 2 χ'.preserves_hom J.arr_char J.ide_char χ'.component_in_hom
χ'.is_extensional χ'.preserves_reflects_arr comp_in_homE null_is_zero(2) in_homE
by metis
moreover have "D.cones_map l (D.mkCone p q) = χ'"
using l D.cones_map_mkCone_eq_iff [of p q "χ' J.AA" "χ' J.BB" l]
by (metis (no_types, lifting) 1 2 D.mkCone_cone χ' calculation dom_comp in_homE seqE)
ultimately have "∃l. «l : x → ?a» ∧ D.cones_map l (D.mkCone p q) = χ'"
by blast
moreover have "⋀l'. ⟦«l' : x → ?a»; D.cones_map l' (D.mkCone p q) = χ'⟧ ⟹ l' = l"
proof -
fix l'
assume l': "«l' : x → ?a»"
assume eq: "D.cones_map l' (D.mkCone p q) = χ'"
have "p ⋅ l' = χ' J.AA ∧ q ⋅ l' = χ' J.BB"
using l' eq J.arr_char χ.cone_axioms D.mkCone_def by auto
thus "l' = l"
using 3 l by blast
qed
ultimately show "∃!l. «l : x → ?a» ∧ D.cones_map l (D.mkCone p q) = χ'"
by blast
qed
show "D.has_as_pullback p q"
using assms χ.limit_cone_axioms by blast
qed
qed

lemma has_as_pullbackE [elim]:
assumes "has_as_pullback f g p q"
and "⟦cospan f g; commutative_square f g p q;
⋀h k. commutative_square f g h k ⟹ ∃!l. p ⋅ l = h ∧ q ⋅ l = k⟧ ⟹ T"
shows T
proof -
interpret J: cospan_shape .
interpret D: cospan_diagram C f g
using assms(1) has_as_pullback_def
by (meson category_axioms cospan_diagram.intro cospan_diagram_axioms.intro)
have 1: "⋀h k. commutative_square f g h k ⟷ D.cone (dom h) (D.mkCone h k)"
using D.cone_iff_commutative_square by presburger
let ?χ = "D.mkCone p q"
interpret χ: limit_cone J.comp C D.map ‹dom p› ?χ
using assms(1) has_as_pullback_def D.cone_mkCone by blast
have "cospan f g"
using D.is_cospan by blast
moreover have csq: "commutative_square f g p q"
using 1 χ.cone_axioms by blast
moreover have "⋀h k. commutative_square f g h k ⟹ ∃!l. p ⋅ l = h ∧ q ⋅ l = k"
proof -
fix h k
assume 2: "commutative_square f g h k"
let ?χ' = "D.mkCone h k"
interpret χ': cone J.comp C D.map ‹dom h› ?χ'
using 1 2 by blast
have 3: "∃!l. «l : dom h → dom p» ∧ D.cones_map l ?χ = ?χ'"
using 1 2 χ.is_universal [of "dom h" "D.mkCone h k"] by blast
obtain l where l: "«l : dom h → dom p» ∧ D.cones_map l ?χ = ?χ'"
using 3 by blast
have "p ⋅ l = h ∧ q ⋅ l = k"
proof
have "p ⋅ l = D.cones_map l ?χ J.AA"
using χ.cone_axioms D.mkCone_def J.seq_char in_homE
apply simp
by (metis J.seqE l)
also have "... = h"
using l χ'.cone_axioms D.mkCone_def J.seq_char in_homE by simp
finally show "p ⋅ l = h" by blast
have "q ⋅ l = D.cones_map l ?χ J.BB"
using χ.cone_axioms D.mkCone_def J.seq_char in_homE
apply simp
by (metis J.seqE l)
also have "... = k"
using l χ'.cone_axioms D.mkCone_def J.seq_char in_homE by simp
finally show "q ⋅ l = k" by blast
qed
moreover have "⋀l'. p ⋅ l' = h ∧ q ⋅ l' = k ⟹ l' = l"
proof -
fix l'
assume 1: "p ⋅ l' = h ∧ q ⋅ l' = k"
have 2: "«l' : dom h → dom p»"
using 1
by (metis χ'.ide_apex arr_dom_iff_arr arr_iff_in_hom ideD(1) seqE dom_comp)
moreover have "D.cones_map l' ?χ = ?χ'"
using D.cones_map_mkCone_eq_iff
by (meson 1 2 csq D.cone_iff_commutative_square χ'.cone_axioms
commutative_squareE seqI)
ultimately show "l' = l"
using l χ.is_universal χ'.cone_axioms by blast
qed
ultimately show "∃!l. p ⋅ l = h ∧ q ⋅ l = k" by blast
qed
ultimately show T
using assms(2) by blast
qed

end

locale category_with_pullbacks =
category +
assumes has_pullbacks: has_pullbacks

section "Elementary Category with Pullbacks"

text ‹
An \emph{elementary category with pullbacks} is a category equipped with a specific
way of mapping each cospan to a span such that the resulting square commutes and
such that the span is universal for that property.  It is useful to assume that the
functions, mapping a cospan to the two projections of the pullback, are extensional;
that is, they yield @{term null} when applied to arguments that do not form a cospan.
›

locale elementary_category_with_pullbacks =
category C
for C :: "'a comp"                              (infixr "⋅" 55)
and prj0 :: "'a ⇒ 'a ⇒ 'a"                    ("𝗉⇩0[_, _]")
and prj1 :: "'a ⇒ 'a ⇒ 'a"                    ("𝗉⇩1[_, _]") +
assumes prj0_ext: "¬ cospan f g ⟹ 𝗉⇩0[f, g] = null"
and prj1_ext: "¬ cospan f g ⟹ 𝗉⇩1[f, g] = null"
and pullback_commutes [intro]: "cospan f g ⟹ commutative_square f g 𝗉⇩1[f, g] 𝗉⇩0[f, g]"
and universal: "commutative_square f g h k ⟹ ∃!l. 𝗉⇩1[f, g] ⋅ l = h ∧ 𝗉⇩0[f, g] ⋅ l = k"
begin

lemma pullback_commutes':
assumes "cospan f g"
shows "f ⋅ 𝗉⇩1[f, g] = g ⋅ 𝗉⇩0[f, g]"
using assms commutative_square_def by blast

lemma prj0_in_hom':
assumes "cospan f g"
shows "«𝗉⇩0[f, g] : dom 𝗉⇩0[f, g] → dom g»"
using assms pullback_commutes
by (metis category.commutative_squareE category_axioms in_homI)

lemma prj1_in_hom':
assumes "cospan f g"
shows "«𝗉⇩1[f, g] : dom 𝗉⇩0[f, g] → dom f»"
using assms pullback_commutes
by (metis category.commutative_squareE category_axioms in_homI)

text ‹
The following gives us a notation for the common domain of the two projections
of a pullback.
›

definition pbdom        (infix "↓↓" 51)
where "f ↓↓ g ≡ dom 𝗉⇩0[f, g]"

lemma pbdom_in_hom [intro]:
assumes "cospan f g"
shows "«f ↓↓ g : f ↓↓ g → f ↓↓ g»"
unfolding pbdom_def
using assms prj0_in_hom'
by (metis arr_dom_iff_arr arr_iff_in_hom cod_dom dom_dom in_homE)

lemma ide_pbdom [simp]:
assumes "cospan f g"
shows "ide (f ↓↓ g)"
using assms ide_in_hom by auto[1]

lemma prj0_in_hom [intro, simp]:
assumes "cospan f g" and "a = f ↓↓ g" and "b = dom g"
shows "«𝗉⇩0[f, g] : a → b»"
unfolding pbdom_def
using assms prj0_in_hom' by (simp add: pbdom_def)

lemma prj1_in_hom [intro, simp]:
assumes "cospan f g" and "a = f ↓↓ g" and "b = dom f"
shows "«𝗉⇩1[f, g] : a → b»"
unfolding pbdom_def
using assms prj1_in_hom' by (simp add: pbdom_def)

lemma prj0_simps [simp]:
assumes "cospan f g"
shows "arr 𝗉⇩0[f, g]" and "dom 𝗉⇩0[f, g] = f ↓↓ g" and "cod 𝗉⇩0[f, g] = dom g"
using assms prj0_in_hom by (blast, blast, blast)

lemma prj0_simps_arr [iff]:
shows "arr 𝗉⇩0[f, g] ⟷ cospan f g"
proof
show "cospan f g ⟹ arr 𝗉⇩0[f, g]"
using prj0_in_hom by auto
show "arr 𝗉⇩0[f, g] ⟹ cospan f g"
using prj0_ext not_arr_null by metis
qed

lemma prj1_simps [simp]:
assumes "cospan f g"
shows "arr 𝗉⇩1[f, g]" and "dom 𝗉⇩1[f, g] = f ↓↓ g" and "cod 𝗉⇩1[f, g] = dom f"
using assms prj1_in_hom by (blast, blast, blast)

lemma prj1_simps_arr [iff]:
shows "arr 𝗉⇩1[f, g] ⟷ cospan f g"
proof
show "cospan f g ⟹ arr 𝗉⇩1[f, g]"
using prj1_in_hom by auto
show "arr 𝗉⇩1[f, g] ⟹ cospan f g"
using prj1_ext not_arr_null by metis
qed

lemma span_prj:
assumes "cospan f g"
shows "span 𝗉⇩0[f, g] 𝗉⇩1[f, g]"
using assms by simp

text ‹
We introduce a notation for tupling, which produces the induced arrow into a pullback.
In our notation, the $0$-side'', which we regard as the input, occurs on the right,
and the $1$-side'', which we regard as the output, occurs on the left.
›

definition tuple         ("⟨_ ⟦_, _⟧ _⟩")
where "⟨h ⟦f, g⟧ k⟩ ≡ if commutative_square f g h k then
THE l. 𝗉⇩0[f, g] ⋅ l = k ∧ 𝗉⇩1[f, g] ⋅ l = h
else null"

lemma tuple_in_hom [intro]:
assumes "commutative_square f g h k"
shows "«⟨h ⟦f, g⟧ k⟩ : dom h → f ↓↓ g»"
proof
have 1: "𝗉⇩0[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ = k ∧ 𝗉⇩1[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ = h"
unfolding tuple_def
using assms universal theI [of "λl. 𝗉⇩0[f, g] ⋅ l = k ∧ 𝗉⇩1[f, g] ⋅ l = h"]
apply simp
by meson
show "arr ⟨h ⟦f, g⟧ k⟩"
using assms 1
apply (elim commutative_squareE)
by (metis (no_types, lifting) seqE)
show "dom ⟨h ⟦f, g⟧ k⟩ = dom h"
using assms 1
apply (elim commutative_squareE)
by (metis (no_types, lifting) dom_comp)
show "cod ⟨h ⟦f, g⟧ k⟩ = f ↓↓ g"
unfolding pbdom_def
using assms 1
apply (elim commutative_squareE)
by (metis seqE)
qed

lemma tuple_is_extensional:
assumes "¬ commutative_square f g h k"
shows "⟨h ⟦f, g⟧ k⟩ = null"
unfolding tuple_def
using assms by simp

lemma tuple_simps [simp]:
assumes "commutative_square f g h k"
shows "arr ⟨h ⟦f, g⟧ k⟩" and "dom ⟨h ⟦f, g⟧ k⟩ = dom h" and "cod ⟨h ⟦f, g⟧ k⟩ = f ↓↓ g"
using assms tuple_in_hom apply blast
using assms tuple_in_hom apply blast
using assms tuple_in_hom by blast

lemma prj_tuple [simp]:
assumes "commutative_square f g h k"
shows "𝗉⇩0[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ = k" and "𝗉⇩1[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ = h"
proof -
have 1: "𝗉⇩0[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ = k ∧ 𝗉⇩1[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ = h"
unfolding tuple_def
using assms universal theI [of "λl. 𝗉⇩0[f, g] ⋅ l = k ∧ 𝗉⇩1[f, g] ⋅ l = h"]
apply simp
by meson
show "𝗉⇩0[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ = k" using 1 by simp
show "𝗉⇩1[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ = h" using 1 by simp
qed

lemma tuple_prj:
assumes "cospan f g" and "seq 𝗉⇩1[f, g] h"
shows "⟨𝗉⇩1[f, g] ⋅ h ⟦f, g⟧ 𝗉⇩0[f, g] ⋅ h⟩ = h"
proof -
have 1: "commutative_square f g (𝗉⇩1[f, g] ⋅ h) (𝗉⇩0[f, g] ⋅ h)"
using assms pullback_commutes
have "𝗉⇩0[f, g] ⋅ ⟨𝗉⇩1[f, g] ⋅ h ⟦f, g⟧ 𝗉⇩0[f, g] ⋅ h⟩ = 𝗉⇩0[f, g] ⋅ h"
using assms 1 by simp
moreover have "𝗉⇩1[f, g] ⋅ ⟨𝗉⇩1[f, g] ⋅ h ⟦f, g⟧ 𝗉⇩0[f, g] ⋅ h⟩ = 𝗉⇩1[f, g] ⋅ h"
using assms 1 by simp
ultimately show ?thesis
unfolding tuple_def
using assms 1 universal [of f g "𝗉⇩1[f, g] ⋅ h" "𝗉⇩0[f, g] ⋅ h"]
theI_unique [of "λl. 𝗉⇩0[f, g] ⋅ l = 𝗉⇩0[f, g] ⋅ h ∧ 𝗉⇩1[f, g] ⋅ l = 𝗉⇩1[f, g] ⋅ h" h]
by auto
qed

lemma tuple_prj_spc [simp]:
assumes "cospan f g"
shows "⟨𝗉⇩1[f, g] ⟦f, g⟧ 𝗉⇩0[f, g]⟩ = f ↓↓ g"
proof -
have "⟨𝗉⇩1[f, g] ⟦f, g⟧ 𝗉⇩0[f, g]⟩ = ⟨𝗉⇩1[f, g] ⋅ (f ↓↓ g) ⟦f, g⟧ 𝗉⇩0[f, g] ⋅ (f ↓↓ g)⟩"
using assms comp_arr_dom by simp
thus ?thesis
using assms tuple_prj by simp
qed

lemma prj_joint_monic:
assumes "cospan f g" and "seq 𝗉⇩1[f, g] h" and "seq 𝗉⇩1[f, g] h'"
and "𝗉⇩0[f, g] ⋅ h = 𝗉⇩0[f, g] ⋅ h'" and "𝗉⇩1[f, g] ⋅ h = 𝗉⇩1[f, g] ⋅ h'"
shows "h = h'"
proof -
have "h = ⟨𝗉⇩1[f, g] ⋅ h ⟦f, g⟧ 𝗉⇩0[f, g] ⋅ h⟩"
using assms tuple_prj [of f g h] by simp
also have "... = ⟨𝗉⇩1[f, g] ⋅ h' ⟦f, g⟧ 𝗉⇩0[f, g] ⋅ h'⟩"
using assms by simp
also have "... = h'"
using assms tuple_prj [of f g h'] by simp
finally show ?thesis by blast
qed

text ‹
The pullback of an identity along an arbitrary arrow is an isomorphism.
›

lemma iso_pullback_ide:
assumes "cospan μ ν" and "ide μ"
shows "iso 𝗉⇩0[μ, ν]"
proof -
have "inverse_arrows 𝗉⇩0[μ, ν] ⟨ν ⟦μ, ν⟧ dom ν⟩"
proof
show 1: "ide (𝗉⇩0[μ, ν] ⋅ ⟨ν ⟦μ, ν⟧ dom ν⟩)"
using assms comp_arr_dom comp_cod_arr prj_tuple(1) by simp
show "ide (⟨ν ⟦μ, ν⟧ dom ν⟩ ⋅ 𝗉⇩0[μ, ν])"
proof -
have "⟨ν ⟦μ, ν⟧ dom ν⟩ ⋅ 𝗉⇩0[μ, ν] = (μ ↓↓ ν)"
proof -
have "𝗉⇩0[μ, ν] ⋅ ⟨ν ⟦μ, ν⟧ dom ν⟩ ⋅ 𝗉⇩0[μ, ν] = 𝗉⇩0[μ, ν] ⋅ (μ ↓↓ ν)"
proof -
have "𝗉⇩0[μ, ν] ⋅ ⟨ν ⟦μ, ν⟧ dom ν⟩ ⋅ 𝗉⇩0[μ, ν] = (𝗉⇩0[μ, ν] ⋅ ⟨ν ⟦μ, ν⟧ dom ν⟩) ⋅ 𝗉⇩0[μ, ν]"
using assms 1 comp_reduce by blast
also have "... = 𝗉⇩0[μ, ν] ⋅ (μ ↓↓ ν)"
using assms prj_tuple(1) pullback_commutes comp_arr_dom comp_cod_arr by simp
finally show ?thesis by blast
qed
moreover have "𝗉⇩1[μ, ν] ⋅ ⟨ν ⟦μ, ν⟧ dom ν⟩ ⋅ 𝗉⇩0[μ, ν] = 𝗉⇩1[μ, ν] ⋅ (μ ↓↓ ν)"
proof -
have "𝗉⇩1[μ, ν] ⋅ ⟨ν ⟦μ, ν⟧ dom ν⟩ ⋅ 𝗉⇩0[μ, ν] = (𝗉⇩1[μ, ν] ⋅ ⟨ν ⟦μ, ν⟧ dom ν⟩) ⋅ 𝗉⇩0[μ, ν]"
using assms(2) comp_assoc by simp
also have "... = ν ⋅ 𝗉⇩0[μ, ν]"
using assms comp_arr_dom comp_cod_arr prj_tuple(2) by fastforce
also have "... = μ ⋅ 𝗉⇩1[μ, ν]"
using assms pullback_commutes commutative_square_def by simp
also have "... = 𝗉⇩1[μ, ν] ⋅ (μ ↓↓ ν)"
using assms comp_arr_dom comp_cod_arr pullback_commutes commutative_square_def
by simp
finally show ?thesis by simp
qed
ultimately show ?thesis
using assms prj0_in_hom prj1_in_hom comp_arr_dom prj1_simps(1-2) prj_joint_monic
by metis
qed
thus ?thesis
using assms by auto
qed
qed
thus ?thesis by auto
qed

lemma comp_tuple_arr:
assumes "commutative_square f g h k" and "seq h l"
shows "⟨h ⟦f, g⟧ k⟩ ⋅ l = ⟨h ⋅ l ⟦f, g⟧ k ⋅ l⟩"
proof -
have "𝗉⇩0[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ ⋅ l = 𝗉⇩0[f, g] ⋅ ⟨h ⋅ l ⟦f, g⟧ k ⋅ l⟩"
proof -
have "𝗉⇩0[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ ⋅ l = (𝗉⇩0[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩) ⋅ l"
using comp_assoc by simp
also have "... = 𝗉⇩0[f, g] ⋅ ⟨h ⋅ l ⟦f, g⟧ k ⋅ l⟩"
using assms commutative_square_comp_arr by auto
finally show ?thesis by blast
qed
moreover have "𝗉⇩1[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ ⋅ l = 𝗉⇩1[f, g] ⋅ ⟨h ⋅ l ⟦f, g⟧ k ⋅ l⟩"
proof -
have "𝗉⇩1[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩ ⋅ l = (𝗉⇩1[f, g] ⋅ ⟨h ⟦f, g⟧ k⟩) ⋅ l"
using comp_assoc by simp
also have "... = 𝗉⇩1[f, g] ⋅ ⟨h ⋅ l ⟦f, g⟧ k ⋅ l⟩"
using assms commutative_square_comp_arr by auto
finally show ?thesis by blast
qed
moreover have "seq 𝗉⇩1[f, g] (⟨h ⟦f, g⟧ k⟩ ⋅ l)"
using assms tuple_in_hom prj1_in_hom by fastforce
ultimately show ?thesis
using assms prj_joint_monic [of f g "⟨h ⟦f, g⟧ k⟩ ⋅ l" "⟨h ⋅ l ⟦f, g⟧ k ⋅ l⟩"]
by auto
qed

lemma pullback_arr_cod:
assumes "arr f"
shows "inverse_arrows 𝗉⇩1[f, cod f] ⟨dom f ⟦f, cod f⟧ f⟩"
and "inverse_arrows 𝗉⇩0[cod f, f] ⟨f ⟦cod f, f⟧ dom f⟩"
proof -
show "inverse_arrows 𝗉⇩1[f, cod f] ⟨dom f ⟦f, cod f⟧ f⟩"
proof
show "ide (⟨dom f ⟦f, cod f⟧ f⟩ ⋅ 𝗉⇩1[f, cod f])"
proof -
have "⟨dom f ⟦f, cod f⟧ f⟩ ⋅ 𝗉⇩1[f, cod f] = f ↓↓ cod f"
proof -
have "𝗉⇩0[f, cod f] ⋅ ⟨dom f ⟦f, cod f⟧ f⟩ ⋅ 𝗉⇩1[f, cod f] = 𝗉⇩0[f, cod f] ⋅ (f ↓↓ cod f)"
proof -
have "𝗉⇩0[f, cod f] ⋅ ⟨dom f ⟦f, cod f⟧ f⟩ ⋅ 𝗉⇩1[f, cod f] =
(𝗉⇩0[f, cod f] ⋅ ⟨dom f ⟦f, cod f⟧ f⟩) ⋅ 𝗉⇩1[f, cod f]"
using comp_assoc by simp
also have "... = 𝗉⇩0[f, cod f] ⋅ (f ↓↓ cod f)"
using assms pullback_commutes [of f "cod f"] comp_arr_dom comp_cod_arr
by auto
finally show ?thesis by blast
qed
moreover
have "𝗉⇩1[f, cod f] ⋅ ⟨dom f ⟦f, cod f⟧ f⟩ ⋅ 𝗉⇩1[f, cod f] = 𝗉⇩1[f, cod f] ⋅ (f ↓↓ cod f)"
proof -
have "𝗉⇩1[f, cod f] ⋅ ⟨dom f ⟦f, cod f⟧ f⟩ ⋅ 𝗉⇩1[f, cod f] =
(𝗉⇩1[f, cod f] ⋅ ⟨dom f ⟦f, cod f⟧ f⟩) ⋅ 𝗉⇩1[f, cod f]"
using assms comp_assoc by presburger
also have "... = 𝗉⇩1[f, cod f] ⋅ (f ↓↓ cod f)"
using assms comp_arr_dom comp_cod_arr by simp
finally show ?thesis by blast
qed
ultimately show ?thesis
using assms
prj_joint_monic
[of f "cod f" "⟨dom f ⟦f, cod f⟧ f⟩ ⋅ 𝗉⇩1[f, cod f]" "f ↓↓ cod f"]
by simp
qed
thus ?thesis
using assms arr_cod cod_cod prj1_simps_arr by simp
qed
show "ide (𝗉⇩1[f, cod f] ⋅ ⟨dom f ⟦f, cod f⟧ f⟩)"
using assms comp_arr_dom comp_cod_arr by fastforce
qed
show "inverse_arrows 𝗉⇩0[cod f, f] ⟨f ⟦cod f, f⟧ dom f⟩"
proof
show "ide (𝗉⇩0[cod f, f] ⋅ ⟨f ⟦cod f, f⟧ dom f⟩)"
using assms comp_arr_dom comp_cod_arr by simp
show "ide (⟨f ⟦cod f, f⟧ dom f⟩ ⋅ 𝗉⇩0[cod f, f])"
proof -
have "⟨f ⟦cod f, f⟧ dom f⟩ ⋅ 𝗉⇩0[cod f, f] = cod f ↓↓ f"
proof -
have "𝗉⇩0[cod f, f] ⋅ ⟨f ⟦cod f, f⟧ dom f⟩ ⋅ 𝗉⇩0[cod f, f] = 𝗉⇩0[cod f, f] ⋅ (cod f ↓↓ f)"
proof -
have "𝗉⇩0[cod f, f] ⋅ ⟨f ⟦cod f, f⟧ dom f⟩ ⋅ 𝗉⇩0[cod f, f] =
(𝗉⇩0[cod f, f] ⋅ ⟨f ⟦cod f, f⟧ dom f⟩) ⋅ 𝗉⇩0[cod f, f]"
using comp_assoc by simp
also have "... = dom f ⋅ 𝗉⇩0[cod f, f]"
using assms comp_arr_dom comp_cod_arr by simp
also have "... = 𝗉⇩0[cod f, f] ⋅ (cod f ↓↓ f)"
using assms comp_arr_dom comp_cod_arr by simp
finally show ?thesis
using prj0_in_hom by blast
qed
moreover
have "𝗉⇩1[cod f, f] ⋅ ⟨f ⟦cod f, f⟧ dom f⟩ ⋅ 𝗉⇩0[cod f, f] = 𝗉⇩1[cod f, f] ⋅ (cod f ↓↓ f)"
proof -
have "𝗉⇩1[cod f, f] ⋅ ⟨f ⟦cod f, f⟧ dom f⟩ ⋅ 𝗉⇩0[cod f, f] =
(𝗉⇩1[cod f, f] ⋅ ⟨f ⟦cod f, f⟧ dom f⟩) ⋅ 𝗉⇩0[cod f, f]"
using comp_assoc by simp
also have "... = 𝗉⇩1[cod f, f] ⋅ (cod f ↓↓ f)"
using assms pullback_commutes [of "cod f" f] comp_arr_dom comp_cod_arr
by auto
finally show ?thesis by blast
qed
ultimately show ?thesis
using assms prj_joint_monic [of "cod f" f "⟨f ⟦cod f, f⟧ dom f⟩ ⋅ 𝗉⇩0[cod f, f]"]
by simp
qed
thus ?thesis using assms by simp
qed
qed
qed

text ‹
The pullback of a monomorphism along itself is automatically symmetric: the left
and right projections are equal.
›

lemma pullback_mono_self:
assumes "mono f"
shows "𝗉⇩0[f, f] = 𝗉⇩1[f, f]"
proof -
have "f ⋅ 𝗉⇩0[f, f] = f ⋅ 𝗉⇩1[f, f]"
using assms pullback_commutes [of f f]
by (metis commutative_squareE mono_implies_arr)
thus ?thesis
using assms monoE [of f "𝗉⇩1[f, f]" "𝗉⇩0[f, f]"]
by (metis mono_implies_arr prj0_simps(1,3) seqI)
qed

lemma pullback_iso_self:
assumes "iso f"
shows "𝗉⇩0[f, f] = 𝗉⇩1[f, f]"
using assms pullback_mono_self iso_is_section section_is_mono by simp

lemma pullback_ide_self [simp]:
assumes "ide a"
shows "𝗉⇩0[a, a] = 𝗉⇩1[a, a]"
using assms pullback_iso_self ide_is_iso by blast

end

section "Agreement between the Definitions"

text ‹
It is very easy to write locale assumptions that have unintended consequences
or that are even inconsistent.  So, to keep ourselves honest, we don't just accept the
definition of elementary category with pullbacks'', but in fact we formally establish
the sense in which it agrees with our standard definition of category with pullbacks'',
which is given in terms of limit cones.
This is extra work, but it ensures that we didn't make a mistake.
›

context category_with_pullbacks
begin

definition some_prj1  ("𝗉⇩1⇧?[_, _]")
where "𝗉⇩1⇧?[f, g] ≡ if cospan f g then
fst (SOME x. cospan_diagram.has_as_pullback C f g (fst x) (snd x))
else null"

definition some_prj0  ("𝗉⇩0⇧?[_, _]")
where "𝗉⇩0⇧?[f, g] ≡ if cospan f g then
snd (SOME x. cospan_diagram.has_as_pullback C f g (fst x) (snd x))
else null"

lemma prj_yields_pullback:
assumes "cospan f g"
shows "cospan_diagram.has_as_pullback C f g 𝗉⇩1⇧?[f, g] 𝗉⇩0⇧?[f, g]"
proof -
have "∃x. cospan_diagram.has_as_pullback C f g (fst x) (snd x)"
using assms has_pullbacks has_pullbacks_def has_as_pullback_def by simp
thus ?thesis
using assms has_pullbacks has_pullbacks_def some_prj0_def some_prj1_def
someI_ex [of "λx. cospan_diagram.has_as_pullback C f g (fst x) (snd x)"]
by simp
qed

interpretation elementary_category_with_pullbacks C some_prj0 some_prj1
proof
show "⋀f g. ¬ cospan f g ⟹ 𝗉⇩0⇧?[f, g] = null"
using some_prj0_def by auto
show "⋀f g. ¬ cospan f g ⟹ 𝗉⇩1⇧?[f, g] = null"
using some_prj1_def by auto
show "⋀f g. cospan f g ⟹ commutative_square f g 𝗉⇩1⇧?[f, g] 𝗉⇩0⇧?[f, g]"
proof
fix f g
assume fg: "cospan f g"
show "cospan f g" by fact
interpret J: cospan_shape .
interpret D: cospan_diagram C f g
using fg by (unfold_locales, auto)
let ?χ = "D.mkCone 𝗉⇩1⇧?[f, g] 𝗉⇩0⇧?[f, g]"
interpret χ: limit_cone J.comp C D.map ‹dom 𝗉⇩1⇧?[f, g]› ?χ
using fg prj_yields_pullback by auto
have 1: "𝗉⇩1⇧?[f, g] = ?χ J.AA ∧ 𝗉⇩0⇧?[f, g] = ?χ J.BB"
using D.mkCone_def by simp
show "span 𝗉⇩1⇧?[f, g] 𝗉⇩0⇧?[f, g]"
proof -
have "arr 𝗉⇩1⇧?[f, g] ∧ arr 𝗉⇩0⇧?[f, g]"
using 1 J.arr_char J.seq_char
by (metis J.seqE χ.preserves_reflects_arr)
moreover have "dom 𝗉⇩1⇧?[f, g] = dom 𝗉⇩0⇧?[f, g]"
using 1 D.is_rendered_commutative_by_cone χ.cone_axioms J.seq_char
by (metis J.cod_eqI J.seqE χ.A.map_simp χ.preserves_dom J.ide_char)
ultimately show ?thesis by simp
qed
show "dom f = cod 𝗉⇩1⇧?[f, g]"
using 1 fg χ.preserves_cod [of J.BB] J.cod_char D.mkCone_def
by (metis D.map.simps(1) D.preserves_cod J.seqE χ.preserves_cod cod_dom J.seq_char)
show "f ⋅ 𝗉⇩1⇧?[f, g] = g ⋅ 𝗉⇩0⇧?[f, g]"
using 1 fg D.is_rendered_commutative_by_cone χ.cone_axioms by force
qed
show "⋀f g h k. commutative_square f g h k ⟹ ∃!l. 𝗉⇩1⇧?[f, g] ⋅ l = h ∧ 𝗉⇩0⇧?[f, g] ⋅ l = k"
proof -
fix f g h k
assume fghk: "commutative_square f g h k"
interpret J: cospan_shape .
interpret D: cospan_diagram C f g
using fghk by (unfold_locales, auto)
let ?χ = "D.mkCone 𝗉⇩1⇧?[f, g] 𝗉⇩0⇧?[f, g]"
interpret χ: limit_cone J.comp C D.map ‹dom 𝗉⇩1⇧?[f, g]› ?χ
using fghk prj_yields_pullback by auto
interpret χ: pullback_cone C f g ‹𝗉⇩1⇧?[f, g]› ‹𝗉⇩0⇧?[f, g]› ..
have 1: "𝗉⇩1⇧?[f, g] = ?χ J.AA ∧ 𝗉⇩0⇧?[f, g] = ?χ J.BB"
using D.mkCone_def by simp
show "∃!l. 𝗉⇩1⇧?[f, g] ⋅ l = h ∧ 𝗉⇩0⇧?[f, g] ⋅ l = k"
proof
let ?l = "SOME l. 𝗉⇩1⇧?[f, g] ⋅ l = h ∧ 𝗉⇩0⇧?[f, g] ⋅ l = k"
show "𝗉⇩1⇧?[f, g] ⋅ ?l = h ∧ 𝗉⇩0⇧?[f, g] ⋅ ?l = k"
using fghk χ.is_universal' χ.renders_commutative
someI_ex [of "λl. 𝗉⇩1⇧?[f, g] ⋅ l = h ∧ 𝗉⇩0⇧?[f, g] ⋅ l = k"]
by blast
thus "⋀l. 𝗉⇩1⇧?[f, g] ⋅ l = h ∧ 𝗉⇩0⇧?[f, g] ⋅ l = k ⟹ l = ?l"
using fghk χ.is_universal' χ.renders_commutative limit_cone_def
by (metis (no_types, lifting) in_homI seqE commutative_squareE dom_comp seqI)
qed
qed
qed

proposition extends_to_elementary_category_with_pullbacks:
shows "elementary_category_with_pullbacks C some_prj0 some_prj1"
..

end

context elementary_category_with_pullbacks
begin

interpretation category_with_pullbacks C
proof
show "has_pullbacks"
proof (unfold has_pullbacks_def)
have "⋀f g. cospan f g ⟹ ∃p0 p1. has_as_pullback f g p0 p1"
proof -
fix f g
assume fg: "cospan f g"
have "has_as_pullback f g 𝗉⇩1[f, g] 𝗉⇩0[f, g]"
using fg has_as_pullbackI pullback_commutes universal by presburger
thus "∃p0 p1. has_as_pullback f g p0 p1" by blast
qed
thus "∀f g. cospan f g ⟶ (∃p0 p1. has_as_pullback f g p0 p1)"
by simp
qed
qed

proposition is_category_with_pullbacks:
shows "category_with_pullbacks C"
..

end

sublocale elementary_category_with_pullbacks ⊆ category_with_pullbacks
using is_category_with_pullbacks by auto

end