Theory MonoidalFunctor

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

chapter "Monoidal Functor"

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

theory MonoidalFunctor
imports MonoidalCategory
begin

    text ‹
      A monoidal functor is a functor @{term F} between monoidal categories @{term C}
      and @{term D} that preserves the monoidal structure up to isomorphism.
      The traditional definition assumes a monoidal functor to be equipped with
      two natural isomorphisms, a natural isomorphism @{term φ} that expresses the preservation
      of tensor product and a natural isomorphism @{term ψ} that expresses the preservation
      of the unit object.  These natural isomorphisms are subject to coherence conditions;
      the condition for @{term φ} involving the associator and the conditions for @{term ψ}
      involving the unitors.  However, as pointed out in cite‹"Etingof15"› (Section 2.4),
      it is not necessary to take the natural isomorphism @{term ψ} as given,
      since the mere assumption that @{term "F ℐC"} is isomorphic to @{term "ℐD"}
      is sufficient for there to be a canonical definition of @{term ψ} from which the
      coherence conditions can be derived.  This leads to a more economical definition
      of monoidal functor, which is the one we adopt here.
›

  locale monoidal_functor =
    C: monoidal_category C TC αC ιC +
    D: monoidal_category D TD αD ιD +
    "functor" C D F +
    CC: product_category C C +
    DD: product_category D D +
    FF: product_functor C C D D F F +
    FoTC: composite_functor C.CC.comp C D TC F +
    TDoFF: composite_functor C.CC.comp D.CC.comp D FF.map TD +
    φ: natural_isomorphism C.CC.comp D TDoFF.map FoTC.map φ
  for C :: "'c comp"                    (infixr ‹⋅C› 55)
  and TC :: "'c * 'c ⇒ 'c"
  and αC :: "'c * 'c * 'c ⇒ 'c"
  and ιC :: "'c"
  and D :: "'d comp"                    (infixr ‹⋅D› 55)
  and TD :: "'d * 'd ⇒ 'd"
  and αD :: "'d * 'd * 'd ⇒ 'd"
  and ιD :: "'d"
  and F :: "'c ⇒ 'd"
  and φ :: "'c * 'c ⇒ 'd" +
  assumes preserves_unity: "D.isomorphic D.unity (F C.unity)"
  and assoc_coherence:
      "⟦ C.ide a; C.ide b; C.ide c ⟧ ⟹
         F (αC (a, b, c)) ⋅D φ (TC (a, b), c) ⋅D TD (φ (a, b), F c)
           = φ (a, TC (b, c)) ⋅D TD (F a, φ (b, c)) ⋅D αD (F a, F b, F c)"
  begin

    notation C.tensor                     (infixr ‹⊗C› 53)
    and C.unity                           (‹ℐC›)
    and C.lunit                           (‹𝗅C[_]›)
    and C.runit                           (‹𝗋C[_]›)
    and C.assoc                           (‹𝖺C[_, _, _]›)
    and D.tensor                          (infixr ‹⊗D› 53)
    and D.unity                           (‹ℐD›)
    and D.lunit                           (‹𝗅D[_]›)
    and D.runit                           (‹𝗋D[_]›)
    and D.assoc                           (‹𝖺D[_, _, _]›)

    lemma φ_in_hom:
    assumes "C.ide a" and "C.ide b"
    shows "«φ (a, b) : F a ⊗D F b →D F (a ⊗C b)»"
      using assms by auto

    text ‹
      We wish to exhibit a canonical definition of an isomorphism
      @{term "ψ ∈ D.hom ℐD (F ℐC)"} that satisfies certain coherence conditions that
      involve the left and right unitors.  In cite‹"Etingof15"›, the isomorphism @{term ψ}
      is defined by the equation @{term "𝗅D[F ℐC] = F 𝗅C[ℐC] ⋅D φ (ℐC, ℐC) ⋅D (ψ ⊗D F ℐC)"},
      which suffices for the definition because the functor ‹- ⊗D F ℐC› is fully faithful.
      It is then asserted (Proposition 2.4.3) that the coherence condition
      @{term "𝗅D[F a] = F 𝗅C[a] ⋅D φ (ℐC, a) ⋅D (ψ ⊗D F a)"} is satisfied for any object @{term a}
      of ‹C›, as well as the corresponding condition for the right unitor.
      However, the proof is left as an exercise (Exercise 2.4.4).
      The organization of the presentation suggests that that one should derive the
      general coherence condition from the special case
      @{term "𝗅D[F ℐC] = F 𝗅C[ℐC] ⋅D φ (ℐC, ℐC) ⋅D (ψ ⊗D F ℐC)"} used as the definition of @{term ψ}.
      However, I did not see how to do it that way, so I used a different approach.
      The isomorphism @{term "ιD' ≡ F ιC ⋅D φ (ℐC, ℐC)"} serves as an alternative unit for the
      monoidal category ‹D›.  There is consequently a unique isomorphism that maps
      @{term "ιD"} to @{term "ιD'"}.  We define @{term ψ} to be this isomorphism and then use
      the definition to establish the desired coherence conditions.
›

    abbreviation ι1
    where "ι1 ≡ F ιC ⋅D φ (ℐC, ℐC)"

    lemma ι1_in_hom:
    shows "«ι1 : F ℐC ⊗D F ℐC →D F ℐC»"
      using C.unit_in_hom by (intro D.in_homI, auto)

    lemma ι1_is_iso:
    shows "D.iso ι1"
      using C.unit_is_iso C.unit_in_hom φ_in_hom D.isos_compose by auto

    interpretation D: monoidal_category_with_alternate_unit D TD αD ιD ι1
    proof -
      have 1: "∃ψ. «ψ : F ℐC →D ℐD» ∧ D.iso ψ"
      proof -
        obtain ψ' where ψ': "«ψ' : ℐD →D F ℐC» ∧ D.iso ψ'"
          using preserves_unity by auto
        have "«D.inv ψ' : F ℐC →D ℐD» ∧ D.iso (D.inv ψ')"
          using ψ' by simp
        thus ?thesis by auto
      qed
      obtain ψ where ψ: "«ψ : F ℐC →D ℐD» ∧ D.iso ψ"
        using 1 by blast
      interpret L: equivalence_functor D D ‹λf. (D.cod ι1) ⊗D f›
      proof -
        interpret L: "functor" D D ‹λf. (F ℐC) ⊗D f›
          using D.T.fixing_ide_gives_functor_1 by simp
        interpret L: endofunctor D ‹λf. (F ℐC) ⊗D f› ..
        interpret ψx: natural_transformation D D ‹λf. (F ℐC) ⊗D f› ‹λf. ℐD ⊗D f›
                        ‹λf. ψ ⊗D f›
          using ψ D.T.fixing_arr_gives_natural_transformation_1 [of ψ] by auto
        interpret ψx: natural_isomorphism D D ‹λf. (F ℐC) ⊗D f› ‹λf. ℐD ⊗D f› ‹λf. ψ ⊗D f›
          apply unfold_locales using ψ D.tensor_preserves_iso by simp
        interpret 𝔩Doψx: vertical_composite D D ‹λf. (F ℐC) ⊗D f› ‹λf. ℐD ⊗D f› D.map
                                           ‹λf. ψ ⊗D f› D.𝔩 ..
        interpret 𝔩Doψx: natural_isomorphism D D ‹λf. (F ℐC) ⊗D f› D.map 𝔩Doψx.map
          using ψx.natural_isomorphism_axioms D.𝔩.natural_isomorphism_axioms
                natural_isomorphisms_compose by blast
        interpret L: equivalence_functor D D ‹λf. (F ℐC) ⊗D f›
          using L.isomorphic_to_identity_is_equivalence 𝔩Doψx.natural_isomorphism_axioms
          by simp
        show "equivalence_functor D D (λf. (D.cod ι1) ⊗D f)"
          using L.equivalence_functor_axioms C.unit_in_hom by auto
      qed
      interpret R: equivalence_functor D D ‹λf. TD (f, D.cod ι1)›
      proof -
        interpret R: "functor" D D ‹λf. TD (f, F ℐC)›
          using D.T.fixing_ide_gives_functor_2 by simp
        interpret R: endofunctor D ‹λf. TD (f, F ℐC)› ..
        interpret xψ: natural_transformation D D ‹λf. f ⊗D (F ℐC)› ‹λf. f ⊗D ℐD›
                        ‹λf. f ⊗D ψ›
          using ψ D.T.fixing_arr_gives_natural_transformation_2 [of ψ] by auto
        interpret xψ: natural_isomorphism D D ‹λf. f ⊗D (F ℐC)› ‹λf. f ⊗D ℐD› ‹λf. f ⊗D ψ›
          using ψ D.tensor_preserves_iso by (unfold_locales, simp)
        interpret ρDoxψ: vertical_composite D D ‹λf. f ⊗D (F ℐC)› ‹λf. f ⊗D ℐD› D.map
                                                ‹λf. f ⊗D ψ› D.ρ ..
        interpret ρDoxψ: natural_isomorphism D D ‹λf. f ⊗D (F ℐC)› D.map ρDoxψ.map
          using xψ.natural_isomorphism_axioms D.ρ.natural_isomorphism_axioms
                natural_isomorphisms_compose by blast
        interpret R: equivalence_functor D D ‹λf. f ⊗D (F ℐC)›
          using R.isomorphic_to_identity_is_equivalence ρDoxψ.natural_isomorphism_axioms
          by simp
        show "equivalence_functor D D (λf. f ⊗D (D.cod ι1))"
          using R.equivalence_functor_axioms C.unit_in_hom by auto
      qed
      show "monoidal_category_with_alternate_unit D TD αD ιD ι1"
        using D.pentagon C.unit_is_iso C.unit_in_hom preserves_hom ι1_is_iso ι1_in_hom
        by (unfold_locales, auto)
    qed

    no_notation D.tensor   (infixr ‹⊗D› 53)
    notation D.C1.tensor   (infixr ‹⊗D› 53)   (* equal to D.tensor *)
    no_notation D.assoc    (‹𝖺D[_, _, _]›)
    notation D.C1.assoc    (‹𝖺D[_, _, _]›)      (* equal to D.assoc *)
    no_notation D.assoc'   (‹𝖺D-1[_, _, _]›)
    notation D.C1.assoc'   (‹𝖺D-1[_, _, _]›)   (* equal to D.assoc' *)
    notation D.C1.unity    (‹ℐ1›)
    notation D.C1.lunit    (‹𝗅1[_]›)
    notation D.C1.runit    (‹𝗋1[_]›)

    lemma ℐ1_char [simp]:
    shows "ℐ1 = F ℐC"
      using ι1_in_hom by auto

    definition ψ
    where "ψ ≡ THE ψ. «ψ : ℐD →D F ℐC» ∧ D.iso ψ ∧ ψ ⋅D ιD = ι1 ⋅D (ψ ⊗D ψ)"

    lemma ψ_char:
    shows "«ψ : ℐD →D F ℐC»" and "D.iso ψ" and "ψ ⋅D ιD = ι1 ⋅D (ψ ⊗D ψ)"
    and "∃!ψ. «ψ : ℐD →D F ℐC» ∧ D.iso ψ ∧ ψ ⋅D ιD = ι1 ⋅D (ψ ⊗D ψ)"
    proof -
      show "∃!ψ. «ψ : ℐD →D F ℐC» ∧ D.iso ψ ∧ ψ ⋅D ιD = ι1 ⋅D (ψ ⊗D ψ)"
        using D.unit_unique_upto_unique_iso ι1_in_hom
        by (elim D.in_homE, auto)
      hence 1: "«ψ : ℐD →D F ℐC» ∧ D.iso ψ ∧ ψ ⋅D ιD = ι1 ⋅D (ψ ⊗D ψ)"
        unfolding ψ_def
        using theI' [of "λψ. «ψ : ℐD →D F ℐC» ∧ D.iso ψ ∧ ψ ⋅D ιD = ι1 ⋅D (ψ ⊗D ψ)"]
          by fast
      show "«ψ : ℐD →D F ℐC»" using 1 by simp
      show "D.iso ψ" using 1 by simp
      show "ψ ⋅D ιD = ι1 ⋅D (ψ ⊗D ψ)" using 1 by simp
    qed

    lemma ψ_eqI:
    assumes "«f: ℐD →D F ℐC»" and "D.iso f" and "f ⋅D ιD = ι1 ⋅D (f ⊗D f)"
    shows "f = ψ"
      using assms ψ_def ψ_char
            the1_equality [of "λf. «f: ℐD →D F ℐC» ∧ D.iso f ∧ f ⋅D ιD = ι1 ⋅D (f ⊗D f)" f]
      by simp

    lemma lunit_coherence1:
    assumes "C.ide a"
    shows "𝗅1[F a] ⋅D (ψ ⊗D F a) = 𝗅D[F a]"
    proof -
      have "D.par (𝗅1[F a] ⋅D (ψ ⊗D F a)) 𝗅D[F a]"
        using assms D.C1.lunit_in_hom D.tensor_in_hom D.lunit_in_hom ψ_char(1)
        by auto
      text ‹
        The upper left triangle in the following diagram commutes.
›
      text ‹
\newcommand\xIc{{\cal I}}
\newcommand\xId{{\cal I}}
\newcommand\xac[3]{{\scriptsize ‹𝖺›}[{#1},{#2},{#3}]}
\newcommand\xad[3]{{\scriptsize ‹𝖺›}[{#1},{#2},{#3}]}
\newcommand\xlc[1]{{\scriptsize ‹𝗅›}[{#1}]}
\newcommand\xld[1]{{\scriptsize ‹𝗅›}[{#1}]}
\newcommand\xldp[1]{{\scriptsize ‹𝗅›}_1[{#1}]}
$$\xymatrix{
  {\xId\otimes F a}
     \ar[rrr]^{\psi\otimes F a}
  & & &
  {F\xIc\otimes F a}
  \\
  &
  {\xId\otimes(F\xIc \otimes F a)}
     \ar[ul]_{\xId\otimes\xldp{F a}}
     \ar[ddr]^{\psi\otimes(F\xIc\otimes F a)}
  \\ \\
  &
  {\xId\otimes(\xId \otimes F a)}
     \ar[r]_{\psi\otimes(\psi\otimes F a)}
     \ar[uuul]^{\xId\otimes\xld{F a}}
     \ar[uu]_{\xId\otimes(\psi\otimes F a)}
  &
  {F\xIc\otimes (F\xIc\otimes F a)}
     \ar[uuur]^{F\xIc\otimes\xldp{F a}}
  \\ \\
  {(\xId\otimes\xId)\otimes F a}
     \ar[uuuuu]^{\iota\otimes F a}
     \ar[uur]_{\xad{\xId}{\xId}{F a}}
     \ar[rrr]^{(\psi\otimes\psi)\otimes F a}
  & & &
  {(F\xIc\otimes F\xIc)\otimes F a}
     \ar[uuuuu]_{\iota_1\otimes F a}
     \ar[uul]^{\xad{F\xIc}{F\xIc}{F a}}
}$$
›
      moreover have "(ℐD ⊗D 𝗅1[F a]) ⋅D (ℐD ⊗D ψ ⊗D F a) = ℐD ⊗D 𝗅D[F a]"
      proof -
        have "(ℐD ⊗D 𝗅1[F a]) ⋅D (ℐD ⊗D ψ ⊗D F a)
                = (ℐD ⊗D 𝗅1[F a]) ⋅D (D.inv ψ ⊗D F ℐC ⊗D F a) ⋅D (ψ ⊗D ψ ⊗D F a)"
          using assms ψ_char(1-2) D.interchange [of "D.inv ψ"] D.comp_cod_arr
                D.inv_is_inverse D.comp_inv_arr
          by (elim D.in_homE, simp)
        also have "... = (D.inv ψ ⊗D F a) ⋅D (F ℐC ⊗D 𝗅1[F a]) ⋅D (ψ ⊗D ψ ⊗D F a)"
        proof -
          have "(ℐD ⊗D 𝗅1[F a]) ⋅D (D.inv ψ ⊗D F ℐC ⊗D F a) =
                (D.inv ψ ⊗D F a) ⋅D (F ℐC ⊗D 𝗅1[F a])"
            using assms ψ_char(1-2) D.interchange [of "ℐD"] D.interchange [of "D.inv ψ"]
                  D.comp_arr_dom D.comp_cod_arr
            by (elim D.in_homE, auto)
          thus ?thesis
            using assms ψ_char(1-2) D.inv_in_hom
                  D.comp_permute [of "ℐD ⊗D 𝗅1[F a]" "D.inv ψ ⊗D F ℐC ⊗D F a"
                                     "D.inv ψ ⊗D F a" "F ℐC ⊗D 𝗅1[F a]"]
            by (elim D.in_homE, auto)
        qed
        also have "... = (D.inv ψ ⊗D F a) ⋅D (ι1 ⊗D F a) ⋅D D.inv 𝖺D[F ℐC, F ℐC, F a] ⋅D
                         (ψ ⊗D ψ ⊗D F a)"
          using assms ψ_char(1-2) D.C1.lunit_char(2) D.comp_assoc by auto
        also have "... = ((D.inv ψ ⊗D F a) ⋅D (ι1 ⊗D F a) ⋅D ((ψ ⊗D ψ) ⊗D F a)) ⋅D
                         D.inv 𝖺D[ℐD, ℐD, F a]"
          using assms ψ_char(1-2) D.assoc'_naturality [of ψ ψ "F a"] D.comp_assoc by auto
        also have "... = (ιD ⊗D F a) ⋅D D.inv 𝖺D[ℐD, ℐD, F a]"
        proof -
          have "(D.inv ψ ⊗D F a) ⋅D (ι1 ⊗D F a) ⋅D ((ψ ⊗D ψ) ⊗D F a) = ιD ⊗D F a"
          proof -
            have "(D.inv ψ ⊗D F a) ⋅D (ι1 ⊗D F a) ⋅D ((ψ ⊗D ψ) ⊗D F a) =
                  D.inv ψ ⋅D ψ ⋅D ιD ⊗D F a"
              using assms ψ_char(1-3) ι1_in_hom D.interchange
              by (elim D.in_homE, auto)
            also have "... = ιD ⊗D F a"
              using assms ψ_char(1-2) D.inv_is_inverse D.comp_inv_arr D.comp_cod_arr
                    D.comp_reduce D.unit_in_hom
              by (elim D.in_homE, auto)
            finally show ?thesis by blast
          qed
          thus ?thesis by simp
        qed
        also have "... = ℐD ⊗D 𝗅D[F a]"
          using assms D.lunit_char by simp
        finally show ?thesis by blast
      qed
      ultimately show ?thesis
        using D.L.is_faithful [of "𝗅1[F a] ⋅D (ψ ⊗D F a)" "𝗅D[F a]"] by force
    qed

    lemma lunit_coherence2:
    assumes "C.ide a"
    shows "F 𝗅C[a] ⋅D φ (ℐC, a) = 𝗅1[F a]"
    proof -
      text ‹
        We show that the lower left triangle in the following diagram commutes.
›
      text ‹
\newcommand\xIc{{\cal I}}
\newcommand\xId{{\cal I}}
\newcommand\xac[3]{{\scriptsize ‹𝖺›}[{#1},{#2},{#3}]}
\newcommand\xad[3]{{\scriptsize ‹𝖺›}[{#1},{#2},{#3}]}
\newcommand\xlc[1]{{\scriptsize ‹𝗅›}[{#1}]}
\newcommand\xld[1]{{\scriptsize ‹𝗅›}[{#1}]}
\newcommand\xldp[1]{{\scriptsize ‹𝗅›}_1[{#1}]}
$$\xymatrix{
  {(F\xIc\otimes F\xIc)\otimes F a}
      \ar[rrrrr]^{\phi(\xIc,\xIc)\otimes F a}
      \ar[ddd]_{\xad{F\xIc}{F\xIc}{Fa}}
      \ar[dddrr]^{\iota_1\otimes F a}
  &&&&&{F(\xIc\otimes\xIc)\otimes F a}
      \ar[ddd]^{\phi(\xIc\otimes\xIc, a)}
      \ar[dddlll]_{F\iota\otimes F a}
  \\ \\ \\
  {F\xIc\otimes(F\xIc\otimes F a)}
      \ar[ddd]_{F\xIc\otimes\phi(\xIc, a)}
      \ar[rr]_{F\xIc\otimes\xldp{Fa}}
  &&{F\xIc\otimes F a}
      \ar[r]_{\phi(\xIc, a)}
  &{F(\xIc\otimes a)}
  &&{F((\xIc\otimes\xIc)\otimes a)}
      \ar[ddd]^{F\xac{\xIc}{\xIc}{a}}
      \ar[ll]^{F(\iota\otimes a)}
  \\ \\ \\
  {F\xIc\otimes F (\xIc\otimes a)}
      \ar[rrrrr]_{\phi(\xIc, \xIc\otimes a)}
      \ar[uuurr]_{F\xIc\otimes F\xlc{a}}
  &&&&&{F(\xIc\otimes (\xIc \otimes a))}
      \ar[uuull]^{F(\xIc\otimes\xlc{a})}
}$$
›
      have "(F ℐC ⊗D F 𝗅C[a]) ⋅D (F ℐC ⊗D φ (ℐC, a)) = F ℐC ⊗D 𝗅1[F a]"
      proof -
        have "(F ℐC ⊗D F 𝗅C[a]) ⋅D (F ℐC ⊗D φ (ℐC, a))
                = (F ℐC ⊗D F 𝗅C[a]) ⋅D D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D F 𝖺C[ℐC, ℐC, a] ⋅D
                  φ (ℐC ⊗C ℐC, a) ⋅D (φ (ℐC, ℐC) ⊗D F a) ⋅D D.inv 𝖺D[F ℐC, F ℐC, F a]"
        proof -
          have "D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D F 𝖺C[ℐC, ℐC, a] ⋅D φ (ℐC ⊗C ℐC, a) ⋅D
                       (φ (ℐC, ℐC) ⊗D F a)
                   = (F ℐC ⊗D φ (ℐC, a)) ⋅D 𝖺D[F ℐC, F ℐC, F a]"
            using assms φ_in_hom assoc_coherence D.invert_side_of_triangle(1) by simp
          hence "F ℐC ⊗D φ (ℐC, a)
                    = (D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D F 𝖺C[ℐC, ℐC, a] ⋅D φ (ℐC ⊗C ℐC, a) ⋅D
                      (φ (ℐC, ℐC) ⊗D F a)) ⋅D D.inv 𝖺D[F ℐC, F ℐC, F a]"
            using assms φ_in_hom D.invert_side_of_triangle(2) by simp
          thus ?thesis
            using D.comp_assoc by simp
        qed
        also have "... = (F ℐC ⊗D F 𝗅C[a]) ⋅D D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D
                         (D.inv (F (ℐC ⊗C 𝗅C[a])) ⋅D F (ιC ⊗C a)) ⋅D
                         φ (ℐC ⊗C ℐC, a) ⋅D (φ (ℐC, ℐC) ⊗D F a) ⋅D
                         D.inv 𝖺D[F ℐC, F ℐC, F a]"
        proof -
          have 1: "F (ℐC ⊗C 𝗅C[a]) = F (ιC ⊗C a) ⋅D D.inv (F 𝖺C[ℐC, ℐC, a])"
            using assms C.lunit_char(1-2) C.unit_in_hom preserves_inv by auto
          hence "F 𝖺C[ℐC, ℐC, a] = D.inv (F (ℐC ⊗C 𝗅C[a])) ⋅D F (ιC ⊗C a)"
          proof -
            have "F 𝖺C[ℐC, ℐC, a] ⋅D D.inv (F (ιC ⊗C a))
                    = D.inv (F (ιC ⊗C a) ⋅D D.inv (F 𝖺C[ℐC, ℐC ,a]))"
              using assms 1 preserves_iso C.ide_is_iso C.unit_is_iso C.ide_unity C.iso_assoc
                    C.iso_lunit C.tensor_preserves_iso D.inv_comp D.inv_inv
                    D.iso_inv_iso D.iso_is_arr
              by metis
            thus ?thesis
              using assms 1 preserves_iso C.ide_is_iso C.unit_is_iso C.ide_unity C.iso_assoc
                    C.iso_lunit C.tensor_preserves_iso D.inv_comp D.inv_inv
                    D.iso_inv_iso D.iso_is_arr D.invert_side_of_triangle(2)
              by metis
          qed
         thus ?thesis by argo
        qed
        also have "... = (F ℐC ⊗D F 𝗅C[a]) ⋅D D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D
                         D.inv (F (ℐC ⊗C 𝗅C[a])) ⋅D (F (ιC ⊗C a) ⋅D φ (ℐC ⊗C ℐC, a)) ⋅D
                         (φ (ℐC, ℐC) ⊗D F a) ⋅D D.inv 𝖺D[F ℐC, F ℐC, F a]"
          using D.comp_assoc by auto
        also have "... = (F ℐC ⊗D F 𝗅C[a]) ⋅D D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D
                         D.inv (F (ℐC ⊗C 𝗅C[a])) ⋅D (φ (ℐC, a) ⋅D (F ιC ⊗D F a)) ⋅D
                         (φ (ℐC, ℐC) ⊗D F a) ⋅D D.inv 𝖺D[F ℐC, F ℐC, F a]"
          using assms φ.naturality [of "(ιC, a)"] C.unit_in_hom by auto
        also have "... = (F ℐC ⊗D F 𝗅C[a]) ⋅D D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D
                         D.inv (F (ℐC ⊗C 𝗅C[a])) ⋅D φ (ℐC, a) ⋅D
                         ((F ιC ⊗D F a) ⋅D (φ (ℐC, ℐC) ⊗D F a)) ⋅D
                         D.inv 𝖺D[F ℐC, F ℐC, F a]"
          using D.comp_assoc by auto
        also have "... = (F ℐC ⊗D F 𝗅C[a]) ⋅D D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D
                         D.inv (F (ℐC ⊗C 𝗅C[a])) ⋅D φ (ℐC, a) ⋅D (ι1 ⊗D F a) ⋅D
                         D.inv 𝖺D[F ℐC, F ℐC, F a]"
          using assms D.interchange C.unit_in_hom by auto
        also have "... = (F ℐC ⊗D F 𝗅C[a]) ⋅D D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D
                         D.inv (F (ℐC ⊗C 𝗅C[a])) ⋅D φ (ℐC, a) ⋅D
                         ((F ℐC ⊗D 𝗅1[F a]) ⋅D 𝖺D[F ℐC, F ℐC, F a]) ⋅D
                         D.inv 𝖺D[F ℐC, F ℐC, F a]"
        proof -
          have "(ι1 ⊗D F a) ⋅D 𝖺D-1[F ℐC, F ℐC, F a] = F ℐC ⊗D 𝗅1[F a]"
            using assms D.C1.lunit_char [of "F a"] by auto
          thus ?thesis
            using assms D.inv_is_inverse ι1_in_hom φ_in_hom D.invert_side_of_triangle(2)
            by simp
        qed
        also have "... = (F ℐC ⊗D F 𝗅C[a]) ⋅D
                         (D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D D.inv (F (ℐC ⊗C 𝗅C[a])) ⋅D φ (ℐC, a)) ⋅D
                         (F ℐC ⊗D 𝗅1[F a])"
          using assms D.comp_arr_dom [of "F ℐC ⊗D 𝗅1[F a]"] D.comp_assoc by auto
        also have "... = (F ℐC ⊗D F 𝗅C[a]) ⋅D D.inv (F ℐC ⊗D F 𝗅C[a]) ⋅D (F ℐC ⊗D 𝗅1[F a])"
        proof -
          have "D.inv (F ℐC ⊗D F 𝗅C[a])
                   = D.inv (D.inv (φ (ℐC, a)) ⋅D F (ℐC ⊗C 𝗅C[a]) ⋅D φ (ℐC, ℐC ⊗C a))"
            using assms φ.naturality [of "(ℐC, 𝗅C[a])"] D.invert_side_of_triangle(1) by simp
          also have "... = D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D D.inv (F (ℐC ⊗C 𝗅C[a])) ⋅D φ (ℐC, a)"
            using assms D.inv_comp D.inv_is_inverse D.isos_compose D.comp_assoc
            by simp
          finally have "D.inv (F ℐC ⊗D F 𝗅C[a])
                          = D.inv (φ (ℐC, ℐC ⊗C a)) ⋅D D.inv (F (ℐC ⊗C 𝗅C[a])) ⋅D φ (ℐC, a)"
            by blast
          thus ?thesis by argo
        qed
        also have "... = ((F ℐC ⊗D F 𝗅C[a]) ⋅D D.inv (F ℐC ⊗D F 𝗅C[a])) ⋅D (F ℐC ⊗D 𝗅1[F a])"
          using assms D.tensor_preserves_iso D.comp_assoc by simp
        also have "... = F ℐC ⊗D 𝗅1[F a]"
          using assms D.tensor_preserves_iso D.comp_arr_inv D.inv_is_inverse D.comp_cod_arr
                D.interchange
          by simp
        finally show ?thesis by blast
      qed
      hence "F ℐC ⊗D F 𝗅C[a] ⋅D φ (ℐC, a) = F ℐC ⊗D 𝗅1[F a]"
        using assms φ_in_hom D.interchange by simp
      moreover have "D.par (F 𝗅C[a] ⋅D φ (ℐC, a)) 𝗅1[F a]"
        using assms φ_in_hom by simp
      ultimately show ?thesis
        using D.C1.L.is_faithful [of "F 𝗅C[a] ⋅D φ (ℐC, a)" "𝗅1[F a]"] by simp
    qed

    text ‹
      Combining the two previous lemmas yields the coherence result we seek.
      This is the condition that is traditionally taken as part of the definition
      of monoidal functor.
›

    lemma lunit_coherence:
    assumes "C.ide a"
    shows "𝗅D[F a] = F 𝗅C[a] ⋅D φ (ℐC, a) ⋅D (ψ ⊗D F a)"
    proof -
      have "𝗅D[F a] ⋅D D.inv (ψ ⊗D F a) = 𝗅1[F a]"
        using assms lunit_coherence1 ψ_char(2)
              D.invert_side_of_triangle(2) [of "𝗅D[F a]" "𝗅1[F a]" "ψ ⊗D F a"]
        by auto
      also have "... = F 𝗅C[a] ⋅D φ (ℐC, a)"
        using assms lunit_coherence2 by simp
      finally have "𝗅D[F a] ⋅D D.inv (ψ ⊗D F a) = F 𝗅C[a] ⋅D φ (ℐC, a)"
        by blast
      hence "𝗅D[F a] = (F 𝗅C[a] ⋅D φ (ℐC, a)) ⋅D (ψ ⊗D F a)"
        using assms ψ_char(2) φ_in_hom
              D.invert_side_of_triangle(2) [of "F 𝗅C[a] ⋅D φ (ℐC, a)" "𝗅D[F a]" "D.inv (ψ ⊗D F a)"]
        by simp
      thus ?thesis
        using assms ψ_char(1) D.comp_assoc by auto
    qed

    text ‹
      We now want to obtain the corresponding result for the right unitor.
      To avoid a repetition of what would amount to essentially the same tedious diagram chases
      that were carried out above, we instead show here that @{term F} becomes a monoidal functor
      from the opposite of ‹C› to the opposite of ‹D›,
      with @{term "λf. φ (snd f, fst f)"} as the structure map.
      The fact that in the opposite monoidal categories the left and right unitors are exchanged
      then permits us to obtain the result for the right unitor from the result already proved
      for the left unitor.
›

    interpretation C': opposite_monoidal_category C TC αC ιC ..
    interpretation D': opposite_monoidal_category D TD αD ιD ..
    interpretation TD'oFF: composite_functor C.CC.comp D.CC.comp D FF.map D'.T ..
    interpretation FoTC': composite_functor C.CC.comp C D C'.T F ..
    interpretation φ': natural_transformation C.CC.comp D TD'oFF.map FoTC'.map
                                              ‹λf. φ (snd f, fst f)›
      using φ.is_natural_1 φ.is_natural_2 φ.is_extensional by (unfold_locales, auto)
    interpretation φ': natural_isomorphism C.CC.comp D TD'oFF.map FoTC'.map
                                           ‹λf. φ (snd f, fst f)›
      by (unfold_locales, simp)
    interpretation F': monoidal_functor C C'.T C'.α ιC D D'.T D'.α ιD F ‹λf. φ (snd f, fst f)›
      using preserves_unity apply (unfold_locales; simp)
    proof -
      fix a b c
      assume a: "C.ide a" and b: "C.ide b" and c: "C.ide c"
      have "(φ (c ⊗C b, a) ⋅D (φ (c, b) ⊗D F a)) ⋅D 𝖺D-1[F c, F b, F a] =
            F (C.assoc' c b a) ⋅D φ (c, b ⊗C a) ⋅D (F c ⊗D φ (b, a))"
      proof -
        have "D.seq (F 𝖺C[c, b, a]) (φ (c ⊗C b, a) ⋅D (φ (c, b) ⊗D F a))"
          using a b c φ_in_hom by simp
        moreover have "D.seq (φ (c, b ⊗C a) ⋅D (F c ⊗D φ (b, a))) 𝖺D[F c, F b, F a]"
          using a b c φ_in_hom by simp
        moreover have
             "F 𝖺C[c, b, a] ⋅D φ (c ⊗C b, a) ⋅D (φ (c, b) ⊗D F a) =
              (φ (c, b ⊗C a) ⋅D (F c ⊗D φ (b, a))) ⋅D 𝖺D[F c, F b, F a]"
          using a b c assoc_coherence D.comp_assoc by simp
        moreover have "D.iso (F 𝖺C[c,b,a])"
          using a b c by simp
        moreover have "D.iso 𝖺D[F c, F b, F a]"
          using a b c by simp
        moreover have "D.inv (F 𝖺C[c,b,a]) = F (C.assoc' c b a)"
          using a b c preserves_inv by simp
        ultimately show ?thesis
          using D.invert_opposite_sides_of_square by simp
      qed
      thus "F (C.assoc' c b a) ⋅D φ (c, b ⊗C a) ⋅D (F c ⊗D φ (b, a)) =
            φ (c ⊗C b, a) ⋅D (φ (c, b) ⊗D F a) ⋅D 𝖺D-1[F c, F b, F a]"
        using D.comp_assoc by simp
    qed

    lemma induces_monoidal_functor_between_opposites:
    shows "monoidal_functor C C'.T C'.α ιC D D'.T D'.α ιD F (λf. φ (snd f, fst f))"
      ..

    lemma runit_coherence:
    assumes "C.ide a"
    shows "𝗋D[F a] = F 𝗋C[a] ⋅D φ (a, ℐC) ⋅D (F a ⊗D ψ)"
    proof -
      have "C'.lunit a = 𝗋C[a]"
        using assms C'.lunit_simp by simp
      moreover have "D'.lunit (F a) = 𝗋D[F a]"
        using assms D'.lunit_simp by simp
      moreover have "F'.ψ = ψ"
      proof (intro ψ_eqI)
        show "«F'.ψ : D'.unity →D F C'.unity»" using F'.ψ_char(1) by simp
        show "D.iso F'.ψ" using F'.ψ_char(2) by simp
        show "F'.ψ ⋅D ιD = ι1 ⋅D (F'.ψ ⊗D F'.ψ)" using F'.ψ_char(3) by simp
      qed
      moreover have "D'.lunit (F a) = F (C'.lunit a) ⋅D φ (a, C'.unity) ⋅D (F a ⊗D F'.ψ)"
        using assms F'.lunit_coherence by simp
      ultimately show ?thesis by simp
    qed

  end

  section "Strict Monoidal Functor"

  text ‹
    A strict monoidal functor preserves the monoidal structure ``on the nose''.
›

  locale strict_monoidal_functor =
    C: monoidal_category C TC αC ιC +
    D: monoidal_category D TD αD ιD +
    "functor" C D F
  for C :: "'c comp"                    (infixr ‹⋅C› 55)
  and TC :: "'c * 'c ⇒ 'c"
  and αC :: "'c * 'c * 'c ⇒ 'c"
  and ιC :: "'c"
  and D :: "'d comp"                    (infixr ‹⋅D› 55)
  and TD :: "'d * 'd ⇒ 'd"
  and αD :: "'d * 'd * 'd ⇒ 'd"
  and ιD :: "'d"
  and F :: "'c ⇒ 'd" +
  assumes strictly_preserves_ι: "F ιC = ιD"
  and strictly_preserves_T: "⟦ C.arr f; C.arr g ⟧ ⟹ F (TC (f, g)) = TD (F f, F g)"
  and strictly_preserves_α_ide: "⟦ C.ide a; C.ide b; C.ide c ⟧ ⟹
                                   F (αC (a, b, c)) = αD (F a, F b, F c)"
  begin

    notation C.tensor                  (infixr ‹⊗C› 53)
    and C.unity                        (‹ℐC›)
    and C.lunit                        (‹𝗅C[_]›)
    and C.runit                        (‹𝗋C[_]›)
    and C.assoc                        (‹𝖺C[_, _, _]›)
    and D.tensor                       (infixr ‹⊗D› 53)
    and D.unity                        (‹ℐD›)
    and D.lunit                        (‹𝗅D[_]›)
    and D.runit                        (‹𝗋D[_]›)
    and D.assoc                        (‹𝖺D[_, _, _]›)

    lemma strictly_preserves_tensor:
    assumes "C.arr f" and "C.arr g"
    shows "F (f ⊗C g) = F f ⊗D F g"
      using assms strictly_preserves_T by blast

    lemma strictly_preserves_α:
    assumes "C.arr f" and "C.arr g" and "C.arr h"
    shows "F (αC (f, g, h)) = αD (F f, F g, F h)"
    proof -
      have "F (αC (f, g, h)) = F ((f ⊗C g ⊗C h) ⋅C αC (C.dom f, C.dom g, C.dom h))"
        using assms C.α.is_natural_1 [of "(f, g, h)"] C.T.ToCT_simp by force
      also have "... = (F f ⊗D F g ⊗D F h) ⋅D αD (D.dom (F f), D.dom (F g), D.dom (F h))"
        using assms strictly_preserves_α_ide strictly_preserves_tensor by simp
      also have "... = αD (F f, F g, F h)"
        using assms D.α.is_natural_1 [of "(F f, F g, F h)"] by simp
      finally show ?thesis by blast
    qed

    lemma strictly_preserves_unity:
    shows "F ℐC = ℐD"
      using C.unit_in_hom strictly_preserves_ι by auto

    lemma strictly_preserves_assoc:
    assumes "C.arr a" and "C.arr b" and "C.arr c"
    shows "F 𝖺C[a, b, c] = 𝖺D[F a, F b, F c] "
      using assms strictly_preserves_α by simp

    lemma strictly_preserves_lunit:
    assumes "C.ide a"
    shows "F 𝗅C[a] = 𝗅D[F a]"
    proof -
      let ?P = "λf. f ∈ C.hom (ℐC ⊗C a) a ∧ ℐC ⊗C f = (ιC ⊗C a) ⋅C C.assoc' ℐC ℐC a"
      let ?Q = "λf. f ∈ D.hom (ℐD ⊗D F a) (F a) ∧
                    ℐD ⊗D f = (ιD ⊗D F a) ⋅D D.assoc' ℐD ℐD (F a)"
      have 1: "?P 𝗅C[a]" using assms C.lunit_char by simp
      hence "?Q (F 𝗅C[a])"
      proof -
        have "F 𝗅C[a] ∈ D.hom (ℐD ⊗D F a) (F a)"
          using assms 1 strictly_preserves_unity strictly_preserves_tensor by auto
        moreover have
            "F ((ιC ⊗C a) ⋅C C.assoc' ℐC ℐC a) = (ιD ⊗D F a) ⋅D D.assoc' ℐD ℐD (F a)"
          using assms 1 strictly_preserves_ι strictly_preserves_assoc strictly_preserves_unity
                strictly_preserves_tensor preserves_inv C.unit_in_hom
          by auto
        moreover have "ℐD ⊗D F 𝗅C[a] = F (ℐC ⊗C 𝗅C[a])"
          using assms strictly_preserves_unity strictly_preserves_tensor by simp
        ultimately show ?thesis
          using assms C.lunit_char(2) by simp
      qed
      thus ?thesis using assms D.lunit_eqI by simp
    qed

    lemma strictly_preserves_runit:
    assumes "C.ide a"
    shows "F 𝗋C[a] = 𝗋D[F a]"
    proof -
      let ?P = "λf. f ∈ C.hom (a ⊗C ℐC) a ∧ f ⊗C ℐC = (a ⊗C ιC) ⋅C C.assoc a ℐC ℐC"
      let ?Q = "λf. f ∈ D.hom (F a ⊗D ℐD) (F a) ∧
                    f ⊗D ℐD = (F a ⊗D ιD) ⋅D D.assoc (F a) ℐD ℐD"
      have 1: "?P 𝗋C[a]" using assms C.runit_char by simp
      hence "?Q (F 𝗋C[a])"
      proof -
        have "F 𝗋C[a] ∈ D.hom (F a ⊗D ℐD) (F a)"
          using assms 1 strictly_preserves_unity strictly_preserves_tensor by auto
        moreover have "F ((a ⊗C ιC) ⋅C C.assoc a ℐC ℐC)
                         = (F a ⊗D ιD) ⋅D D.assoc (F a) ℐD ℐD"
          using assms 1 strictly_preserves_ι strictly_preserves_assoc strictly_preserves_unity
                strictly_preserves_tensor preserves_inv C.unit_in_hom
          by auto
        moreover have "F 𝗋C[a] ⊗D ℐD = F (𝗋C[a] ⊗C ℐC)"
          using assms strictly_preserves_unity strictly_preserves_tensor by simp
        ultimately show ?thesis
          using assms C.runit_char(2) by simp
      qed
      thus ?thesis using assms D.runit_eqI by simp
    qed

    text ‹
      The following are used to simplify the expression of the sublocale relationship between
      @{locale strict_monoidal_functor} and @{locale monoidal_functor}, as the definition of
      the latter mentions the structure map @{term φ}.  For a strict monoidal functor,
      this is an identity transformation.
›

    interpretation FF: product_functor C C D D F F ..
    interpretation FoTC: composite_functor C.CC.comp C D TC F ..
    interpretation TDoFF: composite_functor C.CC.comp D.CC.comp D FF.map TD ..

    lemma structure_is_trivial:
    shows "TDoFF.map = FoTC.map"
    proof
      fix x
      have "C.CC.arr x ⟹ TDoFF.map x = FoTC.map x"
      proof -
        assume x: "C.CC.arr x"
        have "TDoFF.map x = F (fst x) ⊗D F (snd x)"
          using x by simp
        also have "... = FoTC.map x"
          using x strictly_preserves_tensor [of "fst x" "snd x"] by simp
        finally show "TDoFF.map x = FoTC.map x" by simp
      qed
      moreover have "¬ C.CC.arr x ⟹ TDoFF.map x = FoTC.map x"
        using TDoFF.is_extensional FoTC.is_extensional by simp
      ultimately show "TDoFF.map x = FoTC.map x" by blast
    qed

    abbreviation φ where "φ ≡ TDoFF.map"

    lemma structure_is_natural_isomorphism:
    shows "natural_isomorphism C.CC.comp D TDoFF.map FoTC.map φ"
      using TDoFF.as_nat_iso.natural_isomorphism_axioms structure_is_trivial by force

  end

  text ‹
    A strict monoidal functor is a monoidal functor.
›

  sublocale strict_monoidal_functor ⊆ monoidal_functor C TC αC ιC D TD αD ιD F φ
  proof -
    interpret FF: product_functor C C D D F F ..
    interpret FoTC: composite_functor C.CC.comp C D TC F ..
    interpret TDoFF: composite_functor C.CC.comp D.CC.comp D FF.map TD ..
    interpret φ: natural_isomorphism C.CC.comp D TDoFF.map FoTC.map φ
      using structure_is_natural_isomorphism by simp
    show "monoidal_functor C TC αC ιC D TD αD ιD F φ"
    proof
      show "D.isomorphic ℐD (F ℐC)"
      proof (unfold D.isomorphic_def)
        have "«ℐD : ℐD →D F ℐC» ∧ D.iso ℐD"
          using strictly_preserves_unity by auto
        thus "∃f. «f : ℐD →D F ℐC» ∧ D.iso f" by blast
      qed
      fix a b c
      assume a: "C.ide a"
      assume b: "C.ide b"
      assume c: "C.ide c"
      show "F 𝖺C[a, b, c] ⋅D φ (a ⊗C b, c) ⋅D (φ (a, b) ⊗D F c) =
            φ (a, b ⊗C c) ⋅D (F a ⊗D φ (b, c)) ⋅D 𝖺D[F a, F b, F c]"
        using a b c strictly_preserves_tensor strictly_preserves_assoc
              D.comp_arr_dom D.comp_cod_arr
        by simp
    qed
  qed

  lemma strict_monoidal_functors_compose:
  assumes "strict_monoidal_functor B TB αB ιB C TC αC ιC F"
  and "strict_monoidal_functor C TC αC ιC D TD αD ιD G"
  shows "strict_monoidal_functor B TB αB ιB D TD αD ιD (G o F)"
  proof -
    interpret F: strict_monoidal_functor B TB αB ιB C TC αC ιC F
      using assms(1) by auto
    interpret G: strict_monoidal_functor C TC αC ιC D TD αD ιD G
      using assms(2) by auto
    interpret GoF: composite_functor B C D F G ..
    show ?thesis
      using F.strictly_preserves_T F.strictly_preserves_ι F.strictly_preserves_α
            G.strictly_preserves_T G.strictly_preserves_ι G.strictly_preserves_α
      by (unfold_locales, simp_all)
  qed

  text ‹
    An equivalence of monoidal categories is a monoidal functor whose underlying
    ordinary functor is also part of an ordinary equivalence of categories.
›

  locale equivalence_of_monoidal_categories =
    C: monoidal_category C TC αC ιC +
    D: monoidal_category D TD αD ιD +
    equivalence_of_categories C D F G η ε +
    monoidal_functor D TD αD ιD C TC αC ιC F φ
  for C :: "'c comp"                    (infixr ‹⋅C› 55)
  and TC :: "'c * 'c ⇒ 'c"
  and αC :: "'c * 'c * 'c ⇒ 'c"
  and ιC :: "'c"
  and D :: "'d comp"                    (infixr ‹⋅D› 55)
  and TD :: "'d * 'd ⇒ 'd"
  and αD :: "'d * 'd * 'd ⇒ 'd"
  and ιD :: "'d"
  and F :: "'d ⇒ 'c"
  and φ :: "'d * 'd ⇒ 'c"
  and ι :: 'c
  and G :: "'c ⇒ 'd"
  and η :: "'d ⇒ 'd"
  and ε :: "'c ⇒ 'c"

end