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

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

  end

  locale category_with_binary_products =
    category +
  assumes has_binary_products: has_binary_products

  subsection "Elementary Category with Binary Products"

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

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

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

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

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

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

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

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

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

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

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

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

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

    lemma tuple_ext:
    assumes "¬ span f g"
    shows "f, g = null"
      unfolding tuple_def
      by (simp add: assms)

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

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

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

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

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

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

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

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

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

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

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

  end

  subsection "Agreement between the Definitions"

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

  context category_with_binary_products
  begin

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

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

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

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

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

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

  end

  context elementary_category_with_binary_products
  begin

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

    proposition is_category_with_binary_products:
    shows "category_with_binary_products C"
      ..

  end

  subsection "Further Properties"

  context elementary_category_with_binary_products
  begin

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    interpretation CC: product_category C C ..

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

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

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

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

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

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

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

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

  section "Cartesian Category"

  locale cartesian_category =
    category_with_binary_products +
    category_with_terminal_object

  locale category_with_pullbacks_and_terminal_object =
    category_with_pullbacks +
    category_with_terminal_object
  begin

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

    sublocale cartesian_category C ..

  end

  locale elementary_cartesian_category =
    elementary_category_with_binary_products +
    elementary_category_with_terminal_object
  begin

    sublocale cartesian_category C
      using cartesian_category.intro is_category_with_binary_products
            is_category_with_terminal_object
      by auto

    proposition is_cartesian_category:
    shows "cartesian_category C"
      ..

  end

  context cartesian_category
  begin

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

  end

subsection "Monoidal Structure"

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

  context elementary_cartesian_category
  begin

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

    lemma pr_coincidence:
    shows "ι = 𝔭1[𝟭, 𝟭]"
      using ide_one
      by (simp add: terminal_arr_unique terminal_one)

    lemma unit_is_terminal_arr:
    shows "terminal_arr ι"
      using ide_one
      by (simp add: terminal_one)

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

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

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

    lemma trm_tensor:
    assumes "ide a" and "ide b"
    shows "𝗍[a  b] = ι  (𝗍[a]  𝗍[b])"
      using assms unit_is_terminal_arr terminal_arr_unique ide_one
      by (simp add: unit_eq_trm)

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

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

    abbreviation lunit ("𝗅[_]")
    where