Theory CartesianCategory
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 "span p q" and "cod p = a" and "cod q = b"
and "⋀x f g. ⟦«f : x → a»; «g : x → b»⟧ ⟹ ∃!h. «h : x → dom p» ∧ 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 a: "ide a"
using assms by auto
show b: "ide b"
using assms by auto
let ?c = "dom p"
interpret J: binary_product_shape .
interpret D: binary_product_diagram C a b
using a b by unfold_locales auto
show "D.has_as_binary_product p q"
proof -
have 1: "D.is_rendered_commutative_by p q"
using assms a b 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(4) [of "χ' J.FF" x "χ' J.TT"] by simp
qed
have 3: "D.is_rendered_commutative_by (χ' J.FF) (χ' J.TT)"
using a b 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
apply (cases "J.ide j")
by (metis (no_types, lifting))+
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"
by (simp add: assms(4) in_homI)
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
by (simp add: binary_product_diagram.intro binary_product_diagram_axioms.intro
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.
›
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
by (simp add: assms)
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 "span 𝔭⇩1[a, b] 𝔭⇩0[a, b]" and "cod 𝔭⇩1[a, b] = a" and "cod 𝔭⇩0[a, b] = b"
using assms by auto
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
lemma (in category) elementary_category_with_binary_productsI:
assumes "⋀a b. ⟦ide a; ide b⟧ ⟹ has_as_binary_product a b (p a b) (q a b)"
shows "elementary_category_with_binary_products C
(λa b. if ide a ∧ ide b then q a b else null)
(λa b. if ide a ∧ ide b then p a b else null)"
proof -
let ?p = "λa b. if ide a ∧ ide b then p a b else null"
let ?q = "λa b. if ide a ∧ ide b then q a b else null"
show ?thesis
proof
fix a b
assume a: "ide a" and b: "ide b"
show "span (?p a b) (?q a b)"
using assms a b
by auto force
show "cod (?q a b) = b"
using a b assms has_as_binary_productE by auto
show "cod (?p a b) = a"
using a b assms has_as_binary_productE by auto
next
fix f g
assume fg: "span f g"
have 1: "has_as_binary_product (cod f) (cod g)
(p (cod f) (cod g)) (q (cod f) (cod g))"
using assms fg by simp
obtain l where "p (cod f) (cod g) ⋅ l = f ∧ q (cod f) (cod g) ⋅ l = g"
using 1 fg has_as_binary_productE
by (metis in_homI)
hence "∃l. ?p (cod f) (cod g) ⋅ l = f ∧ ?q (cod f) (cod g) ⋅ l = g"
using fg by auto
moreover have
"⋀l l'. ?p (cod f) (cod g) ⋅ l = f ∧ ?q (cod f) (cod g) ⋅ l = g ∧
?p (cod f) (cod g) ⋅ l' = f ∧ ?q (cod f) (cod g) ⋅ l' = g
⟹ l = l'"
using 1 fg arr_iff_in_hom ide_cod
by (elim has_as_binary_productE, auto) metis
ultimately show "∃!l. ?p (cod f) (cod g) ⋅ l = f ∧ ?q (cod f) (cod g) ⋅ l = g"
by blast
qed
qed
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
by (simp add: has_as_binary_product_def)
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
locale binary_product =
category C
for C :: "'a comp"
and a :: 'a
and b :: 'a
and p :: 'a
and q :: 'a +
assumes has_as_binary_product: "has_as_binary_product a b p q"
begin
definition product
where "product ≡ dom p"
lemma ide_product [intro, simp]:
shows "ide product"
unfolding product_def
using has_as_binary_product by fastforce
lemma prj_in_hom [intro, simp]:
shows "«p : product → a»"
and "«q : product → b»"
using has_as_binary_product product_def by auto
lemma prj_simps [simp]:
shows "dom p = product" and "cod p = a" and "dom q = product" and "cod q = b"
using prj_in_hom by blast+
definition tuple
where "tuple f g ≡ (THE h. C p h = f ∧ C q h = g)"
lemma tuple_props:
assumes "span f g" and "cod f = a" and "cod g = b"
shows [intro, simp]: "«tuple f g : dom f → product»"
and [simp]: "dom (tuple f g) = dom f"
and [simp]: "cod (tuple f g) = product"
and [simp]: "C p (tuple f g) = f"
and [simp]: "C q (tuple f g) = g"
and "⋀h. ⟦C p h = f; C q h = g⟧ ⟹ h = tuple f g"
proof -
have 0: "∃!h. C p h = f ∧ C q h = g"
using assms has_as_binary_product by blast
hence *: "C p (tuple f g) = f ∧ C q (tuple f g) = g"
using tuple_def theI' [of "λh. C p h = f ∧ C q h = g"] by simp
show 1: "«tuple f g : dom f → product»"
using assms *
by (metis dom_comp in_homI prj_simps(3) seqE)
show "dom (tuple f g) = dom f"
using 1 by auto
show "cod (tuple f g) = product"
using 1 by auto
show 2: "C p (tuple f g) = f"
using * by auto
show 3: "C q (tuple f g) = g"
using * by auto
show 4: "⋀h. ⟦C p h = f; C q h = g⟧ ⟹ h = tuple f g"
using * 0 2 3 by blast
qed
lemma tuple_proj:
shows [simp]: "tuple p q = product"
by (metis comp_arr_dom in_homE tuple_props(6) prj_in_hom(1-2))
lemma pr_joint_monic:
assumes "seq p x" and "seq p y" and "C p x = C p y" and "C q x = C q y"
shows "x = y"
by (metis (mono_tags, lifting) assms(1,3-4) cod_comp dom_comp tuple_props(6)
product_def arrI prj_in_hom(2) prj_simps(2-4) seqE seqI)
end
lemma (in category) binary_products_are_isomorphic:
assumes "has_as_binary_product a b p q" and "has_as_binary_product a b p' q'"
shows "isomorphic (dom p) (dom p')"
and "inverse_arrows (binary_product.tuple C p q p' q')
(binary_product.tuple C p' q' p q)"
proof -
show "isomorphic (dom p) (dom p')"
using assms limits_are_isomorphic(1)
unfolding has_as_binary_product_def by blast
interpret pq: binary_product C a b p q
using assms(1) by unfold_locales auto
interpret p'q': binary_product C a b p' q'
using assms(2) by unfold_locales auto
show "inverse_arrows (pq.tuple p' q') (p'q'.tuple p q)"
proof
show "ide (p'q'.tuple p q ⋅ pq.tuple p' q')"
proof -
have "p' ⋅ p'q'.tuple p q ⋅ pq.tuple p' q' = p' ⋅ p'q'.product ∧
q' ⋅ p'q'.tuple p q ⋅ pq.tuple p' q' = q' ⋅ p'q'.product"
using pq.tuple_props [of p' q'] p'q'.tuple_props [of p q]
comp_assoc
by (metis arrI comp_arr_dom p'q'.prj_in_hom(1-2) p'q'.prj_simps(2-4)
p'q'.product_def pq.prj_in_hom(1-2) pq.prj_simps(2-4) pq.product_def)
thus ?thesis
by (metis comp_arr_dom p'q'.ide_product p'q'.tuple_props(6)
p'q'.prj_in_hom(1-2) p'q'.prj_simps(1-4) arrI)
qed
show "ide (pq.tuple p' q' ⋅ p'q'.tuple p q)"
proof -
have "p ⋅ pq.tuple p' q' ⋅ p'q'.tuple p q = p ⋅ pq.product ∧
q ⋅ pq.tuple p' q' ⋅ p'q'.tuple p q = q ⋅ pq.product"
using pq.tuple_props [of p' q'] p'q'.tuple_props [of p q]
comp_assoc
by (metis arrI comp_arr_dom p'q'.prj_in_hom(1-2) p'q'.prj_simps(2-4)
p'q'.product_def pq.prj_in_hom(1-2) pq.prj_simps(2-4)
pq.product_def)
thus ?thesis
by (metis arrI comp_arr_dom ide_char' pq.tuple_props(6) pq.prj_in_hom(1-2)
pq.prj_simps(2-4) pq.product_def seqE)
qed
qed
qed
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))"
by (simp add: assms(2-4))
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
by (auto simp add: tuple_pr_arr)
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))"]
by (simp add: comp_arr_dom in_homI)
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"
by (simp add: Δoδ_πoΔ.is_extensional)
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"
by (simp add: Π.is_extensional Πoπ_δoΠ.is_extensional)
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
proposition induces_unit_counit_adjunction:
shows "unit_counit_adjunction CC.comp C Diag Prod dup π.map"
using ΔΠ.unit_counit_adjunction_axioms by simp
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