Theory CartesianMonoidalCategory

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

chapter "Cartesian Monoidal Category"

theory CartesianMonoidalCategory
imports MonoidalCategory Category3.CartesianCategory
begin

section "Symmetric Monoidal Category"

  locale symmetric_monoidal_category =
    monoidal_category C T α ι +
    S: symmetry_functor C C +
    ToS: composite_functor CC.comp CC.comp C S.map T +
    σ: natural_isomorphism CC.comp C T ToS.map σ
  for C :: "'a comp"                            (infixr "" 55)
  and T :: "'a * 'a  'a"
  and α :: "'a * 'a * 'a  'a"
  and ι :: 'a
  and σ :: "'a * 'a  'a" +
  assumes sym_inverse: " ide a; ide b   inverse_arrows (σ (a, b)) (σ (b, a))"
  and unitor_coherence: "ide a  𝗅[a]  σ (a, ) = 𝗋[a]"
  and assoc_coherence: " ide a; ide b; ide c  
                          α (b, c, a)  σ (a, b  c)  α (a, b, c)
                             = (b  σ (a, c))  α (b, a, c)  (σ (a, b)  c)"
  begin

    abbreviation sym                  ("𝗌[_, _]")
    where "sym a b  σ (a, b)"

  end

  locale elementary_symmetric_monoidal_category =
    elementary_monoidal_category C tensor unity lunit runit assoc
  for C :: "'a comp"                  (infixr "" 55)
  and tensor :: "'a  'a  'a"       (infixr "" 53)
  and unity :: 'a                      ("")
  and lunit :: "'a  'a"              ("𝗅[_]")
  and runit :: "'a  'a"              ("𝗋[_]")
  and assoc :: "'a  'a  'a  'a"  ("𝖺[_, _, _]")
  and sym :: "'a  'a  'a"          ("𝗌[_, _]") +
  assumes sym_in_hom: " ide a; ide b   «𝗌[a, b] : a  b  b  a»"
  and sym_naturality: " arr f; arr g   𝗌[cod f, cod g]  (f  g) = (g  f)  𝗌[dom f, dom g]"
  and sym_inverse: " ide a; ide b   inverse_arrows 𝗌[a, b] 𝗌[b, a]"
  and unitor_coherence: "ide a  𝗅[a]  𝗌[a, ] = 𝗋[a]"
  and assoc_coherence: " ide a; ide b; ide c  
                          𝖺[b, c, a]  𝗌[a, b  c]  𝖺[a, b, c]
                             = (b  𝗌[a, c])  𝖺[b, a, c]  (𝗌[a, b]  c)"
  begin

    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

    interpretation CC: product_category C C ..
    sublocale MC: monoidal_category C T α ι
      using induces_monoidal_category by simp

    interpretation S: symmetry_functor C C ..
    interpretation ToS: composite_functor CC.comp CC.comp C S.map T ..

    definition σ :: "'a * 'a  'a"
    where "σ f  if CC.arr f then 𝗌[cod (fst f), cod (snd f)]  (fst f  snd f) else null"

    interpretation σ: natural_isomorphism CC.comp C T ToS.map σ
    proof -
      interpret σ: transformation_by_components CC.comp C T ToS.map "λa. 𝗌[fst a, snd a]"
        using sym_in_hom sym_naturality
        by unfold_locales auto
      interpret σ: natural_isomorphism CC.comp C T ToS.map σ.map
        using sym_inverse σ.map_simp_ide
        by unfold_locales auto
      have "σ = σ.map"
        using σ_def σ.map_def sym_naturality by fastforce
      thus "natural_isomorphism CC.comp C T ToS.map σ"
        using σ.natural_isomorphism_axioms by presburger
    qed

    interpretation symmetric_monoidal_category C T α ι σ
    proof
      show "a b.  ide a; ide b   inverse_arrows (σ (a, b)) (σ (b, a))"
        using sym_inverse comp_arr_dom σ_def by auto
      show "a. ide a  MC.lunit a  σ (a, MC.unity) = MC.runit a"
        using lunit_agreement ℐ_agreement sym_in_hom comp_arr_dom
              unitor_coherence runit_agreement σ_def
         by simp
      show "a b c.  ide a; ide b; ide c  
                      MC.assoc b c a  σ (a, MC.tensor b c)  MC.assoc a b c =
                      MC.tensor b (σ (a, c))  MC.assoc b a c  MC.tensor (σ (a, b)) c"
        using sym_in_hom tensor_preserves_ide σ_def assoc_coherence
              comp_arr_dom comp_cod_arr
        by simp
    qed

    lemma induces_symmetric_monoidal_categoryCMC:
    shows "symmetric_monoidal_category C T α ι σ"
      ..

  end

  context symmetric_monoidal_category
  begin

    interpretation EMC: elementary_monoidal_category C tensor unity lunit runit assoc
      using induces_elementary_monoidal_category by auto

    lemma induces_elementary_symmetric_monoidal_categoryCMC:
    shows "elementary_symmetric_monoidal_category
             C tensor unity lunit runit assoc (λa b. σ (a, b))"
      using σ.naturality unitor_coherence assoc_coherence sym_inverse
      by unfold_locales auto

  end

  locale dual_symmetric_monoidal_category =
    M: symmetric_monoidal_category
  begin

    sublocale dual_monoidal_category C T α ι ..
    interpretation S: symmetry_functor comp comp ..
    interpretation ToS: composite_functor MM.comp MM.comp comp S.map T ..
    sublocale σ': inverse_transformation M.CC.comp C T M.ToS.map σ ..
    interpretation σ: natural_transformation MM.comp comp T ToS.map σ'.map
      using σ'.is_extensional σ'.is_natural_1 σ'.is_natural_2
      by unfold_locales auto
    interpretation σ: natural_isomorphism MM.comp comp T ToS.map σ'.map
      by unfold_locales auto

    sublocale symmetric_monoidal_category comp T M.α' M.inv ι σ'.map
    proof
      show "a b. ide a; ide b  inverse_arrows (σ'.map (a, b)) (σ'.map (b, a))"
        apply auto
        by (metis M.inverse_arrowsE M.inverse_unique M.isoI M.sym_inverse ide_char
            iso_char comp_def section_retraction_of_iso(1))
      show "a. ide a  lunit a op σ'.map (a, unity) = runit a"
        using M.unitor_coherence M.unit_in_hom M.unit_is_iso lunit_char runit_char
        apply auto
        by (metis M.inv_comp_left(1) M.iso_lunit M.iso_runit)
      show "a b c.
              ide a; ide b; ide c
                  assoc b c a op σ'.map (a, tensor b c) op assoc a b c =
                     (tensor b (σ'.map (a, c))) op assoc b a c op (tensor (σ'.map (a, b)) c)"
      proof -
        fix a b c
        assume a: "ide a" and b: "ide b" and c: "ide c"
        show "assoc b c a op σ'.map (a, tensor b c) op assoc a b c =
              (tensor b (σ'.map (a, c))) op assoc b a c op (tensor (σ'.map (a, b)) c)"
        proof -
          have "assoc b c a op σ'.map (a, tensor b c) op assoc a b c =
                (𝖺-1[a, b, c]  M.inv 𝗌[a, tensor b c])  𝖺-1[b, c, a]"
            using a b c by auto
          also have "... = M.inv (𝗌[a, tensor b c]  M.assoc a b c)  M.inv (M.assoc b c a)"
            using a b c M.iso_assoc M.inv_comp by auto
          also have "... = M.inv (M.assoc b c a  𝗌[a, tensor b c]  M.assoc a b c)"
            using a b c M.iso_assoc
                  M.inv_comp [of "𝗌[a, tensor b c]  M.assoc a b c" "M.assoc b c a"]
            by fastforce
          also have "... = M.inv (tensor b 𝗌[a, c]  𝖺[b, a, c]  (tensor 𝗌[a, b] c))"
            using a b c M.assoc_coherence by simp
          also have "... = M.inv (𝖺[b, a, c]  (tensor 𝗌[a, b] c))  M.inv (tensor b 𝗌[a, c])"
            using a b c M.iso_assoc
                  M.inv_comp [of "𝖺[b, a, c]  (tensor 𝗌[a, b] c)"]
            by fastforce
          also have "... =
                     (tensor (M.inv 𝗌[a, b]) c  M.inv 𝖺[b, a, c])  tensor b (M.inv 𝗌[a, c])"
            using a b c M.iso_assoc M.inv_comp by simp
          also have "... =
                     (tensor b (σ'.map (a, c))) op assoc b a c op (tensor (σ'.map (a, b)) c)"
            using a b c by auto
          finally show ?thesis by simp
        qed
      qed
    qed

    lemma is_symmetric_monoidal_category:
    shows "symmetric_monoidal_category comp T M.α' (M.inv ι) σ'.map"
      ..

  end

section "Cartesian Monoidal Category"

  text ‹
    Here we define ``cartesian monoidal category'' by imposing additional properties,
    but not additional structure, on top of ``monoidal category''.  The additional properties
    are that the unit is a terminal object and that the tensor is a categorical product,
    with projections defined in terms of unitors, terminators, and tensor.  It then follows
    that the associators are induced by the product structure.
  ›

  locale cartesian_monoidal_category =
    monoidal_category C T α ι
  for C :: "'a comp"                            (infixr "" 55)
  and T :: "'a * 'a  'a"
  and α :: "'a * 'a * 'a  'a"
  and ι :: 'a +
  assumes terminal_unity: "terminal "
  and tensor_is_product:
        "ide a; ide b; «ta : a  »; «tb : b  » 
            has_as_binary_product a b (𝗋[a]  (a  tb)) (𝗅[b]  (ta  b))"
  begin

    sublocale category_with_terminal_object
      using terminal_unity by unfold_locales blast

    lemma is_category_with_terminal_object:
    shows "category_with_terminal_object C"
      ..

    definition the_trm  ("𝗍[_]")
    where "the_trm  λf. THE t. «t : dom f  »"

    lemma trm_in_hom [intro]:
    assumes "ide a"
    shows "«𝗍[a] : a  »"
      unfolding the_trm_def
      using assms theI [of "λt. «t : dom a  »"] terminal_unity terminal_arr_unique
      by (metis ideD(2) terminalE)

    lemma trm_simps [simp]:
    assumes "ide a"
    shows "arr 𝗍[a]" and "dom 𝗍[a] = a" and "cod 𝗍[a] = "
      using assms trm_in_hom by auto

    interpretation elementary_category_with_terminal_object C  the_trm
    proof
      show "ide "
        using ide_unity by blast
      fix a
      show "ide a  «the_trm a : a  »"
        using the_trm_def theI [of "λt. «t : dom a  »"] terminalE terminal_unity by auto
      thus "f. ide a; «f : a  »  f = the_trm a"
        using theI [of "λt. «t : dom a  »"]
        by (metis terminalE terminal_unity)
    qed

    lemma extends_to_elementary_category_with_terminal_objectCMC:
    shows "elementary_category_with_terminal_object C  the_trm"
      ..

    definition pr0  ("𝔭0[_, _]")
    where "pr0 a b  𝗅[b]  (𝗍[a]  b)"

    definition pr1  ("𝔭1[_, _]")
    where "pr1 a b  𝗋[a]  (a  𝗍[b])"

    (* TODO: Must use qualified name to avoid clash between definitions of assoc. *)
    sublocale ECC: elementary_category_with_binary_products C pr0 pr1
    proof
      fix f g
      assume fg: "span f g"
      have "has_as_binary_product (cod f) (cod g) 𝔭1[cod f, cod g] 𝔭0[cod f, cod g]"
        using fg tensor_is_product pr0_def pr1_def by auto
      thus "∃!l. 𝔭1[cod f, cod g]  l = f  𝔭0[cod f, cod g]  l = g"
        using fg
        by (elim has_as_binary_productE) blast
    qed (unfold pr0_def pr1_def, auto)

    lemma induces_elementary_category_with_binary_productsCMC:
    shows "elementary_category_with_binary_products C pr0 pr1"
      ..

    lemma is_category_with_binary_products:
    shows "category_with_binary_products C"
      using ECC.is_category_with_binary_products by blast

    sublocale category_with_binary_products C
      using is_category_with_binary_products by blast

    (* TODO: Here the clash is on lunit and runit. *)
    sublocale ECC: elementary_cartesian_category C pr0 pr1  the_trm ..

    lemma extends_to_elementary_cartesian_categoryCMC:
    shows "elementary_cartesian_category C pr0 pr1  the_trm"
      ..

    lemma is_cartesian_category:
    shows "cartesian_category C"
      using ECC.is_cartesian_category by simp

    sublocale cartesian_category C
      using is_cartesian_category by blast

    abbreviation dup  ("𝖽[_]")
    where "dup  ECC.dup"

    abbreviation tuple  ("_, _")
    where "f, g  ECC.tuple f g"

    lemma prod_eq_tensor:
    shows "ECC.prod = tensor"
    proof -
      have "f g. ECC.prod f g = f  g"
      proof -
        fix f g
        show "ECC.prod f g = f  g"
        proof (cases "arr f  arr g")
          show "¬ (arr f  arr g)  ?thesis"
            by (metis CC.arrE ECC.prod_def ECC.tuple_ext T.is_extensional fst_conv seqE snd_conv)
          assume 0: "arr f  arr g"
          have 1: "span (f  𝔭1[dom f, dom g]) (g  𝔭0[dom f, dom g])"
            using 0 by simp
          have "𝔭1[cod f, cod g]  ECC.prod f g = 𝔭1[cod f, cod g]  (f  g)"
          proof -
            have "𝔭1[cod f, cod g]  ECC.prod f g =
                  𝔭1[cod f, cod g]  f  𝔭1[dom f, dom g], g  𝔭0[dom f, dom g]"
              unfolding ECC.prod_def by simp
            also have "... = f  𝔭1[dom f, dom g]"
              using 0 1 ECC.pr_tuple(1) by fastforce
            also have "... = (f  𝗋[dom f])  (dom f  𝗍[dom g])"
              unfolding pr1_def
              using comp_assoc by simp
            also have "... = (𝗋[cod f]  (f  ))  (dom f  𝗍[dom g])"
              using 0 runit_naturality by auto
            also have "... = 𝗋[cod f]  (f  )  (dom f  𝗍[dom g])"
              using comp_assoc by simp
            also have "... = 𝗋[cod f]  (cod f  𝗍[cod g])  (f  g)"
              using 0 interchange comp_arr_dom comp_cod_arr trm_naturality trm_simps(1)
              by force
            also have "... = (𝗋[cod f]  (cod f  𝗍[cod g]))  (f  g)"
              using comp_assoc by simp
            also have "... = 𝔭1[cod f, cod g]  (f  g)"
              unfolding pr1_def by simp
            finally show ?thesis by blast
          qed
          moreover have "𝔭0[cod f, cod g]  ECC.prod f g = 𝔭0[cod f, cod g]  (f  g)"
          proof -
            have "𝔭0[cod f, cod g]  ECC.prod f g =
                  𝔭0[cod f, cod g]  f  𝔭1[dom f, dom g], g  𝔭0[dom f, dom g]"
              unfolding ECC.prod_def by simp
            also have "... = g  𝔭0[dom f, dom g]"
              using 0 1 ECC.pr_tuple by fastforce
            also have "... = (g  𝗅[dom g])  (𝗍[dom f]  dom g)"
              unfolding pr0_def
              using comp_assoc by simp
            also have "... = (𝗅[cod g]  (  g))  (𝗍[dom f]  dom g)"
              using 0 lunit_naturality by auto
            also have "... = 𝗅[cod g]  (  g)  (𝗍[dom f]  dom g)"
              using comp_assoc by simp
            also have "... = 𝗅[cod g]  (𝗍[cod f]  cod g)  (f  g)"
              using 0 interchange comp_arr_dom comp_cod_arr trm_naturality trm_simps(1)
              by force
            also have "... = (𝗅[cod g]  (𝗍[cod f]  cod g))  (f  g)"
              using comp_assoc by simp
            also have "... = 𝔭0[cod f, cod g]  (f  g)"
              unfolding pr0_def by simp
            finally show ?thesis by blast
          qed
          ultimately show ?thesis
            by (metis 0 1 ECC.pr_naturality(1-2) ECC.tuple_pr_arr ide_cod)
        qed
      qed
      thus ?thesis by blast
    qed

    lemma Prod_eq_T:
    shows "ECC.Prod = T"
    proof
      fix fg
      show "ECC.Prod fg = T fg"
        using prod_eq_tensor
        by (cases "CC.arr fg") auto
    qed

    lemma tuple_pr [simp]:
    assumes "ide a" and "ide b"
    shows "𝔭1[a, b], 𝔭0[a, b] = a  b"
      using assms prod_eq_tensor by simp

    lemma tensor_expansion:
    assumes "arr f" and "arr g"
    shows "f  g = f  𝔭1[dom f, dom g], g  𝔭0[dom f, dom g]"
      using assms
      by (metis ECC.prod_def prod_eq_tensor)

  text ‹
     It is somewhat amazing that once the tensor product has been assumed to be a
     categorical product with the indicated projections, then the associators are
     forced to be those induced by the categorical product.
  ›

    lemma pr_assoc:
    assumes "ide a" and "ide b" and "ide c"
    shows "𝔭1[a, b  c]  𝖺[a, b, c] = 𝔭1[a, b]  𝔭1[a  b, c]"
    and "𝔭1[b, c]  𝔭0[a, b  c]  𝖺[a, b, c] = 𝔭0[a, b]  𝔭1[a  b, c]"
    and "𝔭0[b, c]  𝔭0[a, b  c]  𝖺[a, b, c] = 𝔭0[a  b, c]"
    proof -
      show "𝔭1[a, b  c]  𝖺[a, b, c] = 𝔭1[a, b]  𝔭1[a  b, c]"
      proof -
        have "𝔭1[a, b  c]  𝖺[a, b, c] = (𝗋[a]  (a  ι  (𝗍[b]  𝗍[c])))  𝖺[a, b, c]"
          by (metis ECC.trm_tensor ECC.unit_eq_trm arr_cod_iff_arr assms(2-3) comp_cod_arr
              dom_lunit ide_unity pr1_def prod_eq_tensor trm_naturality trm_one trm_simps(1)
              unitor_coincidence(1))
        also have "... = (𝗋[a]  (a  ι)  (a  𝗍[b]  𝗍[c]))  𝖺[a, b, c]"
          using assms interchange unit_in_hom_ax by auto
        also have "... = 𝗋[a]  (a  ι)  (a  𝗍[b]  𝗍[c])  𝖺[a, b, c]"
          using comp_assoc by simp
        also have "... = 𝗋[a]  (a  ι)  𝖺[a, , ]  ((a  𝗍[b])  𝗍[c])"
          using assms assoc_naturality [of a "𝗍[b]" "𝗍[c]"] by force
        also have "... = 𝗋[a]  (𝗋[a]  )  ((a  𝗍[b])  𝗍[c])"
          using assms runit_char comp_assoc by simp
        also have "... = 𝗋[a]  (𝔭1[a, b]  𝗍[c])"
          using assms comp_arr_dom comp_cod_arr interchange [of "𝗋[a]" "a  𝗍[b]"  "𝗍[c]"]
          by (metis ECC.pr_simps(4) pr1_def trm_simps(1) trm_simps(3))
        also have "... = 𝗋[a]  (𝔭1[a, b]  (a  b)    𝗍[c])"
          using assms comp_arr_dom comp_cod_arr
          by (metis (no_types, lifting) ECC.pr_simps(4-5) prod_eq_tensor trm_simps(1,3))
        also have "... = 𝗋[a]  (𝔭1[a, b]  )  ((a  b)  𝗍[c])"
          using assms interchange [of "𝔭1[a, b]" "a  b"  " 𝗍[c]"]
          by (metis (no_types, lifting) ECC.pr_simps(4-5) Prod_eq_T comp_arr_dom comp_cod_arr
              fst_conv snd_conv trm_simps(1,3))
        also have "... = (𝗋[a]  (𝔭1[a, b]  ))  ((a  b)  𝗍[c])"
          using comp_assoc by simp
        also have "... = (𝔭1[a, b]  𝗋[a  b])  ((a  b)  𝗍[c])"
          using assms runit_naturality
          by (metis (no_types, lifting) ECC.cod_pr1 ECC.pr_simps(4,5) prod_eq_tensor)
        also have "... = 𝔭1[a, b]  𝔭1[a  b, c]"
          using pr1_def comp_assoc by simp
        finally show ?thesis by blast
      qed
      show "𝔭1[b, c]  𝔭0[a, b  c]  𝖺[a, b, c] = 𝔭0[a, b]  𝔭1[a  b, c]"
      proof -
        have "𝔭1[b, c]  𝔭0[a, b  c]  𝖺[a, b, c] =
              𝗋[b]  (b  𝗍[c])  𝗅[b  c]  𝖺[, b, c]  ((𝗍[a]  b)  c)"
          using assms pr0_def pr1_def assoc_naturality [of "𝗍[a]" b c] comp_assoc by auto
        also have "... = 𝗋[b]  ((b  𝗍[c])  𝗅[b  c])  𝖺[, b, c]  ((𝗍[a]  b)  c)"
          using comp_assoc by simp
        also have "... = 𝗋[b]  (𝗅[b  ]  (  b  𝗍[c]))  𝖺[, b, c]  ((𝗍[a]  b)  c)"
          using assms lunit_naturality [of "b  𝗍[c]"] by auto
        also have "... = 𝗋[b]  𝗅[b  ]  ((  b  𝗍[c])  𝖺[, b, c])  ((𝗍[a]  b)  c)"
          using comp_assoc by simp
        also have "... = 𝗋[b]  𝗅[b  ]  (𝖺[, b, ]  ((  b)  𝗍[c]))  ((𝗍[a]  b)  c)"
          using assms assoc_naturality [of  b "𝗍[c]"] by auto
        also have "... = 𝗋[b]  (𝗅[b]  )  ((  b)  𝗍[c])  ((𝗍[a]  b)  c)"
          using assms lunit_tensor [of b ] comp_assoc
          by (metis ide_unity lunit_tensor')
        also have "... = 𝗋[b]  (𝗅[b]  )  ((𝗍[a]  b)  )  ((a  b)  𝗍[c])"
          using assms comp_arr_dom comp_cod_arr interchange by simp
        also have "... = (𝗋[b]  (𝔭0[a, b]  ))  ((a  b)  𝗍[c])"
          using assms pr0_def ECC.pr_simps(1) R.preserves_comp comp_assoc by simp
        also have "... = (𝔭0[a, b]  𝗋[a  b])  ((a  b)  𝗍[c])"
          using assms pr0_def runit_naturality [of "𝔭0[a, b]"] comp_assoc by simp
        also have "... = 𝔭0[a, b]  𝔭1[a  b, c]"
          using pr0_def pr1_def comp_assoc by simp
        finally show ?thesis by blast
      qed
      show "𝔭0[b, c]  𝔭0[a, b  c]  𝖺[a, b, c] = 𝔭0[a  b, c]"
      proof -
        have "𝔭0[b, c]  𝔭0[a, b  c]  𝖺[a, b, c] =
              𝗅[c]  (𝗍[b]  c)  𝗅[b  c]  (𝗍[a]  b  c)  𝖺[a, b, c]"
          using pr0_def comp_assoc by simp
        also have "... = 𝗅[c]  ((𝗍[b]  c)  𝗅[b  c])  𝖺[, b, c]  ((𝗍[a]  b)  c)"
          using assms assoc_naturality [of "𝗍[a]" b c] comp_assoc by simp
        also have "... = 𝗅[c]  (𝗅[  c]  (  𝗍[b]  c))  𝖺[, b, c]  ((𝗍[a]  b)  c)"
          using assms lunit_naturality [of "𝗍[b]  c"] by simp
        also have "... = 𝗅[c]  𝗅[  c]  (𝖺[, , c]  ((  𝗍[b])  c))  ((𝗍[a]  b)  c)"
          using assms assoc_naturality [of  "𝗍[b]" c] comp_assoc by simp
        also have "... = 𝗅[c]  (𝗅[  c]  𝖺[, , c])  ((  𝗍[b])  c)  ((𝗍[a]  b)  c)"
          using comp_assoc by simp
        also have "... = 𝗅[c]  (ι  c)  ((  𝗍[b])  c)  ((𝗍[a]  b)  c)"
          using assms lunit_tensor' unitor_coincidence(1) by simp
        also have "... = 𝗅[c]  (ι  c)  ((  𝗍[b])  (𝗍[a]  b)  c)"
          using assms comp_arr_dom comp_cod_arr
          by (metis arr_tensor ide_char interchange trm_simps(1-3))
        also have "... = 𝗅[c]  (ι  c)  ((𝗍[a]  𝗍[b])  c)"
          using assms comp_arr_dom comp_cod_arr interchange by simp
        also have "... = 𝗅[c]  (ι  (𝗍[a]  𝗍[b])  c)"
          using assms interchange unit_in_hom_ax by auto
        also have "... = 𝔭0[a  b, c]"
          using assms pr0_def ECC.trm_tensor category.comp_arr_dom category_axioms prod_eq_tensor
                trm_one unit_in_hom_ax unitor_coincidence(1)
          by fastforce
        finally show ?thesis by blast
      qed
    qed

    lemma assoc_agreement:
    assumes "ide a" and "ide b" and "ide c"
    shows "ECC.assoc a b c = 𝖺[a, b, c]"
    proof -
      have "𝔭1[a, b  c]  ECC.assoc a b c = 𝔭1[a, b  c]  𝖺[a, b, c]"
        using assms ECC.pr_assoc(3) pr_assoc(1) prod_eq_tensor by force
      moreover have "𝔭0[a, b  c]  ECC.assoc a b c = 𝔭0[a, b  c]  𝖺[a, b, c]"
      proof -
        have "𝔭1[b, c]  𝔭0[a, b  c]  ECC.assoc a b c = 𝔭1[b, c]  𝔭0[a, b  c]  𝖺[a, b, c]"
          using assms ECC.pr_assoc(2) pr_assoc(2) prod_eq_tensor by force
        moreover have "𝔭0[b, c]  𝔭0[a, b  c]  ECC.assoc a b c =
                       𝔭0[b, c]  𝔭0[a, b  c]  𝖺[a, b, c]"
          using assms prod_eq_tensor ECC.pr_assoc(1) pr_assoc(3) by force
        ultimately show ?thesis
          using assms prod_eq_tensor
                ECC.pr_joint_monic
                  [of b c "𝔭0[a, b  c]  ECC.assoc a b c " "𝔭0[a, b  c]  𝖺[a, b, c]"]
          by fastforce
      qed
      ultimately show ?thesis
        using assms prod_eq_tensor
              ECC.pr_joint_monic [of a "b  c" "ECC.assoc a b c" "𝖺[a, b, c]"]
        by fastforce
    qed

    lemma lunit_eq:
    assumes "ide a"
    shows "𝔭0[, a] = 𝗅[a]"
      by (simp add: assms comp_arr_dom pr0_def trm_one)

    lemma runit_eq:
    assumes "ide a"
    shows "𝔭1[a, ] = 𝗋[a]"
      by (simp add: assms comp_arr_dom pr1_def trm_one)

    lemma lunit'_as_tuple:
    assumes "ide a"
    shows "tuple 𝗍[a] a = lunit' a"
      using ECC.inverse_arrows_lunit assms inverse_unique lunit_eq by fastforce

    lemma runit'_as_tuple:
    assumes "ide a"
    shows "tuple a 𝗍[a] = runit' a"
      using ECC.inverse_arrows_runit assms inverse_unique runit_eq by fastforce

    interpretation S: symmetry_functor C C ..
    interpretation ToS: composite_functor CC.comp CC.comp C S.map T ..

    interpretation σ: natural_transformation CC.comp C T ToS.map ECC.σ
    proof -
      have "ECC.Prod' = ToS.map"
      proof
        fix fg
        show "ECC.Prod' fg = ToS.map fg"
          using prod_eq_tensor
          by (metis CC.arr_char ECC.prod_def ECC.tuple_ext S.map_def ToS.is_extensional o_apply seqE)
      qed
      thus "natural_transformation CC.comp C T ToS.map ECC.σ"
        using Prod_eq_T ECC.σ_is_natural_transformation by simp
    qed

    interpretation σ: natural_isomorphism CC.comp C T ToS.map ECC.σ
      using ECC.sym_inverse_arrows comp_arr_dom
      by unfold_locales auto

    sublocale SMC: symmetric_monoidal_category C T α ι ECC.σ
    proof
      show "a b. ide a; ide b  inverse_arrows (ECC.σ (a, b)) (ECC.σ (b, a))"
        using comp_arr_dom by auto
      show "a. ide a  𝗅[a]  ECC.σ (a, ) = 𝗋[a]"
        using σ.naturality prod_eq_tensor
        by (metis (no_types, lifting) CC.arr_char ECC.prj_sym(1) R.preserves_ide
            𝔩_ide_simp ρ_ide_simp σ.preserves_reflects_arr comp_arr_ide fst_conv
            ideD(1) ideD(3) ide_unity lunit_naturality pr0_def pr1_def runit_naturality
            snd_conv trm_one)
      show "a b c. ide a; ide b; ide c 
                       𝖺[b, c, a]  ECC.σ (a, b  c)  𝖺[a, b, c] =
                       (b  ECC.σ (a, c))  𝖺[b, a, c]  (ECC.σ (a, b)  c)"
      proof -
        fix a b c
        assume a: "ide a" and b: "ide b" and c: "ide c"
        show "𝖺[b, c, a]  ECC.σ (a, b  c)  𝖺[a, b, c] =
              (b  ECC.σ (a, c))  𝖺[b, a, c]  (ECC.σ (a, b)  c)"
          using a b c prod_eq_tensor assoc_agreement comp_arr_dom ECC.sym_assoc_coherence [of a b c]
          by simp
        qed
      qed

  end

section "Elementary Cartesian Monoidal Category"

  locale elementary_cartesian_monoidal_category =
    elementary_monoidal_category C tensor unity lunit runit assoc
  for C :: "'a comp"                   (infixr "" 55)
  and tensor :: "'a  'a  'a"       (infixr "" 53)
  and unity :: 'a                      ("")
  and lunit :: "'a  'a"              ("𝗅[_]")
  and runit :: "'a  'a"              ("𝗋[_]")
  and assoc :: "'a  'a  'a  'a"  ("𝖺[_, _, _]")
  and trm :: "'a  'a"                ("𝗍[_]")
  and dup :: "'a  'a"                ("𝖽[_]") +
  assumes trm_in_hom: "ide a  «𝗍[a] : a  »"
  and trm_unity: "𝗍[] = "
  and trm_naturality: "arr f  𝗍[cod f]  f = 𝗍[dom f]"
  and dup_in_hom [intro]: "ide a  «𝖽[a] : a  a  a»"
  and dup_naturality: "arr f  𝖽[cod f]  f = (f  f)  𝖽[dom f]"
  and prj0_dup: "ide a  𝗋[a]  (a  𝗍[a])  𝖽[a] = a"
  and prj1_dup: "ide a  𝗅[a]  (𝗍[a]  a)  𝖽[a] = a"
  and tuple_prj: " ide a; ide b   (𝗋[a]  (a  𝗍[b])  𝗅[b]  (𝗍[a]  b))  𝖽[a  b] = a  b"

  context cartesian_monoidal_category
  begin

    interpretation elementary_category_with_terminal_object C  the_trm
      using extends_to_elementary_category_with_terminal_objectCMC by blast

    interpretation elementary_monoidal_category C tensor unity lunit runit assoc
      using induces_elementary_monoidal_category by simp

    interpretation elementary_cartesian_monoidal_category C
                     tensor unity lunit runit assoc the_trm dup
      using ECC.trm_one ECC.trm_naturality ECC.tuple_in_hom' prod_eq_tensor ECC.dup_naturality in_homI
            ECC.comp_runit_term_dup runit_eq ECC.comp_lunit_term_dup lunit_eq ECC.tuple_expansion
            comp_cod_arr
      apply unfold_locales
             apply auto
    proof -
      fix a b
      assume a: "ide a" and b: "ide b"
      show "(𝗋[a]  (a  𝗍[b])  𝗅[b]  (𝗍[a]  b))  𝖽[a  b] = a  b"
        using a b ECC.tuple_pr pr0_def pr1_def prod_eq_tensor
        by (metis ECC.pr_simps(5) ECC.span_pr ECC.tuple_expansion)
    qed

    lemma induces_elementary_cartesian_monoidal_categoryCMC:
    shows "elementary_cartesian_monoidal_category C tensor  lunit runit assoc the_trm dup"
      ..

  end

  context elementary_cartesian_monoidal_category
  begin

    lemma trm_simps [simp]:
    assumes "ide a"
    shows "arr 𝗍[a]" and "dom 𝗍[a] = a" and "cod 𝗍[a] = "
      using assms trm_in_hom by auto

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

    interpretation elementary_category_with_terminal_object C  trm
      apply unfold_locales
        apply auto
      by (metis comp_cod_arr in_homE trm_naturality trm_unity)

    lemma is_elementary_category_with_terminal_object:
    shows "elementary_category_with_terminal_object C  trm"
      ..

    (* Must use a qualified name here because locale parameters shadow lunit, runit, etc. *)
    interpretation MC: monoidal_category C T α ι
      using induces_monoidal_category by auto

    interpretation ECBP: elementary_category_with_binary_products C
                           λa b. 𝗅[b]  (𝗍[a]  b) λa b. 𝗋[a]  (a  𝗍[b])
    proof -
      let ?pr0 = "λa b. 𝗅[b]  (𝗍[a]  b)"
      let ?pr1 = "λa b. 𝗋[a]  (a  𝗍[b])"
      show "elementary_category_with_binary_products C ?pr0 ?pr1"
      proof
        fix a b
        assume a: "ide a" and b: "ide b"
        show 0: "cod (?pr0 a b) = b"
          by (metis a arr_tensor b cod_comp cod_tensor ide_char in_homE lunit_in_hom
              seqI trm_simps(1,3))
        show 1: "cod (?pr1 a b) = a"
          by (metis a arr_tensor b cod_comp cod_tensor ideD(1,3) in_homE runit_in_hom
              seqI trm_simps(1,3))
        show "span (?pr1 a b) (?pr0 a b)"
          by (metis 0 1 a arr_cod_iff_arr b dom_cod dom_comp dom_tensor ideD(1) trm_simps(1-2))
        next
        fix f g
        assume fg: "span f g"
        show "∃!l. ?pr1 (cod f) (cod g)  l = f  ?pr0 (cod f) (cod g)  l = g"
        proof
          show 1: "?pr1 (cod f) (cod g)  (f  g)  𝖽[dom f] = f 
                   ?pr0 (cod f) (cod g)  (f  g)  𝖽[dom f] = g"
          proof
            show "?pr1 (cod f) (cod g)  (f  g)  𝖽[dom f] = f"
            proof -
              have "?pr1 (cod f) (cod g)  (f  g)  𝖽[dom f] =
                    MC.runit (cod f)  (MC.tensor (cod f) 𝗍[cod g]  (f  g))  𝖽[dom f]"
                by (simp add: fg comp_assoc runit_agreement)
              also have "... = MC.runit (cod f)  (MC.tensor f   (dom f  𝗍[dom g]))  𝖽[dom f]"
                using fg
                by (simp add: comp_arr_dom comp_cod_arr interchange trm_naturality)
              also have "... = (MC.runit (cod f)  MC.tensor f  )  (dom f  𝗍[dom g])  𝖽[dom f]"
                using comp_assoc by simp
              also have "... = f  ?pr1 (dom f) (dom g)  𝖽[dom f]"
                using MC.runit_naturality ℐ_agreement fg comp_assoc runit_agreement by force
              also have "... = f"
                using fg comp_arr_dom comp_assoc prj0_dup runit_agreement by fastforce
              finally show ?thesis by blast
            qed
            show "?pr0 (cod f) (cod g)  (f  g)  𝖽[dom f] = g"
            proof -
              have "?pr0 (cod f) (cod g)  (f  g)  𝖽[dom f] =
                    MC.lunit (cod g)  (MC.tensor 𝗍[cod f] (cod g)  (f  g))  𝖽[dom f]"
                by (simp add: fg comp_assoc lunit_agreement)
              also have "... = MC.lunit (cod g)  (MC.tensor  g  (𝗍[dom f]  dom g))  𝖽[dom f]"
                using fg
                by (simp add: comp_arr_dom comp_cod_arr interchange trm_naturality)
              also have "... = (MC.lunit (cod g)  MC.tensor  g)  (𝗍[dom f]  dom g)  𝖽[dom f]"
                using comp_assoc by simp
              also have "... = g  ?pr0 (dom f) (dom g)  𝖽[dom f]"
                using MC.lunit_naturality ℐ_agreement fg comp_assoc lunit_agreement by force
              also have "... = g"
                using fg comp_arr_dom comp_assoc prj1_dup lunit_agreement by fastforce
              finally show ?thesis by blast
            qed
          qed
          fix l
          assume l: "?pr1 (cod f) (cod g)  l = f  ?pr0 (cod f) (cod g)  l = g"
          show "l = (f  g)  𝖽[dom f]"
          proof -
            have 2: "«l : dom f  cod f  cod g»"
              by (metis 1 arr_iff_in_hom cod_comp cod_tensor dom_comp fg l seqE)
            have "l = ((?pr1 (cod f) (cod g)  ?pr0 (cod f) (cod g))  𝖽[cod f  cod g])  l"
              using fg 2 tuple_prj [of "cod f" "cod g"] lunit_agreement runit_agreement comp_cod_arr
              by auto
            also have "... = (?pr1 (cod f) (cod g)  ?pr0 (cod f) (cod g))  𝖽[cod f  cod g]  l"
              using comp_assoc by simp
            also have "... = ((?pr1 (cod f) (cod g)  ?pr0 (cod f) (cod g))  (l  l))  𝖽[dom f]"
              using 2 dup_naturality [of l] comp_assoc by auto
            also have "... = (f  g)  𝖽[dom f]"
              using fg l interchange [of "?pr1 (cod f) (cod g)" l "?pr0 (cod f) (cod g)" l] by simp
            finally show ?thesis by blast
          qed
        qed
      qed
    qed

    lemma induces_elementary_category_with_binary_productsECMC:
    shows "elementary_category_with_binary_products C
             (λa b. 𝗅[b]  (𝗍[a]  b)) (λa b. 𝗋[a]  (a  𝗍[b]))"
      ..

    sublocale cartesian_monoidal_category C T α ι
    proof
      show "terminal MC.unity"
        by (simp add: ℐ_agreement terminal_one)
      show "a b ta tb. ide a; ide b; «ta : a  MC.unity»; «tb : b  MC.unity» 
                           has_as_binary_product a b
                             (MC.runit a  MC.tensor a tb) (MC.lunit b  MC.tensor ta b)"
        by (metis ECBP.has_as_binary_product T_simp ℐ_agreement arrI ideD(1)
            lunit_agreement runit_agreement trm_eqI)
    qed

    lemma induces_cartesian_monoidal_categoryECMC:
    shows "cartesian_monoidal_category C T α ι"
      ..

  end

  (* TODO: This definition of "diagonal_functor" conflicts with the one in Category3.Limit. *)
  locale diagonal_functor =
    C: category C +
    CC: product_category C C
  for C :: "'a comp"
  begin

    abbreviation map
    where "map f  if C.arr f then (f, f) else CC.null"

    lemma is_functor:
    shows "functor C CC.comp map"
      using map_def by unfold_locales auto

    sublocale "functor" C CC.comp map
      using is_functor by simp

  end

  context cartesian_monoidal_category
  begin

    sublocale Δ: diagonal_functor C ..
    interpretation ToΔ: composite_functor C CC.comp C Δ.map T ..

    sublocale δ: natural_transformation C C map T o Δ.map dup
    proof
      show "f. ¬ arr f  𝖽[f] = null"
        using ECC.tuple_ext by blast
      show "f. arr f  dom 𝖽[f] = map (dom f)"
        using dup_def by simp
      show "f. arr f  cod 𝖽[f] = ToΔ.map (cod f)"
        by (simp add: prod_eq_tensor)
      show "f. arr f  ToΔ.map f  𝖽[dom f] = 𝖽[f]"
        using ECC.tuple_expansion prod_eq_tensor by force
      show "f. arr f  𝖽[cod f]  map f = 𝖽[f]"
        by (simp add: comp_cod_arr dup_def)
    qed

  end

section "Cartesian Monoidal Category from Cartesian Category"

  text ‹
    A cartesian category extends to a cartesian monoidal category by using the product
    structure to obtain the various canonical maps.
  ›

  context elementary_cartesian_category
  begin

    interpretation CC: product_category C C ..
    interpretation CCC: product_category C CC.comp ..
    interpretation T: binary_functor C C C Prod
      using binary_functor_Prod by simp
    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

    interpretation α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α
      using α_is_natural_isomorphism by blast

    interpretation L: "functor" C C λf. Prod (cod ι, f)
      using unit_is_terminal_arr T.fixing_ide_gives_functor_1 by simp
    interpretation L: endofunctor C λf. Prod (cod ι, f) ..
    interpretation 𝗅: transformation_by_components C C
                        λf. Prod (cod ι, f) map λa. pr0 (cod ι) a
      using unit_is_terminal_arr
      by unfold_locales auto
    interpretation 𝗅: natural_isomorphism C C λf. Prod (cod ι, f) map 𝗅.map
      using 𝗅.map_simp_ide inverse_arrows_lunit ide_one
      by unfold_locales auto
    interpretation L: equivalence_functor C C λf. Prod (cod ι, f)
      using 𝗅.natural_isomorphism_axioms naturally_isomorphic_def
            L.isomorphic_to_identity_is_equivalence
      by blast

    interpretation R: "functor" C C λf. Prod (f, cod ι)
      using unit_is_terminal_arr T.fixing_ide_gives_functor_2 by simp
    interpretation R: endofunctor Cλf. Prod (f, cod ι) ..
    interpretation ρ: transformation_by_components C C
                        λf. Prod (f, cod ι) map λa. 𝔭1[a, cod ι]
      using unit_is_terminal_arr
      by unfold_locales auto
    interpretation ρ: natural_isomorphism C C λf. Prod (f, cod ι) map ρ.map
      using ρ.map_simp_ide inverse_arrows_runit ide_one
      by unfold_locales auto
    interpretation R: equivalence_functor C C λf. Prod (f, cod ι)
      using ρ.natural_isomorphism_axioms naturally_isomorphic_def
            R.isomorphic_to_identity_is_equivalence
      by blast

    interpretation MC: monoidal_category C Prod α ι
      using ide_one ι_is_iso pentagon comp_assoc α_simp_ide comp_cod_arr
      by unfold_locales auto

    lemma induces_monoidal_categoryECC:
    shows "monoidal_category C Prod α ι"
      ..

    lemma unity_agreement:
    shows "MC.unity = 𝟭"
      using ide_one by simp

    lemma assoc_agreement:
    assumes "ide a" and "ide b" and "ide c"
    shows "MC.assoc a b c = 𝖺[a, b, c]"
      using assms assoc_def α_simp_ide by auto

    lemma assoc'_agreement:
    assumes "ide a" and "ide b" and "ide c"
    shows "MC.assoc' a b c = 𝖺-1[a, b, c]"
      using assms inverse_arrows_assoc inverse_unique α_simp_ide by auto

    lemma runit_char_eqn:
    assumes "ide a"
    shows "𝗋[a]  𝟭 = (a  ι)  𝖺[a, 𝟭, 𝟭]"
      using assms ide_one assoc_def comp_assoc prod_tuple comp_cod_arr
      by (intro pr_joint_monic [of a "𝟭" "𝗋[a]  𝟭" "(a  ι)  𝖺[a, 𝟭, 𝟭]"]) auto

    lemma runit_agreement:
    assumes "ide a"
    shows "MC.runit a = 𝗋[a]"
      using assms unity_agreement assoc_agreement MC.runit_char(2) runit_char_eqn ide_one
      by (metis (no_types, lifting) MC.runit_eqI fst_conv runit_in_hom snd_conv)

    lemma lunit_char_eqn:
    assumes "ide a"
    shows "𝟭  𝗅[a] = (ι  a)  𝖺-1[𝟭, 𝟭, a]"
    proof (intro pr_joint_monic [of "𝟭" a "𝟭  𝗅[a]" "(ι  a)  𝖺-1[𝟭, 𝟭, a]"])
      show "ide a" by fact
      show "ide 𝟭"
        using ide_one by simp
      show "seq 𝗅[a] (𝟭  𝗅[a])"
        using assms ide_one by simp
      show "𝗅[a]  (𝟭  𝗅[a]) = 𝗅[a]  (ι  a)  𝖺-1[𝟭, 𝟭, a]"
        using assms ide_one assoc'_def comp_assoc prod_tuple comp_cod_arr by simp
      show "𝔭1[𝟭, a]  prod 𝟭 (lunit a) = 𝔭1[𝟭, a]  prod ι a  assoc' 𝟭 𝟭 a"
        using assms ide_one assoc'_def comp_cod_arr prod_tuple pr_naturality
        apply simp
        by (metis (full_types) cod_pr0 cod_pr1 elementary_category_with_binary_products.ide_prod
            elementary_category_with_binary_products_axioms pr_simps(1-2,4-5) trm_naturality
            trm_one)
    qed

    lemma lunit_agreement:
    assumes "ide a"
    shows "MC.lunit a = 𝗅[a]"
      by (metis (no_types, lifting) MC.lunit_eqI assms assoc'_agreement fst_conv ide_one
          lunit_char_eqn lunit_in_hom snd_conv unity_agreement)

    interpretation CMC: cartesian_monoidal_category C Prod α ι
    proof
      show "terminal MC.unity"
        by (simp add: terminal_one unity_agreement)
      fix a b ta tb
      assume a: "ide a" and b: "ide b"
      and ta: "«ta : a  MC.unity»" and tb: "«tb : b  MC.unity»"
      have 0: "𝔭0[a, b] = MC.lunit b  MC.tensor 𝗍[a] b"
        by (metis (no_types, lifting) a b ide_char cod_pr0 comp_cod_arr lunit_agreement
            pr_naturality(1) pr_simps(1) prod.sel(1-2) trm_simps(1-3))
      have 1: "𝔭1[a, b] = MC.runit a  MC.tensor a 𝗍[b]"
        by (metis (no_types, lifting) a b cod_pr1 comp_cod_arr ide_char pr_naturality(2)
            pr_simps(4) prod.sel(1-2) runit_agreement trm_simps(1-3))
      have 2: "𝗍[a] = ta  𝗍[b] = tb"
        using a b ta tb terminal_arr_unique trm_eqI unity_agreement by metis
      show "has_as_binary_product a b (MC.runit a  MC.tensor a tb) (MC.lunit b  MC.tensor ta b)"
        using a b 0 1 2 has_as_binary_product by force
    qed

    lemma extends_to_cartesian_monoidal_categoryECC:
    shows "cartesian_monoidal_category C Prod α ι"
      ..

    lemma trm_agreement:
    assumes "ide a"
    shows "CMC.the_trm a = 𝗍[a]"
      by (metis assms CMC.extends_to_elementary_category_with_terminal_objectCMC
          elementary_category_with_terminal_object.trm_eqI trm_in_hom unity_agreement)

    lemma pr_agreement:
    assumes "ide a" and "ide b"
    shows "CMC.pr0 a b = 𝔭0[a, b]" and "CMC.pr1 a b = 𝔭1[a, b]"
    proof -
      show "CMC.pr0 a b = 𝔭0[a, b]"
        unfolding CMC.pr0_def
        using assms(1-2) lunit_agreement pr_expansion(1) trm_agreement by auto
      show "CMC.pr1 a b = 𝔭1[a, b]"
        unfolding CMC.pr1_def
        using assms(1-2) pr_expansion(2) runit_agreement trm_agreement by force
    qed

    lemma dup_agreement:
    assumes "ide a"
    shows "CMC.dup a = 𝖽[a]"
      by (metis (no_types, lifting) CMC.ECC.tuple_eqI assms ideD(1) pr_agreement(1-2) pr_dup(1-2))

  end

section "Cartesian Monoidal Category from Elementary Cartesian Category"

  context elementary_cartesian_category
  begin

    interpretation MC: monoidal_category C Prod α ι
      using induces_monoidal_categoryECC by blast

    (*
     * TODO: There are a number of facts from the monoidal_category locale that it
     * would be useful to re-interpret in the present context.  The following is one
     * for which we have an immediate use, but some systematic plan is needed here.
     *)

    lemma triangle:
    assumes "ide a" and "ide b"
    shows "(a  𝗅[b])  𝖺[a, 𝟭, b] = 𝗋[a]  b"
      using assms MC.triangle [of a b] assoc_agreement ide_one lunit_agreement
            runit_agreement unity_agreement fst_conv snd_conv
      by (metis (no_types, lifting))

    lemma induces_elementary_cartesian_monoidal_categoryECC:
    shows "elementary_cartesian_monoidal_category (⋅) prod 𝟭 lunit runit assoc trm dup"
      using ide_one inverse_arrows_lunit inverse_arrows_runit inverse_arrows_assoc
            interchange lunit_naturality runit_naturality assoc_naturality
            triangle pentagon comp_assoc trm_one trm_naturality
            in_homI prod_tuple isoI arr_dom MC.tensor_in_homI comp_arr_dom comp_cod_arr
      apply unfold_locales
                          apply simp_all
           apply blast
          apply blast
         by meson

  end

  context cartesian_category
  begin

    interpretation ECC: elementary_cartesian_category C
                          some_pr0 some_pr1 some_terminal some_terminator
      using extends_to_elementary_cartesian_category by simp

    lemma extends_to_cartesian_monoidal_categoryCC:
    shows "cartesian_monoidal_category C ECC.Prod ECC.α ECC.ι"
      using ECC.extends_to_cartesian_monoidal_categoryECC by blast

  end

  (*
   * TODO: I would like to have coherence theorems for symmetric monoidal and cartesian
   * monoidal categories here, but I haven't yet figured out a suitably economical way
   * to extend the existing result.
   *)

end