Theory CartesianCategory

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

chapter "Cartesian Category"

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

theory CartesianCategory
imports Limit SetCat CategoryWithPullbacks
begin

  section "Category with Binary Products"

  subsection "Binary Product Diagrams"

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

  locale binary_product_shape
  begin

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

    abbreviation comp
    where "comp  COMP"

    abbreviation FF
    where "FF  MkIde False"

    abbreviation TT
    where "TT  MkIde True"

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

    lemma ide_char:
    shows "ide f  f = FF  f = TT"
      using ide_charCC ide_MkIde by (cases f, auto)

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

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

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

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

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

  end

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

    notation J.comp      (infixr "J" 55)

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

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

  end

  subsection "Category with Binary Products"

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

  context binary_product_diagram
  begin

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

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

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

    lemma cone_mkCone:
    assumes "is_rendered_commutative_by p0 p1"
    shows "cone (C.dom p0) (mkCone p0 p1)"
    proof -
      interpret E: constant_functor J.comp C C.dom p0
        using assms by unfold_locales auto
      show "cone (C.dom p0) (mkCone p0 p1)"
        using assms mkCone_def J.arr_char E.map_simp is_discrete C.comp_ide_arr C.comp_arr_dom
        by unfold_locales auto
    qed

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

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

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

    lemma cones_map_mkCone_eq_iff:
    assumes "is_rendered_commutative_by p0 p1" and "is_rendered_commutative_by p0' p1'"
    and "«h : C.dom p0'  C.dom p0»"
    shows "cones_map h (mkCone p0 p1) = mkCone p0' p1'  p0  h = p0'  p1  h = p1'"
    proof -
      interpret χ: cone J.comp C map C.dom p0 mkCone p0 p1
        using assms(1) cone_mkCone [of p0 p1] by blast
      interpret χ': cone J.comp C map C.dom p0' mkCone p0' p1'
        using assms(2) cone_mkCone [of p0' p1'] by blast
      show ?thesis
      proof
        assume 1: "cones_map h (mkCone p0 p1) = mkCone p0' p1'"
        show "p0  h = p0'  p1  h = p1'"
        proof
          show "p0  h = p0'"
          proof -
            have "p0' = cones_map h (mkCone p0 p1) J.FF"
              using 1 mkCone_def J.arr_char by simp
            also have "... = p0  h"
              using assms mkCone_def J.arr_char χ.cone_axioms by auto
            finally show ?thesis by auto
          qed
          show "p1  h = p1'"
          proof -
            have "p1' = cones_map h (mkCone p0 p1) J.TT"
              using 1 mkCone_def J.arr_char by simp
            also have "... = p1  h"
              using assms mkCone_def J.arr_char χ.cone_axioms by auto
            finally show ?thesis by auto
          qed
        qed
        next
        assume "p0  h = p0'  p1  h = p1'"
        thus "cones_map h (mkCone p0 p1) = mkCone p0' p1'"
          using assms χ.cone_axioms mkCone_def J.arr_char by auto
      qed
    qed

  end

  locale binary_product_cone =
    J: binary_product_shape +
    C: category C +
    D: binary_product_diagram C f0 f1 +
    limit_cone J.comp C D.map C.dom p0 D.mkCone p0 p1
  for C :: "'c comp"      (infixr "" 55)
  and f0 :: 'c
  and f1 :: 'c
  and p0 :: 'c
  and p1 :: 'c
  begin

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

    lemma is_universal':
    assumes "D.is_rendered_commutative_by p0' p1'"
    shows "∃!h. «h : C.dom p0'  C.dom p0»  p0  h = p0'  p1  h = p1'"
    proof -
      have "D.cone (C.dom p0') (D.mkCone p0' p1')"
        using assms D.cone_mkCone by blast
      hence "∃!h. «h : C.dom p0'  C.dom p0» 
                  D.cones_map h (D.mkCone p0 p1) = D.mkCone p0' p1'"
        using is_universal by simp
      moreover have "h. «h : C.dom p0'  C.dom p0» 
                           D.cones_map h (D.mkCone p0 p1) = D.mkCone p0' p1' 
                           p0  h = p0'  p1  h = p1'"
        using assms D.cones_map_mkCone_eq_iff [of p0 p1 p0' p1'] renders_commutative
        by blast
      ultimately show ?thesis by blast
    qed

    lemma induced_arrowI':
    assumes "D.is_rendered_commutative_by p0' p1'"
    shows "«induced_arrow (C.dom p0') (D.mkCone p0' p1') : C.dom p0'  C.dom p0»"
    and "p0  induced_arrow (C.dom p0') (D.mkCone p0' p1') = p0'"
    and "p1  induced_arrow (C.dom p1') (D.mkCone p0' p1') = p1'"
    proof -
      interpret A': constant_functor J.comp C C.dom p0'
        using assms by (unfold_locales, auto)
      have cone: "D.cone (C.dom p0') (D.mkCone p0' p1')"
        using assms D.cone_mkCone [of p0' p1'] by blast
      show 0: "p0  induced_arrow (C.dom p0') (D.mkCone p0' p1') = p0'"
      proof -
        have "p0  induced_arrow (C.dom p0') (D.mkCone p0' p1') =
                D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1')) (D.mkCone p0 p1) J.FF"
          using cone induced_arrowI(1) D.mkCone_def J.arr_char is_cone by force
        also have "... = p0'"
          by (metis (no_types, lifting) D.mkCone_def cone induced_arrowI(2)
              mem_Collect_eq restrict_apply)
        finally show ?thesis by auto
      qed
      show "p1  induced_arrow (C.dom p1') (D.mkCone p0' p1') = p1'"
      proof -
        have "p1  induced_arrow (C.dom p1') (D.mkCone p0' p1') =
                D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1')) (D.mkCone p0 p1) J.TT"
          using assms cone induced_arrowI(1) D.mkCone_def J.arr_char is_cone by fastforce
        also have "... = p1'"
        proof -
          have "D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1')) (D.mkCone p0 p1) =
                D.mkCone p0' p1'"
            using cone induced_arrowI by blast
          thus ?thesis
            using J.arr_char D.mkCone_def by simp
        qed
        finally show ?thesis by auto
      qed
      show "«induced_arrow (C.dom p0') (D.mkCone p0' p1') : C.dom p0'  C.dom p0»"
        using 0 cone induced_arrowI by simp
    qed

  end

  context category
  begin

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

    definition has_binary_products
    where "has_binary_products =
           (a0 a1. ide a0  ide a1  (p0 p1. has_as_binary_product a0 a1 p0 p1))"

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

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

  end

  locale category_with_binary_products =
    category +
  assumes has_binary_products: has_binary_products

  subsection "Elementary Category with Binary Products"

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

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

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

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

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

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

    text ‹
      The following defines product of arrows (not just of objects).  It will take a little
      while before we can prove that it is functorial, but for right now it is nice to have
      it as a notation for the apex of a product cone.  We have to go through some slightly
      unnatural contortions in the development here, though, to avoid having to introduce a
      separate preliminary notation just for the product of objects.
    ›
    (* 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 "span 𝔭1[a, b] 𝔭0[a, b]" and "cod 𝔭1[a, b] = a" and "cod 𝔭0[a, b] = b"
        using assms by auto
      fix x f g
      assume f: "«f : x  a»" and g: "«g : x  b»"
      have "span f g"
        using f g by auto
      hence "∃!l. 𝔭1[a, b]  l = f  𝔭0[a, b]  l = g"
        using assms f g universal [of f g]
        by (metis in_homE)
      thus "∃!h. «h : x  dom 𝔭1[a, b]»  𝔭1[a, b]  h = f  𝔭0[a, b]  h = g"
        using f by blast
    qed

  end

  lemma (in category) elementary_category_with_binary_productsI:
  assumes "a b. ide a; ide b  has_as_binary_product a b (p a b) (q a b)"
  shows "elementary_category_with_binary_products C
           (λa b. if ide a  ide b then q a b else null)
           (λa b. if ide a  ide b then p a b else null)"
  proof -
    let ?p = "λa b. if ide a  ide b then p a b else null"
    let ?q = "λa b. if ide a  ide b then q a b else null"
    show ?thesis
    proof
      fix a b
      assume a: "ide a" and b: "ide b"
      show "span (?p a b) (?q a b)"
        using assms a b
        by auto force
      show "cod (?q a b) = b"
        using a b assms has_as_binary_productE by auto
      show "cod (?p a b) = a"
        using a b assms has_as_binary_productE by auto
      next
      fix f g
      assume fg: "span f g"
      have 1: "has_as_binary_product (cod f) (cod g)
                 (p (cod f) (cod g)) (q (cod f) (cod g))"
        using assms fg by simp
      obtain l where "p (cod f) (cod g)  l = f  q (cod f) (cod g)  l = g"
        using 1 fg has_as_binary_productE
        by (metis in_homI)
      hence "l. ?p (cod f) (cod g)  l = f  ?q (cod f) (cod g)  l = g"
        using fg by auto
      moreover have
        "l l'. ?p (cod f) (cod g)  l = f  ?q (cod f) (cod g)  l = g 
                 ?p (cod f) (cod g)  l' = f  ?q (cod f) (cod g)  l' = g
                     l = l'"
        using 1 fg arr_iff_in_hom ide_cod
        by (elim has_as_binary_productE, auto) metis
      ultimately show "∃!l. ?p (cod f) (cod g)  l = f  ?q (cod f) (cod g)  l = g"
        by blast
    qed
  qed

  subsection "Agreement between the Definitions"

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

  context category_with_binary_products
  begin

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

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

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

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

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

    abbreviation some_prod    (infixr "?" 51)
    where "some_prod  prod"

  end

  locale binary_product =
    category C
    for C :: "'a comp"
    and a :: 'a
    and b :: 'a
    and p :: 'a
    and q :: 'a +
    assumes has_as_binary_product: "has_as_binary_product a b p q"
  begin

    definition product
    where "product  dom p"

    lemma ide_product [intro, simp]:
    shows "ide product"
      unfolding product_def
      using has_as_binary_product by fastforce

    lemma prj_in_hom [intro, simp]:
    shows "«p : product  a»"
    and "«q : product  b»"
      using has_as_binary_product product_def by auto

    lemma prj_simps [simp]:
    shows "dom p = product" and "cod p = a" and "dom q = product" and "cod q = b"
      using prj_in_hom by blast+

    definition tuple
    where "tuple f g  (THE h. C p h = f  C q h = g)"

    lemma tuple_props:
    assumes "span f g" and "cod f = a" and "cod g = b"
    shows [intro, simp]: "«tuple f g : dom f  product»"
    and [simp]: "dom (tuple f g) = dom f"
    and [simp]: "cod (tuple f g) = product"
    and [simp]: "C p (tuple f g) = f"
    and [simp]: "C q (tuple f g) = g"
    and "h. C p h = f; C q h = g  h = tuple f g"
    proof -
      have 0: "∃!h. C p h = f  C q h = g"
        using assms has_as_binary_product by blast
      hence *: "C p (tuple f g) = f  C q (tuple f g) = g"
        using tuple_def theI' [of "λh. C p h = f  C q h = g"] by simp
      show 1: "«tuple f g : dom f  product»"
        using assms *
        by (metis dom_comp in_homI prj_simps(3) seqE)
      show "dom (tuple f g) = dom f"
        using 1 by auto
      show "cod (tuple f g) = product"
        using 1 by auto
      show 2: "C p (tuple f g) = f"
        using * by auto
      show 3: "C q (tuple f g) = g"
        using * by auto
      show 4: "h. C p h = f; C q h = g  h = tuple f g"
        using * 0 2 3 by blast
    qed

    lemma tuple_proj:
    shows [simp]: "tuple p q = product"
      by (metis comp_arr_dom in_homE tuple_props(6) prj_in_hom(1-2))

    lemma pr_joint_monic:
    assumes "seq p x" and "seq p y" and "C p x = C p y" and "C q x = C q y"
    shows "x = y"
      by (metis (mono_tags, lifting) assms(1,3-4) cod_comp dom_comp tuple_props(6)
          product_def arrI prj_in_hom(2) prj_simps(2-4) seqE seqI)

  end

  lemma (in category) binary_products_are_isomorphic:
  assumes "has_as_binary_product a b p q" and "has_as_binary_product a b p' q'"
  shows "isomorphic (dom p) (dom p')"
  and "inverse_arrows (binary_product.tuple C p q p' q')
                      (binary_product.tuple C p' q' p q)"
  proof -
    show "isomorphic (dom p) (dom p')"
      using assms limits_are_isomorphic(1)
      unfolding has_as_binary_product_def by blast
    interpret pq: binary_product C a b p q
      using assms(1) by unfold_locales auto
    interpret p'q': binary_product C a b p' q'
      using assms(2) by unfold_locales auto
    show "inverse_arrows (pq.tuple p' q') (p'q'.tuple p q)"
    proof
      show "ide (p'q'.tuple p q  pq.tuple p' q')"
      proof -
        have "p'  p'q'.tuple p q  pq.tuple p' q' = p'  p'q'.product 
              q'  p'q'.tuple p q  pq.tuple p' q' = q'  p'q'.product"
          using pq.tuple_props [of p' q'] p'q'.tuple_props [of p q]
                comp_assoc
          by (metis arrI comp_arr_dom p'q'.prj_in_hom(1-2) p'q'.prj_simps(2-4)
              p'q'.product_def pq.prj_in_hom(1-2) pq.prj_simps(2-4) pq.product_def)
        thus ?thesis
          by (metis comp_arr_dom p'q'.ide_product p'q'.tuple_props(6)
              p'q'.prj_in_hom(1-2) p'q'.prj_simps(1-4) arrI)
      qed
      show "ide (pq.tuple p' q'  p'q'.tuple p q)"
      proof -
        have "p  pq.tuple p' q'  p'q'.tuple p q = p  pq.product 
              q  pq.tuple p' q'  p'q'.tuple p q = q  pq.product"
          using pq.tuple_props [of p' q'] p'q'.tuple_props [of p q]
                comp_assoc
            by (metis arrI comp_arr_dom p'q'.prj_in_hom(1-2) p'q'.prj_simps(2-4)
                p'q'.product_def pq.prj_in_hom(1-2) pq.prj_simps(2-4)
                pq.product_def)
        thus ?thesis
          by (metis arrI comp_arr_dom ide_char' pq.tuple_props(6) pq.prj_in_hom(1-2)
              pq.prj_simps(2-4) pq.product_def seqE)
      qed
    qed
  qed

  context elementary_category_with_binary_products
  begin

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

    proposition is_category_with_binary_products:
    shows "category_with_binary_products C"
      ..

  end

  subsection "Further Properties"

  context elementary_category_with_binary_products
  begin

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

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

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

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

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

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

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

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

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

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

    definition assoc ("𝖺[_, _, _]")
    where "𝖺[a, b, c]  𝔭1[a, b]  𝔭1[a  b, c], 𝔭0[a, b]  𝔭1[a  b, c], 𝔭0[a  b, c]"

    definition assoc' ("𝖺-1[_, _, _]")
    where "𝖺-1[a, b, c]  𝔭1[a, b  c], 𝔭1[b, c]  𝔭0[a, b  c], 𝔭0[b, c]  𝔭0[a, b  c]"

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

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

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

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

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

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

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

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

    lemma inverse_arrows_assoc:
    assumes "ide a" and "ide b" and "ide c"
    shows "inverse_arrows 𝖺[a, b, c] 𝖺-1[a, b, c]"
      using assms assoc_def assoc'_def comp_assoc
      by (auto simp add: tuple_pr_arr)

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

    interpretation CC: product_category C C ..

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

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

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

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

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

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

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

    interpretation α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α
    proof
      fix f
      show "¬ CCC.arr f  α f = null"
        by (metis CC.arr_char CCC.arr_char ext prod_def seqE tuple_ext)
      assume f: "CCC.arr f"
      show "dom (α f) = T.ToTC (CCC.dom f)"
        using f by auto
      show "cod (α f) = T.ToCT (CCC.cod f)"
        using f by auto
      show "T.ToCT f  α (CCC.dom f) = α f"
        using f T.ToCT_def T.ToTC_def comp_assoc
              assoc_naturality
                [of "fst f" "dom (fst f)" "cod (fst f)"
                    "fst (snd f)" "dom (fst (snd f))" "cod (fst (snd f))"
                    "snd (snd f)" "dom (snd (snd f))" "cod (snd (snd f))"]
        by (simp add: comp_arr_dom in_homI)
      show "α (CCC.cod f)  T.ToTC f = α f"
        using T.ToTC_def comp_arr_dom f by auto
      next
      show "a. CCC.ide a  iso (α a)"
        using CCC.ide_charPC CC.ide_charPC 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

  lemma (in category_with_terminal_object) binary_product_is_pullback:
  assumes "has_as_binary_product a b p q"
  shows "has_as_pullback 𝗍?[a] 𝗍?[b] p q"
  proof
    interpret elementary_category_with_terminal_object C 𝟭? λa. 𝗍?[a]
      using extends_to_elementary_category_with_terminal_object by blast
    show "cospan 𝗍?[a] 𝗍?[b]"
      using assms by fastforce
    show "commutative_square 𝗍?[a] 𝗍?[b] p q"
      using assms trm_naturality by fastforce
    show "h k. commutative_square 𝗍?[a] 𝗍?[b] h k  ∃!l. p  l = h  q  l = k"
    proof -
      fix h k
      assume 1: "commutative_square 𝗍?[a] 𝗍?[b] h k"
      have "«h : dom h  a»  «k : dom h  b»"
        by (metis 1 commutative_square 𝗍?[a] 𝗍?[b] p q arr_iff_in_hom assms
            commutative_squareE has_as_binary_productE in_homE)
      thus "∃!l. p  l = h  q  l = k"
        using assms has_as_binary_productE [of a b p q] by metis
    qed
  qed

  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 "span p0 p1"
              using p0p1 by blast
            show "cod p0 = a0" and "cod 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 p0»"
              using f g by blast
            ultimately show "∃!l. «l : x  dom p0»  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 "𝗅[a]  𝔭0[𝟭, a]"

    abbreviation lunit' ("𝗅-1[_]")
    where "𝗅-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 "«𝗋-1[a] : a  a  𝟭»"
      using assms ide_in_hom trm_in_hom 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 "«𝗅-1[a] : a  𝟭  a»"
      using assms ide_in_hom trm_in_hom by blast

    lemma runit_naturality:
    assumes "arr f"
    shows "𝗋[cod f]  (f  𝟭) = f  𝗋[dom f]"
      using assms pr_naturality(2) ide_char ide_one by blast

    lemma inverse_arrows_runit:
    assumes "ide a"
    shows "inverse_arrows 𝗋[a] 𝗋-1[a]"
    proof
      show "ide (𝗋[a]  𝗋-1[a])"
        using assms by auto
      show "ide (𝗋-1[a]  𝗋[a])"
      proof -
        have "ide (a  𝟭)"
          using assms ide_one by blast
        moreover have "𝗋-1[a]  𝗋[a] = a  𝟭"
        proof (intro pr_joint_monic [of a 𝟭 "𝗋-1[a]  𝗋[a]" "a  𝟭"])
          show "ide a" by fact
          show "ide 𝟭"
            using ide_one by blast
          show "seq 𝔭0[a, 𝟭] (𝗋-1[a]  𝗋[a])"
            using assms ide_one runit'_in_hom [of a]
            by (intro seqI) auto
          show "𝔭0[a, 𝟭]  𝗋-1[a]  𝗋[a] = 𝔭0[a, 𝟭]  (a  𝟭)"
          proof -
            have "𝔭0[a, 𝟭]  𝗋-1[a]  𝗋[a] = (𝔭0[a, 𝟭]  𝗋-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)
            also have "... = 𝗍[a  𝟭]"
              using assms ide_one trm_naturality [of "𝗋[a]"] by simp
            also have "... = 𝔭0[a, 𝟭]  (a  𝟭)"
              by (simp add: assms ide_one trm_one trm_tensor)
            finally show ?thesis by blast
          qed
          show "𝔭1[a, 𝟭]  𝗋-1[a]  𝗋[a] = 𝔭1[a, 𝟭]  (a  𝟭)"
            using assms
            by (metis ide (𝗋[a]  𝗋-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] 𝗅-1[a]"
    proof
      show "ide (C 𝗅[a] 𝗅-1[a])"
        using assms by auto
      show "ide (𝗅-1[a]  𝗅[a])"
      proof -
        have "𝗅-1[a]  𝗅[a] = 𝟭  a"
        proof (intro pr_joint_monic [of 𝟭 a "𝗅-1[a]  𝗅[a]" "𝟭  a"])
          show "ide a" by fact
          show "ide 𝟭"
            using ide_one by blast
          show "seq 𝗅[a] (𝗅-1[a]  𝗅[a])"
            using assms ide (𝗅[a]  𝗅-1[a]) by blast
          show "𝗅[a]  𝗅-1[a]  𝗅[a] = 𝗅[a]  (𝟭  a)"
            using assms
            by (metis ide (𝗅[a]  𝗅-1[a]) cod_comp cod_pr0 dom_cod ide_compE ide_one
                comp_assoc lunit_naturality)
          show "𝔭1[𝟭, a]  𝗅-1[a]  𝗅[a] = 𝔭1[𝟭, a]  (𝟭  a)"
          proof -
            have "𝔭1[𝟭, a]  𝗅-1[a]  𝗅[a] = (𝔭1[𝟭, a]  𝗅-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)
            also have "... = 𝗍[𝟭  a]"
              using assms ide_one trm_naturality [of "𝗅[a]"] by simp
            also have "... = 𝔭1[𝟭, a]  (𝟭  a)"
              by (simp add: assms ide_one pr_coincidence trm_one trm_tensor)
            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 pr_expansion:
    assumes "ide a" and "ide b"
    shows "𝔭0[a, b] = 𝗅[b]  (𝗍[a]  b)" and "𝔭1[a, b] = 𝗋[a]  (a  𝗍[b])"
      using assms
      by (auto simp add: comp_ide_arr)

    lemma comp_lunit_term_dup:
    assumes "ide a"
    shows "𝗅[a]  (𝗍[a]  a)  𝖽[a] = a"
      using assms prod_tuple by force

    lemma comp_runit_term_dup:
    assumes "ide a"
    shows "𝗋[a]  (a  𝗍[a])  𝖽[a] = a"
      using assms prod_tuple by force

    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 "ide a" by fact
      show "ide (a  a)"
        by (simp add: assms)
      show "seq 𝔭0[a, a  a] (𝖺[a, a, a]  (𝖽[a]  a)  𝖽[a])"
        using assms by simp
      show "𝔭0[a, a  a]  𝖺[a, a, a]  (𝖽[a]  a)  𝖽[a] = 𝔭0[a, a  a]  (a  𝖽[a])  𝖽[a]"
      proof -
        have "𝔭0[a, a  a]  𝖺[a, a, a]  (𝖽[a]  a)  𝖽[a] =
              ((𝔭0[a, a  a]  𝖺[a, a, a])  (𝖽[a]  a))  𝖽[a]"
          using comp_assoc by simp
        also have "... = ((𝔭0[a, a]  𝔭1[a  a, a])  (𝖽[a]  a))  𝖽[a], (a  𝔭0[a, a])  𝖽[a]"
          using assms assoc_def by simp
        also have "... = 𝖽[a]"
          using assms comp_assoc by simp
        also have "... = (𝔭0[a, a  a]  (a  𝖽[a]))  𝖽[a]"
          using assms assoc_def comp_assoc by simp
        also have "... = 𝔭0[a, a  a]  (a  𝖽[a])  𝖽[a]"
          using comp_assoc by simp
        finally show ?thesis by blast
      qed
      show "𝔭1[a, a  a]  𝖺[a, a, a]  (𝖽[a]  a)  𝖽[a] = 𝔭1[a, a  a]  (a  𝖽[a])  𝖽[a]"
      proof -
        have "𝔭1[a, a  a]  𝖺[a, a, a]  (𝖽[a]  a)  𝖽[a] =
              ((𝔭1[a, a  a]  𝖺[a, a, a])  (𝖽[a]  a))  𝖽[a]"
          using comp_assoc by simp
        also have "... = ((𝔭1[a, a]  𝔭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  𝔭1[a, a])  𝖽[a]"
          using assms comp_assoc by simp
        also have "... = (𝔭1[a, a  a]  (a  𝖽[a]))  𝖽[a]"
          using assms by simp
        also have "... = 𝔭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 "𝖺-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] = 𝖺-1[a, b, a  b]  (a  𝖺[b, a, b])  (a  σ (a, b)  b) 
                        (a  𝖺-1[a, b, b])  𝖺[a, a, b  b]  (𝖽[a]  𝖽[b])"
    proof (intro pr_joint_monic [of "a  b" "a  b" "𝖽[a  b]"])
      show "ide (a  b)" and "ide (a  b)"
        by (auto simp add: assms)
      show "seq 𝔭0[a  b, a  b] (𝖽[a  b])"
        using assms by simp
      have 1: "𝖺-1[a, b, a  b]  (a  𝖺[b, a, b])  (a  σ (a, b)  b) 
                 (a  𝖺-1[a, b, b])  𝖺[a, a, b  b]  (𝖽[a]  𝖽[b]) =
               a  b, a  b"
      proof -
        have "𝖺-1[a, b, a  b]  (a  𝖺[b, a, b])  (a  σ (a, b)  b) 
              (a  𝖺-1[a, b, b])  𝖺[a, a, b  b]  (𝖽[a]  𝖽[b])
                = 𝖺-1[a, b, a  b]  (a  𝖺[b, a, b])  (a  σ (a, b)  b) 
                  (a  𝖺-1[a, b, b])  𝔭1[a, b], 𝔭1[a, b], 𝖽[b]  𝔭0[a, b]"
        proof -
          have "𝖺[a, a, b  b]  (𝖽[a]  𝖽[b]) = 𝔭1[a, b], 𝔭1[a, b], 𝖽[b]  𝔭0[a, b]"
            using assms assoc_def comp_assoc pr_naturality comp_cod_arr by simp
          thus ?thesis by presburger
        qed
        also have "... = 𝖺-1[a, b, a  b] 
                           a  a  a  𝔭1[a, b],
                            𝖺[b, a, b]  (𝗌[a, b]  (a  b)  b) 
                              𝖺-1[a, b, b]  𝔭1[a, b], 𝖽[b  𝔭0[a, b]]"
          using assms prod_tuple by simp
        also have "... = 𝖺-1[a, b, a  b] 
                           𝔭1[a, b],
                            𝖺[b, a, b]  (𝗌[a, b]  b)  𝖺-1[a, b, b]  𝔭1[a, b], 𝖽[𝔭0[a, b]]"
        proof -
          have "a  a  a  𝔭1[a, b] = 𝔭1[a, b]"
            using assms comp_cod_arr by simp
          moreover have "b  𝔭0[a, b] = 𝔭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 "... = 𝖺-1[a, b, a  b]  𝔭1[a, b], 𝖺[b, a, b]  (𝗌[a, b]  b) 
                           𝔭1[a, b], 𝔭0[a, b], 𝔭0[a, b]"
        proof -
          have "𝖺-1[a, b, b]  𝔭1[a, b], 𝖽[𝔭0[a, b]] = 𝔭1[a, b], 𝔭0[a, b], 𝔭0[a, b]"
            using assms comp_assoc_tuple(2) by blast
          thus ?thesis by simp
        qed
        also have "... = 𝖺-1[a, b, a  b]  𝔭1[a, b], 𝖺[b, a, b]  𝗌[a, b], 𝔭0[a, b]"
          using assms prod_tuple comp_arr_dom comp_cod_arr by simp
        also have "... = 𝖺-1[a, b, a  b]  𝔭1[a, b], 𝔭0[a, b], 𝔭1[a, b], 𝔭0[a, b]"
          using assms comp_assoc_tuple(1)
          by (metis sym_def pr_in_hom)
        also have "... = 𝔭1[a, b], 𝔭0[a, b], 𝔭1[a, b], 𝔭0[a, b]"
          using assms comp_assoc_tuple(2)
          by (metis ide (a  b) ide_in_hom pr_in_hom tuple_pr)
        also have "... = 𝖽[a  b]"
          using assms by simp
        finally show ?thesis by simp
      qed
      show "𝔭0[a  b, a  b]  𝖽[a  b]
              = 𝔭0[a  b, a  b] 
                𝖺-1[a, b, a  b]  (a  𝖺[b, a, b])  (a  σ (a, b)  b) 
                (a  𝖺-1[a, b, b])  𝖺[a, a, b  b]  (𝖽[a]  𝖽[b])"
        using assms 1 by force
      show "𝔭1[a  b, a  b]  𝖽[a  b]
              = 𝔭1[a  b, a  b] 
                𝖺-1[a, b, a  b]  (a  𝖺[b, a, b])  (a  σ (a, b)  b) 
                (a  𝖺-1[a, b, b])  𝖺[a, a, b  b]  (𝖽[a]  𝖽[b])"
        using assms 1 by force
    qed

    (* TODO: Not sure if the following fact is useful. *)

    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
          show "f. «f : a  𝟭  𝟭»  f = inv ι  𝗍[a]"
            by (metis «local.inv ι  𝗍[a] : a  𝟭  𝟭» a in_homE ide_one pr_coincidence
                pr_joint_monic trm_naturality trm_simps(1) unit_eq_trm)
        qed
      qed
    qed

  end

subsection "Exponentials"

  text ‹
    The following prepare the way for the definition of cartesian closed categories.
    The notion of exponential has to be defined in relation to products.
    Here we use a generic choice of products for this purpose.
  ›

  context cartesian_category
  begin

    definition has_as_exponential
    where "has_as_exponential b c x e 
           ide b  ide x  «e : some_prod x b  c» 
           (a g. ide a  «g : some_prod a b  c» 
                    (∃!f. «f : a  x»  g = C e (some_prod f b)))"

    lemma has_as_exponentialI [intro]:
    assumes "ide b" and "ide x" and "«e : some_prod x b  c»"
    and "a g. ide a; «g : some_prod a b  c»  ∃!f. «f : a  x»  g = C e (some_prod f b)"
    shows "has_as_exponential b c x e"
      using assms has_as_exponential_def by simp

    lemma has_as_exponentialE [elim]:
    assumes "has_as_exponential b c x e"
    and "ide b; ide x; «e : some_prod x b  c»;
          a g. ide a; «g : some_prod a b  c»  ∃!f. «f : a  x»  g = C e (some_prod f b)
              T"
    shows T
      using assms has_as_exponential_def by simp

    lemma exponentials_are_isomorphic:
    assumes "has_as_exponential b c x e" and "has_as_exponential b c x' e'"
    shows "∃!h. «h : x  x'»  e = e'  some_prod h b"
    and "h. «h : x  x'»; e = e'  (some_prod h b)  iso h"
    proof -
      have "ide b  ide c"
        using assms(1) has_as_exponential_def by auto
      have "ide x  «e : some_prod x b  c»"
        using assms(1) has_as_exponential_def by blast
      have "ide x'  «e' : some_prod x' b  c»"
        using assms(2) has_as_exponential_def by blast
      show 1: "∃!h. «h : x  x'»  e = e'  some_prod h b"
        using assms has_as_exponential_def by simp
      have 2: "∃!h. «h : x'  x»  e' = e  some_prod h b"
        using assms has_as_exponential_def by simp
      have 3: "∃!h. «h : x  x»  e = e  some_prod h b"
        using assms has_as_exponential_def by simp
      have 4: "∃!h. «h : x'  x'»  e' = e'  some_prod h b"
        using assms has_as_exponential_def by simp
      have 5: "h. «h : x  x»  e = e  some_prod h b  h = x"
        by (metis assms(1) 3 category.in_homE category_axioms comp_arr_dom has_as_exponential_def
            partial_composition.ide_in_hom partial_composition_axioms)
      have 6: "h. «h : x'  x'»  e' = e'  some_prod h b  h = x'"
        by (metis assms(2) 4 category.in_homE category_axioms comp_arr_dom has_as_exponential_def
            partial_composition.ide_in_hom partial_composition_axioms)
      let ?f = "THE h. «h : x'  x»  e' = e  some_prod h b"
      let ?g = "THE h. «h : x  x'»  e = e'  some_prod h b"
      have "inverse_arrows ?f ?g"
      proof
        have "?g  ?f = x'"
        proof -
          have "«?g  ?f : x'  x'»  e' = e'  some_prod ?g b  some_prod ?f b"
          proof
            show "«?g  ?f : x'  x'»"
              using 1 2 theI [of "λh. «h : x  x'»  e = e'  some_prod h b"]
                    theI [of "λh. «h : x'  x»  e' = e  some_prod h b"]
              by (meson comp_in_homI)
            show "e' = e'  some_prod ?g b  some_prod ?f b"
              using 1 2 theI [of "λh. «h : x  x'»  e = e'  some_prod h b"]
                    theI [of "λh. «h : x'  x»  e' = e  some_prod h b"]
              by (metis (no_types, lifting) comp_assoc)
          qed
          hence "«?g  ?f : x'  x'»  e' = e'  some_prod (?g  ?f) (b  b)"
            by (metis (no_types, lifting) ide b  ide c arrI ext
                elementary_category_with_binary_products.interchange
                extends_to_elementary_category_with_binary_products ide_def)
          thus ?thesis
            using 6
            by (simp add: ide b  ide c)
        qed
        thus "ide (?g  ?f)"
          using ide x'  «e' : some_prod x' b  c» by presburger
        have "?f  ?g = x"
        proof -
          have "«?f  ?g : x  x»  e = e  some_prod ?f b  some_prod ?g b"
          proof
            show "«?f  ?g : x  x»"
              using 1 2 theI [of "λh. «h : x  x'»  e = e'  some_prod h b"]
                    theI [of "λh. «h : x'  x»  e' = e  some_prod h b"]
              by (meson comp_in_homI)
            show "e = e  some_prod ?f b  some_prod ?g b"
              using 1 2 theI [of "λh. «h : x  x'»  e = e'  some_prod h b"]
                    theI [of "λh. «h : x'  x»  e' = e  some_prod h b"]
              by (metis (no_types, lifting) comp_assoc)
          qed
          hence "«?f  ?g : x  x»  e = e  some_prod (?f  ?g) (b  b)"
            by (metis (no_types, lifting) ide b  ide c arrI ext
                elementary_category_with_binary_products.interchange
                extends_to_elementary_category_with_binary_products ide_def)
          thus ?thesis
            using 5
            by (simp add: ide b  ide c)
        qed
        thus "ide (?f  ?g)"
          using ide x  «e : some_prod x b  c» by presburger
      qed
      hence "iso ?g"
        by blast
      moreover have "h. «h : x  x'»; e = e'  (some_prod h b)  h = ?g"
        using 1 theI [of "λh. «h : x  x'»  e = e'  some_prod h b"] by auto
      ultimately show "h. «h : x  x'»; e = e'  (some_prod h b)  iso h" by simp
    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 2: "a π. D.limit_cone a π"
          proof -
            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
            thus ?thesis
              unfolding product_cone_def by simp
          qed
          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_productsCFP:
  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_objectCFP:
  shows "category_with_terminal_object C"
    ..

  sublocale category_with_finite_products  cartesian_category ..

  proposition (in category_with_finite_products) is_cartesian_categoryCFP:
  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_composition.arr J0)  Collect (partial_composition.arr J1) = {}"
    and "partial_magma.null J0 = partial_magma.null J1"
    shows "has_as_product
             (discrete_category.comp
                (Collect (partial_composition.arr J0)  Collect (partial_composition.arr J1))
                (partial_magma.null J0))
             (λi. if i  Collect (partial_composition.arr J0) then D0 i
                  else if i  Collect (partial_composition.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"
            by (metis D0.is_discrete J0.ide_char π0.is_natural_1 comp_assoc)
          have 1: "J1.arr j  D1 j  π1 j  p1 = π1 j  p1"
            by (metis D1.is_discrete J1.ide_char π1.is_natural_1 comp_assoc)
          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 elementary_category_with_terminal_object C 𝟭? λa. 𝗍?[a]
              using extends_to_elementary_category_with_terminal_object by blast
            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 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 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_composition.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