diff --git a/thys/Category3/CartesianCategory.thy b/thys/Category3/CartesianCategory.thy --- a/thys/Category3/CartesianCategory.thy +++ b/thys/Category3/CartesianCategory.thy @@ -1,2444 +1,2444 @@ (* Title: CartesianCategory Author: Eugene W. Stark , 2020 Maintainer: Eugene W. Stark *) 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\<^sub>C\<^sub>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 "\\<^sub>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 \\<^sub>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" using cone_mkCone mkCone_def J.arr_char J.ide_char is_rendered_commutative_by_cone apply (intro iffI) apply (metis (no_types, lifting) C.cod_eqI C.comp_ide_arr J.arr.inject is_discrete) by auto lemma cones_map_mkCone_eq_iff: assumes "is_rendered_commutative_by p0 p1" and "is_rendered_commutative_by p0' p1'" and "\h : C.dom p0' \ C.dom p0\" shows "cones_map h (mkCone p0 p1) = mkCone p0' p1' \ p0 \ h = p0' \ p1 \ h = p1'" proof - interpret \: cone J.comp C map \C.dom p0\ \mkCone p0 p1\ using assms(1) cone_mkCone [of p0 p1] by blast interpret \': cone J.comp C map \C.dom p0'\ \mkCone p0' p1'\ using assms(2) cone_mkCone [of p0' p1'] by blast show ?thesis proof assume 3: "cones_map h (mkCone p0 p1) = mkCone p0' p1'" show "p0 \ h = p0' \ p1 \ h = p1'" proof show "p0 \ h = p0'" proof - have "p0' = cones_map h (mkCone p0 p1) J.FF" using 3 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 3 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 cone_\ by force also have "... = p0'" proof - have "D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1')) (D.mkCone p0 p1) = D.mkCone p0' p1'" using cone induced_arrowI by blast thus ?thesis using J.arr_char D.mkCone_def by simp qed finally show ?thesis by auto qed show "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 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 2: "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 2 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 1: "\!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 1 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 2 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") apply auto[1] by auto qed qed moreover have "\h'. \h' : x \ c\ \ D.cones_map h' (D.mkCone p q) = \' \ h' = h" proof - fix h' assume 1: "\h' : x \ c\ \ D.cones_map h' (D.mkCone p q) = \'" have "\!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 h assms(5) [of "\' J.FF" x "\' J.TT"] J.ide_char by auto qed 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 1 \.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 3: "\!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 3 by blast have "p \ l = f \ q \ l = g" 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 "p \ l = f" by blast 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 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 \\\<^sub>1[a, b]\ and \\\<^sub>0[a, b]\ that comprise a universal span. It is useful to assume that the mappings that produce \\\<^sub>1[a, b]\ and \\\<^sub>0[a, b]\ from \a\ and \b\ are extensional; that is, if either \a\ or \b\ is not an identity, then \\\<^sub>1[a, b]\ and \\\<^sub>0[a, b]\ are \null\. \ locale elementary_category_with_binary_products = category C for C :: "'a comp" (infixr "\" 55) and pr0 :: "'a \ 'a \ 'a" ("\\<^sub>0[_, _]") and pr1 :: "'a \ 'a \ 'a" ("\\<^sub>1[_, _]") + assumes pr0_ext: "\ (ide a \ ide b) \ \\<^sub>0[a, b] = null" and pr1_ext: "\ (ide a \ ide b) \ \\<^sub>1[a, b] = null" and span_pr: "\ ide a; ide b \ \ span \\<^sub>1[a, b] \\<^sub>0[a, b]" and cod_pr0: "\ ide a; ide b \ \ cod \\<^sub>0[a, b] = b" and cod_pr1: "\ ide a; ide b \ \ cod \\<^sub>1[a, b] = a" and universal: "span f g \ \!l. \\<^sub>1[cod f, cod g] \ l = f \ \\<^sub>0[cod f, cod g] \ l = g" begin lemma pr0_in_hom': assumes "ide a" and "ide b" shows "\\\<^sub>0[a, b] : dom \\<^sub>0[a, b] \ b\" using assms span_pr cod_pr0 by auto lemma pr1_in_hom': assumes "ide a" and "ide b" shows "\\\<^sub>1[a, b] : dom \\<^sub>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. \\<^sub>1[cod f, cod g] \ l = f \ \\<^sub>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 \ \\<^sub>1[dom f, dom g], g \ \\<^sub>0[dom f, dom g]\" lemma seq_pr_tuple: assumes "span f g" shows "seq \\<^sub>0[cod f, cod g] \f, g\" proof - have "\\<^sub>0[cod f, cod g] \ \f, g\ = g" unfolding tuple_def using assms universal theI [of "\l. \\<^sub>1[cod f, cod g] \ l = f \ \\<^sub>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 \\<^sub>0[a, b] h" shows "\\\<^sub>1[a, b] \ h, \\<^sub>0[a, b] \ h\ = h" unfolding tuple_def using assms span_pr cod_pr0 cod_pr1 universal [of "\\<^sub>1[a, b] \ h" "\\<^sub>0[a, b] \ h"] theI_unique [of "\l. \\<^sub>1[a, b] \ l = \\<^sub>1[a, b] \ h \ \\<^sub>0[a, b] \ l = \\<^sub>0[a, b] \ h" h] by auto lemma pr_tuple [simp]: assumes "span f g" and "cod f = a" and "cod g = b" shows "\\<^sub>1[a, b] \ \f, g\ = f" and "\\<^sub>0[a, b] \ \f, g\ = g" proof - have 1: "\\<^sub>1[a, b] \ \f, g\ = f \ \\<^sub>0[a, b] \ \f, g\ = g" unfolding tuple_def using assms universal theI [of "\l. \\<^sub>1[a, b] \ l = f \ \\<^sub>0[a, b] \ l = g"] by simp meson show "\\<^sub>1[a, b] \ \f, g\ = f" using 1 by simp show "\\<^sub>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 = \\\<^sub>1[cod f, cod g], \\<^sub>0[cod f, cod g]\" unfolding prod_def using assms comp_cod_arr span_pr cod_pr0 cod_pr1 by simp also have "... = \\\<^sub>1[cod f, cod g] \ dom \\<^sub>0[cod f, cod g], \\<^sub>0[cod f, cod g] \ dom \\<^sub>0[cod f, cod g]\" using assms span_pr comp_arr_dom by simp also have "... = dom \\<^sub>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 "\\\<^sub>1[a, b], \\<^sub>0[a, b]\ = a \ b" proof - have 1: "dom \\<^sub>0[a, b] = a \ b" using assms seq_pr_tuple cod_tuple [of "\\<^sub>1[a, b]" "\\<^sub>0[a, b]"] span_pr pr0_in_hom' pr1_in_hom' by (metis cod_pr0 cod_pr1 seqE) hence "\\\<^sub>1[a, b], \\<^sub>0[a, b]\ = \\\<^sub>1[a, b] \ (a \ b), \\<^sub>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" shows "\\\<^sub>0[a, b] : a \ b \ b\" and "\\\<^sub>1[a, b] : a \ b \ a\" proof - show 0: "\\\<^sub>0[a, b] : a \ b \ b\" using assms pr0_in_hom' seq_pr_tuple [of "\\<^sub>1[a, b]" "\\<^sub>0[a, b]"] cod_tuple [of "\\<^sub>1[a, b]" "\\<^sub>0[a, b]"] span_pr cod_pr0 cod_pr1 by (intro in_homI, auto) show "\\\<^sub>1[a, b] : a \ b \ a\" using assms 0 span_pr pr1_in_hom' by fastforce qed lemma pr_simps [simp]: assumes "ide a" and "ide b" shows "arr \\<^sub>0[a, b]" and "dom \\<^sub>0[a, b] = a \ b" and "cod \\<^sub>0[a, b] = b" and "arr \\<^sub>1[a, b]" and "dom \\<^sub>1[a, b] = a \ b" and "cod \\<^sub>1[a, b] = a" using assms pr_in_hom by blast+ lemma arr_pr0_iff [iff]: shows "arr \\<^sub>0[a, b] \ ide a \ ide b" proof show "ide a \ ide b \ arr \\<^sub>0[a, b]" using pr_in_hom by auto show "arr \\<^sub>0[a, b] \ ide a \ ide b" using pr0_ext not_arr_null by metis qed lemma arr_pr1_iff [iff]: shows "arr \\<^sub>1[a, b] \ ide a \ ide b" proof show "ide a \ ide b \ arr \\<^sub>1[a, b]" using pr_in_hom by auto show "arr \\<^sub>1[a, b] \ ide a \ ide b" using pr1_ext not_arr_null by metis qed lemma pr_joint_monic: assumes "seq \\<^sub>0[a, b] h" and "\\<^sub>0[a, b] \ h = \\<^sub>0[a, b] \ h'" and "\\<^sub>1[a, b] \ h = \\<^sub>1[a, b] \ h'" shows "h = h'" using assms by (metis arr_pr0_iff seqE 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 "seq \\<^sub>0[cod f, cod g] (\f, g\ \ h)" using assms by fastforce show "\\<^sub>0[cod f, cod g] \ \f, g\ \ h = \\<^sub>0[cod f, cod g] \ \f \ h, g \ h\" proof - have "\\<^sub>0[cod f, cod g] \ \f, g\ \ h = (\\<^sub>0[cod f, cod g] \ \f, g\) \ h" using comp_assoc by simp thus ?thesis using assms by simp qed show "\\<^sub>1[cod f, cod g] \ \f, g\ \ h = \\<^sub>1[cod f, cod g] \ \f \ h, g \ h\" proof - have "\\<^sub>1[cod f, cod g] \ \f, g\ \ h = (\\<^sub>1[cod f, cod g] \ \f, g\) \ h" using comp_assoc by simp thus ?thesis using assms by simp qed qed lemma ide_prod [intro, simp]: assumes "ide a" and "ide b" shows "ide (a \ b)" using assms pr_simps ide_dom [of "\\<^sub>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+ 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 pr1 where "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 pr0 where "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 (pr1 a b) (pr0 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 pr0_def 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 pr0 pr1 proof show "\a b. \ (ide a \ ide b) \ pr0 a b = null" using pr0_def by auto show "\a b. \ (ide a \ ide b) \ pr1 a b = null" using pr1_def by auto 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 (pr1 a b) (pr0 a b)" interpret \: limit_cone J.comp C D.map \dom (pr1 a b)\ ?\ using a b pr_yields_binary_product by (simp add: has_as_binary_product_def) have 1: "pr1 a b = ?\ J.FF \ pr0 a b = ?\ J.TT" using D.mkCone_def by simp show "span (pr1 a b) (pr0 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 (pr1 a b) = a" using 1 \.preserves_cod [of J.FF] J.cod_char J.arr_char by auto show "cod (pr0 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. pr1 (cod f) (cod g) \ l = f \ pr0 (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 (pr1 (cod f) (cod g)) (pr0 (cod f) (cod g))" interpret \: limit_cone J.comp C D.map \dom (pr1 (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\ \pr1 (cod f) (cod g)\ \pr0 (cod f) (cod g)\ .. have 1: "pr1 (cod f) (cod g) = ?\ J.FF \ pr0 (cod f) (cod g) = ?\ J.TT" using D.mkCone_def by simp show "\!l. pr1 (cod f) (cod g) \ l = f \ pr0 (cod f) (cod g) \ l = g" proof - have "\!l. \l : dom f \ dom (pr1 (cod f) (cod g))\ \ pr1 (cod f) (cod g) \ l = f \ pr0 (cod f) (cod g) \ l = g" using fg \.is_universal' by simp moreover have "\l. pr1 (cod f) (cod g) \ l = f \ \l : dom f \ dom (pr1 (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 pr0 pr1" .. end context elementary_category_with_binary_products begin interpretation category_with_binary_products C proof show "has_binary_products" proof (unfold has_binary_products_def, intro allI impI) show "\a b. ide a \ ide b \ \p0 p1. has_as_binary_product a b p0 p1" proof - fix a b assume ab: "ide a \ ide b" have "has_as_binary_product a b \\<^sub>1[a, b] \\<^sub>0[a, b]" proof show "ide a" and "ide b" and "\\\<^sub>1[a, b] : a \ b \ a\" and "\\\<^sub>0[a, b] : a \ b \ b\" using ab by auto show "\x f g. \\f : x \ a\; \g : x \ b\\ \ \!h. \h : x \ a \ b\ \ \\<^sub>1[a, b] \ h = f \ \\<^sub>0[a, b] \ h = g" proof - fix x f g assume f: "\f : x \ a\" and g: "\g : x \ b\" show "\!h. \h : x \ a \ b\ \ \\<^sub>1[a, b] \ h = f \ \\<^sub>0[a, b] \ h = g" using ab f g tuple_pr_arr pr_tuple [of f g a b] tuple_in_hom' by (metis in_homE) qed qed thus "\p0 p1. has_as_binary_product a b p0 p1" by blast qed qed 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 "\\<^sub>0[c, d] \ (f \ g) = g \ \\<^sub>0[a, b]" and "\\<^sub>1[c, d] \ (f \ g) = f \ \\<^sub>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 "\\<^sub>0[a, a] \ \[a] = a" and "\\<^sub>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 "seq \\<^sub>0[b, c] f" and "seq \\<^sub>1[b, c] f" and "\\<^sub>0[b, c] \ f = f0" and "\\<^sub>1[b, c] \ f = f1" shows "f = \f1, f0\" using assms pr_joint_monic [of b c "\f1, f0\" f] pr_tuple by auto definition assoc ("\[_, _, _]") where "\[a, b, c] \ \\\<^sub>1[a, b] \ \\<^sub>1[a \ b, c], \\\<^sub>0[a, b] \ \\<^sub>1[a \ b, c], \\<^sub>0[a \ b, c]\\" definition assoc' ("\\<^sup>-\<^sup>1[_, _, _]") where "\\<^sup>-\<^sup>1[a, b, c] \ \\\\<^sub>1[a, b \ c], \\<^sub>1[b, c] \ \\<^sub>0[a, b \ c]\, \\<^sub>0[b, c] \ \\<^sub>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 "\\\<^sup>-\<^sup>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 \\<^sup>-\<^sup>1[a, b, c]" and "dom \\<^sup>-\<^sup>1[a, b, c] = a \ (b \ c)" and "cod \\<^sup>-\<^sup>1[a, b, c] = (a \ b) \ c" using assms assoc'_in_hom by auto 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 "\\<^sub>0[b0, b1 \ b2] \ \[b0, b1, b2] \ ((f0 \ f1) \ f2) = \\<^sub>0[b0, b1 \ b2] \ (f0 \ (f1 \ f2)) \ \[a0, a1, a2]" proof - have "\\<^sub>0[b0, b1 \ b2] \ \[b0, b1, b2] \ ((f0 \ f1) \ f2) = (\\<^sub>0[b0, b1 \ b2] \ \[b0, b1, b2]) \ ((f0 \ f1) \ f2)" using comp_assoc by simp also have "... = \\\<^sub>0[b0, b1] \ \\<^sub>1[b0 \ b1, b2], \\<^sub>0[b0 \ b1, b2]\ \ ((f0 \ f1) \ f2)" using assms assoc_def by fastforce also have "... = \(\\<^sub>0[b0, b1] \ \\<^sub>1[b0 \ b1, b2]) \ ((f0 \ f1) \ f2), \\<^sub>0[b0 \ b1, b2] \ ((f0 \ f1) \ f2)\" using assms comp_tuple_arr by fastforce also have "... = \(\\<^sub>0[b0, b1] \ (f0 \ f1)) \ \\<^sub>1[a0 \ a1, a2], f2 \ \\<^sub>0[a0 \ a1, a2]\" using assms comp_assoc by fastforce also have "... = \f1 \ \\<^sub>0[a0, a1] \ \\<^sub>1[a0 \ a1, a2], f2 \ \\<^sub>0[a0 \ a1, a2]\" using assms comp_assoc by (metis in_homE pr_naturality(1)) also have "... = \\<^sub>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 "\\<^sub>1[b0, b1 \ b2] \ \[b0, b1, b2] \ ((f0 \ f1) \ f2) = \\<^sub>1[b0, b1 \ b2] \ (f0 \ (f1 \ f2)) \ \[a0, a1, a2]" proof - have "\\<^sub>1[b0, b1 \ b2] \ \[b0, b1, b2] \ ((f0 \ f1) \ f2) = (\\<^sub>1[b0, b1 \ b2] \ \[b0, b1, b2]) \ ((f0 \ f1) \ f2)" using comp_assoc by simp also have "... = (\\<^sub>1[b0, b1] \ \\<^sub>1[b0 \ b1, b2]) \ ((f0 \ f1) \ f2)" using assms assoc_def by fastforce also have "... = (\\<^sub>1[b0, b1] \ (f0 \ f1)) \ \\<^sub>1[a0 \ a1, a2]" using assms comp_assoc by fastforce also have "... = f0 \ \\<^sub>1[a0, a1] \ \\<^sub>1[a0 \ a1, a2]" using assms comp_assoc by (metis in_homE pr_naturality(2)) also have "... = \\<^sub>1[b0, b1 \ b2] \ (f0 \ (f1 \ f2)) \ \[a0, a1, a2]" proof - have "\\<^sub>1[b0, b1 \ b2] \ (f0 \ (f1 \ f2)) \ \[a0, a1, a2] = (\\<^sub>1[b0, b1 \ b2] \ (f0 \ (f1 \ f2))) \ \[a0, a1, a2]" using comp_assoc by simp also have "... = f0 \ \\<^sub>1[a0, a1 \ a2] \ \[a0, a1, a2]" using assms comp_assoc by fastforce also have "... = f0 \ \\<^sub>1[a0, a1] \ \\<^sub>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 "seq \\<^sub>0[a, b \ (c \ d)] (((a \ \[b, c, d]) \ \[a, b \ c, d]) \ (\[a, b, c] \ d))" using assms by simp show "\\<^sub>1[a, b \ c \ d] \ ((a \ \[b, c, d]) \ \[a, b \ c, d]) \ (\[a, b, c] \ d) = \\<^sub>1[a, b \ c \ d] \ \[a, b, c \ d] \ \[a \ b, c, d]" proof - have "\\<^sub>1[a, b \ c \ d] \ ((a \ \[b, c, d]) \ \[a, b \ c, d]) \ (\[a, b, c] \ d) = ((\\<^sub>1[a, b \ c \ d] \ (a \ \[b, c, d])) \ \[a, b \ c, d]) \ (\[a, b, c] \ d)" using comp_assoc by simp also have "... = (\\<^sub>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 "... = \\<^sub>1[a, b \ c] \ \\<^sub>1[a \ b \ c, d] \ (\[a, b, c] \ d)" using assms assoc_def comp_assoc by simp also have "... = (\\<^sub>1[a, b \ c] \ \[a, b, c]) \ \\<^sub>1[(a \ b) \ c, d]" using assms pr_naturality(2) comp_assoc by fastforce also have "... = \\<^sub>1[a, b] \ \\<^sub>1[a \ b, c] \ \\<^sub>1[(a \ b) \ c, d]" using assms assoc_def comp_assoc by simp finally have "\\<^sub>1[a, b \ c \ d] \ ((a \ \[b, c, d]) \ \[a, b \ c, d]) \ (\[a, b, c] \ d) = \\<^sub>1[a, b] \ \\<^sub>1[a \ b, c] \ \\<^sub>1[(a \ b) \ c, d]" by blast also have "... = \\<^sub>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 "\\<^sub>0[a, b \ (c \ d)] \ ((a \ \[b, c, d]) \ \[a, b \ c, d]) \ (\[a, b, c] \ d) = \\<^sub>0[a, b \ (c \ d)] \ \[a, b, c \ d] \ \[a \ b, c, d]" proof - have "\\<^sub>0[a, b \ (c \ d)] \ ((a \ \[b, c, d]) \ \[a, b \ c, d]) \ (\[a, b, c] \ d) = \\<^sub>0[a, b \ c \ d] \ ((a \ \\\<^sub>1[b, c] \ \\<^sub>1[b \ c, d], \\\<^sub>0[b, c] \ \\<^sub>1[b \ c, d], \\<^sub>0[b \ c, d]\\) \ \\\<^sub>1[a, b \ c] \ \\<^sub>1[a \ b \ c, d], \\\<^sub>0[a, b \ c] \ \\<^sub>1[a \ b \ c, d], \\<^sub>0[a \ b \ c, d]\\) \ (\\\<^sub>1[a, b] \ \\<^sub>1[a \ b, c], \\\<^sub>0[a, b] \ \\<^sub>1[a \ b, c], \\<^sub>0[a \ b, c]\\ \ d)" using assms assoc_def by simp also have "... = \\\<^sub>1[b, c] \ \\<^sub>1[b \ c, d], \\\<^sub>0[b, c] \ \\<^sub>1[b \ c, d], \\<^sub>0[b \ c, d]\\ \ (\\<^sub>0[a, (b \ c) \ d] \ \\\<^sub>1[a, b \ c] \ \\<^sub>1[a \ b \ c, d], \\\<^sub>0[a, b \ c] \ \\<^sub>1[a \ b \ c, d], \\<^sub>0[a \ b \ c, d]\\) \ (\\\<^sub>1[a, b] \ \\<^sub>1[a \ b, c], \\\<^sub>0[a, b] \ \\<^sub>1[a \ b, c], \\<^sub>0[a \ b, c]\\ \ d)" proof - have "\\<^sub>0[a, b \ c \ d] \ (a \ \\\<^sub>1[b, c] \ \\<^sub>1[b \ c, d], \\\<^sub>0[b, c] \ \\<^sub>1[b \ c, d], \\<^sub>0[b \ c, d]\\) = \\\<^sub>1[b, c] \ \\<^sub>1[b \ c, d], \\\<^sub>0[b, c] \ \\<^sub>1[b \ c, d], \\<^sub>0[b \ c, d]\\ \ \\<^sub>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 "... = \\\<^sub>0[a, b] \ \\<^sub>1[a \ b, c] \ \\<^sub>1[(a \ b) \ c, d], \\\<^sub>0[a \ b, c] \ \\<^sub>1[(a \ b) \ c, d], d \ \\<^sub>0[(a \ b) \ c, d]\\" using assms comp_assoc by simp also have "... = \\\<^sub>0[a, b] \ \\<^sub>1[a \ b, c] \ \\<^sub>1[(a \ b) \ c, d], \\\<^sub>0[a \ b, c] \ \\<^sub>1[(a \ b) \ c, d], \\<^sub>0[(a \ b) \ c, d]\\" using assms comp_cod_arr by simp also have "... = \\<^sub>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] \\<^sup>-\<^sup>1[a, b, c]" using assms assoc_def assoc'_def comp_assoc by (auto simp add: tuple_pr_arr) 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'" .. definition sym ("\[_, _]") where "\[a1, a0] \ if ide a0 \ ide a1 then \\\<^sub>0[a1, a0], \\<^sub>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 "\\<^sub>0[a1, a0] \ \[a0, a1] = \\<^sub>1[a0, a1]" and "\\<^sub>1[a1, a0] \ \[a0, a1] = \\<^sub>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). (\\<^sub>1[cod f, cod g] \ (f \ g), \\<^sub>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 = (\\<^sub>1[cod (fst fg), cod (snd fg)] \ \\<^sub>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 "... = ((\\<^sub>1[cod (fst fg), cod (snd fg)] \ \\<^sub>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 "... = \\\<^sub>1[cod (fst fg), cod (snd fg)] \ (cod (fst fg) \ cod (snd fg)), \\<^sub>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: "ide a \ \\[a] : a \ \\" - and trm_eqI: "\ ide a; \f : a \ \\ \ \ f = \[a]" + and trm_in_hom_ax: "ide a \ \\[a] : a \ \\" + and trm_eqI_ax: "\ ide a; \f : a \ \\ \ \ f = \[a]" begin - lemma trm_simps: + lemma trm_simps_ide: assumes "ide a" shows "arr \[a]" and "dom \[a] = a" and "cod \[a] = \" - using assms trm_in_hom by auto + using assms trm_in_hom_ax by auto lemma trm_one: shows "\[\] = \" - using ide_one trm_in_hom trm_eqI ide_in_hom by auto + using ide_one trm_in_hom_ax trm_eqI_ax ide_in_hom by auto lemma terminal_one: shows "terminal \" - using ide_one trm_in_hom trm_eqI terminal_def by metis + using ide_one trm_in_hom_ax trm_eqI_ax 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) + using assms trm_eqI_ax + by (metis comp_in_homI' ide_cod ide_dom in_homE trm_in_hom_ax) proposition is_category_with_terminal_object: shows "category_with_terminal_object C" apply unfold_locales using terminal_one by auto end context category_with_terminal_object begin definition some_terminal ("\") where "some_terminal \ SOME t. terminal t" definition "trm" ("\[_]") 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 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 trm_def terminal_def terminal_some_terminal by simp thus ?thesis using assms trm_def [of f] theI' [of "\t. \t : dom f \ \\"] by auto qed lemma trm_simps [simp]: assumes "arr f" shows "arr \[f]" and "dom \[f] = dom f" and "cod \[f] = \" using assms trm_in_hom by auto lemma 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 trm_def the1_equality [of "\t. \t : dom f \ \\" t] \ide (dom f)\ arr_dom_iff_arr by fastforce qed sublocale elementary_category_with_terminal_object C \ trm using ide_some_terminal trm_eqI by unfold_locales auto proposition extends_to_elementary_category_with_terminal_object: shows "elementary_category_with_terminal_object C \ trm" .. 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 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" using a0 a1 p0p1 apply (elim has_as_pullbackE, intro has_as_binary_productI) apply blast apply blast apply fastforce apply fastforce proof - fix x f g assume f: "\f : x \ a0\" and g: "\g : x \ a1\" assume "\h k. commutative_square \[a0] \[a1] h k \ \!l. p0 \ l = h \ p1 \ l = k" moreover have "commutative_square \[a0] \[a1] f g" using f g by (metis a0 commutative_squareI in_homE - elementary_category_with_terminal_object.trm_simps(2) + elementary_category_with_terminal_object.trm_simps_ide(2) extends_to_elementary_category_with_terminal_object has_as_pullbackE p0p1 trm_naturality) 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 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 proposition is_cartesian_category: shows "cartesian_category C" using cartesian_category.intro is_category_with_binary_products is_category_with_terminal_object by auto end context cartesian_category begin proposition extends_to_elementary_cartesian_category: shows "elementary_cartesian_category C pr0 pr1 \ trm" by (simp add: elementary_cartesian_category_def elementary_category_with_terminal_object_axioms extends_to_elementary_category_with_binary_products) sublocale elementary_cartesian_category C pr0 pr1 \ trm using extends_to_elementary_cartesian_category by simp end 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 "\ \ \\<^sub>0[\, \]" lemma pr_coincidence: shows "\ = \\<^sub>1[\, \]" using ide_one by (simp add: terminal_arr_unique terminal_one) lemma \_is_terminal_arr: shows "terminal_arr \" using ide_one by (simp add: terminal_one) lemma inverse_arrows_\: shows "inverse_arrows \ \\, \\" using ide_one by (metis (no_types, lifting) dup_is_natural_transformation \_is_terminal_arr cod_pr0 comp_cod_arr pr_dup(1) ide_dom inverse_arrows_def map_simp - natural_transformation.is_natural_2 pr_simps(2) pr1_in_hom' trm_eqI trm_naturality + natural_transformation.is_natural_2 pr_simps(2) pr1_in_hom' trm_eqI_ax trm_naturality trm_one tuple_pr) lemma \_is_iso: shows "iso \" using inverse_arrows_\ by auto lemma trm_tensor: assumes "ide a" and "ide b" shows "\[a \ b] = \ \ (\[a] \ \[b])" proof - have "\[a \ b] = \[a] \ \\<^sub>1[a, b]" by (metis assms(1-2) cod_pr1 pr_simps(4-6) trm_naturality) moreover have "\\[b] : b \ \\" - using assms(2) trm_in_hom by blast + using assms(2) trm_in_hom_ax by blast ultimately show ?thesis - using assms(1) pr_coincidence trm_in_hom by fastforce + using assms(1) pr_coincidence trm_in_hom_ax by fastforce qed abbreviation runit ("\[_]") where "\[a] \ \\<^sub>1[a, \]" abbreviation runit' ("\\<^sup>-\<^sup>1[_]") where "\\<^sup>-\<^sup>1[a] \ \a, \[a]\" abbreviation lunit ("\[_]") where "\[a] \ \\<^sub>0[\, a]" abbreviation lunit' ("\\<^sup>-\<^sup>1[_]") where "\\<^sup>-\<^sup>1[a] \ \\[a], a\" lemma runit_in_hom: assumes "ide a" shows "\\[a] : a \ \ \ a\" using assms ide_one by simp lemma runit'_in_hom: assumes "ide a" shows "\\\<^sup>-\<^sup>1[a] : a \ a \ \\" - using assms ide_in_hom trm_in_hom by blast + using assms ide_in_hom trm_in_hom_ax by blast lemma lunit_in_hom: assumes "ide a" shows "\\[a] : \ \ a \ a\" using assms ide_one by simp lemma lunit'_in_hom: assumes "ide a" shows "\\\<^sup>-\<^sup>1[a] : a \ \ \ a\" - using assms ide_in_hom trm_in_hom by blast + using assms ide_in_hom trm_in_hom_ax by blast lemma runit_naturality: assumes "ide a" shows "\[cod a] \ (a \ \) = a \ \[dom a]" using assms pr_naturality(2) ide_char ide_one by blast lemma inverse_arrows_runit: assumes "ide a" shows "inverse_arrows \[a] \\<^sup>-\<^sup>1[a]" proof show "ide (\[a] \ \\<^sup>-\<^sup>1[a])" proof - have "\[a] \ \\<^sup>-\<^sup>1[a] = a" using assms - by (metis in_homE ide_char pr_tuple(1) trm_in_hom) + by (metis in_homE ide_char pr_tuple(1) trm_in_hom_ax) thus ?thesis using assms by presburger qed show "ide (\\<^sup>-\<^sup>1[a] \ \[a])" proof - have "ide (a \ \)" using assms ide_one by blast moreover have "\\<^sup>-\<^sup>1[a] \ \[a] = a \ \" proof (intro pr_joint_monic [of a \ "\\<^sup>-\<^sup>1[a] \ \[a]" "a \ \"]) show "seq \\<^sub>0[a, \] (\\<^sup>-\<^sup>1[a] \ \[a])" using assms ide_one runit'_in_hom [of a] by (intro seqI) auto show "\\<^sub>0[a, \] \ \\<^sup>-\<^sup>1[a] \ \[a] = \\<^sub>0[a, \] \ (a \ \)" proof - have "\\<^sub>0[a, \] \ \\<^sup>-\<^sup>1[a] \ \[a] = (\\<^sub>0[a, \] \ \\<^sup>-\<^sup>1[a]) \ \[a]" using comp_assoc by simp also have "... = \[a] \ \[a]" using assms ide_one - by (metis in_homE pr_tuple(2) ide_char trm_in_hom) + by (metis in_homE pr_tuple(2) ide_char trm_in_hom_ax) also have "... = \[a \ \]" using assms ide_one trm_naturality [of "\[a]"] by simp also have "... = \\<^sub>0[a, \] \ (a \ \)" using assms comp_arr_dom ide_one trm_naturality trm_one by fastforce finally show ?thesis by blast qed show "\\<^sub>1[a, \] \ \\<^sup>-\<^sup>1[a] \ \[a] = \\<^sub>1[a, \] \ (a \ \)" using assms by (metis \ide (\[a] \ \\<^sup>-\<^sup>1[a])\ cod_comp cod_pr1 dom_comp ide_compE ide_one comp_assoc runit_naturality) qed ultimately show ?thesis by simp qed qed lemma lunit_naturality: assumes "arr f" shows "C \[cod f] (\ \ f) = C f \[dom f]" using assms pr_naturality(1) ide_char ide_one by blast lemma inverse_arrows_lunit: assumes "ide a" shows "inverse_arrows \[a] \\<^sup>-\<^sup>1[a]" proof show "ide (C \[a] \\<^sup>-\<^sup>1[a])" proof - have "C \[a] \\<^sup>-\<^sup>1[a] = a" using assms - by (metis ide_char in_homE pr_tuple(2) trm_in_hom) + by (metis ide_char in_homE pr_tuple(2) trm_in_hom_ax) thus ?thesis using assms by simp qed show "ide (\\<^sup>-\<^sup>1[a] \ \[a])" proof - have "\\<^sup>-\<^sup>1[a] \ \[a] = \ \ a" proof (intro pr_joint_monic [of \ a "\\<^sup>-\<^sup>1[a] \ \[a]" "\ \ a"]) show "seq \[a] (\\<^sup>-\<^sup>1[a] \ \[a])" using assms \ide (\[a] \ \\<^sup>-\<^sup>1[a])\ by blast show "\[a] \ \\<^sup>-\<^sup>1[a] \ \[a] = \[a] \ (\ \ a)" using assms by (metis \ide (\[a] \ \\<^sup>-\<^sup>1[a])\ cod_comp cod_pr0 dom_cod ide_compE ide_one comp_assoc lunit_naturality) show "\\<^sub>1[\, a] \ \\<^sup>-\<^sup>1[a] \ \[a] = \\<^sub>1[\, a] \ (\ \ a)" proof - have "\\<^sub>1[\, a] \ \\<^sup>-\<^sup>1[a] \ \[a] = (\\<^sub>1[\, a] \ \\<^sup>-\<^sup>1[a]) \ \[a]" using comp_assoc by simp also have "... = \[a] \ \[a]" using assms ide_one - by (metis pr_tuple(1) ide_char in_homE trm_in_hom) + by (metis pr_tuple(1) ide_char in_homE trm_in_hom_ax) also have "... = \[\ \ a]" using assms ide_one trm_naturality [of "\[a]"] by simp also have "... = \\<^sub>1[\, a] \ (\ \ a)" using assms comp_arr_dom ide_one trm_naturality trm_one by fastforce finally show ?thesis by simp qed qed moreover have "ide (\ \ a)" using assms ide_one by simp finally show ?thesis by blast qed qed lemma comp_lunit_term_dup: assumes "ide a" shows "\[a] \ (\[a] \ a) \ \[a] = a" proof - have "\\[a] : a \ \\" - using assms trm_in_hom by blast + using assms trm_in_hom_ax by blast hence "\[a] \ (\[a] \ a) = a \ \\<^sub>0[a, a]" by (metis assms pr_naturality(1) ide_char in_homE) thus ?thesis by (metis (no_types) assms comp_assoc comp_ide_self pr_dup(1)) qed lemma comp_runit_term_dup: assumes "ide a" shows "\[a] \ (a \ \[a]) \ \[a] = a" proof - have "\\[a] : a \ \\" - using assms trm_in_hom by blast + using assms trm_in_hom_ax by blast hence "\[a] \ (a \ \[a]) = a \ \\<^sub>1[a, a]" using assms by auto thus ?thesis using assms by (metis comp_ide_arr pr_dup(2) ide_char comp_assoc seqI) qed lemma comp_proj_assoc: assumes "ide a0" and "ide a1" and "ide a2" shows "\\<^sub>1[a0, a1 \ a2] \ \[a0, a1, a2] = \\<^sub>1[a0, a1] \ \\<^sub>1[a0 \ a1, a2]" and "\\<^sub>0[a0, a1 \ a2] \ \[a0, a1, a2] = \\\<^sub>0[a0, a1] \ \\<^sub>1[a0 \ a1, a2], \\<^sub>0[a0 \ a1, a2]\" using assms assoc_def by auto lemma dup_coassoc: assumes "ide a" shows "\[a, a, a] \ (\[a] \ a) \ \[a] = (a \ \[a]) \ \[a]" proof (intro pr_joint_monic [of a "a \ a" "\[a, a, a] \ (\[a] \ a) \ \[a]" "(a \ \[a]) \ \[a]"]) show "seq \\<^sub>0[a, a \ a] (\[a, a, a] \ (\[a] \ a) \ \[a])" using assms by simp show "\\<^sub>0[a, a \ a] \ \[a, a, a] \ (\[a] \ a) \ \[a] = \\<^sub>0[a, a \ a] \ (a \ \[a]) \ \[a]" proof - have "\\<^sub>0[a, a \ a] \ \[a, a, a] \ (\[a] \ a) \ \[a] = ((\\<^sub>0[a, a \ a] \ \[a, a, a]) \ (\[a] \ a)) \ \[a]" using comp_assoc by simp also have "... = \((\\<^sub>0[a, a] \ \\<^sub>1[a \ a, a]) \ (\[a] \ a)) \ \[a], (a \ \\<^sub>0[a, a]) \ \[a]\" using assms assoc_def by simp also have "... = \[a]" using assms comp_assoc by simp also have "... = (\\<^sub>0[a, a \ a] \ (a \ \[a])) \ \[a]" using assms assoc_def comp_assoc by simp also have "... = \\<^sub>0[a, a \ a] \ (a \ \[a]) \ \[a]" using comp_assoc by simp finally show ?thesis by blast qed show "\\<^sub>1[a, a \ a] \ \[a, a, a] \ (\[a] \ a) \ \[a] = \\<^sub>1[a, a \ a] \ (a \ \[a]) \ \[a]" proof - have "\\<^sub>1[a, a \ a] \ \[a, a, a] \ (\[a] \ a) \ \[a] = ((\\<^sub>1[a, a \ a] \ \[a, a, a]) \ (\[a] \ a)) \ \[a]" using comp_assoc by simp also have "... = ((\\<^sub>1[a, a] \ \\<^sub>1[a \ a, a]) \ (\[a] \ a)) \ \[a]" using assms assoc_def by simp also have "... = a" using assms comp_assoc by simp also have "... = (a \ \\<^sub>1[a, a]) \ \[a]" using assms comp_assoc by simp also have "... = (\\<^sub>1[a, a \ a] \ (a \ \[a])) \ \[a]" using assms by simp also have "... = \\<^sub>1[a, a \ a] \ (a \ \[a]) \ \[a]" using comp_assoc by simp finally show ?thesis by blast qed qed lemma comp_assoc_tuple: assumes "\f0 : a \ b0\" and "\f1 : a \ b1\" and "\f2 : a \ b2\" shows "\[b0, b1, b2] \ \\f0, f1\, f2\ = \f0, \f1, f2\\" and "\\<^sup>-\<^sup>1[b0, b1, b2] \ \f0, \f1, f2\\ = \\f0, f1\, f2\" using assms assoc_def assoc'_def comp_assoc by fastforce+ lemma dup_tensor: assumes "ide a" and "ide b" shows "\[a \ b] = \\<^sup>-\<^sup>1[a, b, a \ b] \ (a \ \[b, a, b]) \ (a \ \ (a, b) \ b) \ (a \ \\<^sup>-\<^sup>1[a, b, b]) \ \[a, a, b \ b] \ (\[a] \ \[b])" proof (intro pr_joint_monic [of "a \ b" "a \ b" "\[a \ b]"]) show "seq \\<^sub>0[a \ b, a \ b] (\[a \ b])" using assms by simp have 1: "\\<^sup>-\<^sup>1[a, b, a \ b] \ (a \ \[b, a, b]) \ (a \ \ (a, b) \ b) \ (a \ \\<^sup>-\<^sup>1[a, b, b]) \ \[a, a, b \ b] \ (\[a] \ \[b]) = \a \ b, a \ b\" proof - have "\\<^sup>-\<^sup>1[a, b, a \ b] \ (a \ \[b, a, b]) \ (a \ \ (a, b) \ b) \ (a \ \\<^sup>-\<^sup>1[a, b, b]) \ \[a, a, b \ b] \ (\[a] \ \[b]) = \\<^sup>-\<^sup>1[a, b, a \ b] \ (a \ \[b, a, b]) \ (a \ \ (a, b) \ b) \ (a \ \\<^sup>-\<^sup>1[a, b, b]) \ \\\<^sub>1[a, b], \\\<^sub>1[a, b], \[b] \ \\<^sub>0[a, b]\\" proof - have "\[a, a, b \ b] \ (\[a] \ \[b]) = \\\<^sub>1[a, b], \\\<^sub>1[a, b], \[b] \ \\<^sub>0[a, b]\\" using assms assoc_def comp_assoc pr_naturality comp_cod_arr by simp thus ?thesis by presburger qed also have "... = \\<^sup>-\<^sup>1[a, b, a \ b] \ \a \ a \ a \ \\<^sub>1[a, b], \[b, a, b] \ (\[a, b] \ (a \ b) \ b) \ \\<^sup>-\<^sup>1[a, b, b] \ \\\<^sub>1[a, b], \[b \ \\<^sub>0[a, b]]\\" using assms prod_tuple by simp also have "... = \\<^sup>-\<^sup>1[a, b, a \ b] \ \\\<^sub>1[a, b], \[b, a, b] \ (\[a, b] \ b) \ \\<^sup>-\<^sup>1[a, b, b] \ \\\<^sub>1[a, b], \[\\<^sub>0[a, b]]\\" proof - have "a \ a \ a \ \\<^sub>1[a, b] = \\<^sub>1[a, b]" using assms comp_cod_arr by simp moreover have "b \ \\<^sub>0[a, b] = \\<^sub>0[a, b]" using assms comp_cod_arr by simp moreover have "\[a, b] \ (a \ b) \ b = \[a, b] \ b" using assms comp_arr_dom by simp ultimately show ?thesis by simp qed also have "... = \\<^sup>-\<^sup>1[a, b, a \ b] \ \\\<^sub>1[a, b], \[b, a, b] \ (\[a, b] \ b) \ \\\\<^sub>1[a, b], \\<^sub>0[a, b]\, \\<^sub>0[a, b]\\" proof - have "\\<^sup>-\<^sup>1[a, b, b] \ \\\<^sub>1[a, b], \[\\<^sub>0[a, b]]\ = \\\\<^sub>1[a, b], \\<^sub>0[a, b]\, \\<^sub>0[a, b]\" using assms comp_assoc_tuple(2) by blast thus ?thesis by simp qed also have "... = \\<^sup>-\<^sup>1[a, b, a \ b] \ \\\<^sub>1[a, b], \[b, a, b] \ \\[a, b], \\<^sub>0[a, b]\\" using assms prod_tuple comp_arr_dom comp_cod_arr by simp also have "... = \\<^sup>-\<^sup>1[a, b, a \ b] \ \\\<^sub>1[a, b], \\\<^sub>0[a, b], \\\<^sub>1[a, b], \\<^sub>0[a, b]\\\" using assms comp_assoc_tuple(1) by (metis sym_def pr_in_hom) also have "... = \\\\<^sub>1[a, b], \\<^sub>0[a, b]\, \\\<^sub>1[a, b], \\<^sub>0[a, b]\\" using assms comp_assoc_tuple(2) by force also have "... = \[a \ b]" using assms by simp finally show ?thesis by simp qed show "\\<^sub>0[a \ b, a \ b] \ \[a \ b] = \\<^sub>0[a \ b, a \ b] \ \\<^sup>-\<^sup>1[a, b, a \ b] \ (a \ \[b, a, b]) \ (a \ \ (a, b) \ b) \ (a \ \\<^sup>-\<^sup>1[a, b, b]) \ \[a, a, b \ b] \ (\[a] \ \[b])" using assms 1 by force show "\\<^sub>1[a \ b, a \ b] \ \[a \ b] = \\<^sub>1[a \ b, a \ b] \ \\<^sup>-\<^sup>1[a, b, a \ b] \ (a \ \[b, a, b]) \ (a \ \ (a, b) \ b) \ (a \ \\<^sup>-\<^sup>1[a, b, b]) \ \[a, a, b \ b] \ (\[a] \ \[b])" using assms 1 by force qed (* TODO: Not sure if the remaining facts are useful. *) lemma \_eq_trm: shows "\ = \[\ \ \]" proof (intro terminal_arr_unique) show "par \ \[\ \ \]" by (simp add: ide_one trm_one trm_tensor) show "terminal_arr \[\ \ \]" using ide_one \_is_terminal_arr \par \ \[\ \ \]\ by auto show "terminal_arr \" using \_is_terminal_arr by blast qed lemma terminal_tensor_one_one: shows "terminal (\ \ \)" proof show "ide (\ \ \)" using ide_one by simp show "\a. ide a \ \!f. \f : a \ \ \ \\" proof - fix a assume a: "ide a" show "\!f. \f : a \ \ \ \\" proof show "\inv \ \ \[a] : a \ \ \ \\" - using a ide_one inverse_arrows_\ inverse_unique trm_in_hom by fastforce + using a ide_one inverse_arrows_\ inverse_unique trm_in_hom_ax by fastforce show "\f. \f : a \ \ \ \\ \ f = inv \ \ \[a]" proof - fix f assume f: "\f : a \ \ \ \\" have "\ \ f = \[a]" proof (intro terminal_arr_unique) show "par (\ \ f) \[a]" using a f by (metis \_is_iso \_is_terminal_arr \\inv \ \ \[a] : a \ \ \ \\\ cod_comp dom_comp dom_inv ide_one in_homE pr_simps(2-3) seqE seqI) show "terminal_arr (\ \ f)" using a f \_is_terminal_arr cod_comp by force show "terminal_arr \[a]" using a \par (\ \ f) \[a]\ \terminal_arr (\ \ f)\ by auto qed thus "f = inv \ \ \[a]" using a f \_is_iso invert_side_of_triangle(1) \\inv \ \ \[a] : a \ \ \ \\\ by blast qed qed qed qed end section "Category with Finite Products" text \ In this last section, we show that the notion ``cartesian category'', which we defined to be a category with binary products and terminal object, coincides with the notion ``category with finite products''. Due to the inability to quantify over types in HOL, we content ourselves with defining the latter notion as "has \I\-indexed products for every finite set \I\ of natural numbers." We can transfer this property to finite sets at other types using the fact that products are preserved under bijections of the index sets. \ locale category_with_finite_products = category C for C :: "'c comp" + assumes has_finite_products: "finite (I :: nat set) \ has_products I" begin lemma has_finite_products': assumes "I \ UNIV" shows "finite I \ has_products I" proof - assume I: "finite I" obtain n \ where \: "bij_betw \ {k. k < (n :: nat)} I" using I finite_imp_nat_seg_image_inj_on inj_on_imp_bij_betw by fastforce show "has_products I" using assms(1) \ has_finite_products has_products_preserved_by_bijection category_with_finite_products.has_finite_products by blast qed end lemma (in category) has_binary_products_if: assumes "has_products ({0, 1} :: nat set)" shows "has_binary_products" proof (unfold has_binary_products_def) show "\a0 a1. ide a0 \ ide a1 \ (\p0 p1. has_as_binary_product a0 a1 p0 p1)" proof (intro allI impI) fix a0 a1 assume 1: "ide a0 \ ide a1" show "\p0 p1. has_as_binary_product a0 a1 p0 p1" proof - interpret J: binary_product_shape by unfold_locales interpret D: binary_product_diagram C a0 a1 using 1 by unfold_locales auto interpret discrete_diagram J.comp C D.map using J.is_discrete by unfold_locales auto show "\p0 p1. has_as_binary_product a0 a1 p0 p1" proof (unfold has_as_binary_product_def) text \ Here we have to work around the fact that \has_finite_products\ is defined in terms of @{typ "nat set"}, whereas \has_as_binary_product\ is defined in terms of \J.arr set\. \ let ?\ = "(\x :: nat. if x = 0 then J.FF else J.TT)" let ?\ = "\j. if j = J.FF then 0 else 1" have "bij_betw ?\ ({0, 1} :: nat set) {J.FF, J.TT}" using bij_betwI [of ?\ "{0, 1} :: nat set" "{J.FF, J.TT}" ?\] by fastforce hence "has_products {J.FF, J.TT}" using assms has_products_def [of "{J.FF, J.TT}"] has_products_preserved_by_bijection [of "{0, 1} :: nat set" ?\ "{J.FF, J.TT}"] by blast hence "\a. has_as_product J.comp D.map a" using has_products_def [of "{J.FF, J.TT}"] discrete_diagram_axioms J.arr_char by blast hence "\a \. product_cone J.comp C D.map a \" using has_as_product_def by blast hence 2: "\a \. D.limit_cone a \" unfolding product_cone_def by simp obtain a \ where \: "D.limit_cone a \" using 2 by auto interpret \: limit_cone J.comp C D.map a \ using \ by auto have "\ = D.mkCone (\ J.FF) (\ J.TT)" proof - have "\a. J.ide a \ \ a = D.mkCone (\ J.FF) (\ J.TT) a" using D.mkCone_def J.ide_char by auto moreover have "a = dom (\ J.FF)" by simp moreover have "D.cone a (D.mkCone (\ (J.MkIde False)) (\ (J.MkIde True)))" using 1 D.cone_mkCone [of "\ J.FF" "\ J.TT"] by auto ultimately show ?thesis using D.mkCone_def \.natural_transformation_axioms D.cone_mkCone [of "\ J.FF" "\ J.TT"] NaturalTransformation.eqI [of "J.comp" C \.A.map "D.map" \ "D.mkCone (\ J.FF) (\ J.TT)"] cone_def [of J.comp C D.map a "D.mkCone (\ J.FF) (\ J.TT)"] J.ide_char by blast qed hence "D.limit_cone (dom (\ J.FF)) (D.mkCone (\ J.FF) (\ J.TT))" using \.limit_cone_axioms by simp thus "\p0 p1. ide a0 \ ide a1 \ D.has_as_binary_product p0 p1" using 1 by blast qed qed qed qed sublocale category_with_finite_products \ category_with_binary_products C using has_binary_products_if has_finite_products by (unfold_locales, unfold has_binary_products_def) simp - proposition (in category_with_finite_products) is_category_with_binary_products: + proposition (in category_with_finite_products) is_category_with_binary_products\<^sub>C\<^sub>F\<^sub>P: shows "category_with_binary_products C" .. sublocale category_with_finite_products \ category_with_terminal_object C proof interpret J: discrete_category "{} :: nat set" by unfold_locales auto interpret D: empty_diagram J.comp C "\j. null" by unfold_locales auto interpret D: discrete_diagram J.comp C "\j. null" using J.is_discrete by unfold_locales auto have "\a. D.has_as_limit a \ has_as_product J.comp (\j. null) a" using product_cone_def J.category_axioms category_axioms D.discrete_diagram_axioms has_as_product_def product_cone_def by metis moreover have "\a. has_as_product J.comp (\j. null) a" using has_finite_products [of "{} :: nat set"] has_products_def [of "{} :: nat set"] D.discrete_diagram_axioms by blast ultimately have "\a. D.has_as_limit a" by blast thus "\a. terminal a" using D.has_as_limit_iff_terminal by blast qed - proposition (in category_with_finite_products) is_category_with_terminal_object: + proposition (in category_with_finite_products) is_category_with_terminal_object\<^sub>C\<^sub>F\<^sub>P: shows "category_with_terminal_object C" .. sublocale category_with_finite_products \ cartesian_category .. - proposition (in category_with_finite_products) is_cartesian_category: + proposition (in category_with_finite_products) is_cartesian_category\<^sub>C\<^sub>F\<^sub>P: shows "cartesian_category C" .. context category begin lemma binary_product_of_products_is_product: assumes "has_as_product J0 D0 a0" and "has_as_product J1 D1 a1" and "has_as_binary_product a0 a1 p0 p1" and "Collect (partial_magma.arr J0) \ Collect (partial_magma.arr J1) = {}" and "partial_magma.null J0 = partial_magma.null J1" shows "has_as_product (discrete_category.comp (Collect (partial_magma.arr J0) \ Collect (partial_magma.arr J1)) (partial_magma.null J0)) (\i. if i \ Collect (partial_magma.arr J0) then D0 i else if i \ Collect (partial_magma.arr J1) then D1 i else null) (dom p0)" proof - obtain \0 where \0: "product_cone J0 (\) D0 a0 \0" using assms(1) has_as_product_def by blast obtain \1 where \1: "product_cone J1 (\) D1 a1 \1" using assms(2) has_as_product_def by blast interpret J0: category J0 using \0 product_cone.axioms(1) by metis interpret J1: category J1 using \1 product_cone.axioms(1) by metis interpret D0: discrete_diagram J0 C D0 using \0 product_cone.axioms(3) by metis interpret D1: discrete_diagram J1 C D1 using \1 product_cone.axioms(3) by metis interpret \0: product_cone J0 C D0 a0 \0 using \0 by auto interpret \1: product_cone J1 C D1 a1 \1 using \1 by auto interpret J: discrete_category \Collect J0.arr \ Collect J1.arr\ J0.null using J0.not_arr_null assms(5) by unfold_locales auto interpret X: binary_product_shape . interpret a0xa1: binary_product_diagram C a0 a1 using assms(3) has_as_binary_product_def by (simp add: binary_product_diagram.intro binary_product_diagram_axioms.intro category_axioms) have p0p1: "a0xa1.has_as_binary_product p0 p1" using assms(3) has_as_binary_product_def [of a0 a1 p0 p1] by simp let ?D = "(\i. if i \ Collect J0.arr then D0 i else if i \ Collect J1.arr then D1 i else null)" let ?a = "dom p0" let ?\ = "\i. if i \ Collect J0.arr then \0 i \ p0 else if i \ Collect J1.arr then \1 i \ p1 else null" let ?p0p1 = "a0xa1.mkCone p0 p1" interpret p0p1: limit_cone X.comp C a0xa1.map ?a ?p0p1 using p0p1 by simp have a: "ide ?a" using p0p1.ide_apex by simp have p0: "\p0 : ?a \ a0\" using a0xa1.mkCone_def p0p1.preserves_hom [of X.FF X.FF X.FF] X.ide_char X.ide_in_hom by auto have p1: "\p1 : ?a \ a1\" using a0xa1.mkCone_def p0p1.preserves_hom [of X.TT X.TT X.TT] X.ide_char X.ide_in_hom by auto interpret D: discrete_diagram J.comp C ?D using assms J.arr_char J.dom_char J.cod_char J.is_discrete D0.is_discrete D1.is_discrete J.cod_comp J.seq_char by unfold_locales auto interpret A: constant_functor J.comp C ?a using p0p1.ide_apex by unfold_locales simp interpret \: natural_transformation J.comp C A.map ?D ?\ proof fix j show "\ J.arr j \ ?\ j = null" by simp assume j: "J.arr j" have \0j: "J0.arr j \ \\0 j : a0 \ D0 j\" using D0.is_discrete by auto have \1j: "J1.arr j \ \\1 j : a1 \ D1 j\" using D1.is_discrete by auto show "dom (?\ j) = A.map (J.dom j)" using j J.arr_char p0 p1 \0j \1j by fastforce show "cod (?\ j) = ?D (J.cod j)" using j J.arr_char p0 p1 \0j \1j by fastforce show "?D j \ ?\ (J.dom j) = ?\ j" proof - have 0: "J0.arr j \ D0 j \ \0 j \ p0 = \0 j \ p0" proof - have "J0.arr j \ (D0 j \ \0 j) \ p0 = \0 j \ p0" using p0 \0.is_natural_1 \0.is_natural_2 D0.is_discrete by simp thus "J0.arr j \ D0 j \ \0 j \ p0 = \0 j \ p0" using comp_assoc by simp qed have 1: "J1.arr j \ D1 j \ \1 j \ p1 = \1 j \ p1" proof - have "J1.arr j \ (D1 j \ \1 j) \ p1 = \1 j \ p1" using p1 \1.is_natural_1 \1.is_natural_2 D1.is_discrete by simp thus "J1.arr j \ D1 j \ \1 j \ p1 = \1 j \ p1" using comp_assoc by simp qed show ?thesis using 0 1 by auto qed show "?\ (J.cod j) \ A.map j = ?\ j" using j comp_arr_dom p0 p1 comp_assoc by auto qed interpret \: cone J.comp C ?D ?a ?\ .. interpret \: product_cone J.comp C ?D ?a ?\ proof show "\a' \'. D.cone a' \' \ \!f. \f : a' \ ?a\ \ D.cones_map f ?\ = \'" proof - fix a' \' assume \': "D.cone a' \'" interpret \': cone J.comp C ?D a' \' using \' by simp show "\!f. \f : a' \ ?a\ \ D.cones_map f ?\ = \'" proof let ?\0' = "\i. if i \ Collect J0.arr then \' i else null" let ?\1' = "\i. if i \ Collect J1.arr then \' i else null" have 0: "\i. i \ Collect J0.arr \ \' i \ hom a' (D0 i)" using J.arr_char by auto have 1: "\i. i \ Collect J1.arr \ \' i \ hom a' (D1 i)" using J.arr_char \Collect J0.arr \ Collect J1.arr = {}\ by force interpret A0': constant_functor J0 C a' apply unfold_locales using \'.ide_apex by auto interpret A1': constant_functor J1 C a' apply unfold_locales using \'.ide_apex by auto interpret \0': cone J0 C D0 a' ?\0' proof (unfold_locales) fix j show "\ J0.arr j \ (if j \ Collect J0.arr then \' j else null) = null" by simp assume j: "J0.arr j" show 0: "dom (?\0' j) = A0'.map (J0.dom j)" using j by simp show 1: "cod (?\0' j) = D0 (J0.cod j)" using j J.arr_char J.cod_char D0.is_discrete by simp show "D0 j \ (?\0' (J0.dom j)) = ?\0' j" using 1 j J.arr_char D0.is_discrete comp_cod_arr by simp show "?\0' (J0.cod j) \ A0'.map j = ?\0' j" using 0 j J.arr_char D0.is_discrete comp_arr_dom by simp qed interpret \1': cone J1 C D1 a' ?\1' proof (unfold_locales) fix j show "\ J1.arr j \ (if j \ Collect J1.arr then \' j else null) = null" by simp assume j: "J1.arr j" show 0: "dom (?\1' j) = A1'.map (J1.dom j)" using j by simp show 1: "cod (?\1' j) = D1 (J1.cod j)" using assms(4) j J.arr_char J.cod_char D1.is_discrete by auto show "D1 j \ (?\1' (J1.dom j)) = ?\1' j" using 1 j J.arr_char D1.is_discrete comp_cod_arr by simp show "?\1' (J1.cod j) \ A1'.map j = ?\1' j" using 0 j J.arr_char D1.is_discrete comp_arr_dom by simp qed define f0 where "f0 = \0.induced_arrow a' ?\0'" define f1 where "f1 = \1.induced_arrow a' ?\1'" have f0: "\f0 : a' \ a0\" using f0_def \0.induced_arrowI \0'.cone_axioms by simp have f1: "\f1 : a' \ a1\" using f1_def \1.induced_arrowI \1'.cone_axioms by simp have 2: "a0xa1.is_rendered_commutative_by f0 f1" using f0 f1 by auto interpret p0p1: binary_product_cone C a0 a1 p0 p1 .. interpret f0f1: cone X.comp C a0xa1.map a' \a0xa1.mkCone f0 f1\ using 2 f0 f1 a0xa1.cone_mkCone [of f0 f1] by auto define f where "f = p0p1.induced_arrow a' (a0xa1.mkCone f0 f1)" have f: "\f : a' \ ?a\" using f_def 2 f0 f1 p0p1.induced_arrowI'(1) by auto moreover have \': "D.cones_map f ?\ = \'" proof fix j show "D.cones_map f ?\ j = \' j" proof (cases "J0.arr j", cases "J1.arr j") show "\J0.arr j; J1.arr j\ \ D.cones_map f ?\ j = \' j" using assms(4) by auto show "\J0.arr j; \ J1.arr j\ \ D.cones_map f ?\ j = \' j" proof - assume J0: "J0.arr j" and J1: "\ J1.arr j" have "D.cones_map f ?\ j = (\0 j \ p0) \ f" using f J0 J1 \.cone_axioms by auto also have "... = \0 j \ p0 \ f" using comp_assoc by simp also have "... = \0 j \ f0" using 2 f0 f1 f_def p0p1.induced_arrowI' by auto also have "... = \' j" proof - have "\0 j \ f0 = \0 j \ \0.induced_arrow' a' \'" unfolding f0_def by simp also have "... = (\j. if J0.arr j then \0 j \ \0.induced_arrow a' (\i. if i \ Collect J0.arr then \' i else null) else null) j" using J0 by simp also have "... = D0.mkCone \' j" proof - have "(\j. if J0.arr j then \0 j \ \0.induced_arrow a' (\i. if i \ Collect J0.arr then \' i else null) else null) = D0.mkCone \'" using f0 f0_def \0.induced_arrowI(2) [of ?\0' a'] J0 D0.mkCone_cone \0'.cone_axioms \0.cone_axioms J0 by auto thus ?thesis by meson qed also have "... = \' j" using J0 by simp finally show ?thesis by blast qed finally show ?thesis by simp qed show "\ J0.arr j \ D.cones_map f ?\ j = \' j" proof (cases "J1.arr j") show "\\ J0.arr j; \ J1.arr j\ \ D.cones_map f ?\ j = \' j" using f \.cone_axioms \'.is_extensional by auto show "\\ J0.arr j; J1.arr j\ \ D.cones_map f ?\ j = \' j" proof - assume J0: "\ J0.arr j" and J1: "J1.arr j" have "D.cones_map f ?\ j = (\1 j \ p1) \ f" using J0 J1 f \.cone_axioms by auto also have "... = \1 j \ p1 \ f" using comp_assoc by simp also have "... = \1 j \ f1" using 2 f0 f1 f_def p0p1.induced_arrowI' by auto also have "... = \' j" proof - have "\1 j \ f1 = \1 j \ \1.induced_arrow' a' \'" unfolding f1_def by simp also have "... = (\j. if J1.arr j then \1 j \ \1.induced_arrow a' (\i. if i \ Collect J1.arr then \' i else null) else null) j" using J1 by simp also have "... = D1.mkCone \' j" proof - have "(\j. if J1.arr j then \1 j \ \1.induced_arrow a' (\i. if i \ Collect J1.arr then \' i else null) else null) = D1.mkCone \'" using f1 f1_def \1.induced_arrowI(2) [of ?\1' a'] J1 D1.mkCone_cone [of a' \'] \1'.cone_axioms \1.cone_axioms J1 by auto thus ?thesis by meson qed also have "... = \' j" using J1 by simp finally show ?thesis by blast qed finally show ?thesis by simp qed qed qed qed ultimately show "\f : a' \ ?a\ \ D.cones_map f ?\ = \'" by blast show "\f'. \f' : a' \ ?a\ \ D.cones_map f' ?\ = \' \ f' = f" proof - fix f' assume f': "\f' : a' \ ?a\ \ D.cones_map f' ?\ = \'" let ?f0' = "p0 \ f'" let ?f1' = "p1 \ f'" have 1: "a0xa1.is_rendered_commutative_by ?f0' ?f1'" using f' p0 p1 p0p1.renders_commutative seqI' by auto have f0': "\?f0' : a' \ a0\" using f' p0 by auto have f1': "\?f1' : a' \ a1\" using f' p1 by auto have "p0 \ f = p0 \ f'" proof - have "D0.cones_map (p0 \ f) \0 = ?\0'" using f p0 \0.cone_axioms \' \.cone_axioms comp_assoc assms(4) seqI' by fastforce moreover have "D0.cones_map (p0 \ f') \0 = ?\0'" using f' p0 \0.cone_axioms \.cone_axioms comp_assoc assms(4) seqI' by fastforce moreover have "p0 \ f = f0" using 2 f0 f_def p0p1.induced_arrowI'(2) by blast ultimately show ?thesis using f0 f0' \0'.cone_axioms \0.is_universal [of a'] by auto qed moreover have "p1 \ f = p1 \ f'" proof - have "D1.cones_map (p1 \ f) \1 = ?\1'" proof fix j show "D1.cones_map (p1 \ f) \1 j = ?\1' j" using f p1 \1.cone_axioms \' \.cone_axioms comp_assoc assms(4) seqI' apply auto by auto qed moreover have "D1.cones_map (p1 \ f') \1 = ?\1'" proof fix j show "D1.cones_map (p1 \ f') \1 j = ?\1' j" using f' p1 \1.cone_axioms \.cone_axioms comp_assoc assms(4) seqI' apply auto by auto qed moreover have "p1 \ f = f1" using 2 f1 f_def p0p1.induced_arrowI'(3) by blast ultimately show ?thesis using f1 f1' \1'.cone_axioms \1.is_universal [of a'] by auto qed ultimately show "f' = f" using f f' p0p1.is_universal' [of a'] by (metis (no_types, lifting) "1" dom_comp in_homE p0p1.is_universal' p1 seqI') qed qed qed qed show "has_as_product J.comp ?D ?a" unfolding has_as_product_def using \.product_cone_axioms by auto qed end sublocale cartesian_category \ category_with_finite_products proof obtain t where t: "terminal t" using has_terminal by blast { fix n :: nat have "\I :: nat set. finite I \ card I = n \ has_products I" proof (induct n) show "\I :: nat set. finite I \ card I = 0 \ has_products I" proof - fix I :: "nat set" assume "finite I \ card I = 0" hence I: "I = {}" by force thus "has_products I" proof - interpret J: discrete_category I 0 apply unfold_locales using I by auto have "\D. discrete_diagram J.comp C D \ \a. has_as_product J.comp D a" proof - fix D assume D: "discrete_diagram J.comp C D" interpret D: discrete_diagram J.comp C D using D by auto interpret D: empty_diagram J.comp C D using I J.arr_char by unfold_locales simp have "has_as_product J.comp D t" using t D.has_as_limit_iff_terminal has_as_product_def product_cone_def J.category_axioms category_axioms D.discrete_diagram_axioms by metis thus "\a. has_as_product J.comp D a" by blast qed moreover have "I \ UNIV" using I by blast ultimately show ?thesis using I has_products_def by (metis category_with_terminal_object.has_terminal discrete_diagram.product_coneI discrete_diagram_def empty_diagram.has_as_limit_iff_terminal empty_diagram.intro empty_diagram_axioms.intro empty_iff has_as_product_def is_category_with_terminal_object mem_Collect_eq) qed qed show "\n I :: nat set. \ (\I :: nat set. finite I \ card I = n \ has_products I); finite I \ card I = Suc n \ \ has_products I" proof - fix n :: nat fix I :: "nat set" assume IH: "\I :: nat set. finite I \ card I = n \ has_products I" assume I: "finite I \ card I = Suc n" show "has_products I" proof - have "card I = 1 \ has_products I" using I has_unary_products by blast moreover have "card I \ 1 \ has_products I" proof - assume "card I \ 1" hence cardI: "card I > 1" using I by simp obtain i where i: "i \ I" using cardI by fastforce let ?I0 = "{i}" and ?I1 = "I - {i}" have 1: "I = ?I0 \ ?I1 \ ?I0 \ ?I1 = {} \ card ?I0 = 1 \ card ?I1 = n" using i I cardI by auto show "has_products I" proof (unfold has_products_def, intro conjI allI impI) show "I \ UNIV" using I by auto fix J D assume D: "discrete_diagram J C D \ Collect (partial_magma.arr J) = I" interpret D: discrete_diagram J C D using D by simp have Null: "D.J.null \ ?I0 \ D.J.null \ ?I1" using D D.J.not_arr_null i by blast interpret J0: discrete_category ?I0 D.J.null using 1 Null D by unfold_locales auto interpret J1: discrete_category ?I1 D.J.null using Null by unfold_locales auto interpret J0uJ1: discrete_category \Collect J0.arr \ Collect J1.arr\ J0.null using Null 1 J0.null_char J1.null_char by unfold_locales auto interpret D0: discrete_diagram_from_map ?I0 C D D.J.null using 1 J0.ide_char D.preserves_ide D D.is_discrete i by unfold_locales auto interpret D1: discrete_diagram_from_map ?I1 C D D.J.null using 1 J1.ide_char D.preserves_ide D D.is_discrete i by unfold_locales auto obtain a0 where a0: "has_as_product J0.comp D0.map a0" using 1 has_unary_products [of ?I0] has_products_def [of ?I0] D0.discrete_diagram_axioms by fastforce obtain a1 where a1: "has_as_product J1.comp D1.map a1" using 1 I IH [of ?I1] has_products_def [of ?I1] D1.discrete_diagram_axioms by blast have 2: "\p0 p1. has_as_binary_product a0 a1 p0 p1" proof - have "ide a0 \ ide a1" using a0 a1 product_is_ide by auto thus ?thesis using a0 a1 has_binary_products has_binary_products_def by simp qed obtain p0 p1 where a: "has_as_binary_product a0 a1 p0 p1" using 2 by auto let ?a = "dom p0" have "has_as_product J D ?a" proof - have "D = (\j. if j \ Collect J0.arr then D0.map j else if j \ Collect J1.arr then D1.map j else null)" proof fix j show "D j = (if j \ Collect J0.arr then D0.map j else if j \ Collect J1.arr then D1.map j else null)" using 1 D0.map_def D1.map_def D.is_extensional D J0.arr_char J1.arr_char by auto qed moreover have "J = J0uJ1.comp" proof - have "\j j'. J j j' = J0uJ1.comp j j'" proof - fix j j' show "J j j' = J0uJ1.comp j j'" using D J0uJ1.arr_char J0.arr_char J1.arr_char D.is_discrete i apply (cases "j \ ?I0", cases "j' \ ?I0") apply simp_all apply auto[1] apply (metis D.J.comp_arr_ide D.J.comp_ide_arr D.J.ext D.J.seqE D.is_discrete J0.null_char J0uJ1.null_char) by (metis D.J.comp_arr_ide D.J.comp_ide_arr D.J.comp_ide_self D.J.ext D.J.seqE D.is_discrete J0.null_char J0uJ1.null_char mem_Collect_eq) qed thus ?thesis by blast qed moreover have "Collect J0.arr \ Collect J1.arr = {}" by auto moreover have "J0.null = J1.null" using J0.null_char J1.null_char by simp ultimately show "has_as_product J D ?a" using binary_product_of_products_is_product [of J0.comp D0.map a0 J1.comp D1.map a1 p0 p1] J0.arr_char J1.arr_char 1 a0 a1 a by simp qed thus "\a. has_as_product J D a" by blast qed qed ultimately show "has_products I" by blast qed qed qed } hence 1: "\n I :: nat set. finite I \ card I = n \ has_products I" by simp thus "\I :: nat set. finite I \ has_products I" by blast qed proposition (in cartesian_category) is_category_with_finite_products: shows "category_with_finite_products C" .. end