# Theory CartesianCategory

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

chapter "Cartesian Category"

text‹
In this chapter, we explore the notion of a cartesian category'', which we define
to be a category having binary products and a terminal object.
We show that every cartesian category extends to an elementary cartesian category'',
whose definition assumes that specific choices have been made for projections and
terminal object.
Conversely, the underlying category of an elementary cartesian category is a
cartesian category.
We also show that cartesian categories are the same thing as categories with
finite products.
›

theory CartesianCategory
imports Limit SetCat CategoryWithPullbacks
begin

section "Category with Binary Products"

subsection "Binary Product Diagrams"

text ‹
The shape'' of a binary product diagram is a category having two distinct identity arrows
and no non-identity arrows.
›

locale binary_product_shape
begin

sublocale concrete_category ‹UNIV :: bool set› ‹λa b. if a = b then {()} else {}›
‹λ_. ()› ‹λ_ _ _ _ _. ()›
apply (unfold_locales, auto)
apply (meson empty_iff)
by (meson empty_iff)

abbreviation comp
where "comp ≡ COMP"

abbreviation FF
where "FF ≡ MkIde False"

abbreviation TT
where "TT ≡ MkIde True"

lemma arr_char:
shows "arr f ⟷ f = FF ∨ f = TT"
using arr_char by (cases f, simp_all)

lemma ide_char:
shows "ide f ⟷ f = FF ∨ f = TT"
using ide_char⇩C⇩C ide_MkIde by (cases f, auto)

lemma is_discrete:
shows "ide f ⟷ arr f"
using arr_char ide_char by simp

lemma dom_simp [simp]:
assumes "arr f"
shows "dom f = f"
using assms is_discrete by simp

lemma cod_simp [simp]:
assumes "arr f"
shows "cod f = f"
using assms is_discrete by simp

lemma seq_char:
shows "seq f g ⟷ arr f ∧ f = g"
by auto

lemma comp_simp [simp]:
assumes "seq f g"
shows "comp f g = f"
using assms seq_char by fastforce

end

locale binary_product_diagram =
J: binary_product_shape +
C: category C
for C :: "'c comp"      (infixr "⋅" 55)
and a0 :: 'c
and a1 :: 'c +
assumes is_discrete: "C.ide a0 ∧ C.ide a1"
begin

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

fun map
where "map J.FF = a0"
| "map J.TT = a1"
| "map _ = C.null"

sublocale diagram J.comp C map
proof
show "⋀f. ¬ J.arr f ⟹ map f = C.null"
using J.arr_char map.elims by auto
fix f
assume f: "J.arr f"
show "C.arr (map f)"
using f J.arr_char is_discrete C.ideD(1) map.simps(1-2) by metis
show "C.dom (map f) = map (J.dom f)"
using f J.arr_char J.dom_char is_discrete by force
show "C.cod (map f) = map (J.cod f)"
using f J.arr_char J.cod_char is_discrete by force
next
fix f g
assume fg: "J.seq g f"
show "map (g ⋅⇩J f) = map g ⋅ map f"
using fg J.arr_char J.seq_char J.null_char J.not_arr_null is_discrete
by (metis (no_types, lifting) C.comp_ide_self J.comp_simp map.simps(1-2))
qed

end

subsection "Category with Binary Products"

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

context binary_product_diagram
begin

definition mkCone
where "mkCone p0 p1 ≡ λj. if j = J.FF then p0 else if j = J.TT then p1 else C.null"

abbreviation is_rendered_commutative_by
where "is_rendered_commutative_by p0 p1 ≡
C.seq a0 p0 ∧ C.seq a1 p1 ∧ C.dom p0 = C.dom p1"

abbreviation has_as_binary_product
where "has_as_binary_product 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›
using assms by unfold_locales auto
show "cone (C.dom p0) (mkCone p0 p1)"
using assms mkCone_def J.arr_char E.map_simp is_discrete C.comp_ide_arr C.comp_arr_dom
by unfold_locales auto
qed

lemma is_rendered_commutative_by_cone:
assumes "cone a χ"
shows "is_rendered_commutative_by (χ J.FF) (χ J.TT)"
proof -
interpret χ: cone J.comp C map a χ
using assms by auto
show ?thesis
using is_discrete by simp
qed

lemma mkCone_cone:
assumes "cone a χ"
shows "mkCone (χ J.FF) (χ J.TT) = χ"
proof -
interpret χ: cone J.comp C map a χ
using assms by auto
interpret mkCone_χ: cone J.comp C map ‹C.dom (χ J.FF)› ‹mkCone (χ J.FF) (χ J.TT)›
using assms is_rendered_commutative_by_cone cone_mkCone by blast
show ?thesis
using mkCone_def χ.is_extensional J.ide_char mkCone_def
NaturalTransformation.eqI [of J.comp C]
χ.natural_transformation_axioms mkCone_χ.natural_transformation_axioms
by fastforce
qed

lemma cone_iff_span:
shows "cone (C.dom h) (mkCone h k) ⟷ C.span h k ∧ C.cod h = a0 ∧ C.cod k = a1"
by (metis (no_types, lifting) C.cod_eqI C.comp_cod_arr C.comp_ide_arr J.arr.simps(1)
cone_mkCone is_discrete is_rendered_commutative_by_cone mkCone_def)

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 1: "cones_map h (mkCone p0 p1) = mkCone p0' p1'"
show "p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
proof
show "p0 ⋅ h = p0'"
proof -
have "p0' = cones_map h (mkCone p0 p1) J.FF"
using 1 mkCone_def J.arr_char 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' = cones_map h (mkCone p0 p1) J.TT"
using 1 mkCone_def J.arr_char 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 "p0 ⋅ h = p0' ∧ p1 ⋅ h = p1'"
thus "cones_map h (mkCone p0 p1) = mkCone p0' p1'"
using assms χ.cone_axioms mkCone_def J.arr_char by auto
qed
qed

end

locale binary_product_cone =
J: binary_product_shape +
C: category C +
D: binary_product_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

lemma renders_commutative:
shows "D.is_rendered_commutative_by p0 p1"
using cone_axioms D.is_rendered_commutative_by_cone D.mkCone_def D.cone_iff_span
by force

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 "∃!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
moreover have "⋀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 blast
ultimately show ?thesis 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 0: "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.FF"
using cone induced_arrowI(1) D.mkCone_def J.arr_char is_cone by force
also have "... = p0'"
by (metis (no_types, lifting) D.mkCone_def cone induced_arrowI(2)
mem_Collect_eq restrict_apply)
finally show ?thesis by auto
qed
show "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.TT"
using assms cone induced_arrowI(1) D.mkCone_def J.arr_char is_cone by fastforce
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 0 cone induced_arrowI by simp
qed

end

context category
begin

definition has_as_binary_product
where "has_as_binary_product a0 a1 p0 p1 ≡
ide a0 ∧ ide a1 ∧ binary_product_diagram.has_as_binary_product C a0 a1 p0 p1"

definition has_binary_products
where "has_binary_products =
(∀a0 a1. ide a0 ∧ ide a1 ⟶ (∃p0 p1. has_as_binary_product a0 a1 p0 p1))"

lemma has_as_binary_productI [intro]:
assumes "ide a" and "ide b"
and "«p : c → a»" and "«q : c → b»"
and "⋀x f g. ⟦«f : x → a»; «g : x → b»⟧ ⟹ ∃!h. «h : x → c» ∧ p ⋅ h = f ∧ q ⋅ h = g"
shows "has_as_binary_product a b p q"
proof (unfold has_as_binary_product_def, intro conjI)
show "ide a" by fact
show "ide b" by fact
interpret J: binary_product_shape .
interpret D: binary_product_diagram C a b
using assms(1-2) by unfold_locales auto
show "D.has_as_binary_product p q"
proof -
have 1: "D.is_rendered_commutative_by p q"
using assms ide_in_hom by blast
let ?χ = "D.mkCone p q"
interpret χ: cone J.comp C D.map c ?χ
using assms(4) D.cone_mkCone 1 by auto
interpret χ: limit_cone J.comp C D.map c ?χ
proof
fix x χ'
assume χ': "D.cone x χ'"
interpret χ': cone J.comp C D.map x χ'
using χ' by simp
have 2: "∃!h. «h : x → c» ∧ p ⋅ h = χ' J.FF ∧ q ⋅ h = χ' J.TT"
proof -
have "«χ' J.FF : x → a» ∧ «χ' J.TT : x → b»"
by auto
thus ?thesis
using assms(5) [of "χ' J.FF" x "χ' J.TT"] by simp
qed
have 3: "D.is_rendered_commutative_by (χ' J.FF) (χ' J.TT)"
using assms(1-2) by force
obtain h where h: "«h : x → c» ∧ p ⋅ h = χ' J.FF ∧ q ⋅ h = χ' J.TT"
using 2 by blast
have 4: "«h : dom (χ' (J.MkIde False)) → dom p»"
using assms(3) h by auto
have "«h : x → c» ∧ D.cones_map h (D.mkCone p q) = χ'"
proof (intro conjI)
show "«h : x → c»"
using h by blast
show "D.cones_map h (D.mkCone p q) = χ'"
proof
fix j
show "D.cones_map h (D.mkCone p q) j = χ' j"
using h 1 3 4 D.cones_map_mkCone_eq_iff [of p q "χ' J.FF" "χ' J.TT"]
χ.cone_axioms J.is_discrete χ'.is_extensional
D.mkCone_def binary_product_shape.ide_char
by (cases "J.ide j") auto
qed
qed
moreover have "⋀h'. «h' : x → c» ∧ D.cones_map h' (D.mkCone p q) = χ' ⟹ h' = h"
proof -
fix h'
assume 5: "«h' : x → c» ∧ D.cones_map h' (D.mkCone p q) = χ'"
have "∃!h. «h : x → c» ∧ p ⋅ h = χ' J.FF ∧ q ⋅ h = χ' J.TT"
moreover have "«h : x → c» ∧ χ' J.FF = p ⋅ h ∧ q ⋅ h = χ' J.TT"
using h by simp
moreover have "«h' : x → c» ∧ χ' J.FF = p ⋅ h' ∧ q ⋅ h' = χ' J.TT"
using 5 χ.cone_axioms D.mkCone_def [of p q] by auto
ultimately show "h' = h" by auto
qed
ultimately show "∃!h. «h : x → c» ∧ D.cones_map h (D.mkCone p q) = χ'"
by blast
qed
show "D.has_as_binary_product p q"
using assms χ.limit_cone_axioms by blast
qed
qed

lemma has_as_binary_productE [elim]:
assumes "has_as_binary_product a b p q"
and "⟦«p : dom p → a»; «q : dom p → b»;
⋀x f g. ⟦«f : x → a»; «g : x → b»⟧ ⟹ ∃!h. p ⋅ h = f ∧ q ⋅ h = g⟧ ⟹ T"
shows T
proof -
interpret J: binary_product_shape .
interpret D: binary_product_diagram C a b
using assms(1) has_as_binary_product_def
category_axioms)
have 1: "⋀h k. span h k ∧ cod h = a ∧ cod k = b ⟷ D.cone (dom h) (D.mkCone h k)"
using D.cone_iff_span by presburger
let ?χ = "D.mkCone p q"
interpret χ: limit_cone J.comp C D.map ‹dom p› ?χ
using assms(1) has_as_binary_product_def D.cone_mkCone by blast
have span: "span p q"
using 1 χ.cone_axioms by blast
moreover have "«p : dom p → a» ∧ «q : dom p → b»"
using span χ.preserves_hom χ.cone_axioms binary_product_shape.arr_char
by (metis D.cone_iff_span arr_iff_in_hom)
moreover have "⋀x f g. ⟦«f : x → a»; «g : x → b»⟧ ⟹ ∃!l. p ⋅ l = f ∧ q ⋅ l = g"
proof -
fix x f g
assume f: "«f : x → a»" and g: "«g : x → b»"
let ?χ' = "D.mkCone f g"
interpret χ': cone J.comp C D.map x ?χ'
using 1 f g by blast
have 2: "∃!l. «l : x → dom p» ∧ D.cones_map l ?χ = ?χ'"
using 1 f g χ.is_universal [of x "D.mkCone f g"] χ'.cone_axioms by fastforce
obtain l where l: "«l : x → dom p» ∧ D.cones_map l ?χ = ?χ'"
using 2 by blast
have "p ⋅ l = f ∧ q ⋅ l = g"
proof
show "p ⋅ l = f"
proof -
have "p ⋅ l = ?χ J.FF ⋅ l"
using D.mkCone_def by presburger
also have "... = D.cones_map l ?χ J.FF"
using χ.cone_axioms
apply simp
using l by fastforce
also have "... = f"
using D.mkCone_def l by presburger
finally show ?thesis by blast
qed
show "q ⋅ l = g"
proof -
have "q ⋅ l = ?χ J.TT ⋅ l"
using D.mkCone_def by simp
also have "... = D.cones_map l ?χ J.TT"
using χ.cone_axioms
apply simp
using l by fastforce
also have "... = g"
using D.mkCone_def l by simp
finally show "q ⋅ l = g" by blast
qed
qed
moreover have "⋀l'. p ⋅ l' = f ∧ q ⋅ l' = g ⟹ l' = l"
proof -
fix l'
assume 1: "p ⋅ l' = f ∧ q ⋅ l' = g"
have 2: "«l' : x → dom p»"
using 1 f by blast
moreover have "D.cones_map l' ?χ = ?χ'"
using 1 2 D.cones_map_mkCone_eq_iff [of p q f g l']
by (metis (no_types, lifting) f g ‹«p : dom p → a» ∧ «q : dom p → b»›
comp_cod_arr in_homE)
ultimately show "l' = l"
using l χ.is_universal χ'.cone_axioms by blast
qed
ultimately show "∃!l. p ⋅ l = f ∧ q ⋅ l = g" by blast
qed
ultimately show T
using assms(2) by simp
qed

end

locale category_with_binary_products =
category +
assumes has_binary_products: has_binary_products

subsection "Elementary Category with Binary Products"

text ‹
An \emph{elementary category with binary products} is a category equipped with a specific
way of mapping each pair of objects ‹a› and ‹b› to a pair of arrows ‹𝔭⇩1[a, b]› and ‹𝔭⇩0[a, b]›
that comprise a universal span.
›

locale elementary_category_with_binary_products =
category C
for C :: "'a comp"                             (infixr "⋅" 55)
and pr0 :: "'a ⇒ 'a ⇒ 'a"                    ("𝔭⇩0[_, _]")
and pr1 :: "'a ⇒ 'a ⇒ 'a"                    ("𝔭⇩1[_, _]") +
assumes span_pr: "⟦ ide a; ide b ⟧ ⟹ span 𝔭⇩1[a, b] 𝔭⇩0[a, b]"
and cod_pr0: "⟦ ide a; ide b ⟧ ⟹ cod 𝔭⇩0[a, b] = b"
and cod_pr1: "⟦ ide a; ide b ⟧ ⟹ cod 𝔭⇩1[a, b] = a"
and universal: "span f g ⟹ ∃!l. 𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g"
begin

lemma pr0_in_hom':
assumes "ide a" and "ide b"
shows "«𝔭⇩0[a, b] : dom 𝔭⇩0[a, b] → b»"
using assms span_pr cod_pr0 by auto

lemma pr1_in_hom':
assumes "ide a" and "ide b"
shows "«𝔭⇩1[a, b] : dom 𝔭⇩0[a, b] → a»"
using assms span_pr cod_pr1 by auto

text ‹
We introduce a notation for tupling, which denotes the arrow into a product that
is induced by a span.
›

definition tuple         ("⟨_, _⟩")
where "⟨f, g⟩ ≡ if span f g then
THE l. 𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g
else null"

text ‹
The following defines product of arrows (not just of objects).  It will take a little
while before we can prove that it is functorial, but for right now it is nice to have
it as a notation for the apex of a product cone.  We have to go through some slightly
unnatural contortions in the development here, though, to avoid having to introduce a
separate preliminary notation just for the product of objects.
›
(* TODO: I want to use × but it has already been commandeered for product types. *)
definition prod         (infixr "⊗" 51)
where "f ⊗ g ≡ ⟨f ⋅ 𝔭⇩1[dom f, dom g], g ⋅ 𝔭⇩0[dom f, dom g]⟩"

lemma seq_pr_tuple:
assumes "span f g"
shows "seq 𝔭⇩0[cod f, cod g] ⟨f, g⟩"
proof -
have "𝔭⇩0[cod f, cod g] ⋅ ⟨f, g⟩ = g"
unfolding tuple_def
using assms universal theI [of "λl. 𝔭⇩1[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0[cod f, cod g] ⋅ l = g"]
by simp meson
thus ?thesis
using assms by simp
qed

lemma tuple_pr_arr:
assumes "ide a" and "ide b" and "seq 𝔭⇩0[a, b] h"
shows "⟨𝔭⇩1[a, b] ⋅ h, 𝔭⇩0[a, b] ⋅ h⟩ = h"
unfolding tuple_def
using assms span_pr cod_pr0 cod_pr1 universal [of "𝔭⇩1[a, b] ⋅ h" "𝔭⇩0[a, b] ⋅ h"]
theI_unique [of "λl. 𝔭⇩1[a, b] ⋅ l = 𝔭⇩1[a, b] ⋅ h ∧ 𝔭⇩0[a, b] ⋅ l = 𝔭⇩0[a, b] ⋅ h" h]
by auto

lemma pr_tuple [simp]:
assumes "span f g" and "cod f = a" and "cod g = b"
shows "𝔭⇩1[a, b] ⋅ ⟨f, g⟩ = f" and "𝔭⇩0[a, b] ⋅ ⟨f, g⟩ = g"
proof -
have 1: "𝔭⇩1[a, b] ⋅ ⟨f, g⟩ = f ∧ 𝔭⇩0[a, b] ⋅ ⟨f, g⟩ = g"
unfolding tuple_def
using assms universal theI [of "λl. 𝔭⇩1[a, b] ⋅ l = f ∧ 𝔭⇩0[a, b] ⋅ l = g"]
by simp meson
show "𝔭⇩1[a, b] ⋅ ⟨f, g⟩ = f" using 1 by simp
show "𝔭⇩0[a, b] ⋅ ⟨f, g⟩ = g" using 1 by simp
qed

lemma cod_tuple:
assumes "span f g"
shows "cod ⟨f, g⟩ = cod f ⊗ cod g"
proof -
have "cod f ⊗ cod g = ⟨𝔭⇩1[cod f, cod g], 𝔭⇩0[cod f, cod g]⟩"
unfolding prod_def
using assms comp_cod_arr span_pr cod_pr0 cod_pr1 by simp
also have "... = ⟨𝔭⇩1[cod f, cod g] ⋅ dom 𝔭⇩0[cod f, cod g],
𝔭⇩0[cod f, cod g] ⋅ dom 𝔭⇩0[cod f, cod g]⟩"
using assms span_pr comp_arr_dom by simp
also have "... = dom 𝔭⇩0[cod f, cod g]"
using assms tuple_pr_arr span_pr by simp
also have "... = cod ⟨f, g⟩"
using assms seq_pr_tuple by blast
finally show ?thesis by simp
qed

lemma tuple_in_hom [intro]:
assumes "«f : a → b»" and "«g : a → c»"
shows "«⟨f, g⟩ : a → b ⊗ c»"
using assms pr_tuple dom_comp cod_tuple
apply (elim in_homE, intro in_homI)
apply (metis seqE)
by metis+

lemma tuple_in_hom' [simp]:
assumes "arr f" and "dom f = a" and "cod f = b"
and "arr g" and "dom g = a" and "cod g = c"
shows "«⟨f, g⟩ : a → b ⊗ c»"
using assms by auto

lemma tuple_ext:
assumes "¬ span f g"
shows "⟨f, g⟩ = null"
unfolding tuple_def

lemma tuple_simps [simp]:
assumes "span f g"
shows "arr ⟨f, g⟩" and "dom ⟨f, g⟩ = dom f" and "cod ⟨f, g⟩ = cod f ⊗ cod g"
proof -
show "arr ⟨f, g⟩"
using assms tuple_in_hom by blast
show "dom ⟨f, g⟩ = dom f"
using assms tuple_in_hom
by (metis dom_comp pr_tuple(1))
show "cod ⟨f, g⟩ = cod f ⊗ cod g"
using assms cod_tuple by auto
qed

lemma tuple_pr [simp]:
assumes "ide a" and "ide b"
shows "⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩ = a ⊗ b"
proof -
have 1: "dom 𝔭⇩0[a, b] = a ⊗ b"
using assms seq_pr_tuple cod_tuple [of "𝔭⇩1[a, b]" "𝔭⇩0[a, b]"] span_pr
pr0_in_hom' pr1_in_hom'
by (metis cod_pr0 cod_pr1 seqE)
hence "⟨𝔭⇩1[a, b], 𝔭⇩0[a, b]⟩ = ⟨𝔭⇩1[a, b] ⋅ (a ⊗ b), 𝔭⇩0[a, b] ⋅ (a ⊗ b)⟩"
using assms pr0_in_hom' pr1_in_hom' comp_arr_dom span_pr by simp
thus ?thesis
using assms 1 tuple_pr_arr span_pr
by (metis comp_arr_dom)
qed

lemma pr_in_hom [intro, simp]:
assumes "ide a" and "ide b" and "x = a ⊗ b"
shows "«𝔭⇩0[a, b] : x → b»" and "«𝔭⇩1[a, b] : x → a»"
proof -
show 0: "«𝔭⇩0[a, b] : x → b»"
using assms pr0_in_hom' seq_pr_tuple [of "𝔭⇩1[a, b]" "𝔭⇩0[a, b]"]
cod_tuple [of "𝔭⇩1[a, b]" "𝔭⇩0[a, b]"] span_pr cod_pr0 cod_pr1
by (intro in_homI, auto)
show "«𝔭⇩1[a, b] : x → a»"
using assms 0 span_pr pr1_in_hom' by fastforce
qed

lemma pr_simps [simp]:
assumes "ide a" and "ide b"
shows "arr 𝔭⇩0[a, b]" and "dom 𝔭⇩0[a, b] = a ⊗ b" and "cod 𝔭⇩0[a, b] = b"
and "arr 𝔭⇩1[a, b]" and "dom 𝔭⇩1[a, b] = a ⊗ b" and "cod 𝔭⇩1[a, b] = a"
using assms pr_in_hom by blast+

lemma pr_joint_monic:
assumes "ide a" and "ide b" and "seq 𝔭⇩0[a, b] h"
and "𝔭⇩0[a, b] ⋅ h = 𝔭⇩0[a, b] ⋅ h'" and "𝔭⇩1[a, b] ⋅ h = 𝔭⇩1[a, b] ⋅ h'"
shows "h = h'"
using assms by (metis tuple_pr_arr)

lemma comp_tuple_arr [simp]:
assumes "span f g" and "arr h" and "dom f = cod h"
shows "⟨f, g⟩ ⋅ h = ⟨f ⋅ h, g ⋅ h⟩"
proof (intro pr_joint_monic [where h = "⟨f, g⟩ ⋅ h"])
show "ide (cod f)" and "ide (cod g)"
using assms ide_cod by blast+
show "seq 𝔭⇩0[cod f, cod g] (⟨f, g⟩ ⋅ h)"
using assms by fastforce
show "𝔭⇩0[cod f, cod g] ⋅ ⟨f, g⟩ ⋅ h = 𝔭⇩0[cod f, cod g] ⋅ ⟨f ⋅ h, g ⋅ h⟩"
using assms(1-3) comp_reduce by auto
show "𝔭⇩1[cod f, cod g] ⋅ ⟨f, g⟩ ⋅ h = 𝔭⇩1[cod f, cod g] ⋅ ⟨f ⋅ h, g ⋅ h⟩"
using assms comp_reduce by auto
qed

lemma ide_prod [intro, simp]:
assumes "ide a" and "ide b"
shows "ide (a ⊗ b)"
using assms pr_simps ide_dom [of "𝔭⇩0[a, b]"] by simp

lemma prod_in_hom [intro]:
assumes "«f : a → c»" and "«g : b → d»"
shows "«f ⊗ g : a ⊗ b → c ⊗ d»"
using assms prod_def by fastforce

lemma prod_in_hom' [simp]:
assumes "arr f" and "dom f = a" and "cod f = c"
and "arr g" and "dom g = b" and "cod g = d"
shows "«f ⊗ g : a ⊗ b → c ⊗ d»"
using assms by blast

lemma prod_simps [simp]:
assumes "arr f0" and "arr f1"
shows "arr (f0 ⊗ f1)"
and "dom (f0 ⊗ f1) = dom f0 ⊗ dom f1"
and "cod (f0 ⊗ f1) = cod f0 ⊗ cod f1"
using assms prod_in_hom by blast+

lemma has_as_binary_product:
assumes "ide a" and "ide b"
shows "has_as_binary_product a b 𝔭⇩1[a, b] 𝔭⇩0[a, b]"
proof
show "ide a" and "ide b"
using assms by auto
show "«𝔭⇩1[a, b] : dom 𝔭⇩1[a, b] → a»"
using assms by simp
show "«𝔭⇩0[a, b] : dom 𝔭⇩1[a, b] → b»"
using assms by simp
fix x f g
assume f: "«f : x → a»" and g: "«g : x → b»"
have "span f g"
using f g by auto
hence "∃!l. 𝔭⇩1[a, b] ⋅ l = f ∧ 𝔭⇩0[a, b] ⋅ l = g"
using assms f g universal [of f g]
by (metis in_homE)
thus "∃!h. «h : x → dom 𝔭⇩1[a, b]» ∧ 𝔭⇩1[a, b] ⋅ h = f ∧ 𝔭⇩0[a, b] ⋅ h = g"
using f by blast
qed

end

subsection "Agreement between the Definitions"

text ‹
We now show that a category with binary products extends (by making a choice)
to an elementary category with binary products, and that the underlying category
of an elementary category with binary products is a category with binary products.
›

context category_with_binary_products
begin

definition some_pr1  ("𝔭⇩1⇧?[_, _]")
where "some_pr1 a b ≡ if ide a ∧ ide b then
fst (SOME x. has_as_binary_product a b (fst x) (snd x))
else null"

definition some_pr0  ("𝔭⇩0⇧?[_, _]")
where "some_pr0 a b ≡ if ide a ∧ ide b then
snd (SOME x. has_as_binary_product a b (fst x) (snd x))
else null"

lemma pr_yields_binary_product:
assumes "ide a" and "ide b"
shows "has_as_binary_product a b 𝔭⇩1⇧?[a, b] 𝔭⇩0⇧?[a, b]"
proof -
have "∃x. has_as_binary_product a b (fst x) (snd x)"
using assms has_binary_products has_binary_products_def has_as_binary_product_def
by simp
thus ?thesis
using assms has_binary_products has_binary_products_def some_pr0_def some_pr1_def
someI_ex [of "λx. has_as_binary_product a b (fst x) (snd x)"]
by simp
qed

interpretation elementary_category_with_binary_products C some_pr0 some_pr1
proof
fix a b
assume a: "ide a" and b: "ide b"
interpret J: binary_product_shape .
interpret D: binary_product_diagram C a b
using a b by unfold_locales auto
let ?χ = "D.mkCone 𝔭⇩1⇧?[a, b] 𝔭⇩0⇧?[a, b]"
interpret χ: limit_cone J.comp C D.map ‹dom 𝔭⇩1⇧?[a, b]› ?χ
using a b pr_yields_binary_product
have 1: "𝔭⇩1⇧?[a, b] = ?χ J.FF ∧ 𝔭⇩0⇧?[a, b] = ?χ J.TT"
using D.mkCone_def by simp
show "span 𝔭⇩1⇧?[a, b] 𝔭⇩0⇧?[a, b]"
using 1 χ.preserves_reflects_arr J.seqE J.arr_char J.seq_char J.is_category
D.is_rendered_commutative_by_cone χ.cone_axioms
by metis
show "cod 𝔭⇩1⇧?[a, b] = a"
using 1 χ.preserves_cod [of J.FF] J.cod_char J.arr_char by auto
show "cod 𝔭⇩0⇧?[a, b] = b"
using 1 χ.preserves_cod [of J.TT] J.cod_char J.arr_char by auto
next
fix f g
assume fg: "span f g"
show "∃!l. 𝔭⇩1⇧?[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0⇧?[cod f, cod g] ⋅ l = g"
proof -
interpret J: binary_product_shape .
interpret D: binary_product_diagram C ‹cod f› ‹cod g›
using fg by unfold_locales auto
let ?χ = "D.mkCone 𝔭⇩1⇧?[cod f, cod g] 𝔭⇩0⇧?[cod f, cod g]"
interpret χ: limit_cone J.comp C D.map ‹dom 𝔭⇩1⇧?[cod f, cod g]› ?χ
using fg pr_yields_binary_product [of "cod f" "cod g"] has_as_binary_product_def
by simp
interpret χ: binary_product_cone C ‹cod f› ‹cod g› ‹𝔭⇩1⇧?[cod f, cod g]› ‹𝔭⇩0⇧?[cod f, cod g]› ..
have 1: "𝔭⇩1⇧?[cod f, cod g] = ?χ J.FF ∧ 𝔭⇩0⇧?[cod f, cod g] = ?χ J.TT"
using D.mkCone_def by simp
show "∃!l. 𝔭⇩1⇧?[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0⇧?[cod f, cod g] ⋅ l = g"
proof -
have "∃!l. «l : dom f → dom 𝔭⇩1⇧?[cod f, cod g]» ∧
𝔭⇩1⇧?[cod f, cod g] ⋅ l = f ∧ 𝔭⇩0⇧?[cod f, cod g] ⋅ l = g"
using fg χ.is_universal' by simp
moreover have "⋀l. 𝔭⇩1⇧?[cod f, cod g] ⋅ l = f ⟹ «l : dom f → dom 𝔭⇩1⇧?[cod f, cod g]»"
using fg dom_comp in_homI seqE seqI by metis
ultimately show ?thesis by auto
qed
qed
qed

proposition extends_to_elementary_category_with_binary_products:
shows "elementary_category_with_binary_products C some_pr0 some_pr1"
..

abbreviation some_prod    (infixr "⊗⇧?" 51)
where "some_prod ≡ prod"

end

context elementary_category_with_binary_products
begin

sublocale category_with_binary_products C
proof
show "has_binary_products"
by (meson has_as_binary_product has_binary_products_def)
qed

proposition is_category_with_binary_products:
shows "category_with_binary_products C"
..

end

subsection "Further Properties"

context elementary_category_with_binary_products
begin

lemma interchange:
assumes "seq h f" and "seq k g"
shows "(h ⊗ k) ⋅ (f ⊗ g) = h ⋅ f ⊗ k ⋅ g"
using assms prod_def comp_tuple_arr comp_assoc by fastforce

lemma pr_naturality [simp]:
assumes "arr g" and "dom g = b" and "cod g = d"
and "arr f" and "dom f = a" and "cod f = c"
shows "𝔭⇩0[c, d] ⋅ (f ⊗ g) = g ⋅ 𝔭⇩0[a, b]"
and "𝔭⇩1[c, d] ⋅ (f ⊗ g) = f ⋅ 𝔭⇩1[a, b]"
using assms prod_def by fastforce+

abbreviation dup ("𝖽[_]")
where "𝖽[f] ≡ ⟨f, f⟩"

lemma dup_in_hom [intro, simp]:
assumes "«f : a → b»"
shows "«𝖽[f] : a → b ⊗ b»"
using assms by fastforce

lemma dup_simps [simp]:
assumes "arr f"
shows "arr 𝖽[f]" and "dom 𝖽[f] = dom f" and "cod 𝖽[f] = cod f ⊗ cod f"
using assms dup_in_hom by auto

lemma dup_naturality:
assumes "«f : a → b»"
shows "𝖽[b] ⋅ f = (f ⊗ f) ⋅ 𝖽[a]"
using assms prod_def comp_arr_dom comp_cod_arr comp_tuple_arr comp_assoc
by fastforce

lemma pr_dup [simp]:
assumes "ide a"
shows "𝔭⇩0[a, a] ⋅ 𝖽[a] = a" and "𝔭⇩1[a, a] ⋅ 𝖽[a] = a"
using assms by simp_all

lemma prod_tuple:
assumes "span f g" and "seq h f" and "seq k g"
shows "(h ⊗ k) ⋅ ⟨f, g⟩ = ⟨h ⋅ f, k ⋅ g⟩"
using assms prod_def comp_assoc comp_tuple_arr by fastforce

lemma tuple_eqI:
assumes "ide b" and "ide c" and "seq 𝔭⇩0[b, c] f" and "seq 𝔭⇩1[b, c] f"
and "𝔭⇩0[b, c] ⋅ f = f0" and "𝔭⇩1[b, c] ⋅ f = f1"
shows "f = ⟨f1, f0⟩"
using assms pr_joint_monic [of b c "⟨f1, f0⟩" f] pr_tuple by auto

lemma tuple_expansion:
assumes "span f g"
shows "(f ⊗ g) ⋅ 𝖽[dom f] = ⟨f, g⟩"
using assms prod_tuple comp_arr_dom by simp

definition assoc ("𝖺[_, _, _]")
where "𝖺[a, b, c] ≡ ⟨𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩⟩"

definition assoc' ("𝖺⇧-⇧1[_, _, _]")
where "𝖺⇧-⇧1[a, b, c] ≡ ⟨⟨𝔭⇩1[a, b ⊗ c], 𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c]⟩, 𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c]⟩"

lemma assoc_in_hom [intro]:
assumes "ide a" and "ide b" and "ide c"
shows "«𝖺[a, b, c] : (a ⊗ b) ⊗ c → a ⊗ (b ⊗ c)»"
using assms assoc_def by auto

lemma assoc_simps [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "arr 𝖺[a, b, c]"
and "dom 𝖺[a, b, c] = (a ⊗ b) ⊗ c"
and "cod 𝖺[a, b, c] = a ⊗ (b ⊗ c)"
using assms assoc_in_hom by auto

lemma assoc'_in_hom [intro]:
assumes "ide a" and "ide b" and "ide c"
shows "«𝖺⇧-⇧1[a, b, c] : a ⊗ (b ⊗ c) → (a ⊗ b) ⊗ c»"
using assms assoc'_def by auto

lemma assoc'_simps [simp]:
assumes "ide a" and "ide b" and "ide c"
shows "arr 𝖺⇧-⇧1[a, b, c]"
and "dom 𝖺⇧-⇧1[a, b, c] = a ⊗ (b ⊗ c)"
and "cod 𝖺⇧-⇧1[a, b, c] = (a ⊗ b) ⊗ c"
using assms assoc'_in_hom by auto

lemma pr_assoc:
assumes "ide a" and "ide b" and "ide c"
shows "𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩0[a ⊗ b, c]"
and "𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]"
and "𝔭⇩1[a, b ⊗ c] ⋅ 𝖺[a, b, c] = 𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c]"
using assms assoc_def by force+

lemma pr_assoc':
assumes "ide a" and "ide b" and "ide c"
shows "𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝖺⇧-⇧1[a, b, c] = 𝔭⇩1[a, b ⊗ c]"
and "𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝖺⇧-⇧1[a, b, c] = 𝔭⇩1[b, c] ⋅ 𝔭⇩0[a, b ⊗ c]"
and "𝔭⇩0[a ⊗ b, c] ⋅ 𝖺⇧-⇧1[a, b, c] = 𝔭⇩0[b, c] ⋅ 𝔭⇩0[a, b ⊗ c]"
using assms assoc'_def by force+

lemma assoc_naturality:
assumes "«f0 : a0 → b0»" and "«f1 : a1 → b1»" and "«f2 : a2 → b2»"
shows "𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2) = (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"
proof -
have "𝔭⇩0[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2) =
𝔭⇩0[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"
proof -
have "𝔭⇩0[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2) =
(𝔭⇩0[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2]) ⋅ ((f0 ⊗ f1) ⊗ f2)"
using comp_assoc by simp
also have "... = ⟨𝔭⇩0[b0, b1] ⋅ 𝔭⇩1[b0 ⊗ b1, b2], 𝔭⇩0[b0 ⊗ b1, b2]⟩ ⋅ ((f0 ⊗ f1) ⊗ f2)"
using assms assoc_def by fastforce
also have "... = ⟨(𝔭⇩0[b0, b1] ⋅ 𝔭⇩1[b0 ⊗ b1, b2]) ⋅ ((f0 ⊗ f1) ⊗ f2),
𝔭⇩0[b0 ⊗ b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2)⟩"
using assms comp_tuple_arr by fastforce
also have "... = ⟨(𝔭⇩0[b0, b1] ⋅ (f0 ⊗ f1)) ⋅ 𝔭⇩1[a0 ⊗ a1, a2], f2 ⋅ 𝔭⇩0[a0 ⊗ a1, a2]⟩"
using assms comp_assoc by fastforce
also have "... = ⟨f1 ⋅ 𝔭⇩0[a0, a1] ⋅ 𝔭⇩1[a0 ⊗ a1, a2], f2 ⋅ 𝔭⇩0[a0 ⊗ a1, a2]⟩"
using assms comp_assoc
by (metis in_homE pr_naturality(1))
also have "... = 𝔭⇩0[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"
using assms comp_assoc assoc_def prod_tuple by fastforce
finally show ?thesis by blast
qed
moreover have "𝔭⇩1[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2) =
𝔭⇩1[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"
proof -
have "𝔭⇩1[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2) =
(𝔭⇩1[b0, b1 ⊗ b2] ⋅ 𝖺[b0, b1, b2]) ⋅ ((f0 ⊗ f1) ⊗ f2)"
using comp_assoc by simp
also have "... = (𝔭⇩1[b0, b1] ⋅ 𝔭⇩1[b0 ⊗ b1, b2]) ⋅ ((f0 ⊗ f1) ⊗ f2)"
using assms assoc_def by fastforce
also have "... = (𝔭⇩1[b0, b1] ⋅ (f0 ⊗ f1)) ⋅ 𝔭⇩1[a0 ⊗ a1, a2]"
using assms comp_assoc by fastforce
also have "... = f0 ⋅ 𝔭⇩1[a0, a1] ⋅ 𝔭⇩1[a0 ⊗ a1, a2]"
using assms comp_assoc
by (metis in_homE pr_naturality(2))
also have "... = 𝔭⇩1[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"
proof -
have "𝔭⇩1[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2] =
(𝔭⇩1[b0, b1 ⊗ b2] ⋅ (f0 ⊗ (f1 ⊗ f2))) ⋅ 𝖺[a0, a1, a2]"
using comp_assoc by simp
also have "... = f0 ⋅ 𝔭⇩1[a0, a1 ⊗ a2] ⋅ 𝖺[a0, a1, a2]"
using assms comp_assoc by fastforce
also have "... = f0 ⋅ 𝔭⇩1[a0, a1] ⋅ 𝔭⇩1[a0 ⊗ a1, a2]"
using assms assoc_def by fastforce
finally show ?thesis by simp
qed
finally show ?thesis by blast
qed
ultimately show ?thesis
using assms pr_joint_monic [of b0 "b1 ⊗ b2" "𝖺[b0, b1, b2] ⋅ ((f0 ⊗ f1) ⊗ f2)"
"(f0 ⊗ (f1 ⊗ f2)) ⋅ 𝖺[a0, a1, a2]"]
by fastforce
qed

lemma pentagon:
assumes "ide a" and "ide b" and "ide c" and "ide d"
shows "((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) = 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
proof (intro pr_joint_monic
[where h = "((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d)"
and h' = "𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"])
show "ide a" by fact
show "ide (b ⊗ (c ⊗ d))"
show "seq 𝔭⇩0[a, b ⊗ (c ⊗ d)] (((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d))"
using assms by simp
show "𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ ((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) =
𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
proof -
have "𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ ((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) =
((𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ (a ⊗ 𝖺[b, c, d])) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d)"
using comp_assoc by simp
also have "... = (𝔭⇩1[a, (b ⊗ c) ⊗ d] ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d)"
using assms pr_naturality(2) comp_cod_arr by force
also have "... = 𝔭⇩1[a, b ⊗ c] ⋅ 𝔭⇩1[a ⊗ b ⊗ c, d] ⋅ (𝖺[a, b, c] ⊗ d)"
using assms assoc_def comp_assoc by simp
also have "... = (𝔭⇩1[a, b ⊗ c] ⋅ 𝖺[a, b, c]) ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d]"
using assms pr_naturality(2) comp_assoc by fastforce
also have "... = 𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d]"
using assms assoc_def comp_assoc by simp
finally have "𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ ((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) =
𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d]"
by blast
also have "... = 𝔭⇩1[a, b ⊗ c ⊗ d] ⋅ 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
using assms assoc_def comp_assoc by auto
finally show ?thesis by blast
qed
show "𝔭⇩0[a, b ⊗ (c ⊗ d)] ⋅ ((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) =
𝔭⇩0[a, b ⊗ (c ⊗ d)] ⋅ 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
proof -
have "𝔭⇩0[a, b ⊗ (c ⊗ d)] ⋅ ((a ⊗ 𝖺[b, c, d]) ⋅ 𝖺[a, b ⊗ c, d]) ⋅ (𝖺[a, b, c] ⊗ d) =
𝔭⇩0[a, b ⊗ c ⊗ d] ⋅
((a ⊗ ⟨𝔭⇩1[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], ⟨𝔭⇩0[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], 𝔭⇩0[b ⊗ c, d]⟩⟩) ⋅
⟨𝔭⇩1[a, b ⊗ c] ⋅ 𝔭⇩1[a ⊗ b ⊗ c, d],
⟨𝔭⇩0[a, b ⊗ c] ⋅ 𝔭⇩1[a ⊗ b ⊗ c, d], 𝔭⇩0[a ⊗ b ⊗ c, d]⟩⟩) ⋅
(⟨𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩⟩ ⊗ d)"
using assms assoc_def by simp
also have "... = ⟨𝔭⇩1[b, c] ⋅ 𝔭⇩1[b ⊗ c, d],
⟨𝔭⇩0[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], 𝔭⇩0[b ⊗ c, d]⟩⟩ ⋅ (𝔭⇩0[a, (b ⊗ c) ⊗ d] ⋅
⟨𝔭⇩1[a, b ⊗ c] ⋅ 𝔭⇩1[a ⊗ b ⊗ c, d],
⟨𝔭⇩0[a, b ⊗ c] ⋅ 𝔭⇩1[a ⊗ b ⊗ c, d], 𝔭⇩0[a ⊗ b ⊗ c, d]⟩⟩) ⋅
(⟨𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c],
⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩⟩ ⊗ d)"
proof -
have "𝔭⇩0[a, b ⊗ c ⊗ d] ⋅
(a ⊗ ⟨𝔭⇩1[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], ⟨𝔭⇩0[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], 𝔭⇩0[b ⊗ c, d]⟩⟩) =
⟨𝔭⇩1[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], ⟨𝔭⇩0[b, c] ⋅ 𝔭⇩1[b ⊗ c, d], 𝔭⇩0[b ⊗ c, d]⟩⟩ ⋅
𝔭⇩0[a, (b ⊗ c) ⊗ d]"
using assms assoc_def ide_in_hom pr_naturality(1) by auto
thus ?thesis using comp_assoc by metis
qed
also have "... = ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d],
⟨𝔭⇩0[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d], d ⋅ 𝔭⇩0[(a ⊗ b) ⊗ c, d]⟩⟩"
using assms comp_assoc by simp
also have "... = ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d],
⟨𝔭⇩0[a ⊗ b, c] ⋅ 𝔭⇩1[(a ⊗ b) ⊗ c, d], 𝔭⇩0[(a ⊗ b) ⊗ c, d]⟩⟩"
using assms comp_cod_arr by simp
also have "... = 𝔭⇩0[a, b ⊗ (c ⊗ d)] ⋅ 𝖺[a, b, c ⊗ d] ⋅ 𝖺[a ⊗ b, c, d]"
using assms assoc_def comp_assoc by simp
finally show ?thesis by simp
qed
qed

lemma inverse_arrows_assoc:
assumes "ide a" and "ide b" and "ide c"
shows "inverse_arrows 𝖺[a, b, c] 𝖺⇧-⇧1[a, b, c]"
using assms assoc_def assoc'_def comp_assoc

lemma inv_prod:
assumes "iso f" and "iso g"
shows "iso (prod f g)"
and "inv (prod f g) = prod (inv f) (inv g)"
proof -
have 1: "inverse_arrows (prod f g) (prod (inv f) (inv g))"
by (auto simp add: assms comp_inv_arr' comp_arr_inv' iso_is_arr interchange)
show "iso (prod f g)"
using 1 by blast
show "inv (prod f g) = prod (inv f) (inv g)"
using 1 by (simp add: inverse_unique)
qed

interpretation CC: product_category C C ..

abbreviation Prod
where "Prod fg ≡ fst fg ⊗ snd fg"
abbreviation Prod'
where "Prod' fg ≡ snd fg ⊗ fst fg"

interpretation Π: binary_functor C C C Prod
using tuple_ext CC.comp_char interchange
apply unfold_locales
apply auto
by (metis prod_def seqE)+

interpretation Prod': binary_functor C C C Prod'
using tuple_ext CC.comp_char interchange
apply unfold_locales
apply auto
by (metis prod_def seqE)+

lemma binary_functor_Prod:
shows "binary_functor C C C Prod" and "binary_functor C C C Prod'"
..

interpretation CCC: product_category C CC.comp ..
interpretation T: binary_endofunctor C Prod ..
interpretation ToTC: "functor" CCC.comp C T.ToTC
using T.functor_ToTC by auto
interpretation ToCT: "functor" CCC.comp C T.ToCT
using T.functor_ToCT by auto

abbreviation α
where "α f ≡ 𝖺[cod (fst f), cod (fst (snd f)), cod (snd (snd f))] ⋅
((fst f ⊗ fst (snd f)) ⊗ snd (snd f))"

lemma α_simp_ide:
assumes "CCC.ide a"
shows "α a = 𝖺[fst a, fst (snd a), snd (snd a)]"
using assms comp_arr_dom by auto

interpretation α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α
proof
fix f
show "¬ CCC.arr f ⟹ α f = null"
by (metis CC.arr_char CCC.arr_char ext prod_def seqE tuple_ext)
assume f: "CCC.arr f"
show "dom (α f) = T.ToTC (CCC.dom f)"
using f by auto
show "cod (α f) = T.ToCT (CCC.cod f)"
using f by auto
show "T.ToCT f ⋅ α (CCC.dom f) = α f"
using f T.ToCT_def T.ToTC_def comp_assoc
assoc_naturality
[of "fst f" "dom (fst f)" "cod (fst f)"
"fst (snd f)" "dom (fst (snd f))" "cod (fst (snd f))"
"snd (snd f)" "dom (snd (snd f))" "cod (snd (snd f))"]
show "α (CCC.cod f) ⋅ T.ToTC f = α f"
using T.ToTC_def comp_arr_dom f by auto
next
show "⋀a. CCC.ide a ⟹ iso (α a)"
using CCC.ide_char⇩P⇩C CC.ide_char⇩P⇩C comp_arr_dom inverse_arrows_assoc isoI
by (metis assoc_simps(1-2) ideD(3))
qed

lemma α_is_natural_isomorphism:
shows "natural_isomorphism CCC.comp C T.ToTC T.ToCT α"
..

definition sym ("𝗌[_, _]")
where "𝗌[a1, a0] ≡ if ide a0 ∧ ide a1 then ⟨𝔭⇩0[a1, a0], 𝔭⇩1[a1, a0]⟩ else null"

lemma sym_in_hom [intro]:
assumes "ide a" and "ide b"
shows "«𝗌[a, b] : a ⊗ b → b ⊗ a»"
using assms sym_def by auto

lemma sym_simps [simp]:
assumes "ide a" and "ide b"
shows "arr 𝗌[a, b]" and "dom 𝗌[a, b] = a ⊗ b" and "cod 𝗌[a, b] = b ⊗ a"
using assms sym_in_hom by auto

lemma comp_sym_tuple [simp]:
assumes "«f0 : a → b0»" and "«f1 : a → b1»"
shows "𝗌[b0, b1] ⋅ ⟨f0, f1⟩ = ⟨f1, f0⟩"
using assms sym_def comp_tuple_arr by fastforce

lemma prj_sym [simp]:
assumes "ide a0" and "ide a1"
shows "𝔭⇩0[a1, a0] ⋅ 𝗌[a0, a1] = 𝔭⇩1[a0, a1]"
and "𝔭⇩1[a1, a0] ⋅ 𝗌[a0, a1] = 𝔭⇩0[a0, a1]"
using assms sym_def by auto

lemma comp_sym_sym [simp]:
assumes "ide a0" and "ide a1"
shows "𝗌[a1, a0] ⋅ 𝗌[a0, a1] = (a0 ⊗ a1)"
using assms sym_def comp_tuple_arr by auto

lemma sym_inverse_arrows:
assumes "ide a0" and "ide a1"
shows "inverse_arrows 𝗌[a0, a1] 𝗌[a1, a0]"
using assms sym_in_hom comp_sym_sym by auto

lemma sym_assoc_coherence:
assumes "ide a" and "ide b" and "ide c"
shows "𝖺[b, c, a] ⋅ 𝗌[a, b ⊗ c] ⋅ 𝖺[a, b, c] = (b ⊗ 𝗌[a, c]) ⋅ 𝖺[b, a, c] ⋅ (𝗌[a, b] ⊗ c)"
using assms sym_def assoc_def comp_assoc prod_tuple comp_cod_arr by simp

lemma sym_naturality:
assumes "«f0 : a0 → b0»" and "«f1 : a1 → b1»"
shows "𝗌[b0, b1] ⋅ (f0 ⊗ f1) = (f1 ⊗ f0) ⋅ 𝗌[a0, a1]"
using assms sym_def comp_assoc prod_tuple by fastforce

abbreviation σ
where "σ fg ≡ 𝗌[cod (fst fg), cod (snd fg)] ⋅ (fst fg ⊗ snd fg)"

interpretation σ: natural_transformation CC.comp C Prod Prod' σ
using sym_def CC.arr_char CC.null_char comp_arr_dom comp_cod_arr
apply unfold_locales
apply auto
using arr_cod_iff_arr ideD(1)
apply metis
using arr_cod_iff_arr ideD(1)
apply metis
using prod_tuple by simp

lemma σ_is_natural_transformation:
shows "natural_transformation CC.comp C Prod Prod' σ"
..

abbreviation Diag
where "Diag f ≡ if arr f then (f, f) else CC.null"

interpretation Δ: "functor" C CC.comp Diag
by (unfold_locales, auto)

lemma functor_Diag:
shows "functor C CC.comp Diag"
..

interpretation ΔoΠ: composite_functor CC.comp C CC.comp Prod Diag ..
interpretation ΠoΔ: composite_functor C CC.comp C Diag Prod ..

abbreviation π
where "π ≡ λ(f, g). (𝔭⇩1[cod f, cod g] ⋅ (f ⊗ g), 𝔭⇩0[cod f, cod g] ⋅ (f ⊗ g))"

interpretation π: transformation_by_components CC.comp CC.comp ΔoΠ.map CC.map π
using pr_naturality comp_arr_dom comp_cod_arr
by unfold_locales auto

lemma π_is_natural_transformation:
shows "natural_transformation CC.comp CC.comp ΔoΠ.map CC.map π"
proof -
have "π.map = π"
using π.map_def ext Π.is_extensional comp_arr_dom comp_cod_arr by auto
thus "natural_transformation CC.comp CC.comp ΔoΠ.map CC.map π"
using π.natural_transformation_axioms by simp
qed

interpretation δ: natural_transformation C C map ΠoΔ.map dup
using dup_naturality comp_arr_dom comp_cod_arr prod_tuple tuple_ext
by unfold_locales auto

lemma dup_is_natural_transformation:
shows "natural_transformation C C map ΠoΔ.map dup"
..

interpretation ΔoΠoΔ: composite_functor C CC.comp CC.comp Diag ΔoΠ.map ..
interpretation ΠoΔoΠ: composite_functor CC.comp C C Prod ΠoΔ.map ..

interpretation Δoδ: natural_transformation C CC.comp Diag ΔoΠoΔ.map ‹Diag ∘ dup›
proof -
have "Diag ∘ map = Diag"
by auto
thus "natural_transformation C CC.comp Diag ΔoΠoΔ.map (Diag ∘ dup)"
using Δ.as_nat_trans.natural_transformation_axioms δ.natural_transformation_axioms
o_assoc horizontal_composite [of C C map ΠoΔ.map dup CC.comp Diag Diag Diag]
by metis
qed

interpretation δoΠ: natural_transformation CC.comp C Prod ΠoΔoΠ.map ‹dup ∘ Prod›
using δ.natural_transformation_axioms Π.as_nat_trans.natural_transformation_axioms
o_assoc horizontal_composite [of CC.comp C Prod Prod Prod C map ΠoΔ.map dup]
by simp

interpretation πoΔ: natural_transformation C CC.comp ΔoΠoΔ.map Diag ‹π.map ∘ Diag›
using π.natural_transformation_axioms Δ.as_nat_trans.natural_transformation_axioms
horizontal_composite
[of C CC.comp Diag Diag Diag CC.comp ΔoΠ.map CC.map π.map]
by simp

interpretation Πoπ: natural_transformation CC.comp C ΠoΔoΠ.map Prod ‹Prod ∘ π.map›
proof -
have "Prod ∘ ΔoΠ.map = ΠoΔoΠ.map"
by auto
thus "natural_transformation CC.comp C ΠoΔoΠ.map Prod (Prod ∘ π.map)"
using π.natural_transformation_axioms Π.as_nat_trans.natural_transformation_axioms
o_assoc
horizontal_composite
[of CC.comp CC.comp ΔoΠ.map CC.map π.map C Prod Prod Prod]
by simp
qed

interpretation Δoδ_πoΔ: vertical_composite C CC.comp Diag ΔoΠoΔ.map Diag
‹Diag ∘ dup› ‹π.map ∘ Diag›
..
interpretation Πoπ_δoΠ: vertical_composite CC.comp C Prod ΠoΔoΠ.map Prod
‹dup ∘ Prod› ‹Prod ∘ π.map›
..

interpretation ΔΠ: unit_counit_adjunction CC.comp C Diag Prod dup π.map
proof
show "Δoδ_πoΔ.map = Diag"
proof
fix f
have "¬ arr f ⟹ Δoδ_πoΔ.map f = Diag f"
moreover have "arr f ⟹ Δoδ_πoΔ.map f = Diag f"
using comp_cod_arr comp_assoc Δoδ_πoΔ.map_def by auto
ultimately show "Δoδ_πoΔ.map f = Diag f" by blast
qed
show "Πoπ_δoΠ.map = Prod"
proof
fix fg
show "Πoπ_δoΠ.map fg = Prod fg"
proof -
have "¬ CC.arr fg ⟹ ?thesis"
moreover have "CC.arr fg ⟹ ?thesis"
proof -
assume fg: "CC.arr fg"
have 1: "dup (Prod fg) = ⟨cod (fst fg) ⊗ cod (snd fg), cod (fst fg) ⊗ cod (snd fg)⟩ ⋅
(fst fg ⊗ snd fg)"
using fg δ.is_natural_2
apply simp
by (metis (no_types, lifting) prod_simps(1) prod_simps(3))
have "Πoπ_δoΠ.map fg =
(𝔭⇩1[cod (fst fg), cod (snd fg)] ⊗ 𝔭⇩0[cod (fst fg), cod (snd fg)]) ⋅
⟨cod (fst fg) ⊗ cod (snd fg), cod (fst fg) ⊗ cod (snd fg)⟩ ⋅
(fst fg ⊗ snd fg)"
using fg 1 Πoπ_δoΠ.map_def comp_cod_arr by simp
also have "... = ((𝔭⇩1[cod (fst fg), cod (snd fg)] ⊗ 𝔭⇩0[cod (fst fg), cod (snd fg)]) ⋅
⟨cod (fst fg) ⊗ cod (snd fg), cod (fst fg) ⊗ cod (snd fg)⟩) ⋅
(fst fg ⊗ snd fg)"
using comp_assoc by simp
also have "... = ⟨𝔭⇩1[cod (fst fg), cod (snd fg)] ⋅ (cod (fst fg) ⊗ cod (snd fg)),
𝔭⇩0[cod (fst fg), cod (snd fg)] ⋅ (cod (fst fg) ⊗ cod (snd fg))⟩ ⋅
(fst fg ⊗ snd fg)"
using fg prod_tuple by simp
also have "... = Prod fg"
using fg comp_arr_dom Π.as_nat_trans.is_natural_2 by auto
finally show ?thesis by simp
qed
ultimately show ?thesis by blast
qed
qed
qed

shows "unit_counit_adjunction CC.comp C Diag Prod dup π.map"

end

section "Category with Terminal Object"

locale category_with_terminal_object =
category +
assumes has_terminal: "∃t. terminal t"

locale elementary_category_with_terminal_object =
category C
for C :: "'a comp"                              (infixr "⋅" 55)
and one :: "'a"                                 ("𝟭")
and trm :: "'a ⇒ 'a"                           ("𝗍[_]") +
assumes ide_one: "ide 𝟭"
and trm_in_hom [intro, simp]: "ide a ⟹ «𝗍[a] : a → 𝟭»"
and trm_eqI: "⟦ ide a; «f : a → 𝟭» ⟧ ⟹ f = 𝗍[a]"
begin

lemma trm_simps [simp]:
assumes "ide a"
shows "arr 𝗍[a]" and "dom 𝗍[a] = a" and "cod 𝗍[a] = 𝟭"
using assms trm_in_hom by blast+

lemma trm_one:
shows "𝗍[𝟭] = 𝟭"
using ide_one trm_eqI ide_in_hom by auto

lemma terminal_one:
shows "terminal 𝟭"
using ide_one trm_in_hom trm_eqI terminal_def by metis

lemma trm_naturality:
assumes "arr f"
shows "𝗍[cod f] ⋅ f = 𝗍[dom f]"
using assms trm_eqI
by (metis comp_in_homI' ide_cod ide_dom in_homE trm_in_hom)

sublocale category_with_terminal_object C
apply unfold_locales
using terminal_one by auto

proposition is_category_with_terminal_object:
shows "category_with_terminal_object C"
..

definition τ
where "τ = (λf. if arr f then trm (dom f) else null)"

lemma τ_in_hom [intro, simp]:
assumes "arr f"
shows "«τ f : dom f → 𝟭»"

lemma τ_simps [simp]:
assumes "arr f"
shows "arr (τ f)" and "dom (τ f) = dom f" and "cod (τ f) = 𝟭"
using assms by (auto simp add: τ_def assms)

sublocale Ω: constant_functor C C 𝟭
using ide_one
by unfold_locales auto

sublocale τ: natural_transformation C C map Ω.map τ
unfolding τ_def
using trm_simps(1-3) comp_cod_arr trm_naturality
by unfold_locales auto

end

context category_with_terminal_object
begin

definition some_terminal ("𝟭⇧?")
where "some_terminal ≡ SOME t. terminal t"

definition "some_terminator" ("𝗍⇧?[_]")
where "𝗍⇧?[f] ≡ if arr f then THE t. «t : dom f → 𝟭⇧?» else null"

lemma terminal_some_terminal [intro]:
shows "terminal 𝟭⇧?"
using some_terminal_def has_terminal someI_ex [of "λt. terminal t"] by presburger

lemma ide_some_terminal:
shows "ide 𝟭⇧?"
using terminal_def by blast

lemma some_trm_in_hom [intro]:
assumes "arr f"
shows "«𝗍⇧?[f] : dom f → 𝟭⇧?»"
proof -
have "ide (dom f)" using assms by fastforce
hence "∃!t. «t : dom f → 𝟭⇧?»"
using assms some_terminator_def terminal_def terminal_some_terminal by simp
thus ?thesis
using assms some_terminator_def [of f] theI' [of "λt. «t : dom f → 𝟭⇧?»"] by auto
qed

lemma some_trm_simps [simp]:
assumes "arr f"
shows "arr 𝗍⇧?[f]" and "dom 𝗍⇧?[f] = dom f" and "cod 𝗍⇧?[f] = 𝟭⇧?"
using assms some_trm_in_hom by auto

lemma some_trm_eqI:
assumes "«t : dom f → 𝟭⇧?»"
shows "t = 𝗍⇧?[f]"
proof -
have "ide (dom f)" using assms
by (metis ide_dom in_homE)
hence "∃!t. «t : dom f → 𝟭⇧?»"
using terminal_def [of "𝟭⇧?"] terminal_some_terminal by auto
moreover have "«t : dom f → 𝟭⇧?»"
using assms by simp
ultimately show ?thesis
using assms some_terminator_def the1_equality [of "λt. «t : dom f → 𝟭⇧?»" t]
‹ide (dom f)› arr_dom_iff_arr
by fastforce
qed

proposition extends_to_elementary_category_with_terminal_object:
shows "elementary_category_with_terminal_object C 𝟭⇧? (λa. 𝗍⇧?[a])"
using ide_some_terminal some_trm_eqI
by unfold_locales auto

end

section "Cartesian Category"

locale cartesian_category =
category_with_binary_products +
category_with_terminal_object

locale category_with_pullbacks_and_terminal_object =
category_with_pullbacks +
category_with_terminal_object
begin

sublocale category_with_binary_products C
proof
interpret elementary_category_with_terminal_object C ‹𝟭⇧?› ‹λa. 𝗍⇧?[a]›
using extends_to_elementary_category_with_terminal_object by blast
show "has_binary_products"
proof -
have "⋀a0 a1. ⟦ide a0; ide a1⟧ ⟹ ∃p0 p1. has_as_binary_product a0 a1 p0 p1"
proof -
fix a0 a1
assume a0: "ide a0" and a1: "ide a1"
obtain p0 p1 where p0p1: "has_as_pullback 𝗍⇧?[a0] 𝗍⇧?[a1] p0 p1"
using a0 a1 has_pullbacks has_pullbacks_def by force
have "has_as_binary_product a0 a1 p0 p1"
proof
show "ide a0" and "ide a1"
using a0 a1 by auto
show "«p0 : dom p1 → a0»" and "«p1 : dom p1 → a1»"
using p0p1 a0 a1 commutative_squareE has_as_pullbackE in_homI trm_simps(2)
by metis+
fix x f g
assume f: "«f : x → a0»" and g: "«g : x → a1»"
have "commutative_square 𝗍⇧?[a0] 𝗍⇧?[a1] f g"
by (metis a0 has_as_pullbackE in_homE commutative_squareI f g p0p1 trm_naturality
trm_simps(2))
moreover have "⋀l. p0 ⋅ l = f ∧ p1 ⋅ l = g ⟹ «l : x → dom p1»"
using f g by blast
ultimately show "∃!l. «l : x → dom p1» ∧ p0 ⋅ l = f ∧ p1 ⋅ l = g"
by (metis has_as_pullbackE p0p1)
qed
thus "∃p0 p1. has_as_binary_product a0 a1 p0 p1"
by auto
qed
thus ?thesis
using has_binary_products_def by force
qed
qed

sublocale cartesian_category C ..

end

locale elementary_cartesian_category =
elementary_category_with_binary_products +
elementary_category_with_terminal_object
begin

sublocale cartesian_category C
using cartesian_category.intro is_category_with_binary_products
is_category_with_terminal_object
by auto

proposition is_cartesian_category:
shows "cartesian_category C"
..

end

context cartesian_category
begin

proposition extends_to_elementary_cartesian_category:
shows "elementary_cartesian_category C some_pr0 some_pr1 𝟭⇧? (λa. 𝗍⇧?[a])"
extends_to_elementary_category_with_terminal_object
extends_to_elementary_category_with_binary_products)

end

subsection "Monoidal Structure"

text ‹
Here we prove some facts that will later allow us to show that an elementary cartesian
category is a monoidal category.
›

context elementary_cartesian_category
begin

abbreviation ι
where "ι ≡ 𝔭⇩0[𝟭, 𝟭]"

lemma pr_coincidence:
shows "ι = 𝔭⇩1[𝟭, 𝟭]"
using ide_one

lemma unit_is_terminal_arr:
shows "terminal_arr ι"
using ide_one

lemma unit_eq_trm:
shows "ι = 𝗍[𝟭 ⊗ 𝟭]"
by (metis unit_is_terminal_arr cod_pr1 comp_cod_arr pr_simps(5) trm_naturality ide_one
pr_coincidence trm_one)

lemma inverse_arrows_ι:
shows "inverse_arrows ι ⟨𝟭, 𝟭⟩"
using ide_one
by (metis unit_is_terminal_arr cod_pr0 comp_tuple_arr ide_char ide_dom inverse_arrows_def
prod_def pr_coincidence pr_dup(2) pr_simps(2))

lemma ι_is_iso:
shows "iso ι"
using inverse_arrows_ι by auto

lemma trm_tensor:
assumes "ide a" and "ide b"
shows "𝗍[a ⊗ b] = ι ⋅ (𝗍[a] ⊗ 𝗍[b])"
using assms unit_is_terminal_arr terminal_arr_unique ide_one

abbreviation runit ("𝗋[_]")
where "𝗋[a] ≡ 𝔭⇩1[a, 𝟭]"

abbreviation runit' ("𝗋⇧-⇧1[_]")
where "𝗋⇧-⇧1[a] ≡ ⟨a, 𝗍[a]⟩"

abbreviation lunit ("𝗅[_]")
where