Theory EnrichedCategory

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

text ‹
  The notion of an enriched category cite"kelly-enriched-category"
  generalizes the concept of category by replacing the hom-sets of an ordinary category by
  objects of an arbitrary monoidal category M›.
  The choice, for each object a›, of a distinguished element id a : a → a› as an identity,
  is replaced by an arrow Id a : ℐ → Hom a a› of M›.  The composition operation is similarly
  replaced by a family of arrows Comp a b c : Hom B C ⊗ Hom A B → Hom A C› of M›.
  The identity and composition are required to satisfy unit and associativity laws which are
  expressed as commutative diagrams in M›.
›

theory EnrichedCategory
imports ClosedMonoidalCategory
begin

  (* TODO: Move this. *)
  context monoidal_category
  begin

    abbreviation ι'  ("ι-1")
    where "ι'  inv ι"

  end

  (* TODO: Put the following with the rest of the symmetric monoidal category development. *)
  context elementary_symmetric_monoidal_category
  begin

    lemma sym_unit:
    shows "ι  𝗌[, ] = ι"
      by (simp add: ι_def unitor_coherence unitor_coincidence(2))

    lemma sym_inv_unit:
    shows "𝗌[, ]  inv ι = inv ι"
      using sym_unit
      by (metis MC.unit_is_iso arr_inv cod_inv comp_arr_dom comp_cod_arr
          iso_cancel_left iso_is_arr)

  end

  section "Basic Definitions"

  (*
   * TODO: The arguments of Comp here are the reverse of the way they are in ConcreteCategory,
   * because I have found that ordering confusing.  At some point these should be made
   * consistent in the way that seems to work out the best.
   *)

  locale enriched_category =
    monoidal_category +
  fixes Obj :: "'o set"
  and Hom :: "'o  'o  'a"
  and Id :: "'o  'a"
  and Comp :: "'o  'o  'o  'a"
  assumes ide_Hom [intro, simp]: "a  Obj; b  Obj  ide (Hom a b)"
    and Id_in_hom [intro]: "a  Obj  «Id a :   Hom a a»"
    and Comp_in_hom [intro]: "a  Obj; b  Obj; c  Obj 
                                 «Comp a b c : Hom b c  Hom a b  Hom a c»"
    and Comp_Hom_Id: "a  Obj; b  Obj 
                        Comp a a b  (Hom a b  Id a) = 𝗋[Hom a b]"
    and Comp_Id_Hom: "a  Obj; b  Obj 
                        Comp a b b  (Id b  Hom a b) = 𝗅[Hom a b]"
    and Comp_assoc: "a  Obj; b  Obj; c  Obj; d  Obj 
                       Comp a b d  (Comp b c d  Hom a b) =
                       Comp a c d  (Hom c d  Comp a b c) 
                         𝖺[Hom c d, Hom b c, Hom a b]"

  text‹
    A functor from an enriched category A› to an enriched category B› consists of
    an object map Fo : ObjA → ObjB and a map Fa that assigns to each pair of objects
    a› b› in ObjA an arrow Fa a b : HomA a b → HomB (Fo a) (Fo b)› of the underlying
    monoidal category, subject to equations expressing that identities and composition
    are preserved.
  ›

  locale enriched_functor =
    monoidal_category C T α ι +
    A: enriched_category C T α ι ObjA HomA IdA CompA +
    B: enriched_category C T α ι ObjB HomB IdB CompB
  for C :: "'m  'm  'm"  (infixr  55)
  and T :: "'m × 'm  'm"
  and α :: "'m × 'm × 'm  'm"
  and ι :: "'m"
  and ObjA :: "'a set"
  and HomA :: "'a  'a  'm"
  and IdA :: "'a  'm"
  and CompA :: "'a  'a  'a  'm"
  and ObjB :: "'b set"
  and HomB :: "'b  'b  'm"
  and IdB :: "'b  'm"
  and CompB :: "'b  'b  'b  'm"
  and Fo :: "'a  'b"
  and Fa :: "'a  'a  'm" +
  assumes extensionality: "a  ObjA  b  ObjA  Fa a b = null"
  assumes preserves_Obj [intro]: "a  ObjA  Fo a  ObjB"
  and preserves_Hom: "a  ObjA; b  ObjA 
                         «Fa a b : HomA a b  HomB (Fo a) (Fo b)»"
  and preserves_Id: "a  ObjA  Fa a a  IdA a = IdB (Fo a)"
  and preserves_Comp: "a  ObjA; b  ObjA; c  ObjA 
                          CompB (Fo a) (Fo b) (Fo c)  T (Fa b c, Fa a b) =
                          Fa a c  CompA a b c"

  locale fully_faithful_enriched_functor =
    enriched_functor +
  assumes locally_iso: "a  ObjA; b  ObjA  iso (Fa a b)"

  text‹
    A natural transformation from an an enriched functor F = (Fo, Fa)› to an
    enriched functor G = (Go, Ga)› consists of a map τ› that assigns to each
    object a ∈ ObjA a ``component at a›'', which is an arrow τ a : ℐ → HomB (Fo a) (Go a)›,
    subject to an equation that expresses the naturality condition.
  ›

  locale enriched_natural_transformation =
    monoidal_category C T α ι +
    A: enriched_category C T α ι ObjA HomA IdA CompA +
    B: enriched_category C T α ι ObjB HomB IdB CompB +
    F: enriched_functor C T α ι
         ObjA HomA IdA CompA ObjB HomB IdB CompB Fo Fa +
    G: enriched_functor C T α ι
         ObjA HomA IdA CompA ObjB HomB IdB CompB Go Ga
  for C :: "'m  'm  'm"  (infixr  55)
  and T :: "'m × 'm  'm"
  and α :: "'m × 'm × 'm  'm"
  and ι :: "'m"
  and ObjA :: "'a set"
  and HomA :: "'a  'a  'm"
  and IdA :: "'a  'm"
  and CompA :: "'a  'a  'a  'm"
  and ObjB :: "'b set"
  and HomB :: "'b  'b  'm"
  and IdB :: "'b  'm"
  and CompB :: "'b  'b  'b  'm"
  and Fo :: "'a  'b"
  and Fa :: "'a  'a  'm"
  and Go :: "'a  'b"
  and Ga :: "'a  'a  'm"
  and τ :: "'a  'm" +
  assumes extensionality: "a  ObjA  τ a = null"
  and component_in_hom [intro]: "a  ObjA  «τ a :   HomB (Fo a) (Go a)»"
  and naturality: "a  ObjA; b  ObjA 
                     CompB (Fo a) (Fo b) (Go b)  (τ b  Fa a b)  𝗅-1[HomA a b] =
                     CompB (Fo a) (Go a) (Go b)  (Ga a b  τ a)  𝗋-1[HomA a b]"

  subsection "Self-Enrichment"

  context elementary_closed_monoidal_category
  begin

    text ‹
      Every closed monoidal category M› admits a structure of enriched category,
      where the exponentials in M› itself serve as the ``hom-objects''
      (\emph{cf.}~cite"kelly-enriched-category" Section 1.6).
      Essentially all the work in proving this theorem has already been done in
      @{theory EnrichedCategoryBasics.ClosedMonoidalCategory}.
    ›

    interpretation closed_monoidal_category
      using is_closed_monoidal_category by blast

    interpretation EC: enriched_category C T α ι Collect ide exp Id Comp
      using Id_in_hom Comp_in_hom Comp_unit_right Comp_unit_left Comp_assocECMC(2)
      by unfold_locales auto

    theorem is_enriched_in_itself:
    shows "enriched_category C T α ι (Collect ide) exp Id Comp"
      ..

    text‹
      The following mappings define a bijection between hom a b› and hom ℐ (exp a b)›.
      These have functorial properties which are encountered repeatedly.
    ›

    definition UP  ("_" [100] 100)
    where "t  if arr t then Curry[, dom t, cod t] (t  𝗅[dom t]) else null"

    definition DN
    where "DN a b t   if arr t then Uncurry[a, b] t  𝗅-1[a] else null"

    abbreviation DN'  ("_[_, _]" [100] 99)
    where "t[a, b]  DN a b t"

    lemma UP_DN:
    shows [intro]: "arr t  «t :   exp (dom t) (cod t)»"
    and [intro]: "ide a; ide b; «t :   exp a b»  «t[a, b]: a  b»"
    and [simp]: "arr t  (t)[dom t, cod t] = t"
    and [simp]: "ide a; ide b; «t :   exp a b»  (t[a, b]) = t"
      using UP_def DN_def Uncurry_Curry Curry_Uncurry [of  a b t]
            comp_assoc comp_arr_dom
      by auto

    lemma UP_simps [simp]:
    assumes "arr t"
    shows "arr (t)" and "dom (t) = " and "cod (t) = exp (dom t) (cod t)"
      using assms UP_DN by auto

    lemma DN_simps [simp]:
    assumes "ide a" and "ide b" and "arr t" and "dom t = " and "cod t = exp a b"
    shows "arr (t[a, b])" and "dom (t[a, b]) = a" and "cod (t[a, b]) = b"
      using assms UP_DN DN_def by auto

    lemma UP_ide:
    assumes "ide a"
    shows "a = Id a"
      using assms Id_def comp_cod_arr UP_def by auto

    lemma DN_Id:
    assumes "ide a"
    shows "(Id a)[a, a] = a"
      using assms Uncurry_Curry lunit_in_hom Id_def DN_def by auto

    lemma UP_comp:
    assumes "seq t u"
    shows "(t  u) = Comp (dom u) (cod u) (cod t)  (t  u)  ι-1"
    proof -
      have "Comp (dom u) (cod u) (cod t)  (t  u)  ι-1 =
            (Curry[exp (cod u) (cod t)  exp (dom u) (cod u), dom u, cod t]
              (eval (cod u) (cod t) 
                (exp (cod u) (cod t)  eval (dom u) (cod u)) 
                   𝖺[exp (cod u) (cod t), exp (dom u) (cod u), dom u]) 
                     (t  u))  ι-1"
        unfolding Comp_def
        using assms comp_assoc by simp
      also have "... =
            (Curry[  , dom u, cod t]
              ((eval (cod u) (cod t) 
                  (exp (cod u) (cod t)  eval (dom u) (cod u)) 
                     𝖺[exp (cod u) (cod t), exp (dom u) (cod u), dom u]) 
                       ((t  u)  dom u)))  ι-1"
        using assms
              comp_Curry_arr
                [of "dom u" "t  u"
                    "  " "exp (cod u) (cod t)  exp (dom u) (cod u)"
                    "eval (cod u) (cod t) 
                       (exp (cod u) (cod t)  eval (dom u) (cod u)) 
                         𝖺[exp (cod u) (cod t), exp (dom u) (cod u), dom u]"
                    "cod t"]
        by fastforce
      also have "... =
            Curry[  , dom u, cod t]
              (eval (cod u) (cod t) 
                 ((exp (cod u) (cod t)  eval (dom u) (cod u)) 
                    (t  u  dom u))  𝖺[, , dom u])  ι-1"
        using assms assoc_naturality [of "t" "u" "dom u"] comp_assoc by auto
      also have "... =
            Curry[  , dom u, cod t]
              (eval (cod u) (cod t) 
                 (exp (cod u) (cod t)  t  Uncurry[dom u, cod u] (u)) 
                    𝖺[, , dom u])  ι-1"
        using assms comp_cod_arr UP_DN interchange by auto
      also have "... =
            Curry[  , dom u, cod t]
              (eval (cod u) (cod t) 
                 (exp (cod u) (cod t)  t  u  𝗅[dom u]) 
                    𝖺[, , dom u])  ι-1"
        using assms Uncurry_Curry UP_def by auto
      also have "... =
            Curry[  , dom u, cod t]
              (eval (cod u) (cod t) 
                 (t  u  𝗅[dom u])  𝖺[, , dom u])  ι-1"
        using assms comp_cod_arr by auto
      also have "... =
            Curry[  , dom u, cod t]
              (eval (cod u) (cod t) 
                ((t  cod u)  (  u  𝗅[dom u])) 
                  𝖺[, , dom u])  ι-1"
        using assms comp_arr_dom [of "t" ] comp_cod_arr [of "u  𝗅[dom u]" "cod u"]
              interchange [of "t"   "cod u" "u  𝗅[dom u]"]
        by auto
      also have "... =
            Curry[, dom u, cod t]
              ((eval (cod u) (cod t) 
                 ((t  cod u)  (  u  𝗅[dom u])) 
                    𝖺[, , dom u])  (ι-1  dom u))"
      proof -
        have "«ι-1 :     »"
          using inv_in_hom unit_is_iso by blast
        thus ?thesis
          using assms comp_Curry_arr by fastforce
      qed
      also have "... =
            Curry[, dom u, cod t]
              ((Uncurry[cod u, cod t] (t))  (  u  𝗅[dom u]) 
                  𝖺[, , dom u]  (ι-1  dom u))"
        using comp_assoc by simp
      also have "... = Curry[, dom u, cod t] (Uncurry[cod u, cod t] (t)  (  u))"
      proof -
        have "(  u  𝗅[dom u])  𝖺[, , dom u]  (ι-1  dom u) =
              ((  u)  (  𝗅[dom u]))  𝖺[, , dom u]  (ι-1  dom u)"
          using assms by auto
        also have "... = (  u)  (  𝗅[dom u])  𝖺[, , dom u]  (ι-1  dom u)"
          using comp_assoc by simp
        also have "... = (  u)  (  𝗅[dom u])  (  𝗅-1[dom u])"
        proof -
          have "𝖺[, , dom u]  (ι-1  dom u) =   𝗅-1[dom u]"
          proof -
            have "𝖺[, , dom u]  (ι-1  dom u) =
                  inv ((ι  dom u)  𝖺-1[, , dom u])"
              using assms inv_inv inv_comp [of "𝖺-1[, , dom u]" "ι  dom u"]
                   inv_tensor [of ι "dom u"]
              by (metis ide_dom ide_is_iso ide_unity inv_ide iso_assoc iso_inv_iso
                  iso_is_arr lunit_char(2) seqE tensor_preserves_iso triangle
                  unit_is_iso unitor_coincidence(2))
            also have "... = inv (  𝗅[dom u])"
              using assms lunit_char [of "dom u"] by auto
            also have "... =   𝗅-1[dom u]"
              using assms inv_tensor by auto
            finally show ?thesis by blast
          qed
          thus ?thesis by simp
        qed
        also have "... = (  u)  (  dom u)"
          using assms
          by (metis comp_ide_self comp_lunit_lunit'(1) dom_comp ideD(1)
              ide_dom ide_unity interchange)
        also have "... =   u"
          using assms by blast
        finally have "(  u  𝗅[dom u])  𝖺[, , dom u]  (ι-1  dom u) =   u"
          by blast
        thus ?thesis by argo
      qed
      also have "... = Curry[, dom u, cod t] ((t  𝗅[cod u])  (  u))"
        using assms Uncurry_Curry UP_def by auto
      also have "... = Curry[, dom u, cod t] (t  u  𝗅[dom u])"
        using assms comp_assoc lunit_naturality by auto
      also have "... = (t  u)"
        using assms comp_assoc UP_def by simp
      finally show ?thesis by simp
    qed

  end

  section "Underlying Category, Functor, and Natural Transformation"

  subsection "Underlying Category"

  text‹
     The underlying category (\emph{cf.}~cite"kelly-enriched-category" Section 1.3)
     of an enriched category has as its arrows from a› to b› the arrows ℐ → Hom a b› of M›
     (\emph{i.e.}~the points of Hom a b›). The identity at a› is Id a›.  The composition of
     arrows f› and g› is given by the formula: Comp a b c ⋅ (g ⊗ f) ⋅ ι-1.
  ›

  locale underlying_category =
    M: monoidal_category +
    A: enriched_category
  begin

    sublocale concrete_category Obj λa b. M.hom  (Hom a b) Id
                λc b a g f. Comp a b c  (g  f)  ι-1
    proof
      show "a. a  Obj  Id a  M.hom  (Hom a a)"
        using A.Id_in_hom by blast
      show 1: "a b c f g.
                 a  Obj; b  Obj; c  Obj;
                  f  M.hom  (Hom a b); g  M.hom  (Hom b c)
                      Comp a b c  (g  f)  ι-1  M.hom  (Hom a c)"
        using A.Comp_in_hom M.inv_in_hom M.unit_is_iso M.comp_in_homI
              M.unit_in_hom
        apply auto[1]
        apply (intro M.comp_in_homI)
        by auto
      show "a b f. a  Obj; b  Obj; f  M.hom  (Hom a b)
                        Comp a a b  (f  Id a)  ι-1 = f"
      proof -
        fix a b f
        assume a: "a  Obj" and b: "b  Obj" and f: "f  M.hom  (Hom a b)"
        show "Comp a a b  (f  Id a)  ι-1 = f"
        proof -
          have "Comp a a b  (f  Id a)  ι-1 = (Comp a a b  (f  Id a))  ι-1"
            using M.comp_assoc by simp
          also have "... = (Comp a a b  (Hom a b  Id a)  (f  ))  ι-1"
            using a f M.comp_arr_dom M.comp_cod_arr A.Id_in_hom
                  M.in_homE M.interchange mem_Collect_eq
            by metis
          also have "... = (𝗋[Hom a b]  (f  ))  ι-1"
            using a b f A.Comp_Hom_Id M.comp_assoc by metis
          also have "... = (f  𝗋[])  ι-1"
            using f M.runit_naturality by fastforce
          also have "... = f  ι  ι-1"
            by (simp add: M.unitor_coincidence(2) M.comp_assoc)
          also have "... = f"
            using f M.comp_arr_dom M.comp_arr_inv' M.unit_is_iso by auto
          finally show "Comp a a b  (f  Id a)  ι-1 = f" by blast
        qed
      qed
      show "a b f. a  Obj; b  Obj; f  M.hom  (Hom a b)
                        Comp a b b  (Id b  f)  ι-1 = f"
      proof -
        fix a b f
        assume a: "a  Obj" and b: "b  Obj" and f: "f  M.hom  (Hom a b)"
        show "Comp a b b  (Id b  f)  ι-1 = f"
        proof -
          have "Comp a b b  (Id b  f)  ι-1 = (Comp a b b  (Id b  f))  ι-1"
            using M.comp_assoc by simp
          also have "... = (Comp a b b  (Id b  Hom a b)  (  f))  ι-1"
            using a b f M.comp_arr_dom M.comp_cod_arr A.Id_in_hom
                  M.in_homE M.interchange mem_Collect_eq
            by metis
          also have "... = (𝗅[Hom a b]  (  f))  ι-1"
            using a b A.Comp_Id_Hom M.comp_assoc by metis
          also have "... = (f  𝗅[])  ι-1"
            using a b f M.lunit_naturality [of f] by auto
          also have "... = f  ι  ι-1"
            by (simp add: M.unitor_coincidence(1) M.comp_assoc)
          also have "... = f"
            using M.comp_arr_dom M.comp_arr_inv' M.unit_is_iso f by auto
          finally show "Comp a b b  (Id b  f)  ι-1 = f" by blast
        qed
      qed
      show "a b c d f g h.
                a  Obj; b  Obj; c  Obj; d  Obj;
                 f  M.hom  (Hom a b); g  M.hom  (Hom b c);
                 h  M.hom  (Hom c d)
                     Comp a c d  (h  Comp a b c  (g  f)  ι-1)  ι-1 =
                        Comp a b d  (Comp b c d  (h  g)  ι-1  f)  ι-1"
      proof -
        fix a b c d f g h
        assume a: "a  Obj" and b: "b  Obj" and c: "c  Obj" and d: "d  Obj"
        assume f: "f  M.hom  (Hom a b)" and g: "g  M.hom  (Hom b c)"
        and h: "h  M.hom  (Hom c d)"
        have "Comp a c d  (h  Comp a b c  (g  f)  ι-1)  ι-1 =
              Comp a c d 
                ((Hom c d  Comp a b c)  (h  (g  f)  ι-1))  ι-1"
          using a b c d f g h 1 M.interchange A.ide_Hom M.comp_ide_arr M.comp_cod_arr
                M.in_homE mem_Collect_eq
          by metis
        also have "... = Comp a c d 
                           ((Hom c d  Comp a b c) 
                               (𝖺[Hom c d, Hom b c, Hom a b] 
                                  𝖺-1[Hom c d, Hom b c, Hom a b])) 
                                 (h  (g  f)  ι-1)  ι-1"
        proof -
          have "(Hom c d  Comp a b c) 
                  (𝖺[Hom c d, Hom b c, Hom a b] 
                     𝖺-1[Hom c d, Hom b c, Hom a b]) =
                Hom c d  Comp a b c"
            using a b c d
            by (metis A.Comp_in_hom A.ide_Hom M.comp_arr_ide
                M.comp_assoc_assoc'(1) M.ide_in_hom M.interchange M.seqI'
                M.tensor_preserves_ide)
          thus ?thesis
            using M.comp_assoc by force
        qed
        also have "... = (Comp a c d  (Hom c d  Comp a b c) 
                           𝖺[Hom c d, Hom b c, Hom a b]) 
                             (𝖺-1[Hom c d, Hom b c, Hom a b] 
                               (h  (g  f)  ι-1)) 
                                 ι-1"
          using M.comp_assoc by auto
        also have "... = (Comp a b d  (Comp b c d  Hom a b)) 
                           (𝖺-1[Hom c d, Hom b c, Hom a b]  (h  (g  f)  ι-1))  ι-1"
          using a b c d A.Comp_assoc by auto
        also have "... = (Comp a b d  (Comp b c d  Hom a b)) 
                           (𝖺-1[Hom c d, Hom b c, Hom a b]  (h  (g  f))) 
                             (  ι-1)  ι-1"
        proof -
          have "h  (g  f)  ι-1 = (h  (g  f))  (  ι-1)"
          proof -
            have "M.seq h "
              using h by auto
            moreover have "M.seq (g  f) ι-1"
              using f g M.inv_in_hom M.unit_is_iso by blast
            ultimately show ?thesis
              using a b c d f g h M.interchange M.comp_arr_ide M.ide_unity by metis
          qed
          thus ?thesis
            using M.comp_assoc by simp
        qed
        also have "... = (Comp a b d  (Comp b c d  Hom a b)) 
                           ((h  g)  f)  𝖺-1[, , ]  (  ι-1)  ι-1"
          using f g h M.assoc'_naturality
          by (metis M.comp_assoc M.in_homE mem_Collect_eq)
        also have "... = (Comp a b d  (Comp b c d  Hom a b)) 
                           (((h  g)  f)  (ι-1  ))  ι-1"
        proof -
          have "𝖺-1[, , ]  (  ι-1)  ι-1 = (ι-1  )  ι-1"
            using M.unitor_coincidence
            by (metis (full_types) M.L.preserves_inv M.L.preserves_iso
                M.R.preserves_inv M.arrI M.arr_tensor M.comp_assoc M.ideD(1)
                M.ide_unity M.inv_comp M.iso_assoc M.unit_in_hom_ax
                M.unit_is_iso M.unit_triangle(1))
          thus ?thesis
            using M.comp_assoc by simp
        qed
        also have "... = Comp a b d 
                           ((Comp b c d  Hom a b)  ((h  g)  ι-1  f))  ι-1"
        proof -
          have "((h  g)  f)  (ι-1  ) = (h  g)  ι-1  f"
          proof -
            have "M.seq (h  g) ι-1"
              using g h M.inv_in_hom M.unit_is_iso by blast
            moreover have "M.seq f "
              using M.ide_in_hom M.ide_unity f by blast
            ultimately show ?thesis
              using f g h M.interchange M.comp_arr_ide M.ide_unity by metis
          qed
          thus ?thesis
            using M.comp_assoc by auto
        qed
        also have "... = Comp a b d  (Comp b c d  (h  g)  ι-1  f)  ι-1"
           using b c d f g h 1 M.in_homE mem_Collect_eq M.comp_cod_arr
                 M.interchange A.ide_Hom M.comp_ide_arr
           by metis
        finally show "Comp a c d  (h  Comp a b c  (g  f)  ι-1)  ι-1 =
                      Comp a b d  (Comp b c d  (h  g)  ι-1  f)  ι-1"
          by blast
      qed
    qed

    abbreviation comp  (infixr "0" 55)
    where "comp  COMP"

    lemma hom_char:
    assumes "a  Obj" and "b  Obj"
    shows "hom (MkIde a) (MkIde b) = MkArr a b ` M.hom  (Hom a b)"
    proof
      show "hom (MkIde a) (MkIde b)  MkArr a b ` M.hom  (Hom a b)"
      proof
        fix t
        assume t: "t  hom (MkIde a) (MkIde b)"
        have "t = MkArr a b (Map t)"
          using t MkArr_Map dom_char cod_char by fastforce
        moreover have "Map t  M.hom  (Hom a b)"
          using t arr_char dom_char cod_char by fastforce
        ultimately show "t  MkArr a b ` M.hom  (Hom a b)" by simp
      qed
      show "MkArr a b ` M.hom  (Hom a b)  hom (MkIde a) (MkIde b)"
        using assms MkArr_in_hom by blast
    qed

  end

  subsection "Underlying Functor"

  text‹
     The underlying functor of an enriched functor F : A ⟶ B›
     takes an arrow «f : a → a'»› of the underlying category A0
     (\emph{i.e.}~an arrow «ℐ → Hom a a'»› of M›)
     to the arrow «Fa a a' ⋅ f : Fo a → Fo a'»› of B0
     (\emph{i.e.} the arrow «Fa a a' ⋅ f : ℐ → Hom (Fo a) (Fo a')»› of M›).
  ›

  locale underlying_functor =
    enriched_functor
  begin

    sublocale A0: underlying_category C T α ι ObjA HomA IdA CompA ..
    sublocale B0: underlying_category C T α ι ObjB HomB IdB CompB ..

    notation A0.comp  (infixr "A0" 55)
    notation B0.comp  (infixr "B0" 55)

    definition map0
    where "map0 f = (if A0.arr f
                     then B0.MkArr (Fo (A0.Dom f)) (Fo (A0.Cod f))
                            (Fa (A0.Dom f) (A0.Cod f)  A0.Map f)
                     else B0.null)"

    sublocale "functor" A0.comp B0.comp map0
    proof
      fix f
      show "¬ A0.arr f  map0 f = B0.null"
        using map0_def by simp
      show 1: "f. A0.arr f  B0.arr (map0 f)"
      proof -
        fix f
        assume f: "A0.arr f"
        have "B0.arr (B0.MkArr (Fo (A0.Dom f)) (Fo (A0.Cod f))
                     (Fa (A0.Dom f) (A0.Cod f)  A0.Map f))"
          using f preserves_Hom A0.Dom_in_Obj A0.Cod_in_Obj A0.arrE
          by (metis (mono_tags, lifting) B0.arr_MkArr comp_in_homI
              mem_Collect_eq preserves_Obj)
        thus "B0.arr (map0 f)"
          using f map0_def by simp
      qed
      show "A0.arr f  B0.dom (map0 f) = map0 (A0.dom f)"
        using 1 A0.dom_char B0.dom_char preserves_Id A0.arr_dom_iff_arr
              map0_def A0.Dom_in_Obj
        by auto
      show "A0.arr f  B0.cod (map0 f) = map0 (A0.cod f)"
        using 1 A0.cod_char B0.cod_char preserves_Id A0.arr_cod_iff_arr
              map0_def A0.Cod_in_Obj
        by auto
      fix g
      assume fg: "A0.seq g f"
      show "map0 (g A0 f) = map0 g B0 map0 f"
      proof -
        have "B0.MkArr (Fo (A0.Dom (g A0 f))) (Fo (B0.Cod (g A0 f)))
                       (Fa (A0.Dom (g A0 f))
                       (B0.Cod (g A0 f))  B0.Map (g A0 f)) =
              B0.MkArr (Fo (A0.Dom g)) (Fo (B0.Cod g))
                       (Fa (A0.Dom g) (B0.Cod g)  B0.Map g) B0
                B0.MkArr (Fo (A0.Dom f)) (Fo (B0.Cod f))
                         (Fa (A0.Dom f) (B0.Cod f)  B0.Map f)"
        proof -
          have 2: "B0.arr (B0.MkArr (Fo (A0.Dom f)) (Fo (A0.Dom g))
                          (Fa (A0.Dom f) (A0.Cod f)  A0.Map f))"
            using fg 1 A0.seq_char map0_def by auto
          have 3: "B0.arr (B0.MkArr (Fo (A0.Dom g)) (Fo (A0.Cod g))
                          (Fa (A0.Dom g) (A0.Cod g)  A0.Map g))"
            using fg 1 A0.seq_char map0_def by metis
          have "B0.MkArr (Fo (A0.Dom g)) (Fo (B0.Cod g))
                         (Fa (A0.Dom g) (B0.Cod g)  B0.Map g) B0
                  B0.MkArr (Fo (A0.Dom f)) (Fo (B0.Cod f))
                           (Fa (A0.Dom f) (B0.Cod f)  B0.Map f) =
                B0.MkArr (Fo (A0.Dom f)) (Fo (A0.Cod g))
                         (CompB (Fo (A0.Dom f)) (Fo (A0.Dom g)) (Fo (A0.Cod g)) 
                            (Fa (A0.Dom g) (A0.Cod g)  A0.Map g 
                             Fa (A0.Dom f) (A0.Cod f)  A0.Map f) 
                               ι-1)"
            using fg 2 3 A0.seq_char B0.comp_MkArr by simp
          moreover
          have "CompB (Fo (A0.Dom f)) (Fo (A0.Dom g)) (Fo (A0.Cod g)) 
                      (Fa (A0.Dom g) (A0.Cod g)  A0.Map g 
                       Fa (A0.Dom f) (A0.Cod f)  A0.Map f)  ι-1 =
                Fa (A0.Dom (g A0 f)) (B0.Cod (g A0 f))  B0.Map (g A0 f)"
          proof -
            have "CompB (Fo (A0.Dom f)) (Fo (A0.Dom g)) (Fo (A0.Cod g)) 
                           (Fa (A0.Dom g) (A0.Cod g)  A0.Map g 
                            Fa (A0.Dom f) (A0.Cod f)  A0.Map f)  ι-1 =
                  CompB (Fo (A0.Dom f)) (Fo (A0.Dom g)) (Fo (A0.Cod g)) 
                           ((Fa (A0.Dom g) (A0.Cod g)  Fa (A0.Dom f) (A0.Cod f)) 
                            (A0.Map g  A0.Map f))  ι-1"
              using fg preserves_Hom
                    interchange [of "Fa (A0.Dom g) (A0.Cod g)" "A0.Map g"
                                    "Fa (A0.Dom f) (A0.Cod f)" "A0.Map f"]
              by (metis A0.arrE A0.seqE seqI' mem_Collect_eq)
            also have "... =
                  (CompB (Fo (A0.Dom f)) (Fo (A0.Dom g)) (Fo (A0.Cod g)) 
                           (Fa (A0.Dom g) (A0.Cod g)  Fa (A0.Dom f) (A0.Cod f))) 
                    (A0.Map g  A0.Map f)  ι-1"
              using comp_assoc by auto
           also have "... = (Fa (A0.Dom f) (B0.Cod g) 
                               CompA (A0.Dom f) (A0.Dom g) (B0.Cod g)) 
                               (A0.Map g  A0.Map f)  ι-1"
              using fg A0.seq_char preserves_Comp A0.Dom_in_Obj A0.Cod_in_Obj
              by auto
           also have "... = Fa (A0.Dom (g A0 f)) (B0.Cod (g A0 f)) 
                              CompA (A0.Dom f) (A0.Dom g) (B0.Cod g) 
                                (A0.Map g  A0.Map f)  ι-1"
             using fg comp_assoc A0.seq_char by simp
           also have "... = Fa (A0.Dom (g A0 f)) (B0.Cod (g A0 f)) 
                              B0.Map (g A0 f)"
             using A0.Map_comp A0.seq_char fg by presburger
           finally show ?thesis by blast
          qed
          ultimately show ?thesis
            using A0.seq_char fg by auto
        qed
        thus ?thesis
          using fg map0_def B0.comp_MkArr by auto
      qed
    qed

    proposition is_functor:
    shows "functor A0.comp B0.comp map0"
      ..

  end

  subsection "Underlying Natural Transformation"

  text‹
    The natural transformation underlying an enriched natural transformation τ›
    has components that are essentially those of τ›, except that we have to bother
    ourselves about coercions between types.
  ›

  locale underlying_natural_transformation =
    enriched_natural_transformation
  begin

    sublocale A0: underlying_category C T α ι ObjA HomA IdA CompA ..
    sublocale B0: underlying_category C T α ι ObjB HomB IdB CompB ..
    sublocale F0: underlying_functor C T α ι
                    ObjA HomA IdA CompA ObjB HomB IdB CompB Fo Fa ..
    sublocale G0: underlying_functor C T α ι
                    ObjA HomA IdA CompA ObjB HomB IdB CompB Go Ga ..

    definition mapobj
    where "mapobj a 
           B0.MkArr (B0.Dom (F0.map0 a)) (B0.Dom (G0.map0 a))
             (τ (A0.Dom a))"  

    sublocale τ: NaturalTransformation.transformation_by_components
                   A0.comp B0.comp F0.map0 G0.map0 mapobj
    proof
      show "a. A0.ide a  B0.in_hom (mapobj a) (F0.map0 a) (G0.map0 a)"
        unfolding mapobj_def
        using A0.Dom_in_Obj B0.ide_charCC F0.map0_def G0.map0_def
              F0.preserves_ide G0.preserves_ide component_in_hom
        by auto
      show "f. A0.arr f 
                  mapobj (A0.cod f) B0 F0.map0 f =
                  G0.map0 f B0 mapobj (A0.dom f)"
      proof -
        fix f
        assume f: "A0.arr f"
        show "mapobj (A0.cod f) B0 F0.map0 f =
              G0.map0 f B0 mapobj (A0.dom f)"
        proof (intro B0.arr_eqI)
          show 1: "B0.seq (mapobj (A0.cod f)) (F0.map0 f)"
            using A0.ide_cod
                  a. A0.ide a 
                          B0.in_hom (mapobj a) (F0.map0 a) (G0.map0 a) f
            by blast
          show 2: "B0.seq (G0.map0 f) (mapobj (A0.dom f))"
            using A0.ide_dom
                  a. A0.ide a 
                          B0.in_hom (mapobj a) (F0.map0 a) (G0.map0 a) f
            by blast
          show "B0.Dom (mapobj (A0.cod f) B0 F0.map0 f) =
                B0.Dom (G0.map0 f B0 mapobj (A0.dom f))"
            using f 1 2 B0.comp_char [of "mapobj (A0.cod f)" "F0.map0 f"]
                  B0.comp_char [of "G0.map0 f" "mapobj (A0.dom f)"]
                  F0.map0_def G0.map0_def mapobj_def
            by simp
          show "B0.Cod (mapobj (A0.cod f) B0 F0.map0 f) =
                B0.Cod (G0.map0 f B0 mapobj (A0.dom f))"
            using f 1 2 B0.comp_char [of "mapobj (A0.cod f)" "F0.map0 f"]
                  B0.comp_char [of "G0.map0 f" "mapobj (A0.dom f)"]
                  F0.map0_def G0.map0_def mapobj_def
            by simp
          show "B0.Map (mapobj (A0.cod f) B0 F0.map0 f) =
                B0.Map (G0.map0 f B0 mapobj (A0.dom f))"
          proof -
            have "CompB (Fo (A0.Dom f)) (Fo (A0.Cod f)) (Go (A0.Cod f)) 
                    (τ (A0.Cod f)  Fa (A0.Dom f) (A0.Cod f)  A0.Map f)  ι-1 =
                  CompB (Fo (A0.Dom f)) (Go (A0.Dom f)) (Go (A0.Cod f)) 
                    (Ga (A0.Dom f) (A0.Cod f)  A0.Map f  τ (A0.Dom f))  ι-1"
            proof -
              have "CompB (Fo (A0.Dom f)) (Fo (A0.Cod f)) (Go (A0.Cod f)) 
                      (τ (A0.Cod f)  Fa (A0.Dom f) (A0.Cod f)  A0.Map f)  ι-1 =
                    CompB (Fo (A0.Dom f)) (Fo (A0.Cod f)) (Go (A0.Cod f)) 
                      ((τ (A0.Cod f)  Fa (A0.Dom f) (A0.Cod f))  (  A0.Map f)) 
                         ι-1"
              proof -
                have "τ (A0.Cod f)  Fa (A0.Dom f) (A0.Cod f)  A0.Map f =
                      (τ (A0.Cod f)  Fa (A0.Dom f) (A0.Cod f))  (  A0.Map f)"
                proof -
                  have "seq (τ (A0.Cod f)) "
                    using f seqI component_in_hom
                    by (metis (no_types, lifting) A0.Cod_in_Obj ide_char
                        ide_unity in_homE)
                  moreover have "seq (Fa (A0.Dom f) (B0.Cod f)) (B0.Map f)"
                    using f A0.Map_in_Hom A0.Cod_in_Obj A0.Dom_in_Obj
                          F.preserves_Hom in_homE
                    by blast
                  ultimately show ?thesis
                    using f component_in_hom interchange comp_arr_dom by auto
                qed
                thus ?thesis by simp
              qed
              also have "... =
                    CompB (Fo (A0.Dom f)) (Fo (A0.Cod f)) (Go (A0.Cod f)) 
                      ((τ (B0.Cod f)  Fa (A0.Dom f) (B0.Cod f)) 
                         (𝗅-1[HomA (A0.Dom f) (B0.Cod f)] 
                            𝗅[HomA (A0.Dom f) (B0.Cod f)]) 
                           (  B0.Map f))  ι-1"
              proof -
                have "(𝗅-1[HomA (A0.Dom f) (B0.Cod f)] 
                         𝗅[HomA (A0.Dom f) (B0.Cod f)]) 
                        (  B0.Map f) =
                        B0.Map f"
                  using f comp_lunit_lunit'(2)
                  by (metis (no_types, lifting) A.ide_Hom A0.arrE comp_cod_arr
                      comp_ide_self ideD(1) ide_unity interchange in_homE
                      mem_Collect_eq)
                thus ?thesis by simp
              qed
              also have "... =
                    (CompB (Fo (A0.Dom f)) (Fo (B0.Cod f)) (Go (B0.Cod f)) 
                       (τ (B0.Cod f)  Fa (A0.Dom f) (B0.Cod f)) 
                          𝗅-1[HomA (A0.Dom f) (B0.Cod f)]) 
                      𝗅[HomA (A0.Dom f) (B0.Cod f)]  (  B0.Map f)  ι-1"
                using comp_assoc by simp
              also have "... =
                    CompB (Fo (A0.Dom f)) (Go (A0.Dom f)) (Go (B0.Cod f)) 
                      (Ga (A0.Dom f) (B0.Cod f)  τ (A0.Dom f)) 
                         𝗋-1[HomA (A0.Dom f) (B0.Cod f)] 
                           (𝗅[HomA (A0.Dom f) (B0.Cod f)]  (  B0.Map f))  ι-1"
                using f A0.Cod_in_Obj A0.Dom_in_Obj naturality comp_assoc by simp
              also have "... =
                    CompB (Fo (A0.Dom f)) (Go (A0.Dom f)) (Go (B0.Cod f)) 
                     (Ga (A0.Dom f) (B0.Cod f)  τ (A0.Dom f)) 
                        𝗋-1[HomA (A0.Dom f) (B0.Cod f)]  (B0.Map f  𝗅[])  ι-1"
                using f lunit_naturality A0.Map_in_Hom by force
              also have "... =
                    CompB (Fo (A0.Dom f)) (Go (A0.Dom f)) (Go (B0.Cod f)) 
                      (Ga (A0.Dom f) (B0.Cod f)  τ (A0.Dom f)) 
                        𝗋-1[HomA (A0.Dom f) (B0.Cod f)]  B0.Map f"
              proof -
                have "ι  ι-1 = "
                  using comp_arr_inv' unit_is_iso by blast
                moreover have "«B0.Map f :   HomA (A0.Dom f) (B0.Cod f)»"
                  using f A0.Map_in_Hom by blast
                ultimately show ?thesis
                  using f comp_arr_dom unitor_coincidence(1) comp_assoc by auto
              qed
              also have "... =
                    CompB (Fo (A0.Dom f)) (Go (A0.Dom f)) (Go (B0.Cod f)) 
                      (Ga (A0.Dom f) (B0.Cod f)  τ (A0.Dom f)) 
                        (B0.Map f  )  𝗋-1[]"
                using f runit'_naturality A0.Map_in_Hom by force
              also have "... =
                    CompB (Fo (A0.Dom f)) (Go (A0.Dom f)) (Go (B0.Cod f)) 
                      ((Ga (A0.Dom f) (B0.Cod f)  τ (A0.Dom f)) 
                        (B0.Map f  ))  ι-1"
                using unitor_coincidence comp_assoc by simp
              also have "... =
                    CompB (Fo (A0.Dom f)) (Go (A0.Dom f)) (Go (B0.Cod f)) 
                      (Ga (A0.Dom f) (B0.Cod f)  A0.Map f  τ (A0.Dom f))  ι-1"
              proof -
                have "seq (Ga (A0.Dom f) (B0.Cod f)) (B0.Map f)"
                  using f A0.Map_in_Hom A0.Cod_in_Obj A0.Dom_in_Obj G.preserves_Hom
                  by fast
                moreover have "seq (τ (A0.Dom f)) "
                  using f seqI component_in_hom
                  by (metis (no_types, lifting) A0.Dom_in_Obj ide_char
                      ide_unity in_homE)
                ultimately show ?thesis
                  using f comp_arr_dom interchange by auto
              qed
              finally show ?thesis by simp
            qed
            thus ?thesis
              using f 1 2 B0.comp_char [of "mapobj (A0.cod f)" "F0.map0 f"]
                    B0.comp_char [of "G0.map0 f" "mapobj (A0.dom f)"]  
                    F0.map0_def G0.map0_def mapobj_def
              by simp
          qed
        qed
      qed
    qed

    proposition is_natural_transformation:
    shows "natural_transformation A0.comp B0.comp F0.map0 G0.map0 τ.map"
      ..

  end

  subsection "Self-Enriched Case"

  text‹
    Here we show that a closed monoidal category C›, regarded as a category enriched
    in itself, it is isomorphic to its own underlying category.  This is useful,
    because it is somewhat less cumbersome to work directly in the category C›
    than in the higher-type version that results from the underlying category construction.
    Kelly often regards these two categories as identical.
  ›

  locale self_enriched_category =
    elementary_closed_monoidal_category +
    enriched_category C T α ι Collect ide exp Id Comp
  begin

    sublocale UC: underlying_category C T α ι Collect ide exp Id Comp ..

    abbreviation toUC
    where "toUC g  if arr g
                     then UC.MkArr (dom g) (cod g) (g)
                     else UC.null"

    lemma toUC_simps [simp]:
    assumes "arr f"
    shows "UC.arr (toUC f)"
    and "UC.dom (toUC f) = toUC (dom f)"
    and "UC.cod (toUC f) = toUC (cod f)"
      using assms UC.arr_char UC.dom_char UC.cod_char UP_def
            comp_cod_arr Id_def
      by auto

    lemma toUC_in_hom [intro]:
    assumes "arr f"
    shows "UC.in_hom (toUC f) (UC.MkIde (dom f)) (UC.MkIde (cod f))"
      using assms toUC_simps by fastforce

    sublocale toUC: "functor" C UC.comp toUC
        using toUC_simps UP_comp UC.COMP_def
        by unfold_locales auto

    abbreviation frmUC
    where "frmUC g  if UC.arr g
                       then (UC.Map g)[UC.Dom g, UC.Cod g]
                       else null"

    lemma frmUC_simps [simp]:
    assumes "UC.arr f"
    shows "arr (frmUC f)"
    and "dom (frmUC f) = frmUC (UC.dom f)"
    and "cod (frmUC f) = frmUC (UC.cod f)"
      using assms UC.arr_char UC.dom_char UC.cod_char Uncurry_Curry
            Id_def lunit_in_hom DN_def
      by auto

    lemma frmUC_in_hom [intro]:
    assumes "UC.in_hom f a b"
    shows "«frmUC f : frmUC a  frmUC b»"
      using assms frmUC_simps by blast

    lemma DN_Map_comp:
    assumes "UC.seq g f"
    shows "(UC.Map (UC.comp g f))[UC.Dom f, UC.Cod g] =
           (UC.Map g)[UC.Dom g, UC.Cod g] 
             (UC.Map f)[UC.Dom f, UC.Cod f]"
    proof -
      have "(UC.Map (UC.comp g f))[UC.Dom f, UC.Cod g] =
            ((UC.Map (UC.comp g f))[UC.Dom f, UC.Cod g])
                         [UC.Dom f, UC.Cod g]"
        using assms UC.arr_char UC.seq_char [of g f] by fastforce
      also have "... = ((UC.Map g)[UC.Dom g, UC.Cod g] 
                          (UC.Map f)[UC.Dom f, UC.Cod f])
                             [UC.Dom f, UC.Cod g]"
      proof -
        have "((UC.Map (UC.comp g f))[UC.Dom f, UC.Cod g]) =
               UC.Map (UC.comp g f)"
          using assms UC.arr_char UC.seq_char [of g f] by fastforce
        also have "... = Comp (UC.Dom f) (UC.Dom g) (UC.Cod g) 
                           (UC.Map g  UC.Map f)  ι-1"
          using assms UC.Map_comp UC.seq_char by blast
        also have "... = Comp (UC.Dom f) (UC.Dom g) (UC.Cod g) 
                           (((UC.Map g)[UC.Dom g, UC.Cod g]) 
                                ((UC.Map f)[UC.Dom f, UC.Cod f]))  ι-1"
          using assms UC.seq_char UC.arr_char by auto
        also have "... = ((UC.Map g)[UC.Dom g, UC.Cod g] 
                           (UC.Map f)[UC.Dom f, UC.Cod f])"
        proof -
          have "dom ((UC.Map f)[UC.Dom f, UC.Cod f]) = UC.Dom f"
            using assms DN_Id UC.Dom_in_Obj frmUC_simps(2) by auto
          moreover have "cod ((UC.Map f)[UC.Dom f, UC.Cod f]) = UC.Cod f"
            using assms DN_Id UC.Cod_in_Obj frmUC_simps(3) by auto
          moreover have "seq ((UC.Map g)[UC.Cod f, UC.Cod g])
                             ((UC.Map f)[UC.Dom f, UC.Cod f])"
            using assms frmUC_simps(1-3) UC.seq_char
            apply (intro seqI)
              apply auto[3]
            by metis+
          ultimately show ?thesis
            using assms UP_comp UP_DN(2) UC.arr_char UC.seq_char
                  in_homE seqI
            by auto
        qed
        finally show ?thesis by simp
      qed
      also have "... = (UC.Map g)[UC.Dom g, UC.Cod g] 
                         (UC.Map f)[UC.Dom f, UC.Cod f]"
      proof -
        have 2: "seq ((UC.Map g)[UC.Dom g, UC.Cod g])
                     ((UC.Map f)[UC.Dom f, UC.Cod f])"
          using assms frmUC_simps(1-3) UC.seq_char
          apply (elim UC.seqE, intro seqI)
            apply auto[3]
          by metis+
        moreover have "dom ((UC.Map g)[UC.Dom g, UC.Cod g] 
                              (UC.Map f)[UC.Dom f, UC.Cod f]) =
                       UC.Dom f"
          using assms 2 UC.Dom_comp UC.arr_char [of f] by auto
        moreover have "cod ((UC.Map g)[UC.Dom g, UC.Cod g] 
                               (UC.Map f)[UC.Dom f, UC.Cod f]) =
                       UC.Cod g"
          using assms 2 UC.Cod_comp UC.arr_char [of g] by auto
        ultimately show ?thesis
          using assms
                UP_DN(3) [of "(UC.Map g)[UC.Dom g, UC.Cod g] 
                                 (UC.Map f)[UC.Dom f, UC.Cod f]"]
          by simp
      qed
      finally show ?thesis by blast
    qed

    sublocale frmUC: "functor" UC.comp C frmUC
    proof
      show "f. ¬ UC.arr f  frmUC f = null"
        by simp
      show "f. UC.arr f  arr (frmUC f)"
        using UC.arr_char frmUC_simps(1) by blast
      show "f. UC.arr f  dom (frmUC f) = frmUC (UC.dom f)"
        using frmUC_simps(2) by blast
      show "f. UC.arr f  cod (frmUC f) = frmUC (UC.cod f)"
        using frmUC_simps(3) by blast
      fix f g
      assume fg: "UC.seq g f"
      show "frmUC (UC.comp g f) = frmUC g  frmUC f"
        using fg UC.seq_char DN_Map_comp by auto
    qed

    sublocale inverse_functors UC.comp C toUC frmUC
    proof
      show "frmUC  toUC = map"
        using is_extensional comp_arr_dom comp_assoc Uncurry_Curry by auto
      interpret to_frm: composite_functor UC.comp C UC.comp frmUC toUC ..
      show "toUC  frmUC = UC.map"
      proof
        fix f
        show "(toUC  frmUC) f = UC.map f"
        proof (cases "UC.arr f")
          show "¬ UC.arr f  ?thesis"
            using UC.is_extensional by auto
          assume f: "UC.arr f"
          show ?thesis
          proof (intro UC.arr_eqI)
            show "UC.arr ((toUC  frmUC) f)"
              using f by blast
            show "UC.arr (UC.map f)"
              using f by blast
            show "UC.Dom ((toUC  frmUC) f) = UC.Dom (UC.map f)"
              using f UC.Dom_in_Obj frmUC.preserves_arr UC.arr_char [of f]
              by auto
            show "UC.Cod (to_frm.map f) = UC.Cod (UC.map f)"
              using f UC.arr_char [of f] by auto
            show "UC.Map (to_frm.map f) = UC.Map (UC.map f)"
              using f UP_DN UC.arr_char [of f] by auto
          qed
        qed
      qed
    qed

    lemma inverse_functors_toUC_frmUC:
    shows "inverse_functors UC.comp C toUC frmUC"
      ..

    corollary enriched_category_isomorphic_to_underlying_category:
    shows "isomorphic_categories UC.comp C"
      using inverse_functors_toUC_frmUC
      by unfold_locales blast

  end

  section "Opposite of an Enriched Category"

  text‹
    Construction of the opposite of an enriched category
    (\emph{cf.}~cite"kelly-enriched-category" (1.19)) requires that the underlying monoidal
    category be symmetric, in order to introduce the required ``twist'' in the definition
    of composition.
  ›

  locale opposite_enriched_category =
    symmetric_monoidal_category +
    EC: enriched_category
  begin

    interpretation elementary_symmetric_monoidal_category
                        C tensor unity lunit runit assoc sym
      using induces_elementary_symmetric_monoidal_categoryCMC by blast

    (* TODO: The names "Hom" and "Comp" are already in use as locale parameters. *)
    abbreviation (input) Homop
    where "Homop a b  Hom b a"

    abbreviation Compop
    where "Compop a b c  Comp c b a  𝗌[Hom c b, Hom b a]"

    sublocale enriched_category C T α ι Obj Homop Id Compop
    proof
      show *: "a b. a  Obj; b  Obj  ide (Hom b a)"
        using EC.ide_Hom by blast
      show "a. a  Obj  «Id a :   Hom a a»"
        using EC.Id_in_hom by blast
      show **: "a b c. a  Obj; b  Obj; c  Obj 
                          «Compop a b c : Hom c b  Hom b a  Hom c a»"
        using sym_in_hom EC.ide_Hom EC.Comp_in_hom by auto
      show "a b. a  Obj; b  Obj 
                     Compop a a b  (Hom b a  Id a) = 𝗋[Hom b a]"
      proof -
        fix a b
        assume a: "a  Obj" and b: "b  Obj"
        have "Compop a a b  (Hom b a  Id a) =
              Comp b a a  𝗌[Hom b a, Hom a a]  (Hom b a  Id a)"
          using comp_assoc by simp
        also have "... = Comp b a a  (Id a  Hom b a)  𝗌[Hom b a, ]"
          using a b sym_naturality [of "Hom b a" "Id a"] sym_in_hom
                EC.Id_in_hom EC.ide_Hom
          by fastforce
        also have "... = (Comp b a a  (Id a  Hom b a))  𝗌[Hom b a, ]"
          using comp_assoc by simp
        also have "... = 𝗅[Hom b a]  𝗌[Hom b a, ]"
          using a b EC.Comp_Id_Hom by simp
        also have "... = 𝗋[Hom b a] "
          using a b unitor_coherence EC.ide_Hom by presburger
        finally show "Compop a a b  (Hom b a  Id a) = 𝗋[Hom b a]"
          by blast
      qed
      show "a b. a  Obj; b  Obj 
                     Compop a b b  (Id b  Hom b a) = 𝗅[Hom b a]"
      proof -
        fix a b
        assume a: "a  Obj" and b: "b  Obj"
        have "Compop a b b  (Id b  Hom b a) =
              Comp b b a  𝗌[Hom b b, Hom b a]  (Id b  Hom b a)"
          using comp_assoc by simp
        also have "... = Comp b b a  (Hom b a  Id b)  𝗌[, Hom b a]"
          using a b sym_naturality [of "Id b" "Hom b a"] sym_in_hom
                EC.Id_in_hom EC.ide_Hom
          by force
        also have "... = (Comp b b a  (Hom b a  Id b))  𝗌[, Hom b a]"
          using comp_assoc by simp
        also have "... = 𝗋[Hom b a]  𝗌[, Hom b a]"
          using a b EC.Comp_Hom_Id by simp
        also have "... = 𝗅[Hom b a]"
        proof -
          (* TODO: Should probably be a fact in elementary_symmetric_monoidal_category. *)
          have "𝗋[Hom b a]  𝗌[, Hom b a] =
                (𝗅[Hom b a]  𝗌[Hom b a, ])  𝗌[, Hom b a]"
            using a b unitor_coherence EC.ide_Hom by simp
          also have "... = 𝗅[Hom b a]  𝗌[Hom b a, ]  𝗌[, Hom b a]"
            using comp_assoc by simp
          also have "... = 𝗅[Hom b a]"
            using a b comp_arr_dom comp_arr_inv sym_inverse by simp
          finally show ?thesis by blast
        qed
        finally show "Compop a b b  (Id b  Hom b a) = 𝗅[Hom b a]"
          by blast
      qed
      show "a b c d. a  Obj; b  Obj; c  Obj; d  Obj 
                         Compop a b d  (Compop b c d  Hom b a) =
                         Compop a c d  (Hom d c  Compop a b c) 
                           𝖺[Hom d c, Hom c b, Hom b a]"
      proof -
        fix a b c d
        assume a: "a  Obj" and b: "b  Obj" and c: "c  Obj" and d: "d  Obj"
        have "Compop a b d  (Compop b c d  Hom b a) =
              Compop a b d  (Comp d c b  Hom b a) 
                (𝗌[Hom d c, Hom c b]  Hom b a)"
          using a b c d ** interchange comp_ide_arr ide_in_hom seqI'
                EC.ide_Hom
          by metis
        also have "... = (Comp d b a 
                            (𝗌[Hom d b, Hom b a]  (Comp d c b  Hom b a)) 
                              (𝗌[Hom d c, Hom c b]  Hom b a))"
          using comp_assoc by simp
        also have "... = (Comp d b a 
                            ((Hom b a  Comp d c b) 
                                𝗌[Hom c b  Hom d c, Hom b a]) 
                              (𝗌[Hom d c, Hom c b]  Hom b a))"
          using a b c d sym_naturality EC.Comp_in_hom ide_char
                in_homE EC.ide_Hom
          by metis
        also have "... = (Comp d b a  (Hom b a  Comp d c b)) 
                           (𝗌[Hom c b  Hom d c, Hom b a] 
                              (𝗌[Hom d c, Hom c b]  Hom b a))"
          using comp_assoc by simp
        also have "... = (Comp d c a  (Comp c b a  Hom d c) 
                             𝖺-1[Hom b a, Hom c b, Hom d c]) 
                           (𝗌[Hom c b  Hom d c, Hom b a] 
                              (𝗌[Hom d c, Hom c b]  Hom b a))"
        proof -
          have "Comp d b a  (Hom b a  Comp d c b) =
                (Comp d b a  (Hom b a  Comp d c b)) 
                   (Hom b a  Hom c b  Hom d c)"
              using a b c d EC.Comp_in_hom arrI comp_in_homI ide_in_hom
                    tensor_in_hom EC.ide_Hom
          proof -
            have "seq (Comp d b a) (Hom b a  Comp d c b)"
              using a b c d EC.Comp_in_hom arrI comp_in_homI ide_in_hom
                    tensor_in_hom EC.ide_Hom
              by meson
            moreover have "dom (Comp d b a  (Hom b a  Comp d c b)) =
                           (Hom b a  Hom c b  Hom d c)"
              using a b c d EC.Comp_in_hom dom_comp dom_tensor ideD(1-2)
                    in_homE calculation EC.ide_Hom
              by metis
            ultimately show ?thesis
              using a b c d EC.Comp_in_hom comp_arr_dom by metis
          qed
          also have "... =
                (Comp d b a  (Hom b a  Comp d c b)) 
                   𝖺[Hom b a, Hom c b, Hom d c]  𝖺-1[Hom b a, Hom c b, Hom d c]"
            using a b c d comp_assoc_assoc'(1) EC.ide_Hom by simp
          also have "... = (Comp d b a  (Hom b a  Comp d c b) 
                             𝖺[Hom b a, Hom c b, Hom d c]) 
                               𝖺-1[Hom b a, Hom c b, Hom d c]"
            using comp_assoc by simp
          also have "... = (Comp d c a  (Comp c b a  Hom d c)) 
                              𝖺-1[Hom b a, Hom c b, Hom d c]"
            using a b c d EC.Comp_assoc by simp
          also have "... = Comp d c a  (Comp c b a  Hom d c) 
                             𝖺-1[Hom b a, Hom c b, Hom d c]"
            using comp_assoc by simp
          finally have "Comp d b a  (Hom b a  Comp d c b) =
                        Comp d c a  (Comp c b a  Hom d c) 
                          𝖺-1[Hom b a, Hom c b, Hom d c]"
            by blast
          thus ?thesis by simp
        qed
        also have "... = (Comp d c a  (Comp c b a  Hom d c)) 
                           (𝖺-1[Hom b a, Hom c b, Hom d c] 
                             𝗌[Hom c b  Hom d c, Hom b a] 
                               (𝗌[Hom d c, Hom c b]  Hom b a))"
          using comp_assoc by simp
        finally have LHS: "(Comp d b a  𝗌[Hom d b, Hom b a]) 
                             (Comp d c b  𝗌[Hom d c, Hom c b]  Hom b a) =
                           (Comp d c a  (Comp c b a  Hom d c)) 
                           (𝖺-1[Hom b a, Hom c b, Hom d c] 
                             𝗌[Hom c b  Hom d c, Hom b a] 
                               (𝗌[Hom d c, Hom c b]  Hom b a))"
          by blast
        have "Compop a c d  (Hom d c  Compop a b c) 
                𝖺[Hom d c, Hom c b, Hom b a] =
              Comp d c a 
                (𝗌[Hom d c, Hom c a] 
                  (Hom d c  Comp c b a  𝗌[Hom c b, Hom b a])) 
                  𝖺[Hom d c, Hom c b, Hom b a]"
          using comp_assoc by simp
        also have "... =
              Comp d c a 
                ((Comp c b a  𝗌[Hom c b, Hom b a]  Hom d c) 
                    𝗌[Hom d c, Hom c b  Hom b a]) 
                  𝖺[Hom d c, Hom c b, Hom b a]"
          using a b c d ** sym_naturality ide_char in_homE EC.ide_Hom
          by metis
        also have "... =
              Comp d c a 
                (((Comp c b a  Hom d c)  (𝗌[Hom c b, Hom b a]  Hom d c)) 
                    𝗌[Hom d c, Hom c b  Hom b a]) 
                  𝖺[Hom d c, Hom c b, Hom b a]"
          using a b c d ** interchange comp_arr_dom ideD(1-2)
                in_homE EC.ide_Hom
          by metis
        also have "... = (Comp d c a  (Comp c b a  Hom d c)) 
                           ((𝗌[Hom c b, Hom b a]  Hom d c) 
                             𝗌[Hom d c, Hom c b  Hom b a] 
                               𝖺[Hom d c, Hom c b, Hom b a])"
          using comp_assoc by simp
        also have "... = (Comp d c a  (Comp c b a  Hom d c)) 
                           (𝖺-1[Hom b a, Hom c b, Hom d c] 
                              𝗌[Hom c b  Hom d c, Hom b a] 
                                (𝗌[Hom d c, Hom c b]  Hom b a))"
        proof -
          have "(𝗌[Hom c b, Hom b a]  Hom d c) 
                  𝗌[Hom d c, Hom c b  Hom b a] 
                    𝖺[Hom d c, Hom c b, Hom b a] =
                𝖺-1[Hom b a, Hom c b, Hom d c] 
                  𝗌[Hom c b  Hom d c, Hom b a] 
                    (𝗌[Hom d c, Hom c b]  Hom b a)"
          proof -
            have 1: "𝗌[Hom d c, Hom c b  Hom b a] 
                       𝖺[Hom d c, Hom c b, Hom b a] =
                     𝖺-1[Hom c b, Hom b a, Hom d c] 
                       (Hom c b  𝗌[Hom d c, Hom b a]) 
                         𝖺[Hom c b, Hom d c, Hom b a] 
                           (𝗌[Hom d c, Hom c b]  Hom b a)"
            proof -
              have "𝗌[Hom d c, Hom c b  Hom b a] 
                       𝖺[Hom d c, Hom c b, Hom b a] =
                    (𝖺-1[Hom c b, Hom b a, Hom d c] 
                       𝖺[Hom c b, Hom b a, Hom d c]) 
                      𝗌[Hom d c, Hom c b  Hom b a] 
                        𝖺[Hom d c, Hom c b, Hom b a]"
                using a b c d comp_assoc_assoc'(2) comp_cod_arr by simp
              also have "... =
                    𝖺-1[Hom c b, Hom b a, Hom d c] 
                      𝖺[Hom c b, Hom b a, Hom d c] 
                        𝗌[Hom d c, Hom c b  Hom b a] 
                          𝖺[Hom d c, Hom c b, Hom b a]"
                using comp_assoc by simp
              also have "... =
                    𝖺-1[Hom c b, Hom b a, Hom d c] 
                      (Hom c b  𝗌[Hom d c, Hom b a]) 
                        𝖺[Hom c b, Hom d c, Hom b a] 
                          (𝗌[Hom d c, Hom c b]  Hom b a)"
                using a b c d assoc_coherence EC.ide_Hom by auto
              finally show ?thesis by blast
            qed
            have 2: "(𝗌[Hom c b, Hom b a]  Hom d c) 
                       𝖺-1[Hom c b, Hom b a, Hom d c] 
                         (Hom c b  𝗌[Hom d c, Hom b a]) =
                     𝖺-1[Hom b a, Hom c b, Hom d c] 
                       𝗌[Hom c b  Hom d c, Hom b a] 
                         inv 𝖺[Hom c b, Hom d c, Hom b a]"
            proof -
              have "(𝗌[Hom c b, Hom b a]  Hom d c) 
                      𝖺-1[Hom c b, Hom b a, Hom d c] 
                        (Hom c b  𝗌[Hom d c, Hom b a]) =
                    inv ((Hom c b  𝗌[Hom b a, Hom d c]) 
                           𝖺[Hom c b, Hom b a, Hom d c] 
                             (𝗌[Hom b a, Hom c b]  Hom d c))"
              proof -
                have "inv ((Hom c b  𝗌[Hom b a, Hom d c]) 
                             𝖺[Hom c b, Hom b a, Hom d c] 
                               (𝗌[Hom b a, Hom c b]  Hom d c)) =
                      inv (𝖺[Hom c b, Hom b a, Hom d c] 
                             (𝗌[Hom b a, Hom c b]  Hom d c)) 
                        inv (Hom c b  𝗌[Hom b a, Hom d c])"
                  using a b c d EC.ide_Hom
                        inv_comp [of "𝖺[Hom c b, Hom b a, Hom d c] 
                                          (𝗌[Hom b a, Hom c b]  Hom d c)"
                                       "Hom c b  𝗌[Hom b a, Hom d c]"]
                  by fastforce
                also have "... =
                      (inv (𝗌[Hom b a, Hom c b]  Hom d c) 
                         𝖺-1[Hom c b, Hom b a, Hom d c]) 
                        inv (Hom c b  𝗌[Hom b a, Hom d c])"
                  using a b c d EC.ide_Hom inv_comp by simp
                also have "... =
                      ((𝗌[Hom c b, Hom b a]  Hom d c) 
                         𝖺-1[Hom c b, Hom b a, Hom d c]) 
                        (Hom c b  𝗌[Hom d c, Hom b a])"
                  (* TODO: Need simps for inverse of sym. *)
                  using a b c d sym_inverse inverse_unique
                  apply auto[1]
                  by (metis *)
                finally show ?thesis
                  using comp_assoc by simp
              qed
              also have "... =
                    inv (𝖺[Hom c b, Hom d c, Hom b a] 
                             𝗌[Hom b a, Hom c b  Hom d c] 
                               𝖺[Hom b a, Hom c b, Hom d c])"
                using a b c d assoc_coherence EC.ide_Hom by auto
              also have "... =
                    𝖺-1[Hom b a, Hom c b, Hom d c] 
                      inv 𝗌[Hom b a, Hom c b  Hom d c] 
                        𝖺-1[Hom c b, Hom d c, Hom b a]"
                using a b c d EC.ide_Hom inv_comp inv_tensor comp_assoc
                      isos_compose
                by auto
              also have "... =
                    𝖺-1[Hom b a, Hom c b, Hom d c] 
                      𝗌[Hom c b  Hom d c, Hom b a] 
                        𝖺-1[Hom c b, Hom d c, Hom b a]"
                using a b c d sym_inverse inv_is_inverse inverse_unique
                by (metis tensor_preserves_ide EC.ide_Hom)
              finally show ?thesis by blast
            qed
            hence "(𝗌[Hom c b, Hom b a]  Hom d c) 
                     𝖺-1[Hom c b, Hom b a, Hom d c] 
                       (Hom c b  𝗌[Hom d c, Hom b a]) 
                          𝖺[Hom c b, Hom d c, Hom b a] =
                   𝖺-1[Hom b a, Hom c b, Hom d c] 
                     𝗌[Hom c b  Hom d c, Hom b a] 
                       inv 𝖺[Hom c b, Hom d c, Hom b a] 
                         𝖺[Hom c b, Hom d c, Hom b a]"
              by (metis comp_assoc)
            hence 3: "(𝗌[Hom c b, Hom b a]  Hom d c) 
                        𝖺-1[Hom c b, Hom b a, Hom d c] 
                         (Hom c b  𝗌[Hom d c, Hom b a]) 
                           𝖺[Hom c b, Hom d c, Hom b a] =
                     𝖺-1[Hom b a, Hom c b, Hom d c] 
                       𝗌[Hom c b  Hom d c, Hom b a]"
              using a b c comp_arr_dom d by fastforce
            have "(𝗌[Hom c b, Hom b a]  Hom d c) 
                    𝗌[Hom d c, Hom c b  Hom b a] 
                      𝖺[Hom d c, Hom c b, Hom b a] =
                  (𝗌[Hom c b, Hom b a]  Hom d c) 
                     𝖺-1[Hom c b, Hom b a, Hom d c] 
                       (Hom c b  𝗌[Hom d c, Hom b a]) 
                         𝖺[Hom c b, Hom d c, Hom b a] 
                           (𝗌[Hom d c, Hom c b]  Hom b a)"
              using 1 by simp
            also have "... =
                  ((𝗌[Hom c b, Hom b a]  Hom d c) 
                     𝖺-1[Hom c b, Hom b a, Hom d c] 
                       (Hom c b  𝗌[Hom d c, Hom b a]) 
                         𝖺[Hom c b, Hom d c, Hom b a]) 
                           (𝗌[Hom d c, Hom c b]  Hom b a)"
              using comp_assoc by simp
            also have "... =
                  (𝖺-1[Hom b a, Hom c b, Hom d c] 
                     𝗌[Hom c b  Hom d c, Hom b a]) 
                        (𝗌[Hom d c, Hom c b]  Hom b a)"
              using 3 by simp
            also have "... =
                  𝖺-1[Hom b a, Hom c b, Hom d c] 
                     𝗌[Hom c b  Hom d c, Hom b a] 
                        (𝗌[Hom d c, Hom c b]  Hom b a)"
              using comp_assoc by simp
            finally show ?thesis by simp
          qed
          thus ?thesis by auto
        qed
        finally have RHS: "Compop a c d 
                             (Hom d c  Compop a b c) 
                                𝖺[Hom d c, Hom c b, Hom b a] =
                           (Comp d c a  (Comp c b a  Hom d c)) 
                             (𝖺-1[Hom b a, Hom c b, Hom d c] 
                                𝗌[Hom c b  Hom d c, Hom b a] 
                                  (𝗌[Hom d c, Hom c b]  Hom b a))"
          by blast
        show "Compop a b d  (Compop b c d  Hom b a) =
              Compop a c d  (Hom d c  Compop a b c) 
                𝖺[Hom d c, Hom c b, Hom b a]"
          using LHS RHS by simp
      qed
    qed

  end

  subsection "Relation between (-op)0 and (-0)op"

  text‹
    Kelly (comment before (1.22)) claims, for a category A› enriched in a symmetric
    monoidal category, that we have (Aop)0 = (A0)op.  This point becomes somewhat
    confusing, as it depends on the particular formalization one adopts for the
    notion of ``category''.

    \sloppypar
    As we can see from the next two facts (Op_UC_hom_char› and UC_Op_hom_char›),
    the hom-sets Op.UC.hom a b› and UC.Op.hom a b› are both obtained by using UC.MkArr›
    to ``tag'' elements of hom ℐ (Hom (UC.Dom b) (UC.Dom a))› with UC.Dom a› and UC.Dom b›.
    These two hom-sets are formally distinct if (as is the case for us), the arrows of a
    category are regarded as containing information about their domain and codomain,
    so that the hom-sets are disjoint.  On the other hand, if one regards a category
    as a collection of mappings that assign to each pair of objects a› and b›
    a corresponding set hom a b›, then the hom-sets Op.UC.hom a b› and UC.Op.hom a b›
    could be arranged to be equal, as Kelly suggests.
  ›

  locale category_enriched_in_symmetric_monoidal_category =
    symmetric_monoidal_category +
    enriched_category
  begin

    interpretation elementary_symmetric_monoidal_category
                      C tensor unity lunit runit assoc sym
      using induces_elementary_symmetric_monoidal_categoryCMC by blast

    interpretation Op: opposite_enriched_category C T α ι σ Obj Hom Id Comp ..
    interpretation Op0: underlying_category C T α ι Obj Op.Homop Id Op.Compop
      ..

    interpretation UC: underlying_category C T α ι Obj Hom Id Comp ..
    interpretation UC.Op: dual_category UC.comp ..

    lemma Op_UC_hom_char:
    assumes "UC.ide a" and "UC.ide b"
    shows "Op0.hom a b =
           UC.MkArr (UC.Dom a) (UC.Dom b) `
             hom  (Hom (UC.Dom b) (UC.Dom a))"
      using assms Op0.hom_char [of "UC.Dom a" "UC.Dom b"]
            UC.ide_char [of a] UC.ide_char [of b] UC.arr_char
      by force

    lemma UC_Op_hom_char:
    assumes "UC.ide a" and "UC.ide b"
    shows "UC.Op.hom a b =
           UC.MkArr (UC.Dom b) (UC.Dom a) `
             hom  (Hom (UC.Dom b) (UC.Dom a))"
      using assms UC.Op.hom_char UC.hom_char [of "UC.Dom b" "UC.Dom a"]
            UC.ide_charCC
      by simp

    abbreviation toUCOp
    where "toUCOp f  if Op0.arr f
                       then UC.MkArr (Op0.Cod f) (Op0.Dom f) (Op0.Map f)
                       else UC.Op.null"

    sublocale toUCOp: "functor" Op0.comp UC.Op.comp toUCOp
    proof
      show "f. ¬ Op0.arr f  toUCOp f = UC.Op.null"
        by simp
      show 1: "f. Op0.arr f  UC.Op.arr (toUCOp f)"
        using Op0.arr_char by auto
      show "f. Op0.arr f  UC.Op.dom (toUCOp f) = toUCOp (Op0.dom f)"
        using 1 by simp
      show "f. Op0.arr f  UC.Op.cod (toUCOp f) = toUCOp (Op0.cod f)"
        using 1 by simp
      show "g f. Op0.seq g f 
                     toUCOp (Op0.comp g f) = UC.Op.comp (toUCOp g) (toUCOp f)"
      proof -
        fix f g
        assume fg: "Op0.seq g f"
        show "toUCOp (Op0.comp g f) = UC.Op.comp (toUCOp g) (toUCOp f)"
        proof (intro UC.arr_eqI)
          show "UC.arr (toUCOp (Op0.comp g f))"
            using 1 fg UC.Op.arr_char by blast
          show 2: "UC.arr (UC.Op.comp (toUCOp g) (toUCOp f))"
            using 1 Op0.seq_char UC.seq_char fg by force
          show "Op0.Dom (toUCOp (Op0.comp g f)) =
                Op0.Dom (UC.Op.comp (toUCOp g) (toUCOp f))"
            using 1 2 fg Op0.seq_char by fastforce
          show "Op0.Cod (toUCOp (Op0.comp g f)) =
                Op0.Cod (UC.Op.comp (toUCOp g) (toUCOp f))"
            using 1 2 fg Op0.seq_char by fastforce
          show "Op0.Map (toUCOp (Op0.comp g f)) =
                Op0.Map (UC.Op.comp (toUCOp g) (toUCOp f))"
          proof -
            have "Op0.Map (toUCOp (Op0.comp g f)) =
                  Op.Compop (UC.Dom f) (UC.Dom g) (UC.Cod g) 
                    (UC.Map g  UC.Map f)  ι-1"
              using 1 2 fg Op0.seq_char by auto
            also have "... = Comp (Op0.Cod g) (Op0.Dom g) (Op0.Dom f) 
                             (𝗌[Hom (Op0.Cod g) (Op0.Dom g),
                                Hom (Op0.Dom g) (Op0.Dom f)] 
                                (Op0.Map g  Op0.Map f))  ι-1"
              using comp_assoc by simp
            also have "... = Comp (Op0.Cod g) (Op0.Dom g) (Op0.Dom f) 
                             ((Op0.Map f  Op0.Map g)  𝗌[, ])  ι-1"
              using fg Op0.seq_char Op0.arr_char sym_naturality
              by (metis (no_types, lifting) in_homE mem_Collect_eq)
            also have "... = Comp (Op0.Cod g) (Op0.Dom g) (Op0.Dom f) 
                             (Op0.Map f  Op0.Map g)  𝗌[, ]  ι-1"
              using comp_assoc by simp
            also have "... = Comp (Op0.Cod g) (Op0.Dom g) (Op0.Dom f) 
                             (Op0.Map f  Op0.Map g)  ι-1"
              using sym_inv_unit ι_def monoidal_category_axioms
              by (simp add: monoidal_category.unitor_coincidence(1))
            finally have "Op0.Map (toUCOp (Op0.comp g f)) =
                        Comp (Op0.Cod g) (Op0.Dom g) (Op0.Dom f) 
                             (Op0.Map f  Op0.Map g)  ι-1"
              by blast
            also have "... = Op0.Map (UC.Op.comp (toUCOp g) (toUCOp f))"
              using fg 2 by auto
            finally show ?thesis by blast
          qed
        qed
      qed
    qed

    lemma functor_toUCOp:
    shows "functor Op0.comp UC.Op.comp toUCOp"
      ..

    abbreviation toOp0
      where "toOp0 f  if UC.Op.arr f
                         then Op0.MkArr (UC.Cod f) (UC.Dom f) (UC.Map f)
                         else Op0.null"

    sublocale toOp0: "functor" UC.Op.comp Op0.comp toOp0
    proof
      show "f. ¬ UC.Op.arr f  toOp0 f = Op0.null"
        by simp
      show 1: "f. UC.Op.arr f  Op0.arr (toOp0 f)"
        using UC.arr_char by simp
      show "f. UC.Op.arr f  Op0.dom (toOp0 f) = toOp0 (UC.Op.dom f)"
        using 1 by auto
      show "f. UC.Op.arr f  Op0.cod (toOp0 f) = toOp0 (UC.Op.cod f)"
        using 1 by auto
      show "g f. UC.Op.seq g f 
                     toOp0 (UC.Op.comp g f) = Op0.comp (toOp0 g) (toOp0 f)"
      proof -
        fix f g
        assume fg: "UC.Op.seq g f"
        show "toOp0 (UC.Op.comp g f) = Op0.comp (toOp0 g) (toOp0 f)"
        proof (intro Op0.arr_eqI)
          show "Op0.arr (toOp0 (UC.Op.comp g f))"
            using fg 1 by blast
          show 2: "Op0.seq (toOp0 g) (toOp0 f)"
            using fg 1 UC.seq_char UC.arr_char Op0.seq_char by fastforce
          show "Op0.Dom (toOp0 (UC.Op.comp g f)) =
                Op0.Dom (Op0.comp (toOp0 g) (toOp0 f))"
            using fg 1 2 Op0.dom_char Op0.cod_char UC.seq_char Op0.seq_char
            by auto
          show "Op0.Cod (toOp0 (UC.Op.comp g f)) =
                Op0.Cod (Op0.comp (toOp0 g) (toOp0 f))"
            using fg 1 2 Op0.dom_char Op0.cod_char UC.seq_char Op0.seq_char
            by auto
          show "Op0.Map (toOp0 (UC.Op.comp g f)) =
                Op0.Map (Op0.comp (toOp0 g) (toOp0 f))"
          proof -
            have "Op0.Map (Op0.comp (toOp0 g) (toOp0 f)) =
                  Op.Compop (Op0.Dom (toOp0 f)) (Op0.Dom (toOp0 g))
                    (Op0.Cod (toOp0 g)) 
                    (Op0.Map (toOp0 g)  Op0.Map (toOp0 f))  inv ι"
              using fg 1 2 UC.seq_char by auto
            also have "... =
                       Comp (Op0.Dom g) (Op0.Cod g) (Op0.Cod f) 
                         (𝗌[Hom (Op0.Dom g) (Op0.Cod g),
                            Hom (Op0.Cod g) (Op0.Cod f)] 
                            (Op0.Map g  Op0.Map f))  inv ι"
              using fg comp_assoc by auto
            also have "... =
                       Comp (Op0.Dom g) (Op0.Cod g) (Op0.Cod f) 
                         ((Op0.Map f  Op0.Map g)  𝗌[unity, unity])  inv ι"
              using fg UC.seq_char UC.arr_char sym_naturality
              by (metis (no_types, lifting) in_homE UC.Op.arr_char
                  UC.Op.comp_def mem_Collect_eq)
            also have "... =
                       Comp (Op0.Dom g) (Op0.Cod g) (Op0.Cod f) 
                         (Op0.Map f  Op0.Map g)  𝗌[unity, unity]  inv ι"
              using comp_assoc by simp
            also have "... =
                       Comp (Op0.Dom g) (Op0.Cod g) (Op0.Cod f) 
                         (Op0.Map f  Op0.Map g)  inv ι"
              using sym_inv_unit ι_def monoidal_category_axioms
              by (simp add: monoidal_category.unitor_coincidence(1))
            also have "... = Op0.Map (toOp0 (UC.Op.comp g f))"
              using fg UC.seq_char by simp
            finally show ?thesis by argo
          qed
        qed
      qed
    qed

    lemma functor_toOp0:
    shows "functor UC.Op.comp Op0.comp toOp0"
      ..

    sublocale inverse_functors UC.Op.comp Op0.comp toUCOp toOp0
      using Op0.MkArr_Map toUCOp.preserves_reflects_arr Op0.is_extensional
            UC.MkArr_Map toOp0.preserves_reflects_arr UC.Op.is_extensional
      by unfold_locales auto

    lemma inverse_functors_toUCOp_toOp0:
    shows "inverse_functors UC.Op.comp Op0.comp toUCOp toOp0"
      ..

  end

  section "Enriched Hom Functors"

  text‹
    Here we exhibit covariant and contravariant hom functors as enriched functors,
    as in cite"kelly-enriched-category" Section 1.6.  We don't bother to exhibit
    them as partial functors of a single two-argument functor, as to do so would
    require us to define the tensor product of enriched categories; something that would
    require more technology for proving coherence conditions than we have developed
    at present.
  ›

  subsection "Covariant Case"

  locale covariant_Hom =
    monoidal_category +
    (* We need qualifier C here because otherwise there is a clash on Id and Comp. *)
    C: elementary_closed_monoidal_category +
    enriched_category +
  fixes x :: 'o
  assumes x: "x  Obj"
  begin

    interpretation C: enriched_category C T α ι Collect ide exp C.Id C.Comp
      using C.is_enriched_in_itself by simp
    interpretation C: self_enriched_category C T α ι exp eval Curry ..

    abbreviation homo
    where "homo  Hom x"

    abbreviation homa
    where "homa  λb c. if b  Obj  c  Obj
                        then Curry[Hom b c, Hom x b, Hom x c] (Comp x b c)
                        else null"

    sublocale enriched_functor C T α ι
                Obj Hom Id Comp
                Collect ide exp C.Id C.Comp
                homo homa
    proof
      show "a b. a  Obj  b  Obj  homa a b = null"
        by auto
      show "y. y  Obj  homo y  Collect ide"
        using x ide_Hom by auto
      show *: "a b. a  Obj; b  Obj 
                        «homa a b : Hom a b  exp (homo a) (homo b)»"
        using x by auto
      show "a. a  Obj  homa a a  Id a = C.Id (homo a)"
        using x Comp_Id_Hom Comp_in_hom Id_in_hom C.Id_def C.comp_Curry_arr
        apply auto[1]
        by (metis ide_Hom)
      show "a b c. a  Obj; b  Obj; c  Obj 
                       C.Comp (homo a) (homo b) (homo c) 
                         (homa b c  homa a b) =
                       homa a c  Comp a b c"
      proof -
        fix a b c
        assume a: "a  Obj" and b: "b  Obj" and c: "c  Obj"
        have "Uncurry[homo a, homo c]
                (C.Comp (homo a) (homo b) (homo c)  (homa b c  homa a b)) =
              Uncurry[homo a, homo c] (homa a c  Comp a b c)"
        proof -
          have "Uncurry[homo a, homo c]
                  (C.Comp (homo a) (homo b) (homo c)  (homa b c  homa a b)) =
                Uncurry[homo a, homo c]
                  (Curry[exp (homo b) (homo c)  exp (homo a) (homo b), homo a,
                         homo c]
                     (eval (homo b) (homo c) 
                        (exp (homo b) (homo c)  eval (homo a) (homo b)) 
                          𝖺[exp (homo b) (homo c), exp (homo a) (homo b),
                            homo a]) 
                       (homa b c  homa a b))"
            using C.Comp_def by simp
          also have "... =
                     Uncurry[homo a, homo c]
                       (Curry[Hom b c  Hom a b, homo a, homo c]
                          ((eval (homo b) (homo c) 
                              (exp (homo b) (homo c)  eval (homo a) (homo b)) 
                                 𝖺[exp (homo b) (homo c), exp (homo a) (homo b),
                                   homo a]) 
                            ((homa b c  homa a b)  homo a)))"
          proof -
            have "«homa b c  homa a b :
                    Hom b c  Hom a b 
                    exp (homo b) (homo c)  exp (homo a) (homo b)»"
              using x a b c * by force
            moreover have "«eval (homo b) (homo c) 
                              (exp (homo b) (homo c)  eval (homo a) (homo b)) 
                                𝖺[exp (homo b) (homo c), exp (homo a) (homo b), homo a]
                              : (exp (homo b) (homo c)  exp (homo a) (homo b))
                                    homo a
                                      homo c»"
              using x a b c by simp
            ultimately show ?thesis
              using x a b c C.comp_Curry_arr by simp
          qed
          also have "... =
                     (eval (homo b) (homo c) 
                        (exp (homo b) (homo c)  eval (homo a) (homo b)) 
                          𝖺[exp (homo b) (homo c), exp (homo a) (homo b), homo a]) 
                       ((homa b c  homa a b)  homo a)"
            using x a b c
                  C.Uncurry_Curry
                     [of "Hom b c  Hom a b" "homo a" "homo c"
                         "(eval (homo b) (homo c) 
                          (exp (homo b) (homo c)  eval (homo a) (homo b)) 
                            𝖺[exp (homo b) (homo c), exp (homo a) (homo b), homo a]) 
                              ((Curry[Hom b c, homo b, homo c] (Comp x b c) 
                                Curry[Hom a b, homo a, homo b] (Comp x a b))
                                   homo a)"]
            by fastforce
          also have "... =
                     eval (homo b) (homo c) 
                       (exp (homo b) (homo c)  eval (homo a) (homo b)) 
                         𝖺[exp (homo b) (homo c), exp (homo a) (homo b), homo a] 
                           ((homa b c  homa a b)  homo a)"
            by (simp add: comp_assoc)
          also have "... =
                     eval (homo b) (homo c) 
                       ((exp (homo b) (homo c)  eval (homo a) (homo b)) 
                         (homa b c  homa a b  homo a)) 
                           𝖺[Hom b c, Hom a b, homo a]"
             using x a b c Comp_in_hom
                   assoc_naturality
                     [of "Curry[Hom b c, homo b, homo c] (Comp x b c)"
                         "Curry[Hom a b, homo a, homo b] (Comp x a b)"
                         "homo a"]
            using comp_assoc by auto
          also have "... =
                     eval (homo b) (homo c) 
                       (exp (homo b) (homo c) 
                          homa b c  Uncurry[homo a, homo b] (homa a b)) 
                            𝖺[Hom b c, Hom a b, homo a]"
            using x a b c Comp_in_hom interchange by simp
          also have "... =
                     eval (homo b) (homo c) 
                       (exp (homo b) (homo c)  homa b c  Comp x a b) 
                         𝖺[Hom b c, Hom a b, homo a]"
            using x a b c C.Uncurry_Curry Comp_in_hom by auto
          also have "... =
                     eval (homo b) (homo c)  (homa b c  Comp x a b) 
                       𝖺[Hom b c, Hom a b, homo a]"
            using x a b c
            by (simp add: Comp_in_hom comp_ide_arr)
          also have "... =
                     eval (homo b) (homo c) 
                       ((homa b c  homo b)  (Hom b c  Comp x a b)) 
                         𝖺[Hom b c, Hom a b, homo a]"
          proof -
            have "seq (homa b c) (Hom b c)"
              using x a b c Comp_in_hom C.Curry_in_hom ide_Hom by simp
            moreover have "seq (homo b) (Comp x a b)"
              using x a b c Comp_in_hom by fastforce
            ultimately show ?thesis
              using x a b c Comp_in_hom C.Curry_in_hom comp_arr_ide
                    comp_ide_arr ide_Hom interchange
              by metis
          qed
          also have "... =
                     Uncurry[homo b, homo c] (homa b c) 
                       (Hom b c  Comp x a b) 
                         𝖺[Hom b c, Hom a b, homo a]"
            using comp_assoc by simp
          also have "... = Comp x a c  (Comp a b c  homo a)"
            using x a b c C.Uncurry_Curry Comp_in_hom Comp_assoc by auto
          also have "... = Uncurry[homo a, homo c]
                             (Curry[Hom b c  Hom a b, homo a, homo c]
                                (Comp x a c  (Comp a b c  homo a)))"
            using x a b c Comp_in_hom comp_assoc
                  C.Uncurry_Curry
                    [of "Hom b c  Hom a b" "homo a" "homo c"
                        "Comp x a c  (Comp a b c  homo a)"]
            by fastforce
          also have "... = Uncurry[homo a, homo c] (homa a c  Comp a b c)"
            using x a b c Comp_in_hom
                  C.comp_Curry_arr 
                    [of "homo a" "Comp a b c" "Hom b c  Hom a b"
                        "Hom a c" "Comp x a c" "homo c"]
            by auto
          finally show ?thesis by blast
        qed
        hence "Curry[Hom b c  Hom a b, homo a, homo c]
                 (Uncurry[homo a, homo c]
                    (C.Comp (homo a) (homo b) (homo c) 
                       (homa b c  homa a b))) =
               Curry[Hom b c  Hom a b, homo a, homo c]
                 (Uncurry[homo a, homo c] (homa a c  Comp a b c))"
          by simp
        thus "C.Comp (homo a) (homo b) (homo c)  (homa b c  homa a b) =
              homa a c  Comp a b c"
          using x a b c Comp_in_hom
                C.Curry_Uncurry
                  [of "Hom b c  Hom a b" "homo a" "homo c" "homa a c  Comp a b c"]
                C.Curry_Uncurry
                  [of "Hom b c  Hom a b" "homo a" "homo c"
                      "C.Comp (homo a) (homo b) (homo c)  (homa b c  homa a b)"]
          by auto
      qed
    qed

    lemma is_enriched_functor:
    shows "enriched_functor C T α ι
             Obj Hom Id Comp
             (Collect ide) exp C.Id C.Comp
             homo homa"
      ..

    sublocale C0: underlying_category C T α ι Collect ide exp C.Id C.Comp ..
    sublocale UC: underlying_category C T α ι Obj Hom Id Comp ..
    sublocale UF: underlying_functor C T α ι
                    Obj Hom Id Comp
                    Collect ide exp C.Id C.Comp
                    homo homa
      ..

    text‹
      The following is Kelly's formula (1.31), for the result of applying the ordinary
      functor underlying the covariant hom functor, to an arrow g : ℐ → Hom b c› of C0,
      resulting in an arrow Hom x g : Hom x b → Hom x c› of C›.  The point of the result
      is that this can be expressed explicitly as Comp x b c ⋅ (g ⊗ homo b) ⋅ 𝗅-1[homo b]›.
      This is all very confusing at first, because Kelly identifies C› with the
      underlying category C0 of C› regarded as a self-enriched category, whereas here we
      cannot ignore the fact that they are merely isomorphic via C.frmUC: UC.comp → C0.comp›.
      There is also the bother that, for an arrow g : ℐ → Hom b c› of C›,
      the corresponding arrow of the underlying category UC› has to be formally
      constructed using UC.MkArr›, \emph{i.e.}~as UC.MkArr b c g›.
    ›

    lemma Kelly_1_31:
    assumes "b  Obj" and "c  Obj" and "«g :   Hom b c»"
    shows "C.frmUC (UF.map0 (UC.MkArr b c g)) =
           Comp x b c  (g  homo b)  𝗅-1[homo b]"
    proof -
      have "C.frmUC (UF.map0 (UC.MkArr b c g)) =
            (Curry[Hom b c, homo b, homo c] (Comp x b c)  g) [homo b, homo c]"
        using assms x ide_Hom UF.map0_def
              C.UC.arr_MkArr
                [of "Hom x b" "Hom x c"
                    "Curry[Hom b c, Hom x b, Hom x c] (Comp x b c)  g"]
        by fastforce
      also have "... = C.Uncurry (Hom x b) (Hom x c)
                         (Curry[, Hom x b, Hom x c]
                            (Comp x b c  (g  Hom x b)))  𝗅-1[homo b]"
        using assms x C.comp_Curry_arr C.DN_def
        by (metis Comp_in_hom C.Curry_simps(1-2) in_homE seqI ide_Hom)
      also have "... = (Comp x b c  (g  Hom x b))  𝗅-1[homo b]"
        using assms x ide_Hom ide_unity
              C.Uncurry_Curry
                [of  "Hom x b" "Hom x c" "Comp x b c  (g  Hom x b)"]
        by fastforce
      also have "... = Comp x b c  (g  Hom x b)  𝗅-1[homo b]"
        using comp_assoc by simp
      finally show ?thesis by blast
    qed

    (*
     * TODO: Rationalize the naming between here and ClosedMonoidalCategory
     * to avoid clashes and be understandable.  I don't like having the generally
     * redundant subscript on "map0", but right now the unadorned name "map" clashes
     * with a value defined for the base category C.  The alternative is to qualify
     * all references to C, but that is worse.
     *)

    abbreviation map0
    where "map0 b c g  Comp x b c  (g  Hom x b)  𝗅-1[homo b]"    

  end

  context elementary_closed_monoidal_category
  begin

    lemma cov_Exp_DN:
    assumes "«g :   exp a b»"
    and "ide a" and "ide b" and "ide x"
    shows "Exp x (g [a, b]) =
           (Curry[exp a b, exp x a, exp x b] (Comp x a b)  g) [exp x a, exp x b]"
    proof -
      have "(Curry[exp a b, exp x a, exp x b] (Comp x a b)  g) [exp x a, exp x b] =
            Uncurry[exp x a, exp x b]
              (Curry[, exp x a, exp x b] (Comp x a b  (g  exp x a)))  𝗅-1[exp x a]"
        using assms DN_def
              comp_Curry_arr
                [of "exp x a" g  "exp a b" "Comp x a b" "exp x b"]
        by force
      also have "... = (Comp x a b  (g  exp x a))  𝗅-1[exp x a]"
        using assms Uncurry_Curry by auto
      also have "... = Curry[exp a b  exp x a, x, b]
                         (eval a b  (exp a b  eval x a)  𝖺[exp a b, exp x a, x]) 
                           (g  exp x a)  𝗅-1[exp x a]"
        unfolding Comp_def
        using assms comp_assoc by auto
      also have "... = Curry[exp x a, x, b]
                         ((eval a b  (exp a b  eval x a)  𝖺[exp a b, exp x a, x]) 
                            ((g  exp x a)  𝗅-1[exp x a]  x))"
        using assms comp_Curry_arr by auto
      also have "... = Curry[exp x a, x, b]
                         (eval a b  (exp a b  eval x a) 
                            (𝖺[exp a b, exp x a, x]  ((g  exp x a)  x)) 
                               (𝗅-1[exp x a]  x))"
        using assms comp_arr_dom comp_cod_arr interchange comp_assoc by fastforce
      also have "... = Curry[exp x a, x, b]
                         (eval a b  (exp a b  eval x a) 
                            ((g  exp x a  x)  𝖺[, exp x a, x]) 
                               (𝗅-1[exp x a]  x))"
        using assms assoc_naturality [of g "exp x a" x] by auto
      also have "... = Curry[exp x a, x, b]
                         (eval a b  ((exp a b  eval x a)  (g  exp x a  x)) 
                            𝖺[, exp x a, x]  (𝗅-1[exp x a]  x))"
        using assms comp_assoc by simp
      also have "... = Curry[exp x a, x, b]
                         (eval a b  ((g  a)  (  eval x a)) 
                            𝖺[, exp x a, x]  (𝗅-1[exp x a]  x))"
        using assms comp_arr_dom comp_cod_arr interchange by auto
      also have "... = Curry[exp x a, x, b]
                         (Uncurry[a, b] g  (  eval x a)  𝗅-1[exp x a  x])"
        using assms lunit_tensor inv_comp comp_assoc by simp
      also have "... = Exp x (g [a, b])"
        using assms lunit'_naturality [of "eval x a"] comp_assoc DN_def by auto
      finally show ?thesis by simp
    qed

  end

  subsection "Contravariant Case"

  locale contravariant_Hom =
    symmetric_monoidal_category +
    C: elementary_closed_symmetric_monoidal_category +
    enriched_category +
  fixes y :: 'o
  assumes y: "y  Obj"
  begin

    interpretation C: enriched_category C T α ι Collect ide exp C.Id C.Comp
      using C.is_enriched_in_itself by simp
    interpretation C: self_enriched_category C T α ι exp eval Curry ..

    sublocale Op: opposite_enriched_category C T α ι σ Obj Hom Id Comp ..

    abbreviation homo
    where "homo  λa. Hom a y"

    abbreviation homa
    where "homa  λb c. if b  Obj  c  Obj
                        then Curry[Hom c b, Hom b y, Hom c y] (Op.Compop y b c)
                        else null"

    sublocale enriched_functor C T α ι
                Obj Op.Homop Id Op.Compop
                Collect ide exp C.Id C.Comp
                homo homa
    proof
      show "a b. a  Obj  b  Obj  homa a b = null"
        by auto
      show "x. x  Obj  homo x  Collect ide"
        using y by auto
      show *: "a b. a  Obj; b  Obj 
                        «homa a b : Hom b a  exp (homo a) (homo b)»"
        using y C.cnt_Exp_ide C.Curry_in_hom Op.Comp_in_hom [of y] by simp
      show "a. a  Obj  homa a a  Id a = C.Id (homo a)"
        using y Id_in_hom C.Id_def C.comp_Curry_arr Op.Comp_Id_Hom Op.Comp_in_hom
        by fastforce
      show "a b c. a  Obj; b  Obj; c  Obj 
                       C.Comp (homo a) (homo b) (homo c) 
                         (homa b c  homa a b) =
                       homa a c  Op.Compop a b c "
      proof -
        fix a b c
        assume a: "a  Obj" and b: "b  Obj" and c: "c  Obj"
        have "C.Comp (homo a) (homo b) (homo c)  (homa b c  homa a b) =
              Curry[exp (homo b) (homo c)  exp (homo a) (homo b),
                    homo a, homo c]
                (eval (homo b) (homo c) 
                  (exp (homo b) (homo c)  eval (homo a) (homo b)) 
                    𝖺[exp (homo b) (homo c), exp (homo a) (homo b), homo a]) 
                  (homa b c  homa a b)"
          using y a b c comp_assoc C.Comp_def by simp
        also have "... = Curry[Hom c b  Hom b a, homo a, homo c]
                           ((eval (homo b) (homo c) 
                              (exp (homo b) (homo c)  eval (homo a) (homo b)) 
                                𝖺[exp (homo b) (homo c), exp (homo a) (homo b),
                                  homo a]) 
                              ((homa b c  homa a b)  homo a))"
          using y a b c
                C.comp_Curry_arr
                  [of "Hom a y" "homa b c  homa a b" "Hom c b  Hom b a"
                       "exp (homo b) (homo c)  exp (homo a) (homo b)"
                       "eval (homo b) (homo c) 
                          (exp (homo b) (homo c)  eval (homo a) (homo b)) 
                            𝖺[exp (homo b) (homo c), exp (homo a) (homo b), homo a]"
                       "homo c"]
          by fastforce
        also have "... = Curry[Hom c b  Hom b a, homo a, homo c]
                           (eval (homo b) (homo c) 
                             (exp (homo b) (homo c)  eval (homo a) (homo b)) 
                               (homa b c  homa a b  homo a) 
                                 𝖺[Hom c b, Hom b a, homo a])"
          using y a b c Op.Comp_in_hom comp_assoc
                C.assoc_naturality
                  [of "Curry[Hom c b, homo b, homo c] (Op.Compop y b c)"
                      "Curry[Hom b a, homo a, homo b] (Op.Compop y a b)"
                      "homo a"]
          by auto
        also have "... = Curry[Hom c b  Hom b a, homo a, homo c]
                           (eval (homo b) (homo c) 
                             (exp (homo b) (homo c)  homa b c 
                              Uncurry[homo a, homo b] (homa a b)) 
                               𝖺[Hom c b, Hom b a, homo a])"
        proof -
          have "seq (exp (homo b) (homo c)) (homa b c)"
            using y a b c by force
          moreover have "seq (eval (homo a) (homo b)) (homa a b  homo a)"
            using y a b c by fastforce
          ultimately show ?thesis
            using y a b c comp_assoc
                  C.interchange
                    [of "exp (Hom b y) (Hom c y)" "homa b c"
                        "eval (Hom a y) (Hom b y)" "homa a b  homo a"]
            by metis
        qed
        also have "... = Curry[Hom c b  Hom b a, homo a, homo c]
                           (eval (homo b) (homo c) 
                             (exp (homo b) (homo c)  homa b c  Op.Compop y a b) 
                               𝖺[Hom c b, Hom b a, homo a])"
          using y a b c C.Uncurry_Curry Op.Comp_in_hom by auto
        also have "... = Curry[Hom c b  Hom b a, homo a, homo c]
                           (eval (homo b) (homo c) 
                              (homa b c  Op.Compop y a b) 
                                𝖺[Hom c b, Hom b a, homo a])"
          using y a b c
          by (simp add: comp_ide_arr Op.Comp_in_hom)
        also have "... = Curry[Hom c b  Hom b a, homo a, homo c]
                           (eval (homo b) (homo c) 
                             (homa b c  Hom c b  homo b  Op.Compop y a b) 
                               𝖺[Hom c b, Hom b a, homo a])"
          using y a b c *
          by (metis Op.Comp_in_hom comp_cod_arr comp_arr_dom in_homE)
         also have "... = Curry[Hom c b  Hom b a, homo a, homo c]
                           (eval (homo b) (homo c) 
                             ((homa b c  homo b)  (Hom c b  Op.Compop y a b)) 
                               𝖺[Hom c b, Hom b a, homo a])"
          using y a b c *
                C.interchange [of "homa b c" "Hom c b" "homo b" "Op.Compop y a b"]
          by (metis Op.Comp_in_hom ide_Hom ide_char in_homE seqI)
        also have "... = Curry[Hom c b  Hom b a, homo a, homo c]
                           (Uncurry[homo b, homo c] (homa b c) 
                              (Hom c b  Op.Compop y a b) 
                                𝖺[Hom c b, Hom b a, homo a])"
          using comp_assoc by simp
        also have "... = Curry[Hom c b  Hom b a, homo a, homo c]
                           (Op.Compop y b c 
                             (Hom c b  Op.Compop y a b) 
                               𝖺[Hom c b, Hom b a, homo a])"
          using y a b c C.Uncurry_Curry
          by (simp add: Op.Comp_in_hom)
        also have "... = Curry[Hom c b  Hom b a, homo a, homo c]
                           (Op.Compop y a c  (Op.Compop a b c  homo a))"
          using y a b c Op.Comp_assoc [of y a b c] by simp
        also have "... = homa a c  Op.Compop a b c"
          using y a b c C.comp_Curry_arr [of "Hom a y" "Op.Compop a b c"]
                ide_Hom Op.Comp_in_hom
          by fastforce
        finally
        show "C.Comp (homo a) (homo b) (homo c)  (homa b c  homa a b) =
              homa a c  Op.Compop a b c"
          by blast
      qed
    qed

    lemma is_enriched_functor:
    shows "enriched_functor C T α ι
             Obj Op.Homop Id Op.Compop
             (Collect ide) exp C.Id C.Comp
             homo homa"
      ..

    sublocale C0: underlying_category C T α ι Collect ide exp C.Id C.Comp ..
    sublocale Op0: underlying_category C T α ι Obj Op.Homop Id Op.Compop ..
    sublocale UF: underlying_functor C T α ι
                    Obj Op.Homop Id Op.Compop
                    Collect ide exp C.Id C.Comp
                    homo homa
      ..

    text‹
      The following is Kelly's formula (1.32) for Hom f y : Hom b y → Hom a y›.
    ›

     lemma Kelly_1_32:
     assumes "a  Obj" and "b  Obj" and "«f :   Hom a b»"
     shows "C.frmUC (UF.map0 (Op0.MkArr b a f)) =
            Comp a b y  (Hom b y  f)  𝗋-1[homo b]"
     proof -
       have "C.frmUC (UF.map0 (Op0.MkArr b a f)) =
             (Curry[Hom a b, homo b, homo a] (Op.Compop y b a)  f)
                [homo b, homo a]"
       proof -
         have "C.UC.arr (Op0.MkArr (Hom b y) (Hom a y)
                 (Curry[Hom a b, Hom b y, Hom a y] (Op.Compop y b a)  f))"
           using assms y ide_Hom
           apply auto[1]
           using C.UC.arr_MkArr
                   [of "Hom b y" "Hom a y"
                       "Curry[Hom a b, homo b, homo a] (Op.Compop y b a)  f"]
           by blast
         thus ?thesis
           using assms UF.map0_def Op0.arr_MkArr UF.preserves_arr by auto
       qed
       also have 1: "... = Curry[, homo b, homo a]
                             (Op.Compop y b a  (f  homo b)) [homo b, homo a]"
       proof -
         have "Curry[Hom a b, Hom b y, Hom a y] (Op.Compop y b a)  f =
               Curry[, Hom b y, Hom a y] (Op.Compop y b a  (f  Hom b y))"
           using assms y C.comp_Curry_arr by blast
         thus ?thesis by simp
       qed
       also have "... = (Op.Compop y b a  (f  Hom b y))  𝗅-1[homo b]"
       proof -
         have "arr (Curry[, Hom b y, Hom a y]
                      (Op.Compop y b a  (f  Hom b y)))"
           using assms y ide_Hom C.ide_unity
           by (metis 1 C.Curry_simps(1-3) C.DN_def C.DN_simps(1) cod_comp
               dom_comp in_homE not_arr_null seqI Op.Comp_in_hom)
         thus ?thesis
         unfolding C.DN_def
         using assms y ide_Hom C.ide_unity
               C.Uncurry_Curry
                 [of  "Hom b y" "Hom a y" "Op.Compop y b a  (f  Hom b y)"]
         apply auto[1]
         by fastforce
       qed
       also have "... =
                  Comp a b y  (𝗌[Hom a b, Hom b y]  (f  Hom b y))  𝗅-1[homo b]"
         using comp_assoc by simp
       also have "... = Comp a b y  ((Hom b y  f)  𝗌[, Hom b y])  𝗅-1[homo b]"
         using assms y C.sym_naturality [of f "Hom b y"] by auto
       also have "... = Comp a b y  (Hom b y  f)  𝗌[, Hom b y]  𝗅-1[homo b]"
         using comp_assoc by simp
       also have "... = Comp a b y  (Hom b y  f)  𝗋-1[homo b]"
       proof -
         have "𝗋-1[homo b] = inv (𝗅[homo b]  𝗌[Hom b y, ])"
            using assms y unitor_coherence by simp
         also have "... = 𝗌[, Hom b y]  𝗅-1[homo b]"
           using assms y
           by (metis C.ide_unity inv_comp_left(1) inverse_unique
               C.iso_lunit C.iso_runit C.sym_inverse C.unitor_coherence
               Op.ide_Hom)
         finally show ?thesis by simp
       qed
       finally show ?thesis by blast
     qed

     abbreviation map0
     where "map0 a b f  Comp a b y  (Hom b y  f)  𝗋-1[homo b]"

  end

  context elementary_closed_symmetric_monoidal_category
  begin

    interpretation enriched_category C T α ι Collect ide exp Id Comp
      using is_enriched_in_itself by simp
    interpretation self_enriched_category C T α ι exp eval Curry ..

    sublocale Op: opposite_enriched_category C T α ι σ Collect ide exp Id Comp
      ..

    lemma cnt_Exp_DN:
    assumes "«f :   exp a b»"
    and "ide a" and "ide b" and "ide y"
    shows "Exp (f [a, b]) y =
           (Curry[exp a b, exp b y, exp a y] (Op.Compop y b a)  f)
              [exp b y, exp a y]"
    proof -
      have "(Curry[exp a b, exp b y, exp a y] (Op.Compop y b a)  f)
               [exp b y, exp a y] =
            Uncurry[exp b y, exp a y]
              (Curry[, exp b y, exp a y] (Op.Compop y b a  (f  exp b y))) 
                 𝗅-1[exp b y]"
        using assms Op.Comp_in_hom DN_def comp_Curry_arr by force
      also have "... = (Op.Compop y b a  (f  exp b y))  𝗅-1[exp b y]"
        using assms Uncurry_Curry by auto
      also have "... = Comp a b y  (𝗌[exp a b, exp b y]  (f  exp b y)) 
                         𝗅-1[exp b y]"
        using comp_assoc by simp
      also have "... = Comp a b y  ((exp b y  f)  𝗌[, exp b y])  𝗅-1[exp b y]"
        using assms sym_naturality [of f "exp b y"] by auto
      also have "... = Comp a b y  (exp b y  f)  𝗌[, exp b y]  𝗅-1[exp b y]"
        using comp_assoc by simp
      also have "... = Comp a b y  (exp b y  f)  𝗋-1[exp b y]"
      proof -
        have "𝗋-1[exp b y] = inv (𝗅[exp b y]  𝗌[exp b y, ])"
          using assms unitor_coherence by auto
        also have "... = inv 𝗌[exp b y, ]  𝗅-1[exp b y]"
          using assms inv_comp by simp
        also have "... = 𝗌[, exp b y]  𝗅-1[exp b y]"
          using assms
          by (metis ide_exp ide_unity inverse_unique sym_inverse)
        finally show ?thesis by simp
      qed
      also have "... = Curry[exp b y  exp a b, a, y]
                         (eval b y  (exp b y  eval a b)  𝖺[exp b y, exp a b, a]) 
                            (exp b y  f)  𝗋-1[exp b y]"
        unfolding Comp_def by simp
      also have "... = Curry[exp b y, a, y]
                         ((eval b y  (exp b y  eval a b)  𝖺[exp b y, exp a b, a]) 
                            ((exp b y  f)  𝗋-1[exp b y]  a))"
        using assms
              comp_Curry_arr
                [of a "(exp b y  f)  𝗋-1[exp b y]" "exp b y" "exp b y  exp a b"
                    "eval b y  (exp b y  eval a b)  𝖺[exp b y, exp a b, a]" y]
        by auto
      also have "... = Curry[exp b y, a, y]
                         ((eval b y  (exp b y  eval a b)  𝖺[exp b y, exp a b, a]) 
                            (((exp b y  f)  a)  (𝗋-1[exp b y]  a)))"
        using assms comp_arr_dom comp_cod_arr interchange by auto
      also have "... = Curry[exp b y, a, y]
                         (eval b y  (exp b y  eval a b) 
                            (𝖺[exp b y, exp a b, a]  ((exp b y  f)  a)) 
                               (𝗋-1[exp b y]  a))"
        using comp_assoc by simp
      also have "... = Curry[exp b y, a, y]
                         (eval b y  (exp b y  eval a b) 
                            ((exp b y  f  a)  𝖺[exp b y, , a]) 
                               (𝗋-1[exp b y]  a))"
        using assms assoc_naturality [of "exp b y" f a] by auto
      also have "... = Curry[exp b y, a, y]
                         (eval b y 
                            ((exp b y  eval a b)  (exp b y  f  a)) 
                               𝖺[exp b y, , a]  (𝗋-1[exp b y]  a))"
        using comp_assoc by simp
      also have "... = Curry[exp b y, a, y]
                         (eval b y  (exp b y  Uncurry[a, b] f) 
                            𝖺[exp b y, , a]  (𝗋-1[exp b y]  a))"
        using assms comp_arr_dom comp_cod_arr interchange by simp
      also have "... = Curry[exp b y, a, y]
                         (eval b y  (exp b y  Uncurry[a, b] f)  (exp b y  𝗅-1[a]))"
      proof -
        have "exp b y  𝗅-1[a] = inv ((𝗋[exp b y]  a)  𝖺-1[exp b y, , a])"
          using assms triangle' inv_inv iso_inv_iso
          by (metis ide_exp ide_is_iso inv_ide inv_tensor iso_lunit)
        also have "... = 𝖺[exp b y, , a]  (𝗋-1[exp b y]  a)"
          using assms inv_comp by simp
        finally show ?thesis by simp
      qed
      also have "... = Curry[exp b y, a, y]
                         (eval b y  (exp b y  Uncurry[a, b] f  𝗅-1[a]))"
        using assms comp_arr_dom comp_cod_arr interchange by fastforce
      also have "... = Exp (f [a, b]) y"
        using assms DN_def by auto
      finally show ?thesis by simp
    qed

  end

  section "Enriched Yoneda Lemma"

  text‹
    In this section we prove the (weak) Yoneda lemma for enriched categories,
    as in Kelly, Section 1.9.  The weakness is due to the fact that the lemma
    asserts only a bijection between sets, rather than an isomorphism of objects of
    the underlying base category.
  ›

  subsection "Preliminaries"

  text‹
    The following gives conditions under which τ› defined as τ x = (𝒯 x)
    yields an enriched natural transformation between enriched functors F› and G›
    to the self-enriched base category.
  ›

  context elementary_closed_monoidal_category
  begin

    lemma transformation_lam_UP:
    assumes "enriched_functor C T α ι
               ObjA HomA IdA CompA (Collect ide) exp Id Comp Fo Fa"
    assumes "enriched_functor C T α ι
               ObjA HomA IdA CompA (Collect ide) exp Id Comp Go Ga"
    and "x. x  ObjA  𝒯 x = null"
    and "x. x  ObjA  «𝒯 x : Fo x  Go x»"
    and "a b. a  ObjA; b  ObjA 
                  𝒯 b  Uncurry[Fo a, Fo b] (Fa a b) =
                  eval (Go a) (Go b)  (Ga a b  𝒯 a)"
    shows "enriched_natural_transformation C T α ι
             ObjA HomA IdA CompA (Collect ide) exp Id Comp
             Fo Fa Go Ga (λx. (𝒯 x))"
    proof -
      interpret F: enriched_functor C T α ι
                     ObjA HomA IdA CompA Collect ide exp Id Comp Fo Fa
        using assms(1) by blast
      interpret G: enriched_functor C T α ι
                     ObjA HomA IdA CompA Collect ide exp Id Comp Go Ga
        using assms(2) by blast
      show ?thesis
      proof
        show "x. x  ObjA  (𝒯 x) = null"
          unfolding UP_def
          using assms(3) by auto
        show "x. x  ObjA  «(𝒯 x) :   exp (Fo x) (Go x)»"
          unfolding UP_def
          using assms(4)
          apply auto[1]
          by force
        fix a b
        assume a: "a  ObjA" and b: "b  ObjA"
        have 1: "«((𝒯 b)  Fa a b)  𝗅-1[HomA a b]
                     : HomA a b  exp (Fo b) (Go b)  exp (Fo a) (Fo b)»"
          using assms(4) [of b] a b UP_DN F.preserves_Hom
          apply (intro comp_in_homI tensor_in_homI)
              apply auto[5]
          by fastforce
        have 2: "«(Ga a b  (𝒯 a))  𝗋-1[HomA a b]
                     : HomA a b  exp (Go a) (Go b)  exp (Fo a) (Go a)»"
          using assms(4) [of a] a b UP_DN F.preserves_Obj G.preserves_Hom
          apply (intro comp_in_homI tensor_in_homI)
              apply auto[5]
          by fastforce
        have 3: "«Comp (Fo a) (Fo b) (Go b)  ((𝒯 b)  Fa a b)  𝗅-1[HomA a b]
                    : HomA a b  exp (Fo a) (Go b)»"
          using a b 1 F.preserves_Obj G.preserves_Obj by blast
        have 4: "«Comp (Fo a) (Go a) (Go b)  (Ga a b  (𝒯 a))  𝗋-1[HomA a b]
                    : HomA a b  exp (Fo a) (Go b)»"
          using a b 2 F.preserves_Obj G.preserves_Obj by blast

        have "Uncurry[Fo a, Go b]
                (Comp (Fo a) (Fo b) (Go b) 
                   ((𝒯 b)  Fa a b)  𝗅-1[HomA a b]) =
              Uncurry[Fo a, Go b]
                (Curry[exp (Fo b) (Go b)  exp (Fo a) (Fo b), Fo a, Go b]
                  (eval (Fo b) (Go b) 
                     (exp (Fo b) (Go b)  eval (Fo a) (Fo b)) 
                        𝖺[exp (Fo b) (Go b), exp (Fo a) (Fo b), Fo a]) 
                    ((𝒯 b)  Fa a b)  𝗅-1[HomA a b])"
          using a b Comp_def comp_assoc by auto
        also have "... =
              Uncurry[Fo a, Go b]
                (Curry[HomA a b, Fo a, Go b]
                   ((eval (Fo b) (Go b) 
                      (exp (Fo b) (Go b)  eval (Fo a) (Fo b)) 
                         𝖺[exp (Fo b) (Go b), exp (Fo a) (Fo b), Fo a]) 
                           (((𝒯 b)  Fa a b)  𝗅-1[HomA a b]  Fo a)))"
          using a b 1 F.preserves_Obj G.preserves_Obj comp_Curry_arr by auto
        also have "... =
                   (eval (Fo b) (Go b) 
                      (exp (Fo b) (Go b)  eval (Fo a) (Fo b)) 
                         𝖺[exp (Fo b) (Go b), exp (Fo a) (Fo b), Fo a]) 
                           (((𝒯 b)  Fa a b)  𝗅-1[HomA a b]  Fo a)"
          using a b 1 F.preserves_Obj G.preserves_Obj Uncurry_Curry by auto
        also have "... =
                   (eval (Fo b) (Go b) 
                      (exp (Fo b) (Go b)  eval (Fo a) (Fo b)) 
                         𝖺[exp (Fo b) (Go b), exp (Fo a) (Fo b), Fo a]) 
                           ((((𝒯 b)  Fa a b)  Fo a)  (𝗅-1[HomA a b]  Fo a))"
        proof -
          have "seq ((𝒯 b)  Fa a b) 𝗅-1[HomA a b]"
            using assms(4) a b 1 F.preserves_Hom [of a b] UP_DN
            apply (intro seqI)
              apply auto[2]
            by (metis F.A.ide_Hom arrI cod_inv dom_lunit iso_lunit seqE)
          thus ?thesis
            using assms(3) a b F.preserves_Obj F.preserves_Hom interchange
            by simp
        qed
        also have "... =
                   eval (Fo b) (Go b) 
                      (exp (Fo b) (Go b)  eval (Fo a) (Fo b)) 
                         (𝖺[exp (Fo b) (Go b), exp (Fo a) (Fo b), Fo a] 
                           (((𝒯 b)  Fa a b)  Fo a))  (𝗅-1[HomA a b]  Fo a)"
          using comp_assoc by simp
        also have "... =
                   eval (Fo b) (Go b) 
                      (exp (Fo b) (Go b)  eval (Fo a) (Fo b)) 
                         (((𝒯 b)  Fa a b  Fo a) 
                           𝖺[, HomA a b, Fo a]) 
                             (𝗅-1[HomA a b]  Fo a)"
          using assms(4) a b F.preserves_Obj F.preserves_Hom
                assoc_naturality [of "(𝒯 b)" "Fa a b" "Fo a"]
          by force
        also have "... =
                   eval (Fo b) (Go b) 
                      ((exp (Fo b) (Go b)  eval (Fo a) (Fo b)) 
                         ((𝒯 b)  Fa a b  Fo a)) 
                           𝖺[, HomA a b, Fo a]  (𝗅-1[HomA a b]  Fo a)"
          using comp_assoc by simp
        also have "... =
                   eval (Fo b) (Go b) 
                      ((𝒯 b)  Uncurry[Fo a, Fo b] (Fa a b)) 
                           𝖺[, HomA a b, Fo a]  (𝗅-1[HomA a b]  Fo a)"
        proof -
          have "seq (exp (Fo b) (Go b)) (UP (𝒯 b))"
            using assms(4) b F.preserves_Obj G.preserves_Obj by fastforce
          moreover have "seq (eval (Fo a) (Fo b)) (Fa a b  Fo a)"
            using a b F.preserves_Obj F.preserves_Hom by force
          ultimately show ?thesis
            using assms(4) [of b] a b UP_DN(1) comp_cod_arr interchange by auto
        qed
        also have "... =
                   eval (Fo b) (Go b) 
                      (((𝒯 b)  Fo b)  (  Uncurry[Fo a, Fo b] (Fa a b))) 
                           𝖺[, HomA a b, Fo a]  (𝗅-1[HomA a b]  Fo a)"
          using assms(4) [of b] a b F.preserves_Obj F.preserves_Hom [of a b]
                comp_arr_dom comp_cod_arr [of "Uncurry[Fo a, Fo b] (Fa a b)"]
                interchange [of "(𝒯 b)"  "Fo b" "Uncurry[Fo a, Fo b] (Fa a b)"]
          by auto
        also have "... =
                   Uncurry[Fo b, Go b] ((𝒯 b)) 
                      (  Uncurry[Fo a, Fo b] (Fa a b)) 
                         𝖺[, HomA a b, Fo a]  (𝗅-1[HomA a b]  Fo a)"
          using comp_assoc by simp
        also have "... = (𝒯 b  𝗅[Fo b]) 
                           (  Uncurry[Fo a, Fo b] (Fa a b)) 
                             𝖺[, HomA a b, Fo a]  (𝗅-1[HomA a b]  Fo a)"
        proof -
          have "Uncurry[Fo b, Go b] ((𝒯 b)) = 𝒯 b  𝗅[Fo b]"
            unfolding UP_def
            using assms(4) a b Uncurry_Curry
            apply simp
            by (metis F.preserves_Obj arr_lunit cod_lunit comp_in_homI' dom_lunit
                ide_cod ide_unity in_homE mem_Collect_eq)
          thus ?thesis by simp
        qed
        also have "... = 𝒯 b  (𝗅[Fo b]  (  Uncurry[Fo a, Fo b] (Fa a b))) 
                             𝖺[, HomA a b, Fo a]  (𝗅-1[HomA a b]  Fo a)"
          using comp_assoc by simp
        also have "... = 𝒯 b  (Uncurry[Fo a, Fo b] (Fa a b)  𝗅[HomA a b  Fo a]) 
                             𝖺[, HomA a b, Fo a]  (𝗅-1[HomA a b]  Fo a)"
          using a b lunit_naturality [of "Uncurry[Fo a, Fo b] (Fa a b)"]
                F.preserves_Obj F.preserves_Hom [of a b]
          by auto
        also have "... = 𝒯 b  Uncurry[Fo a, Fo b] (Fa a b) 
                           𝗅[HomA a b  Fo a]  𝖺[, HomA a b, Fo a] 
                             (𝗅-1[HomA a b]  Fo a)"
          using comp_assoc by simp
        also have "... = 𝒯 b  Uncurry[Fo a, Fo b] (Fa a b)"
        proof -
          have "𝗅[HomA a b  Fo a]  𝖺[, HomA a b, Fo a] 
                  (𝗅-1[HomA a b]  Fo a) =
                HomA a b  Fo a"
          proof -
            have "𝗅[HomA a b  Fo a]  𝖺[, HomA a b, Fo a] 
                    (𝗅-1[HomA a b]  Fo a) =
                  (𝗅[HomA a b]  Fo a)  (𝗅-1[HomA a b]  Fo a)"
              using a b lunit_tensor' [of "HomA a b" "Fo a"]
              by (metis F.A.ide_Hom F.preserves_Obj comp_assoc mem_Collect_eq)
            also have "... = 𝗅[HomA a b]  𝗅-1[HomA a b]  Fo a  Fo a"
              using a b interchange F.preserves_Obj by force
            also have "... = HomA a b  Fo a"
              using a b F.preserves_Obj by auto
            finally show ?thesis by blast
          qed
          thus ?thesis
            using a b F.preserves_Obj F.preserves_Hom [of a b] comp_arr_dom
            by auto
        qed
        finally have LHS: "Uncurry[Fo a, Go b]
                             (Comp (Fo a) (Fo b) (Go b)  ((𝒯 b)  Fa a b) 
                                𝗅-1[HomA a b]) =
                           𝒯 b  Uncurry[Fo a, Fo b] (Fa a b)"
          by blast

        have "Uncurry[Fo a, Go b] (Comp (Fo a) (Go a) (Go b) 
                (Ga a b  (𝒯 a))  𝗋-1[HomA a b]) =
              Uncurry[Fo a, Go b]
                (Curry[exp (Go a) (Go b)  exp (Fo a) (Go a), Fo a, Go b]
                  (eval (Go a) (Go b) 
                    (exp (Go a) (Go b)  eval (Fo a) (Go a)) 
                      𝖺[exp (Go a) (Go b), exp (Fo a) (Go a), Fo a]) 
                    (Ga a b  (𝒯 a))  𝗋-1[HomA a b])"
          using a b Comp_def comp_assoc by auto
        also have "... =
              Uncurry[Fo a, Go b]
                (Curry[HomA a b, Fo a, Go b]
                  ((eval (Go a) (Go b) 
                     (exp (Go a) (Go b)  eval (Fo a) (Go a)) 
                       𝖺[exp (Go a) (Go b), exp (Fo a) (Go a), Fo a]) 
                        ((Ga a b  (𝒯 a))  𝗋-1[HomA a b]  Fo a)))"
          using assms(3) a b 2 F.preserves_Obj G.preserves_Obj comp_Curry_arr
          by auto
        also have "... =
                  (eval (Go a) (Go b) 
                     (exp (Go a) (Go b)  eval (Fo a) (Go a)) 
                       𝖺[exp (Go a) (Go b), exp (Fo a) (Go a), Fo a]) 
                        ((Ga a b  (𝒯 a))  𝗋-1[HomA a b]  Fo a)"
          using assms(3) a b 2 F.preserves_Obj G.preserves_Obj Uncurry_Curry
          by auto
        also have "... =
                  (eval (Go a) (Go b) 
                     (exp (Go a) (Go b)  eval (Fo a) (Go a)) 
                       𝖺[exp (Go a) (Go b), exp (Fo a) (Go a), Fo a]) 
                        (((Ga a b  (𝒯 a))  Fo a)  (𝗋-1[HomA a b]  Fo a))"
          using assms(4) a b F.preserves_Obj G.preserves_Hom
                interchange [of "Ga a b  (𝒯 a)" "𝗋-1[HomA a b]" "Fo a" "Fo a"]
          by fastforce
        also have "... =
                  eval (Go a) (Go b) 
                    (exp (Go a) (Go b)  eval (Fo a) (Go a)) 
                      (𝖺[exp (Go a) (Go b), exp (Fo a) (Go a), Fo a] 
                         ((Ga a b  (𝒯 a))  Fo a))  (𝗋-1[HomA a b]  Fo a)"
          using comp_assoc by simp
        also have "... =
                  eval (Go a) (Go b) 
                    (exp (Go a) (Go b)  eval (Fo a) (Go a)) 
                      ((Ga a b  (𝒯 a)  Fo a) 
                         𝖺[HomA a b, , Fo a]) 
                           (𝗋-1[HomA a b]  Fo a)"
          using assms(4) a b F.preserves_Obj G.preserves_Hom
                assoc_naturality [of "Ga a b" "(𝒯 a)" "Fo a"]
          by fastforce
        also have "... =
                  eval (Go a) (Go b) 
                    ((exp (Go a) (Go b)  eval (Fo a) (Go a)) 
                       (Ga a b  (𝒯 a)  Fo a)) 
                         𝖺[HomA a b, , Fo a]  (𝗋-1[HomA a b]  Fo a)"
          using comp_assoc by simp
        also have "... =
                  eval (Go a) (Go b) 
                    (Ga a b  Uncurry[Fo a, Go a] ((𝒯 a))) 
                       𝖺[HomA a b, , Fo a]  (𝗋-1[HomA a b]  Fo a)"
          using assms(4) a b F.preserves_Obj G.preserves_Obj
                G.preserves_Hom [of a b] comp_cod_arr interchange
          by fastforce
        also have "... =
                  eval (Go a) (Go b) 
                    ((Ga a b  Go a)  (HomA a b  Uncurry[Fo a, Go a] ((𝒯 a)))) 
                       𝖺[HomA a b, , Fo a]  (𝗋-1[HomA a b]  Fo a)"
        proof -
          have "seq (Go a) (Uncurry[Fo a, Go a] ((𝒯 a)))"
            using assms(4) [of a] a b F.preserves_Obj G.preserves_Obj by auto
          moreover have "Go a  Uncurry[Fo a, Go a] ((𝒯 a)) =
                         Uncurry[Fo a, Go a] ((𝒯 a))"
            using a b F.preserves_Obj G.preserves_Obj calculation(1)
                  comp_ide_arr
            by blast
          ultimately show ?thesis
            using assms(3) a b G.preserves_Hom [of a b] interchange
                  comp_arr_dom
            by auto
        qed
        also have "... =
                  Uncurry[Go a, Go b] (Ga a b) 
                     (HomA a b  Uncurry[Fo a, Go a] ((𝒯 a))) 
                       𝖺[HomA a b, , Fo a]  (𝗋-1[HomA a b]  Fo a)"
          using comp_assoc by simp
        also have "... =
                  Uncurry[Go a, Go b] (Ga a b) 
                     (HomA a b  𝒯 a  𝗅[Fo a]) 
                       𝖺[HomA a b, , Fo a]  (𝗋-1[HomA a b]  Fo a)"
          using assms(4) [of a] a b F.preserves_Obj G.preserves_Obj UP_def
                Uncurry_Curry
          by auto
        also have "... =
                  Uncurry[Go a, Go b] (Ga a b) 
                     ((HomA a b  𝒯 a)  (HomA a b  𝗅[Fo a])) 
                       𝖺[HomA a b, , Fo a]  (𝗋-1[HomA a b]  Fo a)"
          using assms(4) [of a] a b F.preserves_Obj G.preserves_Obj interchange
          by auto
        also have "... =
                  Uncurry[Go a, Go b] (Ga a b)  (HomA a b  𝒯 a) 
                    (HomA a b  𝗅[Fo a])  𝖺[HomA a b, , Fo a] 
                       (𝗋-1[HomA a b]  Fo a)"
          using comp_assoc by simp
        also have "... = Uncurry[Go a, Go b] (Ga a b)  (HomA a b  𝒯 a)"
        proof -
          have "(HomA a b  𝗅[Fo a])  𝖺[HomA a b, , Fo a] 
                   (𝗋-1[HomA a b]  Fo a) =
                HomA a b  Fo a"
          proof -
            have "(HomA a b  𝗅[Fo a])  𝖺[HomA a b, , Fo a] 
                     (𝗋-1[HomA a b]  Fo a) =
                  (𝗋[HomA a b]  Fo a)  (𝗋-1[HomA a b]  Fo a)"
              using a b triangle [of "HomA a b" "Fo a"]
              by (metis F.A.ide_Hom F.preserves_Obj comp_assoc mem_Collect_eq)
            also have "... = 𝗋[HomA a b]  𝗋-1[HomA a b]  Fo a  Fo a"
              using a b interchange F.preserves_Obj by force
            also have "... = HomA a b  Fo a"
              using a b F.preserves_Obj by auto
            finally show ?thesis by blast
          qed
          thus ?thesis
            using assms(4) [of a] a b comp_arr_dom by auto
        qed
        also have "... = eval (Go a) (Go b)  (Ga a b  Go a)  (HomA a b  𝒯 a)"
          using comp_assoc by auto
        also have "... = eval (Go a) (Go b)  (Ga a b  𝒯 a)"
          using assms(4) a b G.preserves_Hom comp_arr_dom comp_cod_arr
                interchange
          by (metis in_homE)
        finally have RHS: "Uncurry[Fo a, Go b]
                             (Comp (Fo a) (Go a) (Go b)  (Ga a b  (𝒯 a)) 
                                𝗋-1[HomA a b]) =
                           eval (Go a) (Go b)  (Ga a b  𝒯 a)"
          by blast

        have "Uncurry[Fo a, Go b]
                (Comp (Fo a) (Fo b) (Go b)  ((𝒯 b)  Fa a b)  𝗅-1[HomA a b]) =
              Uncurry[Fo a, Go b]
                (Comp (Fo a) (Go a) (Go b)  (Ga a b  (𝒯 a))  𝗋-1[HomA a b])"
          using a b assms(5) LHS RHS by simp
        moreover have "«Comp (Fo a) (Fo b) (Go b) 
                          ((𝒯 b)  Fa a b)  𝗅-1[HomA a b]
                          : HomA a b  exp (Fo a) (Go b)»"
            using assms(4) a b 1 F.preserves_Obj G.preserves_Obj
                  F.preserves_Hom G.preserves_Hom
            apply (intro comp_in_homI' seqI)
                  apply auto[1]
            by fastforce+
        moreover have "«Comp (Fo a) (Go a) (Go b) 
                          (Ga a b  (𝒯 a))  𝗋-1[HomA a b]
                          : HomA a b  exp (Fo a) (Go b)»"
            using assms(4) a b 2 UP_DN(1) F.preserves_Obj G.preserves_Obj
                  F.preserves_Hom G.preserves_Hom [of a b]
            apply (intro comp_in_homI' seqI)
                  apply auto[7]
            by fastforce
        ultimately show "Comp (Fo a) (Fo b) (Go b) 
                           ((𝒯 b)  Fa a b)  𝗅-1[HomA a b] =
                         Comp (Fo a) (Go a) (Go b) 
                           (Ga a b  (𝒯 a))  𝗋-1[HomA a b]"
          using a b Curry_Uncurry F.A.ide_Hom F.preserves_Obj
                G.preserves_Obj mem_Collect_eq
          by metis
      qed
    qed

  end

  text‹
    Kelly (1.39) expresses enriched naturality in an alternate form, using the underlying
    functors of the covariant and contravariant enriched hom functors.
  ›

  locale Kelly_1_39 =
    symmetric_monoidal_category +
    elementary_closed_monoidal_category +
    enriched_natural_transformation
    for a :: 'a
    and b :: 'a +
    assumes a: "a  ObjA"
    and b: "b  ObjA"
  begin

    interpretation enriched_category C T α ι Collect ide exp Id Comp
      using is_enriched_in_itself by blast
    interpretation self_enriched_category C T α ι exp eval Curry
      ..

    sublocale cov_Hom: covariant_Hom C T α ι
                         exp eval Curry ObjB HomB IdB CompB Fo a
      using a F.preserves_Obj by unfold_locales
    sublocale cnt_Hom: contravariant_Hom C T α ι σ
                         exp eval Curry ObjB HomB IdB CompB Go b
      using b G.preserves_Obj by unfold_locales

    lemma Kelly_1_39:
    shows "cov_Hom.map0 (Fo b) (Go b) (τ b)  Fa a b =
           cnt_Hom.map0 (Fo a) (Go a) (τ a)  Ga a b"
    proof -
      have "cov_Hom.map0 (Fo b) (Go b) (τ b)  Fa a b =
            CompB (Fo a) (Fo b) (Go b)  (τ b  Fa a b)  𝗅-1[HomA a b]"
      proof -
        have "cov_Hom.map0 (Fo b) (Go b) (τ b)  Fa a b =
              CompB (Fo a) (Fo b) (Go b) 
                (τ b  HomB (Fo a) (Fo b))  𝗅-1[HomB (Fo a) (Fo b)]  Fa a b"
          using comp_assoc by simp
        also have "... = CompB (Fo a) (Fo b) (Go b) 
                            (τ b  HomB (Fo a) (Fo b))  (  Fa a b)  𝗅-1[HomA a b]"
          using a b lunit'_naturality F.preserves_Hom [of a b] by fastforce
        also have "... = CompB (Fo a) (Fo b) (Go b) 
                            ((τ b  HomB (Fo a) (Fo b))  (  Fa a b)) 
                               𝗅-1[HomA a b]"
          using comp_assoc by simp
        also have "... = CompB (Fo a) (Fo b) (Go b)  (τ b  Fa a b) 
                           𝗅-1[HomA a b]"
          using a b component_in_hom [of b] F.preserves_Hom [of a b]
                comp_arr_dom comp_cod_arr [of "Fa a b" "HomB (Fo a) (Fo b)"]
                interchange
          by fastforce
        finally show ?thesis by blast
      qed
      moreover have "cnt_Hom.map0 (Fo a) (Go a) (τ a)  Ga a b =
                     CompB (Fo a) (Go a) (Go b)  (Ga a b  τ a)  𝗋-1[HomA a b]"
      proof -
        have "cnt_Hom.map0 (Fo a) (Go a) (τ a)  Ga a b =
              CompB (Fo a) (Go a) (Go b)  (HomB (Go a) (Go b)  τ a) 
                 𝗋-1[HomB (Go a) (Go b)]  Ga a b"
          using comp_assoc by simp
        also have "... = CompB (Fo a) (Go a) (Go b) 
                           (HomB (Go a) (Go b)  τ a)  (Ga a b  ) 
                              𝗋-1[HomA a b]"
          using a b runit'_naturality G.preserves_Hom [of a b] by fastforce
        also have "... = CompB (Fo a) (Go a) (Go b) 
                           ((HomB (Go a) (Go b)  τ a)  (Ga a b  )) 
                               𝗋-1[HomA a b]"
          using comp_assoc by simp
        also have "... = CompB (Fo a) (Go a) (Go b)  (Ga a b  τ a) 
                           𝗋-1[HomA a b]"
          using a b interchange component_in_hom [of a] G.preserves_Hom [of a b]
                comp_arr_dom comp_cod_arr [of "Ga a b" "HomB (Go a) (Go b)"]
          by fastforce
        finally show ?thesis by blast
      qed
      ultimately show ?thesis
        using a b naturality by simp
    qed

  end

  subsection "Covariant Case"

  locale covariant_yoneda_lemma =
    symmetric_monoidal_category +
    C: closed_symmetric_monoidal_category +
    covariant_Hom +
    F: enriched_functor C T α ι Obj Hom Id Comp Collect ide exp C.Id C.Comp
  begin

    interpretation C: elementary_closed_symmetric_monoidal_category C T α ι σ exp eval Curry ..
    interpretation C: self_enriched_category C T α ι exp eval Curry ..
 
    text‹
      Every element e : ℐ → Fo x› of Fo x› determines an enriched natural transformation
      τe: hom x - → F›.  The formula here is Kelly (1.47): τe y: hom x y → F y›
      is obtained as the composite:
      \[
        hom x y› \labarrow{Fa x y›} exp (F x) (F y)›
                  \labarrow{Exp e (F y)›} exp ℐ (F y)› \labarrow{} F y›
      \]
      where the third component is a canonical isomorphism.
      This basically amounts to evaluating Fa x y› on element e› of Fo x› to obtain
      an element of Fo y›.

      Note that the above composite gives an arrow τe y: hom x y → F y›, whereas the
      definition of enriched natural transformation formally requires
      τe y: ℐ → exp (hom x y) (F y)›.
      So we need to transform the composite to achieve that.
    ›

    abbreviation generated_transformation
    where "generated_transformation e 
           λy. (eval  (Fo y)  𝗋-1[exp  (Fo y)]  Exp e (Fo y)  Fa x y)"

    lemma enriched_natural_transformation_generated_transformation:
    assumes "«e :   Fo x»"
    shows "enriched_natural_transformation C T α ι
             Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
             homo homa Fo Fa (generated_transformation e)"
    proof (intro C.transformation_lam_UP)
      show "y. y  Obj 
                  eval  (Fo y)  𝗋-1[exp  (Fo y)]  Exp e (Fo y)  Fa x y = null"
        by (simp add: F.extensionality)
      show "enriched_functor (⋅) T α ι Obj Hom Id Comp
              (Collect ide) exp C.Id C.Comp homo homa"
        ..
      show "enriched_functor (⋅) T α ι Obj Hom Id Comp
              (Collect ide) exp C.Id C.Comp Fo Fa"
        ..
      show *: "y. y  Obj 
                     «eval  (Fo y)  𝗋-1[exp  (Fo y)]  Exp e (Fo y)  Fa x y
                        : homo y  Fo y»"
        using assms x F.preserves_Obj F.preserves_Hom
        apply (intro in_homI seqI)
                apply auto[6]
        by fastforce+
      show "a b. a  Obj; b  Obj 
                    (eval  (Fo b)  𝗋-1[exp  (Fo b)] 
                       Exp e (Fo b)  Fa x b) 
                         Uncurry[homo a, homo b] (homa a b) =
                    eval (Fo a) (Fo b) 
                      (Fa a b  eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                         Exp e (Fo a)  Fa x a)"
      proof -
        fix a b
        assume a: "a  Obj" and b: "b  Obj"
        have "(eval  (Fo b)  𝗋-1[exp  (Fo b)] 
                 Exp e (Fo b)  Fa x b)  Uncurry[homo a, homo b] (homa a b) =
              eval (Fo x) (Fo b)  (Fa x b  Comp x a b  e) 
                𝗋-1[Hom a b  homo a]"
        proof -
          have "(eval  (Fo b)  𝗋-1[exp  (Fo b)] 
                   Exp e (Fo b)  Fa x b)  Uncurry[homo a, homo b] (homa a b) =
                eval  (Fo b) 
                   (𝗋-1[exp  (Fo b)]  Exp e (Fo b)  Fa x b) 
                      Uncurry[homo a, homo b] (homa a b)"
            using comp_assoc by simp
          also have "... = eval  (Fo b) 
                             (𝗋-1[exp  (Fo b)]  Exp e (Fo b)  Fa x b) 
                               Comp x a b"
            using a b x C.Uncurry_Curry [of _ "homo a" "homo b"] Comp_in_hom
            by auto
          also have "... = eval  (Fo b) 
                             ((Exp e (Fo b)  Fa x b  ) 
                                 𝗋-1[homo b])  Comp x a b"
          proof -
            have "«Exp e (Fo b)  Fa x b : homo b  exp  (Fo b)»"
              using assms a b x F.preserves_Obj F.preserves_Hom [of x b] by force
            thus ?thesis
              using a b F.preserves_Obj F.preserves_Hom
                    runit'_naturality [of "Exp e (Fo b)  Fa x b"]
              by auto
          qed
          also have "... = eval  (Fo b) 
                             (((Exp e (Fo b)  )  (Fa x b  )) 
                                  𝗋-1[homo b]) 
                               Comp x a b"
            using assms a b x F.preserves_Obj F.preserves_Hom [of x b]
                  interchange [of "Exp e (Fo b)" "Fa x b"  ]
            by fastforce
          also have "... = Uncurry[, Fo b] (Exp e (Fo b))  (Fa x b  ) 
                             𝗋-1[homo b]  Comp x a b"
            using comp_assoc by simp
          also have "... = (eval (Fo x) (Fo b)  (exp (Fo x) (Fo b)  e)) 
                              (Fa x b  )  𝗋-1[homo b]  Comp x a b"
            using assms a b x F.preserves_Obj C.Uncurry_Curry by auto
          also have "... = eval (Fo x) (Fo b) 
                             ((exp (Fo x) (Fo b)  e)  (Fa x b  )) 
                               𝗋-1[homo b]  Comp x a b"
            using comp_assoc by simp
          also have "... = eval (Fo x) (Fo b)  (Fa x b  e)  𝗋-1[homo b] 
                             Comp x a b"
            using assms a b x F.preserves_Hom [of x b]
                  comp_cod_arr [of "Fa x b" "exp (Fo x) (Fo b)"] comp_arr_dom
                  interchange
            by fastforce
          also have "... = eval (Fo x) (Fo b)  (Fa x b  e) 
                             (Comp x a b  )  𝗋-1[Hom a b  homo a]"
            using assms a b x runit'_naturality [of "Comp x a b"]
                  Comp_in_hom [of x a b]
            by auto
          also have "... = eval (Fo x) (Fo b)  ((Fa x b  e)  (Comp x a b  )) 
                             𝗋-1[Hom a b  homo a]"
            using comp_assoc by simp
          also have "... = eval (Fo x) (Fo b)  (Fa x b  Comp x a b  e) 
                             𝗋-1[Hom a b  homo a]"
            using assms a b x F.preserves_Hom [of x b] Comp_in_hom comp_arr_dom
                  interchange [of "Fa x b" "Comp x a b" e ]
            by fastforce
          finally show ?thesis by blast
        qed
        also have "... = eval (Fo a) (Fo b) 
                           (Fa a b  eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                              Exp e (Fo a)  Fa x a)"
        proof -
          have "eval (Fo a) (Fo b) 
                  (Fa a b  eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                     Exp e (Fo a)  Fa x a) =
                eval (Fo a) (Fo b) 
                  (Fa a b  eval  (Fo a)  (𝗋-1[exp  (Fo a)] 
                     Exp e (Fo a))  Fa x a)"
            using comp_assoc by simp
          also have "... =
                eval (Fo a) (Fo b) 
                  (Fa a b  eval  (Fo a) 
                    ((Exp e (Fo a)  )  𝗋-1[exp (Fo x) (Fo a)]) 
                       Fa x a)"
            using assms a b x F.preserves_Obj F.preserves_Hom
                  runit'_naturality [of "Exp e (Fo a)"]
            by auto
          also have "... =
                eval (Fo a) (Fo b) 
                  (Fa a b 
                     Uncurry[, Fo a] (Exp e (Fo a))  𝗋-1[exp (Fo x) (Fo a)] 
                       Fa x a)"
            using comp_assoc by simp
          also have "... =
                eval (Fo a) (Fo b) 
                  (Fa a b 
                     (eval (Fo x) (Fo a)  (exp (Fo x) (Fo a)  e)) 
                        𝗋-1[exp (Fo x) (Fo a)]  Fa x a)"
            using assms a b x F.preserves_Obj C.Uncurry_Curry by auto
          also have "... =
                eval (Fo a) (Fo b) 
                  (Fa a b 
                     (eval (Fo x) (Fo a)  (exp (Fo x) (Fo a)  e)) 
                        (Fa x a  )  𝗋-1[homo a])"
            using a b x F.preserves_Hom [of x a] runit'_naturality by fastforce
          also have "... =
                eval (Fo a) (Fo b) 
                  (Fa a b 
                     eval (Fo x) (Fo a)  (exp (Fo x) (Fo a)  e) 
                       (Fa x a  )  𝗋-1[homo a])"
            using comp_assoc by simp
          also have "... =
                eval (Fo a) (Fo b) 
                  (Fa a b  eval (Fo x) (Fo a)  (Fa x a  e)  𝗋-1[homo a])"
            using assms a b x F.preserves_Obj F.preserves_Hom F.preserves_Hom
                  comp_arr_dom [of e ]
                  comp_cod_arr [of "Fa x a" "exp (Fo x) (Fo a)"]
                  interchange [of "exp (Fo x) (Fo a)" "Fa x a" e ] comp_assoc
            by (metis in_homE)
          also have "... =
                eval (Fo a) (Fo b) 
                  (exp (Fo a) (Fo b)  eval (Fo x) (Fo a)) 
                    (Fa a b  (Fa x a  e)  𝗋-1[homo a])"
            using assms a b x F.preserves_Obj F.preserves_Hom [of x a]
                  F.preserves_Hom [of a b]
                  comp_cod_arr [of "Fa a b" "exp (Fo a) (Fo b)"]
                  interchange
                    [of "exp (Fo a) (Fo b)" "Fa a b"
                        "eval (Fo x) (Fo a)" "(Fa x a  e)  𝗋-1[homo a]"]
            by fastforce
          also have "... = (eval (Fo a) (Fo b) 
                              (exp (Fo a) (Fo b)  eval (Fo x) (Fo a))) 
                             (Fa a b  (Fa x a  e)  𝗋-1[homo a])"
            using comp_assoc by simp
          also have "... = (eval (Fo a) (Fo b) 
                              (exp (Fo a) (Fo b)  eval (Fo x) (Fo a))) 
                             (Fa a b  (Fa x a  e))  (Hom a b  𝗋-1[homo a])"
            using assms a b x F.preserves_Obj F.preserves_Hom [of a b]
                  F.preserves_Hom [of x a] comp_arr_dom [of "Fa a b" "Hom a b"]
                  interchange [of "Fa a b" "Hom a b" "Fa x a  e" "𝗋-1[homo a]"]
            by fastforce
          also have "... = (eval (Fo a) (Fo b) 
                              (exp (Fo a) (Fo b)  eval (Fo x) (Fo a))) 
                             (exp (Fo a) (Fo b)  exp (Fo x) (Fo a)  Fo x) 
                             (Fa a b  Fa x a  e)  (Hom a b  𝗋-1[homo a])"
            using assms a b x F.preserves_Obj F.preserves_Hom [of a b]
                  F.preserves_Hom [of x a]
                  comp_cod_arr [of "(Fa a b  Fa x a  e)  (Hom a b  𝗋-1[homo a])"
                                   "exp (Fo a) (Fo b)  exp (Fo x) (Fo a)  Fo x"]
            by fastforce
          also have "... = (eval (Fo a) (Fo b) 
                              (exp (Fo a) (Fo b)  eval (Fo x) (Fo a))) 
                             (𝖺[exp (Fo a) (Fo b), exp (Fo x) (Fo a), Fo x] 
                                𝖺-1[exp (Fo a) (Fo b), exp (Fo x) (Fo a), Fo x]) 
                             (Fa a b  (Fa x a  e))  (Hom a b  𝗋-1[homo a])"
            using assms a b x F.preserves_Obj comp_assoc_assoc' by simp
          also have "... = (eval (Fo a) (Fo b) 
                              (exp (Fo a) (Fo b)  eval (Fo x) (Fo a)) 
                              𝖺[exp (Fo a) (Fo b), exp (Fo x) (Fo a), Fo x]) 
                              (𝖺-1[exp (Fo a) (Fo b), exp (Fo x) (Fo a), Fo x] 
                                (Fa a b  Fa x a  e))  (Hom a b  𝗋-1[homo a])"
            using comp_assoc by simp
          also have "... = Uncurry[Fo x, Fo b] (C.Comp (Fo x) (Fo a) (Fo b)) 
                              (𝖺-1[exp (Fo a) (Fo b), exp (Fo x) (Fo a), Fo x] 
                                (Fa a b  Fa x a  e))  (Hom a b  𝗋-1[homo a])"
            using assms a b x F.preserves_Obj C.Uncurry_Curry C.Comp_def
            by auto
          also have "... = Uncurry[Fo x, Fo b] (C.Comp (Fo x) (Fo a) (Fo b)) 
                              (((Fa a b  Fa x a)  e)  𝖺-1[Hom a b, homo a, ]) 
                                (Hom a b  𝗋-1[homo a])"
            using assms a b x F.preserves_Hom [of a b] F.preserves_Hom [of x a]
                  assoc'_naturality [of "Fa a b" "Fa x a" e]
            by fastforce
          also have "... = eval (Fo x) (Fo b) 
                             ((C.Comp (Fo x) (Fo a) (Fo b)  Fo x) 
                                ((Fa a b  Fa x a)  e)) 
                               𝖺-1[Hom a b, homo a, ]  (Hom a b  𝗋-1[homo a])"
            using comp_assoc by simp
          also have "... = eval (Fo x) (Fo b) 
                             (C.Comp (Fo x) (Fo a) (Fo b)  (Fa a b  Fa x a)  e) 
                               𝖺-1[Hom a b, homo a, ]  (Hom a b  𝗋-1[homo a])"
            using assms a b x F.preserves_Obj F.preserves_Hom [of a b]
                  F.preserves_Hom [of x a] comp_cod_arr [of e "Fo x"]
                  interchange
                    [of "C.Comp (Fo x) (Fo a) (Fo b)" "Fa a b  Fa x a" "Fo x" e]
            by fastforce
          also have "... = eval (Fo x) (Fo b)  (Fa x b  Comp x a b  e) 
                               𝖺-1[Hom a b, homo a, ]  (Hom a b  𝗋-1[homo a])"
            using assms a b x F.preserves_Obj F.preserves_Hom F.preserves_Comp
            by simp
          also have "... = eval (Fo x) (Fo b)  (Fa x b  Comp x a b  e) 
                             𝗋-1[Hom a b  homo a]"
          proof -
            have "𝖺-1[Hom a b, homo a, ]  (Hom a b  𝗋-1[homo a]) =
                  𝗋-1[Hom a b  homo a]"
            proof -
              have "𝖺-1[Hom a b, homo a, ]  (Hom a b  𝗋-1[homo a]) =
                    inv ((Hom a b  𝗋[homo a])  𝖺[Hom a b, homo a, ])"
                using assms a b x inv_comp by auto
              also have "... = 𝗋-1[Hom a b  homo a]"
                using assms a b x runit_tensor by auto
              finally show ?thesis by blast
            qed
            thus ?thesis by simp
          qed
          finally show ?thesis by simp
        qed
        finally show "(eval  (Fo b)  𝗋-1[exp  (Fo b)]  Exp e (Fo b)  Fa x b) 
                         Uncurry[homo a, homo b] (homa a b) =
                      eval (Fo a) (Fo b)  (Fa a b  eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                         Exp e (Fo a)  Fa x a)"
          by argo
      qed
    qed

    text‹
      If τ: hom x - → F› is an enriched natural transformation, then there exists an
      element eτ : ℐ → F x› that generates τ› via the preceding formula.
      The idea (Kelly 1.46) is to take:
      \[
          eτ = ℐ›\;\labarrow{Id x›}\;homo x›\;\labarrow{τ x›}\; F x›
      \]
      This amounts to the ``evaluation of τ x› at the identity on x›''.

      However, note once again that, according to the formal definition of enriched
      natural transformation, we have τ x : ℐ → exp (homo x) (Fo x)›, so it is
      necessary to transform this to an arrow: (τ x) [homo x, Fo x]: homo x → F x›.
    ›

    abbreviation generating_elem
    where "generating_elem τ  (τ x) [homo x, Fo x]  Id x"

    lemma generating_elem_in_hom:
    assumes "enriched_natural_transformation C T α ι
               Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
               homo homa Fo Fa τ"
    shows "«generating_elem τ :   Fo x»"
    proof -
      interpret τ: enriched_natural_transformation C T α ι
                     Obj Hom Id Comp Collect ide exp C.Id C.Comp
                     homo homa Fo Fa τ
        using assms by blast
      show "«generating_elem τ :   Fo x»"
        using x Id_in_hom τ.component_in_hom [of x] F.preserves_Obj C.DN_def
        by auto fastforce
    qed
    text‹
      Now we have to verify the elements of the diagram after Kelly (1.47):
$$\xymatrix{
 homo a›
   \xuppertwocell[rrrrr]{}^{homo a›}<15>{\omit{}}
   \ar[rr] _{homa x a›}
   \ar[d] _{Fa a›}
  &&
 [homo x, homo a]›
   \ar[rr] _{[Id x, homo a]›}
   \ar[d] ^{[homo x, τ a]›}
  &&
 [ℐ, homo a]›
   \ar[r] _{\textrm{iso}}
   \ar[d] ^{[ℐ, τ a]›}
  &
 homo a›
   \ar[d] ^{τ a›}
  \\
 [Fo x, Fo a]›
   \ar[rr] ^{e x, Fo a]›}
   \xlowertwocell[rrrr]{}_{e x ⋅ Id x, Fo a]›}<-15>{\omit{}}
  &&
 [homo x, Fo a]›
   \ar[rr] ^{[Id x, Fo a]›}
  &&
 [ℐ, Fo a]›
   \ar[r] ^{\textrm{iso}}
  &
 Fo a›
}$$
    ›
    (*
                   homa x a                    [Id x, homo a]           iso
         homo a ----------------> [homo x, homo a] -------> [ℐ, homo a] -----> homo a
           |                             |                     |               |
       Fa  |                             | [homo x, τ a]        | [ℐ, τ a ]     | τ a
           v                             v                     v               v
         [Fo x, Fo a] ----------> [homo x, Fo a] ----------> [ℐ, Fo a] -------> Fo a
                     [τe x, Fo a]                [Id x, Fo a]             iso
                                      =
                                [τe x, Fo a]
     *)
    text‹
      The left square is enriched naturality of τ› (Kelly (1.39)).
      The middle square commutes trivially.
      The right square commutes by the naturality of the canonical isomorphismm
      from [ℐ, homo a]› to homo a›.
      The top edge composes to homo a› (an identity).
      The commutativity of the entire diagram shows that τ a› is recovered from eτ.
      Note that where τ a› appears, what is actually meant formally is (τ a) [homo a, Fo a]›.
    ›

    lemma center_square:
    assumes "enriched_natural_transformation C T α ι
               Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
               homo homa Fo Fa τ"
    and "a  Obj"
    shows "C.Exp  (τ a [homo a, Fo a])  C.Exp (Id x) (homo a) =
           C.Exp (Id x) (Fo a)  C.Exp (homo x) (τ a [homo a, Fo a])"
    proof -
      interpret τ: enriched_natural_transformation C T α ι
                     Obj Hom Id Comp Collect ide exp C.Id C.Comp
                     homo homa Fo Fa τ
        using assms by blast
      let a = "τ a [homo a, Fo a]"
      show "C.Exp  a  C.Exp (Id x) (homo a) =
            C.Exp (Id x) (Fo a)  C.Exp (homo x) a"
        by (metis assms(2) x C.Exp_comp F.preserves_Obj Id_in_hom
            C.DN_simps(1-3) comp_arr_dom comp_cod_arr in_homE τ.component_in_hom
            ide_Hom mem_Collect_eq)
    qed

    lemma right_square:
    assumes "enriched_natural_transformation C T α ι
               Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
               homo homa Fo Fa τ"
    and "a  Obj"
    shows "τ a [homo a, Fo a]  C.Dn (homo a) =
           C.Dn (Fo a)  C.Exp  (τ a [homo a, Fo a])"
    proof -
      interpret τ: enriched_natural_transformation C T α ι
                     Obj Hom Id Comp Collect ide exp C.Id C.Comp
                     homo homa Fo Fa τ
        using assms by blast
      show ?thesis
        using assms(2) C.Up_Dn_naturality C.DN_simps τ.component_in_hom
        apply auto[1]
        by (metis C.Exp_ide_y C.UP_DN(2) F.preserves_Obj ide_Hom ide_unity
            in_homE mem_Collect_eq x)
    qed

    lemma top_path:
    assumes "a  Obj"
    shows "eval  (homo a)  𝗋-1[exp  (homo a)]  C.Exp (Id x) (homo a) 
             homa x a =
           homo a"
    proof -
      have "eval  (homo a)  𝗋-1[exp  (homo a)]  C.Exp (Id x) (homo a) 
              homa x a =
            eval  (homo a)  𝗋-1[exp  (homo a)] 
              (Curry[exp  (homo a), , homo a] (homo a  eval  (homo a)) 
                 Curry[exp (homo x) (homo a), , homo a]
                   (eval (homo x) (homo a)  (exp (homo x) (homo a)  Id x))) 
              homa x a"
        using assms x C.Exp_def Id_in_hom [of x] by auto
      also have "... =
            eval  (homo a)  𝗋-1[exp  (homo a)] 
              Curry[exp  (homo a), , homo a] (homo a  eval  (homo a)) 
                Curry[exp (homo x) (homo a), , homo a]
                  (eval (homo x) (homo a)  (exp (homo x) (homo a)  Id x)) 
                     homa x a"
        using comp_assoc by simp
      also have "... =
            eval  (homo a)  𝗋-1[exp  (homo a)] 
              Curry[exp  (homo a), , homo a] (homo a  eval  (homo a)) 
                Curry[homo a, , homo a]
                  ((eval (homo x) (homo a)  (exp (homo x) (homo a)  Id x)) 
                     (homa x a  ))"
      proof -
        have "«eval (homo x) (homo a)  (exp (homo x) (homo a)  Id x)
                 : exp (homo x) (homo a)    homo a»"
          using assms x
          by (meson Id_in_hom comp_in_homI C.eval_in_hom_ax C.ide_exp
              ide_in_hom tensor_in_hom ide_Hom)
        thus ?thesis
          using assms x preserves_Hom [of x a] C.comp_Curry_arr by simp
      qed
      also have "... =
            eval  (homo a)  𝗋-1[exp  (homo a)] 
              Curry[exp  (homo a), , homo a] (homo a  eval  (homo a)) 
                Curry[homo a, , homo a]
                  (eval (homo x) (homo a) 
                     (exp (homo x) (homo a)  Id x)  (homa x a  ))"
        using comp_assoc by simp
      also have "... =
            eval  (homo a)  𝗋-1[exp  (homo a)] 
              Curry[exp  (homo a), , homo a] (homo a  eval  (homo a)) 
                Curry[homo a, , homo a]
                  (eval (homo x) (homo a)  (homa x a  Id x))"
      proof -
        have "seq (Id x)   seq (homo x) (Id x)"
          using x Id_in_hom ide_in_hom ide_unity by blast
        thus ?thesis
          using assms x preserves_Hom comp_arr_dom [of "Id x" ]
                interchange [of "exp (homo x) (homo a)" "homa x a" "Id x" ]
          by (metis comp_cod_arr comp_ide_arr dom_eqI ide_unity
              in_homE ide_Hom)
      qed
      also have "... =
            eval  (homo a)  𝗋-1[exp  (homo a)] 
              Curry[exp  (homo a), , homo a] (eval  (homo a)) 
                Curry[homo a, , homo a]
                  (Uncurry[homo x, homo a] (homa x a)  (homo a  Id x))"
      proof -
        have "eval (homo x) (homo a)  (homa x a  Id x) =
              eval (homo x) (homo a)  (homa x a  homo a  homo x  Id x)"
          using assms x Id_in_hom comp_cod_arr comp_arr_dom Comp_in_hom
          by (metis in_homE preserves_Hom)
        also have "... = eval (homo x) (homo a)  (homa x a  homo x) 
                           (homo a  Id x)"
            using assms x Id_in_hom Comp_in_hom
                  interchange [of "homa x a" "homo a" "homo x" "Id x"]
            by (metis comp_arr_dom comp_cod_arr in_homE preserves_Hom)
        also have "... = Uncurry[homo x, homo a] (homa x a)  (homo a  Id x)"
          using comp_assoc by simp
        finally show ?thesis
          using assms x comp_cod_arr ide_Hom ide_unity C.eval_simps(1,3) by metis
      qed
      also have "... =
            eval  (homo a)  𝗋-1[exp  (homo a)] 
              Curry[homo a, , homo a]
                (Uncurry[, homo a]
                   (Curry[homo a, , homo a]
                      (Uncurry[homo x, homo a] (homa x a)  (homo a  Id x))))"
        using assms x
              C.comp_Curry_arr
                 [of 
                     "Curry[homo a, , homo a]
                        (Uncurry[homo x, homo a] (homa x a)  (homo a  Id x))"
                     "homo a" "exp  (homo a)"
                     "eval  (homo a)" "homo a"]
        apply auto[1]
        by (metis Comp_Hom_Id Comp_in_hom C.Uncurry_Curry C.eval_in_hom_ax
            ide_unity C.isomorphic_exp_unity(1) ide_Hom)
      also have "... =
            eval  (homo a)  𝗋-1[exp  (homo a)] 
              Curry[homo a, , homo a]
                (Uncurry[homo x, homo a] (homa x a)  (homo a  Id x))"
        using assms x C.Uncurry_Curry
        by (simp add: Comp_Hom_Id Comp_in_hom C.Curry_Uncurry
            C.isomorphic_exp_unity(1))
      also have "... =
            eval  (homo a)  𝗋-1[exp  (homo a)] 
              Curry[homo a, , homo a]
                (eval (homo x) (homo a)  (homa x a  homo x)  (homo a  Id x))"
        using comp_assoc by simp
      also have "... =
            eval  (homo a)  𝗋-1[exp  (homo a)] 
              Curry[homo a, , homo a]
                (eval (homo x) (homo a)  (homa x a  Id x))"
        using assms x comp_cod_arr [of "Id x" "homo x"] comp_arr_dom
              interchange [of "homa x a" "homo a" "homo x" "Id x"]
              preserves_Hom [of x a] Id_in_hom
        apply auto[1]
        by fastforce
      also have "... =
            eval  (homo a) 
              (Curry[homo a, , homo a]
                 (eval (homo x) (homo a)  (homa x a  Id x))  ) 
                 𝗋-1[homo a]"
      proof -
        have "«Curry[homo a, , homo a]
                 (eval (homo x) (homo a)  (homa x a  Id x))
                 : homo a  exp  (homo a)»"
          using assms x preserves_Hom [of x a] Id_in_hom [of x] by force
        thus ?thesis
          using assms x runit'_naturality by fastforce
      qed
      also have "... =
             Uncurry[, homo a]
               (Curry[homo a, , homo a]
                  (eval (homo x) (homo a)  (homa x a  Id x)))  𝗋-1[homo a]"
        using comp_assoc by simp
      also have "... = (eval (homo x) (homo a) 
                         (Curry[homo a, homo x, homo a] (Comp x x a)  Id x)) 
                            𝗋-1[homo a]"
        using assms x C.Uncurry_Curry preserves_Hom [of x a] Id_in_hom [of x]
        by fastforce
      also have "... = (eval (homo x) (homo a) 
                         ((Curry[homo a, homo x, homo a] (Comp x x a)  homo x) 
                            (homo a  Id x)))  𝗋-1[homo a]"
        using assms x Id_in_hom [of x] Comp_in_hom comp_arr_dom comp_cod_arr
              interchange
        by auto
      also have "... = Uncurry[homo x, homo a]
                         (Curry[homo a, homo x, homo a] (Comp x x a)) 
                         (homo a  Id x)  𝗋-1[homo a]"
        using comp_assoc by simp
      also have "... = Comp x x a  (homo a  Id x)  𝗋-1[homo a]"
        using assms x C.Uncurry_Curry Comp_in_hom by simp
      also have "... = (Comp x x a  (homo a  Id x))  𝗋-1[homo a]"
        using comp_assoc by simp
      also have "... = 𝗋[homo a]  𝗋-1[homo a]"
        using assms x Comp_Hom_Id by auto
      also have "... = homo a"
        using assms x comp_runit_runit' by blast
      finally show ?thesis by blast
    qed

    text‹
      The left square is an instance of Kelly (1.39), so we can get that by
      instantiating that result.  The confusing business is that the target
      enriched category is the base category C.
    ›

    lemma left_square:
    assumes "enriched_natural_transformation C T α ι
               Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
               homo homa Fo Fa τ"
    and "a  Obj"
    shows "Exp (homo x) ((τ a) [homo a, Fo a])  homa x a =
           Exp ((τ x) [homo x, Fo x]) (Fo a)  Fa x a"
    proof -
      interpret τ: enriched_natural_transformation C T α ι
                     Obj Hom Id Comp Collect ide exp C.Id C.Comp
                     homo homa Fo Fa τ
        using assms(1) by blast

      interpret cov_Hom: covariant_Hom C T α ι exp eval Curry
                           Collect ide exp C.Id C.Comp homo x
        using x by unfold_locales auto
      interpret cnt_Hom: contravariant_Hom C T α ι σ exp eval Curry
                           Collect ide exp C.Id C.Comp Fo a
        using assms(2) F.preserves_Obj by unfold_locales
      interpret Kelly: Kelly_1_39 C T α ι σ exp eval Curry
                         Obj Hom Id Comp Collect ide exp C.Id C.Comp
                         homo homa Fo Fa τ x a
        using assms(2) x
        by unfold_locales

      text‹
        The following is the enriched naturality of τ›, expressed in the alternate form
        involving the underlying ordinary functors of the enriched hom functors.
      ›
      have 1: "cov_Hom.map0 (homo a) (Fo a) (τ a)  homa x a =
               cnt_Hom.map0 (homo x) (Fo x) (τ x)  Fa x a"
        using Kelly.Kelly_1_39 by simp

      text‹
        Here we have the underlying ordinary functor of the enriched covariant hom,
        expressed in terms of the covariant endofunctor Exp (homo x)› on the base
        category.
      ›
      have 2: "cov_Hom.map0 (homo a) (Fo a) (τ a) =
               Exp (homo x) ((τ a) [homo a, Fo a])"
      proof -
        have "cov_Hom.map0 (homo a) (Fo a) (τ a) =
              (Curry[cnt_Hom.homo (homo a), cov_Hom.homo (homo a),
                     cnt_Hom.homo (homo x)]
                 (C.Comp (homo x) (homo a) (Fo a))  τ a)
                [cov_Hom.homo (homo a), cnt_Hom.homo (homo x)]"
        proof -
          have "cov_Hom.map0 (homo a) (Fo a) (τ a) =
                  cnt_Hom.Op0.Map
                    (cov_Hom.UF.map0 (cnt_Hom.Op0.MkArr (homo a) (Fo a) (τ a)))
                    [cnt_Hom.Op0.Dom
                        (cov_Hom.UF.map0
                           (cnt_Hom.Op0.MkArr (homo a) (Fo a) (τ a))),
                      cnt_Hom.Op0.Cod
                        (cov_Hom.UF.map0
                           (cnt_Hom.Op0.MkArr (homo a) (Fo a) (τ a)))]"
            using assms x preserves_Obj F.preserves_Obj τ.component_in_hom
                  cov_Hom.Kelly_1_31 cov_Hom.UF.preserves_arr
            by force
          moreover
          have "cnt_Hom.Op0.Dom
                  (cov_Hom.UF.map0
                     (cnt_Hom.Op0.MkArr (homo a) (Fo a) (τ a))) =
                exp (homo x) (homo a)"
            using assms x cov_Hom.UF.map0_def
            apply auto[1]
            using cnt_Hom.y τ.component_in_hom by force
          moreover
          have "cnt_Hom.Op0.Cod
                  (cov_Hom.UF.map0
                     (cnt_Hom.Op0.MkArr (homo a) (Fo a) (τ a))) =
                exp (homo x) (Fo a)"
            using assms x cov_Hom.UF.map0_def
            apply auto[1]
            using cnt_Hom.y τ.component_in_hom by fastforce
          moreover
          have "cnt_Hom.Op0.Map
                  (cov_Hom.UF.map0
                     (cnt_Hom.Op0.MkArr (homo a) (Fo a) (τ a))) =
                cov_Hom.homa (homo a) (Fo a)  τ a"
            using assms x cov_Hom.UF.map0_def
            apply auto[1]
            using cnt_Hom.y τ.component_in_hom by auto
          ultimately show ?thesis
            using assms x ide_Hom F.preserves_Obj by simp
        qed
        also have "... = Exp (homo x) ((τ a) [homo a, Fo a])"
          using assms(2) x C.cov_Exp_DN τ.component_in_hom F.preserves_Obj
          by simp
        finally show ?thesis by blast
      qed

      text‹
        Here we have the underlying ordinary functor of the enriched contravariant hom,
        expressed in terms of the contravariant endofunctor λf. Exp f (Fo a)› on the base
        category.
      ›
      have 3: "cnt_Hom.map0 (homo x) (Fo x) (τ x) =
               Exp (τ x [homo x, Fo x]) (Fo a)"
      proof -
        have "cnt_Hom.map0 (homo x) (Fo x) (τ x) =
              Uncurry[exp (Fo x) (Fo a), exp (homo x) (Fo a)]
                (cnt_Hom.homa (Fo x) (homo x)  τ x) 
                   𝗅-1[exp (Fo x) (Fo a)]"
        proof -
          have "cnt_Hom.map0 (homo x) (Fo x) (τ x) =
                Uncurry[cnt_Hom.Op0.Dom
                          (cnt_Hom.UF.map0
                             (cnt_Hom.Op0.MkArr (Fo x) (homo x) (τ x))),
                        cnt_Hom.Op0.Cod
                          (cnt_Hom.UF.map0
                             (cnt_Hom.Op0.MkArr (Fo x) (homo x) (τ x)))]
                  (cnt_Hom.Op0.Map
                     (cnt_Hom.UF.map0
                        (cnt_Hom.Op0.MkArr (Fo x) (Hom x x) (τ x)))) 
                     𝗅-1[cnt_Hom.Op0.Dom
                          (cnt_Hom.UF.map0
                             (cnt_Hom.Op0.MkArr (Fo x) (homo x) (τ x)))]"
            using assms x 1 2 cnt_Hom.Kelly_1_32 [of "homo x" "Fo x" "τ x"]
                  C.Curry_simps(1-3) C.DN_def C.UP_DN(2) C.eval_simps(1-3)
                  C.ide_exp Comp_in_hom F.preserves_Obj comp_in_homI'
                  not_arr_null preserves_Obj τ.component_in_hom in_homE
                  mem_Collect_eq seqE
            by (smt (verit))
          moreover have "cnt_Hom.Op0.Dom
                           (cnt_Hom.UF.map0
                              (cnt_Hom.Op0.MkArr (Fo x) (homo x) (τ x))) =
                         exp (Fo x) (Fo a)"
            using assms x cnt_Hom.UF.map0_def
            apply auto[1]
            using F.preserves_Obj cnt_Hom.Op0.arr_MkArr τ.component_in_hom
            by blast
          moreover have "cnt_Hom.Op0.Cod
                           (cnt_Hom.UF.map0
                              (cnt_Hom.Op0.MkArr (Fo x) (homo x) (τ x))) =
                         exp (homo x) (Fo a)"
            using assms x cnt_Hom.UF.map0_def
            apply auto[1]
            using F.preserves_Obj cnt_Hom.Op0.arr_MkArr τ.component_in_hom
            by blast
          moreover have "cnt_Hom.Op0.Map
                           (cnt_Hom.UF.map0
                              (cnt_Hom.Op0.MkArr (Fo x) (homo x) (τ x))) =
                         cnt_Hom.homa (Fo x) (homo x)  τ x"
            using assms x cnt_Hom.UF.map0_def F.preserves_Obj
            by (simp add: τ.component_in_hom)
          ultimately show ?thesis by argo
        qed
        also have "... = Exp (τ x [homo x, Fo x]) (Fo a)"
          using assms(2) x τ.component_in_hom [of x] F.preserves_Obj
                C.DN_def C.cnt_Exp_DN
          by fastforce
        finally show ?thesis by simp
      qed
      show ?thesis
        using 1 2 3 by auto
    qed

    lemma transformation_generated_by_element:
    assumes "enriched_natural_transformation C T α ι
               Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
               homo homa Fo Fa τ"
    and "a  Obj"
    shows "τ a = generated_transformation (generating_elem τ) a"
    proof -
      interpret τ: enriched_natural_transformation C T α ι
                     Obj Hom Id Comp Collect ide exp C.Id C.Comp
                     homo homa Fo Fa τ
        using assms(1) by blast
      have "τ a [homo a, Fo a] =
            τ a [homo a, Fo a] 
              eval  (homo a)  𝗋-1[exp  (homo a)]  C.Exp (Id x) (homo a) 
                Curry[homo a, homo x, homo a] (Comp x x a)"
        using assms(2) x top_path τ.component_in_hom [of a] F.preserves_Obj
              comp_arr_dom C.UP_DN(2)
        by auto
      also have "... =
              (τ a [homo a, Fo a]  eval  (homo a)  𝗋-1[exp  (homo a)]) 
                C.Exp (Id x) (homo a) 
                  Curry[homo a, homo x, homo a] (Comp x x a)"
        using comp_assoc by simp
      also have "... =
              (eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                 C.Exp  (Uncurry[homo a, Fo a] (τ a)  𝗅-1[homo a])) 
                 C.Exp (Id x) (homo a) 
                   Curry[homo a, homo x, homo a] (Comp x x a)"
        using assms right_square C.DN_def τ.component_in_hom comp_assoc
        by auto blast
      also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                (C.Exp  (Uncurry[homo a, Fo a] (τ a)  𝗅-1[homo a]) 
                   C.Exp (Id x) (homo a)) 
                  Curry[homo a, homo x, homo a] (Comp x x a)"
        using comp_assoc by simp
      also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                (C.Exp (Id x) (Fo a) 
                   C.Exp (homo x) (Uncurry[homo a, Fo a] (τ a)  𝗅-1[homo a])) 
                  Curry[homo a, homo x, homo a] (Comp x x a)"
        using assms center_square C.DN_def
              enriched_natural_transformation.component_in_hom
        by fastforce
      also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)]  C.Exp (Id x) (Fo a) 
                C.Exp (homo x) (Uncurry[homo a, Fo a] (τ a)  𝗅-1[homo a]) 
                  Curry[homo a, homo x, homo a] (Comp x x a)"
        using comp_assoc by simp
      also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)]  C.Exp (Id x) (Fo a)  
                Exp (Uncurry[homo x, Fo x] (τ x)  𝗅-1[homo x]) (Fo a)  Fa x a"
      proof -
        have "eval  (Fo a)  𝗋-1[exp  (Fo a)]  C.Exp (Id x) (Fo a) 
                C.Exp (homo x) (Uncurry[homo a, Fo a] (τ a)  𝗅-1[homo a]) 
                  Curry[homo a, homo x, homo a] (Comp x x a) =
              eval  (Fo a)  𝗋-1[exp  (Fo a)]  C.Exp (Id x) (Fo a) 
                C.Exp (homo x) (Uncurry[homo a, Fo a] (τ a)  𝗅-1[homo a]) 
                  homa x a"
          using assms(2) x by force
        also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)]  C.Exp (Id x) (Fo a) 
                Exp (homo x) (Uncurry[homo a, Fo a] (τ a)  𝗅-1[homo a]) 
                  homa x a"
          using assms x C.Exp_def C.cnt_Exp_ide comp_arr_dom by auto
        also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)]  C.Exp (Id x) (Fo a) 
                Exp (homo x) (τ a[homo a, Fo a])  homa x a"
          using assms x C.DN_def by fastforce
        also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)]  C.Exp (Id x) (Fo a) 
                Exp (τ x[homo x, Fo x]) (Fo a)  Fa x a"
          using assms(2) left_square τ.enriched_natural_transformation_axioms
          by fastforce
        also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)]  C.Exp (Id x) (Fo a) 
                Exp (Uncurry[homo x, Fo x] (τ x)  𝗅-1[homo x]) (Fo a)  Fa x a"
          using C.DN_def by fastforce
        finally show ?thesis by blast
      qed
      also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                (C.Exp (Id x) (Fo a) 
                   Exp (Uncurry[homo x, Fo x] (τ x)  𝗅-1[homo x]) (Fo a)) 
                   Fa x a"
        using comp_assoc by simp
      also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                (Exp (Id x) (Fo a) 
                   Exp (Uncurry[homo x, Fo x] (τ x)  𝗅-1[homo x]) (Fo a)) 
                   Fa x a"
        using assms x F.preserves_Obj C.Exp_def C.cov_Exp_ide
                comp_cod_arr [of "Exp (Id x) (dom (Fo a))"]
        by auto
      also have "... =
              eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                Exp ((Uncurry[homo x, Fo x] (τ x)  𝗅-1[homo x])  Id x) (Fo a) 
                  Fa x a"
      proof -
        have "seq (Uncurry[homo x, Fo x] (τ x)  𝗅-1[homo x]) (Id x)"
          using assms x F.preserves_Obj Id_in_hom τ.component_in_hom
          apply (intro seqI)
                apply auto[1]
          by force+
        thus ?thesis
          using assms x F.preserves_Obj C.cnt_Exp_comp by simp
      qed
      also have "... = eval  (Fo a)  𝗋-1[exp  (Fo a)] 
                         Exp (generating_elem τ) (Fo a)  Fa x a"
        using x C.DN_def comp_assoc τ.component_in_hom by fastforce
      also have 1: "... =
                    (generated_transformation (generating_elem τ) a) [homo a, Fo a]"
        using assms x F.preserves_Obj C.UP_DN(4) τ.component_in_hom calculation
              ide_Hom
        by (metis (no_types, lifting) mem_Collect_eq)
      finally have *: "(τ a) [homo a, Fo a] =
                       (generated_transformation (generating_elem τ) a)
                          [homo a, Fo a]"
        by blast
      have "τ a = ((τ a) [homo a, Fo a])"
        using assms x τ.component_in_hom ide_Hom F.preserves_Obj by auto
      also have "... = ((generated_transformation (generating_elem τ) a)
                           [homo a, Fo a])"
        using * by argo
      also have "... = generated_transformation (generating_elem τ) a"
        using assms x 1 ide_Hom by presburger
      finally show "τ a = generated_transformation (generating_elem τ) a" by blast
    qed

    lemma element_of_generated_transformation:
    assumes "e  hom  (Fo x)"
    shows "generating_elem (generated_transformation e) = e"
    proof -
      have "generating_elem (generated_transformation e) =
            Uncurry[homo x, Fo x]
              ((eval  (Fo x)  𝗋-1[exp  (Fo x)] 
                  Curry[exp (Fo x) (Fo x), , Fo x]
                    (eval (Fo x) (Fo x)  (exp (Fo x) (Fo x)  e))  Fa x x)) 
              𝗅-1[homo x]  Id x"
      proof -
        have "arr ((eval  (Fo x) 
                      𝗋-1[exp  (Fo x)] 
                        Curry[exp (Fo x) (Fo x), , Fo x]
                          (eval (Fo x) (Fo x)  (exp (Fo x) (Fo x)  e))  Fa x x))"
          using assms x F.preserves_Hom F.preserves_Obj
          apply (intro C.UP_simps seqI)
                apply auto[1]
          by fastforce+
        thus ?thesis
          using assms x C.DN_def comp_assoc by auto
      qed
      also have "... =
            Uncurry[homo x, Fo x]
              ((eval  (Fo x) 
                  (𝗋-1[exp  (Fo x)] 
                     Curry[exp (Fo x) (Fo x), , Fo x]
                       (eval (Fo x) (Fo x)  (exp (Fo x) (Fo x)  e)))  Fa x x)) 
              𝗅-1[homo x]  Id x"
        using comp_assoc by simp
      also have "... =
            Uncurry[homo x, Fo x]
              ((eval  (Fo x) 
                  ((Curry[exp (Fo x) (Fo x), , Fo x]
                      (eval (Fo x) (Fo x)  (exp (Fo x) (Fo x)  e))  ) 
                     𝗋-1[exp (Fo x) (Fo x)]) 
                    Fa x x)) 
              𝗅-1[homo x]  Id x"
      proof -
        have "«Curry[exp (Fo x) (Fo x), , Fo x]
                 (eval (Fo x) (Fo x)  (exp (Fo x) (Fo x)  e))
                 : exp (Fo x) (Fo x)  exp  (Fo x)»"
          using assms x F.preserves_Obj C.ide_exp
          by (intro C.Curry_in_hom) auto
        thus ?thesis
          using assms
                runit'_naturality
                  [of "Curry[exp (Fo x) (Fo x), , Fo x]
                         (eval (Fo x) (Fo x)  (exp (Fo x) (Fo x)  e))"]
          by force
      qed
      also have "... =
            Uncurry[homo x, Fo x]
              ((Uncurry[, Fo x]
                  (Curry[exp (Fo x) (Fo x), , Fo x]
                     (eval (Fo x) (Fo x)  (exp (Fo x) (Fo x)  e))) 
                  𝗋-1[exp (Fo x) (Fo x)]  Fa x x)) 
              𝗅-1[homo x]  Id x"
        using comp_assoc by simp
      also have "... =
            Uncurry[homo x, Fo x]
              (((eval (Fo x) (Fo x)  (exp (Fo x) (Fo x)  e)) 
                   𝗋-1[exp (Fo x) (Fo x)]  Fa x x)) 
              𝗅-1[homo x]  Id x"
        using assms x F.preserves_Obj C.Uncurry_Curry by auto
      also have "... =
            Uncurry[homo x, Fo x]
              (((eval (Fo x) (Fo x)  (exp (Fo x) (Fo x)  e)) 
                   (Fa x x  )  𝗋-1[homo x])) 
              𝗅-1[homo x]  Id x"
        using assms x runit'_naturality F.preserves_Hom [of x x] by fastforce
      also have "... =
            Uncurry[homo x, Fo x]
              (((eval (Fo x) (Fo x)  (exp (Fo x) (Fo x)  e)  (Fa x x  )) 
                  𝗋-1[homo x])) 
              𝗅-1[homo x]  Id x"
        using comp_assoc by simp
      also have "... =
            Uncurry[homo x, Fo x]
              (((eval (Fo x) (Fo x)  (Fa x x  e))  𝗋-1[homo x])) 
              𝗅-1[homo x]  Id x"
        using assms x F.preserves_Hom [of x x] comp_arr_dom [of e ] comp_cod_arr
             interchange
        by fastforce
      also have "... =
            Uncurry[homo x, Fo x]
              (Curry[, homo x, Fo x]
                 (((eval (Fo x) (Fo x)  (Fa x x  e))  𝗋-1[homo x])  𝗅[homo x])) 
              𝗅-1[homo x]  Id x"
      proof -
        have "seq (eval (Fo x) (Fo x)  (Fa x x  e)) 𝗋-1[Hom x x]"
          using assms x F.preserves_Obj F.preserves_Hom by blast
        thus ?thesis
          using assms x C.UP_def F.preserves_Obj by auto
      qed
      also have "... =
            (((eval (Fo x) (Fo x)  (Fa x x  e))  𝗋-1[Hom x x])  𝗅[Hom x x]) 
              𝗅-1[Hom x x]  Id x"
        using assms x C.Uncurry_Curry F.preserves_Obj F.preserves_Hom by force
      also have "... =
            eval (Fo x) (Fo x)  (Fa x x  e)  𝗋-1[Hom x x] 
              (𝗅[Hom x x]  𝗅-1[Hom x x])  Id x"
        using comp_assoc by simp
      also have "... = eval (Fo x) (Fo x)  (Fa x x  e)  𝗋-1[Hom x x]  Id x"
        using assms x ide_Hom Id_in_hom comp_lunit_lunit'(1) comp_cod_arr
        by fastforce
      also have "... = eval (Fo x) (Fo x)  (Fa x x  e)  (Id x  )  𝗋-1[]"
        using x Id_in_hom runit'_naturality by fastforce
      also have "... = eval (Fo x) (Fo x)  ((Fa x x  e)  (Id x  ))  𝗋-1[]"
        using comp_assoc by simp
      also have "... = eval (Fo x) (Fo x)  (Fa x x  Id x  e)  𝗋-1[]"
        using assms x interchange [of "Fa x x" "Id x" e ] F.preserves_Hom
              comp_arr_dom Id_in_hom
        by fastforce
      also have "... = eval (Fo x) (Fo x)  (C.Id (Fo x)  e)  𝗋-1[]"
        using x F.preserves_Id by auto
      also have "... =
                 eval (Fo x) (Fo x)  ((C.Id (Fo x)  Fo x)  (  e))  𝗋-1[]"
        using assms x interchange C.Id_in_hom F.preserves_Obj comp_arr_dom
              comp_cod_arr
        by (metis in_homE mem_Collect_eq)
      also have "... = Uncurry[Fo x, Fo x] (C.Id (Fo x))  (  e)  𝗋-1[]"
        using comp_assoc by simp
      also have "... = 𝗅[Fo x]  (  e)  𝗋-1[]"
        using x F.preserves_Obj C.Id_def C.Uncurry_Curry by fastforce
      also have "... = 𝗅[Fo x]  (  e)  𝗅-1[]"
        using unitor_coincidence by simp
      also have "... = 𝗅[Fo x]  𝗅-1[Fo x]  e"
        using assms lunit'_naturality by fastforce
      also have "... = (𝗅[Fo x]  𝗅-1[Fo x])  e"
        using comp_assoc by simp
      also have "... = e"
        using assms x comp_lunit_lunit' F.preserves_Obj comp_cod_arr by auto
      finally show "generating_elem (generated_transformation e) = e"
        by blast
    qed

    text‹
      We can now state and prove the (weak) covariant Yoneda lemma (Kelly, Section 1.9)
      for enriched categories.
    ›

    theorem covariant_yoneda:
    shows "bij_betw generated_transformation
             (hom  (Fo x))
             (Collect (enriched_natural_transformation C T α ι
                         Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
                         homo homa Fo Fa))"
    proof (intro bij_betwI)
      show "generated_transformation 
              hom  (Fo x)  Collect
                               (enriched_natural_transformation C T α ι
                                  Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
                                  homo homa Fo Fa)"
        using enriched_natural_transformation_generated_transformation by blast
      show "generating_elem 
              Collect (enriched_natural_transformation C T α ι
                         Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
                         homo homa Fo Fa)
                 hom  (Fo x)"
        using generating_elem_in_hom by blast
      show "e. e  hom  (Fo x) 
                   generating_elem (generated_transformation e) = e"
        using element_of_generated_transformation by blast
      show "τ. τ  Collect (enriched_natural_transformation C T α ι
                               Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
                               homo homa Fo Fa)
                   generated_transformation (generating_elem τ) = τ"
      proof -
        fix τ
        assume τ: "τ  Collect (enriched_natural_transformation C T α ι
                                  Obj Hom Id Comp (Collect ide) exp C.Id C.Comp
                                  homo homa Fo Fa)"
        interpret τ: enriched_natural_transformation C T α ι
                       Obj Hom Id Comp Collect ide exp C.Id C.Comp
                       homo homa Fo Fa τ
          using τ by blast
        show "generated_transformation (generating_elem τ) = τ"
        proof
          fix a
          show "generated_transformation (generating_elem τ) a = τ a"
            using τ transformation_generated_by_element τ.extensionality
                  F.extensionality C.UP_def not_arr_null null_is_zero(2)
            by (cases "a  Obj") auto
        qed
      qed
    qed

  end

  subsection "Contravariant Case"

  text‹
    The (weak) contravariant Yoneda lemma is obtained by just replacing the enriched category
    by its opposite in the covariant version.
  ›

  locale contravariant_yoneda_lemma =
    opposite_enriched_category C T α ι σ Obj Hom Id Comp +
    covariant_yoneda_lemma C T α ι σ exp eval Curry Obj Homop Id Compop y Fo Fa
  for C :: "'a  'a  'a"  (infixr  55)
  and T :: "'a × 'a  'a"
  and α :: "'a × 'a × 'a  'a"
  and ι :: "'a"
  and σ :: "'a × 'a  'a"
  and exp :: "'a  'a  'a"
  and eval :: "'a  'a  'a"
  and Curry :: "'a  'a  'a  'a  'a"
  and Obj :: "'b set"
  and Hom :: "'b  'b  'a"
  and Id :: "'b  'a"
  and Comp :: "'b  'b  'b  'a"
  and y :: 'b
  and Fo :: "'b  'a"
  and Fa :: "'b  'b  'a"
  begin

    corollary contravariant_yoneda:
    shows "bij_betw generated_transformation
             (hom  (Fo y))
             (Collect
                (enriched_natural_transformation
                   C T α ι Obj Homop Id Compop (Collect ide) exp C.Id C.Comp
                   homo homa Fo Fa))"
      using covariant_yoneda by blast

  end

end