(* 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" by (simp add: assms(5) 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. › (* 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 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 "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 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 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 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 → 𝟭»" by (simp add: τ_def assms) 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])" by (simp add: elementary_cartesian_category_def 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 by (simp add: terminal_arr_unique terminal_one) lemma unit_is_terminal_arr: shows "terminal_arr ι" using ide_one by (simp add: terminal_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 by (simp add: unit_eq_trm) abbreviation runit ("𝗋[_]") where "𝗋[a] ≡ 𝔭⇩_{1}[a, 𝟭]" abbreviation runit' ("𝗋⇧^{-}⇧^{1}[_]") where "𝗋⇧^{-}⇧^{1}[a] ≡ ⟨a, 𝗍[a]⟩" abbreviation lunit ("𝗅[_]") where