Theory MonoidalCategory.MonoidalCategory

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

chapter "Monoidal Category"

text_raw‹
\label{monoidal-category-chap}
›

text ‹
  In this theory, we define the notion ``monoidal category,'' and develop consequences of
  the definition.  The main result is a proof of MacLane's coherence theorem.
›
    
theory MonoidalCategory
imports Category3.EquivalenceOfCategories
begin

  section "Monoidal Category"

  text ‹
    A typical textbook presentation defines a monoidal category to be a category @{term C}
    equipped with (among other things) a binary ``tensor product'' functor ⊗: C × C → C›
    and an ``associativity'' natural isomorphism α›, whose components are isomorphisms
    α (a, b, c): (a ⊗ b) ⊗ c → a ⊗ (b ⊗ c)› for objects a›, b›,
    and c› of C›.  This way of saying things avoids an explicit definition of
    the functors that are the domain and codomain of α› and, in particular, what category
    serves as the domain of these functors.  The domain category is in fact the product
    category C × C × C› and the domain and codomain of α› are the functors
    T o (T × C): C × C × C → C› and T o (C × T): C × C × C → C›.
    In a formal development, though, we can't gloss over the fact that
    C × C × C› has to mean either C × (C × C)› or (C × C) × C›,
    which are not formally identical, and that associativities are somehow involved in the
    definitions of the functors T o (T × C)› and T o (C × T)›.
    Here we use the @{locale binary_endofunctor} locale to codify our choices about what
    C × C × C›, T o (T × C)›, and T o (C × T)› actually mean.
    In particular, we choose C × C × C› to be C × (C × C)› and define the
    functors T o (T × C)›, and T o (C × T)› accordingly.
›

  text ‹
    Our primary definition for ``monoidal category'' follows the somewhat non-traditional
    development in cite"Etingof15".  There a monoidal category is defined to be a category
    C› equipped with a binary \emph{tensor product} functor T: C × C → C›,
    an \emph{associativity isomorphism}, which is a natural isomorphism
    α: T o (T × C) → T o (C × T)›, a \emph{unit object} ℐ› of C›,
    and an isomorphism ι: T (ℐ, ℐ) → ℐ›, subject to two axioms:
    the \emph{pentagon axiom}, which expresses the commutativity of certain pentagonal diagrams
    involving components of α›, and the left and right \emph{unit axioms}, which state
    that the endofunctors T (ℐ, -)› and T (-, ℐ)› are equivalences of categories.
    This definition is formalized in the monoidal_category› locale.

    In more traditional developments, the definition of monoidal category involves additional
    left and right \emph{unitor} isomorphisms λ› and ρ› and associated axioms
    involving their components.
    However, as is shown in cite"Etingof15" and formalized here, the unitors are uniquely
    determined by α› and their values λ(ℐ)› and ρ(ℐ)› at ℐ›,
    which coincide.  Treating λ› and ρ› as defined notions results in a more
    economical basic definition of monoidal category that requires less data to be given,
    and has a similar effect on the definition of ``monoidal functor.''
    Moreover, in the context of the formalization of categories that we use here,
    the unit object ℐ› also need not be given separately, as it can be obtained as the
    codomain of the isomorphism ι›.
›

  locale monoidal_category =
    category C +
    CC: product_category C C +
    CCC: product_category C CC.comp +
    T: binary_endofunctor C T +
    α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α +
    L: equivalence_functor C C "λf. T (cod ι, f)" +
    R: equivalence_functor C C "λf. T (f, cod ι)"
  for C :: "'a comp"       (infixr  55)
  and T :: "'a * 'a  'a"
  and α :: "'a * 'a * 'a  'a"
  and ι :: 'a +
  assumes unit_in_hom_ax: "«ι : T (cod ι, cod ι)  cod ι»"
  and unit_is_iso: "iso ι"
  and pentagon: " ide a; ide b; ide c; ide d  
                 T (a, α (b, c, d))  α (a, T (b, c), d)  T (α (a, b, c), d) =
                 α (a, b, T (c, d))  α (T (a, b), c, d)"
  begin

    text‹
      We now define helpful notation and abbreviations to improve readability.
      We did not define and use the notation ⊗› for the tensor product
      in the definition of the locale because to define ⊗› as a binary
      operator requires that it be in curried form, whereas for T›
      to be a binary functor requires that it take a pair as its argument.
›

    abbreviation unity :: 'a ()
    where "unity  cod ι"

    abbreviation L :: "'a  'a"
    where "L f  T (, f)"

    abbreviation R :: "'a  'a"
    where "R f  T (f, )"

    abbreviation tensor      (infixr  53)
    where "f  g  T (f, g)"

    abbreviation assoc       (𝖺[_, _, _])
    where "𝖺[a, b, c]  α (a, b, c)"

    text‹
      In HOL we can just give the definitions of the left and right unitors ``up front''
      without any preliminary work.  Later we will have to show that these definitions
      have the right properties.  The next two definitions define the values of the
      unitors when applied to identities; that is, their components as natural transformations.
›

    definition lunit (𝗅[_])
    where "lunit a  THE f. «f :   a  a»    f = (ι  a)  inv 𝖺[, , a]"

    definition runit (𝗋[_])
    where "runit a  THE f. «f : a    a»  f   = (a  ι)  𝖺[a, , ]"

    text‹
      We now embark upon a development of the consequences of the monoidal category axioms.
      One of our objectives is to be able to show that an interpretation of the
      monoidal_category› locale induces an interpretation of a locale corresponding
      to a more traditional definition of monoidal category.
      Another is to obtain the facts we need to prove the coherence theorem.
›

    lemma unit_in_hom [intro]:
    shows "«ι :     »"
      using unit_in_hom_ax by force

    lemma ide_unity [simp]:
    shows "ide "
      using unit_in_hom by auto

    lemma tensor_in_hom [simp]:
    assumes "«f : a  b»" and "«g : c  d»"
    shows "«f  g : a  c  b  d»"
      using assms T.preserves_hom CC.arr_char by simp

    lemma tensor_in_homI [intro]:
    assumes "«f : a  b»" and "«g : c  d»" and "x = a  c" and "y = b  d"
    shows "«f  g : x  y»"
      using assms tensor_in_hom
      by force

    lemma arr_tensor [simp]:
    assumes "arr f" and "arr g"
    shows "arr (f  g)"
      using assms by simp

    lemma dom_tensor [simp]:
    assumes "«f : a  b»" and "«g : c  d»"
    shows "dom (f  g) = a  c"
      using assms by fastforce

    lemma cod_tensor [simp]:
    assumes "«f : a  b»" and "«g : c  d»"
    shows "cod (f  g) = b  d"
      using assms by fastforce

    lemma tensor_preserves_ide [simp]:
    assumes "ide a" and "ide b"
    shows "ide (a  b)"
      using assms T.preserves_ide CC.ide_char by simp

    lemma tensor_preserves_iso [simp]:
    assumes "iso f" and "iso g"
    shows "iso (f  g)"
      using assms by simp

    lemma inv_tensor [simp]:
    assumes "iso f" and "iso g"
    shows "inv (f  g) = inv f  inv g"
      using assms T.preserves_inv by auto

    lemma interchange:
    assumes "seq h g" and "seq h' g'"
    shows "(h  h')  (g  g') = h  g  h'  g'"
      using assms T.preserves_comp [of "(h, h')" "(g, g')"] by simp

    lemma α_simp:
    assumes "arr f" and "arr g" and "arr h"
    shows "α (f, g, h) = (f  g  h)  𝖺[dom f, dom g, dom h]"
      using assms α.is_natural_1 [of "(f, g, h)"] by simp

    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 CCC.in_homE by auto

    lemma arr_assoc [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "arr 𝖺[a, b, c]"
      using assms assoc_in_hom by simp

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

    lemma cod_assoc [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "cod 𝖺[a, b, c] = a  b  c"
      using assms assoc_in_hom by simp

    lemma assoc_naturality:
    assumes "arr f0" and "arr f1" and "arr f2"
    shows "𝖺[cod f0, cod f1, cod f2]  ((f0  f1)  f2) =
           (f0  f1  f2)  𝖺[dom f0, dom f1, dom f2]"
      using assms α.naturality by auto

    lemma iso_assoc [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "iso 𝖺[a, b, c]"
      using assms α.preserves_iso by simp

    text‹
      The next result uses the fact that the functor L› is an equivalence
      (and hence faithful) to show the existence of a unique solution to the characteristic
      equation used in the definition of a component @{term "𝗅[a]"} of the left unitor.
      It follows that @{term "𝗅[a]"}, as given by our definition using definite description,
      satisfies this characteristic equation and is therefore uniquely determined by
      by ⊗›, @{term α}, and ι›.
›

    lemma lunit_char:
    assumes "ide a"
    shows "«𝗅[a] :   a  a»" and "  𝗅[a] = (ι  a)  inv 𝖺[, , a]"
    and "∃!f. «f :   a  a»    f = (ι  a)  inv 𝖺[, , a]"
    proof -
      obtain F η ε where L: "equivalence_of_categories C C F (λf.   f) η ε"
        using L.induces_equivalence by auto
      interpret L: equivalence_of_categories C C F λf.   f η ε
        using L by auto
      let ?P = "λf. «f :   a  a»    f = (ι  a)  inv 𝖺[, , a]"
      show "∃!f. ?P f"
      proof -
        have "f. ?P f"
        proof -
          have "«(ι  a)  inv 𝖺[, , a] :     a    a»"
          proof
            show "«ι  a : (  )  a    a»"
              using assms ide_in_hom by blast
            show "«inv 𝖺[, , a] :     a  (  )  a»"
              using assms by auto
          qed
          moreover have "ide (  a)" using assms by simp
          ultimately show ?thesis
            using assms L.is_full by blast
        qed
        moreover have "f f'. ?P f  ?P f'  f = f'"
          by (metis L.is_faithful in_homE)
        ultimately show ?thesis by blast
      qed
      hence 1: "?P 𝗅[a]"
        unfolding lunit_def using theI' [of ?P] by auto
      show "«𝗅[a] :   a  a»" using 1 by fast
      show "  𝗅[a] = (ι  a)  inv 𝖺[, , a]" using 1 by fast
    qed

    lemma lunit_in_hom [intro]:
    assumes "ide a"
    shows "«𝗅[a] :   a  a»"
      using assms lunit_char(1) by blast

    lemma arr_lunit [simp]:
    assumes "ide a"
    shows "arr 𝗅[a]"
      using assms lunit_in_hom by auto

    lemma dom_lunit [simp]:
    assumes "ide a"
    shows "dom 𝗅[a] =   a"
      using assms lunit_in_hom by auto

    lemma cod_lunit [simp]:
    assumes "ide a"
    shows "cod 𝗅[a] = a"
      using assms lunit_in_hom by auto

    text‹
      As the right-hand side of the characteristic equation for @{term "  𝗅[a]"}
      is an isomorphism, and the equivalence functor L› reflects isomorphisms,
      it follows that @{term "𝗅[a]"} is an isomorphism.
›

    lemma iso_lunit [simp]:
    assumes "ide a"
    shows "iso 𝗅[a]"
      using assms lunit_char(2) unit_is_iso ide_unity isos_compose iso_assoc iso_inv_iso
            unit_in_hom L.reflects_iso arr_lunit arr_tensor ideD(1) ide_is_iso lunit_in_hom
            tensor_preserves_iso
      by metis

    text‹
      To prove that an arrow @{term f} is equal to @{term "𝗅[a]"} we need only show
      that it is parallel to @{term "𝗅[a]"} and that @{term "  f"} satisfies the same
      characteristic equation as @{term "  𝗅[a]"} does.
›

    lemma lunit_eqI:
    assumes "«f :   a  a»" and "  f = (ι  a)  inv 𝖺[, , a]"
    shows "f = 𝗅[a]"
    proof -
      have "ide a" using assms(1) by auto
      thus ?thesis
        using assms lunit_char the1_equality by blast
    qed

    text‹
      The next facts establish the corresponding results for the components of the
      right unitor.
›

    lemma runit_char:
    assumes "ide a"
    shows "«𝗋[a] : a    a»" and "𝗋[a]   = (a  ι)  𝖺[a, , ]"
    and "∃!f. «f : a    a»  f   = (a  ι)  𝖺[a, , ]"
    proof -
      obtain F η ε where R: "equivalence_of_categories C C F (λf. f  ) η ε"
        using R.induces_equivalence by auto
      interpret R: equivalence_of_categories C C F λf. f   η ε
        using R by auto
      let ?P = "λf. «f : a    a»  f   = (a  ι)  𝖺[a, , ]"
      show "∃!f. ?P f"
      proof -
        have "f. ?P f"
        proof -
          have "«(a  ι)  𝖺[a, , ] : (a  )    a  »"
            using assms by fastforce
          moreover have "ide (a  )" using assms by simp
          ultimately show ?thesis
            using assms R.is_full [of a "a  " "(a  ι)  𝖺[a, , ]"] by blast
        qed
        moreover have "f f'. ?P f  ?P f'  f = f'"
          by (metis R.is_faithful in_homE)
        ultimately show ?thesis by blast
      qed
      hence 1: "?P 𝗋[a]" unfolding runit_def using theI' [of ?P] by fast
      show "«𝗋[a] : a    a»" using 1 by fast
      show "𝗋[a]   = (a  ι)  𝖺[a, , ]" using 1 by fast
    qed

    lemma runit_in_hom [intro]:
    assumes "ide a"
    shows "«𝗋[a] : a    a»"
      using assms runit_char(1) by blast

    lemma arr_runit [simp]:
    assumes "ide a"
    shows "arr 𝗋[a]"
      using assms runit_in_hom by blast

    lemma dom_runit [simp]:
    assumes "ide a"
    shows "dom 𝗋[a] = a  "
      using assms runit_in_hom by blast

    lemma cod_runit [simp]:
    assumes "ide a"
    shows "cod 𝗋[a] = a"
      using assms runit_in_hom by blast

    lemma runit_eqI:
    assumes "«f : a    a»" and "f   = (a  ι)  𝖺[a, , ]"
    shows "f = 𝗋[a]"
    proof -
      have "ide a" using assms(1) by auto
      thus ?thesis
        using assms runit_char the1_equality by blast
    qed

    lemma iso_runit [simp]:
    assumes "ide a"
    shows "iso 𝗋[a]"
      using assms unit_is_iso iso_inv_iso isos_compose ide_is_iso R.preserves_reflects_arr
            arrI ide_unity iso_assoc runit_char tensor_preserves_iso R.reflects_iso
      by metis

    text‹
      We can now show that the components of the left and right unitors have the
      naturality properties required of a natural transformation.
›

    lemma lunit_naturality:
    assumes "arr f"
    shows "𝗅[cod f]  (  f) = f  𝗅[dom f]"
    proof -
      interpret α': inverse_transformation CCC.comp C T.ToTC T.ToCT α ..
      have par: "par (𝗅[cod f]  (  f)) (f  𝗅[dom f])"
        using assms by simp
      moreover have "  𝗅[cod f]  (  f) =   f  𝗅[dom f]"
      proof -
        have "  𝗅[cod f]  (  f) = ((ι  cod f)  ((  )  f))  inv 𝖺[, , dom f]"
          using assms interchange [of   "  f" "𝗅[cod f]"] lunit_char(2)
                α'.naturality [of "(, , f)"] comp_assoc
          by auto
        also have "... = ((  f)  (ι  dom f))  inv 𝖺[, , dom f]"
          using assms interchange comp_arr_dom comp_cod_arr unit_in_hom by auto
        also have "... = (  f)  (  𝗅[dom f])"
          using assms lunit_char(2) comp_assoc by auto
        also have "... =   f  𝗅[dom f]"
          using assms interchange L.preserves_comp par by metis
        finally show ?thesis by blast
      qed
      ultimately show "𝗅[cod f]  (  f) = f  𝗅[dom f]"
        using L.is_faithful by metis
    qed

    lemma runit_naturality:
    assumes "arr f"
    shows "𝗋[cod f]  (f  ) = f  𝗋[dom f]"
    proof -
      have par: "par (𝗋[cod f]  (f  )) (f  𝗋[dom f])"
        using assms by force
      moreover have "𝗋[cod f]  (f  )   = f  𝗋[dom f]  "
      proof -
        have "𝗋[cod f]  (f  )   = (cod f  ι)  𝖺[cod f, , ]  ((f  )  )"
          using assms interchange [of   "  f" "𝗋[cod f]"] runit_char(2)
                comp_assoc
          by auto
        also have "... = (cod f  ι)  (f    )   𝖺[dom f, , ]"
          using assms α.naturality [of "(f, , )"] by auto
        also have "... = ((cod f  ι)  (f    ))  𝖺[dom f, , ]"
          using comp_assoc by simp
        also have "... = ((f  )  (dom f  ι))  𝖺[dom f, , ]"
          using assms unit_in_hom interchange comp_arr_dom comp_cod_arr by auto
        also have "... = (f  )  (𝗋[dom f]  )"
          using assms runit_char comp_assoc by auto
        also have "... = f  𝗋[dom f]  "
          using assms interchange R.preserves_comp par by metis
        finally show ?thesis by blast
      qed
      ultimately show "𝗋[cod f]  (f  ) = f  𝗋[dom f]"
        using R.is_faithful by metis
    qed

    text‹
      The next two definitions extend the unitors to all arrows, not just identities.
      Unfortunately, the traditional symbol λ› for the left unitor is already
      reserved for a higher purpose, so we have to make do with a poor substitute.
›

    abbreviation 𝔩
    where "𝔩 f  if arr f then f  𝗅[dom f] else null"

    abbreviation ρ
    where "ρ f  if arr f then f  𝗋[dom f] else null"

    lemma 𝔩_ide_simp:
    assumes "ide a"
    shows "𝔩 a = 𝗅[a]"
      using assms lunit_char comp_cod_arr ide_in_hom by (metis in_homE)

    lemma ρ_ide_simp:
    assumes "ide a"
    shows "ρ a = 𝗋[a]"
      using assms runit_char [of a] comp_cod_arr by auto

  end

  context monoidal_category
  begin

    sublocale 𝔩: natural_transformation C C L map 𝔩
    proof -
      interpret 𝔩: transformation_by_components C C L map λa. 𝗅[a]
        using lunit_in_hom lunit_naturality unit_in_hom_ax L.is_extensional
        by (unfold_locales, auto)
      have "𝔩.map = 𝔩"
        using 𝔩.is_natural_1 𝔩.is_extensional by auto
      thus "natural_transformation C C L map 𝔩"
        using 𝔩.natural_transformation_axioms by auto
    qed

    sublocale 𝔩: natural_isomorphism C C L map 𝔩
      apply unfold_locales
      using iso_lunit 𝔩_ide_simp by simp

    sublocale ρ: natural_transformation C C R map ρ
    proof -
      interpret ρ: transformation_by_components C C R map λa. 𝗋[a]
        using runit_naturality unit_in_hom_ax R.is_extensional
        by (unfold_locales, auto)
      have "ρ.map = ρ"
        using ρ.is_natural_1 ρ.is_extensional by auto
      thus "natural_transformation C C R map ρ"
        using ρ.natural_transformation_axioms by auto
    qed

    sublocale ρ: natural_isomorphism C C R map ρ
      apply unfold_locales
      using ρ_ide_simp by simp

    sublocale 𝔩': inverse_transformation C C L map 𝔩 ..
    sublocale ρ': inverse_transformation C C R map ρ ..
    sublocale α': inverse_transformation CCC.comp C T.ToTC T.ToCT α ..

    abbreviation α'
    where "α'  α'.map"

    abbreviation assoc' (𝖺-1[_, _, _])
    where "𝖺-1[a, b, c]  inv 𝖺[a, b, c]"

    lemma α'_ide_simp:
    assumes "ide a" and "ide b" and "ide c"
    shows "α' (a, b, c) = 𝖺-1[a, b, c]"
      using assms α'.inverts_components inverse_unique by force

    lemma α'_simp:
    assumes "arr f" and "arr g" and "arr h"
    shows "α' (f, g, h) = ((f  g)  h)  𝖺-1[dom f, dom g, dom h]"
      using assms T.ToTC_simp α'.is_natural_1 α'_ide_simp by force

    lemma assoc_inv:
    assumes "ide a" and "ide b" and "ide c"
    shows "inverse_arrows 𝖺[a, b, c] 𝖺-1[a, b, c]"
      using assms inv_is_inverse by simp

    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 by auto

    lemma arr_assoc' [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "arr 𝖺-1[a, b, c]"
      using assms by simp

    lemma dom_assoc' [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "dom 𝖺-1[a, b, c] = a  b  c"
      using assms by simp

    lemma cod_assoc' [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "cod 𝖺-1[a, b, c] = (a  b)  c"
      using assms by simp

    lemma comp_assoc_assoc' [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "𝖺[a, b, c]  𝖺-1[a, b, c] = a  (b  c)"
    and "𝖺-1[a, b, c]  𝖺[a, b, c] = (a  b)  c"
      using assms assoc_inv comp_arr_inv comp_inv_arr by auto

    lemma assoc'_naturality:
    assumes "arr f0" and "arr f1" and "arr f2"
    shows "((f0  f1)  f2)  𝖺-1[dom f0, dom f1, dom f2] =
           𝖺-1[cod f0, cod f1, cod f2]  (f0  f1  f2)"
      using assms α'.naturality by auto

    abbreviation 𝔩'
    where "𝔩'  𝔩'.map"

    abbreviation lunit'                (𝗅-1[_])
    where "𝗅-1[a]  inv 𝗅[a]"

    lemma 𝔩'_ide_simp:
    assumes "ide a"
    shows "𝔩'.map a = 𝗅-1[a]"
      using assms 𝔩'.inverts_components 𝔩_ide_simp inverse_unique by force

    lemma lunit_inv:
    assumes "ide a"
    shows "inverse_arrows 𝗅[a] 𝗅-1[a]"
      using assms inv_is_inverse by simp

    lemma lunit'_in_hom [intro]:
    assumes "ide a"
    shows "«𝗅-1[a] : a    a»"
      using assms by auto

    lemma comp_lunit_lunit' [simp]:
    assumes "ide a"
    shows "𝗅[a]  𝗅-1[a] = a"
    and "𝗅-1[a]  𝗅[a] =   a"
    proof -
      show "𝗅[a]  𝗅-1[a] = a"
        using assms comp_arr_inv lunit_inv by fastforce
      show "𝗅-1[a]  𝗅[a] =   a"
        using assms comp_arr_inv lunit_inv by fastforce
    qed

    lemma lunit'_naturality:
    assumes "arr f"
    shows "(  f)  𝗅-1[dom f] = 𝗅-1[cod f]  f"
      using assms 𝔩'.naturality 𝔩'_ide_simp by simp

    abbreviation ρ'
    where "ρ'  ρ'.map"

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

    lemma ρ'_ide_simp:
    assumes "ide a"
    shows "ρ'.map a = 𝗋-1[a]"
      using assms ρ'.inverts_components ρ_ide_simp inverse_unique by auto

    lemma runit_inv:
    assumes "ide a"
    shows "inverse_arrows 𝗋[a] 𝗋-1[a]"
      using assms inv_is_inverse by simp

    lemma runit'_in_hom [intro]:
    assumes "ide a"
    shows "«𝗋-1[a] : a  a  »"
      using assms by auto

    lemma comp_runit_runit' [simp]:
    assumes "ide a"
    shows "𝗋[a]  𝗋-1[a] = a"
    and "𝗋-1[a]  𝗋[a] = a  "
    proof -
      show "𝗋[a]  𝗋-1[a] = a"
        using assms runit_inv by fastforce
      show "𝗋-1[a]  𝗋[a] = a  "
        using assms runit_inv by fastforce
    qed

    lemma runit'_naturality:
    assumes "arr f"
    shows "(f  )  𝗋-1[dom f] = 𝗋-1[cod f]  f"
      using assms ρ'.naturality ρ'_ide_simp by simp

    lemma lunit_commutes_with_L:
    assumes "ide a"
    shows "𝗅[  a] =   𝗅[a]"
      using assms lunit_naturality lunit_in_hom iso_lunit iso_is_section
            section_is_mono monoE L.preserves_ide arrI cod_lunit dom_lunit seqI
      by metis

    lemma runit_commutes_with_R:
    assumes "ide a"
    shows "𝗋[a  ] = 𝗋[a]  "
      using assms runit_naturality runit_in_hom iso_runit iso_is_section
            section_is_mono monoE R.preserves_ide arrI cod_runit dom_runit seqI
      by metis

    text‹
      The components of the left and right unitors are related via a ``triangle''
      diagram that also involves the associator.
      The proof follows cite"Etingof15", Proposition 2.2.3.
›

    lemma triangle:
    assumes "ide a" and "ide b"
    shows "(a  𝗅[b])  𝖺[a, , b] = 𝗋[a]  b"
    proof -
      text‹
        We show that the lower left triangle in the following diagram commutes.
›
      text‹
$$\xymatrix{
  {@{term "((a  )  )  b"}}
     \ar[rrrr]^{\scriptsize @{term "𝖺[a, , ]  b"}}
     \ar[ddd]_{\scriptsize @{term "𝖺[a  , , b]"}}
     \ar[drr]_{\scriptsize @{term "(𝗋[a]  )  b"}}
  && &&
  {@{term "(a  (  ))  b"}}
     \ar[dll]^{\scriptsize @{term "(a  ι)  b"}}
     \ar[ddd]^{\scriptsize @{term "𝖺[a,   , b]"}} \\
  && {@{term "(a  )  b"}}
      \ar[d]^{\scriptsize @{term "𝖺[a, , b]"}} \\
  && {@{term "a    b"}}  \\
  {@{term "(a  )    b"}}
      \ar[urr]^{\scriptsize @{term "𝗋[a]    b"}}
      \ar[drr]_{\scriptsize @{term "𝖺[a, ,   b]"}}
  && &&
  {@{term "a  (  )  b"}}
      \ar[ull]_{\scriptsize @{term "a  ι  b"}}
      \ar[dll]^{\scriptsize @{term "a  𝖺[, , b]"}}  \\
  && {@{term "a      b"}}
      \ar[uu]^{\scriptsize @{term "a  𝗅[  b]"}}
}$$
›
      have *: "(a  𝗅[  b])  𝖺[a, ,   b] = 𝗋[a]    b"
      proof -
        have 1: "((a  𝗅[  b])  𝖺[a, ,   b])  𝖺[a  , , b]
                    = (𝗋[a]    b)  𝖺[a  , , b]"
        proof -
          have "((a  𝗅[  b])  𝖺[a, ,   b])  𝖺[a  , , b] =
                ((a  𝗅[  b])  (a  𝖺[, , b]))  𝖺[a,   , b]  (𝖺[a, , ]  b)"
            using assms pentagon comp_assoc by auto
          also have "... = (a  ((  𝗅[b])  𝖺[, , b]))  𝖺[a,   , b]  (𝖺[a, , ]  b)"
            using assms interchange lunit_commutes_with_L by simp
          also have "... = ((a  (ι  b))  𝖺[a,   , b])  (𝖺[a, , ]  b)"
            using assms lunit_char unit_in_hom comp_arr_dom comp_assoc by auto
          also have "... = (𝖺[a, , b]  ((a  ι)  b))  (𝖺[a, , ]  b)"
            using assms unit_in_hom assoc_naturality [of a ι b] by fastforce
          also have "... = 𝖺[a, , b]  ((𝗋[a]  )  b)"
            using assms unit_in_hom interchange runit_char(2) comp_assoc by auto
          also have "... = (𝗋[a]    b)  𝖺[a  , , b]"
            using assms assoc_naturality [of "𝗋[a]"  b] by simp
          finally show ?thesis by blast
        qed
        show ?thesis
        proof -
          have "epi 𝖺[a  , , b]"
            using assms iso_assoc iso_is_retraction retraction_is_epi by simp
          thus ?thesis
            using 1 assms epiE [of "𝖺[a  , , b]" "(a  𝗅[  b])  𝖺[a, ,   b]"]
            by fastforce
        qed
      qed
      text‹
         In cite"Etingof15" it merely states that the preceding result suffices
         ``because any object of C› is isomorphic to one of the form @{term "  b"}.''
         However, it seems a little bit more involved than that to formally transport the
         equation (*)› along the isomorphism @{term "𝗅[b]"} from @{term "  b"}
         to @{term b}.
›
      have "(a  𝗅[b])  𝖺[a, , b] = ((a  𝗅[b])  (a  𝗅[  b])  (a    𝗅-1[b])) 
                                     (a    𝗅[b])  𝖺[a, ,   b]  ((a  )  𝗅-1[b])"
      proof -
        have "𝖺[a, , b] = (a    𝗅[b])  𝖺[a, ,   b]  ((a  )  𝗅-1[b])"
        proof -
          have "(a    𝗅[b])  𝖺[a, ,   b]  ((a  )  𝗅-1[b])
                  = ((a    𝗅[b])  (a    𝗅-1[b]))  𝖺[a, , b]"
            using assms assoc_naturality [of a  "𝗅-1[b]"] comp_assoc by simp
          also have "... = 𝖺[a, , b]"
            using assms inv_is_inverse interchange comp_cod_arr by simp
          finally show ?thesis by auto
        qed
        moreover have "a  𝗅[b] = (a  𝗅[b])  (a  𝗅[  b])  (a    𝗅-1[b])"
          using assms lunit_commutes_with_L comp_arr_dom interchange by auto
        ultimately show ?thesis by argo
      qed
      also have "... = (a  𝗅[b])  (a  𝗅[  b])  ((a    𝗅-1[b])  (a    𝗅[b])) 
                       𝖺[a, ,   b]  ((a  )  𝗅-1[b])"
        using assms comp_assoc by auto
      also have "... = (a  𝗅[b])  ((a  𝗅[  b])  𝖺[a, ,   b])  ((a  )  𝗅-1[b])"
        using assms interchange comp_cod_arr comp_assoc by auto
      also have "... = 𝗋[a]  b"
        using assms * interchange runit_char(1) comp_arr_dom comp_cod_arr by auto
      finally show ?thesis by blast
    qed

    lemma lunit_tensor_gen:
    assumes "ide a" and "ide b" and "ide c"
    shows "(a  𝗅[b  c])  (a  𝖺[, b, c]) = a  𝗅[b]  c"
    proof -
      text‹
        We show that the lower right triangle in the following diagram commutes.
›
      text‹
$$\xymatrix{
  {@{term "((a  )  b)  c"}}
     \ar[rrrr]^{\scriptsize @{term "𝖺[a, , b]  c"}}
     \ar[ddd]_{\scriptsize @{term "𝖺[a  , b, c]"}}
     \ar[drr]_{\scriptsize @{term "𝗋[a]  b  c"}}
  && &&
  {@{term "(a  (  b))  c"}}
     \ar[dll]^{\scriptsize @{term "(a  𝗅[b])  c"}}
     \ar[ddd]^{\scriptsize @{term "𝖺[a,   b, c]"}} \\
  && {@{term "(a  b)  c"}}
      \ar[d]^{\scriptsize @{term "𝖺[a, b, c]"}}    \\
  && {@{term "a  b  c"}}        \\
  {@{term "(a  )  b  c"}}
      \ar[urr]^{\scriptsize @{term "𝗋[a]  b  c"}}
      \ar[drr]_{\scriptsize @{term "𝖺[a, , b  c]"}}
  && &&
  {@{term "a  (  b)  c"}}
      \ar[ull]_{\scriptsize @{term "a  𝗅[b]  c"}}
      \ar[dll]^{\scriptsize @{term "a  𝖺[, b, c]"}}  \\
  && {@{term "a    b  c"}}
      \ar[uu]^{\scriptsize @{term "a  𝗅[b  c]"}}
}$$
›
      have "((a  𝗅[b  c])  (a  𝖺[, b, c]))  (𝖺[a,   b, c]  (𝖺[a, , b]  c)) =
            ((a  𝗅[b  c])  𝖺[a, , b  c])  𝖺[a  , b, c]"
        using assms pentagon comp_assoc by simp
      also have "... = (𝗋[a]  (b  c))  𝖺[a  , b, c]"
        using assms triangle by auto
      also have "... = 𝖺[a, b, c]  ((𝗋[a]  b)  c)"
        using assms assoc_naturality [of "𝗋[a]" b c] by auto
      also have "... = (𝖺[a, b, c]  ((a  𝗅[b])  c))  (𝖺[a, , b]  c)"
        using assms triangle interchange comp_assoc by auto
      also have "... = (a  (𝗅[b]  c))  (𝖺[a,   b, c]  (𝖺[a, , b]  c))"
        using assms assoc_naturality [of a "𝗅[b]" c] comp_assoc by auto
      finally have 1: "((a  𝗅[b  c])  (a  𝖺[, b, c]))  𝖺[a,   b, c]  (𝖺[a, , b]  c)
                        = (a  (𝗅[b]  c))  𝖺[a,   b, c]  (𝖺[a, , b]  c)"
        by blast
      text‹
        The result follows by cancelling the isomorphism
        @{term "𝖺[a,   b, c]  (𝖺[a, , b]  c)"}
      have 2: "iso (𝖺[a,   b, c]  (𝖺[a, , b]  c))"
        using assms isos_compose by simp
      moreover have
          "seq ((a  𝗅[b  c])  (a  𝖺[, b, c])) (𝖺[a,   b, c]  (𝖺[a, , b]  c))"
        using assms by auto
      moreover have "seq (a  (𝗅[b]  c)) (𝖺[a,   b, c]  (𝖺[a, , b]  c))"
        using assms by auto
      ultimately show ?thesis
        using 1 2 assms iso_is_retraction retraction_is_epi
              epiE [of "𝖺[a,   b, c]  (𝖺[a, , b]  c)"
                       "(a  𝗅[b  c])  (a  𝖺[, b, c])" "a  𝗅[b]  c"]
        by auto
    qed

    text‹
      The following result is quoted without proof as Theorem 7 of cite"Kelly64" where it is
      attributed to MacLane cite"MacLane63".  It also appears as cite"MacLane71",
      Exercise 1, page 161.  I did not succeed within a few hours to construct a proof following
      MacLane's hint.  The proof below is based on cite"Etingof15", Proposition 2.2.4.
›

    lemma lunit_tensor':
    assumes "ide a" and "ide b"
    shows "𝗅[a  b]  𝖺[, a, b] = 𝗅[a]  b"
    proof -
      have "  (𝗅[a  b]  𝖺[, a, b]) =   (𝗅[a]  b)"
        using assms interchange [of  ] lunit_tensor_gen by simp
      moreover have "par (𝗅[a  b]  𝖺[, a, b]) (𝗅[a]  b)"
        using assms by simp
      ultimately show ?thesis
        using assms L.is_faithful [of "𝗅[a  b]  𝖺[, a, b]" "𝗅[a]  b"] by simp
    qed

    lemma lunit_tensor:
    assumes "ide a" and "ide b"
    shows "𝗅[a  b] = (𝗅[a]  b)  𝖺-1[, a, b]"
      using assms lunit_tensor' invert_side_of_triangle by simp

    text‹
      We next show the corresponding result for the right unitor.
›
      
    lemma runit_tensor_gen:
    assumes "ide a" and "ide b" and "ide c"
    shows "𝗋[a  b]  c = ((a  𝗋[b])  c)  (𝖺[a, b, ]  c)"
    proof -
      text‹
        We show that the upper right triangle in the following diagram commutes.
›
      text‹
$$\xymatrix{
  && {@{term "((a  b)  )  c"}}
     \ar[dll]_{\scriptsize @{term "𝖺[a  b, , c]"}}
     \ar[dd]^{\scriptsize @{term "𝗋[a  b]  c"}}
     \ar[drr]^{\scriptsize @{term "𝖺[a, b, ]  c"}} \\
  {@{term "(a  b)    c"}}
     \ar[ddd]_{\scriptsize @{term "𝖺[a, b,   c]"}}
     \ar[drr]_{\scriptsize @{term "(a  b)  𝗅[c]"}}
  && &&
  {@{term "(a  b  )  c"}}
     \ar[dll]^{\scriptsize @{term "(a  𝗋[b])  c"}}
     \ar[ddd]^{\scriptsize @{term "𝖺[a, b  , c]"}} \\
  && {@{term "(a  b)  c"}}
     \ar[d]^{\scriptsize @{term "𝖺[a, b, c]"}}     \\
  && {@{term "a  b  c"}}        \\
  {@{term "a  b    c"}}
     \ar[urr]^{\scriptsize @{term "a  b  𝗅[c]"}}
  && &&
  {@{term "a  (b  )  c"}}
     \ar[llll]^{\scriptsize @{term "a  𝖺[b, , c]"}}
     \ar[ull]_{\scriptsize @{term "a  𝗋[b]  c"}}
}$$
›
      have "𝗋[a  b]  c = ((a  b)  𝗅[c])  𝖺[a  b, , c]"
        using assms triangle by simp
      also have "... = (𝖺-1[a, b, c]  (a  b  𝗅[c])  𝖺[a, b,   c])  𝖺[a  b, , c]"
        using assms assoc_naturality [of a b "𝗅[c]"] comp_arr_dom comp_cod_arr
              invert_side_of_triangle(1)
        by force
      also have "... = 𝖺-1[a, b, c]  (a  b  𝗅[c])  𝖺[a, b,   c]  𝖺[a  b, , c]"
        using comp_assoc by force
      also have "... = 𝖺-1[a, b, c]  ((a  (𝗋[b]  c))  (a  𝖺-1[b, , c])) 
                       𝖺[a, b,   c]  𝖺[a  b, , c]"
        using assms triangle [of b c] interchange invert_side_of_triangle(2) by force
      also have "... = (((a  𝗋[b])  c)  𝖺-1[a, b  , c])  (a  𝖺-1[b, , c]) 
                       𝖺[a, b,   c]  𝖺[a  b, , c]"
        using assms assoc'_naturality [of a "𝗋[b]" c] comp_assoc by force
      also have "... = ((a  𝗋[b])  c)  𝖺-1[a, b  , c]  (a  𝖺-1[b, , c]) 
                       𝖺[a, b,   c]  𝖺[a  b, , c]"
        using comp_assoc by simp
      also have "... = ((a  𝗋[b])  c)  (𝖺[a, b, ]  c)"
        using assms pentagon invert_side_of_triangle(1)
              invert_side_of_triangle(1)
                [of "𝖺[a, b,   c]  𝖺[a  b, , c]" "a  𝖺[b, , c]"
                    "𝖺[a, b  , c]  (𝖺[a, b, ]  c)"]
        by force
      finally show ?thesis by blast
    qed

    lemma runit_tensor:
    assumes "ide a" and "ide b"
    shows "𝗋[a  b] = (a  𝗋[b])  𝖺[a, b, ]"
    proof -
      have "((a  𝗋[b])  𝖺[a, b, ])   = 𝗋[a  b]  "
        using assms interchange [of  ] runit_tensor_gen by simp
      moreover have "par ((a  𝗋[b])  𝖺[a, b, ]) 𝗋[a  b]"
        using assms by simp
      ultimately show ?thesis
        using assms R.is_faithful [of "(a  𝗋[b])  (𝖺[a, b, ])" "𝗋[a  b]"]
        by fastforce
    qed

    lemma runit_tensor':
    assumes "ide a" and "ide b"
    shows "𝗋[a  b]  𝖺-1[a, b, ] = a  𝗋[b]"
      using assms runit_tensor invert_side_of_triangle by force

    text ‹
      Sometimes inverted forms of the triangle and pentagon axioms are useful.
›

    lemma triangle':
    assumes "ide a" and "ide b"
    shows "(a  𝗅[b]) = (𝗋[a]  b)  𝖺-1[a, , b]"
    proof -
      have "(𝗋[a]  b)  𝖺-1[a, , b] = ((a  𝗅[b])  𝖺[a, , b])  𝖺-1[a, , b]"
          using assms triangle by auto
      also have "... = (a  𝗅[b])"
        using assms comp_arr_dom comp_assoc by auto
      finally show ?thesis by auto
    qed

    lemma pentagon':
    assumes "ide a" and "ide b" and "ide c" and "ide d"
    shows "((𝖺-1[a, b, c]  d)  𝖺-1[a, b  c, d])  (a  𝖺-1[b, c, d])
              = 𝖺-1[a  b, c, d]  𝖺-1[a, b, c  d]"
    proof -
      have "((𝖺-1[a, b, c]  d)  𝖺-1[a, b  c, d])  (a  𝖺-1[b, c, d])
              = inv ((a  𝖺[b, c, d])  (𝖺[a, b  c, d]  (𝖺[a, b, c]  d)))"
        using assms isos_compose inv_comp by simp
      also have "... = inv (𝖺[a, b, c  d]  𝖺[a  b, c, d])"
        using assms pentagon by auto
      also have "... = 𝖺-1[a  b, c, d]  𝖺-1[a, b, c  d]"
        using assms inv_comp by simp
      finally show ?thesis by auto
    qed

    text‹
      The following non-obvious fact is Corollary 2.2.5 from cite"Etingof15".
      The statement that @{term "𝗅[] = 𝗋[]"} is Theorem 6 from cite"Kelly64".
      MacLane cite"MacLane71" does not show this, but assumes it as an axiom.
›

    lemma unitor_coincidence:
    shows "𝗅[] = ι" and "𝗋[] = ι"
    proof -
      have "𝗅[]   = (  𝗅[])  𝖺[, , ]"
        using lunit_tensor' [of  ] lunit_commutes_with_L [of ] by simp
      moreover have "𝗋[]   = (  𝗅[])  𝖺[, , ]"
        using triangle [of  ] by simp
      moreover have "ι   = (  𝗅[])  𝖺[, , ]"
        using lunit_char comp_arr_dom unit_in_hom comp_assoc by auto
      ultimately have "𝗅[]   = ι    𝗋[]   = ι  "
        by argo
      moreover have "par 𝗅[] ι  par 𝗋[] ι"
        using unit_in_hom by force
      ultimately have 1: "𝗅[] = ι  𝗋[] = ι"
        using R.is_faithful by metis
      show "𝗅[] = ι" using 1 by auto
      show "𝗋[] = ι" using 1 by auto
    qed

    lemma unit_triangle:
    shows "ι   = (  ι)  𝖺[, , ]"
    and "(ι  )  𝖺-1[, , ] =   ι"
      using triangle [of  ] triangle' [of  ] unitor_coincidence by auto

    text‹
      The only isomorphism that commutes with @{term ι} is @{term }.
›

    lemma iso_commuting_with_unit_equals_unity:
    assumes "«f :   »" and "iso f" and "f  ι = ι  (f  f)"
    shows "f = "
    proof -
      have "  f =   "
      proof -
        have "f  f = f  "
          by (metis assms(1,3) iso_cancel_left runit_naturality seqE seqI' unit_in_hom_ax
              unit_is_iso unitor_coincidence(2))
        thus ?thesis
          by (metis assms(1-2) R.preserves_comp comp_cod_arr comp_inv_arr' ideD(1) ide_unity
              in_homE interchange)
      qed
      moreover have "par f "
        using assms by auto
      ultimately show "f = "
        using L.is_faithful by metis
    qed

  end

  text‹
    We now show that the unit ι› of a monoidal category is unique up to a unique
    isomorphism (Proposition 2.2.6 of cite"Etingof15").
›

  locale monoidal_category_with_alternate_unit =
    monoidal_category C T α ι +
    C1: monoidal_category C T α ι1
  for C :: "'a comp"      (infixr  55)
  and T :: "'a * 'a  'a"
  and α :: "'a * 'a * 'a  'a"
  and ι :: 'a
  and ι1 :: 'a
  begin

    no_notation C1.tensor (infixr  53)
    no_notation C1.unity  ()
    no_notation C1.lunit  (𝗅[_])
    no_notation C1.runit  (𝗋[_])
    no_notation C1.assoc  (𝖺[_, _, _])
    no_notation C1.assoc' (𝖺-1[_, _, _])

    notation C1.tensor    (infixr 1 53)
    notation C1.unity     (1)
    notation C1.lunit     (𝗅1[_])
    notation C1.runit     (𝗋1[_])
    notation C1.assoc     (𝖺1[_, _, _])
    notation C1.assoc'    (𝖺1-1[_, _, _])

    definition i
    where "i  𝗅[1]  inv 𝗋1[]"

    lemma iso_i:
    shows "«i :   1»" and "iso i"
    proof -
      show "«i :   1»"
        using C1.iso_runit inv_in_hom i_def by auto
      show "iso i"
        using iso_lunit C1.iso_runit isos_compose i_def by simp
    qed

    text‹
      The following is Exercise 2.2.7 of cite"Etingof15".
›

    lemma i_maps_ι_to_ι1:
    shows "i  ι = ι1  (i  i)"
    proof -
      have 1: "inv 𝗋1[]  ι = (𝗋1[]  𝗅[1])  (inv 𝗋1[]  inv 𝗋1[])"
      proof -
        have "ι  (𝗋1[]  𝗋1[]) = 𝗋1[]  (𝗋1[]  𝗅[1])"
        proof -
          text ‹
$$\xymatrix{
  && {@{term[source=true] "(  1)    1"}}
     \ar[dddll]_{\scriptsize @{term[source=true] "𝗋1[]  𝗋1[]"}}
     \ar[dd]^{\scriptsize @{term[source=true] "𝗋1[]    1"}}
     \ar[dddrr]^{\scriptsize @{term[source=true] "𝗋1[]  𝗅[1]"}}
  \\
  \\
  && {@{term[source=true] "    1"}}
     \ar[dll]^{\scriptsize @{term[source=true] "  𝗋1[]"}}
     \ar[drr]_{\scriptsize @{term[source=true] "  𝗅[1]"}}
     \ar[dd]^{\scriptsize @{term[source=true] "𝖺-1[, , 1]"}}
  \\
  {@{term[source=true] "  "}}
     \ar[dddrr]_{\scriptsize @{term[source=true] "ι"}}
  &&
  &&
  {@{term[source=true] "  1"}}
     \ar[dddll]^{\scriptsize @{term[source=true] "𝗋1[]"}}
  \\
  && {@{ term[source=true] "(  )  1"}}
     \ar[ull]_{\scriptsize @{term[source=true] "𝗋1[  ]"}}
     \ar[urr]^{\scriptsize @{term[source=true] "ι  "}}
  \\
  \\
  && {@{term[source=true] ""}}
}$$
›
          have "ι  (𝗋1[]  𝗋1[]) = ι  (  𝗋1[])  (𝗋1[]    1)"
            using interchange comp_cod_arr comp_arr_dom by simp
          also have "... = ι  (𝗋1[  ]  𝖺-1[, , 1])  (𝗋1[]    1)"
            using C1.runit_tensor' by auto
          also have "... = (ι  𝗋1[  ])  𝖺-1[, , 1]  (𝗋1[]    1)"
            using comp_assoc by auto
          also have "... = (𝗋1[]  (ι  1))  𝖺-1[, , 1]  (𝗋1[]    1)"
            using C1.runit_naturality [of ι] unit_in_hom by fastforce
          also have "... = 𝗋1[]  ((ι  1)  𝖺-1[, , 1])  (𝗋1[]    1)"
            using comp_assoc by auto
          also have "... = 𝗋1[]  (  𝗅[1])  (𝗋1[]    1)"
            using lunit_tensor lunit_commutes_with_L unitor_coincidence by simp
          also have "... = 𝗋1[]  (𝗋1[]  𝗅[1])"
            using interchange comp_arr_dom comp_cod_arr by simp
          finally show ?thesis by blast
        qed
        moreover have "seq ι (𝗋1[]  𝗋1[])  seq 𝗋1[] (𝗋1[]  𝗅[1])"
          using unit_in_hom by fastforce
        moreover have "iso 𝗋1[]  iso (𝗋1[]  𝗋1[])"
          using C1.iso_runit tensor_preserves_iso by force
        ultimately show ?thesis
          using invert_opposite_sides_of_square inv_tensor by metis
      qed
      have 2: "𝗅[1]  (𝗋1[]  𝗅[1]) = ι1  (𝗅[1]  𝗅[1])"
      proof -
        text ‹
$$\xymatrix{
  && {@{term[source=true] "(  1)  (  1)"}}
     \ar[dddll]_{\scriptsize @{term[source=true] "𝗅[1]  𝗅[1]"}}
     \ar[dd]^{\scriptsize @{term[source=true] "(  1)  𝗅[1]"}}
     \ar[dddrr]^{\scriptsize @{term[source=true] "𝗋1[]  𝗅[1]"}}
  \\
  \\
  && {@{term[source=true] "(  1)  1"}}
     \ar[dll]^{\scriptsize @{term[source=true] "𝗅[1]  1"}}
     \ar[drr]_{\scriptsize @{term[source=true] "𝗋1[]  1"}}
     \ar[dd]^{\scriptsize @{term[source=true] "𝖺[, 1, 1]"}}
  \\
  {@{term[source=true] "1  1"}}
     \ar[dddrr]_{\scriptsize @{term[source=true] "ι1"}}
  &&
  &&
  {@{term[source=true] "  1"}}
     \ar[dddll]^{\scriptsize @{term[source=true] "𝗅[1]"}}
  \\
  && {@{term[source=true] "  1  1"}}
     \ar[ull]_{\scriptsize @{term[source=true] "𝗅[1  1]"}}
     \ar[urr]^{\scriptsize @{term[source=true] "  ι1"}}
  \\
  \\
  && {@{term[source=true] "1"}}
}$$
›
        have "𝗅[1]  (𝗋1[]  𝗅[1]) = 𝗅[1]  (𝗋1[]  1)  ((  1)  𝗅[1])"
          using interchange comp_arr_dom comp_cod_arr by force
        also have "... = 𝗅[1]  ((  ι1)  𝖺[, 1, 1])  ((  1)  𝗅[1])"
          using C1.runit_tensor C1.unitor_coincidence C1.runit_commutes_with_R by simp
        also have "... = (𝗅[1]  (  ι1))  𝖺[, 1, 1]  ((  1)  𝗅[1])"
          using comp_assoc by fastforce
        also have "... = (ι1  𝗅[1  1])  𝖺[, 1, 1]  ((  1)  𝗅[1])"
          using lunit_naturality [of ι1] C1.unit_in_hom lunit_commutes_with_L by fastforce
        also have "... = ι1  (𝗅[1  1]  𝖺[, 1, 1])  ((  1)  𝗅[1])"
          using comp_assoc by force
        also have "... = ι1  (𝗅[1]  1)  ((  1)  𝗅[1])"
          using lunit_tensor' by auto
        also have "... = ι1  (𝗅[1]  𝗅[1])"
          using interchange comp_arr_dom comp_cod_arr by simp
        finally show ?thesis by blast
      qed
      show ?thesis
      proof -
        text ‹
$$\xymatrix{
  {@{term[source=true] "1  1"}}
     \ar[dd]_{\scriptsize @{term "ι1"}}
  &&
  {@{term[source=true] "(  1)  (  1)"}}
     \ar[ll]_{\scriptsize @{term[source=true] "𝗅[1]  𝗅[1]"}}
     \ar[dd]^{\scriptsize @{term[source=true] "𝗋1[]  𝗅[1]"}}
     \ar[rr]^{\scriptsize @{term[source=true] "𝗋1[]  𝗋1[]"}}
  &&
  {@{term[source=true] "1  1"}}
     \ar[dd]^{\scriptsize @{term[source=true] "ι"}}
  \\
  \\
  {@{term[source=true] "1"}}
  &&
  {@{term[source=true] "  1"}}
     \ar[ll]_{\scriptsize @{term[source=true] "𝗅[1]"}}
     \ar[rr]^{\scriptsize @{term[source=true] "𝗋1[]"}}
  &&
  {@{term[source=true] ""}}
}$$
›
        have "i  ι = 𝗅[1]  inv 𝗋1[]  ι"
          using i_def comp_assoc by auto
        also have "... = (𝗅[1]  (𝗋1[]  𝗅[1]))  (inv 𝗋1[]  inv 𝗋1[])"
          using 1 comp_assoc by simp
        also have "... = ι1  (𝗅[1]  𝗅[1])  (inv 𝗋1[]  inv 𝗋1[])"
          using 2 comp_assoc by fastforce
        also have "... = ι1  (i  i)"
          using interchange i_def by simp
        finally show ?thesis by blast
      qed
    qed

    lemma inv_i_iso_ι:
    assumes "«f :   1»" and "iso f" and "f  ι = ι1  (f  f)"
    shows "«inv i  f :   »" and "iso (inv i  f)"
    and "(inv i  f)  ι = ι  (inv i  f  inv i  f)"
    proof -
      show 1: "«inv i  f :   »"
        using assms iso_i inv_in_hom by blast
      show "iso (inv i  f)"
        using assms 1 iso_i inv_in_hom
        by (intro isos_compose, auto)
      show "(inv i  f)  ι = ι  (inv i  f  inv i  f)"
      proof -
        have "(inv i  f)  ι = (inv i  ι1)  (f  f)"
          using assms iso_i comp_assoc by auto
        also have "... = (ι  (inv i  inv i))  (f  f)"
          by (metis unit_in_hom_ax i_maps_ι_to_ι1 invert_opposite_sides_of_square iso_i
              inv_tensor tensor_preserves_iso seqI')
        also have "... = ι  (inv i  f  inv i  f)"
          using assms 1 iso_i interchange comp_assoc by fastforce
        finally show ?thesis by blast
      qed
    qed

    lemma unit_unique_upto_unique_iso:
    shows "∃!f. «f :   1»  iso f  f  ι = ι1  (f  f)"
    proof
      show "«i :   1»  iso i  i  ι = ι1  (i  i)"
        using iso_i i_maps_ι_to_ι1 by auto
      show "f. «f :   1»  iso f  f  ι = ι1  (f  f)  f = i"
      proof -
        fix f
        assume f: "«f :   1»  iso f  f  ι = ι1  (f  f)"
        have "inv i  f = "
          using f inv_i_iso_ι iso_commuting_with_unit_equals_unity by blast
        hence "ide (C (inv i) f)"
          using iso_i by simp
        thus "f = i"
          using section_retraction_of_iso(2) [of "inv i" f] inverse_arrow_unique inv_is_inverse
                iso_i
          by blast
      qed
    qed

  end

  section "Elementary Monoidal Category"

  text‹
    Although the economy of data assumed by @{locale monoidal_category} is useful for general
    results, to establish interpretations it is more convenient to work with a traditional
    definition of monoidal category.  The following locale provides such a definition.
    It permits a monoidal category to be specified by giving the tensor product and the
    components of the associator and unitors, which are required only to satisfy elementary
    conditions that imply functoriality and naturality, without having to worry about
    extensionality or formal interpretations for the various functors and natural transformations.
›

  locale elementary_monoidal_category =
    category C
  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"  (𝖺[_, _, _]) +
  assumes ide_unity [simp]: "ide "
  and iso_lunit: "ide a  iso 𝗅[a]"
  and iso_runit: "ide a  iso 𝗋[a]"
  and iso_assoc: " ide a; ide b; ide c   iso 𝖺[a, b, c]"
  and tensor_in_hom [simp]: " «f : a  b»; «g : c  d»   «f  g : a  c  b  d»"
  and tensor_preserves_ide: " ide a; ide b   ide (a  b)"
  and interchange: " seq g f; seq g' f'   (g  g')  (f  f') = g  f  g'  f'"
  and lunit_in_hom [simp]: "ide a  «𝗅[a] :   a  a»"
  and lunit_naturality: "arr f  𝗅[cod f]  (  f) = f  𝗅[dom f]"
  and runit_in_hom [simp]: "ide a  «𝗋[a] : a    a»"
  and runit_naturality: "arr f  𝗋[cod f]  (f  ) = f  𝗋[dom f]"
  and assoc_in_hom [simp]:
      " ide a; ide b; ide c   «𝖺[a, b, c] : (a  b)  c  a  b  c»"
  and assoc_naturality:
      " arr f0; arr f1; arr f2   𝖺[cod f0, cod f1, cod f2]  ((f0  f1)  f2)
                                        = (f0  (f1  f2))  𝖺[dom f0, dom f1, dom f2]"
  and triangle: " ide a; ide b   (a  𝗅[b])  𝖺[a, , b] = 𝗋[a]  b"
  and pentagon: " ide a; ide b; ide c; ide d  
                   (a  𝖺[b, c, d])  𝖺[a, b  c, d]  (𝖺[a, b, c]  d)
                     = 𝖺[a, b, c  d]  𝖺[a  b, c, d]"

  text‹
    An interpretation for the monoidal_category› locale readily induces an
    interpretation for the elementary_monoidal_category› locale.
›
      
  context monoidal_category
  begin

    lemma induces_elementary_monoidal_category:
      shows "elementary_monoidal_category C tensor  lunit runit assoc"
        using iso_assoc tensor_preserves_ide assoc_in_hom tensor_in_hom
              assoc_naturality lunit_naturality runit_naturality lunit_in_hom runit_in_hom
              iso_lunit iso_runit interchange pentagon triangle
        by unfold_locales auto

  end

  context elementary_monoidal_category
  begin

    interpretation CC: product_category C C ..
    interpretation CCC: product_category C CC.comp ..

    definition T :: "'a * 'a  'a"
    where "T f  if CC.arr f then (fst f  snd f) else null"

    lemma T_simp [simp]:
    assumes "arr f" and "arr g"
    shows "T (f, g) = f  g"
      using assms T_def by simp

    lemma arr_tensor [simp]:
    assumes "arr f" and "arr g"
    shows "arr (f  g)"
      using assms tensor_in_hom by blast

    lemma dom_tensor [simp]:
    assumes "arr f" and "arr g"
    shows "dom (f  g) = dom f  dom g"
      using assms tensor_in_hom by blast

    lemma cod_tensor [simp]:
    assumes "arr f" and "arr g"
    shows "cod (f  g) = cod f  cod g"
      using assms tensor_in_hom by blast

    interpretation T: binary_endofunctor C T
      using interchange T_def
      apply unfold_locales
          apply auto[4]
      by (elim CC.seqE, auto)

    lemma binary_endofunctor_T:
    shows "binary_endofunctor C T" ..

    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

    definition α
    where "α f  if CCC.arr f
                  then (fst f  (fst (snd f)  snd (snd f))) 
                          𝖺[dom (fst f), dom (fst (snd f)), dom (snd (snd f))]
                  else null"

    lemma α_ide_simp [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "α (a, b, c) = 𝖺[a, b, c]"
      unfolding α_def using assms assoc_in_hom comp_cod_arr
      by (metis CC.arrIPC CCC.arrIPC fst_conv ide_char in_homE snd_conv)

    lemma arr_assoc [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "arr 𝖺[a, b, c]"
      using assms assoc_in_hom by blast

    lemma dom_assoc [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "dom 𝖺[a, b, c] = (a  b)  c"
      using assms assoc_in_hom by blast

    lemma cod_assoc [simp]:
    assumes "ide a" and "ide b" and "ide c"
    shows "cod 𝖺[a, b, c] = a  b  c"
      using assms assoc_in_hom by blast
      
    interpretation α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α
    proof -
      interpret α: transformation_by_components CCC.comp C T.ToTC T.ToCT α
        apply unfold_locales
        unfolding α_def T.ToTC_def T.ToCT_def T_def
        using comp_arr_dom comp_cod_arr assoc_naturality
        by simp_all
      interpret α: natural_isomorphism CCC.comp C T.ToTC T.ToCT α.map
        using iso_assoc α.map_simp_ide assoc_in_hom tensor_preserves_ide α_def
        by (unfold_locales, auto)
      have "α = α.map"
        using assoc_naturality α_def comp_cod_arr T.ToTC_def T_def α.map_def by auto
      thus "natural_isomorphism CCC.comp C T.ToTC T.ToCT α"
        using α.natural_isomorphism_axioms by simp
    qed

    interpretation α': inverse_transformation CCC.comp C T.ToTC T.ToCT α ..

    interpretation L: "functor" C C λf. T (, f)
      using T.fixing_ide_gives_functor_1 by auto

    interpretation R: "functor" C C λf. T (f, )
      using T.fixing_ide_gives_functor_2 by auto

    interpretation 𝔩: natural_isomorphism C C λf. T (, f) map
                        λf. if arr f then f  𝗅[dom f] else null
    proof -
      interpret 𝔩: transformation_by_components C C λf. T (, f) map λa. 𝗅[a]
        using lunit_naturality by (unfold_locales, auto)
      interpret 𝔩: natural_isomorphism C C λf. T (, f) map 𝔩.map
        using iso_lunit by (unfold_locales, simp)
      have "𝔩.map = (λf. if arr f then f  𝗅[dom f] else null)"
        using 𝔩.map_def lunit_naturality by fastforce
      thus "natural_isomorphism C C (λf. T (, f)) map (λf. if arr f then f  𝗅[dom f] else null)"
        using 𝔩.natural_isomorphism_axioms by force
    qed

    interpretation ρ: natural_isomorphism C C λf. T (f, ) map
                        λf. if arr f then f  𝗋[dom f] else null
    proof -
      interpret ρ: transformation_by_components C C λf. T (f, ) map λa. 𝗋[a]
        using runit_naturality by (unfold_locales, auto)
      interpret ρ: natural_isomorphism C C λf. T (f, ) map ρ.map
        using iso_runit ρ.map_simp_ide by (unfold_locales, simp)
      have "(λf. if arr f then f  𝗋[dom f] else null) = ρ.map"
        using ρ.map_def runit_naturality T_simp by fastforce
      thus "natural_isomorphism C C (λf. T (f, )) map (λf. if arr f then f  𝗋[dom f] else null)"
        using ρ.natural_isomorphism_axioms by force
    qed

    text‹
      The endofunctors λf. T (ℐ, f)› and λf. T (f, ℐ)› are equivalence functors,
      due to the existence of the unitors.
›

    interpretation L: equivalence_functor C C λf. T (, f)
    proof -
      interpret endofunctor C λf. T (, f) ..
      show "equivalence_functor C C (λf. T (, f))"
        using isomorphic_to_identity_is_equivalence 𝔩.natural_isomorphism_axioms by simp
    qed

    interpretation R: equivalence_functor C C λf. T (f, )
    proof -
      interpret endofunctor C λf. T (f, ) ..
      show "equivalence_functor C C (λf. T (f, ))"
        using isomorphic_to_identity_is_equivalence ρ.natural_isomorphism_axioms by simp
    qed

    text‹
      To complete an interpretation of the @{locale "monoidal_category"} locale,
      we define @{term "ι  𝗅[]"}.
      We could also have chosen @{term "ι  ρ[]"} as the two are equal, though to prove
      that requires some work yet.
›

    definition ι
    where "ι  𝗅[]"

    lemma ι_in_hom:
    shows "«ι :     »"
      using lunit_in_hom ι_def by simp

    lemma induces_monoidal_category:
    shows "monoidal_category C T α ι"
    proof -
      have 1: "«ι :     »"
        using lunit_in_hom ι_def by simp
      interpret L: equivalence_functor C C λf. T (cod ι, f)
      proof -
        have "(λf. T (, f)) = (λf. T (cod ι, f))" using 1 by fastforce
        thus "equivalence_functor C C (λf. T (cod ι, f))"
          using L.equivalence_functor_axioms T_def by simp
      qed
      interpret R: equivalence_functor C C λf. T (f, cod ι)
      proof -
        have "(λf. T (f, )) = (λf. T (f, cod ι))" using 1 by fastforce
        thus "equivalence_functor C C (λf. T (f, cod ι))"
          using R.equivalence_functor_axioms T_def by simp
      qed
      show ?thesis
      proof
        show "«ι : T (cod ι, cod ι)  cod ι»" using 1 by fastforce
        show "iso ι" using iso_lunit ι_def by simp
        show "a b c d.  ide a; ide b; ide c; ide d  
                        T (a, α (b, c, d))  α (a, T (b, c), d)  T (α (a, b, c), d)
                          = α (a, b, T (c, d))  α (T (a, b), c, d)"
          using pentagon tensor_preserves_ide by simp
      qed
    qed

    interpretation MC: monoidal_category C T α ι
      using induces_monoidal_category by auto

    text‹
      We now show that the notions defined in the interpretation MC› agree with their
      counterparts in the present locale.  These facts are needed if we define an
      interpretation for the @{locale elementary_monoidal_category} locale, use it to
      obtain the induced interpretation for @{locale monoidal_category}, and then want to
      transfer facts obtained in the induced interpretation back to the original one.
›

    lemma ℐ_agreement:
    shows "MC.unity = "
      by (metis ι_def ide_unity in_homE lunit_in_hom)

    lemma L_agreement:
    shows "MC.L = (λf. T (, f))"
      using ι_in_hom by auto

    lemma R_agreement:
    shows "MC.R = (λf. T (f, ))"
      using ι_in_hom by auto

    text‹
      We wish to show that the components of the unitors @{term MC.𝔩} and @{term MC.ρ}
      defined in the induced interpretation MC› agree with those given by the
      parameters @{term lunit} and @{term runit} to the present locale.  To avoid a lengthy
      development that repeats work already done in the @{locale monoidal_category} locale,
      we establish the agreement in a special case and then use the properties already
      shown for MC› to prove the general case.  In particular, we first show that
      @{term "𝗅[] = MC.lunit MC.unity"} and @{term "𝗋[] = MC.runit MC.unity"},
      from which it follows by facts already proved for @{term MC} that both are equal to @{term ι}.
      We then show that for an arbitrary identity @{term a} the arrows @{term "𝗅[a]"}
      and @{term "𝗋[a]"} satisfy the equations that uniquely characterize the components
      @{term "MC.lunit a"} and @{term "MC.runit a"}, respectively, and are therefore equal
      to those components.
›
      
    lemma unitor_coincidence:
    shows "𝗅[] = ι" and "𝗋[] = ι"
    proof -
      have "𝗋[] = MC.runit MC.unity"
        by (metis (no_types, lifting) MC.arr_runit MC.runit_eqI MC.unitor_coincidence(2)
            T_simp ℐ_agreement ι_def α_ide_simp ideD(1) ide_unity iso_is_arr iso_runit
            runit_in_hom triangle)
      moreover have "𝗅[] = MC.lunit MC.unity"
        using MC.unitor_coincidence(1) ι_def by force
      ultimately have 1: "𝗅[] = ι  𝗋[] = ι"
        using MC.unitor_coincidence by simp
      show "𝗅[] = ι" using 1 by simp
      show "𝗋[] = ι" using 1 by simp
    qed

    lemma lunit_char:
    assumes "ide a"
    shows "  𝗅[a] = (ι  a)  inv 𝖺[, , a]"
      by (metis MC.iso_assoc α_ide_simp ι_in_hom arrI arr_tensor assms ideD(1)
          ide_unity invert_side_of_triangle(2) triangle unitor_coincidence(2))
    
    lemma runit_char:
    assumes "ide a"
    shows "𝗋[a]   = (a  ι)  𝖺[a, , ]"
      using assms triangle ι_def by simp

    lemma 𝔩_agreement:
    shows "MC.𝔩 = (λf. if arr f then f  𝗅[dom f] else null)"
    proof
      fix f
      have "¬ arr f  MC.𝔩 f = null" by simp 
      moreover have "arr f  MC.𝔩 f = f  𝗅[dom f]"
      proof -
        have "a. ide a  𝗅[a] = MC.lunit a"
          using ℐ_agreement T_def lunit_char ι_in_hom iso_lunit
          apply (intro MC.lunit_eqI)
           apply auto
          by blast
        thus ?thesis
          by (metis ide_dom ext seqE)
      qed
      ultimately show "MC.𝔩 f = (if arr f then f  𝗅[dom f] else null)" by simp
    qed

    lemma ρ_agreement:
    shows "MC.ρ = (λf. if arr f then f  𝗋[dom f] else null)"
    proof
      fix f
      have "¬ arr f  MC.ρ f = null" by simp
      moreover have "arr f  MC.ρ f = f  𝗋[dom f]"
      proof -
        have "a. ide a  𝗋[a] = MC.runit a"
          using ℐ_agreement T_def runit_char ι_in_hom iso_runit
          apply (intro MC.runit_eqI)
           apply auto
          by blast
        thus ?thesis
          by (metis ide_dom local.ext seqE)
      qed
      ultimately show "MC.ρ f = (if arr f then f  𝗋[dom f] else null)" by simp
    qed

    lemma lunit_agreement:
    assumes "ide a"
    shows "MC.lunit a = 𝗅[a]"
      using assms comp_cod_arr 𝔩_agreement
      by (metis (no_types, lifting) MC.𝔩_ide_simp ide_char in_homE lunit_in_hom)

    lemma runit_agreement:
    assumes "ide a"
    shows "MC.runit a = 𝗋[a]"
      using assms comp_cod_arr ρ_agreement
      by (metis (no_types, lifting) MC.ρ_ide_simp ide_char in_homE runit_in_hom)

  end

  (*
   * TODO: The locale parameters lunit, runit, etc. of elementary_monoidal_category
   * shadow the same-named constants defined in the parent locale monoidal category
   * after the following sublocale declaration.  The constants in the parent locale
   * can be accessed by using the qualifier "local", but there seems also to be
   * some kind of shadowing effect on facts.
   *)
(*
  sublocale elementary_monoidal_category ⊆ monoidal_category C T α ι
    using induces_monoidal_category by blast
 *)

  section "Strict Monoidal Category"

  text‹
    A monoidal category is \emph{strict} if the components of the associator and unitors
    are all identities.
›
      
  locale strict_monoidal_category =
    monoidal_category +
  assumes strict_assoc: " ide a0; ide a1; ide a2   ide 𝖺[a0, a1, a2]"
  and strict_lunit: "ide a  𝗅[a] = a"
  and strict_runit: "ide a  𝗋[a] = a"
  begin

    lemma strict_unit:
    shows "ι = "
      using strict_lunit unitor_coincidence(1) by auto

    lemma tensor_assoc [simp]:
    assumes "arr f0" and "arr f1" and "arr f2"
    shows "(f0  f1)  f2 = f0  f1  f2"
      by (metis CC.arrIPC CCC.arrIPC α'.preserves_reflects_arr α'_simp assms(1-3)
          assoc'_naturality ide_cod ide_dom inv_ide comp_arr_ide comp_ide_arr strict_assoc)

  end

  section "Opposite Monoidal Category"

  text‹
    The \emph{opposite} of a monoidal category has the same underlying category, but the
    arguments to the tensor product are reversed and the associator is inverted and its
    arguments reversed.
›
      
  locale opposite_monoidal_category =
    C: monoidal_category C TC αC ι
  for C :: "'a comp"      (infixr  55)
  and TC :: "'a * 'a  'a"
  and αC :: "'a * 'a * 'a  'a"
  and ι :: 'a
  begin

    abbreviation T
    where "T f  TC (snd f, fst f)"

    abbreviation α
    where "α f  C.α' (snd (snd f), fst (snd f), fst f)"

  end

  sublocale opposite_monoidal_category  monoidal_category C T α ι
  proof -
    interpret T: binary_endofunctor C T
      using C.T.is_extensional C.CC.seq_char C.interchange by (unfold_locales, auto)
    interpret ToTC: "functor" C.CCC.comp C T.ToTC
      using T.functor_ToTC by auto
    interpret ToCT: "functor" C.CCC.comp C T.ToCT
      using T.functor_ToCT by auto
    interpret α: natural_transformation C.CCC.comp C T.ToTC T.ToCT α
      using C.α'.is_extensional C.CCC.dom_char C.CCC.cod_char T.ToTC_def T.ToCT_def
            C.α'_simp C.α'.naturality
      by (unfold_locales) auto
    interpret α: natural_isomorphism C.CCC.comp C T.ToTC T.ToCT α
      using C.α'.components_are_iso by (unfold_locales, simp)
    interpret L: equivalence_functor C C λf. T (C.cod ι, f)
      using C.R.equivalence_functor_axioms by simp
    interpret R: equivalence_functor C C λf. T (f, C.cod ι)
      using C.L.equivalence_functor_axioms by simp
    show "monoidal_category C T α ι"
      using C.unit_is_iso C.pentagon' C.comp_assoc
      by (unfold_locales) auto
  qed

  context opposite_monoidal_category
  begin

    lemma lunit_simp:
    assumes "C.ide a"
    shows "lunit a = C.runit a"
      using assms lunit_char C.iso_assoc by (intro C.runit_eqI, auto)

    lemma runit_simp:
    assumes "C.ide a"
    shows "runit a = C.lunit a"
      using assms runit_char C.iso_assoc by (intro C.lunit_eqI, auto)

  end

  section "Dual Monoidal Category"

  text‹
    The \emph{dual} of a monoidal category is obtained by reversing the arrows of the
    underlying category.  The tensor product remains the same, but the associators and
    unitors are inverted.
›

  locale dual_monoidal_category =
    M: monoidal_category
  begin

    sublocale dual_category C ..
    sublocale MM: product_category comp comp ..
    interpretation T: binary_functor comp comp comp T
      using M.T.is_extensional M.interchange MM.comp_char
      by unfold_locales auto
    interpretation T: binary_endofunctor comp ..
    interpretation ToTC: "functor" T.CCC.comp comp T.ToTC
      using T.functor_ToTC by blast
    interpretation ToCT: "functor" T.CCC.comp comp T.ToCT
      using T.functor_ToCT by blast
    interpretation α: natural_transformation T.CCC.comp comp T.ToTC T.ToCT M.α'
      using M.α'.is_extensional M.α'.is_natural_1 M.α'.is_natural_2
      by unfold_locales auto
    interpretation α: natural_isomorphism T.CCC.comp comp T.ToTC T.ToCT M.α'
      by unfold_locales auto
    interpretation L: equivalence_functor comp comp M.tensor (cod (M.inv ι))
    proof -
      interpret L: dual_equivalence_functor C C M.tensor  ..
      show "equivalence_functor comp comp (M.tensor (cod (M.inv ι)))"
        using L.equivalence_functor_axioms
        by (simp add: M.unit_is_iso)
    qed
    interpretation R: equivalence_functor comp comp λf. M.tensor f (cod (M.inv ι))
    proof -
      interpret R: dual_equivalence_functor C C λf. M.tensor f  ..
      show "equivalence_functor comp comp (λf. M.tensor f (cod (M.inv ι)))"
        using R.equivalence_functor_axioms
        by (simp add: M.unit_is_iso)
    qed

    sublocale monoidal_category comp T M.α' M.inv ι
      using T.is_extensional M.unit_in_hom M.inv_in_hom M.unit_is_iso M.pentagon'
            equivalence_functor_def category_axioms
      by unfold_locales auto

    lemma is_monoidal_category:
    shows "monoidal_category comp T M.α' (M.inv ι)"
      ..

    no_notation comp  (infixr  55)

    lemma assoc_char:
    assumes "ide a" and "ide b" and "ide c"
    shows "assoc a b c = M.assoc' a b c" and "assoc' a b c = M.assoc a b c"
      using assms M.inv_inv M.iso_inv_iso
      apply force
      by (metis assms M.α'_ide_simp M.comp_assoc_assoc'(2) M.ideD(1) M.iso_assoc
          M.iso_cancel_left M.iso_inv_iso comp_assoc_assoc'(2) ide_char comp_def
          tensor_preserves_ide)

    lemma lunit_char:
    assumes "ide a"
    shows "lunit a = M.lunit' a"
    proof -
      have "M.lunit' a = lunit a"
      proof (intro lunit_eqI)
        show "in_hom (M.lunit' a) (tensor unity a) a"
          using assms
          by (simp add: M.lunit'_in_hom M.unit_is_iso)
        show "tensor unity (M.lunit' a) = comp (tensor (M.inv ι) a) (assoc' unity unity a)"
        proof -
          have "M.inv (tensor  (M.lunit a)  M.assoc   a) = M.inv (tensor ι a)"
            using assms M.triangle M.unitor_coincidence by auto
          hence "M.assoc'   a  tensor  (M.lunit' a) = tensor (M.inv ι) a"
            using assms M.inv_comp M.unit_is_iso by fastforce
          thus ?thesis
            using assms M.unit_is_iso assoc_char
                  M.invert_side_of_triangle(1)
                    [of "tensor (M.inv ι) a" "M.assoc' unity unity a" "tensor  𝗅-1[a]"]
            by auto
        qed
      qed
      thus ?thesis by simp
    qed

    lemma runit_char:
    assumes "ide a"
    shows "runit a = M.runit' a"
    proof -
      have "M.runit' a = runit a"
      proof (intro runit_eqI)
        show "in_hom (M.runit' a) (tensor a unity) a"
          using assms
          by (simp add: M.runit'_in_hom M.unit_is_iso)
        show "tensor (M.runit' a) unity = comp (tensor a (M.inv ι)) (assoc a unity unity)"
        proof -
          have "M.inv (tensor a ι  M.assoc a  ) = M.inv (tensor (M.runit a) )"
            using assms M.triangle [of a ] M.unitor_coincidence by auto
          hence "M.assoc' a    tensor a (M.inv ι) = tensor (M.runit' a) "
            using assms M.inv_comp M.unit_in_hom M.unit_is_iso by auto
          thus ?thesis
            using assms M.unit_is_iso assoc_char by auto
        qed
      qed
      thus ?thesis by simp
    qed

  end

  section "Monoidal Language"

  text‹
    In this section we assume that a category @{term C} is given, and we define a
    formal syntax of terms constructed from arrows of @{term C} using function symbols
    that correspond to unity, composition, tensor, the associator and its formal inverse,
    and the left and right unitors and their formal inverses.
    We will use this syntax to state and prove the coherence theorem and then to construct
    the free monoidal category generated by @{term C}.
›

  locale monoidal_language =
    C: category C
    for C :: "'a comp"                     (infixr  55)
  begin

    datatype (discs_sels) 't "term" =
      Prim 't                              (_)
    | Unity                                ()
    | Tensor "'t term" "'t term"           (infixr  53)
    | Comp "'t term" "'t term"             (infixr  55)
    | Lunit "'t term"                      (𝗅[_])
    | Lunit' "'t term"                     (𝗅-1[_])
    | Runit "'t term"                      (𝗋[_])
    | Runit' "'t term"                     (𝗋-1[_])
    | Assoc "'t term" "'t term" "'t term"  (𝖺[_, _, _])
    | Assoc' "'t term" "'t term" "'t term" (𝖺-1[_, _, _])

    lemma not_is_Tensor_Unity:
    shows "¬ is_Tensor Unity"
      by simp

    text‹
      We define formal domain and codomain functions on terms.
›

    primrec Dom :: "'a term  'a term"
    where "Dom f = C.dom f"
        | "Dom  = "
        | "Dom (t  u) = (Dom t  Dom u)"
        | "Dom (t  u) = Dom u"
        | "Dom 𝗅[t] = (  Dom t)"
        | "Dom 𝗅-1[t] = Dom t"
        | "Dom 𝗋[t] = (Dom t  )"
        | "Dom 𝗋-1[t] = Dom t"
        | "Dom 𝖺[t, u, v] = ((Dom t  Dom u)  Dom v)"
        | "Dom 𝖺-1[t, u, v] = (Dom t  (Dom u  Dom v))"

    primrec Cod :: "'a term  'a term"
    where "Cod f = C.cod f"
        | "Cod  = "
        | "Cod (t  u) = (Cod t  Cod u)"
        | "Cod (t  u) = Cod t"
        | "Cod 𝗅[t] = Cod t"
        | "Cod 𝗅-1[t] = (  Cod t)"
        | "Cod 𝗋[t] = Cod t"
        | "Cod 𝗋-1[t] = (Cod t  )"
        | "Cod 𝖺[t, u, v] = (Cod t  (Cod u  Cod v))"
        | "Cod 𝖺-1[t, u, v] = ((Cod t  Cod u)  Cod v)"

    text‹
      A term is a ``formal arrow'' if it is constructed from arrows of @{term[source=true] C}
      in such a way that composition is applied only to formally composable pairs of terms.
›

    primrec Arr :: "'a term  bool"
    where "Arr f = C.arr f"
        | "Arr  = True"
        | "Arr (t  u) = (Arr t  Arr u)"
        | "Arr (t  u) = (Arr t  Arr u  Dom t = Cod u)"
        | "Arr 𝗅[t] = Arr t"
        | "Arr 𝗅-1[t] = Arr t"
        | "Arr 𝗋[t] = Arr t"
        | "Arr 𝗋-1[t] = Arr t"
        | "Arr 𝖺[t, u, v] = (Arr t  Arr u  Arr v)"
        | "Arr 𝖺-1[t, u, v] = (Arr t  Arr u  Arr v)"

    abbreviation Par :: "'a term  'a term  bool"
    where "Par t u  Arr t  Arr u  Dom t = Dom u  Cod t = Cod u"

    abbreviation Seq :: "'a term  'a term  bool"
    where "Seq t u  Arr t  Arr u  Dom t = Cod u"

    abbreviation Hom :: "'a term  'a term  'a term set"
    where "Hom a b  { t. Arr t  Dom t = a  Cod t = b }"

    text‹
      A term is a ``formal identity'' if it is constructed from identity arrows of
      @{term[source=true] C} and @{term ""} using only the  operator.
›

    primrec Ide :: "'a term  bool"
    where "Ide f = C.ide f"
        | "Ide  = True"
        | "Ide (t  u) = (Ide t  Ide u)"
        | "Ide (t  u) = False"
        | "Ide 𝗅[t] = False"
        | "Ide 𝗅-1[t] = False"
        | "Ide 𝗋[t] = False"
        | "Ide 𝗋-1[t] = False"
        | "Ide 𝖺[t, u, v] = False"
        | "Ide 𝖺-1[t, u, v] = False"

    lemma Ide_implies_Arr [simp]:
    shows "Ide t  Arr t"
      by (induct t) auto

    lemma Arr_implies_Ide_Dom:
    shows "Arr t  Ide (Dom t)"
      by (induct t) auto

    lemma Arr_implies_Ide_Cod:
    shows "Arr t  Ide (Cod t)"
      by (induct t) auto

    lemma Ide_in_Hom [simp]:
    shows "Ide t  t  Hom t t"
      by (induct t) auto

    text‹
      A formal arrow is ``canonical'' if the only arrows of @{term[source=true] C} used in its
      construction are identities.
›

    primrec Can :: "'a term  bool"
    where "Can f = C.ide f"
        | "Can  = True"
        | "Can (t  u) = (Can t  Can u)"
        | "Can (t  u) = (Can t  Can u  Dom t = Cod u)"
        | "Can 𝗅[t] = Can t"
        | "Can 𝗅-1[t] = Can t"
        | "Can 𝗋[t] = Can t"
        | "Can 𝗋-1[t] = Can t"
        | "Can 𝖺[t, u, v] = (Can t  Can u  Can v)"
        | "Can 𝖺-1[t, u, v] = (Can t  Can u  Can v)"

    lemma Ide_implies_Can:
    shows "Ide t  Can t"
      by (induct t) auto

    lemma Can_implies_Arr:
    shows "Can t  Arr t"
      by (induct t) auto

    text‹
      We next define the formal inverse of a term.
      This is only sensible for formal arrows built using only isomorphisms of
      @{term[source=true] C}; in particular, for canonical formal arrows.
›

    primrec Inv :: "'a term  'a term"
    where "Inv f = C.inv f"
        | "Inv  = "
        | "Inv (t  u) = (Inv t  Inv u)"
        | "Inv (t  u) = (Inv u  Inv t)"
        | "Inv 𝗅[t] = 𝗅-1[Inv t]"
        | "Inv 𝗅-1[t] = 𝗅[Inv t]"
        | "Inv 𝗋[t] = 𝗋-1[Inv t]"
        | "Inv 𝗋-1[t] = 𝗋[Inv t]"
        | "Inv 𝖺[t, u, v] = 𝖺-1[Inv t, Inv u, Inv v]"
        | "Inv 𝖺-1[t, u, v] = 𝖺[Inv t, Inv u, Inv v]"

    lemma Inv_preserves_Ide:
    shows "Ide t  Ide (Inv t)"
      by (induct t) auto

    lemma Inv_preserves_Can:
    assumes "Can t"
    shows "Can (Inv t)" and "Dom (Inv t) = Cod t" and "Cod (Inv t) = Dom t"
    proof -
      have 0: "Can t  Can (Inv t)  Dom (Inv t) = Cod t  Cod (Inv t) = Dom t"
        by (induct t) auto
      show "Can (Inv t)" using assms 0 by blast
      show "Dom (Inv t) = Cod t" using assms 0 by blast
      show "Cod (Inv t) = Dom t" using assms 0 by blast
    qed

    lemma Inv_in_Hom [simp]:
    assumes "Can t"
    shows "Inv t  Hom (Cod t) (Dom t)"
      using assms Inv_preserves_Can Can_implies_Arr by simp

    lemma Inv_Ide [simp]:
    assumes "Ide a"
    shows "Inv a = a"
      using assms by (induct a) auto

    lemma Inv_Inv [simp]:
    assumes "Can t"
    shows "Inv (Inv t) = t"
      using assms by (induct t) auto

    text‹
      We call a term ``diagonal'' if it is either @{term ""} or it is constructed from
      arrows of @{term[source=true] C} using only the  operator associated to the right.
      Essentially, such terms are lists of arrows of @{term[source=true] C}, where @{term ""}
      represents the empty list and  is used as the list constructor.
      We call them ``diagonal'' because terms can regarded as defining ``interconnection matrices''
      of arrows connecting ``inputs'' to ``outputs'', and from this point of view diagonal
      terms correspond to diagonal matrices.  The matrix point of view is suggestive for the
      extension of the results presented here to the symmetric monoidal and cartesian monoidal
      cases.
›

    fun Diag :: "'a term  bool"
    where "Diag  = True"
        | "Diag f = C.arr f"
        | "Diag (f  u) = (C.arr f  Diag u  u  )"
        | "Diag _ = False"

    lemma Diag_TensorE:
    assumes "Diag (Tensor t u)"
    shows "un_Prim t = t" and "C.arr (un_Prim t)" and "Diag t" and "Diag u" and "u  "
    proof -
      have 1: "t = un_Prim t  C.arr (un_Prim t)  Diag t  Diag u  u  "
        using assms by (cases t; simp; cases u; simp)
      show "un_Prim t = t" using 1 by simp
      show "C.arr (un_Prim t)" using 1 by simp
      show "Diag t" using 1 by simp
      show "Diag u" using 1 by simp
      show "u  " using 1 by simp
    qed

    lemma Diag_implies_Arr:
    shows "Diag t  Arr t"
      apply (induct t, simp_all)
      by (simp add: Diag_TensorE)

    lemma Dom_preserves_Diag:
    shows "Diag t  Diag (Dom t)"
    apply (induct t, simp_all)
    proof -
      fix u v
      assume I2: "Diag v  Diag (Dom v)"
      assume uv: "Diag (u  v)"
      show "Diag (Dom u  Dom v)"
      proof -
        have 1: "is_Prim (Dom u)  C.arr (un_Prim (Dom u)) 
                 Dom u = C.dom (un_Prim u)"
          using uv by (cases u; simp; cases v, simp_all)
        have 2: "Diag v  v    ¬ is_Comp v  ¬ is_Lunit' v  ¬ is_Runit' v"
          using uv by (cases u; simp; cases v, simp_all)
        have "Diag (Dom v)  Dom v  "
          using 2 I2 by (cases v, simp_all)
        thus ?thesis using 1 by force
      qed
    qed
    
    lemma Cod_preserves_Diag:
    shows "Diag t  Diag (Cod t)"
    apply (induct t, simp_all)
    proof -
      fix u v
      assume I2: "Diag v  Diag (Cod v)"
      assume uv: "Diag (u  v)"
      show "Diag (Cod u  Cod v)"
      proof -
        have 1: "is_Prim (Cod u)  C.arr (un_Prim (Cod u))  Cod u = C.cod (un_Prim u)"
          using uv by (cases u; simp; cases v; simp)
        have 2: "Diag v  v    ¬ is_Comp v  ¬ is_Lunit' v  ¬ is_Runit' v"
          using uv by (cases u; simp; cases v; simp)
        have "Diag (Cod v)  Cod v  "
          using I2 2 by (cases v, simp_all)
        thus ?thesis using 1 by force
      qed
    qed

    lemma Inv_preserves_Diag:
    assumes "Can t" and "Diag t"
    shows "Diag (Inv t)"
    proof -
      have "Can t  Diag t  Diag (Inv t)"
        apply (induct t, simp_all)
        by (metis (no_types, lifting) Can.simps(1) Inv.simps(1) Inv.simps(2) Diag.simps(3)
            Inv_Inv Diag_TensorE(1) C.inv_ide)
      thus ?thesis using assms by blast
    qed

    text‹
      The following function defines the ``dimension'' of a term,
      which is the number of arrows of @{term C} it contains.
      For diagonal terms, this is just the length of the term when regarded as a list
      of arrows of @{term C}.
      Alternatively, if a term is regarded as defining an interconnection matrix,
      then the dimension is the number of inputs (or outputs).
›

    primrec dim :: "'a term  nat"
    where "dim f = 1"
        | "dim  = 0"
        | "dim (t  u) = (dim t + dim u)"
        | "dim (t  u) = dim t"
        | "dim 𝗅[t] = dim t"
        | "dim 𝗅-1[t] = dim t"
        | "dim 𝗋[t] = dim t"
        | "dim 𝗋-1[t] = dim t"
        | "dim 𝖺[t, u, v] = dim t + dim u + dim v"
        | "dim 𝖺-1[t, u, v] = dim t + dim u + dim v"

    text‹
      The following function defines a tensor product for diagonal terms.
      If terms are regarded as lists, this is just list concatenation.
      If terms are regarded as matrices, this corresponds to constructing a block
      diagonal matrix.
›

    fun TensorDiag      (infixr  53)
    where "  u = u"
        | "t   = t"
        | "f  u = f  u"
        | "(t  u)  v = t  (u  v)"
        | "t  u = undefined"

    lemma TensorDiag_Prim [simp]:
    assumes "t  "
    shows "f  t = f  t"
      using assms by (cases t, simp_all)

    lemma TensorDiag_term_Unity [simp]:
    shows "t   = t"
      by (cases "t = "; cases t, simp_all)

    lemma TensorDiag_Diag:
    assumes "Diag (t  u)"
    shows "t  u = t  u"
      using assms TensorDiag_Prim by (cases t, simp_all)

    lemma TensorDiag_preserves_Diag:
    assumes "Diag t" and "Diag u"
    shows "Diag (t  u)"
    and "Dom (t  u) = Dom t  Dom u"
    and "Cod (t  u) = Cod t  Cod u"
    proof -
      have 0: "u.  Diag t; Diag u  
                     Diag (t  u)  Dom (t  u) = Dom t  Dom u 
                                       Cod (t  u) = Cod t  Cod u"
      apply (induct t, simp_all)
      proof -
        fix f :: 'a and u :: "'a term"
        assume f: "C.arr f"
        assume u: "Diag u"
        show "Diag (f  u)  Dom (f  u) = C.dom f  Dom u 
                                 Cod (f  u) = C.cod f  Cod u"
          using u f by (cases u, simp_all)
        next
        fix u v w
        assume I1: "u. Diag v  Diag u  Diag (v  u) 
                                              Dom (v  u) = Dom v  Dom u 
                                              Cod (v  u) = Cod v  Cod u"
        assume I2: "u. Diag w   Diag u  Diag (w  u) 
                                               Dom (w  u) = Dom w  Dom u 
                                               Cod (w  u) = Cod w  Cod u"
        assume vw: "Diag (v  w)"
        assume u: "Diag u"
        show "Diag ((v  w)  u) 
              Dom ((v  w)  u) = (Dom v  Dom w)  Dom u 
              Cod ((v  w)  u) = (Cod v  Cod w)  Cod u"
        proof -
          have v: "v = un_Prim v  Diag v"
            using vw Diag_implies_Arr Diag_TensorE [of v w] by force
          have w: "Diag w"
            using vw by (simp add: Diag_TensorE)
          have "u =   ?thesis" by (simp add: vw)
          moreover have "u    ?thesis"
            using u v w I1 I2 Dom_preserves_Diag [of u] Cod_preserves_Diag [of u]
            by (cases u, simp_all)
          ultimately show ?thesis by blast
        qed
      qed
      show "Diag (t  u) " using assms 0 by blast
      show "Dom (t  u) = Dom t  Dom u" using assms 0 by blast
      show "Cod (t  u) = Cod t  Cod u" using assms 0 by blast
    qed

    lemma TensorDiag_in_Hom:
    assumes "Diag t" and "Diag u"
    shows "t  u  Hom (Dom t  Dom u) (Cod t  Cod u)"
      using assms TensorDiag_preserves_Diag Diag_implies_Arr by simp

    lemma Dom_TensorDiag:
    assumes "Diag t" and "Diag u"
    shows "Dom (t  u) = Dom t  Dom u"
      using assms TensorDiag_preserves_Diag(2) by simp

    lemma Cod_TensorDiag:
    assumes "Diag t" and "Diag u"
    shows "Cod (t  u) = Cod t  Cod u"
      using assms TensorDiag_preserves_Diag(3) by simp

    lemma not_is_Tensor_TensorDiagE:
    assumes "¬ is_Tensor (t  u)" and "Diag t" and "Diag u"
    and "t  " and "u  "
    shows "False"
    proof -
      have " ¬ is_Tensor (t  u); Diag t; Diag u; t  ; u     False"
      apply (induct t, simp_all)
      proof -
        fix v w
        assume I2: "¬ is_Tensor (w  u)  Diag w  w    False"
        assume 1: "¬ is_Tensor ((v  w)  u)"
        assume vw: "Diag (v  w)"
        assume u: "Diag u"
        assume 2: "u  "
        show "False"
        proof -
          have v: "v = un_Prim v"
            using vw Diag_TensorE [of v w] by force
          have w: "Diag w  w  "
            using vw Diag_TensorE [of v w] by simp
          have "(v  w)  u = v  (w  u)"
          proof -
            have "(v  w)  u = v  (w  u)"
              using u 2 by (cases u, simp_all)
            also have "... = v  (w  u)"
              using u v w I2 TensorDiag_Prim not_is_Tensor_Unity by metis
            finally show ?thesis by simp
          qed
          thus ?thesis using 1 by simp
        qed
      qed
      thus ?thesis using assms by blast
    qed

    lemma TensorDiag_assoc:
    assumes "Diag t" and "Diag u" and "Diag v"
    shows "(t  u)  v = t  (u  v)"
    proof -
      have "n t u v.  dim t = n; Diag t; Diag u; Diag v  
                        (t  u)  v = t  (u  v)"
      proof -
        fix n
        show "t u v.  dim t = n; Diag t; Diag u; Diag v  
                        (t  u)  v = t  (u  v)"
        proof (induction n rule: nat_less_induct)
          fix n :: nat and t :: "'a term" and u v
          assume I: "m<n. t u v. dim t = m  Diag t  Diag u  Diag v 
                                   (t  u)  v = t  (u  v)"
          assume dim: "dim t = n"
          assume t: "Diag t"
          assume u: "Diag u"
          assume v: "Diag v"
          show "(t  u)  v = t  (u  v)"
          proof -
            have "t =   ?thesis" by simp
            moreover have "u =   ?thesis" by simp
            moreover have "v =   ?thesis" by simp
            moreover have "t    u    v    is_Prim t  ?thesis"
              using v by (cases t, simp_all, cases u, simp_all; cases v, simp_all)
            moreover have "t    u    v    is_Tensor t  ?thesis"
            proof (cases t; simp)
              fix w :: "'a term" and x :: "'a term"
              assume 1: "u    v  "
              assume 2: "t = (w  x)"
              show "((w  x)  u)  v = (w  x)  (u  v)"
              proof -
                have w: "w = un_Prim w"
                  using t 1 2 Diag_TensorE [of w x] by auto
                have x: "Diag x"
                  using t w 1 2 by (cases w, simp_all)
                have "((w  x)  u)  v = (w  (x  u))  v"
                  using u v w x 1 2 by (cases u, simp_all)
                also have "... = (w  (x  u))  v"
                  using t w u 1 2 TensorDiag_Prim not_is_Tensor_TensorDiagE Diag_TensorE
                        not_is_Tensor_Unity
                  by metis
                also have "... = w  ((x  u)  v)"
                  using u v w x 1 by (cases u, simp_all; cases v, simp_all)
                also have "... = w  (x  (u  v))"
                proof -
                  have "dim x < dim t"
                    using w 2 by (cases w, simp_all)
                  thus ?thesis 
                    using u v x dim I by simp
                qed
                also have "... = (w  x)  (u  v)"
                proof -
                  have 3: "is_Tensor (u  v)"
                    using u v 1 not_is_Tensor_TensorDiagE by auto
                  obtain u' :: "'a term" and v' where uv': "u  v = u'  v'"
                    using 3 is_Tensor_def by blast
                  thus ?thesis by simp
                qed
                finally show ?thesis by simp
              qed
            qed
            moreover have "t =   is_Prim t  is_Tensor t"
              using t by (cases t, simp_all)
            ultimately show ?thesis by blast
          qed
        qed
      qed
      thus ?thesis using assms by blast
    qed

    lemma TensorDiag_preserves_Ide:
    assumes "Ide t" and "Ide u" and "Diag t" and "Diag u"
    shows "Ide (t  u)"
      using assms
      by (metis (mono_tags, lifting) Arr_implies_Ide_Dom Ide_in_Hom Diag_implies_Arr
          TensorDiag_preserves_Diag(1) TensorDiag_preserves_Diag(2) mem_Collect_eq)

    lemma TensorDiag_preserves_Can:
    assumes "Can t" and "Can u" and "Diag t" and "Diag u"
    shows "Can (t  u)"
    proof -
      have "u.  Can t  Diag t; Can u  Diag u   Can (t  u)"
      proof (induct t; simp)
        show "x u. C.ide x  C.arr x  Can u  Diag u  Can (x  u)"
          by (metis Ide.simps(1) Ide.simps(2) Ide_implies_Can Diag.simps(2) TensorDiag_Prim
                    TensorDiag_preserves_Ide Can.simps(3))
        show "t1 t2 u. (u. Diag t1  Can u  Diag u  Can (t1  u)) 
                         (u. Diag t2  Can u  Diag u  Can (t2  u)) 
                         Can t1  Can t2  Diag (t1  t2)  Can u  Diag u 
                         Can ((t1  t2)  u)"
          by (metis Diag_TensorE(3) Diag_TensorE(4) TensorDiag_Diag TensorDiag_assoc
                    TensorDiag_preserves_Diag(1))
      qed
      thus ?thesis using assms by blast
    qed

    lemma Inv_TensorDiag:
    assumes "Can t" and "Can u" and "Diag t" and "Diag u"
    shows "Inv (t  u) = Inv t  Inv u"
    proof -
      have "u.  Can t  Diag t; Can u  Diag u   Inv (t  u) = Inv t  Inv u"
      proof (induct t, simp_all)
        fix f u
        assume f: "C.ide f  C.arr f"
        assume u: "Can u  Diag u"
        show "Inv (f  u) = f  Inv u"
          using f u by (cases u, simp_all)
        next
        fix t u v
        assume I1: "v.  Diag t; Can v  Diag v   Inv (t  v) = Inv t  Inv v"
        assume I2: "v.  Diag u; Can v  Diag v   Inv (u  v) = Inv u  Inv v"
        assume tu: "Can t  Can u  Diag (t  u)"
        have t: "Can t  Diag t"
          using tu Diag_TensorE [of t u] by force
        have u: "Can u  Diag u"
          using t tu by (cases t, simp_all)
        assume v: "Can v  Diag v"
        show "Inv ((t  u)  v) = (Inv t  Inv u)  Inv v"
        proof -
          have "v = Unity  ?thesis" by simp
          moreover have "v  Unity  ?thesis"
          proof -
            assume 1: "v  Unity"
            have "Inv ((t  u)  v) = Inv (t  (u  v))"
              using 1 by (cases v, simp_all)
            also have "... = Inv t  Inv (u  v)"
              using t u v I1 TensorDiag_preserves_Diag TensorDiag_preserves_Can
                    Inv_preserves_Diag Inv_preserves_Can
              by simp
            also have "... = Inv t  (Inv u  Inv v)"
              using t u v I2 TensorDiag_preserves_Diag TensorDiag_preserves_Can
                    Inv_preserves_Diag Inv_preserves_Can
              by simp
            also have "... = (Inv t  Inv u)  Inv v"
              using v 1 by (cases v, simp_all)
            finally show ?thesis by blast
          qed
          ultimately show ?thesis by blast
        qed
      qed
      thus ?thesis using assms by blast
    qed

    text‹
      The following function defines composition for compatible diagonal terms,
      by ``pushing the composition down'' to arrows of C›.
›

    fun CompDiag :: "'a term  'a term  'a term"      (infixr  55)
    where "  u = u"
        | "f  g = f  g"
        | "(u  v)  (w  x) = (u  w  v  x)"
        | "t   = t"
        | "t  _ = undefined  undefined"

    text‹
      Note that the last clause above is not relevant to diagonal terms.
      We have chosen a provably non-diagonal value in order to validate associativity.
›

    lemma CompDiag_preserves_Diag:
    assumes "Diag t" and "Diag u" and "Dom t = Cod u"
    shows "Diag (t  u)"
    and "Dom (t  u) = Dom u"
    and "Cod (t  u) = Cod t"
    proof -
      have 0: "u.  Diag t; Diag u; Dom t = Cod u  
                     Diag (t  u)  Dom (t  u) = Dom u  Cod (t  u) = Cod t"
      proof (induct t, simp_all add: Diag_TensorE)
        fix f u
        assume f: "C.arr f"
        assume u: "Diag u"
        assume 1: "C.dom f = Cod u"
        show "Diag (f  u)  Dom (f  u) = Dom u  Cod (f  u) = C.cod f"
          using f u 1 by (cases u, simp_all)
        next
        fix u v w
        assume I2: "u.  Diag u; Dom w = Cod u  
                          Diag (w  u)  Dom (w  u) = Dom u  Cod (w  u) = Cod w"
        assume vw: "Diag (v  w)"
        have v: "Diag v"
          using vw Diag_TensorE [of v w] by force
        have w: "Diag w"
          using vw Diag_TensorE [of v w] by force
        assume u: "Diag u"
        assume 1: "(Dom v  Dom w) = Cod u"
        show "Diag ((v  w)  u)  Dom ((v  w)  u) = Dom u 
                                     Cod ((v  w)  u) = Cod v  Cod w"
          using u v w 1
        proof (cases u, simp_all)
          fix x y
          assume 2: "u = Tensor x y"
          have 4: "is_Prim x  x = un_Prim x  C.arr (un_Prim x)  Diag y  y  "
            using u 2 by (cases x, cases y, simp_all)
          have 5: "is_Prim v  v = un_Prim v  C.arr (un_Prim v)  Diag w  w  "
            using v w vw by (cases v, simp_all)
          have 6: "C.dom (un_Prim v) = C.cod (un_Prim x)  Dom w = Cod y"
            using 1 2 4 5 apply (cases u, simp_all)
            by (metis Cod.simps(1) Dom.simps(1) term.simps(1))
          have "(v  w)  u = un_Prim v  un_Prim x  w  y"
            using 2 4 5 6 CompDiag.simps(2) [of "un_Prim v" "un_Prim x"] by simp
          moreover have "Diag (un_Prim v  un_Prim x  w  y)"
          proof -
            have "Diag (w  y)"
              using I2 4 5 6 by simp
            thus ?thesis
              using 4 5 6 Diag.simps(3) [of "un_Prim v  un_Prim x" "(w  y)"]
              by (cases w; cases y) auto
          qed
          ultimately show "Diag (v  x  w  y) 
                           Dom (v  x) = Dom x  Dom (w  y) = Dom y 
                           Cod (v  x) = Cod v  Cod (w  y) = Cod w"
            using 4 5 6 I2
            by (metis (full_types) C.cod_comp C.dom_comp Cod.simps(1) CompDiag.simps(2)
                Dom.simps(1) C.seqI)
        qed
      qed
      show "Diag (t  u)" using assms 0 by blast
      show "Dom (t  u) = Dom u" using assms 0 by blast
      show "Cod (t  u) = Cod t" using assms 0 by blast
    qed

    lemma CompDiag_in_Hom:
    assumes "Diag t" and "Diag u" and "Dom t = Cod u"
    shows "t  u  Hom (Dom u) (Cod t)"
      using assms CompDiag_preserves_Diag Diag_implies_Arr by simp

    lemma Dom_CompDiag:
    assumes "Diag t" and "Diag u" and "Dom t = Cod u"
    shows "Dom (t  u) = Dom u"
      using assms CompDiag_preserves_Diag(2) by simp

    lemma Cod_CompDiag:
    assumes "Diag t" and "Diag u" and "Dom t = Cod u"
    shows "Cod (t  u) = Cod t"
      using assms CompDiag_preserves_Diag(3) by simp

    lemma CompDiag_Cod_Diag [simp]:
    assumes "Diag t"
    shows "Cod t  t = t"
    proof -
      have "Diag t  Cod t  t = t"
        using C.comp_cod_arr
        apply (induct t, auto)
        by (auto simp add: Diag_TensorE)
      thus ?thesis using assms by blast
    qed

    lemma CompDiag_Diag_Dom [simp]:
    assumes "Diag t"
    shows "t  Dom t = t"
    proof -
      have "Diag t  t  Dom t = t"
        using C.comp_arr_dom
        apply (induct t, auto)
        by (auto simp add: Diag_TensorE)
      thus ?thesis using assms by blast
    qed

    lemma CompDiag_Ide_Diag [simp]:
    assumes "Diag t" and "Ide a" and "Dom a = Cod t"
    shows "a  t = t"
      using assms Ide_in_Hom by simp

    lemma CompDiag_Diag_Ide [simp]:
    assumes "Diag t" and "Ide a" and "Dom t = Cod a"
    shows "t  a = t"
      using assms Ide_in_Hom by auto

    lemma CompDiag_assoc:
    assumes "Diag t" and "Diag u" and "Diag v"
    and "Dom t = Cod u" and "Dom u = Cod v"
    shows "(t  u)  v = t  (u  v)"
    proof -
      have "u v.  Diag t; Diag u; Diag v; Dom t = Cod u; Dom u = Cod v  
                    (t  u)  v = t  (u  v)"
      proof (induct t, simp_all)
        fix f u v
        assume f: "C.arr f"
        assume u: "Diag u"
        assume v: "Diag v"
        assume 1: "C.dom f = Cod u"
        assume 2: "Dom u = Cod v"
        show "(f  u)  v = f  (u  v)"
          using C.comp_assoc by (cases u, simp_all; cases v, simp_all)
        next
        fix u v w x
        assume I1: "u v.  Diag w; Diag u; Diag v; Dom w = Cod u; Dom u = Cod v  
                            (w  u)  v = w  (u  v)"
        assume I2: "u v.  Diag x; Diag u; Diag v; Dom x = Cod u; Dom u = Cod v  
                            (x  u)  v = x  (u  v)"
        assume wx: "Diag (w  x)"
        assume u: "Diag u"
        assume v: "Diag v"
        assume 1: "(Dom w  Dom x) = Cod u"
        assume 2: "Dom u = Cod v"
        show "((w  x)  u)  v = (w  x)  u  v"
        proof -
          have w: "Diag w"
            using wx Diag_TensorE by blast
          have x: "Diag x"
            using wx Diag_TensorE by blast
          have "is_Tensor u"
            using u 1 by (cases u) simp_all
          thus ?thesis
            using u v apply (cases u, simp_all, cases v, simp_all)
          proof -
            fix u1 u2 v1 v2
            assume 3: "u = (u1  u2)"
            assume 4: "v = (v1  v2)"
            show "(w  u1)  v1 = w  u1  v1 
                  (x  u2)  v2 = x  u2  v2"
            proof -
              have "Diag u1  Diag u2"
                using u 3 Diag_TensorE by blast
              moreover have "Diag v1  Diag v2"
                using v 4 Diag_TensorE by blast
              ultimately show ?thesis using w x I1 I2 1 2 3 4 by simp
            qed
          qed
        qed
      qed
      thus ?thesis using assms by blast
    qed

    lemma CompDiag_preserves_Ide:
    assumes "Ide t" and "Ide u" and "Diag t" and "Diag u" and "Dom t = Cod u"
    shows "Ide (t  u)"
    proof -
      have "u.  Ide t; Ide u; Diag t; Diag u; Dom t = Cod u   Ide (CompDiag t u)"
        by (induct t; simp)
      thus ?thesis using assms by blast
    qed

    lemma CompDiag_preserves_Can:
    assumes "Can t" and "Can u" and "Diag t" and "Diag u" and "Dom t = Cod u"
    shows "Can (t  u)"
    proof -
      have "u.  Can t  Diag t; Can u  Diag u; Dom t = Cod u   Can (t  u)"
      proof (induct t, simp_all)
        fix t u v
        assume I1: "v.  Diag t; Can v  Diag v; Dom t = Cod v   Can (t  v)"
        assume I2: "v.  Diag u; Can v  Diag v; Dom u = Cod v   Can (u  v)"
        assume tu: "Can t  Can u  Diag (t  u)"
        have t: "Can t  Diag t"
          using tu Diag_TensorE by blast
        have u: "Can u  Diag u"
          using tu Diag_TensorE by blast
        assume v: "Can v  Diag v"
        assume 1: "(Dom t  Dom u) = Cod v"
        show "Can ((t  u)  v)"
        proof -
          have 2: "(Dom t  Dom u) = Cod v" using 1 by simp
          show ?thesis
            using v 2
          proof (cases v; simp)
            fix w x
            assume wx: "v = (w  x)"
            have "Can w  Diag w" using v wx Diag_TensorE [of w x] by auto
            moreover have "Can x  Diag x" using v wx Diag_TensorE [of w x] by auto
            moreover have "Dom t = Cod w" using 2 wx by simp
            moreover have ux: "Dom u = Cod x" using 2 wx by simp
            ultimately show "Can (t  w)  Can (u  x)"
              using t u I1 I2 by simp
          qed
        qed
      qed
      thus ?thesis using assms by blast
    qed

    lemma Inv_CompDiag:
    assumes "Can t" and "Can u" and "Diag t" and "Diag u" and "Dom t = Cod u"
    shows "Inv (t  u) = Inv u  Inv t"
    proof -
      have "u.  Can t  Diag t; Can u  Diag u; Dom t = Cod u  
              Inv (t  u) = Inv u  Inv t"
      proof (induct t, simp_all)
        show "x u.  C.ide x  C.arr x; Can u  Diag u; x = Cod u  
                      Inv u = Inv u  Inv (Cod u)"
          by (metis CompDiag_Diag_Dom Inv_Ide Inv_preserves_Can(2) Inv_preserves_Diag
                    Ide.simps(1))
        show "u. Can u  Diag u   = Cod u  Inv u = Inv u  "
          by (simp add: Inv_preserves_Can(2) Inv_preserves_Diag)
        fix t u v
        assume tu: "Can t  Can u  Diag (t  u)"
        have t: "Can t  Diag t"
          using tu Diag_TensorE by blast
        have u: "Can u  Diag u"
          using tu Diag_TensorE by blast
        assume I1: "v.  Diag t; Can v  Diag v; Dom t = Cod v  
                          Inv (t  v) = Inv v  Inv t"
        assume I2: "v.  Diag u; Can v  Diag v; Dom u = Cod v  
                          Inv (u  v) = Inv v  Inv u"
        assume v: "Can v  Diag v"
        assume 1: "(Dom t  Dom u) = Cod v"
        show "Inv ((t  u)  v) = Inv v  (Inv t  Inv u)"
          using v 1
        proof (cases v, simp_all)
          fix w x
          assume wx: "v = (w  x)"
          have "Can w  Diag w" using v wx Diag_TensorE [of w x] by auto
          moreover have "Can x  Diag x" using v wx Diag_TensorE [of w x] by auto
          moreover have "Dom t = Cod w" using wx 1 by simp
          moreover have "Dom u = Cod x" using wx 1 by simp
          ultimately show "Inv (t  w) = Inv w  Inv t 
                           Inv (u  x) = Inv x  Inv u"
            using t u I1 I2 by simp
        qed
      qed
      thus ?thesis using assms by blast
    qed

    lemma Can_and_Diag_implies_Ide:
    assumes "Can t" and "Diag t"
    shows "Ide t"
    proof -
      have " Can t; Diag t   Ide t"
        apply (induct t, simp_all)
        by (simp add: Diag_TensorE)
      thus ?thesis using assms by blast
    qed

    lemma CompDiag_Can_Inv [simp]:
    assumes "Can t" and "Diag t"
    shows "t  Inv t = Cod t"
      using assms Can_and_Diag_implies_Ide Ide_in_Hom by simp
      
    lemma CompDiag_Inv_Can [simp]:
    assumes "Can t" and "Diag t"
    shows "Inv t  t = Dom t"
      using assms Can_and_Diag_implies_Ide Ide_in_Hom by simp

    text‹
      The next fact is a syntactic version of the interchange law, for diagonal terms.
›

    lemma CompDiag_TensorDiag:
    assumes "Diag t" and "Diag u" and "Diag v" and "Diag w"
    and "Seq t v" and "Seq u w"
    shows "(t  u)  (v  w) = (t  v)  (u  w)"
    proof -
      have "u v w.  Diag t; Diag u; Diag v; Diag w; Seq t v; Seq u w  
                      (t  u)  (v  w) = (t  v)  (u  w)"
      proof (induct t, simp_all)
        fix u v w
        assume u: "Diag u"
        assume v: "Diag v"
        assume w: "Diag w"
        assume uw: "Seq u w"
        show "Arr v   = Cod v  u  (v  w) = v  (u  w)"
          using u v w uw by (cases v) simp_all
        show "f.  C.arr f; Arr v  C.dom f = Cod v  
                    (f  u)  (v  w) = (f  v)  (u  w)"
        proof -
          fix f
          assume f: "C.arr f"
          assume 1: "Arr v  C.dom f = Cod v"
          show "(f  u)  (v  w) = (f  v)  (u  w)"
          proof -
            have 2: "v = un_Prim v  C.arr (un_Prim v)" using v 1 by (cases v) simp_all
            have "u =   ?thesis"
              using v w uw 1 2 Cod.simps(3) CompDiag_Cod_Diag Dom.simps(2)
                    TensorDiag_Prim TensorDiag_term_Unity TensorDiag_preserves_Diag(3)
              by (cases w) simp_all
            moreover have "u    ?thesis"
            proof -
              assume 3: "u  "
              hence 4: "w  " using u w uw by (cases u, simp_all; cases w, simp_all)
              have "(f  u)  (v  w) = (f  u)  (v  w)"
              proof -
                have "f  u = f  u"
                  using u f 3 TensorDiag_Diag by (cases u) simp_all
                moreover have "v  w = v  w"
                  using w 2 4 TensorDiag_Diag by (cases v, simp_all; cases w, simp_all)
                ultimately show ?thesis by simp
              qed
              also have 5: "... = (f  v)  (u  w)" by simp
              also have "... = (f  v)  (u  w)"
                using f u w uw 1 2 3 4 5
                      TensorDiag_Diag TensorDiag_Prim TensorDiag_preserves_Diag(1)
                      CompDiag_preserves_Diag(1)
                by (metis Cod.simps(3) Dom.simps(1) Dom.simps(3) Diag.simps(2))
              finally show ?thesis by blast
            qed
            ultimately show ?thesis by blast
          qed
        qed
        fix t1 t2
        assume I2: "u v w.  Diag t2; Diag u; Diag v; Diag w;
                              Arr v  Dom t2 = Cod v; Seq u w  
                              (t2  u)  (v  w) = (t2  v)  (u  w)"
        assume t12: "Diag (t1  t2)"
        have t1: "t1 = un_Prim t1  C.arr (un_Prim t1)  Diag t1"
          using t12 by (cases t1) simp_all
        have t2: "Diag t2  t2  "
          using t12 by (cases t1) simp_all
        assume 1: "Arr t1  Arr t2  Arr v  Dom t1  Dom t2 = Cod v"
        show "((t1  t2)  u)  (v  w) = ((t1  t2)  v)  (u  w)"
        proof -
          have "u =   ?thesis"
            using w uw TensorDiag_term_Unity CompDiag_Cod_Diag by (cases w) simp_all
          moreover have "u    ?thesis"
          proof -
            assume u': "u  "
            hence w': "w  " using u w uw by (cases u; simp; cases w; simp)
            show ?thesis
              using 1 v
            proof (cases v, simp_all)
              fix v1 v2
              assume v12: "v = Tensor v1 v2"
              have v1: "v1 = un_Prim v1  C.arr (un_Prim v1)  Diag v1"
                using v v12 by (cases v1) simp_all
              have v2: "Diag v2  v2  "
                using v v12 by (cases v1) simp_all
              have 2: "v = (un_Prim v1  v2)"
                using v1 v12 by simp
              show "((t1  t2)  u)  ((v1  v2)  w)
                      = ((t1  v1)  (t2  v2))  (u  w)"
              proof -
                have 3: "(t1  t2)  u = t1  (t2  u)"
                  using u u' by (cases u) simp_all
                have 4: "v  w = v1  (v2  w)"
                  using v w v1 v2 2 TensorDiag_assoc TensorDiag_Diag by metis
                have "((t1  t2)  u)  ((v1  v2)  w)
                        = (t1  (t2  u))  (v1  (v2  w))"
                  using 3 4 v12 by simp
                also have "... = (t1  v1)  ((t2  u)  (v2  w))"
                proof -
                  have "is_Tensor (t2  u)"
                    using t2 u u' not_is_Tensor_TensorDiagE by auto
                  moreover have "is_Tensor (v2  w)"
                    using v2 v12 w w' not_is_Tensor_TensorDiagE by auto
                  ultimately show ?thesis
                    using u u' v w t1 v1 t12 v12 TensorDiag_Prim not_is_Tensor_Unity
                    by (metis (no_types, lifting) CompDiag.simps(2) CompDiag.simps(3)
                        is_Tensor_def)
                qed
                also have "... = (t1  v1)  (t2  v2)  (u  w)"
                  using u w uw t2 v2 1 2 Diag_implies_Arr I2 by fastforce
                also have "... = ((t1  v1)  (t2  v2))  (u  w)"
                proof -
                  have "u  w  Unity"
                  proof -
                    have "Arr v1  C.dom (un_Prim t1) = Cod v1"
                      using t1 v1 1 2 by (cases t1, auto)
                    thus ?thesis
                      using t1 t2 v1 v2 u w uw u' CompDiag_preserves_Diag
                            TensorDiag_preserves_Diag TensorDiag_Prim
                      by (metis (mono_tags, lifting) Cod.simps(2) Cod.simps(3)
                          TensorDiag.simps(2) term.distinct(3))
                  qed
                  hence "((t1  v1)  (t2  v2))  (u  w)
                           = (t1  v1)  ((t2  v2)  (u  w))"
                    by (cases "u  w") simp_all
                  thus ?thesis by argo
                qed
                finally show ?thesis by blast
              qed
            qed
          qed
          ultimately show ?thesis by blast
        qed
      qed
      thus ?thesis using assms by blast
    qed

    text‹
      The following function reduces an arrow to diagonal form.
      The precise relationship between a term and its diagonalization is developed below.
›

    fun Diagonalize :: "'a term  'a term"   (_)
    where "f = f"
        | " = "
        | "t  u = t  u"
        | "t  u = t  u"
        | "𝗅[t] = t"
        | "𝗅-1[t] = t"
        | "𝗋[t] = t"
        | "𝗋-1[t] = t"
        | "𝖺[t, u, v] = (t  u)  v"
        | "𝖺-1[t, u, v] = t  (u  v)"

    lemma Diag_Diagonalize:
    assumes "Arr t"
    shows "Diag t" and "Dom t = Dom t" and "Cod t = Cod t"
    proof -
      have 0: "Arr t  Diag t  Dom t = Dom t  Cod t = Cod t"
        using TensorDiag_preserves_Diag CompDiag_preserves_Diag TensorDiag_assoc
        apply (induct t)
                 apply auto
         apply (metis (full_types))
        by (metis (full_types))
      show "Diag t" using assms 0 by blast
      show "Dom t = Dom t" using assms 0 by blast
      show "Cod t = Cod t" using assms 0 by blast
    qed

    lemma Diagonalize_in_Hom:
    assumes "Arr t"
    shows "t  Hom Dom t Cod t"
      using assms Diag_Diagonalize Diag_implies_Arr by blast

    lemma Diagonalize_Dom:
    assumes "Arr t"
    shows "Dom t = Dom t"
      using assms Diagonalize_in_Hom by simp

    lemma Diagonalize_Cod:
    assumes "Arr t"
    shows "Cod t = Cod t"
      using assms Diagonalize_in_Hom by simp

    lemma Diagonalize_preserves_Ide:
    assumes "Ide a"
    shows "Ide a"
    proof -
      have "Ide a  Ide a"
        using Ide_implies_Arr TensorDiag_preserves_Ide Diag_Diagonalize
        by (induct a) simp_all
      thus ?thesis using assms by blast
    qed

    text‹
      The diagonalizations of canonical arrows are identities.
›

    lemma Ide_Diagonalize_Can:
    assumes "Can t"
    shows "Ide t"
    proof -
      have "Can t  Ide t"
        using Can_implies_Arr TensorDiag_preserves_Ide Diag_Diagonalize CompDiag_preserves_Ide
              TensorDiag_preserves_Diag
        by (induct t) auto
      thus ?thesis using assms by blast
    qed

    lemma Diagonalize_preserves_Can:
    assumes "Can t"
    shows "Can t"
      using assms Ide_Diagonalize_Can Ide_implies_Can by auto

    lemma Diagonalize_Diag [simp]:
    assumes "Diag t"
    shows "t = t"
    proof -
      have "Diag t  t = t"
        apply (induct t, simp_all)
        using TensorDiag_Prim Diag_TensorE by metis
      thus ?thesis using assms by blast
    qed

    lemma Diagonalize_Diagonalize [simp]:
    assumes "Arr t"
    shows "t = t"
      using assms Diag_Diagonalize Diagonalize_Diag by blast

    lemma Diagonalize_Tensor:
    assumes "Arr t" and "Arr u"
    shows "t  u = t  u"
      using assms Diagonalize_Diagonalize by simp

    lemma Diagonalize_Tensor_Unity_Arr [simp]:
    assumes "Arr u"
    shows "  u = u"
      using assms by simp

    lemma Diagonalize_Tensor_Arr_Unity [simp]:
    assumes "Arr t"
    shows "t   = t"
      using assms by simp

    lemma Diagonalize_Tensor_Prim_Arr [simp]:
    assumes "arr f" and "Arr u" and "u  Unity"
    shows "f  u = f  u"
      using assms by simp

    lemma Diagonalize_Tensor_Tensor:
    assumes "Arr t" and "Arr u" and "Arr v"
    shows "(t  u)  v = t  (u  v)"
      using assms Diag_Diagonalize Diagonalize_Diagonalize by (simp add: TensorDiag_assoc)

    lemma Diagonalize_Comp_Cod_Arr:
    assumes "Arr t"
    shows "Cod t  t = t"
    proof -
      have "Arr t  Cod t  t = t"
        using C.comp_cod_arr
        apply (induct t, simp_all)
        using CompDiag_TensorDiag Arr_implies_Ide_Cod Ide_in_Hom Diag_Diagonalize
              Diagonalize_in_Hom
           apply simp
        using CompDiag_preserves_Diag CompDiag_Cod_Diag Diag_Diagonalize
          apply metis
        using CompDiag_TensorDiag Arr_implies_Ide_Cod Ide_in_Hom TensorDiag_in_Hom
              TensorDiag_preserves_Diag Diag_Diagonalize Diagonalize_in_Hom TensorDiag_assoc
        by simp_all
      thus ?thesis using assms by blast
    qed

    lemma Diagonalize_Comp_Arr_Dom:
    assumes "Arr t"
    shows "t  Dom t = t"
    proof -
      have "Arr t  t  Dom t = t"
        by (metis CompDiag_Diag_Dom Diag_Diagonalize(1-2) Diagonalize.simps(4))
      thus ?thesis using assms by blast
    qed

    lemma Diagonalize_Inv:
    assumes "Can t"
    shows "Inv t = Inv t"
    proof -
      have "Can t  Inv t = Inv t"
      proof (induct t, simp_all)
        fix u v
        assume I1: "Inv u = Inv u"
        assume I2: "Inv v = Inv v"
        show "Can u  Can v  Inv u  Inv v = Inv (u  v)"
          using Inv_TensorDiag Diag_Diagonalize Can_implies_Arr Diagonalize_preserves_Can
                I1 I2
          by simp
        show "Can u  Can v  Dom u = Cod v  Inv v  Inv u = Inv (u  v)"
          using Inv_CompDiag Diag_Diagonalize Can_implies_Arr Diagonalize_in_Hom
                Diagonalize_preserves_Can I1 I2
          by simp
        fix w
        assume I3: "Inv w = Inv w"
        assume uvw: "Can u  Can v  Can w"
        show "Inv u  (Inv v  Inv w) = Inv ((u  v)  w)"
          using uvw I1 I2 I3
                Inv_TensorDiag Diag_Diagonalize Can_implies_Arr Diagonalize_preserves_Can
                TensorDiag_preserves_Diag TensorDiag_preserves_Can TensorDiag_assoc
          by simp
        show "(Inv u  Inv v)  Inv w = Inv (u  (v  w))"
          by (simp add: Can_implies_Arr Ide_Diagonalize_Can TensorDiag_assoc
              TensorDiag_preserves_Diag(1) TensorDiag_preserves_Ide Diag_Diagonalize(1) uvw)
      qed
      thus ?thesis using assms by blast
    qed

    text‹
      Our next objective is to begin making the connection, to be completed in a
      subsequent section, between arrows and their diagonalizations.
      To summarize, an arrow @{term t} and its diagonalization @{term "t"} are opposite sides
      of a square whose other sides are certain canonical terms
      Dom t ∈ Hom (Dom t) Dom t and Cod t ∈ Hom (Cod t) Cod t,
      where Dom t and Cod t are defined by the function red›
      below.  The coherence theorem amounts to the statement that every such square commutes
      when the formal terms involved are evaluated in the evident way in any monoidal category.

      Function red› defined below takes an identity term @{term a} to a canonical arrow
      a ∈ Hom a a.  The auxiliary function red2› takes a pair @{term "(a, b)"}
      of diagonal identity terms and produces a canonical arrow
      a  b ∈ Hom (a  b) a  b.
      The canonical arrow a amounts to a ``parallel innermost reduction''
      from @{term a} to @{term "a"}, where the reduction steps are canonical arrows
      that involve the unitors and associator only in their uninverted forms.
      In general, a parallel innermost reduction from @{term a} will not be unique:
      at some points there is a choice available between left and right unitors
      and at other points there are choices between unitors and associators.
      These choices are inessential, and the ordering of the clauses in the function definitions
      below resolves them in an arbitrary way.  What is more important is having chosen an
      innermost reduction, which is what allows us to write these definitions in structurally
      recursive form.

      The essence of coherence is that the axioms for a monoidal category allow us to
      prove that any reduction from @{term a} to @{term "a"} is equivalent
      (under evaluation of terms) to a parallel innermost reduction.
      The problematic cases are terms of the form @{term "((a  b)  c)  d"},
      which present a choice between an inner and outer reduction that lead to terms
      with different structures.  It is of course the pentagon axiom that ensures the
      confluence (under evaluation) of the two resulting paths.

      Although simple in appearance, the structurally recursive definitions below were
      difficult to get right even after I started to understand what I was doing.
      I wish I could have just written them down straightaway.  If so, then I could have
      avoided laboriously constructing and then throwing away thousands of lines of proof
      text that used a non-structural, ``operational'' approach to defining a reduction
      from @{term a} to @{term "a"}.
›

    fun red2                       (infixr  53)
    where "  a = 𝗅[a]"
        | "f   = 𝗋[f]"
        | "f  a = f  a"
        | "(a  b)   = 𝗋[a  b]"
        | "(a  b)  c = (a  b  c)  (a  (b  c))  𝖺[a, b, c]"
        | "a  b = undefined"

    fun red                         (‹_ [56] 56)
    where " = "
        | "f = f"
        | "(a  b) = (if Diag (a  b) then a  b else (a  b)  (a  b))"
        | "a = undefined"

    lemma red_Diag [simp]:
    assumes "Diag a"
    shows "a = a"
      using assms by (cases a) simp_all

    lemma red2_Diag:
    assumes "Diag (a  b)"
    shows "a  b = a  b"
    proof -
      have a: "a = un_Prim a"
        using assms Diag_TensorE by metis
      have b: "Diag b  b  "
        using assms Diag_TensorE by metis
      show ?thesis using a b
        apply (cases b)
          apply simp_all
         apply (metis red2.simps(3))
        by (metis red2.simps(4))
    qed

    lemma Can_red2:
    assumes "Ide a" and "Diag a" and "Ide b" and "Diag b"
    shows "Can (a  b)"
    and "a  b  Hom (a  b) a  b"
    proof -
      have 0: "b.  Ide a  Diag a; Ide b  Diag b  
                     Can (a  b)  a  b  Hom (a  b) a  b"
      proof (induct a, simp_all)
        fix b
        show "Ide b  Diag b  Can b  Dom b = b  Cod b = b"
          using Ide_implies_Can Ide_in_Hom Diagonalize_Diag by auto
        fix f
        show " C.ide f  C.arr f; Ide b  Diag b  
                Can (f  b)  Arr (f  b)  Dom (f  b) = f  b 
                                                Cod (f  b) = f  b"
          using Ide_implies_Can Ide_in_Hom by (cases b; auto)
        next
        fix a b c
        assume ab: "Ide a  Ide b  Diag (Tensor a b)"
        assume c: "Ide c  Diag c"
        assume I1: "c.  Diag a; Ide c  Diag c  
                          Can (a  c)  Arr (a  c)  Dom (a  c) = a  c 
                                                       Cod (a  c) = a  c"
        assume I2: "c.  Diag b; Ide c  Diag c  
                          Can (b  c)  Arr (b  c)  Dom (b  c) = b  c 
                                                       Cod (b  c) = b  c"
        show "Can ((a  b)  c)  Arr ((a  b)  c) 
              Dom ((a  b)  c) = (a  b)  c 
              Cod ((a  b)  c) = (a  b)  c"
        proof -
          have a: "Diag a  Ide a"
            using ab Diag_TensorE by blast
          have b: "Diag b  Ide b"
            using ab Diag_TensorE by blast
          have "c =   ?thesis"
          proof -
            assume 1: "c = "
            have 2: "(a  b)  c = 𝗋[a  b]"
              using 1 by simp
            have 3: "Can (a  b)  Arr (a  b)  Dom (a  b) = a  b  Cod (a  b) = a  b"
              using a b ab 1 2 I1 Diagonalize_Diag Diagonalize.simps(3) by metis
            hence 4: "Seq (a  b) 𝗋[a  b]"
              using ab
              by (metis (mono_tags, lifting) Arr.simps(7) Cod.simps(3) Cod.simps(7)
                  Diag_implies_Arr Ide_in_Hom mem_Collect_eq)
            have "Can ((a  b)  c)"
              using 1 2 3 4 ab by (simp add: Ide_implies_Can)
            moreover have "Dom ((a  b)  c) = (a  b)  c"
              using 1 2 3 4 a b ab I1 Ide_in_Hom TensorDiag_preserves_Diag by simp
            moreover have "Cod ((a  b)  c) = (a  b)  c"
             using 1 2 3 4 ab using Diagonalize_Diag by fastforce
            ultimately show ?thesis using Can_implies_Arr by (simp add: 1 ab)
          qed
          moreover have "c    ?thesis"
          proof -
            assume 1: "c  "
            have 2: "(a  b)  c = (a  b  c)  (a  b  c)  𝖺[a, b, c]"
              using 1 a b ab c by (cases c; simp)
            have 3: "Can (a  b  c)  Dom (a  b  c) = a  b  c 
                                          Cod (a  b  c) = a  (b  c)"
            proof -
              have "Can (a  b  c)  Dom (a  b  c) = a  b  c 
                                         Cod (a  b  c) = a  b  c"
                using a c ab 1 2 I1 Diag_implies_Arr Diag_Diagonalize(1)
                      Diagonalize_preserves_Ide TensorDiag_preserves_Ide
                      TensorDiag_preserves_Diag(1)
                by auto
              moreover have "a  b  c = a  (b  c)"
                using ab c Diagonalize_Tensor Diagonalize_Diagonalize Diag_implies_Arr
                by (metis Arr.simps(3) Diagonalize.simps(3))
              ultimately show ?thesis by metis
            qed
            have 4: "Can (b  c)  Dom (b  c) = b  c  Cod (b  c) = b  c"
              using b c ab 1 2 I2 by simp
            hence "Can (a  (b  c))  Dom (a  (b  c)) = a  (b  c) 
                                        Cod (a  (b  c)) = a  b  c"
              using ab Ide_implies_Can Ide_in_Hom by force
            moreover have "a  b  c = a  b  c"
            proof -
              have "a  b  c = a  (b  c)"
                using a b c 4
                by (metis Arr_implies_Ide_Dom Can_implies_Arr Ide_implies_Arr
                    Diag_Diagonalize(1) Diagonalize.simps(3) Diagonalize_Diag)
              also have "... = (a  b)  c"
                using a b ab c TensorDiag_assoc by metis
              also have "... = a  b  c"
                using a b c by (metis Diagonalize.simps(3) Diagonalize_Diag)
              finally show ?thesis by blast
            qed
            moreover have "Can 𝖺[a, b, c]  Dom 𝖺[a, b, c] = (a  b)  c 
                                            Cod 𝖺[a, b, c] = a  (b  c)"
              using ab c Ide_implies_Can Ide_in_Hom by auto
            ultimately show ?thesis
              using c 2 3 4 Diagonalize_Diagonalize Ide_implies_Can
                    Diagonalize_Diag Arr_implies_Ide_Dom Can_implies_Arr
              by (metis Can.simps(4) Cod.simps(4) Dom.simps(4) Diagonalize.simps(3))
          qed
          ultimately show ?thesis by blast
        qed
      qed
      show "Can (a  b)" using assms 0 by blast
      show "a  b  Hom (a  b) a  b" using 0 assms by blast
    qed

    lemma red2_in_Hom:
    assumes "Ide a" and "Diag a" and "Ide b" and "Diag b"
    shows "a  b  Hom (a  b) a  b"
      using assms Can_red2 Can_implies_Arr by simp

    lemma Can_red:
    assumes "Ide a"
    shows "Can (a)" and "a  Hom a a"
    proof -
      have 0: "Ide a  Can (a)  a  Hom a a"
      proof (induct a, simp_all)
        fix b c
        assume b: "Can (b)  Arr (b)  Dom (b) = b  Cod (b) = b"
        assume c: "Can (c)  Arr (c)  Dom (c) = c  Cod (c) = c"
        assume bc: "Ide b  Ide c"
        show "(Diag (b  c) 
                 Can b  Can c  Dom b = b  Dom c = c  Cod b  Cod c = b  c) 
              (¬ Diag (b  c) 
                 Can (b  c)  Dom (b  c) = b  c  Arr (b  c) 
                 Dom (b  c) = b  c  Cod (b  c) = b  c)"
        proof
          show "Diag (b  c) 
                  Can b  Can c  Dom b = b  Dom c = c  Cod b  Cod c = b  c"
            using bc Diag_TensorE Ide_implies_Can Inv_preserves_Can(2)
                  CompDiag_Ide_Diag Inv_Ide Diagonalize.simps(3) Diagonalize_Diag
            by (metis CompDiag_Inv_Can)
          show "¬ Diag (b  c) 
                  Can (b  c)  Dom (b  c) = b  c  Arr (b  c) 
                                    Dom (b  c) = b  c  Cod (b  c) = b  c"
            using b c bc Ide_in_Hom Ide_implies_Can Can_red2 Diag_Diagonalize
                  Diagonalize_preserves_Ide TensorDiag_preserves_Diag TensorDiag_preserves_Ide
            by force
        qed
      qed
      show "Can (a)" using assms 0 by blast
      show "a  Hom a a" using assms 0 by blast
    qed

    lemma red_in_Hom:
    assumes "Ide a"
    shows "a  Hom a a"
      using assms Can_red Can_implies_Arr by simp

    lemma Diagonalize_red [simp]:
    assumes "Ide a"
    shows "a = a"
      using assms Can_red Ide_Diagonalize_Can Diagonalize_in_Hom Ide_in_Hom by fastforce

    lemma Diagonalize_red2 [simp]:
    assumes "Ide a" and "Ide b" and "Diag a" and "Diag b"
    shows "a  b = a  b"
      using assms Can_red2 Ide_Diagonalize_Can Diagonalize_in_Hom [of "a  b"]
            red2_in_Hom Ide_in_Hom
      by simp

  end

  section "Coherence"

  text‹
    If @{term D} is a monoidal category, then a functor V: C → D› extends
    in an evident way to an evaluation map that interprets each formal arrow of the
    monoidal language of @{term C} as an arrow of @{term D}.
›

  locale evaluation_map =
    monoidal_language C +
    monoidal_category D T α ι +
    V: "functor" C D V
  for C :: "'c comp"                  (infixr C 55)
  and D :: "'d comp"                  (infixr  55)
  and T :: "'d * 'd  'd"
  and α :: "'d * 'd * 'd  'd"
  and ι :: 'd
  and V :: "'c  'd"
  begin

    no_notation C.in_hom               («_ : _  _»)

    notation unity                     ()
    notation runit                     (𝗋[_])
    notation lunit                     (𝗅[_])
    notation assoc'                    (𝖺-1[_, _, _])
    notation runit'                    (𝗋-1[_])
    notation lunit'                    (𝗅-1[_])

    primrec eval :: "'c term  'd"    (_)
    where "f = V f"
        | " = "
        | "t  u = t  u"
        | "t  u = t  u"
        | "𝗅[t] = 𝔩 t"
        | "𝗅-1[t] = 𝔩' t"
        | "𝗋[t] = ρ t"
        | "𝗋-1[t] = ρ' t"
        | "𝖺[t, u, v] = α (t, u, v)"
        | "𝖺-1[t, u, v] = α' (t, u, v)"

    text‹
      Identity terms evaluate to identities of D› and evaluation preserves
      domain and codomain.
›

    lemma ide_eval_Ide [simp]:
    shows "Ide t  ide t"
      by (induct t, auto)

    lemma eval_in_hom:
    shows "Arr t  «t : Dom t  Cod t»"
      apply (induct t)
               apply auto[4]
          apply fastforce
    proof -
      fix t u v
      assume I: "Arr t  «t : Dom t  Cod t»"
      show "Arr 𝗅-1[t]  «𝗅-1[t] : Dom 𝗅-1[t]  Cod 𝗅-1[t]»"
        using I arr_dom_iff_arr [of "t"] by force
      show "Arr 𝗋[t]  «𝗋[t] : Dom 𝗋[t]  Cod 𝗋[t]»"
        using I arr_cod_iff_arr [of "t"] by force
      show "Arr 𝗋-1[t]  «𝗋-1[t] : Dom 𝗋-1[t]  Cod 𝗋-1[t]»"
        using I arr_dom_iff_arr [of "t"] by force
      assume I1: "Arr t  «t : Dom t  Cod t»"
      assume I2: "Arr u  «u : Dom u  Cod u»"
      assume I3: "Arr v  «v : Dom v  Cod v»"
      show "Arr 𝖺[t, u, v]  «𝖺[t, u, v] : Dom 𝖺[t, u, v]  Cod 𝖺[t, u, v]»"
      proof -
        assume 1: "Arr 𝖺[t, u, v]"
        have t: "«t : dom t  cod t»" using 1 I1 by auto
        have u: "«u : dom u  cod u»" using 1 I2 by auto
        have v: "«v : dom v  cod v»" using 1 I3 by auto
        have "𝖺[t, u, v] = (t  u  v)  𝖺[dom t, dom u, dom v]"
          using t u v α_simp [of "t" "u" "v"] by auto
        moreover have "«(t  u  v)  𝖺[dom t, dom u, dom v] :
                         (dom t  dom u)  dom v  cod t  cod u  cod v»"
          using t u v by (elim in_homE, auto)
        moreover have "Dom t = dom t  Dom u = dom u  Dom v = dom v 
                       Cod t = cod t  Cod u = cod u  Cod v = cod v"
          using 1 I1 I2 I3 by auto
        ultimately show "«𝖺[t, u, v] : Dom 𝖺[t, u, v]  Cod 𝖺[t, u, v]»"
          by simp
      qed
      show "Arr 𝖺-1[t, u, v]   «𝖺-1[t, u, v] : Dom 𝖺-1[t, u, v]  Cod 𝖺-1[t, u, v]»"
       proof -
        assume 1: "Arr 𝖺-1[t, u, v]"
        have t: "«t : dom t  cod t»" using 1 I1 by auto
        have u: "«u : dom u  cod u»" using 1 I2 by auto
        have v: "«v : dom v  cod v»" using 1 I3 by auto
        have "𝖺-1[t, u, v] = ((t  u)  v)  𝖺-1[dom t, dom u, dom v]"
          using 1 I1 I2 I3 α'_simp [of "t" "u" "v"] by auto
        moreover have "«((t  u)  v)  𝖺-1[dom t, dom u, dom v] :
                          dom t  dom u  dom v  (cod t  cod u)  cod v»"
          using t u v assoc'_in_hom [of "dom t" "dom u" "dom v"]
          by (elim in_homE, auto)
        moreover have "Dom t = dom t  Dom u = dom u  Dom v = dom v 
                       Cod t = cod t  Cod u = cod u  Cod v = cod v"
          using 1 I1 I2 I3 by auto
        ultimately show " «𝖺-1[t, u, v] : Dom 𝖺-1[t, u, v]  Cod 𝖺-1[t, u, v]»"
          by simp
      qed
    qed

    lemma arr_eval [simp]:
    assumes "Arr f"
    shows "arr f"
      using assms eval_in_hom by auto

    lemma dom_eval [simp]:
    assumes "Arr f"
    shows "dom f = Dom f"
      using assms eval_in_hom by auto
      
    lemma cod_eval [simp]:
    assumes "Arr f"
    shows "cod f = Cod f"
      using assms eval_in_hom by auto
      
    lemma eval_Prim [simp]:
    assumes "C.arr f"
    shows "f = V f"
      by simp

    lemma eval_Tensor [simp]:
    assumes "Arr t" and "Arr u"
    shows "t  u = t  u"
      using assms eval_in_hom by auto

    lemma eval_Comp [simp]:
    assumes "Arr t" and "Arr u" and "Dom t = Cod u"
    shows " t  u = t  u"
      using assms by simp

    lemma eval_Lunit [simp]:
    assumes "Arr t"
    shows "𝗅[t] = 𝗅[Cod t]  (  t)"
      using assms lunit_naturality [of "t"] by simp

    lemma eval_Lunit' [simp]:
    assumes "Arr t"
    shows "𝗅-1[t] = 𝗅-1[Cod t]  t"
      using assms lunit'_naturality [of "t"] 𝔩'.map_simp [of "t"] 𝔩_ide_simp
            Arr_implies_Ide_Cod
      by simp

    lemma eval_Runit [simp]:
    assumes "Arr t"
    shows "𝗋[t] = 𝗋[Cod t]  (t  )"
      using assms runit_naturality [of "t"] by simp

    lemma eval_Runit' [simp]:
    assumes "Arr t"
    shows "𝗋-1[t] = 𝗋-1[Cod t]  t"
      using assms runit'_naturality [of "t"] ρ'.map_simp [of "t"] ρ_ide_simp
            Arr_implies_Ide_Cod
      by simp

    lemma eval_Assoc [simp]:
    assumes "Arr t" and "Arr u" and "Arr v"
    shows "𝖺[t, u, v] = 𝖺[cod t, cod u, cod v]  ((t  u)  v)"
      using assms α.is_natural_2 [of "(t, u, v)"] by auto

    lemma eval_Assoc' [simp]:
    assumes "Arr t" and "Arr u" and "Arr v"
    shows "𝖺-1[t, u, v] = 𝖺-1[cod t, cod u, cod v]  (t  u  v)"
      using assms α'_simp [of "t" "u" "v"] assoc'_naturality [of "t" "u" "v"]
      by simp

    text‹
      The following are conveniences for the case of identity arguments
      to avoid having to get rid of the extra identities that are introduced by
      the general formulas above.
›

    lemma eval_Lunit_Ide [simp]:
    assumes "Ide a"
    shows "𝗅[a] = 𝗅[a]"
      using assms comp_cod_arr by simp

    lemma eval_Lunit'_Ide [simp]:
    assumes "Ide a"
    shows "𝗅-1[a] = 𝗅-1[a]"
      using assms comp_cod_arr by simp

    lemma eval_Runit_Ide [simp]:
    assumes "Ide a"
    shows "𝗋[a] = 𝗋[a]"
      using assms comp_cod_arr by simp

    lemma eval_Runit'_Ide [simp]:
    assumes "Ide a"
    shows "𝗋-1[a] = 𝗋-1[a]"
      using assms comp_cod_arr by simp

    lemma eval_Assoc_Ide [simp]:
    assumes "Ide a" and "Ide b" and "Ide c"
    shows "𝖺[a, b, c] = 𝖺[a, b, c]"
      using assms by simp

    lemma eval_Assoc'_Ide [simp]:
    assumes "Ide a" and "Ide b" and "Ide c"
    shows "𝖺-1[a, b, c] = 𝖺-1[a, b, c]"
      using assms α'_ide_simp by simp

    text‹
      Canonical arrows evaluate to isomorphisms in D›, and formal inverses evaluate
      to inverses in D›.
›

    lemma iso_eval_Can:
    shows "Can t  iso t"
      using Can_implies_Arr 𝔩'.preserves_iso ρ'.preserves_iso α.preserves_iso α'.preserves_iso
            Arr_implies_Ide_Dom
      by (induct t) auto

    lemma eval_Inv_Can:
    shows "Can t  Inv t = inv t"
      apply (induct t)
      using iso_eval_Can inv_comp Can_implies_Arr
               apply auto[4]
    proof -
      fix t
      assume I: "Can t  Inv t = inv t"
      show "Can 𝗅[t]  Inv 𝗅[t] = inv 𝗅[t]"
        using I 𝔩'.is_natural_2 [of "inv t"] iso_eval_Can 𝔩_ide_simp iso_is_arr
             comp_cod_arr inv_comp
        by simp
      show "Can 𝗋[t]  Inv 𝗋[t] = inv 𝗋[t]"
        using I ρ'.is_natural_2 [of "inv t"] iso_eval_Can ρ_ide_simp iso_is_arr
              comp_cod_arr inv_comp
        by simp
      show "Can 𝗅-1[t]  Inv 𝗅-1[t] = inv 𝗅-1[t]"
      proof -
        assume t: "Can 𝗅-1[t]"
        hence 1: "iso t" using iso_eval_Can by simp
        have "inv 𝗅-1[t] = inv (𝔩' t)"
          using t by simp
        also have "... = inv (𝗅-1[cod t]  t)"
          using 1 𝔩'.is_natural_2 [of "t"] 𝔩'_ide_simp iso_is_arr by auto
        also have "... = Inv 𝗅-1[t]"
          using t I 1 iso_is_arr inv_comp by auto
        finally show ?thesis by simp
      qed
      show "Can 𝗋-1[t]  Inv 𝗋-1[t] = inv 𝗋-1[t]"
      proof -
        assume t: "Can 𝗋-1[t]"
        hence 1: "iso t" using iso_eval_Can by simp
        have "inv 𝗋-1[t] = inv (ρ' t)"
          using t by simp
        also have "... = inv (𝗋-1[cod t]  t)"
          using 1 ρ'.is_natural_2 [of "t"] ρ'_ide_simp iso_is_arr by auto
        also have "... = Inv 𝗋-1[t]"
          using t I 1 iso_is_arr inv_comp by auto
        finally show ?thesis by simp
      qed
      next
      fix t u v
      assume I1: "Can t  Inv t = inv t"
      assume I2: "Can u  Inv u = inv u"
      assume I3: "Can v  Inv v = inv v"
      show "Can 𝖺[t, u, v]  Inv 𝖺[t, u, v] = inv 𝖺[t, u, v]"
      proof -
        assume tuv: "Can 𝖺[t, u, v]"
        have t: "iso t" using tuv iso_eval_Can by auto
        have u: "iso u" using tuv iso_eval_Can by auto
        have v: "iso v" using tuv iso_eval_Can by auto
        have "Inv 𝖺[t, u, v] = α' (inv t, inv u, inv v)"
          using tuv I1 I2 I3 by simp
        also have "... = inv (𝖺[cod t, cod u, cod v]  ((t  u)  v))"
          using t u v α'_simp iso_is_arr inv_comp by auto
        also have "... = inv ((t  u  v)  𝖺[dom t, dom u, dom v])"
          using t u v iso_is_arr assoc_naturality by simp
        also have "... = inv 𝖺[t, u, v]"
          using t u v iso_is_arr α_simp [of "t" "u" "v"] by simp
        finally show ?thesis by simp
      qed
      show "Can 𝖺-1[t, u, v]  Inv 𝖺-1[t, u, v] = inv 𝖺-1[t, u, v]"
      proof -
        assume tuv: "Can 𝖺-1[t, u, v]"
        have t: "iso t" using tuv iso_eval_Can by auto
        have u: "iso u" using tuv iso_eval_Can by auto
        have v: "iso v" using tuv iso_eval_Can by auto
        have "Inv 𝖺-1[t, u, v] = α (inv t, inv u, inv v)"
          using tuv I1 I2 I3 by simp
        also have "... = (inv t  inv u  inv v)  𝖺[cod t, cod u, cod v]"
          using t u v iso_is_arr α_simp [of "inv t" "inv u" "inv v"] by simp
        also have "... = inv (𝖺-1[cod t, cod u, cod v]  (t  u  v))"
          using t u v iso_is_arr inv_comp by auto
        also have "... = inv (((t  u)  v)  𝖺-1[dom t, dom u, dom v])"
          using t u v iso_is_arr assoc'_naturality by simp
        also have "... = inv 𝖺-1[t, u, v]"
          using t u v iso_is_arr α'_simp by auto
        finally show ?thesis by blast
      qed
    qed

    text‹
      The operation  evaluates to composition in D›.
›

    lemma eval_CompDiag:
    assumes "Diag t" and "Diag u" and "Seq t u"
    shows "t  u = t  u"
    proof -
      have "u.  Diag t; Diag u; Seq t u   t  u = t  u"
        using eval_in_hom comp_cod_arr
      proof (induct t, simp_all)
        fix u f
        assume u: "Diag u"
        assume f: "C.arr f"
        assume 1: "Arr u  C.dom f = Cod u"
        show "f  u = V f  u"
          using f u 1 as_nat_trans.preserves_comp_2 by (cases u; simp)
        next
        fix u v w
        assume I1: "u.  Diag v; Diag u; Arr u  Dom v = Cod u  
                         v  u = v  u"
        assume I2: "u.  Diag w; Diag u; Arr u  Dom w = Cod u  
                         w  u = w  u"
        assume vw: "Diag (Tensor v w)"
        have v: "Diag v  v = Prim (un_Prim v)"
          using vw by (simp add: Diag_TensorE)
        have w: "Diag w"
          using vw by (simp add: Diag_TensorE)
        assume u: "Diag u"
        assume 1: "Arr v  Arr w  Arr u  Dom v  Dom w = Cod u"
        show "(v  w)  u = (v  w)  u"
          using u 1 eval_in_hom CompDiag_in_Hom
        proof (cases u, simp_all)
          fix x y
          assume 3: "u = x  y"
          assume 4: "Arr v  Arr w  Dom v = Cod x  Dom w = Cod y"
          have x: "Diag x"
            using u 1 3 Diag_TensorE [of x y] by simp
          have y: "Diag y"
            using u x 1 3 Diag_TensorE [of x y] by simp
          show "v  x  w  y = (v  w)  (x  y)"
            using v w x y 4 I1 I2 CompDiag_in_Hom eval_in_hom Diag_implies_Arr interchange
            by auto
        qed
      qed
      thus ?thesis using assms by blast
    qed

    text‹
      For identity terms @{term a} and @{term b}, the reduction @{term "(a  b)"}
      factors (under evaluation in D›) into the parallel reduction @{term "a  b"},
      followed by a reduction of its codomain @{term "a  b"}.
›

    lemma eval_red_Tensor:
    assumes "Ide a" and "Ide b"
    shows "(a  b) = a  b  (a  b)"
    proof -
      have "Diag (a  b)  ?thesis"
        using assms Can_red2 Ide_implies_Arr red_Diag
              Diagonalize_Diag red2_Diag Can_implies_Arr iso_eval_Can iso_is_arr
        apply simp
        using Diag_TensorE eval_Tensor Diagonalize_Diag Diag_implies_Arr red_Diag
              tensor_preserves_ide ide_eval_Ide dom_eval comp_arr_dom
        by metis
      moreover have "¬ Diag (a  b)  ?thesis"
        using assms Can_red2 by (simp add: Can_red(1) iso_eval_Can)
      ultimately show ?thesis by blast
    qed

    lemma eval_red2_Diag_Unity:
    assumes "Ide a" and "Diag a"
    shows "a   = 𝗋[a]"
      using assms tensor_preserves_ide ρ_ide_simp unitor_coincidence unit_in_hom comp_cod_arr
      by (cases a, auto)

    text‹
      Define a formal arrow t to be ``coherent'' if the square formed by @{term t}, @{term "t"}
      and the reductions @{term "Dom t"} and @{term "Cod t"} commutes under evaluation
      in D›.  We will show that all formal arrows are coherent.
      Since the diagonalizations of canonical arrows are identities, a corollary is that parallel
      canonical arrows have equal evaluations.
›

    abbreviation coherent
    where "coherent t  Cod t  t = t  Dom t"

    text‹
      Diagonal arrows are coherent, since for such arrows @{term t} the reductions
      @{term "Dom t"} and @{term "Cod t"} are identities.
›

    lemma Diag_implies_coherent:
    assumes "Diag t"
    shows "coherent t"
      using assms Diag_implies_Arr Arr_implies_Ide_Dom Arr_implies_Ide_Cod
            Dom_preserves_Diag Cod_preserves_Diag Diagonalize_Diag red_Diag
            comp_arr_dom comp_cod_arr
      by simp

    text‹
      The evaluation of a coherent arrow @{term t} has a canonical factorization in D›
      into the evaluations of a reduction @{term "Dom t"}, diagonalization @{term "t"},
      and inverse reduction @{term "Inv (Cod t)"}.
      This will later allow us to use the term @{term "Inv (Cod t)  t  Dom t"}
      as a normal form for @{term t}.
›

    lemma canonical_factorization:
    assumes "Arr t"
    shows "coherent t  t = inv Cod t  t  Dom t"
    proof
      assume 1: "coherent t"
      have "inv Cod t  t  Dom t = inv Cod t  Cod t  t"
        using 1 by simp
      also have "... = (inv Cod t  Cod t)  t"
        using comp_assoc by simp
      also have "... = t"
        using assms 1 red_in_Hom inv_in_hom Arr_implies_Ide_Cod Can_red iso_eval_Can
              comp_cod_arr Ide_in_Hom inv_is_inverse
        by (simp add: comp_inv_arr)
      finally show "t = inv Cod t  t  Dom t" by simp
      next
      assume 1: "t = inv Cod t  t  Dom t"
      hence "Cod t  t = Cod t  inv Cod t  t  Dom t" by simp
      also have "... = (Cod t  inv Cod t)  t  Dom t"
        using comp_assoc by simp
      also have "... = t  Dom t"
        using assms 1 red_in_Hom Arr_implies_Ide_Cod Can_red iso_eval_Can inv_is_inverse
              Diagonalize_in_Hom comp_arr_inv comp_cod_arr Arr_implies_Ide_Dom Diagonalize_in_Hom
        by auto
      finally show "coherent t" by blast
    qed

    text‹
      A canonical arrow is coherent if and only if its formal inverse is.
›

    lemma Can_implies_coherent_iff_coherent_Inv:
    assumes "Can t"
    shows "coherent t  coherent (Inv t)"
    proof
      have 1: "t. Can t  coherent t  coherent (Inv t)"
      proof -
        fix t
        assume "Can t"
        hence t: "Can t  Arr t  Ide (Dom t)  Ide (Cod t) 
                  arr t  iso t  inverse_arrows t (inv t) 
                  Can t  Arr t  arr t  iso t  t  Hom Dom t Cod t 
                  inverse_arrows t (inv t)  Inv t  Hom (Cod t) (Dom t)"
          using assms Can_implies_Arr Arr_implies_Ide_Dom Arr_implies_Ide_Cod iso_eval_Can
                inv_is_inverse Diagonalize_in_Hom Diagonalize_preserves_Can Inv_in_Hom
          by simp
        assume coh: "coherent t"
        have "Cod (Inv t)  Inv t = (inv t  t)  Cod (Inv t)  Inv t"
          using t red_in_Hom comp_cod_arr comp_inv_arr
          by (simp add: canonical_factorization coh Diagonalize_preserves_Can
              Can t inv_is_inverse)
        also have "... = inv t  (Cod t  t)  inv t"
          using t eval_Inv_Can coh comp_assoc by auto
        also have "... = Inv t  Dom (Inv t)"
          using t Diagonalize_Inv eval_Inv_Can comp_arr_inv red_in_Hom comp_arr_dom comp_assoc
          by auto
        finally show "coherent (Inv t)" by blast
      qed
      show "coherent t  coherent (Inv t)" using assms 1 by simp
      show "coherent (Inv t)  coherent t"
      proof -
        assume "coherent (Inv t)"
        hence "coherent (Inv (Inv t))"
          using assms 1 Inv_preserves_Can by blast
        thus ?thesis using assms by simp
      qed
    qed

    text‹
      Some special cases of coherence are readily dispatched.
›

    lemma coherent_Unity:
    shows "coherent "
      by simp

    lemma coherent_Prim:
    assumes "Arr f"
    shows "coherent f"
      using assms by simp

    lemma coherent_Lunit_Ide:
    assumes "Ide a"
    shows "coherent 𝗅[a]"
    proof -
      have a: "Ide a  Arr a  Dom a = a  Cod a = a 
               ide a  ide a  a  hom a a"
        using assms Ide_implies_Arr Ide_in_Hom Diagonalize_preserves_Ide red_in_Hom by auto
      thus ?thesis
        using a lunit_naturality [of "a"] comp_cod_arr by auto
    qed
      
    lemma coherent_Runit_Ide:
    assumes "Ide a"
    shows "coherent 𝗋[a]"
    proof -
      have a: "Ide a  Arr a  Dom a = a  Cod a = a 
               ide a  ide a  a  hom a a"
        using assms Ide_implies_Arr Ide_in_Hom Diagonalize_preserves_Ide red_in_Hom
        by auto
      have "Cod 𝗋[a]  𝗋[a] = a  𝗋[a]"
        using a runit_in_hom comp_cod_arr by simp
      also have "... = 𝗋[a]  (a  )"
        using a eval_Runit runit_naturality [of "red a"] by auto
      also have "... = 𝗋[a]  Dom 𝗋[a]"
      proof -
        have "¬ Diag (a  )" by (cases a; simp)
        thus ?thesis
          using a comp_cod_arr red2_in_Hom eval_red2_Diag_Unity Diag_Diagonalize
                Diagonalize_preserves_Ide
          by auto
      qed
      finally show ?thesis by blast
    qed

    lemma coherent_Lunit'_Ide:
    assumes "Ide a"
    shows "coherent 𝗅-1[a]"
      using assms Ide_implies_Can coherent_Lunit_Ide
            Can_implies_coherent_iff_coherent_Inv [of "Lunit a"] by simp

    lemma coherent_Runit'_Ide:
    assumes "Ide a"
    shows "coherent 𝗋-1[a]"
      using assms Ide_implies_Can coherent_Runit_Ide
            Can_implies_coherent_iff_coherent_Inv [of "Runit a"] by simp

    text‹
      To go further, we need the next result, which is in some sense the crux of coherence:
      For diagonal identities @{term a}, @{term b}, and @{term c},
      the reduction @{term "((a  b)  c)  ((a  b)  c)"} from @{term "(a  b)  c"}
      that first reduces the subterm @{term "a  b"} and then reduces the result,
      is equivalent under evaluation in D› to the reduction that first
      applies the associator @{term "𝖺[a, b, c]"} and then applies the reduction
      @{term "(a  (b  c))  (a  (b  c))"} from @{term "a  (b  c)"}.
      The triangle and pentagon axioms are used in the proof.
›

    lemma coherence_key_fact:
    assumes "Ide a  Diag a" and "Ide b  Diag b" and "Ide c  Diag c"
    shows "(a  b)  c  (a  b  c)
             = (a  (b  c)  (a  b  c))  𝖺[a, b, c]"
    proof -
      have "b =   ?thesis"
        using assms not_is_Tensor_TensorDiagE eval_red2_Diag_Unity triangle
              comp_cod_arr comp_assoc
        by simp
        text ‹The triangle is used!›
      moreover have "c =   ?thesis"
        using assms TensorDiag_preserves_Diag TensorDiag_preserves_Ide
              not_is_Tensor_TensorDiagE eval_red2_Diag_Unity
              red2_in_Hom runit_tensor runit_naturality [of "a  b"] comp_assoc
        by simp
      moreover have " b  ; c     ?thesis"
      proof -
        assume b': "b  "
        hence b: "Ide b  Diag b  Arr b  b   
                  ide b  arr b  b = b  b = b  Dom b = b  Cod b = b"
          using assms Diagonalize_preserves_Ide Ide_in_Hom by simp
        assume c': "c  "
        hence c: "Ide c  Diag c  Arr c  c   
                  ide c  arr c  c = c  c = c  Dom c = c  Cod c = c"
          using assms Diagonalize_preserves_Ide Ide_in_Hom by simp
        have "a. Ide a  Diag a 
                   (a  b)  c  (a  b  c)
                      = (a  (b  c)  (a  b  c))  𝖺[a, b, c]"
        proof -
          fix a :: "'c term"
          show "Ide a  Diag a 
                (a  b)  c  (a  b  c)
                   = (a  (b  c)  (a  b  c))  𝖺[a, b, c]"
            apply (induct a)
            using b c TensorDiag_in_Hom apply simp_all
          proof -
            show "b  c  (b  𝗅[b]  c)
                    = ((b  c  𝗅[b  c])  (  b  c))  𝖺[, b, c]"
            proof -
              have "b  c  (𝗅[b  c]  (  b  c))  𝖺[, b, c] =
                    b  c  (b  c  𝗅[b  c])   𝖺[, b, c]"
                using b c red2_in_Hom lunit_naturality [of "b  c"] by simp
              thus ?thesis
                using b c red2_in_Hom lunit_tensor comp_arr_dom comp_cod_arr comp_assoc by simp
            qed
            show "f. C.ide f  C.arr f 
                       (f  b)  c  (f  b  c)
                         = (f  (b  c)  (V f  b  c))  𝖺[V f, b, c]"
            proof -
              fix f
              assume f: "C.ide f  C.arr f"
              show "(f  b)  c  (f  b  c)
                      = (f  (b  c)  (V f  b  c))  𝖺[V f, b, c]"
              proof -
                have "(f  b)  c  (f  b  c)
                        = ((V f  b  c)  (V f  b  c)  𝖺[V f, b, c]) 
                          ((V f  b)  c)"
                proof -
                  have "f  b = V f  b"
                    using assms f b c red2_Diag by simp
                  moreover have "f  b  c = V f  b  c"
                  proof -
                    have "is_Tensor (b  c)"
                      using assms b c not_is_Tensor_TensorDiagE by blast
                    thus ?thesis
                      using assms f b c red2_Diag TensorDiag_preserves_Diag(1)
                      by (cases "b  c"; simp)
                  qed
                  ultimately show ?thesis
                    using assms b c by (cases c, simp_all)
                qed
                also have "... = ((V f  b  c)  (V f  b  c))  𝖺[V f, b, c]"
                  using b c f TensorDiag_in_Hom red2_in_Hom comp_arr_dom comp_cod_arr
                  by simp
                also have "... = (f  (b  c)  (V f  b  c))  𝖺[V f, b, c]"
                    using b c f Ide_implies_Arr TensorDiag_preserves_Ide not_is_Tensor_TensorDiagE
                    by (cases "b  c", simp_all; blast)
                finally show ?thesis by blast
              qed
            qed
            fix d e
            assume I: "Diag e  (e  b)  c  (e  b  c)
                                    = (e  b  c  (e  b  c))  𝖺[e, b, c]"
            assume de: "Ide d  Ide e  Diag (d  e)"
            show "((d  e)  b)  c  ((d  e)  b  c)
                    = ((d  e)  (b  c)  ((d  e)  b  c))  𝖺[d  e, b, c]"
            proof -
              let ?f = "un_Prim d"
              have "is_Prim d"
                using de by (cases d, simp_all)
              hence "d = ?f  C.ide ?f"
                using de by (cases d, simp_all)
              hence d: "Ide d  Arr d  Dom d = d  Cod d = d  Diag d 
                        d = ?f  C.ide ?f  ide d  arr d"
                using de ide_eval_Ide Ide_implies_Arr Diag_Diagonalize(1) Ide_in_Hom
                      Diag_TensorE [of d e]
                by simp
              have "Diag e  e  "
                using de Diag_TensorE by metis
              hence e: "Ide e  Arr e  Dom e = e  Cod e = e  Diag e 
                        e    ide e  arr e"
                using de Ide_in_Hom by simp
              have 1: "is_Tensor (e  b)  is_Tensor (b  c)  is_Tensor (e  (b  c))"
                using b c e de not_is_Tensor_TensorDiagE TensorDiag_preserves_Diag
                      not_is_Tensor_TensorDiagE [of e "b  c"]
                by auto
              have "((d  e)  b)  c  ((d  e)  b  c)
                      = ((d  (e  b)  c)  (d  (e  b)  c) 
                         𝖺[d, e  b, c]) 
                        ((d  e  b)  (d  e  b)  𝖺[d, e, b]  c)"
              proof -
                have "((d  e)  b)  c
                         = (d  (e  b)  c)  (d  (e  b)  c) 
                           𝖺[d, e  b, c]"
                proof -
                  have "((d  e)  b)  c = (d  (e  b))  c"
                    using b c d e de 1 TensorDiag_Diag TensorDiag_preserves_Diag TensorDiag_assoc
                          TensorDiag_Prim not_is_Tensor_Unity
                    by metis
                  also have "... = (d  (e  b  c))  (d  ((e  b)  c)) 
                                   𝖺[d, e  b, c]"
                    using c d 1 by (cases c) simp_all
                  also have "... = (d  ((e  b)  c))  (d  ((e  b)  c)) 
                                   𝖺[d, e  b, c]"
                    by (metis 1 Diagonalize_Diag TensorDiag_assoc TensorDiag_preserves_Diag(1)
                              b c d e is_Tensor_def red2.simps(4))
                  finally show ?thesis
                    using b c d e TensorDiag_in_Hom red2_in_Hom TensorDiag_preserves_Diag
                          TensorDiag_preserves_Ide
                    by simp
                qed
                moreover have "(d  e)  b
                                 = (d  e  b)  (d  e  b)  𝖺[d, e, b]"
                proof -
                  have "(d  e)  b = (d  (e  b))  (d  (e  b))  𝖺[d, e, b]"
                      using b c d e de 1 TensorDiag_Prim Diagonalize_Diag
                      by (cases b) simp_all
                  also have "... = (d  (e  b))  (d  (e  b))  𝖺[d, e, b]"
                    using b d e 1 TensorDiag_preserves_Diag red2_Diag
                    by (metis Diag.simps(3) de term.disc(12))
                  finally have "(d  e)  b = (d  (e  b))  (d  (e  b))  𝖺[d, e, b]"
                    by simp
                  thus ?thesis using b d e eval_in_hom TensorDiag_in_Hom red2_in_Hom by simp
                qed
                ultimately show ?thesis by argo
              qed
              also have "... = (d  (e  b)  c)  𝖺[d, e  b, c] 
                               ((d  e  b)  c)  (𝖺[d, e, b]  c)"
                using b c d e red2_in_Hom TensorDiag_preserves_Ide
                      TensorDiag_preserves_Diag interchange comp_cod_arr comp_assoc
                by simp
              also have "... = (d  (e  b)  c)  (d  (e  b  c)) 
                               𝖺[d, e  b, c]  (𝖺[d, e, b]  c)"
                using b c d e TensorDiag_in_Hom red2_in_Hom TensorDiag_preserves_Ide
                      TensorDiag_preserves_Diag assoc_naturality [of "d" "e  b" "c"]
                      comp_permute [of "𝖺[d, e  b, c]" "(d  e  b)  c"
                                       "d  (e  b  c)" "𝖺[d, e  b, c]"]
                by simp
              also have "... = (d  (e  b)  c  (e  b  c)) 
                               𝖺[d, e  b, c]  (𝖺[d, e, b]  c)"
                using b c d e TensorDiag_in_Hom red2_in_Hom TensorDiag_preserves_Ide
                      TensorDiag_preserves_Diag interchange
                      comp_reduce [of "d  (e  b)  c"
                                      "d  (e  b  c)"
                                      "d  (e  b)  c  (e  b  c)"
                                      "𝖺[d, e  b, c]  (𝖺[d, e, b]  c)"]
                 by simp
              also have "... = (((d  e  (b  c))  (d  e  b  c)) 
                                (d  𝖺[e, b, c])) 
                               𝖺[d, e  b, c]  (𝖺[d, e, b]  c)"
                using b c d e I TensorDiag_in_Hom red2_in_Hom TensorDiag_preserves_Ide
                      TensorDiag_preserves_Diag interchange
                by simp
              also have "... = ((d  e  (b  c))  (d  (e  b  c))) 
                                 𝖺[d, e, b  c]  𝖺[d  e, b, c]"
                using b c d e comp_assoc red2_in_Hom TensorDiag_in_Hom ide_eval_Ide
                      TensorDiag_preserves_Diag tensor_preserves_ide TensorDiag_preserves_Ide
                      pentagon
                by simp
              text ‹The pentagon is used!›
              also have "... = (((d  e  b  c)  (d  e  b  c) 
                                 𝖺[d, e, b  c])  ((d  e)  b  c)) 
                               𝖺[d  e, b, c]"
                using b c d e red2_in_Hom TensorDiag_preserves_Ide TensorDiag_preserves_Diag
                      assoc_naturality [of "d" "e" "b  c"] comp_cod_arr comp_assoc
                by simp
              also have "... = ((d  e)  (b  c)  ((d  e)  b  c)) 
                               𝖺[d  e, b, c]"
              proof -
                have "(d  e)  (b  c)
                           = (d  e  (b  c))  (d  e  (b  c)) 
                              𝖺[d, e, b  c]"
                proof -
                  have "(d  e)  (b  c)
                          = (d  (e  b  c))  (d  (e  (b  c)))  𝖺[d, e, b  c]"
                    using b c e not_is_Tensor_TensorDiagE
                    by (cases "b  c") auto
                  also have "... = (d  (e  (b  c)))  (d  (e  (b  c))) 
                                   𝖺[d, e, b  c]"
                    using b c d e 1 TensorDiag_preserves_Diag Diagonalize_Diag by simp
                  also have "... = (d  (e  (b  c)))  (d  (e  (b  c))) 
                                   𝖺[d, e, b  c]"
                    using b c d e 1 TensorDiag_preserves_Diag(1) red2_Diag
                    by (metis Diag.simps(3) de not_is_Tensor_Unity)
                  finally have "(d  e)  (b  c)
                                  = (d  (e  (b  c)))  (d  (e  (b  c))) 
                                    𝖺[d, e, b  c]"
                    by blast
                  thus ?thesis
                    using b c d e red2_in_Hom TensorDiag_in_Hom TensorDiag_preserves_Diag
                          TensorDiag_preserves_Ide
                    by simp
                qed
                thus ?thesis using d e b c by simp
              qed
              finally show ?thesis by simp
            qed
          qed
        qed
        thus ?thesis using assms(1) by blast
      qed
      ultimately show ?thesis by blast
    qed

    lemma coherent_Assoc_Ide:
    assumes "Ide a" and "Ide b" and "Ide c"
    shows "coherent 𝖺[a, b, c]"
    proof -
      have a: "Ide a  Arr a  Dom a = a  Cod a = a 
               ide a  ide a  «a : a  a»"
        using assms Ide_implies_Arr Ide_in_Hom Diagonalize_preserves_Ide red_in_Hom by auto
      have b: "Ide b  Arr b  Dom b = b  Cod b = b 
               ide b  ide b  «b : b  b»"
        using assms Ide_implies_Arr Ide_in_Hom Diagonalize_preserves_Ide red_in_Hom by auto
      have c: "Ide c  Arr c  Dom c = c  Cod c = c 
               ide c  ide c  «c : c  c»"
        using assms Ide_implies_Arr Ide_in_Hom Diagonalize_preserves_Ide red_in_Hom by auto
      have "Cod 𝖺[a, b, c]  𝖺[a, b, c]
              = (a  (b  c)  (a  (b  c)) 
                 (a  b  c))  𝖺[a, b, c]"
        using a b c red_in_Hom red2_in_Hom Diagonalize_in_Hom Diag_Diagonalize
              Diagonalize_preserves_Ide interchange Ide_in_Hom eval_red_Tensor
              comp_cod_arr [of "a"]
        by simp
      also have "... = ((a  (b  c)  (a  b  c)) 
                        𝖺[a, b, c])  ((a  b)  c)"
        using a b c red_in_Hom Diag_Diagonalize TensorDiag_preserves_Diag
               assoc_naturality [of "a" "b" "c"] comp_assoc
         by simp
      also have "... = ((a  b)  c  (a  b  c)) 
                       ((a  b)  c)"
        using a b c Diag_Diagonalize Diagonalize_preserves_Ide coherence_key_fact by simp
      also have "... = 𝖺[a, b, c]  Dom 𝖺[a, b, c]"
        using a b c red_in_Hom red2_in_Hom TensorDiag_preserves_Diag
              Diagonalize_preserves_Ide TensorDiag_preserves_Ide Diag_Diagonalize interchange
              eval_red_Tensor TensorDiag_assoc comp_cod_arr [of "c"]
              comp_cod_arr [of "(a  b)  c  (a  b  (a  b)  c)"]
              comp_assoc
        by simp
      finally show ?thesis by blast
    qed

    lemma coherent_Assoc'_Ide:
    assumes "Ide a" and "Ide b" and "Ide c"
    shows "coherent 𝖺-1[a, b, c]"
    proof -
      have "Can 𝖺[a, b, c]" using assms Ide_implies_Can by simp
      moreover have "𝖺-1[a, b, c] = Inv 𝖺[a, b, c]"
        using assms Inv_Ide by simp
      ultimately show ?thesis
        using assms Ide_implies_Can coherent_Assoc_Ide Inv_Ide
              Can_implies_coherent_iff_coherent_Inv
        by metis
    qed

    text‹
      The next lemma implies coherence for the special case of a term that is the tensor
      of two diagonal arrows.
›

    lemma eval_red2_naturality:
    assumes "Diag t" and "Diag u"
    shows "Cod t  Cod u  (t  u) = t  u  Dom t  Dom u"
    proof -
      have *: "t u. Diag (t  u)  arr t  arr u"
        using Diag_implies_Arr by force
      have "t =   ?thesis"
        using assms Diag_implies_Arr lunit_naturality [of "u"]
              Arr_implies_Ide_Dom Arr_implies_Ide_Cod comp_cod_arr
        by simp
      moreover have "t    u =   ?thesis"
        using assms Arr_implies_Ide_Dom Arr_implies_Ide_Cod
              Diag_implies_Arr Dom_preserves_Diag Cod_preserves_Diag
              eval_red2_Diag_Unity runit_naturality [of "t"]
        by simp
      moreover have "t    u    ?thesis"
        using assms * Arr_implies_Ide_Dom Arr_implies_Ide_Cod
              Diag_implies_Arr Dom_preserves_Diag Cod_preserves_Diag
        apply (induct t, simp_all)
      proof -
        fix f
        assume f: "C.arr f"
        assume "u  "
        hence u: "u   
                  Diag u  Diag (Dom u)  Diag (Cod u)  Ide (Dom u)  Ide (Cod u) 
                  arr u  arr Dom u  arr Cod u  ide Dom u  ide Cod u"
          using assms(2) Diag_implies_Arr Dom_preserves_Diag Cod_preserves_Diag
                Arr_implies_Ide_Dom Arr_implies_Ide_Cod
          by simp
        hence 1: "Dom u    Cod u  " using u by (cases u, simp_all)
        show "C.cod f  Cod u  (V f  u) = (V f  u)  C.dom f  Dom u"
          using f u 1 Diag_implies_Arr red2_Diag comp_arr_dom comp_cod_arr by simp
        next
        fix v w
        assume I2: " w  Unity; Diag w  
                      Cod w  Cod u  (w  u) = w  u  Dom w  Dom u"
        assume "u  "
        hence u: "u    Arr u  Arr (Dom u)  Arr (Cod u) 
                  Diag u  Diag (Dom u)  Diag (Cod u)  Ide (Dom u)  Ide (Cod u) 
                  arr u  arr Dom u  arr Cod u  ide Dom u  ide Cod u"
          using assms(2) Diag_implies_Arr Dom_preserves_Diag Cod_preserves_Diag
                Arr_implies_Ide_Dom Arr_implies_Ide_Cod
          by simp
        assume vw: "Diag (v  w)"
        let ?f = "un_Prim v"
        have "v = ?f  C.arr ?f"
          using vw by (metis Diag_TensorE(1) Diag_TensorE(2))
        hence "Arr v  v = un_Prim v  C.arr ?f  Diag v" by (cases v; simp)
        hence v: "v = ?f  C.arr ?f  Arr v  Ide (Dom v)  Ide (Cod v)  Diag v 
                  Diag (Dom v)  arr v  arr Dom v  arr Cod v 
                  ide Dom v  ide Cod v"
          by (cases v, simp_all)
        have "Diag w  w  "
          using vw v by (metis Diag.simps(3))
        hence w: "w    Arr w  Arr (Dom w)  Arr (Cod w) 
                  Diag w  Diag (Dom w)  Diag (Cod w) 
                  Ide (Dom w)  Ide (Cod w) 
                  arr w  arr Dom w  arr Cod w  ide Dom w  ide Cod w"
          using vw * Diag_implies_Arr Dom_preserves_Diag Cod_preserves_Diag Arr_implies_Ide_Dom
                Arr_implies_Ide_Cod ide_eval_Ide Ide_implies_Arr Ide_in_Hom
          by simp
        show "(Cod v  Cod w)  Cod u  ((v  w)  u)
                = (v  w)  u  (Dom v  Dom w)  Dom u"
        proof -
          have u': "Dom u    Cod u  " using u by (cases u) simp_all
          have w':  "Dom w    Cod w  " using w by (cases w) simp_all
          have D: "Diag (Dom v  (Dom w  Dom u))"
          proof -
            have "Dom w  Dom u  "
              using u u' w w' not_is_Tensor_TensorDiagE by blast
            moreover have "Diag (Dom w  Dom u)"
              using u w TensorDiag_preserves_Diag by simp
            moreover have "Dom v = C.dom ?f"
              using v by (cases v, simp_all)
            ultimately show ?thesis
              using u v w TensorDiag_preserves_Diag by auto
          qed
          have C: "Diag (Cod v  (Cod w  Cod u))"
          proof -
            have "Cod w  Cod u  "
              using u u' w w' not_is_Tensor_TensorDiagE by blast
            moreover have "Diag (Cod w  Cod u)"
              using u w TensorDiag_preserves_Diag by simp
            moreover have "Cod v = C.cod ?f"
              using v by (cases v, simp_all)
            ultimately show ?thesis
              using u v w by (cases "Cod w  Cod u") simp_all
          qed
          have "(Cod v  Cod w)  Cod u  ((v  w)  u)
                  = (Cod v  (Cod w  Cod u)  (Cod v  Cod w  Cod u) 
                    𝖺[Cod v, Cod w, Cod u])  ((v  w)  u)"
          proof -
            have "(Cod v  Cod w)  Cod u
                    = (Cod v  (Cod w  Cod u))  (Cod v  Cod w  Cod u) 
                      𝖺[Cod v, Cod w, Cod u]"
              using u v w by (cases u, simp_all)
            hence "(Cod v  Cod w)  Cod u
                     = Cod v  (Cod w  Cod u)  (Cod v  Cod w  Cod u) 
                       𝖺[Cod v, Cod w, Cod u]"
              using u v w by simp
            thus ?thesis by argo
          qed
          also have "... = ((Cod v  Cod w  Cod u)  (Cod v  Cod w  Cod u) 
                            𝖺[Cod v, Cod w, Cod u])  ((v  w)  u)"
            using u v w C red2_Diag by simp
          also have "... = ((Cod v  Cod w  Cod u)  𝖺[Cod v, Cod w, Cod u]) 
                           ((v  w)  u)"
          proof -
            have "(Cod v  Cod w  Cod u)  (Cod v  Cod w  Cod u)
                     = Cod v  Cod w  Cod u"
              using u v w comp_cod_arr red2_in_Hom by simp
            moreover have
                "seq (Cod v  Cod w  Cod u) (Cod v  Cod w  Cod u)"
              using u v w red2_in_Hom TensorDiag_in_Hom Ide_in_Hom by simp
            moreover have "seq (Cod v  Cod w  Cod u) 𝖺[Cod v, Cod w, Cod u]"
              using u v w red2_in_Hom by simp
            ultimately show ?thesis
              using u v w comp_reduce by presburger
          qed
          also have
            "... = (v  w  u  Dom w  Dom u)  𝖺[Dom v, Dom w, Dom u]"
            using u v w I2 red2_in_Hom TensorDiag_in_Hom interchange comp_reduce
                  assoc_naturality [of "v" "w" "u"] comp_cod_arr comp_assoc
            by simp
          also have "... = (v  w  u)  (Dom v  Dom w  Dom u) 
                           𝖺[Dom v, Dom w, Dom u]"
            using u v w red2_in_Hom TensorDiag_in_Hom interchange comp_reduce comp_arr_dom
            by simp
          also have "... = v  w  u  (Dom v  Dom w  Dom u) 
                           𝖺[Dom v, Dom w, Dom u]"
            using u u' v w not_is_Tensor_TensorDiagE TensorDiag_Prim [of "w  u" ?f]
            by force
          also have "... = v  w  u  Dom v  Dom w  Dom u 
                          (Dom v  Dom w  Dom u)  𝖺[Dom v, Dom w, Dom u]"
          proof -
            have
              "v  w  u  (Dom v  Dom w  Dom u) 
                 𝖺[Dom v, Dom w, Dom u] =
               (v  w  u  Dom v  Dom w  Dom u) 
               (Dom v  Dom w  Dom u)  𝖺[Dom v, Dom w, Dom u]"
              using u v w comp_arr_dom TensorDiag_in_Hom TensorDiag_preserves_Diag by simp
            also have "... = v  w  u  Dom v  Dom w  Dom u 
                            (Dom v  Dom w  Dom u)  𝖺[Dom v, Dom w, Dom u]"
              using comp_assoc by simp
            finally show ?thesis by blast
          qed
          also have "... = (v  w)  u  (Dom v  Dom w)  Dom u"
          proof -
            have
              "(Dom v  Dom w)  Dom u
                     = Dom v  (Dom w  Dom u)  (Dom v  Dom w  Dom u) 
                       𝖺[Dom v, Dom w, Dom u]"
            proof -
              have "(Dom v  Dom w)  Dom u
                       = (Dom v  (Dom w  Dom u))  (Dom v  (Dom w  Dom u)) 
                         𝖺[Dom v, Dom w, Dom u]"
                using u u' v w red2_in_Hom TensorDiag_in_Hom Ide_in_Hom
                by (cases u) auto
              thus ?thesis
                using u v w red2_in_Hom by simp
            qed
            also have
              "... = Dom v  Dom w  Dom u  (Dom v  Dom w  Dom u) 
                             𝖺[Dom v, Dom w, Dom u]"
              using D TensorDiag_Diag red2_Diag by simp
            finally have
              "(Dom v  Dom w)  Dom u
                   = Dom v  Dom w  Dom u  (Dom v  Dom w  Dom u) 
                     𝖺[Dom v, Dom w, Dom u]"
              by blast
            thus ?thesis
              using assms v w TensorDiag_assoc by auto
          qed
          finally show ?thesis
            using vw TensorDiag_Diag by simp
        qed
      qed
      ultimately show ?thesis by blast
    qed

    lemma Tensor_preserves_coherent:
    assumes "Arr t" and "Arr u" and "coherent t" and "coherent u"
    shows "coherent (t  u)"
    proof -
      have t: "Arr t  Ide (Dom t)  Ide (Cod t)  Ide Dom t  Ide Cod t 
               arr t  arr Dom t  ide Dom t  arr Cod t  ide Cod t"
        using assms Arr_implies_Ide_Dom Arr_implies_Ide_Cod Diagonalize_preserves_Ide
        by auto
      have u: "Arr u  Ide (Dom u)  Ide (Cod u)  Ide Dom u  Ide Cod u 
               arr u  arr Dom u  ide Dom u  arr Cod u  ide Cod u"
        using assms Arr_implies_Ide_Dom Arr_implies_Ide_Cod Diagonalize_preserves_Ide
        by auto
      have "Cod (t  u)  (t  u)
              = (Cod t  Cod u  (Cod t  Cod u))  (t  u)"
        using t u eval_red_Tensor by simp
      also have "... = Cod t  Cod u  (Cod t  Cod u)  (t  u)"
        using comp_assoc by simp
      also have "... = Cod t  Cod u  (t  u)  (Dom t  Dom u)"
        using assms t u Diagonalize_in_Hom red_in_Hom interchange by simp
      also have "... = (Cod t  Cod u  (t  u))  (Dom t  Dom u)"
        using comp_assoc by simp
      also have "... = (t  u  Dom t  Dom u)  (Dom t  Dom u)"
        using assms t u Diag_Diagonalize Diagonalize_in_Hom
              eval_red2_naturality [of "Diagonalize t" "Diagonalize u"]
        by simp
      also have "... = t  u  Dom t  Dom u  (Dom t  Dom u)"
        using comp_assoc by simp
      also have "... = t  u  (Dom t  Dom u)"
        using t u eval_red_Tensor by simp
      finally have "Cod (t  u)  (t  u) = t  u  (Dom t  Dom u)"
        by blast
      thus ?thesis using t u by simp
    qed

    lemma Comp_preserves_coherent:
    assumes "Arr t" and "Arr u" and "Dom t = Cod u"
    and "coherent t" and "coherent u"
    shows "coherent (t  u)"
    proof -
      have t: "Arr t  Ide (Dom t)  Ide (Cod t)  Ide Dom t  Ide Cod t 
               arr t  arr Dom t  ide Dom t  arr Cod t  ide Cod t"
        using assms Arr_implies_Ide_Dom Arr_implies_Ide_Cod Diagonalize_preserves_Ide
        by auto
      have u: "Arr u  Ide (Dom u)  Ide (Cod u)  Ide Dom u  Ide Cod u 
               arr u  arr Dom u  ide Dom u  arr Cod u  ide Cod u"
        using assms Arr_implies_Ide_Dom Arr_implies_Ide_Cod Diagonalize_preserves_Ide
        by auto
      have "Cod (t  u)  t  u = Cod t  t  u"
        using t u by simp
      also have "... = (Cod t  t)  u"
      proof -
        (* TODO: I still haven't figured out how to do this without spoon-feeding it. *)
        have "seq Cod t t"
          using assms t red_in_Hom by (intro seqI, auto)
        moreover have "seq t u"
          using assms t u by auto
        ultimately show ?thesis using comp_assoc by auto
      qed
      also have "... = t  u  Dom (t  u)"
        using t u assms red_in_Hom Diag_Diagonalize comp_assoc
        by (simp add: Diag_implies_Arr eval_CompDiag)
      finally show "coherent (t  u)" by blast
    qed

    text‹
      The main result: ``Every formal arrow is coherent.''
›

    theorem coherence:
    assumes "Arr t"
    shows "coherent t"
    proof -
      have "Arr t  coherent t"
      proof (induct t)
        fix u v
        show " Arr u  coherent u; Arr v  coherent v   Arr (u  v)
                   coherent (u  v)"
          using Tensor_preserves_coherent by simp
        show " Arr u  coherent u; Arr v  coherent v   Arr (u  v)
                   coherent (u  v)"
          using Comp_preserves_coherent by simp
        next
        show "coherent " by simp
        fix f
        show "Arr f  coherent f" by simp
        next
        fix t
        assume I: "Arr t  coherent t"
        show Lunit: "Arr 𝗅[t]  coherent 𝗅[t]"
          using I Arr_implies_Ide_Dom coherent_Lunit_Ide Ide_in_Hom Ide_implies_Arr
                Comp_preserves_coherent [of t "𝗅[Dom t]"] Diagonalize_Comp_Arr_Dom 𝔩_ide_simp
          by auto
        show Runit: "Arr 𝗋[t]  coherent 𝗋[t]"
          using I Arr_implies_Ide_Dom coherent_Runit_Ide Ide_in_Hom Ide_implies_Arr
                Comp_preserves_coherent [of t "𝗋[Dom t]"] Diagonalize_Comp_Arr_Dom ρ_ide_simp
          by auto
        show "Arr 𝗅-1[t]  coherent 𝗅-1[t]"
        proof -
          assume "Arr 𝗅-1[t]"
          hence t: "Arr t" by simp
          have "coherent (𝗅-1[Cod t]  t)"
            using t I Arr_implies_Ide_Cod coherent_Lunit'_Ide Ide_in_Hom
                  Comp_preserves_coherent [of "𝗅-1[Cod t]" t]
            by fastforce
          thus ?thesis
            using t Arr_implies_Ide_Cod Ide_implies_Arr Ide_in_Hom Diagonalize_Comp_Cod_Arr
                  eval_in_hom 𝔩'.is_natural_2 [of "t"]
            by force
        qed
        show "Arr 𝗋-1[t]  coherent 𝗋-1[t]"
        proof -
          assume "Arr 𝗋-1[t]"
          hence t: "Arr t" by simp
          have "coherent (𝗋-1[Cod t]  t)"
            using t I Arr_implies_Ide_Cod coherent_Runit'_Ide Ide_in_Hom
                  Comp_preserves_coherent [of "𝗋-1[Cod t]" t]
            by fastforce
          thus ?thesis
            using t Arr_implies_Ide_Cod Ide_implies_Arr Ide_in_Hom Diagonalize_Comp_Cod_Arr
                  eval_in_hom ρ'.is_natural_2 [of "t"]
            by force
        qed
        next
        fix t u v
        assume I1: "Arr t  coherent t"
        assume I2: "Arr u  coherent u"
        assume I3: "Arr v  coherent v"
        show "Arr 𝖺[t, u, v]  coherent 𝖺[t, u, v]"
        proof -
          assume tuv: "Arr 𝖺[t, u, v]"
          have t: "Arr t" using tuv by simp
          have u: "Arr u" using tuv by simp
          have v: "Arr v" using tuv by simp
          have "coherent ((t  u  v)  𝖺[Dom t, Dom u, Dom v])"
          proof -
            have "Arr (t  u  v)  coherent (t  u  v)"
            proof
              have 1: "Arr t  coherent t" using t I1 by simp
              have 2: "Arr (u  v)  coherent (u  v)"
                using u v I2 I3 Tensor_preserves_coherent by force
              show "Arr (t  u  v) " using 1 2 by simp
              show "coherent (t  u  v)"
                using 1 2 Tensor_preserves_coherent by blast
            qed
            moreover have "Arr 𝖺[Dom t, Dom u, Dom v]"
              using t u v Arr_implies_Ide_Dom by simp
            moreover have "coherent 𝖺[Dom t, Dom u, Dom v]"
              using t u v Arr_implies_Ide_Dom coherent_Assoc_Ide by blast
            moreover have "Dom (t  u  v) = Cod 𝖺[Dom t, Dom u, Dom v]"
              using t u v Arr_implies_Ide_Dom Ide_in_Hom by simp
            ultimately show ?thesis
              using t u v Arr_implies_Ide_Dom Ide_implies_Arr
                    Comp_preserves_coherent [of "t  u  v" "𝖺[Dom t, Dom u, Dom v]"]
              by blast
          qed
          moreover have "Par 𝖺[t, u, v] ((t  u  v)  𝖺[Dom t, Dom u, Dom v])"
            using t u v Arr_implies_Ide_Dom Ide_implies_Arr Ide_in_Hom by simp
          moreover have "𝖺[t, u, v] = (t  u  v)  𝖺[Dom t, Dom u, Dom v]"
          proof -
            have "(t  u)  v
                     = (t  u  v)  ((Dom t  Dom u)  Dom v)"
            proof -
              have 1: "Diag t  Diag u  Diag v 
                       Dom t = Dom t  Dom u = Dom u  Dom v = Dom v"
                using t u v Diag_Diagonalize by blast
              moreover have "Diag (t  u)"
                using 1 TensorDiag_preserves_Diag(1) by blast
              moreover have "t. Arr t  t  Dom t = t"
                using t Diagonalize_Comp_Arr_Dom by simp
              moreover have "Dom 𝖺[t, u, v] = Dom 𝖺[t, u, v]"
                using Diag_Diagonalize tuv by blast
              ultimately show ?thesis
                using t u v tuv 1 TensorDiag_assoc TensorDiag_preserves_Diag(2)
                by (metis (no_types) Diagonalize.simps(9))
            qed
            thus ?thesis
              using t u v Diagonalize_Comp_Arr_Dom CompDiag_TensorDiag Diag_Diagonalize
              by simp
          qed
          moreover have "𝖺[t, u, v] = (t  u  v)  𝖺[Dom t, Dom u, Dom v]"
            using t u v Arr_implies_Ide_Dom Ide_implies_Arr α_simp [of "t" "u" "v"]
            by simp
          ultimately show "coherent 𝖺[t, u, v]" by argo
        qed
        show "Arr 𝖺-1[t, u, v]  coherent 𝖺-1[t, u, v]"
        proof -
          assume tuv: "Arr 𝖺-1[t, u, v]"
          have t: "Arr t" using tuv by simp
          have u: "Arr u" using tuv by simp
          have v: "Arr v" using tuv by simp
          have "coherent (((t  u)  v)  𝖺-1[Dom t, Dom u, Dom v])"
          proof -
            have "Arr ((t  u)  v)  coherent ((t  u)  v)"
            proof
              have 1: "Arr v  coherent v" using v I3 by simp
              have 2: "Arr (t  u)  coherent (t  u)"
                using t u I1 I2 Tensor_preserves_coherent by force
              show "Arr ((t  u)  v)" using 1 2 by simp
              show "coherent ((t  u)  v)"
                using 1 2 Tensor_preserves_coherent by blast
            qed
            moreover have "Arr 𝖺-1[Dom t, Dom u, Dom v]"
              using t u v Arr_implies_Ide_Dom by simp
            moreover have "coherent 𝖺-1[Dom t, Dom u, Dom v]"
              using t u v Arr_implies_Ide_Dom coherent_Assoc'_Ide by blast
            moreover have "Dom ((t  u)  v) = Cod 𝖺-1[Dom t, Dom u, Dom v]"
              using t u v Arr_implies_Ide_Dom Ide_in_Hom by simp
            ultimately show ?thesis
              using t u v Arr_implies_Ide_Dom Ide_implies_Arr
                    Comp_preserves_coherent [of "((t  u)  v)" "𝖺-1[Dom t, Dom u, Dom v]"]
              by metis
          qed
          moreover have "Par 𝖺-1[t, u, v] (((t  u)  v)  𝖺-1[Dom t, Dom u, Dom v])"
            using t u v Arr_implies_Ide_Dom Ide_implies_Arr Ide_in_Hom by simp
          moreover have "𝖺-1[t, u, v] = ((t  u)  v)  𝖺-1[Dom t, Dom u, Dom v]"
            using t u v Diagonalize_Comp_Arr_Dom CompDiag_TensorDiag Diag_Diagonalize
                  TensorDiag_assoc TensorDiag_preserves_Diag TensorDiag_in_Hom
                  CompDiag_Diag_Dom [of "(t  u)  v"]
            by simp
          moreover have "𝖺-1[t, u, v] = ((t  u)  v)  𝖺-1[Dom t, Dom u, Dom v]"
            using t u v Arr_implies_Ide_Dom Ide_implies_Arr eval_in_hom comp_cod_arr
                  α'.is_natural_1 α'_simp
            by simp
          ultimately show "coherent 𝖺-1[t, u, v]" by argo
        qed
      qed
      thus ?thesis using assms by blast
    qed

    text‹
      MacLane cite"MacLane71" says: ``A coherence theorem asserts `Every diagram commutes',''
      but that is somewhat misleading.  A coherence theorem provides some kind of hopefully
      useful way of distinguishing diagrams that definitely commute from diagrams that might not.
      The next result expresses coherence for monoidal categories in this way.
      As the hypotheses can be verified algorithmically (using the functions @{term Dom},
      @{term Cod}, @{term Arr}, and @{term Diagonalize}) if we are given an oracle for equality
      of arrows in C›, the result provides a decision procedure, relative to C›,
      for the word problem for the free monoidal category generated by C›.
›

    corollary eval_eqI:
    assumes "Par t u" and "t = u"
    shows "t = u"
      using assms coherence canonical_factorization by simp

    text‹
      Our final corollary expresses coherence in a more ``MacLane-like'' fashion:
      parallel canonical arrows are equivalent under evaluation.
›

    corollary maclane_coherence:
    assumes "Par t u" and "Can t" and "Can u"
    shows "t = u"
    proof (intro eval_eqI)
      show "Par t u" by fact
      show "t = u"
      proof -
        have "Ide t  Ide u  Par t u"
          using assms eval_eqI Ide_Diagonalize_Can Diagonalize_in_Hom by simp
        thus ?thesis using Ide_in_Hom by auto
      qed
    qed

  end

end