Quelle  Coherence.thy

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

section "Coherence"

theory Coherence
imports Bicategory
begin

 text ‹
 \sloppypar
 In this section, we generalize to bicategories the proof of the Coherence Theorem
 that we previously gave for monoidal categories
 (see ‹MonoidalCategory.evaluation_map.coherence› in @{session MonoidalCategory}).
 As was the case for the previous proof, the current proof takes a syntactic approach.
 First we define a formal ``bicategorical language'' of terms constructed using
 syntactic operators that correspond to the various operations (vertical and horizontal
 composition, associators and unitors) found in a bicategory.
 Terms of the language are classified as formal ``arrows'', ``identities'', or ``objects''
 according to the syntactic operators used in their formation.
 A class of terms called ``canonical'' is also defined in this way.
 Functions that map ``arrows'' to their ``domain'' and ``codomain'', and to their
 ``source'' and ``target'' are defined by recursion on the structure of terms.
 Next, we define a notion of ``normal form'' for terms in this language and we
 give a recursive definition of a function that maps terms to their normal forms.
 Normalization moves vertical composition inside of horizontal composition and
 ``flattens'' horizontal composition by associating all horizontal compositions to the right.
 In addition, normalization deletes from a term any horizontal composites involving an arrow
 and its source or target, replacing such composites by just the arrow itself.
 We then define a ``reduction function'' that maps each identity term ‹t› to a
 ``canonical'' term ‹t\↓› that connects ‹t› with its normal form. The definition of reduction
 is also recursive, but it is somewhat more complex than normalization in that it
 involves two mutually recursive functions: one that applies to any identity term
 and another that applies only to terms that are the horizontal composite
 of two identity terms.

 The next step is to define an ``evaluation function'' that evaluates terms in a given
 bicategory (which is left as an unspecified parameter). We show that evaluation respects
 bicategorical structure:
 the domain, codomain, source, and target mappings on terms correspond under evaluation
 to the actual domain, codomain, source and target mappings on the given bicategory,
 the vertical and horizontal composition on terms correspond to the actual vertical
 and horizontal composition of the bicategory, and unit and associativity terms evaluate
 to the actual unit and associativity isomorphisms of the bicategory.
 In addition, ``object terms'' evaluate to objects (\emph{i.e.}~0-cells),
 ``identity terms'' evaluate to identities (\emph{i.e.}~1-cells),
 ``arrow terms'' evaluate to arrows (\emph{i.e.}~2-cells), and ``canonical terms'' evaluate
 to canonical isomorphisms.
 A term is defined to be ``coherent'' if, roughly speaking, it is a formal arrow
 whose evaluation commutes with the evaluations of the reductions to normal form of
 its domain and codomain.
 We then prove the Coherence Theorem, expressed in the form: ``every arrow is coherent.''
 This implies a more classical version of the Coherence Theorem, which says that:
 ``syntactically parallel arrows with the same normal form have equal evaluations''.
 ›

  subsection "Bicategorical Language"

    text ‹
 For the most part, the definition of the ``bicategorical language'' of terms is
 a straightforward generalization of the ``monoidal language'' that we used for
 monoidal categories.
 Some modifications are required, however, due to the fact that horizontal composition
 in a bicategory is a partial operation, whereas the the tensor product in a monoidal
 category is well-defined for all pairs of arrows.
 One difference is that we have found it necessary to introduce a new class of primitive
 terms whose elements represent ``formal objects'', so that there is some way to
 identify the source and target of what would otherwise be an empty horizontal composite.
 This was not an issue for monoidal categories, because the totality of horizontal
 composition meant that there was no need for syntactically defined sources and targets.
 Another difference is what we have chosen for the ``generators'' of the language
 and how they are used to form primitive terms. For monoidal categories,
 we supposed that we were given a category ‹C› and the syntax contained a constructor
 to form a primitive term corresponding to each arrow of ‹C›.
 We assumed a category as the given data, rather than something less structured,
 such as a graph, because we were primarily interested in the tensor product and
 the associators and unitors, and were relatively uninterested in the strictly
 associative and unital composition of the underlying category.
 For bicategories, we also take the vertical composition as given for the same
 reasons; however, this is not yet sufficient due to the fact that horizontal
 composition in a bicategory is a partial operation, in contrast to the tensor
 product in a monoidal category, which is defined for all pairs of arrows.
 To deal with this issue, for bicategories we assume that source and target
 mappings are also given, so that the given data forms a category with
 ``horizontal homs''. The given source and target mappings are extended to all terms
 and used to define when two terms are ``formally horizontally composable''.
 ›

  locale bicategorical_language =
    category V +
    horizontal_homs V src trg
    for V :: "'a comp"                       (infixr ‹⋅› 55)
    and src :: "'a ==> 'a"
    and trg :: "'a ==> 'a"
  begin

    text ‹
 Constructor ‹Prim₀› is used to construct ``formal objects'' and ‹Prim› is used to
 construct primitive terms that are not formal objects.
 ›

    datatype (discs_sels) 't "term" =
      Prim₀ 't                             (‹\⟨_\⟩₀›)
    | Prim 't                              (‹\⟨_\⟩›)
    | Hcomp "'t term" "'t term"            (infixr ‹\⋆› 53)
    | Vcomp "'t term" "'t term"            (infixr ‹\⋅› 55)
    | Lunit "'t term"                      (‹\l[_]›)
    | Lunit' "'t term"                     (‹\l^-1[_]›)
    | Runit "'t term"                      (‹\r[_]›)
    | Runit' "'t term"                     (‹\r^-1[_]›)
    | Assoc "'t term" "'t term" "'t term"  (‹\a[_, _, _]›)
    | Assoc' "'t term" "'t term" "'t term" (‹\a^-1[_, _, _]›)

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

    primrec Src :: "'a term ==> 'a term"
    where "Src \<langle>μ\<rangle>₀ = \<langle>μ\<rangle>₀"
        | "Src \<langle>μ\<rangle> = \<langle>src μ\<rangle>₀"
        | "Src (t \<star> u) = Src u"
        | "Src (t \<cdot> u) = Src t"
        | "Src \<l>[t] = Src t"
        | "Src \<l>^-1[t] = Src t"
        | "Src \<r>[t] = Src t"
        | "Src \<r>^-1[t] = Src t"
        | "Src \<a>[t, u, v] = Src v"
        | "Src \<a>^-1[t, u, v] = Src v"

    primrec Trg :: "'a term ==> 'a term"
    where "Trg \<langle>μ\<rangle>₀ = \<langle>μ\<rangle>₀"
        | "Trg \<langle>μ\<rangle> = \<langle>trg μ\<rangle>₀"
        | "Trg (t \<star> u) = Trg t"
        | "Trg (t \<cdot> u) = Trg t"
        | "Trg \<l>[t] = Trg t"
        | "Trg \<l>^-1[t] = Trg t"
        | "Trg \<r>[t] = Trg t"
        | "Trg \<r>^-1[t] = Trg t"
        | "Trg \<a>[t, u, v] = Trg t"
        | "Trg \<a>^-1[t, u, v] = Trg t"

    primrec Dom :: "'a term ==> 'a term"
    where "Dom \<langle>μ\<rangle>₀ = \<langle>μ\<rangle>₀"
        | "Dom \<langle>μ\<rangle> = \<langle>dom μ\<rangle>"
        | "Dom (t \<star> u) = Dom t \<star> Dom u"
        | "Dom (t \<cdot> u) = Dom u"
        | "Dom \<l>[t] = Trg t \<star> Dom t"
        | "Dom \<l>^-1[t] = Dom t"
        | "Dom \<r>[t] = Dom t \<star> Src t"
        | "Dom \<r>^-1[t] = Dom t"
        | "Dom \<a>[t, u, v] = (Dom t \<star> Dom u) \<star> Dom v"
        | "Dom \<a>^-1[t, u, v] = Dom t \<star> (Dom u \<star> Dom v)"

    primrec Cod :: "'a term ==> 'a term"
    where "Cod \<langle>μ\<rangle>₀ = \<langle>μ\<rangle>₀"
        | "Cod \<langle>μ\<rangle> = \<langle>cod μ\<rangle>"
        | "Cod (t \<star> u) = Cod t \<star> Cod u"
        | "Cod (t \<cdot> u) = Cod t"
        | "Cod \<l>[t] = Cod t"
        | "Cod \<l>^-1[t] = Trg t \<star> Cod t"
        | "Cod \<r>[t] = Cod t"
        | "Cod \<r>^-1[t] = Cod t \<star> Src t"
        | "Cod \<a>[t, u, v] = Cod t \<star> (Cod u \<star> Cod v)"
        | "Cod \<a>^-1[t, u, v] = (Cod t \<star> Cod u) \<star> Cod v"

    text ‹
 A term is a ``formal arrow'' if it is constructed from primitive arrows in such a way
 that horizontal and vertical composition are applied only to formally composable pairs
 of terms. The definitions of ``formal identity'' and ``formal object'' follow a
 similar pattern.
 ›

    primrec Arr :: "'a term ==> bool"
    where "Arr \<langle>μ\<rangle>₀ = obj μ"
        | "Arr \<langle>μ\<rangle> = arr μ"
        | "Arr (t \<star> u) = (Arr t ∧ Arr u ∧ Src t = Trg u)"
        | "Arr (t \<cdot> u) = (Arr t ∧ Arr u ∧ Dom t = Cod u)"
        | "Arr \<l>[t] = Arr t"
        | "Arr \<l>^-1[t] = Arr t"
        | "Arr \<r>[t] = Arr t"
        | "Arr \<r>^-1[t] = Arr t"
        | "Arr \<a>[t, u, v] = (Arr t ∧ Arr u ∧ Arr v ∧ Src t = Trg u ∧ Src u = Trg v)"
        | "Arr \<a>^-1[t, u, v] = (Arr t ∧ Arr u ∧ Arr v ∧ Src t = Trg u ∧ Src u = Trg v)"

    primrec Ide :: "'a term ==> bool"
    where "Ide \<langle>μ\<rangle>₀ = obj μ"
        | "Ide \<langle>μ\<rangle> = ide μ"
        | "Ide (t \<star> u) = (Ide t ∧ Ide u ∧ Src t = Trg u)"
        | "Ide (t \<cdot> u) = False"
        | "Ide \<l>[t] = False"
        | "Ide \<l>^-1[t] = False"
        | "Ide \<r>[t] = False"
        | "Ide \<r>^-1[t] = False"
        | "Ide \<a>[t, u, v] = False"
        | "Ide \<a>^-1[t, u, v] = False"

    primrec Obj :: "'a term ==> bool"
    where "Obj \<langle>μ\<rangle>₀ = obj μ"
        | "Obj \<langle>μ\<rangle> = False"
        | "Obj (t \<star> u) = False"
        | "Obj (t \<cdot> u) = False"
        | "Obj \<l>[t] = False"
        | "Obj \<l>^-1[t] = False"
        | "Obj \<r>[t] = False"
        | "Obj \<r>^-1[t] = False"
        | "Obj \<a>[t, u, v] = False"
        | "Obj \<a>^-1[t, u, v] = False"

    abbreviation HSeq :: "'a term ==> 'a term ==> bool"
    where "HSeq t u ≡ Arr t ∧ Arr u ∧ Src t = Trg u"

    abbreviation VSeq :: "'a term ==> 'a term ==> bool"
    where "VSeq t u ≡ Arr t ∧ Arr u ∧ Dom t = Cod u"

    abbreviation HPar :: "'a term => 'a term ==> bool"
    where "HPar t u ≡ Arr t ∧ Arr u ∧ Src t = Src u ∧ Trg t = Trg u"

    abbreviation VPar :: "'a term => 'a term ==> bool"
    where "VPar t u ≡ Arr t ∧ Arr u ∧ Dom t = Dom u ∧ Cod t = Cod u"

    abbreviation HHom :: "'a term ==> 'a term ==> 'a term set"
    where "HHom a b ≡ { t. Arr t ∧ Src t = a ∧ Trg t = b }"

    abbreviation VHom :: "'a term ==> 'a term ==> 'a term set"
    where "VHom f g ≡ { t. Arr t ∧ Dom t = f ∧ Cod t = g }"

    lemma is_Prim0_Src:
    shows "is_Prim₀ (Src t)"
      by (induct t; simp)

    lemma is_Prim0_Trg:
    shows "is_Prim₀ (Trg t)"
      by (induct t; simp)

    lemma Src_Src [simp]:
    shows "Arr t ==> Src (Src t) = Src t"
      by (induct t) auto

    lemma Trg_Trg [simp]:
    shows "Arr t ==> Trg (Trg t) = Trg t"
      by (induct t) auto

    lemma Src_Trg [simp]:
    shows "Arr t ==> Src (Trg t) = Trg t"
      by (induct t) auto

    lemma Trg_Src [simp]:
    shows "Arr t ==> Trg (Src t) = Src t"
      by (induct t) auto

    lemma Dom_Src [simp]:
    shows "Arr t ==> Dom (Src t) = Src t"
      by (induct t) auto

    lemma Dom_Trg [simp]:
    shows "Arr t ==> Dom (Trg t) = Trg t"
      by (induct t) auto

    lemma Cod_Src [simp]:
    shows "Arr t ==> Cod (Src t) = Src t"
      by (induct t) auto

    lemma Cod_Trg [simp]:
    shows "Arr t ==> Cod (Trg t) = Trg t"
      by (induct t) auto

    lemma Src_Dom_Cod:
    shows "Arr t ==> Src (Dom t) = Src t ∧ Src (Cod t) = Src t"
       using src_dom src_cod by (induct t) auto

    lemma Src_Dom [simp]:
    shows "Arr t ==> Src (Dom t) = Src t"
      using Src_Dom_Cod by blast

    lemma Src_Cod [simp]:
    shows "Arr t ==> Src (Cod t) = Src t"
      using Src_Dom_Cod by blast

    lemma Trg_Dom_Cod:
    shows "Arr t ==> Trg (Dom t) = Trg t ∧ Trg (Cod t) = Trg t"
       using trg_dom trg_cod by (induct t) auto

    lemma Trg_Dom [simp]:
    shows "Arr t ==> Trg (Dom t) = Trg t"
      using Trg_Dom_Cod by blast

    lemma Trg_Cod [simp]:
    shows "Arr t ==> Trg (Cod t) = Trg t"
      using Trg_Dom_Cod by blast

    lemma VSeq_implies_HPar:
    shows "VSeq t u ==> HPar t u"
      using Src_Dom [of t] Src_Cod [of u] Trg_Dom [of t] Trg_Cod [of u] by auto

    lemma Dom_Dom [simp]:
    shows "Arr t ==> Dom (Dom t) = Dom t"
      by (induct t, auto)

    lemma Cod_Cod [simp]:
    shows "Arr t ==> Cod (Cod t) = Cod t"
      by (induct t, auto)

    lemma Dom_Cod [simp]:
    shows "Arr t ==> Dom (Cod t) = Cod t"
      by (induct t, auto)

    lemma Cod_Dom [simp]:
    shows "Arr t ==> Cod (Dom t) = Dom t"
      by (induct t, auto)
      
    lemma Obj_implies_Ide (*[simp]*):
    shows "Obj t ==> Ide t"
      by (induct t) auto

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

    lemma Dom_Ide:
    shows "Ide t ==> Dom t = t"
      by (induct t, auto)

    lemma Cod_Ide:
    shows "Ide t ==> Cod t = t"
      by (induct t, auto)

    lemma Obj_Src [simp]:
    shows "Arr t ==> Obj (Src t)"
      by (induct t) auto

    lemma Obj_Trg [simp]:
    shows "Arr t ==> Obj (Trg t)"
      by (induct t) auto

    lemma Ide_Dom [simp]:
    shows "Arr t ==> Ide (Dom t)"
      using Obj_implies_Ide
      by (induct t, auto)

    lemma Ide_Cod [simp]:
    shows "Arr t ==> Ide (Cod t)"
      using Obj_implies_Ide
      by (induct t, auto)

    lemma Arr_in_Hom:
    assumes "Arr t"
    shows "t ∈ HHom (Src t) (Trg t)" and "t ∈ VHom (Dom t) (Cod t)"
    proof -
      have 1: "Arr t ==> t ∈ HHom (Src t) (Trg t) ∧ t ∈ VHom (Dom t) (Cod t)"
        by (induct t, auto)
      show "t ∈ HHom (Src t) (Trg t)" using assms 1 by simp
      show "t ∈ VHom (Dom t) (Cod t)" using assms 1 by simp
    qed

    lemma Ide_in_Hom:
    assumes "Ide t"
    shows "t ∈ HHom (Src t) (Trg t)" and "t ∈ VHom t t"
    proof -
      have 1: "Ide t ==> t ∈ HHom (Src t) (Trg t) ∧ t ∈ VHom t t"
        by (induct t, auto)
      show "t ∈ HHom (Src t) (Trg t)" using assms 1 by simp
      show "t ∈ VHom t t" using assms 1 by simp
    qed

    lemma Obj_in_Hom:
    assumes "Obj t"
    shows "t ∈ HHom t t" and "t ∈ VHom t t"
    proof -
      have 1: "Obj t ==> t ∈ HHom t t ∧ t ∈ VHom t t"
        by (induct t, auto)
      show "t ∈ HHom t t" using assms 1 by simp
      show "t ∈ VHom t t" using assms 1 by simp
    qed

    text ‹
 A formal arrow is ``canonical'' if the only primitive arrows used in its construction
 are objects and identities.
 ›

    primrec Can :: "'a term ==> bool"
    where "Can \<langle>μ\<rangle>₀ = obj μ"
        | "Can \<langle>μ\<rangle> = ide μ"
        | "Can (t \<star> u) = (Can t ∧ Can u ∧ Src t = Trg u)"
        | "Can (t \<cdot> u) = (Can t ∧ Can u ∧ Dom t = Cod u)"
        | "Can \<l>[t] = Can t"
        | "Can \<l>^-1[t] = Can t"
        | "Can \<r>[t] = Can t"
        | "Can \<r>^-1[t] = Can t"
        | "Can \<a>[t, u, v] = (Can t ∧ Can u ∧ Can v ∧ Src t = Trg u ∧ Src u = Trg v)"
        | "Can \<a>^-1[t, u, v] = (Can t ∧ Can u ∧ Can v ∧ Src t = Trg u ∧ Src u = Trg v)"

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

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

    text ‹
 Canonical arrows can be formally inverted.
 ›

    primrec Inv :: "'a term ==> 'a term"
    where "Inv \<langle>μ\<rangle>₀ = \<langle>μ\<rangle>₀"
        | "Inv \<langle>μ\<rangle> = \<langle>inv μ\<rangle>"
        | "Inv (t \<star> u) = (Inv t \<star> Inv u)"
        | "Inv (t \<cdot> u) = (Inv u \<cdot> Inv t)"
        | "Inv \<l>[t] = \<l>^-1[Inv t]"
        | "Inv \<l>^-1[t] = \<l>[Inv t]"
        | "Inv \<r>[t] = \<r>^-1[Inv t]"
        | "Inv \<r>^-1[t] = \<r>[Inv t]"
        | "Inv \<a>[t, u, v] = \<a>^-1[Inv t, Inv u, Inv v]"
        | "Inv \<a>^-1[t, u, v] = \<a>[Inv t, Inv u, Inv v]"

    lemma Src_Inv [simp]:
    shows "Can t ==> Src (Inv t) = Src t"
      using Can_implies_Arr VSeq_implies_HPar
      apply (induct t, auto)
      by metis

    lemma Trg_Inv [simp]:
    shows "Can t ==> Trg (Inv t) = Trg t"
      using Can_implies_Arr VSeq_implies_HPar 
      apply (induct t, auto)
      by metis

    lemma Dom_Inv [simp]:
    shows "Can t ==> Dom (Inv t) = Cod t"
      by (induct t, auto)

    lemma Cod_Inv [simp]:
    shows "Can t ==> Cod (Inv t) = Dom t"
      by (induct t, auto)

    lemma Inv_preserves_Ide:
    shows "Ide t ==> Ide (Inv t)"
      using Ide_implies_Can by (induct t, auto)

    lemma Can_Inv [simp]:
    shows "Can t ==> Can (Inv t)"
      by (induct t, auto)

    lemma Inv_in_Hom [intro]:
    assumes "Can t"
    shows "Inv t ∈ HHom (Src t) (Trg t)" and "Inv t ∈ VHom (Cod t) (Dom t)"
      using assms Can_Inv Can_implies_Arr by simp_all

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

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

    subsection "Normal Terms"

    text ‹
 We call a term ``normal'' if it is either a formal object or it is constructed from
 primitive arrows using only horizontal composition associated to the right.
 Essentially, such terms are (typed) composable sequences of arrows of @{term V},
 where the empty list is represented by a formal object and ‹\⋆› is used as
 the list constructor.
 ›

    fun Nml :: "'a term ==> bool"
    where "Nml \<langle>μ\<rangle>₀ = obj μ"
        | "Nml \<langle>μ\<rangle> = arr μ"
        | "Nml (\<langle>ν\<rangle> \<star> u) = (arr ν ∧ Nml u ∧ ¬ is_Prim₀ u ∧ \<langle>src ν\<rangle>₀ = Trg u)"
        | "Nml _ = False"

    lemma Nml_HcompD:
    assumes "Nml (t \<star> u)"
    shows "\<langle>un_Prim t\<rangle> = t" and "arr (un_Prim t)" and "Nml t" and "Nml u"
    and "¬ is_Prim₀ u" and "\<langle>src (un_Prim t)\<rangle>₀ = Trg u" and "Src t = Trg u"
    proof -
      have 1: "t = \<langle>un_Prim t\<rangle> ∧ arr (un_Prim t) ∧ Nml t ∧ Nml u ∧ ¬ is_Prim₀ u ∧
               \<langle>src (un_Prim t)\<rangle>₀ = Trg u"
        using assms by (cases t; simp; cases u; simp)
      show "\<langle>un_Prim t\<rangle> = t" using 1 by simp
      show "arr (un_Prim t)" using 1 by simp
      show "Nml t" using 1 by simp
      show "Nml u" using 1 by simp
      show "¬ is_Prim₀ u" using 1 by simp
      show "\<langle>src (un_Prim t)\<rangle>₀ = Trg u" using 1 by simp
      show "Src t = Trg u"
        using assms
        apply (cases t) by simp_all
    qed

    lemma Nml_implies_Arr:
    shows "Nml t ==> Arr t"
      by (induct t, auto simp add: Nml_HcompD)

    lemma Nml_Src [simp]:
    shows "Nml t ==> Nml (Src t)"
      apply (induct t, simp_all)
      using Nml_HcompD by metis

    lemma Nml_Trg [simp]:
    shows "Nml t ==> Nml (Trg t)"
      apply (induct t, simp_all)
      using Nml_HcompD by metis

    lemma Nml_Dom [simp]:
    shows "Nml t ==> Nml (Dom t)"
    proof (induct t, simp_all add: Nml_HcompD)
      fix u v
      assume I1: "Nml (Dom u)"
      assume I2: "Nml (Dom v)"
      assume uv: "Nml (u \<star> v)"
      show "Nml (Dom u \<star> Dom v)"
      proof -
        have 1: "is_Prim (Dom u) ∧ arr (un_Prim (Dom u)) ∧ Dom u = \<langle>dom (un_Prim u)\<rangle>"
          using uv by (cases u; simp; cases v, simp_all)
        have 2: "Nml v ∧ ¬ is_Prim₀ v ∧ ¬ is_Vcomp v ∧ ¬ is_Lunit' v ∧ ¬ is_Runit' v"
          using uv by (cases u, simp_all; cases v, simp_all)
        have "arr (dom (un_Prim u))"
          using 1 by fastforce
        moreover have "Nml (Dom v) ∧ ¬ is_Prim₀ v"
          using 2 I2 by (cases v, simp_all)
        moreover have "\<langle>src (dom (un_Prim u))\<rangle>₀ = Trg (Dom v)"
        proof -
          have "Trg (Dom v) = Src (Dom u)"
            using uv Nml_implies_Arr by fastforce
          also have "... = \<langle>src (dom (un_Prim u))\<rangle>₀"
            using 1 by fastforce
          finally show ?thesis by argo
        qed
        moreover have "¬ is_Prim₀ (Dom v)"
          using 2 by (cases v, simp_all)
        ultimately show ?thesis using 1 2 by simp
      qed
    qed
    
    lemma Nml_Cod [simp]:
    shows "Nml t ==> Nml (Cod t)"
    proof (induct t, simp_all add: Nml_HcompD)
      fix u v
      assume I1: "Nml (Cod u)"
      assume I2: "Nml (Cod v)"
      assume uv: "Nml (u \<star> v)"
      show "Nml (Cod u \<star> Cod v)"
      proof -
        have 1: "is_Prim (Cod u) ∧ arr (un_Prim (Cod u)) ∧ Cod u = \<langle>cod (un_Prim u)\<rangle>"
          using uv by (cases u; simp; cases v, simp_all)
        have 2: "Nml v ∧ ¬ is_Prim₀ v ∧ ¬ is_Vcomp v ∧ ¬ is_Lunit' v ∧ ¬ is_Runit' v"
          using uv by (cases u; simp; cases v, simp_all)
        have "arr (cod (un_Prim u))"
          using 1 by fastforce
        moreover have "Nml (Cod v) ∧ ¬ is_Prim₀ v"
          using 2 I2 by (cases v, simp_all)
        moreover have "\<langle>src (cod (un_Prim u))\<rangle>₀ = Trg (Cod v)"
        proof -
          have "Trg (Cod v) = Src (Cod u)"
            using uv Nml_implies_Arr by fastforce
          also have "... = \<langle>src (cod (un_Prim u))\<rangle>₀"
            using 1 by fastforce
          finally show ?thesis by argo
        qed
        moreover have "¬ is_Prim₀ (Cod v)"
          using 2 by (cases v; simp)
        ultimately show ?thesis using 1 2 by simp
      qed
    qed
    
    lemma Nml_Inv [simp]:
    assumes "Can t" and "Nml t"
    shows "Nml (Inv t)"
    proof -
      have "Can t ∧ Nml t ==> Nml (Inv t)"
        apply (induct t, simp_all)
      proof -
        fix u v
        assume I1: "Nml u ==> Nml (Inv u)"
        assume I2: "Nml v ==> Nml (Inv v)"
        assume uv: "Can u ∧ Can v ∧ Src u = Trg v ∧ Nml (u \<star> v)"
        show "Nml (Inv u \<star> Inv v)"
        proof -
          have u: "Arr u ∧ Can u" using uv Can_implies_Arr by blast
          have v: "Arr v ∧ Can v" using uv Can_implies_Arr by blast
          have 1: "\<langle>un_Prim u\<rangle> = u ∧ ide (un_Prim u) ∧ Nml u ∧ Nml v ∧ ¬ is_Prim₀ v ∧
                   \<langle>src (un_Prim u)\<rangle>₀ = Trg v"
            using uv Nml_HcompD [of u v] apply simp
            using uv by (cases u, simp_all)
          have 2: "\<langle>un_Prim (Inv u)\<rangle> = Inv u ∧ arr (un_Prim (Inv u)) ∧ Nml (Inv u)"
            using 1 by (cases u; simp)
          moreover have "Nml (Inv v) ∧ ¬ is_Prim₀ (Inv v)"
            using 1 I2 by (cases v, simp_all)
          moreover have "\<langle>src (un_Prim (Inv u))\<rangle>₀ = Trg (Inv v)"
            using 1 2 v by (cases u, simp_all)
          ultimately show ?thesis
            by (cases u, simp_all)
        qed
      qed
      thus ?thesis using assms by blast
    qed

    text ‹
 The following function defines a horizontal composition for normal terms.
 If such terms are regarded as lists, this is just (typed) list concatenation.
 ›

    fun HcompNml  (infixr ‹\⌊\⋆\⌋› 53)
    where "\<langle>ν\<rangle>₀ \<lfloor>\<star>\<rfloor> u = u"
        | "t \<lfloor>\<star>\<rfloor> \<langle>μ\<rangle>₀ = t"
        | "\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u = \<langle>ν\<rangle> \<star> u"
        | "(t \<star> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)"
        | "t \<lfloor>\<star>\<rfloor> u = undefined"

    lemma HcompNml_Prim [simp]:
    assumes "¬ is_Prim₀ t"
    shows "\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> t = \<langle>ν\<rangle> \<star> t"
      using assms by (cases t, simp_all)

    lemma HcompNml_term_Prim₀ [simp]:
    assumes "Src t = Trg \<langle>μ\<rangle>₀"
    shows "t \<lfloor>\<star>\<rfloor> \<langle>μ\<rangle>₀ = t"
      using assms by (cases t, simp_all)

    lemma HcompNml_Nml:
    assumes "Nml (t \<star> u)"
    shows "t \<lfloor>\<star>\<rfloor> u = t \<star> u"
      using assms HcompNml_Prim by (metis Nml_HcompD(1) Nml_HcompD(5))

    lemma Nml_HcompNml:
    assumes "Nml t" and "Nml u" and "Src t = Trg u"
    shows "Nml (t \<lfloor>\<star>\<rfloor> u)"
    and "Dom (t \<lfloor>\<star>\<rfloor> u) = Dom t \<lfloor>\<star>\<rfloor> Dom u"
    and "Cod (t \<lfloor>\<star>\<rfloor> u) = Cod t \<lfloor>\<star>\<rfloor> Cod u"
    and "Src (t \<lfloor>\<star>\<rfloor> u) = Src u"
    and "Trg (t \<lfloor>\<star>\<rfloor> u) = Trg t"
    proof -
      have 0: "∧u. [ Nml t; Nml u; Src t = Trg u ] ==>
                     Nml (t \<lfloor>\<star>\<rfloor> u) ∧ Dom (t \<lfloor>\<star>\<rfloor> u) = Dom t \<lfloor>\<star>\<rfloor> Dom u ∧
                                      Cod (t \<lfloor>\<star>\<rfloor> u) = Cod t \<lfloor>\<star>\<rfloor> Cod u ∧
                                      Src (t \<lfloor>\<star>\<rfloor> u) = Src u ∧ Trg (t \<lfloor>\<star>\<rfloor> u) = Trg t"
      proof (induct t, simp_all add: Nml_HcompD(1-4))
        fix ν :: 'a and u :: "'a term"
        assume ν: "arr ν"
        assume u: "Nml u"
        assume 1: "\<langle>src ν\<rangle>₀ = Trg u"
        show "Nml (\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u) ∧ Dom (\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u) = \<langle>dom ν\<rangle> \<lfloor>\<star>\<rfloor> Dom u ∧
                                 Cod (\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u) = \<langle>cod ν\<rangle> \<lfloor>\<star>\<rfloor> Cod u ∧
                                 Src (\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u) = Src u ∧ Trg (\<langle>ν\<rangle> \<lfloor>\<star>\<rfloor> u) = \<langle>trg ν\<rangle>₀"
          using u ν 1 by (cases u, simp_all)
        next
        fix u v w
        assume I1: "∧x. Nml x ==> Src v = Trg x ==>
                         Nml (v \<lfloor>\<star>\<rfloor> x) ∧ Dom (v \<lfloor>\<star>\<rfloor> x) = Dom v \<lfloor>\<star>\<rfloor> Dom x ∧
                                          Cod (v \<lfloor>\<star>\<rfloor> x) = Cod v \<lfloor>\<star>\<rfloor> Cod x ∧
                                          Src (v \<lfloor>\<star>\<rfloor> x) = Src x ∧ Trg (v \<lfloor>\<star>\<rfloor> x) = Trg v"
        assume I2: "∧x. Nml x ==> Trg u = Trg x ==>
                         Nml (w \<lfloor>\<star>\<rfloor> x) ∧ Dom (w \<lfloor>\<star>\<rfloor> x) = Dom w \<lfloor>\<star>\<rfloor> Dom x ∧
                                          Cod (w \<lfloor>\<star>\<rfloor> x) = Cod w \<lfloor>\<star>\<rfloor> Cod x ∧
                                          Src (w \<lfloor>\<star>\<rfloor> x) = Src x ∧ Trg (w \<lfloor>\<star>\<rfloor> x) = Trg w"
        assume vw: "Nml (v \<star> w)"
        assume u: "Nml u"
        assume wu: "Src w = Trg u"
        show "Nml ((v \<star> w) \<lfloor>\<star>\<rfloor> u) ∧
              Dom ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = (Dom v \<star> Dom w) \<lfloor>\<star>\<rfloor> Dom u ∧
              Cod ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = (Cod v \<star> Cod w) \<lfloor>\<star>\<rfloor> Cod u ∧
              Src ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = Src u ∧ Trg ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = Trg v"
        proof -
          have v: "v = \<langle>un_Prim v\<rangle> ∧ Nml v"
            using vw Nml_implies_Arr Nml_HcompD by metis
          have w: "Nml w ∧ ¬ is_Prim₀ w ∧ \<langle>src (un_Prim v)\<rangle>₀ = Trg w"
            using vw by (simp add: Nml_HcompD)
          have "is_Prim₀ u ==> ?thesis" by (cases u; simp add: vw wu)
          moreover have "¬ is_Prim₀ u ==> ?thesis"
          proof -
            assume 1: "¬ is_Prim₀ u"
            have "Src v = Trg (w \<lfloor>\<star>\<rfloor> u)"
              using u v w I2 [of u] by (cases v, simp_all)
            hence "Nml (v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u) ∧
                   Dom (v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u) = Dom v \<lfloor>\<star>\<rfloor> Dom (w \<lfloor>\<star>\<rfloor> u) ∧
                   Cod (v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u) = Cod v \<lfloor>\<star>\<rfloor> Cod (w \<lfloor>\<star>\<rfloor> u) ∧
                   Src (v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u) = Src u ∧ Trg (v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u) = Trg v"
              using u v w I1 [of "w \<lfloor>\<star>\<rfloor> u"] I2 [of u] by argo
            moreover have "v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u = (v \<star> w) \<lfloor>\<star>\<rfloor> u"
              using 1 by (cases u, simp_all)
            moreover have "(Dom v \<star> Dom w) \<lfloor>\<star>\<rfloor> Dom u = Dom v \<lfloor>\<star>\<rfloor> Dom (w \<lfloor>\<star>\<rfloor> u)"
              using v w u vw 1 I2 Nml_Dom HcompNml_Prim Nml_HcompD(1) Nml_HcompD(5)
              by (cases u, simp_all)
            moreover have "(Cod v \<star> Cod w) \<lfloor>\<star>\<rfloor> Cod u = Cod v \<lfloor>\<star>\<rfloor> Cod (w \<lfloor>\<star>\<rfloor> u)"
              using v w u vw 1 I2 Nml_HcompD(1) Nml_HcompD(5) HcompNml_Prim
              by (cases u, simp_all)
            ultimately show ?thesis
              by argo
          qed
          ultimately show ?thesis by blast
        qed
        next
        fix a u
        assume a: "obj a"
        assume u: "Nml u"
        assume au: "\<langle>a\<rangle>₀ = Trg u"
        show "Nml (Trg u \<lfloor>\<star>\<rfloor> u) ∧
              Dom (Trg u \<lfloor>\<star>\<rfloor> u) = Dom (Trg u) \<lfloor>\<star>\<rfloor> Dom u ∧
              Cod (Trg u \<lfloor>\<star>\<rfloor> u) = Cod (Trg u) \<lfloor>\<star>\<rfloor> Cod u ∧
              Src (Trg u \<lfloor>\<star>\<rfloor> u) = Src u ∧ Trg (Trg u \<lfloor>\<star>\<rfloor> u) = Trg (Trg u)"
          using au
          by (metis Cod.simps(1) Dom.simps(1) HcompNml.simps(1) Trg.simps(1) u)
      qed
      show "Nml (t \<lfloor>\<star>\<rfloor> u) " using assms 0 by blast
      show "Dom (t \<lfloor>\<star>\<rfloor> u) = Dom t \<lfloor>\<star>\<rfloor> Dom u" using assms 0 by blast
      show "Cod (t \<lfloor>\<star>\<rfloor> u) = Cod t \<lfloor>\<star>\<rfloor> Cod u" using assms 0 by blast
      show "Src (t \<lfloor>\<star>\<rfloor> u) = Src u" using assms 0 by blast
      show "Trg (t \<lfloor>\<star>\<rfloor> u) = Trg t" using assms 0 by blast
    qed

    lemma HcompNml_in_Hom [intro]:
    assumes "Nml t" and "Nml u" and "Src t = Trg u"
    shows "t \<lfloor>\<star>\<rfloor> u ∈ HHom (Src u) (Trg t)"
    and "t \<lfloor>\<star>\<rfloor> u ∈ VHom (Dom t \<lfloor>\<star>\<rfloor> Dom u) (Cod t \<lfloor>\<star>\<rfloor> Cod u)"
      using assms Nml_HcompNml Nml_implies_Arr by auto

    lemma Src_HcompNml:
    assumes "Nml t" and "Nml u" and "Src t = Trg u"
    shows "Src (t \<lfloor>\<star>\<rfloor> u) = Src u"
      using assms Nml_HcompNml(4) by simp

    lemma Trg_HcompNml:
    assumes "Nml t" and "Nml u" and "Src t = Trg u"
    shows "Trg (t \<lfloor>\<star>\<rfloor> u) = Trg t"
      using assms Nml_HcompNml(5) by simp

    lemma Dom_HcompNml:
    assumes "Nml t" and "Nml u" and "Src t = Trg u"
    shows "Dom (t \<lfloor>\<star>\<rfloor> u) = Dom t \<lfloor>\<star>\<rfloor> Dom u"
      using assms Nml_HcompNml(2) by simp

    lemma Cod_HcompNml:
    assumes "Nml t" and "Nml u" and "Src t = Trg u"
    shows "Cod (t \<lfloor>\<star>\<rfloor> u) = Cod t \<lfloor>\<star>\<rfloor> Cod u"
      using assms Nml_HcompNml(3) by simp

    lemma is_Hcomp_HcompNml:
    assumes "Nml t" and "Nml u" and "Src t = Trg u"
    and "¬ is_Prim₀ t" and "¬ is_Prim₀ u"
    shows "is_Hcomp (t \<lfloor>\<star>\<rfloor> u)"
    proof -
      have "[ ¬ is_Hcomp (t \<lfloor>\<star>\<rfloor> u); Nml t; Nml u; Src t = Trg u; ¬ is_Prim₀ t; ¬ is_Prim₀ u ]
                ==> False"
      proof (induct t, simp_all add: Nml_HcompD)
        fix a
        assume a: "obj a"
        assume u: "Nml u"
        assume 1: "¬ is_Hcomp u"
        assume 2: "¬ is_Prim₀ (Trg u)"
        show "False"
          using u 1 2 by (cases u; simp)
        next
        fix v w
        assume I2: "¬ is_Hcomp (w \<lfloor>\<star>\<rfloor> u) ==> False"
        assume vw: "Nml (v \<star> w)"
        assume u: "Nml u"
        assume 1: "¬ is_Hcomp ((v \<star> w) \<lfloor>\<star>\<rfloor> u)"
        assume 2: "¬ is_Prim₀ u"
        assume 3: "Src w = Trg u"
        show "False"
        proof -
          have v: "v = \<langle>un_Prim v\<rangle>"
            using vw Nml_HcompD by metis
          have w: "Nml w ∧ ¬ is_Prim₀ w ∧ \<langle>src (un_Prim v)\<rangle>₀ = Trg w"
            using vw Nml_HcompD [of v w] by blast
          have "(v \<star> w) \<lfloor>\<star>\<rfloor> u = v \<star> (w \<lfloor>\<star>\<rfloor> u)"
          proof -
            have "(v \<star> w) \<lfloor>\<star>\<rfloor> u = \<langle>un_Prim v\<rangle> \<lfloor>\<star>\<rfloor> (w \<lfloor>\<star>\<rfloor> u)"
              using u v 2 by (cases u, simp_all)
            also have "... = \<langle>un_Prim v\<rangle> \<star> (w \<lfloor>\<star>\<rfloor> u)"
              using u w I2 by fastforce
            also have "... = v \<star> (w \<lfloor>\<star>\<rfloor> u)"
              using v by simp
            finally show ?thesis by simp
          qed
          thus ?thesis using 1 by simp
        qed
      qed
      thus ?thesis using assms by blast
    qed

    text ‹
 The following function defines the ``dimension'' of a term,
 which is the number of inputs (or outputs) when the term is regarded as an
 interconnection matrix.
 For normal terms, this is just the length of the term when regarded as a list
 of arrows of @{term C}.
 This function is used as a ranking of terms in the subsequent associativity proof.
 ›

    primrec dim :: "'a term ==> nat"
    where "dim \<langle>μ\<rangle>₀ = 0"
        | "dim \<langle>μ\<rangle> = 1"
        | "dim (t \<star> u) = (dim t + dim u)"
        | "dim (t \<cdot> u) = dim t"
        | "dim \<l>[t] = dim t"
        | "dim \<l>^-1[t] = dim t"
        | "dim \<r>[t] = dim t"
        | "dim \<r>^-1[t] = dim t"
        | "dim \<a>[t, u, v] = dim t + dim u + dim v"
        | "dim \<a>^-1[t, u, v] = dim t + dim u + dim v"

    lemma HcompNml_assoc:
    assumes "Nml t" and "Nml u" and "Nml v" and "Src t = Trg u" and "Src u = Trg v"
    shows "(t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)"
    proof -
      have "∧n t u v. [ dim t = n; Nml t; Nml u; Nml v; Src t = Trg u; Src u = Trg v ] ==>
                        (t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)"
      proof -
        fix n
        show "∧t u v. [ dim t = n; Nml t; Nml u; Nml v; Src t = Trg u; Src u = Trg v ] ==>
                        (t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)"
        proof (induction n rule: nat_less_induct)
          fix n :: nat and t :: "'a term" and u v
          assume I: "∀m<n. ∀t u v. dim t = m ⟶ Nml t ⟶ Nml u ⟶ Nml v ⟶
                                   Src t = Trg u ⟶ Src u = Trg v ⟶
                                   (t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)"
          assume dim: "dim t = n"
          assume t: "Nml t"
          assume u: "Nml u"
          assume v: "Nml v"
          assume tu: "Src t = Trg u"
          assume uv: "Src u = Trg v"
          show "(t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = t \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)"
          proof -
            have "is_Prim₀ t ==> ?thesis" by (cases t; simp)
            moreover have "¬is_Prim₀ t ==> is_Prim₀ u ==> ?thesis"
              by (cases t; simp; cases u; simp)
            moreover have "¬ is_Prim₀ t ==> ¬ is_Prim₀ u ==> is_Prim₀ v ==> ?thesis"
            proof -
              assume 1: "¬ is_Prim₀ t"
              assume 2: "¬ is_Prim₀ u"
              assume 3: "is_Prim₀ v"
              have "¬is_Prim₀ (t \<lfloor>\<star>\<rfloor> u)"
                using 1 2 t u tu is_Hcomp_HcompNml [of t u]
                by (cases t, simp, cases u, auto)
              thus ?thesis
                using 1 2 3 tu uv by (cases v, simp, cases "t \<lfloor>\<star>\<rfloor> u", simp_all)
            qed
            moreover have "¬is_Prim₀ t ∧ ¬ is_Prim₀ u ∧ ¬ is_Prim₀ v ∧ is_Prim t ==> ?thesis"
              using v by (cases t, simp_all, cases u, simp_all; cases v, simp_all)
            moreover have "¬is_Prim₀ t ∧ ¬ is_Prim₀ u ∧ ¬ is_Prim₀ v ∧ is_Hcomp t ==> ?thesis"
            proof (cases t, simp_all)
              fix w :: "'a term" and x :: "'a term"
              assume 1: " ¬ is_Prim₀ u ∧ ¬ is_Prim₀ v"
              assume 2: "t = (w \<star> x)"
              show "((w \<star> x) \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = (w \<star> x) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)"
              proof -
                have w: "w = \<langle>un_Prim w\<rangle>"
                  using t 1 2 Nml_HcompD by metis
                have x: "Nml x"
                  using t w 1 2 by (metis Nml.simps(3))
                have "((w \<star> x) \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v = (w \<lfloor>\<star>\<rfloor> (x \<lfloor>\<star>\<rfloor> u)) \<lfloor>\<star>\<rfloor> v"
                  using u v w x 1 2 by (cases u, simp_all)
                also have "... = (w \<star> (x \<lfloor>\<star>\<rfloor> u)) \<lfloor>\<star>\<rfloor> v"
                  using t w u 1 2 HcompNml_Prim is_Hcomp_HcompNml Nml_HcompD
                  by (metis Src.simps(3) term.distinct_disc(3) tu)
                also have "... = w \<lfloor>\<star>\<rfloor> ((x \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v)"
                  using u v w x 1 by (cases u, simp_all; cases v, simp_all)
                also have "... = w \<lfloor>\<star>\<rfloor> (x \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v))"
                proof -
                  have "dim x < dim t"
                    using 2 w by (cases w; simp)
                  moreover have "Src x = Trg u ∧ Src u = Trg v"
                    using tu uv 2 by auto
                  ultimately show ?thesis 
                    using u v x dim I by simp
                qed
                also have "... = (w \<star> x) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<star>\<rfloor> v)"
                proof -
                  have 3: "is_Hcomp (u \<lfloor>\<star>\<rfloor> v)"
                    using u v uv 1 is_Hcomp_HcompNml by auto
                  obtain u' :: "'a term" and v' where uv': "u \<lfloor>\<star>\<rfloor> v = u' \<star> v'"
                    using 3 is_Hcomp_def by blast
                  thus ?thesis by simp
                qed
                finally show ?thesis by simp
              qed
            qed
            moreover have "is_Prim₀ t ∨ is_Prim t ∨ is_Hcomp t"
              using t by (cases t, simp_all)
            ultimately show ?thesis by blast
          qed
        qed
      qed
      thus ?thesis using assms by blast
    qed

    lemma HcompNml_Trg_Nml:
    assumes "Nml t"
    shows "Trg t \<lfloor>\<star>\<rfloor> t = t"
    proof -
      have "Nml t ==> Trg t \<lfloor>\<star>\<rfloor> t = t"
      proof (induct t, simp_all add: Nml_HcompD)
        fix u v
        assume uv: "Nml (u \<star> v)"
        assume I1: "Trg u \<lfloor>\<star>\<rfloor> u = u"
        have 1: "Nml u ∧ Nml v ∧ Src u = Trg v"
          using uv Nml_HcompD by blast
        have 2: "Trg (u \<star> v) = Trg u"
          using uv by auto
        show "Trg u \<lfloor>\<star>\<rfloor> u \<star> v = u \<star> v"
        proof -
          have "Trg u \<lfloor>\<star>\<rfloor> u \<star> v = Trg u \<lfloor>\<star>\<rfloor> u \<lfloor>\<star>\<rfloor> v"
            using uv HcompNml_Nml by simp
          also have "... = (Trg u \<lfloor>\<star>\<rfloor> u) \<lfloor>\<star>\<rfloor> v"
            using 1 2 HcompNml_assoc Src_Trg Nml_Trg Nml_implies_Arr by simp
          also have "... = u \<star> v"
            using I1 uv HcompNml_Nml by simp
          finally show ?thesis by simp
        qed
      qed
      thus ?thesis using assms by simp
    qed

    lemma HcompNml_Nml_Src:
    assumes "Nml t"
    shows "t \<lfloor>\<star>\<rfloor> Src t = t"
    proof -
      have "Nml t ==> t \<lfloor>\<star>\<rfloor> Src t = t"
      proof (induct t, simp_all add: Nml_HcompD)
        fix u v
        assume uv: "Nml (u \<star> v)"
        assume I2: "v \<lfloor>\<star>\<rfloor> Src v = v"
        have 1: "Nml u ∧ Nml v ∧ Src u = Trg v"
          using uv Nml_HcompD by blast
        have 2: "Src (u \<star> v) = Src v"
          using uv Trg_HcompNml by auto
        show "(u \<star> v) \<lfloor>\<star>\<rfloor> Src v = u \<star> v"
        proof -
          have "(u \<star> v) \<lfloor>\<star>\<rfloor> Src v = (u \<lfloor>\<star>\<rfloor> v) \<lfloor>\<star>\<rfloor> Src v"
            using uv HcompNml_Nml by simp
          also have "... = u \<lfloor>\<star>\<rfloor> (v \<lfloor>\<star>\<rfloor> Src v)"
            using 1 2 HcompNml_assoc Trg_Src Nml_Src Nml_implies_Arr by simp
          also have "... = u \<star> v"
            using I2 uv HcompNml_Nml by simp
          finally show ?thesis by simp
        qed
      qed
      thus ?thesis using assms by simp
    qed

    lemma HcompNml_Obj_Nml:
    assumes "Obj t" and "Nml u" and "Src t = Trg u"
    shows "t \<lfloor>\<star>\<rfloor> u = u"
      using assms by (cases t, simp_all add: HcompNml_Trg_Nml)

    lemma HcompNml_Nml_Obj:
    assumes "Nml t" and "Obj u" and "Src t = Trg u"
    shows "t \<lfloor>\<star>\<rfloor> u = t"
      using assms by (cases u, simp_all)

    lemma Ide_HcompNml:
    assumes "Ide t" and "Ide u" and "Nml t" and "Nml u" and "Src t = Trg u"
    shows "Ide (t \<lfloor>\<star>\<rfloor> u)"
      using assms
      by (metis (mono_tags, lifting) Nml_HcompNml(1) Nml_implies_Arr Dom_HcompNml
          Ide_Dom Ide_in_Hom(2) mem_Collect_eq)

    lemma Can_HcompNml:
    assumes "Can t" and "Can u" and "Nml t" and "Nml u" and "Src t = Trg u"
    shows "Can (t \<lfloor>\<star>\<rfloor> u)"
    proof -
      have "∧u. [ Can t ∧ Nml t; Can u ∧ Nml u; Src t = Trg u ] ==> Can (t \<lfloor>\<star>\<rfloor> u)"
      proof (induct t, simp_all add: HcompNml_Trg_Nml HcompNml_Nml_Src)
        show "∧x u. ide x ∧ arr x ==> Can u ∧ Nml u ==> \<langle>src x\<rangle>₀ = Trg u ==> Can (\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u)"
          by (metis Ide.simps(1-2) Ide_implies_Can Can.simps(3) Nml.elims(2)
              Nml.simps(2) HcompNml.simps(12) HcompNml_Prim Ide_HcompNml
              Src.simps(2) term.disc(2))
        show "∧v w u.
                 (∧u. Nml v ==> Can u ∧ Nml u ==> Trg w = Trg u ==> Can (v \<lfloor>\<star>\<rfloor> u)) ==>
                 (∧ua. Nml w ==> Can ua ∧ Nml ua ==> Trg u = Trg ua ==> Can (w \<lfloor>\<star>\<rfloor> ua)) ==>
                 Can v ∧ Can w ∧ Src v = Trg w ∧ Nml (v \<star> w) ==>
                 Can u ∧ Nml u ==> Src w = Trg u ==> Can ((v \<star> w) \<lfloor>\<star>\<rfloor> u)"
          by (metis Nml_HcompD(3-4) HcompNml_Nml Nml_HcompNml(1)
              HcompNml_assoc Trg_HcompNml)
      qed
      thus ?thesis using assms by blast
    qed

    lemma Inv_HcompNml:
    assumes "Can t" and "Can u" and "Nml t" and "Nml u" and "Src t = Trg u"
    shows "Inv (t \<lfloor>\<star>\<rfloor> u) = Inv t \<lfloor>\<star>\<rfloor> Inv u"
    proof -
      have "∧u. [ Can t ∧ Nml t; Can u ∧ Nml u; Src t = Trg u ]
                   ==> Inv (t \<lfloor>\<star>\<rfloor> u) = Inv t \<lfloor>\<star>\<rfloor> Inv u"
      proof (induct t, simp_all add: HcompNml_Trg_Nml HcompNml_Nml_Src)
        show "∧x u. [ obj x; Can u ∧ Nml u; \<langle>x\<rangle>₀ = Trg u ] ==> Inv u = Inv (Trg u) \<lfloor>\<star>\<rfloor> Inv u"
          by (metis HcompNml.simps(1) Inv.simps(1))
        show "∧x u. ide x ∧ arr x ==> Can u ∧ Nml u ==> \<langle>src x\<rangle>₀ = Trg u ==>
                    Inv (\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u) = \<langle>x\<rangle> \<lfloor>\<star>\<rfloor> Inv u"
          by (metis Ide.simps(2) HcompNml.simps(2) HcompNml_Prim Inv.simps(1,3)
                    Inv_Ide Inv_Inv is_Prim₀_def)
        fix v w u
        assume I1: "∧x. Nml v ==> Can x ∧ Nml x ==> Trg w = Trg x ==>
                        Inv (v \<lfloor>\<star>\<rfloor> x) = Inv v \<lfloor>\<star>\<rfloor> Inv x"
        assume I2: "∧x. Nml w ==> Can x ∧ Nml x ==> Trg u = Trg x ==>
                              Inv (w \<lfloor>\<star>\<rfloor> x) = Inv w \<lfloor>\<star>\<rfloor> Inv x"
        assume vw: "Can v ∧ Can w ∧ Src v = Trg w ∧ Nml (v \<star> w)"
        assume wu: "Src w = Trg u"
        assume u: "Can u ∧ Nml u"
        have v: "Can v ∧ Nml v"
          using vw Nml_HcompD by blast
        have w: "Can w ∧ Nml w"
          using v vw by (cases v, simp_all)
        show "Inv ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = (Inv v \<star> Inv w) \<lfloor>\<star>\<rfloor> Inv u"
        proof -
          have "is_Prim₀ u ==> ?thesis"
            apply (cases u) by simp_all
          moreover have "¬ is_Prim₀ u ==> ?thesis"
          proof -
            assume 1: "¬ is_Prim₀ u"
            have "Inv ((v \<star> w) \<lfloor>\<star>\<rfloor> u) = Inv (v \<lfloor>\<star>\<rfloor> (w \<lfloor>\<star>\<rfloor> u))"
              using 1 by (cases u, simp_all)
            also have "... = Inv v \<lfloor>\<star>\<rfloor> Inv (w \<lfloor>\<star>\<rfloor> u)"
              using u v w vw wu I1 Nml_HcompNml Can_HcompNml Nml_Inv Can_Inv
              by simp
            also have "... = Inv v \<lfloor>\<star>\<rfloor> (Inv w \<lfloor>\<star>\<rfloor> Inv u)"
              using u v w I2 Nml_HcompNml by simp
            also have "... = (Inv v \<star> Inv w) \<lfloor>\<star>\<rfloor> Inv u"
              using v 1 by (cases u, simp_all)
            finally show ?thesis by blast
          qed
          ultimately show ?thesis by blast
        qed
      qed
      thus ?thesis using assms by blast
    qed

    text ‹
 The following function defines vertical composition for compatible normal terms,
 by ``pushing the composition down'' to arrows of @{text V}.
 ›

    fun VcompNml :: "'a term ==> 'a term ==> 'a term"  (infixr ‹\⌊\⋅\⌋› 55)
    where "\<langle>ν\<rangle>₀ \<lfloor>\<cdot>\<rfloor> u = u"
        | "\<langle>ν\<rangle> \<lfloor>\<cdot>\<rfloor> \<langle>μ\<rangle> = \<langle>ν ⋅ μ\<rangle>"
        | "(u \<star> v) \<lfloor>\<cdot>\<rfloor> (w \<star> x) = (u \<lfloor>\<cdot>\<rfloor> w \<star> v \<lfloor>\<cdot>\<rfloor> x)"
        | "t \<lfloor>\<cdot>\<rfloor> \<langle>μ\<rangle>₀ = t"
        | "t \<lfloor>\<cdot>\<rfloor> _ = undefined \<cdot> undefined"

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

    lemma Nml_VcompNml:
    assumes "Nml t" and "Nml u" and "Dom t = Cod u"
    shows "Nml (t \<lfloor>\<cdot>\<rfloor> u)"
    and "Dom (t \<lfloor>\<cdot>\<rfloor> u) = Dom u"
    and "Cod (t \<lfloor>\<cdot>\<rfloor> u) = Cod t"
    proof -
      have 0: "∧u. [ Nml t; Nml u; Dom t = Cod u ] ==>
                     Nml (t \<lfloor>\<cdot>\<rfloor> u) ∧ Dom (t \<lfloor>\<cdot>\<rfloor> u) = Dom u ∧ Cod (t \<lfloor>\<cdot>\<rfloor> u) = Cod t"
      proof (induct t, simp_all add: Nml_HcompD)
        show "∧x u. obj x ==> Nml u ==> \<langle>x\<rangle>₀ = Cod u ==>
                     Nml (Cod u \<lfloor>\<cdot>\<rfloor> u) ∧ Dom (Cod u \<lfloor>\<cdot>\<rfloor> u) = Dom u ∧
                     Cod (Cod u \<lfloor>\<cdot>\<rfloor> u) = Cod (Cod u)"
          by (metis Cod.simps(1) VcompNml.simps(1))
        fix ν u
        assume ν: "arr ν"
        assume u: "Nml u"
        assume 1: "\<langle>dom ν\<rangle> = Cod u"
        show "Nml (\<langle>ν\<rangle> \<lfloor>\<cdot>\<rfloor> u) ∧ Dom (\<langle>ν\<rangle> \<lfloor>\<cdot>\<rfloor> u) = Dom u ∧ Cod (\<langle>ν\<rangle> \<lfloor>\<cdot>\<rfloor> u) = \<langle>cod ν\<rangle>"
          using ν u 1 by (cases u, simp_all)
        next
        fix u v w
        assume I2: "∧u. [ Nml u; Dom w = Cod u ] ==>
                          Nml (w \<lfloor>\<cdot>\<rfloor> u) ∧ Dom (w \<lfloor>\<cdot>\<rfloor> u) = Dom u ∧ Cod (w \<lfloor>\<cdot>\<rfloor> u) = Cod w"
        assume vw: "Nml (v \<star> w)"
        have v: "Nml v"
          using vw Nml_HcompD by blast
        have w: "Nml w"
          using vw Nml_HcompD by blast
        assume u: "Nml u"
        assume 1: "(Dom v \<star> Dom w) = Cod u"
        show "Nml ((v \<star> w) \<lfloor>\<cdot>\<rfloor> u) ∧ Dom ((v \<star> w) \<lfloor>\<cdot>\<rfloor> u) = Dom u ∧
                                     Cod ((v \<star> w) \<lfloor>\<cdot>\<rfloor> u) = Cod v \<star> Cod w"
          using u v w 1
        proof (cases u, simp_all)
          fix x y
          assume 2: "u = x \<star> y"
          have 4: "is_Prim x ∧ x = \<langle>un_Prim x\<rangle> ∧ arr (un_Prim x) ∧ Nml y ∧ ¬ is_Prim₀ y"
            using u 2 by (cases x, cases y, simp_all)
          have 5: "is_Prim v ∧ v = \<langle>un_Prim v\<rangle> ∧ arr (un_Prim v) ∧ Nml w ∧ ¬ is_Prim₀ w"
            using v w vw by (cases v, simp_all)
          have 6: "dom (un_Prim v) = cod (un_Prim x) ∧ Dom w = Cod y"
          proof -
            have "\<langle>src (un_Prim v)\<rangle>₀ = Trg w" using vw Nml_HcompD [of v w] by simp
            thus "dom (un_Prim v) = cod (un_Prim x) ∧ Dom w = Cod y"
              using 1 2 4 5 apply (cases u, simp_all)
              by (metis Cod.simps(2) Dom.simps(2) term.simps(2))
          qed
          have "(v \<star> w) \<lfloor>\<cdot>\<rfloor> u = \<langle>un_Prim v ⋅ un_Prim x\<rangle> \<star> w \<lfloor>\<cdot>\<rfloor> y"
            using 2 4 5 6 VcompNml.simps(2) [of "un_Prim v" "un_Prim x"] by simp
          moreover have "Nml (\<langle>un_Prim v ⋅ un_Prim x\<rangle> \<star> w \<lfloor>\<cdot>\<rfloor> y)"
          proof -
            have "Nml (w \<lfloor>\<cdot>\<rfloor> y)"
              using I2 4 5 6 by simp
            moreover have "¬ is_Prim₀ (w \<lfloor>\<cdot>\<rfloor> y)"
              using vw 4 5 6 I2 Nml_Cod Nml_HcompD(5) is_Prim₀_def
              by (metis Cod.simps(1) Cod.simps(3))
            moreover have "\<langle>src (un_Prim v ⋅ un_Prim x)\<rangle>₀ = Trg (w \<lfloor>\<cdot>\<rfloor> y)"
              using vw 4 5 6 I2 Nml_HcompD(6) Nml_implies_Arr
                    src.as_nat_trans.naturality1 src.as_nat_trans.preserves_comp_2
                    Trg_Cod src_cod
              by (metis seqI)
            ultimately show ?thesis
              using 4 5 6 Nml.simps(3) [of "un_Prim v ⋅ un_Prim x" "(w \<lfloor>\<cdot>\<rfloor> y)"]
              by simp
          qed
          ultimately show "Nml (v \<lfloor>\<cdot>\<rfloor> x \<star> w \<lfloor>\<cdot>\<rfloor> y) ∧
                           Dom (v \<lfloor>\<cdot>\<rfloor> x) = Dom x ∧ Dom (w \<lfloor>\<cdot>\<rfloor> y) = Dom y ∧
                           Cod (v \<lfloor>\<cdot>\<rfloor> x) = Cod v ∧ Cod (w \<lfloor>\<cdot>\<rfloor> y) = Cod w"
            using 4 5 6 I2
            by (metis (no_types, lifting) Cod.simps(2) Dom.simps(2) VcompNml.simps(2)
                cod_comp dom_comp seqI)
        qed
      qed
      show "Nml (t \<lfloor>\<cdot>\<rfloor> u)" using assms 0 by blast
      show "Dom (t \<lfloor>\<cdot>\<rfloor> u) = Dom u" using assms 0 by blast
      show "Cod (t \<lfloor>\<cdot>\<rfloor> u) = Cod t" using assms 0 by blast
    qed

    lemma VcompNml_in_Hom [intro]:
    assumes "Nml t" and "Nml u" and "Dom t = Cod u"
    shows "t \<lfloor>\<cdot>\<rfloor> u ∈ HHom (Src u) (Trg u)" and "t \<lfloor>\<cdot>\<rfloor> u ∈ VHom (Dom u) (Cod t)"
    proof -
      show 1: "t \<lfloor>\<cdot>\<rfloor> u ∈ VHom (Dom u) (Cod t)"
        using assms Nml_VcompNml Nml_implies_Arr by simp
      show "t \<lfloor>\<cdot>\<rfloor> u ∈ HHom (Src u) (Trg u)"
        using assms 1 Src_Dom Trg_Dom Nml_implies_Arr by fastforce
    qed

    lemma Src_VcompNml:
    assumes "Nml t" and "Nml u" and "Dom t = Cod u"
    shows "Src (t \<lfloor>\<cdot>\<rfloor> u) = Src u"
      using assms VcompNml_in_Hom by simp

    lemma Trg_VcompNml:
    assumes "Nml t" and "Nml u" and "Dom t = Cod u"
    shows "Trg (t \<lfloor>\<cdot>\<rfloor> u) = Trg u"
      using assms VcompNml_in_Hom by simp

    lemma Dom_VcompNml:
    assumes "Nml t" and "Nml u" and "Dom t = Cod u"
    shows "Dom (t \<lfloor>\<cdot>\<rfloor> u) = Dom u"
      using assms Nml_VcompNml(2) by simp

    lemma Cod_VcompNml:
    assumes "Nml t" and "Nml u" and "Dom t = Cod u"
    shows "Cod (t \<lfloor>\<cdot>\<rfloor> u) = Cod t"
      using assms Nml_VcompNml(3) by simp

    lemma VcompNml_Cod_Nml [simp]:
    assumes "Nml t"
    shows "VcompNml (Cod t) t = t"
    proof -
      have "Nml t ==> Cod t \<lfloor>\<cdot>\<rfloor> t = t"
        apply (induct t)
        by (auto simp add: Nml_HcompD comp_cod_arr)
      thus ?thesis using assms by blast
    qed

    lemma VcompNml_Nml_Dom [simp]:
    assumes "Nml t"
    shows "t \<lfloor>\<cdot>\<rfloor> (Dom t) = t"
    proof -
      have "Nml t ==> t \<lfloor>\<cdot>\<rfloor> Dom t = t"
        apply (induct t) by (auto simp add: Nml_HcompD comp_arr_dom)
      thus ?thesis using assms by blast
    qed

    lemma VcompNml_Ide_Nml [simp]:
    assumes "Nml t" and "Ide a" and "Dom a = Cod t"
    shows "a \<lfloor>\<cdot>\<rfloor> t = t"
      using assms Ide_in_Hom by simp

    lemma VcompNml_Nml_Ide [simp]:
    assumes "Nml t" and "Ide a" and "Dom t = Cod a"
    shows "t \<lfloor>\<cdot>\<rfloor> a = t"
      using assms Ide_in_Hom by auto

    lemma VcompNml_assoc:
    assumes "Nml t" and "Nml u" and "Nml v"
    and "Dom t = Cod u" and "Dom u = Cod v"
    shows "(t \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = t \<lfloor>\<cdot>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> v)"
    proof -
      have "∧u v. [ Nml t; Nml u; Nml v; Dom t = Cod u; Dom u = Cod v ] ==>
                    (t \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = t \<lfloor>\<cdot>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> v)"
      proof (induct t, simp_all)
        show "∧x u v. obj x ==> Nml u ==> Nml v ==> \<langle>x\<rangle>₀ = Cod u ==> Dom u = Cod v ==>
                       u \<lfloor>\<cdot>\<rfloor> v = Cod u \<lfloor>\<cdot>\<rfloor> u \<lfloor>\<cdot>\<rfloor> v"
          by (metis VcompNml.simps(1))
        fix f u v
        assume f: "arr f"
        assume u: "Nml u"
        assume v: "Nml v"
        assume 1: "\<langle>dom f\<rangle> = Cod u"
        assume 2: "Dom u = Cod v"
        show "(\<langle>f\<rangle> \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = \<langle>f\<rangle> \<lfloor>\<cdot>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> v)"
          using u v f 1 2 comp_assoc
          apply (cases u)
                   apply simp_all
          apply (cases v)
          by simp_all
        next
        fix u v w x
        assume I1: "∧u v. [ Nml w; Nml u; Nml v; Dom w = Cod u; Dom u = Cod v ] ==>
                            (w \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = w \<lfloor>\<cdot>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> v)"
        assume I2: "∧u v. [ Nml x; Nml u; Nml v; Dom x = Cod u; Dom u = Cod v ] ==>
                            (x \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = x \<lfloor>\<cdot>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> v)"
        assume wx: "Nml (w \<star> x)"
        assume u: "Nml u"
        assume v: "Nml v"
        assume 1: "(Dom w \<star> Dom x) = Cod u"
        assume 2: "Dom u = Cod v"
        show "((w \<star> x) \<lfloor>\<cdot>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> v = (w \<star> x) \<lfloor>\<cdot>\<rfloor> u \<lfloor>\<cdot>\<rfloor> v"
        proof -
          have w: "Nml w"
            using wx Nml_HcompD by blast
          have x: "Nml x"
            using wx Nml_HcompD by blast
          have "is_Hcomp u"
            using u 1 by (cases u) simp_all
          thus ?thesis
            using u v apply (cases u, simp_all, cases v, simp_all)
          proof -
            fix u1 u2 v1 v2
            assume 3: "u = (u1 \<star> u2)"
            assume 4: "v = (v1 \<star> v2)"
            show "(w \<lfloor>\<cdot>\<rfloor> u1) \<lfloor>\<cdot>\<rfloor> v1 = w \<lfloor>\<cdot>\<rfloor> u1 \<lfloor>\<cdot>\<rfloor> v1 ∧
                  (x \<lfloor>\<cdot>\<rfloor> u2) \<lfloor>\<cdot>\<rfloor> v2 = x \<lfloor>\<cdot>\<rfloor> u2 \<lfloor>\<cdot>\<rfloor> v2"
            proof -
              have "Nml u1 ∧ Nml u2"
                using u 3 Nml_HcompD by blast
              moreover have "Nml v1 ∧ Nml v2"
                using v 4 Nml_HcompD by blast
              ultimately show ?thesis using w x I1 I2 1 2 3 4 by simp
            qed
          qed
        qed
      qed
      thus ?thesis using assms by blast
    qed

    lemma Ide_VcompNml:
    assumes "Ide t" and "Ide u" and "Nml t" and "Nml u" and "Dom t = Cod u"
    shows "Ide (t \<lfloor>\<cdot>\<rfloor> u)"
    proof -
      have "∧u. [ Ide t; Ide u; Nml t; Nml u; Dom t = Cod u ] ==> Ide (VcompNml t u)"
        by (induct t, simp_all)
      thus ?thesis using assms by blast
    qed

    lemma Can_VcompNml:
    assumes "Can t" and "Can u" and "Nml t" and "Nml u" and "Dom t = Cod u"
    shows "Can (t \<lfloor>\<cdot>\<rfloor> u)"
    proof -
      have "∧u. [ Can t ∧ Nml t; Can u ∧ Nml u; Dom t = Cod u ] ==> Can (t \<lfloor>\<cdot>\<rfloor> u)"
      proof (induct t, simp_all)
        fix t u v
        assume I1: "∧v. [ Nml t; Can v ∧ Nml v; Dom t = Cod v ] ==> Can (t \<lfloor>\<cdot>\<rfloor> v)"
        assume I2: "∧v. [ Nml u; Can v ∧ Nml v; Dom u = Cod v ] ==> Can (u \<lfloor>\<cdot>\<rfloor> v)"
        assume tu: "Can t ∧ Can u ∧ Src t = Trg u ∧ Nml (t \<star> u)"
        have t: "Can t ∧ Nml t"
          using tu Nml_HcompD by blast
        have u: "Can u ∧ Nml u"
          using tu Nml_HcompD by blast
        assume v: "Can v ∧ Nml v"
        assume 1: "(Dom t \<star> Dom u) = Cod v"
        show "Can ((t \<star> u) \<lfloor>\<cdot>\<rfloor> v)"
        proof -
          have 2: "(Dom t \<star> Dom u) = Cod v" using 1 by simp
          show ?thesis
            using v 2
          proof (cases v; simp)
            fix w x
            assume wx: "v = (w \<star> x)"
            have "Can w ∧ Nml w" using v wx Nml_HcompD Can.simps(3) by blast
            moreover have "Can x ∧ Nml x" using v wx Nml_HcompD Can.simps(3) by blast
            moreover have "Dom t = Cod w" using 2 wx by simp
            moreover have ux: "Dom u = Cod x" using 2 wx by simp
            ultimately show "Can (t \<lfloor>\<cdot>\<rfloor> w) ∧ Can (u \<lfloor>\<cdot>\<rfloor> x) ∧ Src (t \<lfloor>\<cdot>\<rfloor> w) = Trg (u \<lfloor>\<cdot>\<rfloor> x)"
              using t u v tu wx I1 I2
              by (metis Nml_HcompD(7) Src_VcompNml Trg_VcompNml)
          qed
        qed
      qed
      thus ?thesis using assms by blast
    qed

    lemma Inv_VcompNml:
    assumes "Can t" and "Can u" and "Nml t" and "Nml u" and "Dom t = Cod u"
    shows "Inv (t \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> Inv t"
    proof -
      have "∧u. [ Can t ∧ Nml t; Can u ∧ Nml u; Dom t = Cod u ] ==>
              Inv (t \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> Inv t"
      proof (induct t, simp_all)
        show "∧x u. [ obj x; Can u ∧ Nml u; \<langle>x\<rangle>₀ = Cod u ] ==> Inv u = Inv u \<lfloor>\<cdot>\<rfloor> Inv (Cod u)"
          by (simp add: Can_implies_Arr)
        show "∧x u. [ ide x ∧ arr x; Can u ∧ Nml u; \<langle>x\<rangle> = Cod u ] ==>
                      Inv u = Inv u \<lfloor>\<cdot>\<rfloor> Inv (Cod u)"
          by (simp add: Can_implies_Arr)
        fix v w u
        assume vw: "Can v ∧ Can w ∧ Src v = Trg w ∧ Nml (v \<star> w)"
        have v: "Can v ∧ Nml w"
          using vw Nml_HcompD by blast
        have w: "Can w ∧ Nml w"
          using vw Nml_HcompD by blast
        assume I1: "∧x. [ Nml v; Can x ∧ Nml x; Dom v = Cod x ] ==>
                          Inv (v \<lfloor>\<cdot>\<rfloor> x) = Inv x \<lfloor>\<cdot>\<rfloor> Inv v"
        assume I2: "∧x. [ Nml w; Can x ∧ Nml x; Dom w = Cod x ] ==>
                          Inv (w \<lfloor>\<cdot>\<rfloor> x) = Inv x \<lfloor>\<cdot>\<rfloor> Inv w"
        assume u: "Can u ∧ Nml u"
        assume 1: "(Dom v \<star> Dom w) = Cod u"
        show "Inv ((v \<star> w) \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> (Inv v \<star> Inv w)"
          using v 1
        proof (cases w, simp_all)
          show "∧μ. obj μ ==> Dom v \<star> \<langle>μ\<rangle>₀ = Cod u ==> w = \<langle>μ\<rangle>₀ ==> Can v ==>
                     Inv ((v \<star> \<langle>μ\<rangle>₀) \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> (Inv v \<star> \<langle>μ\<rangle>₀)"
            using Nml_HcompD(5) is_Prim₀_def vw by blast
          show "∧μ. arr μ ==> Dom v \<star> \<langle>dom μ\<rangle> = Cod u ==> w = \<langle>μ\<rangle> ==> Can v ==>
                     Inv ((v \<star> \<langle>μ\<rangle>) \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> (Inv v \<star> \<langle>inv μ\<rangle>)"
            by (metis Ide.simps(2) Can.simps(2) Nml_HcompD(1) Dom.simps(2) Inv_Ide
                      Dom_Inv Nml_Inv ideD(2) inv_ide VcompNml_Cod_Nml VcompNml_Nml_Dom
                      u vw)
          show "∧y z. Nml (y \<star> z) ==> Dom v \<star> Dom y \<star> Dom z = Cod u ==>
                           w = y \<star> z ==> Can v ==>
                          Inv ((v \<star> y \<star> z) \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> (Inv v \<star> Inv y \<star> Inv z)"
          proof -
            fix y z
            assume 2: "Nml (y \<star> z)"
            assume yz: "w = y \<star> z"
            show "Inv ((v \<star> y \<star> z) \<lfloor>\<cdot>\<rfloor> u) = Inv u \<lfloor>\<cdot>\<rfloor> (Inv v \<star> Inv y \<star> Inv z)"
              using u vw yz I1 I2 1 2 VcompNml_Nml_Ide
              apply (cases u)
                       apply simp_all
              by (metis Nml_HcompD(3-4))
          qed
        qed
      qed
      thus ?thesis using assms by blast
    qed

    lemma Can_and_Nml_implies_Ide:
    assumes "Can t" and "Nml t"
    shows "Ide t"
    proof -
      have "[ Can t; Nml t ] ==> Ide t"
        apply (induct t) by (simp_all add: Nml_HcompD)
      thus ?thesis using assms by blast
    qed

    lemma VcompNml_Can_Inv [simp]:
    assumes "Can t" and "Nml t"
    shows "t \<lfloor>\<cdot>\<rfloor> Inv t = Cod t"
      using assms Can_and_Nml_implies_Ide Ide_in_Hom by simp
      
    lemma VcompNml_Inv_Can [simp]:
    assumes "Can t" and "Nml t"
    shows "Inv t \<lfloor>\<cdot>\<rfloor> t = Dom t"
      using assms Can_and_Nml_implies_Ide Ide_in_Hom by simp

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

    lemma VcompNml_HcompNml:
    assumes "Nml t" and "Nml u" and "Nml v" and "Nml w"
    and "VSeq t v" and "VSeq u w" and "Src v = Trg w"
    shows "(t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = (t \<lfloor>\<cdot>\<rfloor> v) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)"
    proof -
      have "∧u v w. [ Nml t; Nml u; Nml v; Nml w; VSeq t v; VSeq u w;
                      Src t = Trg u; Src v = Trg w ] ==>
                      (t \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = (t \<lfloor>\<cdot>\<rfloor> v) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)"
      proof (induct t, simp_all)
        fix u v w x
        assume u: "Nml u"
        assume v: "Nml v"
        assume w: "Nml w"
        assume uw: "VSeq u w"
        show "∧x. Arr v ∧ \<langle>x\<rangle>₀ = Cod v ==> (Cod v \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = v \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w"
          using u v w uw by (cases v) simp_all
        show "∧x. [ arr x; Arr v ∧ \<langle>dom x\<rangle> = Cod v; \<langle>src x\<rangle>₀ = Trg u; Src v = Trg w ] ==>
                  (\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = \<langle>x\<rangle> \<lfloor>\<cdot>\<rfloor> v \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w"
        proof -
          fix x
          assume x: "arr x"
          assume 1: "Arr v ∧ \<langle>dom x\<rangle> = Cod v"
          assume tu: "\<langle>src x\<rangle>₀ = Trg u"
          assume vw: "Src v = Trg w"
          show "(\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = \<langle>x\<rangle> \<lfloor>\<cdot>\<rfloor> v \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w"
          proof -
            have 2: "v = \<langle>un_Prim v\<rangle> ∧ arr (un_Prim v)" using v 1 by (cases v) simp_all
            have "is_Prim₀ u ==> ?thesis"
              using u v w x tu uw vw 1 2 Cod.simps(3) VcompNml_Cod_Nml Dom.simps(2)
                    HcompNml_Prim HcompNml_term_Prim₀ Nml_HcompNml(3) HcompNml_Trg_Nml
              apply (cases u)
                apply simp_all
              by (cases w, simp_all add: Src_VcompNml)
            moreover have "¬ is_Prim₀ u ==> ?thesis"
            proof -
              assume 3: "¬ is_Prim₀ u"
              hence 4: "¬ is_Prim₀ w" using u w uw by (cases u, simp_all; cases w, simp_all)
              have "(\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = (\<langle>x\<rangle> \<star> u) \<lfloor>\<cdot>\<rfloor> (v \<star> w)"
              proof -
                have "\<langle>x\<rangle> \<lfloor>\<star>\<rfloor> u = \<langle>x\<rangle> \<star> u"
                  using u x 3 HcompNml_Nml by (cases u, simp_all)
                moreover have "v \<lfloor>\<star>\<rfloor> w = v \<star> w"
                  using w 2 4 HcompNml_Nml by (cases v, simp_all; cases w, simp_all)
                ultimately show ?thesis by simp
              qed
              also have 5: "... = (\<langle>x\<rangle> \<lfloor>\<cdot>\<rfloor> v) \<star> (u \<lfloor>\<cdot>\<rfloor> w)" by simp
              also have "... = (\<langle>x\<rangle> \<lfloor>\<cdot>\<rfloor> v) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)"
                using x u w uw vw 1 2 3 4 5
                      HcompNml_Nml HcompNml_Prim Nml_HcompNml(1)
                by (metis Cod.simps(3) Nml.simps(3) Dom.simps(2) Dom.simps(3)
                    Nml_VcompNml(1) tu v)
              finally show ?thesis by blast
            qed
            ultimately show ?thesis by blast
          qed
        qed
        fix t1 t2
        assume t12: "Nml (t1 \<star> t2)"
        assume I1: "∧u v w. [ Nml t1; Nml u; Nml v; Nml w;
                              Arr v ∧ Dom t1 = Cod v; VSeq u w;
                              Trg t2 = Trg u; Src v = Trg w ] ==>
                              (t1 \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = t1 \<lfloor>\<cdot>\<rfloor> v \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w"
        assume I2: "∧u' v w. [ Nml t2; Nml u'; Nml v; Nml w;
                               Arr v ∧ Dom t2 = Cod v; VSeq u' w;
                               Trg u = Trg u'; Src v = Trg w ] ==>
                              (t2 \<lfloor>\<star>\<rfloor> u') \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = (t2 \<lfloor>\<cdot>\<rfloor> v) \<lfloor>\<star>\<rfloor> (u' \<lfloor>\<cdot>\<rfloor> w)"
        have t1: "t1 = \<langle>un_Prim t1\<rangle> ∧ arr (un_Prim t1) ∧ Nml t1"
          using t12 by (cases t1, simp_all)
        have t2: "Nml t2 ∧ ¬is_Prim₀ t2"
          using t12 by (cases t1, simp_all)
        assume vw: "Src v = Trg w"
        assume tu: "Src t2 = Trg u"
        assume 1: "Arr t1 ∧ Arr t2 ∧ Src t1 = Trg t2 ∧ Arr v ∧ (Dom t1 \<star> Dom t2) = Cod v"
        show "((t1 \<star> t2) \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v \<lfloor>\<star>\<rfloor> w) = (t1 \<star> t2) \<lfloor>\<cdot>\<rfloor> v \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w"
        proof -
          have "is_Prim₀ u ==> ?thesis"
            using u v w uw tu vw t12 I1 I2 1 Obj_Src
            apply (cases u)
              apply simp_all
            by (cases w, simp_all add: Src_VcompNml)
          moreover have "¬ is_Prim₀ u ==> ?thesis"
          proof -
            assume u': "¬ is_Prim₀ u"
            hence w': "¬ is_Prim₀ w" using u w uw by (cases u, simp_all; cases w, simp_all)
            show ?thesis
              using 1 v
            proof (cases v, simp_all)
              fix v1 v2
              assume v12: "v = v1 \<star> v2"
              have v1: "v1 = \<langle>un_Prim v1\<rangle> ∧ arr (un_Prim v1) ∧ Nml v1"
                using v v12 by (cases v1, simp_all)
              have v2: "Nml v2 ∧ ¬ is_Prim₀ v2"
                using v v12 by (cases v1, simp_all)
              have 2: "v = (\<langle>un_Prim v1\<rangle> \<star> v2)"
                using v1 v12 by simp
              show "((t1 \<star> t2) \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> ((v1 \<star> v2) \<lfloor>\<star>\<rfloor> w) = (t1 \<lfloor>\<cdot>\<rfloor> v1 \<star> t2 \<lfloor>\<cdot>\<rfloor> v2) \<lfloor>\<star>\<rfloor> u \<lfloor>\<cdot>\<rfloor> w"
              proof -
                have 3: "(t1 \<star> t2) \<lfloor>\<star>\<rfloor> u = t1 \<lfloor>\<star>\<rfloor> (t2 \<lfloor>\<star>\<rfloor> u)"
                  using u u' by (cases u, simp_all)
                have 4: "v \<lfloor>\<star>\<rfloor> w = v1 \<lfloor>\<star>\<rfloor> v2 \<lfloor>\<star>\<rfloor> w"
                proof -
                  have "Src v1 = Trg v2"
                    using v v12 1 Arr.simps(3) Nml_HcompD(7) by blast
                  moreover have "Src v2 = Trg w"
                    using v v12 vw by simp
                  ultimately show ?thesis
                    using v w v1 v2 v12 2 HcompNml_assoc [of v1 v2 w] HcompNml_Nml by metis
                qed
                have "((t1 \<star> t2) \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> ((v1 \<star> v2) \<lfloor>\<star>\<rfloor> w)
                        = (t1 \<lfloor>\<star>\<rfloor> (t2 \<lfloor>\<star>\<rfloor> u)) \<lfloor>\<cdot>\<rfloor> (v1 \<lfloor>\<star>\<rfloor> (v2 \<lfloor>\<star>\<rfloor> w))"
                  using 3 4 v12 by simp
                also have "... = (t1 \<lfloor>\<cdot>\<rfloor> v1) \<lfloor>\<star>\<rfloor> ((t2 \<lfloor>\<star>\<rfloor> u) \<lfloor>\<cdot>\<rfloor> (v2 \<lfloor>\<star>\<rfloor> w))"
                proof -
                  have "is_Hcomp (t2 \<lfloor>\<star>\<rfloor> u)"
                    using t2 u u' tu is_Hcomp_HcompNml by auto
                  moreover have "is_Hcomp (v2 \<lfloor>\<star>\<rfloor> w)"
                    using v2 v12 w w' vw is_Hcomp_HcompNml by auto
                  ultimately show ?thesis
                    using u u' v w t1 v1 t12 v12 HcompNml_Prim
                    by (metis VcompNml.simps(2) VcompNml.simps(3) is_Hcomp_def
                        term.distinct_disc(3))
                qed
                also have "... = (t1 \<lfloor>\<cdot>\<rfloor> v1) \<lfloor>\<star>\<rfloor> (t2 \<lfloor>\<cdot>\<rfloor> v2) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)"
                  using u w tu uw vw t2 v2 1 2 Nml_implies_Arr I2 by auto
                also have "... = ((t1 \<lfloor>\<cdot>\<rfloor> v1) \<star> (t2 \<lfloor>\<cdot>\<rfloor> v2)) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)"
                proof -
                  have "¬is_Prim₀ (u \<lfloor>\<cdot>\<rfloor> w)"
                    using u w u' w' by (cases u, simp_all; cases w, simp_all)
                  hence "((t1 \<lfloor>\<cdot>\<rfloor> v1) \<star> (t2 \<lfloor>\<cdot>\<rfloor> v2)) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w)
                           = (t1 \<lfloor>\<cdot>\<rfloor> v1) \<lfloor>\<star>\<rfloor> ((t2 \<lfloor>\<cdot>\<rfloor> v2) \<lfloor>\<star>\<rfloor> (u \<lfloor>\<cdot>\<rfloor> w))"
                    by (cases "u \<lfloor>\<cdot>\<rfloor> w") simp_all
                  thus ?thesis by presburger
                qed
                finally show ?thesis by blast
              qed
            qed
          qed
          ultimately show ?thesis by blast
        qed
      qed
      moreover have "Src t = Trg u"
        using assms Src_Dom Trg_Dom Src_Cod Trg_Cod Nml_implies_Arr by metis
      ultimately show ?thesis using assms by simp
    qed

    text ‹
 The following function reduces a formal arrow to normal form.
 ›

    fun Nmlize :: "'a term ==> 'a term"   (‹\⌊_\⌋›)
    where "\<lfloor>\<langle>μ\<rangle>₀\<rfloor> = \<langle>μ\<rangle>₀"
        | "\<lfloor>\<langle>μ\<rangle>\<rfloor> = \<langle>μ\<rangle>"
        | "\<lfloor>t \<star> u\<rfloor> = \<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor>"
        | "\<lfloor>t \<cdot> u\<rfloor> = \<lfloor>t\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>u\<rfloor>"
        | "\<lfloor>\<l>[t]\<rfloor> = \<lfloor>t\<rfloor>"
        | "\<lfloor>\<l>^-1[t]\<rfloor> = \<lfloor>t\<rfloor>"
        | "\<lfloor>\<r>[t]\<rfloor> = \<lfloor>t\<rfloor>"
        | "\<lfloor>\<r>^-1[t]\<rfloor> = \<lfloor>t\<rfloor>"
        | "\<lfloor>\<a>[t, u, v]\<rfloor> = (\<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>"
        | "\<lfloor>\<a>^-1[t, u, v]\<rfloor> = \<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> (\<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>)"

    lemma Nml_Nmlize:
    assumes "Arr t"
    shows "Nml \<lfloor>t\<rfloor>" and "Src \<lfloor>t\<rfloor> = Src t" and "Trg \<lfloor>t\<rfloor> = Trg t"
    and "Dom \<lfloor>t\<rfloor> = \<lfloor>Dom t\<rfloor>" and "Cod \<lfloor>t\<rfloor> = \<lfloor>Cod t\<rfloor>"
    proof -
      have 0: "Arr t ==> Nml \<lfloor>t\<rfloor> ∧ Src \<lfloor>t\<rfloor> = Src t ∧ Trg \<lfloor>t\<rfloor> = Trg t ∧
                                     Dom \<lfloor>t\<rfloor> = \<lfloor>Dom t\<rfloor> ∧ Cod \<lfloor>t\<rfloor> = \<lfloor>Cod t\<rfloor>"
        using Nml_HcompNml Nml_VcompNml HcompNml_assoc
              Src_VcompNml Trg_VcompNml VSeq_implies_HPar
        apply (induct t)
                 apply auto
      proof -
        fix t
        assume 1: "Arr t"
        assume 2: "Nml \<lfloor>t\<rfloor>"
        assume 3: "Src \<lfloor>t\<rfloor> = Src t"
        assume 4: "Trg \<lfloor>t\<rfloor> = Trg t"
        assume 5: "Dom \<lfloor>t\<rfloor> = \<lfloor>Dom t\<rfloor>"
        assume 6: "Cod \<lfloor>t\<rfloor> = \<lfloor>Cod t\<rfloor>"
        have 7: "Nml \<lfloor>Dom t\<rfloor>"
          using 2 5 Nml_Dom by fastforce
        have 8: "Trg \<lfloor>t\<rfloor> = \<lfloor>Trg t\<rfloor>"
          using 1 2 4 Nml_Trg Obj_Trg
          by (metis Nml.elims(2) Nmlize.simps(1) Nmlize.simps(2) Obj.simps(3))
        have 9: "Nml \<lfloor>Cod t\<rfloor>"
          using 2 6 Nml_Cod by fastforce
        have 10: "Src \<lfloor>t\<rfloor> = \<lfloor>Src t\<rfloor>"
          using 1 2 3 Nml_Src Obj_Src
          by (metis Nml.elims(2) Nmlize.simps(1) Nmlize.simps(2) Obj.simps(3))
        show "\<lfloor>Dom t\<rfloor> = \<lfloor>Trg t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t\<rfloor>"
          using 2 5 7 8 Nml_implies_Arr Trg_Dom HcompNml_Trg_Nml by metis
        show "\<lfloor>Cod t\<rfloor> = \<lfloor>Trg t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t\<rfloor>"
          using 2 6 8 9 Nml_implies_Arr Trg_Cod HcompNml_Trg_Nml by metis
        show "\<lfloor>Dom t\<rfloor> = \<lfloor>Dom t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Src t\<rfloor>"
          using 2 5 7 10 Nml_implies_Arr Src_Dom HcompNml_Nml_Src by metis
        show "\<lfloor>Cod t\<rfloor> = \<lfloor>Cod t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Src t\<rfloor>"
          using 2 6 9 10 Nml_implies_Arr Src_Cod HcompNml_Nml_Src by metis
        next
        fix t1 t2 t3
        assume "Nml \<lfloor>t1\<rfloor>" and "Nml \<lfloor>t2\<rfloor>" and "Nml \<lfloor>t3\<rfloor>"
        assume "Src t1 = Trg t2" and "Src t2 = Trg t3"
        assume "Src \<lfloor>t1\<rfloor> = Trg t2" and "Src \<lfloor>t2\<rfloor> = Trg t3"
        assume "Trg \<lfloor>t1\<rfloor> = Trg t1" and "Trg \<lfloor>t2\<rfloor> = Trg t2" and "Trg \<lfloor>t3\<rfloor> = Trg t3"
        assume "Dom \<lfloor>t1\<rfloor> = \<lfloor>Dom t1\<rfloor>" and "Cod \<lfloor>t1\<rfloor> = \<lfloor>Cod t1\<rfloor>" and "Dom \<lfloor>t2\<rfloor> = \<lfloor>Dom t2\<rfloor>"
        and "Cod \<lfloor>t2\<rfloor> = \<lfloor>Cod t2\<rfloor>" and "Dom \<lfloor>t3\<rfloor> = \<lfloor>Dom t3\<rfloor>" and "Cod \<lfloor>t3\<rfloor> = \<lfloor>Cod t3\<rfloor>"
        show "\<lfloor>Dom t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t3\<rfloor> =
              (\<lfloor>Dom t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>Dom t3\<rfloor>"
          using Nml_Dom Nml_implies_Arr Src_Dom Trg_Dom
                HcompNml_assoc [of "\<lfloor>Dom t1\<rfloor>" "\<lfloor>Dom t2\<rfloor>" "\<lfloor>Dom t3\<rfloor>"]
                ‹Nml \<lfloor>t1\<rfloor>› ‹Nml \<lfloor>t2\<rfloor>› ‹Nml \<lfloor>t3\<rfloor>›
                ‹Dom \<lfloor>t1\<rfloor> = \<lfloor>Dom t1\<rfloor>› ‹Dom \<lfloor>t2\<rfloor> = \<lfloor>Dom t2\<rfloor>› ‹Dom \<lfloor>t3\<rfloor> = \<lfloor>Dom t3\<rfloor>›
                ‹Src \<lfloor>t1\<rfloor> = Trg t2› ‹Trg \<lfloor>t2\<rfloor> = Trg t2›
                ‹Src \<lfloor>t2\<rfloor> = Trg t3› ‹Trg \<lfloor>t3\<rfloor> = Trg t3›
          by metis
        show "\<lfloor>Cod t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t3\<rfloor> = (\<lfloor>Cod t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>Cod t3\<rfloor>"
          using Nml_Cod Nml_implies_Arr Src_Cod Trg_Cod
                HcompNml_assoc [of "\<lfloor>Cod t1\<rfloor>" "\<lfloor>Cod t2\<rfloor>" "\<lfloor>Cod t3\<rfloor>"]
                ‹Nml \<lfloor>t1\<rfloor>› ‹Nml \<lfloor>t2\<rfloor>› ‹Nml \<lfloor>t3\<rfloor>›
                ‹Cod \<lfloor>t1\<rfloor> = \<lfloor>Cod t1\<rfloor>› ‹Cod \<lfloor>t2\<rfloor> = \<lfloor>Cod t2\<rfloor>› ‹Cod \<lfloor>t3\<rfloor> = \<lfloor>Cod t3\<rfloor>›
                ‹Src \<lfloor>t1\<rfloor> = Trg t2› ‹Trg \<lfloor>t2\<rfloor> = Trg t2›
                ‹Src \<lfloor>t2\<rfloor> = Trg t3› ‹Trg \<lfloor>t3\<rfloor> = Trg t3›
          by metis
      qed
      show "Nml \<lfloor>t\<rfloor>" using assms 0 by blast
      show "Src \<lfloor>t\<rfloor> = Src t" using assms 0 by blast
      show "Trg \<lfloor>t\<rfloor> = Trg t" using assms 0 by blast
      show "Dom \<lfloor>t\<rfloor> = \<lfloor>Dom t\<rfloor>" using assms 0 by blast
      show "Cod \<lfloor>t\<rfloor> = \<lfloor>Cod t\<rfloor>" using assms 0 by blast
    qed

    lemma Nmlize_in_Hom [intro]:
    assumes "Arr t"
    shows "\<lfloor>t\<rfloor> ∈ HHom (Src t) (Trg t)" and "\<lfloor>t\<rfloor> ∈ VHom \<lfloor>Dom t\<rfloor> \<lfloor>Cod t\<rfloor>"
      using assms Nml_Nmlize Nml_implies_Arr by auto

    lemma Nmlize_Src:
    assumes "Arr t"
    shows "\<lfloor>Src t\<rfloor> = Src \<lfloor>t\<rfloor>" and "\<lfloor>Src t\<rfloor> = Src t"
    proof -
      have 1: "Obj (Src t)"
        using assms by simp
      obtain a where a: "obj a ∧ Src t = \<langle>a\<rangle>₀"
        using 1 by (cases "Src t", simp_all)
      show "\<lfloor>Src t\<rfloor> = Src t"
        using a by simp
      thus "\<lfloor>Src t\<rfloor> = Src \<lfloor>t\<rfloor>"
        using assms Nmlize_in_Hom by simp
    qed

    lemma Nmlize_Trg:
    assumes "Arr t"
    shows "\<lfloor>Trg t\<rfloor> = Trg \<lfloor>t\<rfloor>" and "\<lfloor>Trg t\<rfloor> = Trg t"
    proof -
      have 1: "Obj (Trg t)"
        using assms by simp
      obtain a where a: "obj a ∧ Trg t = \<langle>a\<rangle>₀"
        using 1 by (cases "Trg t", simp_all)
      show "\<lfloor>Trg t\<rfloor> = Trg t"
        using a by simp
      thus "\<lfloor>Trg t\<rfloor> = Trg \<lfloor>t\<rfloor>"
        using assms Nmlize_in_Hom by simp
    qed

    lemma Nmlize_Dom:
    assumes "Arr t"
    shows "\<lfloor>Dom t\<rfloor> = Dom \<lfloor>t\<rfloor>"
      using assms Nmlize_in_Hom by simp

    lemma Nmlize_Cod:
    assumes "Arr t"
    shows "\<lfloor>Cod t\<rfloor> = Cod \<lfloor>t\<rfloor>"
      using assms Nmlize_in_Hom by simp

    lemma Ide_Nmlize_Ide:
    assumes "Ide t"
    shows "Ide \<lfloor>t\<rfloor>"
    proof -
      have "Ide t ==> Ide \<lfloor>t\<rfloor>"
        using Ide_HcompNml Nml_Nmlize
        by (induct t, simp_all)
      thus ?thesis using assms by blast
    qed

    lemma Ide_Nmlize_Can:
    assumes "Can t"
    shows "Ide \<lfloor>t\<rfloor>"
    proof -
      have "Can t ==> Ide \<lfloor>t\<rfloor>"
        using Can_implies_Arr Ide_HcompNml Nml_Nmlize Ide_VcompNml Nml_HcompNml
        apply (induct t)
          apply (auto simp add: Dom_Ide Cod_Ide)
        by (metis Ide_VcompNml)
      thus ?thesis using assms by blast
    qed

    lemma Can_Nmlize_Can:
    assumes "Can t"
    shows "Can \<lfloor>t\<rfloor>"
      using assms Ide_Nmlize_Can Ide_implies_Can by auto

    lemma Nmlize_Nml [simp]:
    assumes "Nml t"
    shows "\<lfloor>t\<rfloor> = t"
    proof -
      have "Nml t ==> \<lfloor>t\<rfloor> = t"
        apply (induct t, simp_all)
        using HcompNml_Prim Nml_HcompD by metis
      thus ?thesis using assms by blast
    qed

    lemma Nmlize_Nmlize [simp]:
    assumes "Arr t"
    shows "\<lfloor>\<lfloor>t\<rfloor>\<rfloor> = \<lfloor>t\<rfloor>"
      using assms Nml_Nmlize Nmlize_Nml by blast

    lemma Nmlize_Hcomp:
    assumes "Arr t" and "Arr u"
    shows "\<lfloor>t \<star> u\<rfloor> = \<lfloor>\<lfloor>t\<rfloor> \<star> \<lfloor>u\<rfloor>\<rfloor>"
      using assms Nmlize_Nmlize by simp

    lemma Nmlize_Hcomp_Obj_Arr [simp]:
    assumes "Arr u"
    shows "\<lfloor>\<langle>b\<rangle>₀ \<star> u\<rfloor> = \<lfloor>u\<rfloor>"
      using assms by simp

    lemma Nmlize_Hcomp_Arr_Obj [simp]:
    assumes "Arr t" and "Src t = \<langle>a\<rangle>₀"
    shows "\<lfloor>t \<star> \<langle>a\<rangle>₀\<rfloor> = \<lfloor>t\<rfloor>"
      using assms HcompNml_Nml_Src Nmlize_in_Hom by simp

    lemma Nmlize_Hcomp_Prim_Arr [simp]:
    assumes "Arr u" and "¬ is_Prim₀ \<lfloor>u\<rfloor>"
    shows "\<lfloor>\<langle>μ\<rangle> \<star> u\<rfloor> = \<langle>μ\<rangle> \<star> \<lfloor>u\<rfloor>"
      using assms by simp

    lemma Nmlize_Hcomp_Hcomp:
    assumes "Arr t" and "Arr u" and "Arr v" and "Src t = Trg u" and "Src u = Trg v"
    shows "\<lfloor>(t \<star> u) \<star> v\<rfloor> = \<lfloor>\<lfloor>t\<rfloor> \<star> (\<lfloor>u\<rfloor> \<star> \<lfloor>v\<rfloor>)\<rfloor>"
      using assms Nml_Nmlize Nmlize_Nmlize by (simp add: HcompNml_assoc)

    lemma Nmlize_Hcomp_Hcomp':
    assumes "Arr t" and "Arr u" and "Arr v" and "Src t = Trg u" and "Src u = Trg v"
    shows "\<lfloor>t \<star> u \<star> v\<rfloor> = \<lfloor>\<lfloor>t\<rfloor> \<star> \<lfloor>u\<rfloor> \<star> \<lfloor>v\<rfloor>\<rfloor>"
      using assms Nml_Nmlize Nmlize_Nmlize by (simp add: HcompNml_assoc)

    lemma Nmlize_Vcomp_Cod_Arr:
    assumes "Arr t"
    shows "\<lfloor>Cod t \<cdot> t\<rfloor> = \<lfloor>t\<rfloor>"
    proof -
      have "Arr t ==> \<lfloor>Cod t \<cdot> t\<rfloor> = \<lfloor>t\<rfloor>"
      proof (induct t, simp_all)
        show "∧x. arr x ==> cod x ⋅ x = x"
          using comp_cod_arr by blast
        fix t1 t2
        show "∧t1 t2. \<lfloor>Cod t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t1\<rfloor> = \<lfloor>t1\<rfloor> ==> \<lfloor>Cod t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor> = \<lfloor>t2\<rfloor> ==> HSeq t1 t2 ==>
                      (\<lfloor>Cod t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t2\<rfloor>) \<lfloor>\<cdot>\<rfloor> (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) = \<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>"
          using VcompNml_HcompNml Ide_Cod Nml_Nmlize Nmlize_in_Hom
          by simp
        show "\<lfloor>Cod t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t1\<rfloor> = \<lfloor>t1\<rfloor> ==> \<lfloor>Cod t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor> = \<lfloor>t2\<rfloor> ==> VSeq t1 t2 ==>
              \<lfloor>Cod t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor> = \<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor>"
          using VcompNml_assoc [of "\<lfloor>Cod t1\<rfloor>" "\<lfloor>t1\<rfloor>" "\<lfloor>t2\<rfloor>"] Ide_Cod
                Nml_Nmlize
          by simp
        next
        show "∧t. \<lfloor>Cod t\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t\<rfloor> = \<lfloor>t\<rfloor> ==> Arr t ==> (\<lfloor>Trg t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t\<rfloor>) \<lfloor>\<cdot>\<rfloor> \<lfloor>t\<rfloor> = \<lfloor>t\<rfloor>"
          by (metis Arr.simps(6) Cod.simps(6) Nmlize.simps(3) Nmlize.simps(6)
              Nmlize_Cod)
        show "∧t. \<lfloor>Cod t\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t\<rfloor> = \<lfloor>t\<rfloor> ==> Arr t ==> (\<lfloor>Cod t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Src t\<rfloor>) \<lfloor>\<cdot>\<rfloor> \<lfloor>t\<rfloor> = \<lfloor>t\<rfloor>"
          by (simp add: Nml_Nmlize(1) Nml_Nmlize(2) Nmlize_Src(2) HcompNml_Nml_Obj)
        show "∧t1 t2 t3. \<lfloor>Cod t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t1\<rfloor> = \<lfloor>t1\<rfloor> ==> \<lfloor>Cod t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor> = \<lfloor>t2\<rfloor> ==>
                          \<lfloor>Cod t3\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t3\<rfloor> = \<lfloor>t3\<rfloor> ==>
                          Arr t1 ∧ Arr t2 ∧ Arr t3 ∧ Src t1 = Trg t2 ∧ Src t2 = Trg t3 ==>
                         (\<lfloor>Cod t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t3\<rfloor>) \<lfloor>\<cdot>\<rfloor> ((\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>) =
                         (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>"
          using VcompNml_HcompNml Ide_Cod HcompNml_in_Hom Nml_HcompNml
                Nml_Nmlize Nmlize_in_Hom HcompNml_assoc
          by simp
        show "∧t1 t2 t3. \<lfloor>Cod t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t1\<rfloor> = \<lfloor>t1\<rfloor> ==> \<lfloor>Cod t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor> = \<lfloor>t2\<rfloor> ==>
                          \<lfloor>Cod t3\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t3\<rfloor> = \<lfloor>t3\<rfloor> ==>
                          Arr t1 ∧ Arr t2 ∧ Arr t3 ∧ Src t1 = Trg t2 ∧ Src t2 = Trg t3 ==>
                          ((\<lfloor>Cod t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Cod t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>Cod t3\<rfloor>) \<lfloor>\<cdot>\<rfloor> (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>) =
                          \<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>"
          using VcompNml_HcompNml Ide_Cod HcompNml_in_Hom Nml_HcompNml
                Nml_Nmlize Nmlize_in_Hom HcompNml_assoc
          by simp
      qed
      thus ?thesis using assms by blast
    qed

    lemma Nmlize_Vcomp_Arr_Dom:
    assumes "Arr t"
    shows "\<lfloor>t \<cdot> Dom t\<rfloor> = \<lfloor>t\<rfloor>"
    proof -
      have "Arr t ==> \<lfloor>t \<cdot> Dom t\<rfloor> = \<lfloor>t\<rfloor>"
      proof (induct t, simp_all)
        show "∧x. arr x ==> x ⋅ local.dom x = x"
          using comp_arr_dom by blast
        fix t1 t2
        show "\<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t1\<rfloor> = \<lfloor>t1\<rfloor> ==> \<lfloor>t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t2\<rfloor> = \<lfloor>t2\<rfloor> ==> HSeq t1 t2 ==>
              (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<cdot>\<rfloor> (\<lfloor>Dom t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t2\<rfloor>) = \<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>"
          using VcompNml_HcompNml Ide_Dom HcompNml_in_Hom Nml_HcompNml
                Nml_Nmlize Nmlize_in_Hom HcompNml_assoc
          by simp
        show "\<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Cod t2\<rfloor> = \<lfloor>t1\<rfloor> ==> \<lfloor>t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t2\<rfloor> = \<lfloor>t2\<rfloor> ==> VSeq t1 t2 ==>
              (\<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t2\<rfloor> = \<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>t2\<rfloor>"
          using VcompNml_assoc [of "\<lfloor>t1\<rfloor>" "\<lfloor>t2\<rfloor>" "\<lfloor>Dom t2\<rfloor>"] Ide_Dom Nml_Nmlize
          by simp
        next
        show "∧t. \<lfloor>t\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t\<rfloor> = \<lfloor>t\<rfloor> ==> Arr t ==> \<lfloor>t\<rfloor> \<lfloor>\<cdot>\<rfloor> (\<lfloor>Trg t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t\<rfloor>) = \<lfloor>t\<rfloor>"
          by (simp add: Nml_Nmlize(1) Nml_Nmlize(3) Nmlize_Trg(2)
              HcompNml_Obj_Nml bicategorical_language.Ide_Dom
              bicategorical_language_axioms)
        show "∧t. \<lfloor>t\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t\<rfloor> = \<lfloor>t\<rfloor> ==> Arr t ==> \<lfloor>t\<rfloor> \<lfloor>\<cdot>\<rfloor> (\<lfloor>Dom t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Src t\<rfloor>) = \<lfloor>t\<rfloor>"
          by (simp add: Nml_Nmlize(1) Nml_Nmlize(2) Nmlize_Src(2) HcompNml_Nml_Obj)
        show "∧t1 t2 t3. \<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t1\<rfloor> = \<lfloor>t1\<rfloor> ==> \<lfloor>t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t2\<rfloor> = \<lfloor>t2\<rfloor> ==>
                          \<lfloor>t3\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t3\<rfloor> = \<lfloor>t3\<rfloor> ==>
                          Arr t1 ∧ Arr t2 ∧ Arr t3 ∧ Src t1 = Trg t2 ∧ Src t2 = Trg t3 ==>
                          ((\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>) \<lfloor>\<cdot>\<rfloor> ((\<lfloor>Dom t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>Dom t3\<rfloor>) =
                          (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>"
          using VcompNml_HcompNml Ide_Dom HcompNml_in_Hom Nml_HcompNml
                Nml_Nmlize Nmlize_in_Hom HcompNml_assoc
          by simp
        show "∧t1 t2 t3. \<lfloor>t1\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t1\<rfloor> = \<lfloor>t1\<rfloor> ==> \<lfloor>t2\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t2\<rfloor> = \<lfloor>t2\<rfloor> ==>
                          \<lfloor>t3\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t3\<rfloor> = \<lfloor>t3\<rfloor> ==>
                          Arr t1 ∧ Arr t2 ∧ Arr t3 ∧ Src t1 = Trg t2 ∧ Src t2 = Trg t3 ==>
                          (\<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>) \<lfloor>\<cdot>\<rfloor> (\<lfloor>Dom t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom t3\<rfloor>) =
                          \<lfloor>t1\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t2\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>t3\<rfloor>"
          using VcompNml_HcompNml Ide_Dom HcompNml_in_Hom Nml_HcompNml
                Nml_Nmlize Nmlize_in_Hom HcompNml_assoc
          by simp
      qed
      thus ?thesis using assms by blast
    qed

    lemma Nmlize_Inv:
    assumes "Can t"
    shows "\<lfloor>Inv t\<rfloor> = Inv \<lfloor>t\<rfloor>"
    proof -
      have "Can t ==> \<lfloor>Inv t\<rfloor> = Inv \<lfloor>t\<rfloor>"
      proof (induct t, simp_all)
        fix u v
        assume I1: "\<lfloor>Inv u\<rfloor> = Inv \<lfloor>u\<rfloor>"
        assume I2: "\<lfloor>Inv v\<rfloor> = Inv \<lfloor>v\<rfloor>"
        show "Can u ∧ Can v ∧ Src u = Trg v ==> Inv \<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> Inv \<lfloor>v\<rfloor> = Inv (\<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>)"
          using Inv_HcompNml Nml_Nmlize Can_implies_Arr Can_Nmlize_Can
                I1 I2
          by simp
        show "Can u ∧ Can v ∧ Dom u = Cod v ==> Inv \<lfloor>v\<rfloor> \<lfloor>\<cdot>\<rfloor> Inv \<lfloor>u\<rfloor> = Inv (\<lfloor>u\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>v\<rfloor>)"
          using Inv_VcompNml Nml_Nmlize Can_implies_Arr Nmlize_in_Hom Can_Nmlize_Can
                I1 I2
          by simp
        fix w
        assume I3: "\<lfloor>Inv w\<rfloor> = Inv \<lfloor>w\<rfloor>"
        assume uvw: "Can u ∧ Can v ∧ Can w ∧ Src u = Trg v ∧ Src v = Trg w"
        show "Inv \<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> (Inv \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> Inv \<lfloor>w\<rfloor>) = Inv ((\<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>)"
          using uvw I1 I2 I3
                Inv_HcompNml Nml_Nmlize Can_implies_Arr Can_Nmlize_Can
                Nml_HcompNml Can_HcompNml HcompNml_assoc
          by simp
        show "(Inv \<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> Inv \<lfloor>v\<rfloor>) \<lfloor>\<star>\<rfloor> Inv \<lfloor>w\<rfloor> = Inv (\<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> (\<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>))"
          using uvw I1 I2 I3
                Inv_HcompNml Nml_Nmlize Can_implies_Arr Can_Nmlize_Can
                Nml_HcompNml Can_HcompNml HcompNml_assoc Can_Inv
          by simp
      qed
      thus ?thesis using assms by blast
    qed

    subsection "Reductions"

    text ‹
      Function ‹red› defined below takes a formal identity @{term t} to a canonical arrow
      ‹f\<down> ∈ Hom f \<lfloor>f\<rfloor>›. The auxiliary function ‹red2› takes a pair @{term "(f, g)"}
      of normalized formal identities and produces a canonical arrow
      ‹f \<Down> g ∈ Hom (f \<star> g) \<lfloor>f \<star> g\<rfloor>›.
    ›

    fun red2 (infixr ‹\<Down>› 53)
    where "\<langle>b\<rangle>₀ \<Down> u = \<l>[u]"
        | "\<langle>f\<rangle> \<Down> \<langle>a\<rangle>₀ = \<r>[\<langle>f\<rangle>]"
        | "\<langle>f\<rangle> \<Down> u = \<langle>f\<rangle> \<star> u"
        | "(t \<star> u) \<Down> \<langle>a\<rangle>₀ = \<r>[t \<star> u]"
        | "(t \<star> u) \<Down> v = (t \<Down> \<lfloor>u \<star> v\<rfloor>) \<cdot> (t \<star> (u \<Down> v)) \<cdot> \<a>[t, u, v]"
        | "t \<Down> u = undefined"

    fun red (‹_\<down>› [56] 56)
    where "\<langle>f\<rangle>₀\<down> = \<langle>f\<rangle>₀"
        | "\<langle>f\<rangle>\<down> = \<langle>f\<rangle>"
        | "(t \<star> u)\<down> = (if Nml (t \<star> u) then t \<star> u else (\<lfloor>t\<rfloor> \<Down> \<lfloor>u\<rfloor>) \<cdot> (t\<down> \<star> u\<down>))"
        | "t\<down> = undefined"

    lemma red_Nml [simp]:
    assumes "Nml a"
    shows "a\<down> = a"
      using assms by (cases a, simp_all)

    lemma red2_Nml:
    assumes "Nml (a \<star> b)"
    shows "a \<Down> b = a \<star> b"
    proof -
      have a: "a = \<langle>un_Prim a\<rangle>"
        using assms Nml_HcompD by metis
      have b: "Nml b ∧ ¬ is_Prim₀ b"
        using assms Nml_HcompD by metis
      show ?thesis using a b
        apply (cases b)
          apply simp_all
         apply (metis red2.simps(3))
        by (metis red2.simps(4))
    qed

    lemma Can_red2:
    assumes "Ide a" and "Nml a" and "Ide b" and "Nml b" and "Src a = Trg b"
    shows "Can (a \<Down> b)"
    and "a \<Down> b ∈ VHom (a \<star> b) \<lfloor>a \<star> b\<rfloor>"
    proof -
      have 0: "∧b. [ Ide a ∧ Nml a; Ide b ∧ Nml b; Src a = Trg b ] ==>
                     Can (a \<Down> b) ∧ a \<Down> b ∈ VHom (a \<star> b) \<lfloor>a \<star> b\<rfloor>"
      proof (induct a, simp_all add: HcompNml_Nml_Src HcompNml_Trg_Nml)
        fix x b
        show "Ide b ∧ Nml b ==> Can (Trg b \<Down> b) ∧ Arr (Trg b \<Down> b) ∧
                                 Dom (Trg b \<Down> b) = Trg b \<star> b ∧ Cod (Trg b \<Down> b) = b"
          using Ide_implies_Can Ide_in_Hom Nmlize_Nml
          apply (cases b, simp_all)
        proof -
          fix u v
          assume uv: "Ide u ∧ Ide v ∧ Src u = Trg v ∧ Nml (u \<star> v)"
          show "Can (Trg u \<Down> (u \<star> v)) ∧ Arr (Trg u \<Down> (u \<star> v)) ∧
                Dom (Trg u \<Down> (u \<star> v)) = Trg u \<star> u \<star> v ∧
                Cod (Trg u \<Down> (u \<star> v)) = u \<star> v"
            using uv Ide_implies_Can Can_implies_Arr Ide_in_Hom
            by (cases u, simp_all)
        qed
        show "ide x ∧ arr x ==> Ide b ∧ Nml b ==> \<langle>src x\<rangle>₀ = Trg b ==>
              Can (\<langle>x\<rangle> \<Down> b) ∧ Arr (\<langle>x\<rangle> \<Down> b) ∧ Dom (\<langle>x\<rangle> \<Down> b) = \<langle>x\<rangle> \<star> b ∧ Cod (\<langle>x\<rangle> \<Down> b) =
              \<langle>x\<rangle> \<lfloor>\<star>\<rfloor> b"
            using Ide_implies_Can Can_implies_Arr Nmlize_Nml Ide_in_Hom
            by (cases b, simp_all)
        next
        fix u v w
        assume uv: "Ide u ∧ Ide v ∧ Src u = Trg v ∧ Nml (u \<star> v)"
        assume vw: "Src v = Trg w"
        assume w: "Ide w ∧ Nml w"
        assume I1: "∧w. [ Nml u; Ide w ∧ Nml w; Trg v = Trg w ] ==>
                          Can (u \<Down> w) ∧ Arr (u \<Down> w) ∧
                          Dom (u \<Down> w) = u \<star> w ∧ Cod (u \<Down> w) = u \<lfloor>\<star>\<rfloor> w"
        assume I2: "∧x. [ Nml v; Ide x ∧ Nml x; Trg w = Trg x ] ==>
                          Can (v \<Down> x) ∧ Arr (v \<Down> x) ∧
                          Dom (v \<Down> x) = v \<star> x ∧ Cod (v \<Down> x) = v \<lfloor>\<star>\<rfloor> x"
        show "Can ((u \<star> v) \<Down> w) ∧ Arr ((u \<star> v) \<Down> w) ∧
              Dom ((u \<star> v) \<Down> w) = (u \<star> v) \<star> w ∧
              Cod ((u \<star> v) \<Down> w) = (\<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>) \<lfloor>\<star>\<rfloor> w"
        proof -
          have u: "Nml u ∧ Ide u"
            using uv Nml_HcompD by blast
          have v: "Nml v ∧ Ide v"
            using uv Nml_HcompD by blast
          have "is_Prim₀ w ==> ?thesis"
          proof -
            assume 1: "is_Prim₀ w"
            have 2: "(u \<star> v) \<Down> w = \<r>[u \<star> v]"
              using 1 by (cases w, simp_all)
            have 3: "Can (u \<Down> v) ∧ Arr (u \<Down> v) ∧ Dom (u \<Down> v) = u \<star> v ∧ Cod (u \<Down> v) = u \<star> v"
              using u v uv 1 2 I1 Nmlize_Nml Nmlize.simps(3) by metis
            hence 4: "VSeq (u \<Down> v) \<r>[u \<star> v]"
              using uv
              by (metis (mono_tags, lifting) Arr.simps(7) Cod.simps(3) Cod.simps(7)
                  Nml_implies_Arr Ide_in_Hom(2) mem_Collect_eq)
            have "Can ((u \<star> v) \<Down> w)"
              using 1 2 3 4 uv by (simp add: Ide_implies_Can)
            moreover have "Dom ((u \<star> v) \<Down> w) = (u \<star> v) \<star> w"
              using 1 2 3 4 u v w uv vw I1 Ide_in_Hom Nml_HcompNml Ide_in_Hom
              apply (cases w) by simp_all
            moreover have "Cod ((u \<star> v) \<Down> w) = \<lfloor>(u \<star> v) \<star> w\<rfloor>"
              using 1 2 3 4 uv
              using Nmlize_Nml apply (cases w, simp_all)
              by (metis Nmlize.simps(3) Nmlize_Nml HcompNml.simps(3))
            ultimately show ?thesis using w Can_implies_Arr by (simp add: 1 uv)
          qed
          moreover have "¬ is_Prim₀ w ==> ?thesis"
          proof -
            assume 1: "¬ is_Prim₀ w"
            have 2: "(u \<star> v) \<Down> w = (u \<Down> \<lfloor>v \<star> w\<rfloor>) \<cdot> (u \<star> v \<Down> w) \<cdot> \<a>[u, v, w]"
              using 1 u v uv w by (cases w; simp)
            have 3: "Can (u \<Down> \<lfloor>v \<star> w\<rfloor>) ∧ Dom (u \<Down> \<lfloor>v \<star> w\<rfloor>) = u \<star> \<lfloor>v \<star> w\<rfloor> ∧
                                         Cod (u \<Down> \<lfloor>v \<star> w\<rfloor>) = \<lfloor>u \<star> (v \<star> w)\<rfloor>"
            proof -
              have "Can (u \<Down> \<lfloor>v \<star> w\<rfloor>) ∧ Dom (u \<Down> \<lfloor>v \<star> w\<rfloor>) = u \<star> \<lfloor>v \<star> w\<rfloor> ∧
                                        Cod (u \<Down> \<lfloor>v \<star> w\<rfloor>) = u \<lfloor>\<star>\<rfloor> \<lfloor>v \<star> w\<rfloor>"
                using w uv Ide_HcompNml Nml_HcompNml(1)
                apply (cases u, simp_all)
                using u v vw I1 Nmlize_in_Hom(1) [of "v \<star> w"] Nml_Nmlize Ide_Nmlize_Ide
                by simp
              moreover have "u \<lfloor>\<star>\<rfloor> \<lfloor>v \<star> w\<rfloor> = \<lfloor>u \<star> (v \<star> w)\<rfloor>"
                using uv u w Nmlize_Hcomp Nmlize_Nmlize Nml_implies_Arr by simp
              ultimately show ?thesis by presburger
            qed
            have 4: "Can (v \<Down> w) ∧ Dom (v \<Down> w) = v \<star> w ∧ Cod (v \<Down> w) = \<lfloor>v \<star> w\<rfloor>"
              using v w vw 1 2 I2 by simp
            hence 5: "Src (v \<Down> w) = Src w ∧ Trg (v \<Down> w) = Trg v"
              using Src_Dom Trg_Dom Can_implies_Arr by fastforce
            have "Can (u \<star> (v \<Down> w)) ∧ Dom (u \<star> (v \<Down> w)) = u \<star> (v \<star> w) ∧
                                       Cod (u \<star> (v \<Down> w)) = u \<star> \<lfloor>v \<star> w\<rfloor>"
              using u uv vw 4 5 Ide_implies_Can Ide_in_Hom by simp
            moreover have "\<lfloor>u \<star> \<lfloor>v \<star> w\<rfloor>\<rfloor> = \<lfloor>u \<star> v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>"
            proof -
              have "\<lfloor>u \<star> \<lfloor>v \<star> w\<rfloor>\<rfloor> = u \<lfloor>\<star>\<rfloor> (v \<lfloor>\<star>\<rfloor> w)"
                using u v w 4
                by (metis Ide_Dom Can_implies_Arr Ide_implies_Arr
                    Nml_Nmlize(1) Nmlize.simps(3) Nmlize_Nml)
              also have "... = (u \<lfloor>\<star>\<rfloor> v) \<lfloor>\<star>\<rfloor> w"
                using u v w uv vw HcompNml_assoc by metis
              also have "... = \<lfloor>u \<star> v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>"
                using u v w by (metis Nmlize.simps(3) Nmlize_Nml)
              finally show ?thesis by blast
            qed
            moreover have "Can \<a>[u, v, w] ∧ Dom \<a>[u, v, w] = (u \<star> v) \<star> w ∧
                                            Cod \<a>[u, v, w] = u \<star> (v \<star> w)"
              using uv vw w Ide_implies_Can Ide_in_Hom by auto
            ultimately show ?thesis
              using uv w 2 3 4 Nml_implies_Arr Nmlize_Nmlize Ide_implies_Can
                    Nmlize_Nml Ide_Dom Can_implies_Arr
              by (metis Can.simps(4) Cod.simps(4) Dom.simps(4) Nmlize.simps(3))
          qed
          ultimately show ?thesis by blast
        qed
      qed
      show "Can (a \<Down> b)" using assms 0 by blast
      show "a \<Down> b ∈ VHom (a \<star> b) \<lfloor>a \<star> b\<rfloor>" using 0 assms by blast
    qed

    lemma red2_in_Hom [intro]:
    assumes "Ide u" and "Nml u" and "Ide v" and "Nml v" and "Src u = Trg v"
    shows "u \<Down> v ∈ HHom (Src v) (Trg u)" and "u \<Down> v ∈ VHom (u \<star> v) \<lfloor>u \<star> v\<rfloor>"
    proof -
      show 1: "u \<Down> v ∈ VHom (u \<star> v) \<lfloor>u \<star> v\<rfloor>"
        using assms Can_red2 Can_implies_Arr by simp
      show "u \<Down> v ∈ HHom (Src v) (Trg u)"
        using assms 1 Src_Dom [of "u \<Down> v"] Trg_Dom [of "u \<Down> v"] Can_red2 Can_implies_Arr by simp
    qed

    lemma red2_simps [simp]:
    assumes "Ide u" and "Nml u" and "Ide v" and "Nml v" and "Src u = Trg v"
    shows "Src (u \<Down> v) = Src v" and "Trg (u \<Down> v) = Trg u"
    and "Dom (u \<Down> v) = u \<star> v" and "Cod (u \<Down> v) = \<lfloor>u \<star> v\<rfloor>"
      using assms red2_in_Hom by auto

    lemma Can_red:
    assumes "Ide u"
    shows "Can (u\<down>)" and "u\<down> ∈ VHom u \<lfloor>u\<rfloor>"
    proof -
      have 0: "Ide u ==> Can (u\<down>) ∧ u\<down> ∈ VHom u \<lfloor>u\<rfloor>"
      proof (induct u, simp_all add: Dom_Ide Cod_Ide)
        fix v w
        assume v: "Can (v\<down>) ∧ Arr (v\<down>) ∧ Dom (v\<down>) = v ∧ Cod (v\<down>) = \<lfloor>v\<rfloor>"
        assume w: "Can (w\<down>) ∧ Arr (w\<down>) ∧ Dom (w\<down>) = w ∧ Cod (w\<down>) = \<lfloor>w\<rfloor>"
        assume vw: "Ide v ∧ Ide w ∧ Src v = Trg w"
        show "(Nml (v \<star> w) ⟶
                 Can v ∧ Can w ∧ v \<star> w = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>) ∧
              (¬ Nml (v \<star> w) ⟶
                 Can (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>) ∧
                 Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Arr (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>) ∧
                 Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Cod (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>)"
        proof
          show "Nml (v \<star> w) ⟶
                  Can v ∧ Can w ∧ v \<star> w = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>"
            using vw Nml_HcompD Ide_implies_Can Dom_Inv VcompNml_Ide_Nml Inv_Ide
                  Nmlize.simps(3) Nmlize_Nml
            by metis
          show "¬ Nml (v \<star> w) ⟶
                  Can (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>) ∧
                  Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Arr (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>) ∧
                  Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Cod (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>"
          proof
            assume 1: "¬ Nml (v \<star> w)"
            have "Can (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>)"
              using v w vw Can_red2 Nml_Nmlize Ide_Nmlize_Ide Nml_HcompNml Ide_HcompNml
              by simp
            moreover have "Src (v\<down>) = Trg (w\<down>)"
              using v w vw Src_Dom Trg_Dom by metis
            moreover have "Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Cod (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>"
              using v w vw Can_red2 Nml_Nmlize Ide_Nmlize_Ide by simp
            ultimately show "Can (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧ Src (v\<down>) = Trg (w\<down>) ∧
                             Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧ Arr (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) ∧
                             Src (v\<down>) = Trg (w\<down>) ∧ Dom (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<star> \<lfloor>w\<rfloor> ∧
                             Cod (\<lfloor>v\<rfloor> \<Down> \<lfloor>w\<rfloor>) = \<lfloor>v\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>w\<rfloor>"
              using Can_implies_Arr by blast
          qed
        qed
      qed
      show "Can (u\<down>)" using assms 0 by blast
      show "u\<down> ∈ VHom u \<lfloor>u\<rfloor>" using assms 0 by blast
    qed

    lemma red_in_Hom [intro]:
    assumes "Ide t"
    shows "t\<down> ∈ HHom (Src t) (Trg t)" and "t\<down> ∈ VHom t \<lfloor>t\<rfloor>"
    proof -
      show 1: "t\<down> ∈ VHom t \<lfloor>t\<rfloor>"
        using assms Can_red Can_implies_Arr by simp
      show "t\<down> ∈ HHom (Src t) (Trg t)"
        using assms 1 Src_Dom [of "t\<down>"] Trg_Dom [of "t\<down>"] Can_red Can_implies_Arr by simp
    qed

    lemma red_simps [simp]:
    assumes "Ide t"
    shows "Src (t\<down>) = Src t" and "Trg (t\<down>) = Trg t"
    and "Dom (t\<down>) = t" and "Cod (t\<down>) = \<lfloor>t\<rfloor>"
      using assms red_in_Hom by auto

    lemma red_Src:
    assumes "Ide t"
    shows "Src t\<down> = Src t"
      using assms is_Prim0_Src [of t]
      by (cases "Src t", simp_all)

    lemma red_Trg:
    assumes "Ide t"
    shows "Trg t\<down> = Trg t"
      using assms is_Prim0_Trg [of t]
      by (cases "Trg t", simp_all)

    lemma Nmlize_red [simp]:
    assumes "Ide t"
    shows "\<lfloor>t\<down>\<rfloor> = \<lfloor>t\<rfloor>"
      using assms Can_red Ide_Nmlize_Can Nmlize_in_Hom Ide_in_Hom by fastforce

    lemma Nmlize_red2 [simp]:
    assumes "Ide t" and "Ide u" and "Nml t" and "Nml u" and "Src t = Trg u"
    shows "\<lfloor>t \<Down> u\<rfloor> = \<lfloor>t \<star> u\<rfloor>"
      using assms Can_red2 Ide_Nmlize_Can Nmlize_in_Hom [of "t \<Down> u"] red2_in_Hom Ide_in_Hom
      by simp

  end

  subsection "Evaluation"

  text ‹
    The following locale is concerned with the evaluation of terms of the bicategorical
    language determined by ‹C›, ‹src_C›, and ‹trg_C› in a bicategory ‹(V, H, a, i, src, trg)›,
    given a source and target-preserving functor from ‹C› to ‹V›.
  ›

  locale evaluation_map =
    C: horizontal_homs C src_C trg_C +
    bicategorical_language C src_C trg_C +
    bicategory V H a i src trg +
    E: "functor" C V E
    for C :: "'c comp" (infixr ‹⋅_C› 55)
    and src_C :: "'c ==> 'c"
    and trg_C :: "'c ==> 'c"
    and V :: "'b comp" (infixr ‹⋅› 55)
    and H :: "'b comp" (infixr ‹⋆› 53)
    and a :: "'b ==> 'b ==> 'b ==> 'b" (‹a[_, _, _]›)
    and i :: "'b ==> 'b" (‹i[_]›)
    and src :: "'b ==> 'b"
    and trg :: "'b ==> 'b"
    and E :: "'c ==> 'b" +
    assumes preserves_src: "E (src_C x) = src (E x)"
    and preserves_trg: "E (trg_C x) = trg (E x)"
  begin

    (* TODO: Figure out why this notation has to be reinstated. *)
    notation Nmlize (‹\<lfloor>_\<rfloor>›)
    notation HcompNml (infixr ‹\<lfloor>\<star>\<rfloor>› 53)
    notation VcompNml (infixr ‹\<lfloor>\<cdot>\<rfloor>› 55)
    notation red (‹_\<down>› [56] 56)
    notation red2 (infixr ‹\<Down>› 53)

    primrec eval :: "'c term ==> 'b" (‹{_}›)
    where "{\<langle>f\<rangle>₀} = E f"
        | "{\<langle>f\<rangle>} = E f"
        | "{t \<star> u} = {t} ⋆ {u}"
        | "{t \<cdot> u} = {t} ⋅ {u}"
        | "{\<l>[t]} = l {t}"
        | "{\<l>^-1[t]} = l'.map {t}"
        | "{\<r>[t]} = r {t}"
        | "{\<r>^-1[t]} = r'.map {t}"
        | "{\<a>[t, u, v]} = α ({t}, {u}, {v})"
        | "{\<a>^-1[t, u, v]} = α'.map ({t}, {u}, {v})"

    lemma preserves_obj:
    assumes "C.obj a"
    shows "obj (E a)"
    proof (unfold obj_def)
      show "arr (E a) ∧ src (E a) = E a"
      proof
        show "arr (E a)" using assms C.obj_simps by simp
        have "src (E a) = E (src_C a)"
           using assms preserves_src by metis
        also have "... = E a"
           using assms C.obj_simps by simp
        finally show "src (E a) = E a" by simp
      qed
    qed

    lemma eval_in_hom':
    shows "Arr t ==> «{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬"
    proof (induct t)
      show "∧x. Arr \<langle>x\<rangle>₀ ==>
                 «{\<langle>x\<rangle>₀} : {Src \<langle>x\<rangle>₀} → {Trg \<langle>x\<rangle>₀}¬ ∧ «{\<langle>x\<rangle>₀} : {Dom \<langle>x\<rangle>₀} ==> {Cod \<langle>x\<rangle>₀}¬"
        apply (simp add: preserves_src preserves_trg)
        using preserves_src preserves_trg C.objE
        by (metis (full_types) C.obj_def' E.preserves_arr E.preserves_ide in_hhom_def
            ide_in_hom(2))
      show "∧x. Arr \<langle>x\<rangle> ==>
                «{\<langle>x\<rangle>} : {Src \<langle>x\<rangle>} → {Trg \<langle>x\<rangle>}¬ ∧ «{\<langle>x\<rangle>} : {Dom \<langle>x\<rangle>} ==> {Cod \<langle>x\<rangle>}¬"
        by (auto simp add: preserves_src preserves_trg)
      show "∧t1 t2.
              (Arr t1 ==> «{t1} : {Src t1} → {Trg t1}¬ ∧ «{t1} : {Dom t1} ==> {Cod t1}¬) ==>
              (Arr t2 ==> «{t2} : {Src t2} → {Trg t2}¬ ∧ «{t2} : {Dom t2} ==> {Cod t2}¬) ==>
              Arr (t1 \<star> t2) ==>
              «{t1 \<star> t2} : {Src (t1 \<star> t2)} → {Trg (t1 \<star> t2)}¬ ∧
              «{t1 \<star> t2} : {Dom (t1 \<star> t2)} ==> {Cod (t1 \<star> t2)}¬"
        using hcomp_in_hhom in_hhom_def vconn_implies_hpar(1) vconn_implies_hpar(2) by auto
      show "∧t1 t2.
              (Arr t1 ==> «{t1} : {Src t1} → {Trg t1}¬ ∧ «{t1} : {Dom t1} ==> {Cod t1}¬) ==>
              (Arr t2 ==> «{t2} : {Src t2} → {Trg t2}¬ ∧ «{t2} : {Dom t2} ==> {Cod t2}¬) ==>
              Arr (t1 \<cdot> t2) ==>
              «{t1 \<cdot> t2} : {Src (t1 \<cdot> t2)} → {Trg (t1 \<cdot> t2)}¬ ∧
              «{t1 \<cdot> t2} : {Dom (t1 \<cdot> t2)} ==> {Cod (t1 \<cdot> t2)}¬"
        using VSeq_implies_HPar seqI' by auto
      show "∧t. (Arr t ==> «{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬) ==>
                Arr \<l>[t] ==>
                «{\<l>[t]} : {Src \<l>[t]} → {Trg \<l>[t]}¬ ∧ «{\<l>[t]} : {Dom \<l>[t]} ==> {Cod \<l>[t]}¬"
      proof (simp add: preserves_src preserves_trg)
        fix t
        assume t: "«{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬"
        assume 1: "Arr t"
        show "«l {t} : {Src t} → {Trg t}¬ ∧ «l {t} : {Trg t} ⋆ {Dom t} ==> {Cod t}¬"
        proof -
          have "src (l {t}) = {Src t}"
            using t 1
            by (metis (no_types, lifting) l.preserves_cod arr_cod in_hhomE map_simp src_cod)
          moreover have "trg (l {t}) = {Trg t}"
            using t 1
            by (metis (no_types, lifting) l.preserves_cod arr_cod in_hhomE map_simp trg_cod)
          moreover have "«l {t} : {Trg t} ⋆ {Dom t} ==> {Cod t}¬"
            using t 1
            apply (elim conjE in_hhomE)
            by (intro in_homI, auto)
          ultimately show ?thesis by auto
        qed
      qed
      show "∧t. (Arr t ==> «{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬) ==>
                Arr \<l>^-1[t] ==>
                «{\<l>^-1[t]} : {Src \<l>^-1[t]} → {Trg \<l>^-1[t]}¬ ∧
                «{\<l>^-1[t]} : {Dom \<l>^-1[t]} ==> {Cod \<l>^-1[t]}¬"
      proof (simp add: preserves_src preserves_trg)
        fix t
        assume t: "«{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬"
        assume 1: "Arr t"
        show "«l'.map {t} : {Src t} → {Trg t}¬ ∧
              «l'.map {t} : {Dom t} ==> {Trg t} ⋆ {Cod t}¬"
        proof -
          have "src (l'.map {t}) = {Src t}"
            using t 1 l'.preserves_dom arr_dom map_simp l'.preserves_reflects_arr src_dom
            by (metis (no_types, lifting) in_hhomE)
          moreover have "trg (l'.map {t}) = {Trg t}"
            using t 1 l'.preserves_dom arr_dom map_simp l'.preserves_reflects_arr trg_dom
            by (metis (no_types, lifting) in_hhomE)
          moreover have "«l'.map {t} : {Dom t} ==> {Trg t} ⋆ {Cod t}¬"
            using t 1 l'.preserves_hom
            apply (intro in_homI)
              apply auto[1]
             apply fastforce
            by fastforce
          ultimately show ?thesis by blast
        qed
      qed
      show "∧t. (Arr t ==> «{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬) ==>
                 Arr \<r>[t] ==>
                 «{\<r>[t]} : {Src \<r>[t]} → {Trg \<r>[t]}¬ ∧ «{\<r>[t]} : {Dom \<r>[t]} ==> {Cod \<r>[t]}¬"
      proof (simp add: preserves_src preserves_trg)
        fix t
        assume t: "«{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬"
        assume 1: "Arr t"
        show "«r {t} : {Src t} → {Trg t}¬ ∧ «r {t} : {Dom t} ⋆ {Src t} ==> {Cod t}¬"
        proof -
          have "src (r {t}) = {Src t}"
            using t 1 r.preserves_cod arr_cod map_simp r.preserves_reflects_arr src_cod
            by (metis (no_types, lifting) in_hhomE)
          moreover have "trg (r {t}) = {Trg t}"
            using t 1 r.preserves_cod arr_cod map_simp r.preserves_reflects_arr trg_cod
            by (metis (no_types, lifting) in_hhomE)
          moreover have "«r {t} : {Dom t} ⋆ {Src t} ==> {Cod t}¬"
            using t 1 by force
          ultimately show ?thesis by blast
        qed
      qed
      show "∧t. (Arr t ==> «{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬) ==>
                 Arr \<r>^-1[t] ==>
                 «{\<r>^-1[t]} : {Src \<r>^-1[t]} → {Trg \<r>^-1[t]}¬ ∧
                 «{\<r>^-1[t]} : {Dom \<r>^-1[t]} ==> {Cod \<r>^-1[t]}¬"
      proof (simp add: preserves_src preserves_trg)
        fix t
        assume t: "«{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬"
        assume 1: "Arr t"
        show "«r'.map {t} : {Src t} → {Trg t}¬ ∧
              «r'.map {t} : {Dom t} ==> {Cod t} ⋆ {Src t}¬"
        proof -
          have "src (r'.map {t}) = {Src t}"
            using t 1 r'.preserves_dom arr_dom map_simp r'.preserves_reflects_arr src_dom
            by (metis (no_types, lifting) in_hhomE)
          moreover have "trg (r'.map {t}) = {Trg t}"
            using t 1 r'.preserves_dom arr_dom map_simp r'.preserves_reflects_arr trg_dom
            by (metis (no_types, lifting) in_hhomE)
          moreover have "«r'.map {t} : {Dom t} ==> {Cod t} ⋆ {Src t}¬"
            using t 1 src_cod arr_cod r'.preserves_hom [of "{t}" "{Dom t}" "{Cod t}"]
            apply (elim conjE in_hhomE)
            by (intro in_homI, auto)
          ultimately show ?thesis by blast
        qed
      qed
      show "∧t u v.
            (Arr t ==> «{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬) ==>
            (Arr u ==> «{u} : {Src u} → {Trg u}¬ ∧ «{u} : {Dom u} ==> {Cod u}¬) ==>
            (Arr v ==> «{v} : {Src v} → {Trg v}¬ ∧ «{v} : {Dom v} ==> {Cod v}¬) ==>
            Arr \<a>[t, u, v] ==>
            «{\<a>[t, u, v]} : {Src \<a>[t, u, v]} → {Trg \<a>[t, u, v]}¬ ∧
            «{\<a>[t, u, v]} : {Dom \<a>[t, u, v]} ==> {Cod \<a>[t, u, v]}¬"
      proof (simp add: preserves_src preserves_trg)
        fix t u v
        assume t: "«{t} : {Trg u} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬"
        assume u: "«{u} : {Trg v} → {Trg u}¬ ∧ «{u} : {Dom u} ==> {Cod u}¬"
        assume v: "«{v} : {Src v} → {Trg v}¬ ∧ «{v} : {Dom v} ==> {Cod v}¬"
        assume tuv: "Arr t ∧ Arr u ∧ Arr v ∧ Src t = Trg u ∧ Src u = Trg v"
        show "«α ({t}, {u}, {v}) : {Src v} → {Trg t}¬ ∧
              «α ({t}, {u}, {v}) :
                 ({Dom t} ⋆ {Dom u}) ⋆ {Dom v} ==> {Cod t} ⋆ {Cod u} ⋆ {Cod v}¬"
        proof -
          have 1: "VVV.in_hom ({t}, {u}, {v})
                                ({Dom t}, {Dom u}, {Dom v}) ({Cod t}, {Cod u}, {Cod v})"
          proof -
            have "({t}, {u}, {v}) ∈
                    VxVxV.hom ({Dom t}, {Dom u}, {Dom v}) ({Cod t}, {Cod u}, {Cod v})"
              using t u v tuv by simp
            moreover have "({t}, {u}, {v}) ∈
                             {τμν. arr (fst τμν) ∧ VV.arr (snd τμν) ∧
                                   src (fst τμν) = trg (fst (snd τμν))}"
              using t u v tuv by fastforce
            ultimately show ?thesis
              using VVV.hom_char
                      [of "({Dom t}, {Dom u}, {Dom v})" "({Cod t}, {Cod u}, {Cod v})"]
              by blast
          qed
          have 4: "VVV.arr ({Dom t}, {Dom u}, {Dom v})"
            using 1 VVV.ide_dom VVV.dom_simp by (elim VVV.in_homE) force
          have 5: "VVV.arr ({Cod t}, {Cod u}, {Cod v})"
            using 1 VVV.ide_cod VVV.cod_simp VVV.in_hom_char_SbC by blast
          have 2: "«α ({t}, {u}, {v}) :
                      ({Dom t} ⋆ {Dom u}) ⋆ {Dom v} ==> {Cod t} ⋆ {Cod u} ⋆ {Cod v}¬"
            using 1 4 5 HoHV_def HoVH_def α_def
                  α.preserves_hom [of "({t}, {u}, {v})" "({Dom t}, {Dom u}, {Dom v})"
                                      "({Cod t}, {Cod u}, {Cod v})"]
            by simp
          have 3: "«α ({t}, {u}, {v}) : {Src v} → {Trg t}¬"
          proof
            show "arr (α ({t}, {u}, {v}))"
              using 2 by auto
            show "src (α ({t}, {u}, {v})) = {Src v}"
            proof -
              have "src (α ({t}, {u}, {v})) = src (({Dom t} ⋆ {Dom u}) ⋆ {Dom v})"
                using 2 src_dom [of "α ({t}, {u}, {v})"] by fastforce
              also have "... = src {Dom v}"
                using 4 VVV.arr_char_SbC VV.arr_char_SbC by simp
              also have "... = src (dom {v})"
                using v by fastforce
              also have "... = {Src v}"
                using v by auto
              finally show ?thesis by auto
            qed
            show "trg (α ({t}, {u}, {v})) = {Trg t}"
            proof -
              have "trg (α ({t}, {u}, {v})) = trg (({Dom t} ⋆ {Dom u}) ⋆ {Dom v})"
                using 2 trg_dom [of "α ({t}, {u}, {v})"] by fastforce
              also have "... = trg {Dom t}"
                using 4 VVV.arr_char_SbC VV.arr_char_SbC by simp
              also have "... = trg (dom {t})"
                using t by fastforce
              also have "... = {Trg t}"
                using t by auto
              finally show ?thesis by auto
            qed
          qed
          show ?thesis using 2 3 by simp
        qed
      qed
      show "∧t u v.
            (Arr t ==> «{t} : {Src t} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬) ==>
            (Arr u ==> «{u} : {Src u} → {Trg u}¬ ∧ «{u} : {Dom u} ==> {Cod u}¬) ==>
            (Arr v ==> «{v} : {Src v} → {Trg v}¬ ∧ «{v} : {Dom v} ==> {Cod v}¬) ==>
            Arr \<a>^-1[t, u, v] ==>
            «{\<a>^-1[t, u, v]} : {Src \<a>^-1[t, u, v]} → {Trg \<a>^-1[t, u, v]}¬ ∧
            «{\<a>^-1[t, u, v]} : {Dom \<a>^-1[t, u, v]} ==> {Cod \<a>^-1[t, u, v]}¬"
      proof (simp add: preserves_src preserves_trg)
        fix t u v
        assume t: "«{t} : {Trg u} → {Trg t}¬ ∧ «{t} : {Dom t} ==> {Cod t}¬"
        assume u: "«{u} : {Trg v} → {Trg u}¬ ∧ «{u} : {Dom u} ==> {Cod u}¬"
        assume v: "«{v} : {Src v} → {Trg v}¬ ∧ «{v} : {Dom v} ==> {Cod v}¬"
        assume tuv: "Arr t ∧ Arr u ∧ Arr v ∧ Src t = Trg u ∧ Src u = Trg v"
        show "«α'.map ({t}, {u}, {v}) : {Src v} → {Trg t}¬ ∧
              «α'.map ({t}, {u}, {v}) :
                 {Dom t} ⋆ {Dom u} ⋆ {Dom v} ==> ({Cod t} ⋆ {Cod u}) ⋆ {Cod v}¬"
        proof -
          have 1: "VVV.in_hom ({t}, {u}, {v})
                                ({Dom t}, {Dom u}, {Dom v}) ({Cod t}, {Cod u}, {Cod v})"
            using t u v tuv VVV.hom_char VVV.arr_char_SbC VV.arr_char_SbC VVV.dom_char_SbC VVV.cod_char_SbC
            apply (elim conjE in_hhomE in_homE)
            apply (intro VVV.in_homI)
            by simp_all
          have 4: "VVV.arr ({Dom t}, {Dom u}, {Dom v})"
            using "1" VVV.in_hom_char_SbC by blast
          have 5: "VVV.arr ({Cod t}, {Cod u}, {Cod v})"
            using "1" VVV.in_hom_char_SbC by blast
          have 2: "«α'.map ({t}, {u}, {v}) :
                      {Dom t} ⋆ {Dom u} ⋆ {Dom v} ==> ({Cod t} ⋆ {Cod u}) ⋆ {Cod v}¬"
            using 1 4 5 HoHV_def HoVH_def α'.map_def
                  α'.preserves_hom [of "({t}, {u}, {v})" "({Dom t}, {Dom u}, {Dom v})"
                                       "({Cod t}, {Cod u}, {Cod v})"]
            by simp
          have 3: "«α'.map ({t}, {u}, {v}) : {Src v} → {Trg t}¬"
          proof
            show "arr (α'.map ({t}, {u}, {v}))"
              using 2 by auto
            show "src (α'.map ({t}, {u}, {v})) = {Src v}"
            proof -
              have "src (α'.map ({t}, {u}, {v})) = src ({Dom t} ⋆ {Dom u} ⋆ {Dom v})"
                using 2 src_dom [of "α'.map ({t}, {u}, {v})"] by fastforce
              also have "... = src {Dom v}"
                using 4 VVV.arr_char_SbC VV.arr_char_SbC by simp
              also have "... = src (dom {v})"
                using v by fastforce
              also have "... = {Src v}"
                using v by auto
              finally show ?thesis by auto
            qed
            show "trg (α'.map ({t}, {u}, {v})) = {Trg t}"
            proof -
              have "trg (α'.map ({t}, {u}, {v})) = trg ({Dom t} ⋆ {Dom u} ⋆ {Dom v})"
                using 2 trg_dom [of "α'.map ({t}, {u}, {v})"] by fastforce
              also have "... = trg {Dom t}"
                using 4 VVV.arr_char_SbC VV.arr_char_SbC hseqI' by simp
              also have "... = trg (dom {t})"
                using t by fastforce
              also have "... = {Trg t}"
                using t by auto
              finally show ?thesis by auto
            qed
          qed
          show ?thesis using 2 3 by simp
        qed
      qed
    qed

    lemma eval_in_hom [intro]:
    assumes "Arr t"
    shows "«{t} : {Src t} → {Trg t}¬" and "«{t} : {Dom t} ==> {Cod t}¬"
      using assms eval_in_hom' by simp_all

    (*
     * TODO: It seems to me that the natural useful orientation of these facts is syntax
     * to semantics. However, having this as the default makes it impossible to do various
     * proofs by simp alone. This has to be sorted out. For right now, I am going to include
     * both versions, which will have to be explicitly invoked where needed.
     *)
    lemma eval_simps:
    assumes "Arr f"
    shows "arr {f}" and "{Src f} = src {f}" and "{Trg f} = trg {f}"
    and "{Dom f} = dom {f}" and "{Cod f} = cod {f}"
      using assms eval_in_hom [of f] by auto

    lemma eval_simps':
    assumes "Arr f"
    shows "arr {f}" and "src {f} = {Src f}" and "trg {f} = {Trg f}"
    and "dom {f} = {Dom f}" and "cod {f} = {Cod f}"
      using assms eval_in_hom by auto

    lemma obj_eval_Obj:
    shows "Obj t ==> obj {t}"
      using preserves_obj
      by (induct t) auto

    lemma ide_eval_Ide:
    shows "Ide t ==> ide {t}"
      by (induct t, auto simp add: eval_simps')

    lemma arr_eval_Arr [simp]:
    assumes "Arr t"
    shows "arr {t}"
      using assms by (simp add: eval_simps')

    (*
     * TODO: The next few results want eval_simps oriented from syntax to semantics.
     *)

    lemma eval_Lunit [simp]:
    assumes "Arr t"
    shows "{\<l>[t]} = l[{Cod t}] ⋅ (trg {t} ⋆ {t})"
      using assms l.naturality2 l_ide_simp by (simp add: eval_simps)

    lemma eval_Lunit' [simp]:
    assumes "Arr t"
    shows "{\<l>^-1[t]} = l^-1[{Cod t}] ⋅ {t}"
      using assms l'.naturality2 l_ide_simp by (simp add: eval_simps)

    lemma eval_Runit [simp]:
    assumes "Arr t"
    shows "{\<r>[t]} = r[{Cod t}] ⋅ ({t} ⋆ src {t})"
      using assms r.naturality2 r_ide_simp by (simp add: eval_simps)

    lemma eval_Runit' [simp]:
    assumes "Arr t"
    shows "{\<r>^-1[t]} = r^-1[{Cod t}] ⋅ {t}"
      using assms r'.naturality2 r_ide_simp by (simp add: eval_simps)

    lemma eval_Assoc [simp]:
    assumes "Arr t" and "Arr u" and "Arr v" and "Src t = Trg u" and "Src u = Trg v"
    shows "{\<a>[t, u, v]} = α (cod {t}, cod {u}, cod {v}) ⋅ (({t} ⋆ {u}) ⋆ {v})"
    proof -
      have "{\<a>[t, u, v]} = α ({t}, {u}, {v})" by simp
      also have "... = α (VVV.cod ({t}, {u}, {v})) ⋅ HoHV ({t}, {u}, {v})"
        using assms α.naturality2 [of "({t}, {u}, {v})"] VVV.arr_char_SbC VVV.cod_char_SbC
              α.extensionality α_def
        by auto
      also have "... = α (cod {t}, cod {u}, cod {v}) ⋅ (({t} ⋆ {u}) ⋆ {v})"
        unfolding HoHV_def α_def
        using assms VVV.arr_char_SbC VV.arr_char_SbC VVV.cod_char_SbC α.extensionality
        by auto
      finally show ?thesis by simp
    qed

    lemma eval_Assoc' [simp]:
    assumes "Arr t" and "Arr u" and "Arr v" and "Src t = Trg u" and "Src u = Trg v"
    shows "{\<a>^-1[t, u, v]} = a^-1[cod {t}, cod {u}, cod {v}] ⋅ ({t} ⋆ {u} ⋆ {v})"
    proof -
      have "{\<a>^-1[t, u, v]} = α'.map ({t}, {u}, {v})" by simp
      also have "... = α'.map (VVV.cod ({t}, {u}, {v})) ⋅ HoVH ({t}, {u}, {v})"
        using assms α'.naturality2 [of "({t}, {u}, {v})"] VVV.arr_char_SbC VVV.cod_char_SbC
              α'.extensionality
        by simp
      also have "... = α'.map (cod {t}, cod {u}, cod {v}) ⋅ ({t} ⋆ {u} ⋆ {v})"
        unfolding HoVH_def
        using assms VVV.arr_char_SbC VV.arr_char_SbC VVV.cod_char_SbC α'.extensionality
        apply simp
        using eval_simps'(2) eval_simps'(3) by presburger
      finally show ?thesis
        using a'_def by simp
    qed

    lemma eval_Lunit_Ide [simp]:
    assumes "Ide t"
    shows "{\<l>[t]} = l[{t}]"
      using assms l_ide_simp ide_eval_Ide by simp

    lemma eval_Lunit'_Ide [simp]:
    assumes "Ide t"
    shows "{\<l>^-1[t]} = l^-1[{t}]"
      using assms l_ide_simp ide_eval_Ide by simp

    lemma eval_Runit_Ide [simp]:
    assumes "Ide t"
    shows "{\<r>[t]} = r[{t}]"
      using assms r_ide_simp ide_eval_Ide by simp

    lemma eval_Runit'_Ide [simp]:
    assumes "Ide t"
    shows "{\<r>^-1[t]} = r^-1[{t}]"
      using assms r_ide_simp ide_eval_Ide by simp

    lemma eval_Assoc_Ide [simp]:
    assumes "Ide t" and "Ide u" and "Ide v" and "Src t = Trg u" and "Src u = Trg v"
    shows "{\<a>[t, u, v]} = α ({t}, {u}, {v})"
      using assms by simp

    lemma eval_Assoc'_Ide [simp]:
    assumes "Ide t" and "Ide u" and "Ide v" and "Src t = Trg u" and "Src u = Trg v"
    shows "{\<a>^-1[t, u, v]} = a^-1[{t}, {u}, {v}]"
      using assms a'_def by simp

    lemma iso_eval_Can:
    shows "Can t ==> iso {t}"
    proof (induct t; simp add: fsts.intros snds.intros)
      show "∧x. C.obj x ==> iso (E x)" by auto
      show "∧t1 t2. [ iso {t1}; iso {t2}; Can t1 ∧ Can t2 ∧ Src t1 = Trg t2 ] ==>
                      iso ({t1} ⋆ {t2})"
        using Can_implies_Arr by (simp add: eval_simps')
      show "∧t1 t2. [ iso {t1}; iso {t2}; Can t1 ∧ Can t2 ∧ Dom t1 = Cod t2 ] ==>
                      iso ({t1} ⋅ {t2})"
        using Can_implies_Arr isos_compose by (simp add: eval_simps')
      show "∧t. [ iso {t}; Can t ] ==> iso (l {t})"
        using l.preserves_iso by auto
      show "∧t. [ iso {t}; Can t ] ==> iso (l'.map {t})"
        using l'.preserves_iso by simp
      show "∧t. [ iso {t}; Can t ] ==> iso (r {t})"
        using r.preserves_iso by auto
      show "∧t. [ iso {t}; Can t ] ==> iso (r'.map {t})"
        using r'.preserves_iso by simp
      fix t1 t2 t3
      assume t1: "iso {t1}" and t2: "iso {t2}" and t3: "iso {t3}"
      assume 1: "Can t1 ∧ Can t2 ∧ Can t3 ∧ Src t1 = Trg t2 ∧ Src t2 = Trg t3"
      have 2: "VVV.iso ({t1}, {t2}, {t3})"
      proof -
        have 3: "VxVxV.iso ({t1}, {t2}, {t3})"
          using t1 t2 t3 Can_implies_Arr VxVxV.iso_char VxV.iso_char by simp
        moreover have "VVV.arr (VxVxV.inv ({t1}, {t2}, {t3}))"
        proof -
          have "VxVxV.inv ({t1}, {t2}, {t3}) = (inv {t1}, inv {t2}, inv {t3})"
            using t1 t2 t3 3 by simp
          thus ?thesis
            using t1 t2 t3 1 Can_implies_Arr VVV.arr_char_SbC VV.arr_char_SbC
            by (simp add: eval_simps')
        qed
        ultimately show ?thesis
          using t1 t2 t3 1 Can_implies_Arr VVV.iso_char_SbC VVV.arr_char_SbC
          by (auto simp add: eval_simps')
      qed
      show "iso (α ({t1}, {t2}, {t3}))"
        using 2 α_def α.preserves_iso by auto
      show "iso (α'.map ({t1}, {t2}, {t3}))"
        using 2 α'.preserves_iso by simp
    qed

    lemma eval_Inv_Can:
    shows "Can t ==> {Inv t} = inv {t}"
    proof (induct t)
      show "∧x. Can \<langle>x\<rangle>₀ ==> {Inv \<langle>x\<rangle>₀} = inv {\<langle>x\<rangle>₀}" by auto
      show "∧x. Can \<langle>x\<rangle> ==> {Inv \<langle>x\<rangle>} = inv {\<langle>x\<rangle>}" by simp
      show "∧t1 t2. (Can t1 ==> {Inv t1} = inv {t1}) ==>
                    (Can t2 ==> {Inv t2} = inv {t2}) ==>
                     Can (t1 \<star> t2) ==> {Inv (t1 \<star> t2)} = inv {t1 \<star> t2}"
        using iso_eval_Can Can_implies_Arr
        by (simp add: eval_simps')
      show "∧t1 t2. (Can t1 ==> {Inv t1} = inv {t1}) ==>
                    (Can t2 ==> {Inv t2} = inv {t2}) ==>
                     Can (t1 \<cdot> t2) ==> {Inv (t1 \<cdot> t2)} = inv {t1 \<cdot> t2}"
        using iso_eval_Can inv_comp Can_implies_Arr
        by (simp add: eval_simps')
      fix t
      assume I: "Can t ==> {Inv t} = inv {t}"
      show "Can \<l>[t] ==> {Inv \<l>[t]} = inv {\<l>[t]}"
      proof -
        assume t: "Can \<l>[t]"
        have "{Inv \<l>[t]} = {\<l>^-1[Inv t]}" by simp
        also have "... = l'.map (inv {t})"
          using t I by simp
        also have "... = l'.map (cod (inv {t})) ⋅ inv {t}"
          using t l'.naturality2 iso_inv_iso iso_eval_Can iso_is_arr
          by (metis (no_types, lifting) Can.simps(5) map_simp)
        also have "... = inv ({t} ⋅ l (dom {t}))"
        proof -
          have 1: "iso {t}" using t iso_eval_Can by simp
          moreover have "iso (l (dom {t}))"
            using t 1 l.components_are_iso ide_dom by blast
          moreover have "seq {t} (l (dom {t}))"
            using t 1 iso_is_arr by auto
          ultimately show ?thesis
            using t 1 inv_comp by auto
        qed
        also have "... = inv {\<l>[t]}"
          using t iso_eval_Can l_ide_simp lunit_naturality Can_implies_Arr eval_Lunit
          by (auto simp add: eval_simps)
        finally show ?thesis by blast
      qed
      show "Can \<l>^-1[t] ==> {Inv \<l>^-1[t]} = inv {\<l>^-1[t]}"
      proof -
        assume t: "Can (Lunit' t)"
        have "{Inv (Lunit' t)} = {Lunit (Inv t)}" by simp
        also have "... = l (inv {t})"
          using t I by simp
        also have "... = inv {t} ⋅ l (dom (inv {t}))"
          using t l.naturality1 iso_inv_iso iso_eval_Can iso_is_arr
          by (metis (no_types, lifting) Can.simps(6) map_simp)
        also have "... = inv (l'.map (cod {t}) ⋅ {t})"
        proof -
          have 1: "iso {t}" using t iso_eval_Can by simp
          moreover have "iso (l'.map (cod {t}))"
            using t 1 l'.components_are_iso ide_cod by blast
          moreover have "seq (l'.map (cod {t})) {t}"
            using t 1 iso_is_arr by auto
          ultimately show ?thesis
            using t 1 inv_comp by auto
        qed
        also have "... = inv {\<l>^-1[t]}"
          using t l'.naturality2 iso_eval_Can iso_is_arr by force
        finally show ?thesis by auto
      qed
      show "Can \<r>[t] ==> {Inv \<r>[t]} = inv {\<r>[t]}"
      proof -
        assume t: "Can \<r>[t]"
        have "{Inv \<r>[t]} = {\<r>^-1[Inv t]}" by simp
        also have "... = r'.map (inv {t})"
          using t I by simp
        also have "... = r'.map (cod (inv {t})) ⋅ inv {t}"
          using t r'.naturality2 map_simp iso_inv_iso iso_eval_Can iso_is_arr
          by (metis (no_types, lifting) Can.simps(7))
        also have "... = inv ({t} ⋅ r (dom {t}))"
        proof -
          have 1: "iso {t}" using t iso_eval_Can by simp
          moreover have "iso (r (dom {t}))"
            using t 1 r.components_are_iso ide_dom by blast
          moreover have "seq {t} (r (dom {t}))"
            using t 1 iso_is_arr by simp
          ultimately show ?thesis
            using t 1 inv_comp by auto
        qed
        also have "... = inv {\<r>[t]}"
          using t r_ide_simp iso_eval_Can runit_naturality Can_implies_Arr eval_Runit
          by (auto simp add: eval_simps)
        finally show ?thesis by blast
      qed
      show "Can \<r>^-1[t] ==> {Inv \<r>^-1[t]} = inv {\<r>^-1[t]}"
      proof -
        assume t: "Can \<r>^-1[t]"
        have "{Inv \<r>^-1[t]} = {\<r>[Inv t]}"
          by simp
        also have "... = r (inv {t})"
          using t I by simp
        also have "... = inv {t} ⋅ r (dom (inv {t}))"
          using t r.naturality1 map_simp iso_inv_iso iso_eval_Can iso_is_arr
          by (metis (no_types, lifting) Can.simps(8))
        also have "... = inv (r'.map (cod {t}) ⋅ {t})"
        proof -
          have 1: "iso {t}" using t iso_eval_Can by simp
          moreover have "iso (r'.map (cod {t}))"
            using t 1 r'.components_are_iso ide_cod by blast
          moreover have "seq (r'.map (cod {t})) {t}"
            using t 1 iso_is_arr by auto
          ultimately show ?thesis
            using t 1 inv_comp by auto
        qed
        also have "... = inv {\<r>^-1[t]}"
          using t r'.naturality2 iso_eval_Can iso_is_arr by auto
        finally show ?thesis by auto
      qed
      next
      fix t u v
      assume I1: "Can t ==> {Inv t} = inv {t}"
      assume I2: "Can u ==> {Inv u} = inv {u}"
      assume I3: "Can v ==> {Inv v} = inv {v}"
      show "Can \<a>[t, u, v] ==> {Inv \<a>[t, u, v]} = inv {\<a>[t, u, v]}"
      proof -
        assume "Can \<a>[t, u, v]"
        hence tuv: "Can t ∧ Can u ∧ Can v ∧ Src t = Trg u ∧ Src u = Trg v" by simp
        have "{Inv \<a>[t, u, v]} = {\<a>^-1[Inv t, Inv u, Inv v]}" by simp
        also have "... = a^-1[dom {t}, dom {u}, dom {v}] ⋅ (inv {t} ⋆ inv {u} ⋆ inv {v})"
          using tuv I1 I2 I3 eval_in_hom α'.map_ide_simp inv_in_hom iso_eval_Can assoc'_naturality
                Can_implies_Arr Src_Inv Trg_Inv eval_Assoc' Dom_Inv Can_Inv cod_inv
          by presburger
        also have "... = inv (({t} ⋆ {u} ⋆ {v}) ⋅ α (dom {t}, dom {u}, dom {v}))"
          using tuv iso_eval_Can Can_implies_Arr eval_simps'(2) eval_simps'(3) α_def
          by (simp add: inv_comp)
        also have "... = inv (α ({t}, {u}, {v}))"
          using tuv Can_implies_Arr α_def
          by (metis assoc_naturality1 arr_eval_Arr eval_simps'(2) eval_simps'(3) fst_conv snd_conv)
        also have "... = inv {\<a>[t, u, v]}" by simp
        finally show ?thesis by blast
      qed
      show "Can \<a>^-1[t, u, v] ==> {Inv \<a>^-1[t, u, v]} = inv {\<a>^-1[t, u, v]}"
      proof -
        assume tuv: "Can \<a>^-1[t, u, v]"
        have t: "Can t" using tuv by simp
        have u: "Can u" using tuv by simp
        have v: "Can v" using tuv by simp
        have "{Inv \<a>^-1[t, u, v]} = {\<a>[Inv t, Inv u, Inv v]}" by simp
        also have "... = (inv {t} ⋆ inv {u} ⋆ inv {v}) ⋅ α (cod {t}, cod {u}, cod {v})"
          using α_def tuv I1 I2 I3 iso_eval_Can Can_implies_Arr eval_simps'(2) eval_simps'(3)
          apply simp
          using assoc_naturality1 arr_inv dom_inv src_inv trg_inv by presburger
        also have "... = inv (a^-1[cod {t}, cod {u}, cod {v}] ⋅ ({t} ⋆ {u} ⋆ {v}))"
          using tuv inv_comp [of "{t} ⋆ {u} ⋆ {v}" "a^-1[cod {t}, cod {u}, cod {v}]"]
                Can_implies_Arr iso_assoc α_def
          by (simp add: eval_simps'(2) eval_simps'(3) iso_eval_Can)
        also have 1: "... = inv ((({t} ⋆ {u}) ⋆ {v}) ⋅ a^-1[dom {t}, dom {u}, dom {v}])"
          using tuv assoc'_naturality [of "{t}" "{u}" "{v}"] Can_implies_Arr
                eval_simps'(2) eval_simps'(3)
          by simp
        also have "... = inv {\<a>^-1[t, u, v]}"
          using tuv 1 Can_implies_Arr eval_Assoc' by auto
        finally show ?thesis by blast
      qed
    qed

    lemma eval_VcompNml:
    assumes "Nml t" and "Nml u" and "VSeq t u"
    shows "{t \<lfloor>\<cdot>\<rfloor> u} = {t} ⋅ {u}"
    proof -
      have "∧u. [ Nml t; Nml u; VSeq t u ] ==> {t \<lfloor>\<cdot>\<rfloor> u} = {t} ⋅ {u}"
      proof (induct t, simp_all add: eval_simps)
        fix u a
        assume u: "Nml u"
        assume 1: "Arr u ∧ \<langle>a\<rangle>₀ = Cod u"
        show "{u} = cod {u} ⋅ {u}"
          using 1 comp_cod_arr by simp
        next
        fix u f
        assume u: "Nml u"
        assume f: "C.arr f"
        assume 1: "Arr u ∧ \<langle>C.dom f\<rangle> = Cod u"
        show "{\<langle>f\<rangle> \<lfloor>\<cdot>\<rfloor> u} = E f ⋅ {u}"
          using f u 1 as_nat_trans.preserves_comp_2 by (cases u; simp)
        next
        fix u v w
        assume I1: "∧u. [ Nml v; Nml u; Arr u ∧ Dom v = Cod u ] ==> {v \<lfloor>\<cdot>\<rfloor> u} = {v} ⋅ {u}"
        assume I2: "∧u. [ Nml w; Nml u; Arr u ∧ Dom w = Cod u ] ==> {w \<lfloor>\<cdot>\<rfloor> u} = {w} ⋅ {u}"
        assume vw: "Nml (v \<star> w)"
        have v: "Nml v ∧ v = Prim (un_Prim v)"
          using vw by (simp add: Nml_HcompD)
        have w: "Nml w"
          using vw by (simp add: Nml_HcompD)
        assume u: "Nml u"
        assume 1: "Arr v ∧ Arr w ∧ Src v = Trg w ∧ Arr u ∧ Dom v \<star> Dom w = Cod u"
        show "{(v \<star> w) \<lfloor>\<cdot>\<rfloor> u} = ({v} ⋆ {w}) ⋅ {u}"
          using u 1 HcompNml_in_Hom apply (cases u, simp_all)
        proof -
          fix x y
          assume 3: "u = x \<star> y"
          have x: "Nml x"
            using u 1 3 Nml_HcompD by blast
          have y: "Nml y"
            using u x 1 3 Nml_HcompD by blast
          assume 4: "Arr v ∧ Arr w ∧ Src v = Trg w ∧ Dom v = Cod x ∧ Dom w = Cod y"
          have "{v \<lfloor>\<cdot>\<rfloor> x} ⋆ {w \<lfloor>\<cdot>\<rfloor> y} = {v \<lfloor>\<cdot>\<rfloor> x \<star> w \<lfloor>\<cdot>\<rfloor> y}"
            using v w x y 4 HcompNml_in_Hom by simp
          moreover have "... = {v \<lfloor>\<cdot>\<rfloor> x} ⋆ {w \<lfloor>\<cdot>\<rfloor> y}" by simp
          moreover have "... = {v} ⋅ {x} ⋆ {w} ⋅ {y}"
            using v w x y 4 I1 [of x] I2 [of y] Nml_implies_Arr by simp
          moreover have "... = ({v} ⋆ {w}) ⋅ ({x} ⋆ {y})"
            using v w x y 4 Nml_implies_Arr interchange [of "{v}" "{x}" "{w}" "{y}"]
            by (simp add: eval_simps')
          ultimately have "{v \<lfloor>\<cdot>\<rfloor> x} ⋆ {w \<lfloor>\<cdot>\<rfloor> y} = ({v} ⋆ {w}) ⋅ ({x} ⋆ {y})" by presburger
          moreover have "arr {v \<lfloor>\<cdot>\<rfloor> x} ∧ arr {w \<lfloor>\<cdot>\<rfloor> y}"
            using v w x y 4 VcompNml_in_Hom by simp
          ultimately show "{v \<lfloor>\<cdot>\<rfloor> x} ⋆ {w \<lfloor>\<cdot>\<rfloor> y} = ({v} ⋆ {w}) ⋅ ({x} ⋆ {y})"
            by simp
        qed
      qed
      thus ?thesis using assms by blast
    qed

    lemma eval_red_Hcomp:
    assumes "Ide a" and "Ide b"
    shows "{(a \<star> b)\<down>} = {\<lfloor>a\<rfloor> \<Down> \<lfloor>b\<rfloor>} ⋅ ({a\<down>} ⋆ {b\<down>})"
    proof -
      have "Nml (a \<star> b) ==> ?thesis"
      proof -
        assume 1: "Nml (a \<star> b)"
        hence 2: "Nml a ∧ Nml b ∧ Src a = Trg b"
          using Nml_HcompD(3-4,7) by simp
        have "{(a \<star> b)\<down>} = {a} ⋆ {b}"
          using 1 Nml_HcompD
          by (metis eval.simps(3) red_Nml)
        also have "... = {\<lfloor>a\<rfloor> \<Down> \<lfloor>b\<rfloor>} ⋅ ({a\<down>} ⋆ {b\<down>})"
          using assms 1 2 ide_eval_Ide Nmlize_in_Hom red2_Nml Nmlize_Nml
          by (simp add: eval_simps')
        finally show ?thesis by simp
      qed
      moreover have "¬ Nml (a \<star> b) ==> ?thesis"
        using assms Can_red2 by (simp add: Can_red(1) iso_eval_Can)
      ultimately show ?thesis by blast
    qed

    (* TODO: Would the following still be useful if \<^bold>\a\<^bold>\\<^sub>0 is replaced by Src t? *)
    lemma eval_red2_Nml_Prim₀:
    assumes "Ide t" and "Nml t" and "Src t = \<langle>a\<rangle>₀"
    shows "{t \<Down> \<langle>a\<rangle>₀} = r[{t}]"
      using assms r_ide_simp
      apply (cases t)
               apply simp_all
    proof -
      show "C.obj a ==> t = \<langle>a\<rangle>₀ ==> l (E a) = r[E a]"
        using unitor_coincidence obj_eval_Obj [of t] l_ide_simp by auto
      show "∧b c. Ide b ∧ Ide c ∧ Src b = Trg c ==> r ({b} ⋆ {c}) = r[{b} ⋆ {c}]"
        using r_ide_simp by (simp add: eval_simps' ide_eval_Ide)
    qed

  end

  text ‹
    Most of the time when we interpret the @{locale evaluation_map} locale, we are evaluating
    terms formed from the arrows in a bicategory as arrows of the bicategory itself.
    The following locale streamlines that use case.
  ›

  locale self_evaluation_map =
    bicategory
  begin

    sublocale bicategorical_language V src trg ..

    sublocale evaluation_map V src trg V H a i src trg ‹λμ. if arr μ then μ else null›
      using src.extensionality trg.extensionality
      by (unfold_locales, auto)

    notation eval (‹{_}›)
    notation Nmlize (‹\<lfloor>_\<rfloor>›)

  end

  subsection "Coherence"

  text ‹
    We define an individual term to be \emph{coherent} if it commutes, up to evaluation,
    with the reductions of its domain and codomain. We then formulate the coherence theorem
    as the statement ``every formal arrow is coherent''. Because reductions evaluate
    to isomorphisms, this implies the standard version of coherence, which says that
    ``parallel canonical terms have equal evaluations''.
  ›

  context evaluation_map
  begin

    abbreviation coherent
    where "coherent t ≡ {Cod t\<down>} ⋅ {t} = {\<lfloor>t\<rfloor>} ⋅ {Dom t\<down>}"

    lemma Nml_implies_coherent:
    assumes "Nml t"
    shows "coherent t"
      using assms Nml_implies_Arr Ide_Dom Ide_Cod Nml_Dom Nml_Cod Nmlize_Nml red_Nml
      by (metis Dom_Cod VcompNml_Cod_Nml arr_eval_Arr comp_arr_dom eval_VcompNml
          eval_simps(4))

    lemma canonical_factorization:
    assumes "Arr t"
    shows "coherent t ⟷ {t} = inv {Cod t\<down>} ⋅ {\<lfloor>t\<rfloor>} ⋅ {Dom t\<down>}"
    proof
      assume 1: "coherent t"
      have "inv {Cod t\<down>} ⋅ {\<lfloor>t\<rfloor>} ⋅ {Dom t\<down>} = inv {Cod t\<down>} ⋅ {Cod t\<down>} ⋅ {t}"
        using 1 by simp
      also have "... = (inv {Cod t\<down>} ⋅ {Cod t\<down>}) ⋅ {t}"
        using comp_assoc by simp
      also have "... = {t}"
        using assms red_in_Hom Ide_Cod Can_red iso_eval_Can comp_cod_arr
        by (simp add: comp_inv_arr' eval_simps'(4) eval_simps'(5))
      finally show "{t} = inv {Cod t\<down>} ⋅ {\<lfloor>t\<rfloor>} ⋅ {Dom t\<down>}"
        by presburger
      next
      assume 1: "{t} = inv {Cod t\<down>} ⋅ {\<lfloor>t\<rfloor>} ⋅ {Dom t\<down>}"
      hence "{Cod t\<down>} ⋅ {t} = {Cod t\<down>} ⋅ inv {Cod t\<down>} ⋅ {\<lfloor>t\<rfloor>} ⋅ {Dom t\<down>}" by simp
      also have "... = ({Cod t\<down>} ⋅ inv {Cod t\<down>}) ⋅ {\<lfloor>t\<rfloor>} ⋅ {Dom t\<down>}"
        using comp_assoc by simp
      also have "... = {\<lfloor>t\<rfloor>} ⋅ {Dom t\<down>}"
      proof -
        have "{Cod t\<down>} ⋅ inv {Cod t\<down>} = cod {\<lfloor>t\<rfloor>}"
          using assms red_in_Hom Ide_Cod Can_red iso_eval_Can
                inv_is_inverse Nmlize_in_Hom comp_arr_inv
          by (simp add: eval_simps')
        thus ?thesis
          using assms red_in_Hom Ide_Cod Can_red iso_eval_Can
                Ide_Dom Nmlize_in_Hom comp_cod_arr
          by (auto simp add: eval_simps')
      qed
      finally show "coherent t" by blast
    qed

    lemma coherent_iff_coherent_Inv:
    assumes "Can t"
    shows "coherent t ⟷ coherent (Inv t)"
    proof
      have 1: "∧t. Can t ==> coherent t ==> coherent (Inv t)"
      proof -
        fix t
        assume "Can t"
        hence t: "Can t ∧ Arr t ∧ Ide (Dom t) ∧ Ide (Cod t) ∧
                  arr {t} ∧ iso {t} ∧ inverse_arrows {t} (inv {t}) ∧
                  Can \<lfloor>t\<rfloor> ∧ Arr \<lfloor>t\<rfloor> ∧ arr {\<lfloor>t\<rfloor>} ∧ iso {\<lfloor>t\<rfloor>} ∧ \<lfloor>t\<rfloor> ∈ VHom \<lfloor>Dom t\<rfloor> \<lfloor>Cod t\<rfloor> ∧
                  inverse_arrows {\<lfloor>t\<rfloor>} (inv {\<lfloor>t\<rfloor>}) ∧ Inv t ∈ VHom (Cod t) (Dom t)"
          using assms Can_implies_Arr Ide_Dom Ide_Cod iso_eval_Can inv_is_inverse
                Nmlize_in_Hom Can_Nmlize_Can Inv_in_Hom
          by simp
        assume coh: "coherent t"
        have "{Cod (Inv t)\<down>} ⋅ {Inv t} = (inv {\<lfloor>t\<rfloor>} ⋅ {\<lfloor>t\<rfloor>}) ⋅ {Cod (Inv t)\<down>} ⋅ {Inv t}"
          using t comp_inv_arr red_in_Hom
                comp_cod_arr [of "{Cod (Inv t)\<down>} ⋅ {Inv t}" "inv {\<lfloor>t\<rfloor>} ⋅ {\<lfloor>t\<rfloor>}"]
          by (auto simp add: eval_simps')
        also have "... = inv {\<lfloor>t\<rfloor>} ⋅ {\<lfloor>t\<rfloor>} ⋅ {Dom t\<down>} ⋅ inv {t}"
          using t eval_Inv_Can comp_assoc by auto
        also have "... = inv {\<lfloor>t\<rfloor>} ⋅ ({\<lfloor>t\<rfloor>} ⋅ {Dom t\<down>}) ⋅ inv {t}"
          using comp_assoc by simp
        also have "... = inv {\<lfloor>t\<rfloor>} ⋅ ({Cod t\<down>} ⋅ {t}) ⋅ inv {t}"
          using t coh by simp
        also have "... = inv {\<lfloor>t\<rfloor>} ⋅ {Cod t\<down>} ⋅ {t} ⋅ inv {t}"
          using comp_assoc by simp
        also have "... = {\<lfloor>Inv t\<rfloor>} ⋅ {Dom (Inv t)\<down>}"
        proof -
          have "{Cod t\<down>} ⋅ {t} ⋅ inv {t} = {Dom (Inv t)\<down>}"
            using t eval_Inv_Can red_in_Hom comp_arr_inv comp_arr_dom
            by (simp add: eval_simps')
          thus ?thesis
            using t Nmlize_Inv eval_Inv_Can by simp
        qed
        finally show "coherent (Inv t)" by blast
      qed
      show "coherent t ==> coherent (Inv t)" using assms 1 by simp
      show "coherent (Inv t) ==> coherent t"
      proof -
        assume "coherent (Inv t)"
        hence "coherent (Inv (Inv t))"
          using assms 1 Can_Inv by blast
        thus ?thesis using assms by simp
      qed
    qed

    text ‹
      The next two facts are trivially proved by the simplifier, so formal named facts
      are not really necessary, but we include them for logical completeness of the
      following development, which proves coherence by structural induction.
    ›

    lemma coherent_Prim₀:
    assumes "C.obj a"
    shows "coherent \<langle>a\<rangle>₀"
      by simp

    lemma coherent_Prim:
    assumes "Arr \<langle>f\<rangle>"
    shows "coherent \<langle>f\<rangle>"
      using assms by simp

    lemma coherent_Lunit_Ide:
    assumes "Ide t"
    shows "coherent \<l>[t]"
    proof -
      have t: "Ide t ∧ Arr t ∧ Dom t = t ∧ Cod t = t ∧
               ide {t} ∧ ide {\<lfloor>t\<rfloor>} ∧ {t\<down>} ∈ hom {t} {\<lfloor>t\<rfloor>}"
        using assms Ide_in_Hom Ide_Nmlize_Ide
              red_in_Hom eval_in_hom ide_eval_Ide
        by force
      have 1: "Obj (Trg t)" using t by auto
      have "{Cod \<l>[t]\<down>} ⋅ {\<l>[t]} = l[{\<lfloor>t\<rfloor>}] ⋅ ({Trg t} ⋆ {t\<down>})"
        using t l_ide_simp lunit_naturality [of "{t\<down>}"] red_in_Hom
        by (simp add: eval_simps')
      also have "... = {\<lfloor>t\<rfloor>} ⋅ l[{\<lfloor>t\<rfloor>}] ⋅ ({Trg t} ⋆ {t\<down>})"
         using t 1 lunit_in_hom Nmlize_in_Hom ide_eval_Ide red_in_Hom comp_cod_arr
               Obj_implies_Ide
         by (auto simp add: eval_simps')
      also have "... = {\<lfloor>\<l>[t]\<rfloor>} ⋅ {Dom \<l>[t]\<down>}"
        using 1 t Nml_Trg l_ide_simp by (cases "Trg t"; simp)
      finally show ?thesis by simp
    qed
      
    text ‹
      Unlike many of the other results, the next one was not quite so straightforward to adapt
      from @{session ‹MonoidalCategory›}.
    ›

    lemma coherent_Runit_Ide:
    assumes "Ide t"
    shows "coherent \<r>[t]"
    proof -
      have t: "Ide t ∧ Arr t ∧ Dom t = t ∧ Cod t = t ∧
               ide {t} ∧ ide {\<lfloor>t\<rfloor>} ∧ {t\<down>} ∈ hom {t} {\<lfloor>t\<rfloor>}"
        using assms Ide_in_Hom Ide_Nmlize_Ide
              red_in_Hom eval_in_hom ide_eval_Ide
        by force
      have "{Cod \<r>[t]\<down>} ⋅ {\<r>[t]} = r[{\<lfloor>t\<rfloor>}] ⋅ ({t\<down>} ⋆ {Src t})"
        using t r_ide_simp red_in_Hom runit_naturality [of "{t\<down>}"]
        by (simp add: eval_simps')
      also have "... = {\<lfloor>\<r>[t]\<rfloor>} ⋅ {Dom \<r>[t]\<down>}"
      proof -
         have "{\<lfloor>\<r>[t]\<rfloor>} ⋅ {Dom \<r>[t]\<down>} = {\<lfloor>t\<rfloor>} ⋅ {\<lfloor>t\<rfloor> \<Down> \<lfloor>Src t\<rfloor>} ⋅ ({t\<down>} ⋆ {Src t\<down>})"
           using t by (cases t; simp; cases "Src t"; simp)
         also have "... = ({\<lfloor>t\<rfloor>} ⋅ {\<lfloor>t\<rfloor> \<Down> \<lfloor>Src t\<rfloor>}) ⋅ ({t\<down>} ⋆ {Src t\<down>})"
         proof -
           have "{\<lfloor>t\<rfloor>} ∈ hom {\<lfloor>t\<rfloor>} {\<lfloor>t\<rfloor>}"
             using t Nmlize_in_Hom by auto
           moreover have "{\<lfloor>t\<rfloor> \<Down> \<lfloor>Src t\<rfloor>} ∈ hom ({\<lfloor>t\<rfloor>} ⋆ {Src t}) {\<lfloor>t\<rfloor>}"
           proof -
             have "{\<lfloor>t\<rfloor> \<Down> \<lfloor>Src t\<rfloor>} ∈ hom {\<lfloor>t\<rfloor> \<star> \<lfloor>Src t\<rfloor>} {\<lfloor>t\<rfloor>}"
             proof -
               have "Src \<lfloor>t\<rfloor> = Trg \<lfloor>Src t\<rfloor> ∧ \<lfloor>\<lfloor>t\<rfloor> \<star> \<lfloor>Src t\<rfloor>\<rfloor> = \<lfloor>t\<rfloor>"
                 using t Nmlize_Src Nml_Nmlize HcompNml_Nml_Src [of "\<lfloor>t\<rfloor>"]
                 by simp
               thus ?thesis
                 using t Ide_Nmlize_Ide Nml_Nmlize Obj_Src red2_in_Hom(2) Obj_implies_Ide
                 by (auto simp add: eval_simps')
             qed
             thus ?thesis using t Nmlize_in_Hom Nmlize_Src by simp
           qed
           moreover have "{t\<down>} ⋆ {Src t\<down>} ∈ hom ({t} ⋆ {Src t}) ({\<lfloor>t\<rfloor>} ⋆ {Src t})"
             using t red_in_Hom red_Src Obj_Src eval_simps' Obj_implies_Ide by auto
           ultimately show ?thesis using comp_assoc by fastforce
         qed
         also have "... = r[{\<lfloor>t\<rfloor>}] ⋅ ({t\<down>} ⋆ {Src t\<down>})"
         proof -
           have "{\<lfloor>t\<rfloor> \<Down> \<lfloor>Src t\<rfloor>} = r[{\<lfloor>t\<rfloor>}]"
           proof -
             have "Nml \<lfloor>t\<rfloor>" using t Nml_Nmlize by blast
             moreover have "is_Prim₀ \<lfloor>Src t\<rfloor>"
               using t is_Prim0_Src Nmlize_Src by presburger
             ultimately show ?thesis
               apply (cases "\<lfloor>t\<rfloor>"; simp; cases "\<lfloor>Src t\<rfloor>"; simp)
               using t unitor_coincidence l_ide_simp r_ide_simp Nmlize_in_Hom
                 apply simp_all
               using t is_Prim0_Src
               apply (cases "\<lfloor>t\<rfloor>"; simp)
               using t Nmlize_Src unitor_coincidence preserves_obj by simp
           qed
           moreover have "r[{\<lfloor>t\<rfloor>}] ∈ hom ({\<lfloor>t\<rfloor>} ⋆ {Src t}) {\<lfloor>t\<rfloor>}"
             using t Nmlize_in_Hom by (auto simp add: eval_simps'(2))
           ultimately show ?thesis
             using comp_cod_arr [of "r[{\<lfloor>t\<rfloor>}]"] by fastforce
         qed
         also have "... = r[{\<lfloor>t\<rfloor>}] ⋅ ({t\<down>} ⋆ {Src t})"
           using t red_Src by auto
         finally show ?thesis by argo
      qed
      finally show ?thesis by blast
    qed

    lemma coherent_Lunit'_Ide:
    assumes "Ide a"
    shows "coherent \<l>^-1[a]"
      using assms Ide_implies_Can coherent_Lunit_Ide
            coherent_iff_coherent_Inv [of "Lunit a"]
      by simp

    lemma coherent_Runit'_Ide:
    assumes "Ide a"
    shows "coherent \<r>^-1[a]"
      using assms Ide_implies_Can coherent_Runit_Ide
            coherent_iff_coherent_Inv [of "Runit a"]
      by simp

    lemma red2_Nml_Src:
    assumes "Ide t" and "Nml t"
    shows "{t \<Down> Src t} = r[{t}]"
      using assms eval_red2_Nml_Prim₀ is_Prim0_Src [of t]
      by (cases "Src t"; simp)

    lemma red2_Trg_Nml:
    assumes "Ide t" and "Nml t"
    shows "{Trg t \<Down> t} = l[{t}]"
      using assms is_Prim0_Trg [of t] l_ide_simp ide_eval_Ide
      by (cases "Trg t"; simp)

    lemma coherence_key_fact:
    assumes "Ide a ∧ Nml a" and "Ide b ∧ Nml b" and "Ide c ∧ Nml c"
    and "Src a = Trg b" and "Src b = Trg c"
    shows "{(a \<lfloor>\<star>\<rfloor> b) \<Down> c} ⋅ ({a \<Down> b} ⋆ {c}) =
           ({a \<Down> (b \<lfloor>\<star>\<rfloor> c)} ⋅ ({a} ⋆ {b \<Down> c})) ⋅ a[{a}, {b}, {c}]"
    proof -
      have "is_Prim₀ b ==> ?thesis"
      proof -
        assume b: "is_Prim₀ b"
        have "{a \<Down> c} ⋅ (r[{a}] ⋆ {c}) = ({a \<Down> c} ⋅ ({a} ⋆ l[{c}])) ⋅ a[{a}, {Trg c}, {c}]"
        proof -
          have "Src b = Trg b"
            using b by (cases b; simp)
          thus ?thesis
            using assms triangle [of "{c}" "{a}"] ide_eval_Ide comp_assoc
            by (simp add: eval_simps')
        qed
        thus ?thesis
          using assms b HcompNml_Nml_Src [of a] HcompNml_Trg_Nml red2_Nml_Src [of a]
                red2_Trg_Nml
          by (cases b, simp_all)
      qed
      moreover have "[ ¬ is_Prim₀ b; is_Prim₀ c ] ==> ?thesis"
      proof -
        assume b: "¬ is_Prim₀ b"
        assume c: "is_Prim₀ c"
        have "{(a \<lfloor>\<star>\<rfloor> b) \<Down> c} ⋅ ({a \<Down> b} ⋆ {c}) = {(a \<lfloor>\<star>\<rfloor> b) \<Down> Src b} ⋅ ({a \<Down> b} ⋆ src {b})"
          using assms b c by (cases c, simp_all add: eval_simps')
        also have "... = r[{a \<lfloor>\<star>\<rfloor> b}] ⋅ ({a \<Down> b} ⋆ src {b})"
          using assms red2_Nml_Src [of "a \<lfloor>\<star>\<rfloor> b"] Nml_HcompNml(1) Src_HcompNml Ide_HcompNml
          by simp
        also have "... = {a \<Down> b} ⋅ r[{a} ⋆ {b}]"
        proof -
          have "«{a \<Down> b} : {a} ⋆ {b} ==> {a \<lfloor>\<star>\<rfloor> b}¬"
            using assms red2_in_Hom eval_in_hom [of "a \<Down> b"] by simp
          thus ?thesis
            using assms runit_naturality [of "{a \<Down> b}"] arr_dom in_homE src_dom src_hcomp
                  hcomp_simps(1)
            by (elim in_homE, metis)
        qed
        also have "... = ({a \<Down> (b \<lfloor>\<star>\<rfloor> c)} ⋅ ({a} ⋆ {b \<Down> c})) ⋅ a[{a}, {b}, {c}]"
        proof -
          have "({a \<Down> (b \<lfloor>\<star>\<rfloor> c)} ⋅ ({a} ⋆ {b \<Down> c})) ⋅ a[{a}, {b}, {c}] =
                             ({a \<Down> b} ⋅ ({a} ⋆ r[{b}])) ⋅ a[{a}, {b}, src {b}]"
            using assms c red2_Nml_Src [of b]
            by (cases c, simp_all add: eval_simps')
          thus ?thesis
            using assms runit_hcomp ide_eval_Ide comp_assoc
            by (simp add: eval_simps')
        qed
        finally show ?thesis by blast
      qed
      moreover have "[ ¬ is_Prim₀ b; ¬ is_Prim₀ c ] ==> ?thesis"
      proof -
        assume b': "¬ is_Prim₀ b"
        hence b: "Ide b ∧ Nml b ∧ Arr b ∧ ¬ is_Prim₀ b ∧
                  ide {b} ∧ arr {b} ∧ \<lfloor>b\<rfloor> = b ∧ b\<down> = b ∧ Dom b = b ∧ Cod b = b"
          using assms Ide_Nmlize_Ide Ide_in_Hom ide_eval_Ide by simp
        assume c': "¬ is_Prim₀ c"
        hence c: "Ide c ∧ Nml c ∧ Arr c ∧ ¬ is_Prim₀ c ∧
                  ide {c} ∧ arr {c} ∧ \<lfloor>c\<rfloor> = c ∧ c\<down> = c ∧ Dom c = c ∧ Cod c = c"
          using assms Ide_Nmlize_Ide Ide_in_Hom ide_eval_Ide by simp
        have "∧a. Ide a ∧ Nml a ∧ Src a = Trg b ==>
                   {(a \<lfloor>\<star>\<rfloor> b) \<Down> c} ⋅ ({a \<Down> b} ⋆ {c})
                      = ({a \<Down> (b \<lfloor>\<star>\<rfloor> c)} ⋅ ({a} ⋆ {b \<Down> c})) ⋅ a[{a}, {b}, {c}]"
        proof -
          fix a :: "'c term"
          show "Ide a ∧ Nml a ∧ Src a = Trg b ==>
                {(a \<lfloor>\<star>\<rfloor> b) \<Down> c} ⋅ ({a \<Down> b} ⋆ {c})
                   = ({a \<Down> (b \<lfloor>\<star>\<rfloor> c)} ⋅ ({a} ⋆ {b \<Down> c})) ⋅ a[{a}, {b}, {c}]"
            apply (induct a)
            using b c HcompNml_in_Hom
                     apply (simp_all add: HcompNml_Nml_Src HcompNml_Trg_Nml)
          proof -
            fix f
            assume f: "C.ide f ∧ C.arr f ∧ \<langle>src_C f\<rangle>₀ = Trg b"
            show "{(\<langle>f\<rangle> \<star> b) \<Down> c} ⋅ ({\<langle>f\<rangle> \<Down> b} ⋆ {c}) =
                    ({\<langle>f\<rangle> \<Down> b \<lfloor>\<star>\<rfloor> c} ⋅ (E f ⋆ {b \<Down> c})) ⋅ a[E f, {b}, {c}]"
            proof -
              have "{(\<langle>f\<rangle> \<star> b) \<Down> c} ⋅ ({\<langle>f\<rangle> \<Down> b} ⋆ {c}) =
                      ((E f ⋆ {b \<lfloor>\<star>\<rfloor> c}) ⋅ (E f ⋆ {b \<Down> c}) ⋅ a[E f, {b}, {c}]) ⋅
                      ((E f ⋆ {b}) ⋆ {c})"
              proof -
                have "((E f ⋆ {b \<lfloor>\<star>\<rfloor> c}) ⋅ (E f ⋆ {b \<Down> c}) ⋅ a[E f, {b}, {c}]) ⋅
                      ((E f ⋆ {b}) ⋆ {c}) =
                      ((E f ⋆ {b \<lfloor>\<star>\<rfloor> c}) ⋅ (E f ⋆ {b \<Down> c}) ⋅ a[E f, {b}, {c}]) ⋅
                      ({\<langle>f\<rangle> \<Down> b} ⋆ {c})"
                  using f b red2_Nml by simp
                also have "... = ({\<langle>f\<rangle> \<Down> b \<lfloor>\<star>\<rfloor> c} ⋅ (E f ⋆ {b \<Down> c}) ⋅ a[E f, {b}, {c}]) ⋅
                                 ({\<langle>f\<rangle> \<Down> b} ⋆ {c})"
                proof -
                  have "{\<langle>f\<rangle> \<Down> b \<lfloor>\<star>\<rfloor> c} = E f ⋆ {b \<lfloor>\<star>\<rfloor> c}"
                    using assms(5) b c is_Hcomp_HcompNml red2_Nml Nml_HcompNml(1)
                          is_Hcomp_def
                    by (metis eval.simps(2) eval.simps(3) red2.simps(4))
                  thus ?thesis by argo
                qed
                also have "... = {(\<langle>f\<rangle> \<star> b) \<Down> c} ⋅ ({\<langle>f\<rangle> \<Down> b} ⋆ {c})"
                  using b c α_def by (cases c, simp_all)
                finally show ?thesis by argo
              qed
              also have "... = ((E f ⋆ {b \<lfloor>\<star>\<rfloor> c}) ⋅ (E f ⋆ {b \<Down> c})) ⋅ a[E f, {b}, {c}]"
              proof -
                have "src (E f) = trg {b}"
                  using b f preserves_src
                  by (cases "Trg b", auto simp add: eval_simps')
                thus ?thesis
                  using assms b c f comp_arr_dom comp_assoc
                  by (auto simp add: eval_simps')
              qed
              also have "... = ({\<langle>f\<rangle> \<Down> (b \<lfloor>\<star>\<rfloor> c)} ⋅ (E f ⋆ {b \<Down> c})) ⋅ a[E f, {b}, {c}]"
                using assms f b c Ide_HcompNml Nml_HcompNml is_Hcomp_HcompNml [of b c] α_def
                by (cases "b \<lfloor>\<star>\<rfloor> c") simp_all
              finally show ?thesis by blast
            qed
            next
            fix x
            assume x: "C.obj x ∧ \<langle>x\<rangle>₀ = Trg b"
            show "{b \<Down> c} ⋅ ({Trg b \<Down> b} ⋆ {c}) =
                  ({Trg b \<Down> b \<lfloor>\<star>\<rfloor> c} ⋅ ({Trg b} ⋆ {b \<Down> c})) ⋅ a[{Trg b}, {b}, {c}]"
            proof -
              have 1: "Trg (b \<lfloor>\<star>\<rfloor> c) = Trg b"
                using assms b c Trg_HcompNml by blast
              have 2: "{Trg b \<Down> b \<lfloor>\<star>\<rfloor> c} = l[{b \<lfloor>\<star>\<rfloor> c}]"
                using assms b c 1 Nml_HcompNml red2_Trg_Nml [of "b \<lfloor>\<star>\<rfloor> c"] Ide_HcompNml
                by simp
              have "{b \<Down> c} ⋅ ({Trg b \<Down> b} ⋆ {c}) = {b \<Down> c} ⋅ (l[{b}] ⋆ {c})"
                using b c 1 2 HcompNml_Trg_Nml red2_Trg_Nml Trg_HcompNml by simp
              also have "... = {b \<Down> c} ⋅ l[{b} ⋆ {c}] ⋅ a[{Trg b}, {b}, {c}]"
                using assms b c lunit_hcomp [of "{b}" "{c}"]
                by (metis (no_types, lifting) eval_simps'(3) eval_simps(2))
              also have "... = ({b \<Down> c} ⋅ l[{b} ⋆ {c}]) ⋅ a[{Trg b}, {b}, {c}]"
                using comp_assoc by simp
              also have "... = (l[{b \<lfloor>\<star>\<rfloor> c}] ⋅ ({Trg b} ⋆ {b \<Down> c})) ⋅ a[{Trg b}, {b}, {c}]"
                using assms b c lunit_naturality [of "{b \<Down> c}"] red2_in_Hom
                by (simp add: eval_simps')
              also have "... = ({Trg b \<Down> b \<lfloor>\<star>\<rfloor> c} ⋅ ({Trg b} ⋆ {b \<Down> c})) ⋅ a[{Trg b}, {b}, {c}]"
                using b c 1 2 HcompNml_Trg_Nml red2_Trg_Nml Trg_HcompNml comp_assoc
                by simp
              finally show ?thesis
                by blast
            qed
            next
            fix d e
            assume I: "Nml e ==> {(e \<lfloor>\<star>\<rfloor> b) \<Down> c} ⋅ ({e \<Down> b} ⋆ {c})
                                    = ({e \<Down> b \<lfloor>\<star>\<rfloor> c} ⋅ ({e} ⋆ {b \<Down> c})) ⋅ a[{e}, {b}, {c}]"
            assume de: "Ide d ∧ Ide e ∧ Src d = Trg e ∧ Nml (d \<star> e) ∧ Src e = Trg b"
            show "{((d \<star> e) \<lfloor>\<star>\<rfloor> b) \<Down> c} ⋅ ({(d \<star> e) \<Down> b} ⋆ {c})
                    = ({(d \<star> e) \<Down> (b \<lfloor>\<star>\<rfloor> c)} ⋅ (({d} ⋆ {e}) ⋆ {b \<Down> c})) ⋅ a[{d} ⋆ {e}, {b}, {c}]"
            proof -
              let ?f = "un_Prim d"
              have "is_Prim d"
                using de Nml_HcompD
                by (metis term.disc(12))
              hence "d = \<langle>?f\<rangle> ∧ C.ide ?f"
                using de by (cases d; simp)
              hence d: "Ide d ∧ Arr d ∧ Dom d = d ∧ Cod d = d ∧ Nml d ∧
                        d = \<langle>?f\<rangle> ∧ C.ide ?f ∧ ide {d} ∧ arr {d}"
                using de ide_eval_Ide Nml_Nmlize(1) Ide_in_Hom Nml_HcompD [of d e]
                by simp
              have "Nml e ∧ ¬ is_Prim₀ e"
                using de Nml_HcompD by metis
              hence e: "Ide e ∧ Arr e ∧ Dom e = e ∧ Cod e = e ∧ Nml e ∧
                        ¬ is_Prim₀ e ∧ ide {e} ∧ arr {e}"
                using de Ide_in_Hom ide_eval_Ide by simp
              have 1: "is_Hcomp (e \<lfloor>\<star>\<rfloor> b) ∧ is_Hcomp (b \<lfloor>\<star>\<rfloor> c) ∧ is_Hcomp (e \<lfloor>\<star>\<rfloor> b \<lfloor>\<star>\<rfloor> c)"
                using assms b c e de is_Hcomp_HcompNml [of e b] Nml_HcompNml
                      is_Hcomp_HcompNml [of b c] is_Hcomp_HcompNml [of e "b \<lfloor>\<star>\<rfloor> c"]
                by auto
              have eb: "Src e = Trg b"
                using assms b c e de by argo
              have bc: "Src b = Trg c"
                using assms b c by simp
              have 4: "is_Hcomp ((e \<lfloor>\<star>\<rfloor> b) \<lfloor>\<star>\<rfloor> c)"
                using assms b c e eb de 1 is_Hcomp_HcompNml [of e b]
                      is_Hcomp_HcompNml [of "e \<lfloor>\<star>\<rfloor> b" c] is_Hcomp_HcompNml [of e b]
                      Nml_HcompNml(1) [of e b] Src_HcompNml
                by auto
              have "{((d \<star> e) \<lfloor>\<star>\<rfloor> b) \<Down> c} ⋅ ({(d \<star> e) \<Down> b} ⋆ {c})
                      = (({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<lfloor>\<star>\<rfloor> c}) ⋅ ({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<Down> c}) ⋅
                         a[{d}, {e \<lfloor>\<star>\<rfloor> b}, {c}]) ⋅
                        (({d} ⋆ {e \<lfloor>\<star>\<rfloor> b}) ⋅ ({d} ⋆ {e \<Down> b}) ⋅ a[{d}, {e}, {b}] ⋆ {c})"
              proof -
                have "{((d \<star> e) \<lfloor>\<star>\<rfloor> b) \<Down> c}
                         = ({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<lfloor>\<star>\<rfloor> c}) ⋅ ({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<Down> c}) ⋅
                           a[{d}, {e \<lfloor>\<star>\<rfloor> b}, {c}]"
                proof -
                  have "((d \<star> e) \<lfloor>\<star>\<rfloor> b) \<Down> c = (d \<star> (e \<lfloor>\<star>\<rfloor> b)) \<Down> c"
                    using b c d e de 1 HcompNml_Nml Nml_HcompNml HcompNml_assoc
                          HcompNml_Prim
                    by (metis term.distinct_disc(4))
                  also have "... = (d \<Down> ((e \<lfloor>\<star>\<rfloor> b) \<lfloor>\<star>\<rfloor> c)) \<cdot> (d \<star> ((e \<lfloor>\<star>\<rfloor> b) \<Down> c)) \<cdot>
                                   \<a>[d, e \<lfloor>\<star>\<rfloor> b, c]"
                    using b c d e de 1 Nml_HcompNml Nmlize_Nml
                    by (cases c) simp_all
                  also have "... = (d \<star> ((e \<lfloor>\<star>\<rfloor> b) \<lfloor>\<star>\<rfloor> c)) \<cdot> (d \<star> ((e \<lfloor>\<star>\<rfloor> b) \<Down> c)) \<cdot>
                                   \<a>[d, e \<lfloor>\<star>\<rfloor> b, c]"
                    using d 4
                    apply (cases d, simp_all)
                    by (cases "(e \<lfloor>\<star>\<rfloor> b) \<lfloor>\<star>\<rfloor> c") simp_all
                  finally show ?thesis
                    using b c d e HcompNml_in_Hom red2_in_Hom
                          Nml_HcompNml Ide_HcompNml α_def
                    by simp
                qed
                moreover have "{(d \<star> e) \<Down> b}
                                 = ({d} ⋆ {e \<lfloor>\<star>\<rfloor> b}) ⋅ ({d} ⋆ {e \<Down> b}) ⋅ a[{d}, {e}, {b}]"
                proof -
                  have "(d \<star> e) \<Down> b = (d \<Down> (e \<lfloor>\<star>\<rfloor> b)) \<cdot> (d \<star> (e \<Down> b)) \<cdot> \<a>[d, e, b]"
                      using b c d e de 1 HcompNml_Prim Nmlize_Nml
                      by (cases b, simp_all)
                  also have "... = (d \<star> (e \<lfloor>\<star>\<rfloor> b)) \<cdot> (d \<star> (e \<Down> b)) \<cdot> \<a>[d, e, b]"
                    using b c d e de 1 HcompNml_Nml Nml_HcompNml
                    apply (cases d, simp_all)
                    by (cases "e \<lfloor>\<star>\<rfloor> b", simp_all)
                  finally show ?thesis
                    using b d e HcompNml_in_Hom red2_in_Hom α_def by simp
                qed
                ultimately show ?thesis by argo
              qed
              also have "... = (({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<Down> c}) ⋅ a[{d}, {e \<lfloor>\<star>\<rfloor> b}, {c}]) ⋅
                               (({d} ⋆ {e \<Down> b}) ⋆ {c}) ⋅ (a[{d}, {e}, {b}] ⋆ {c})"
              proof -
                have "({d} ⋆ {e \<lfloor>\<star>\<rfloor> b}) ⋅ ({d} ⋆ {e \<Down> b}) ⋅ a[{d}, {e}, {b}] ⋆ {c}
                        = (({d} ⋆ {e \<Down> b}) ⋆ {c}) ⋅ (a[{d}, {e}, {b}] ⋆ {c})"
                  using assms b c d e de eb HcompNml_in_Hom red2_in_Hom comp_cod_arr
                        Ide_HcompNml Nml_HcompNml comp_assoc
                        interchange [of "{d} ⋆ {e \<Down> b}" "a[{d}, {e}, {b}]" "{c}" "{c}"]
                  by (auto simp add: eval_simps')
                moreover have "({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<lfloor>\<star>\<rfloor> c}) ⋅ ({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<Down> c}) ⋅
                                 a[{d}, {e \<lfloor>\<star>\<rfloor> b}, {c}] =
                               ({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<Down> c}) ⋅ a[{d}, {e \<lfloor>\<star>\<rfloor> b}, {c}]"
                proof -
                  have "({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<lfloor>\<star>\<rfloor> c}) ⋅ ({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<Down> c}) ⋅
                                   a[{d}, {e \<lfloor>\<star>\<rfloor> b}, {c}] =
                                   (({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<lfloor>\<star>\<rfloor> c}) ⋅ ({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<Down> c})) ⋅
                                   a[{d}, {e \<lfloor>\<star>\<rfloor> b}, {c}]"
                    using comp_assoc by simp
                  thus ?thesis
                    using assms b c d e de eb HcompNml_in_Hom red2_in_Hom
                          Ide_HcompNml Nml_HcompNml comp_cod_arr
                    by (simp add: eval_simps')
                qed
                ultimately show ?thesis by argo
              qed
              also have "... = ({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<Down> c}) ⋅ ({d} ⋆ ({e \<Down> b} ⋆ {c})) ⋅
                               a[{d}, {e} ⋆ {b}, {c}] ⋅ (a[{d}, {e}, {b}] ⋆ {c})"
                using assms b c d e de HcompNml_in_Hom red2_in_Hom
                      Ide_HcompNml Nml_HcompNml ide_eval_Ide
                      assoc_naturality [of "{d}" "{e \<Down> b}" "{c}"]
                      comp_permute [of "a[{d}, {e \<lfloor>\<star>\<rfloor> b}, {c}]" "({d} ⋆ {e \<Down> b}) ⋆ {c}"
                                       "{d} ⋆ ({e \<Down> b} ⋆ {c})" "a[{d}, {e} ⋆ {b}, {c}]"]
                      comp_assoc
                by (simp add: eval_simps')
              also have "... = (({d} ⋆ {(e \<lfloor>\<star>\<rfloor> b) \<Down> c}) ⋅ ({d} ⋆ ({e \<Down> b} ⋆ {c}))) ⋅
                               a[{d}, {e} ⋆ {b}, {c}] ⋅ (a[{d}, {e}, {b}] ⋆ {c})"
                using comp_assoc by simp
              also have "... = ((({d} ⋆ {e \<Down> (b \<lfloor>\<star>\<rfloor> c)}) ⋅ ({d} ⋆ {e} ⋆ {b \<Down> c})) ⋅
                                ({d} ⋆ a[{e}, {b}, {c}])) ⋅
                               a[{d}, {e} ⋆ {b}, {c}] ⋅ (a[{d}, {e}, {b}] ⋆ {c})"
                using assms b c d e de eb I HcompNml_in_Hom red2_in_Hom
                      Ide_HcompNml Nml_HcompNml whisker_left [of "{d}"]
                      interchange [of "{d}" "{d}" "{(e \<lfloor>\<star>\<rfloor> b) \<Down> c}" "{e \<Down> b} ⋆ {c}"]
                by (auto simp add: eval_simps')
              also have "... = (({d} ⋆ {e \<Down> (b \<lfloor>\<star>\<rfloor> c)}) ⋅ ({d} ⋆ {e} ⋆ {b \<Down> c})) ⋅
                               (({d} ⋆ a[{e}, {b}, {c}]) ⋅
                                a[{d}, {e} ⋆ {b}, {c}] ⋅ (a[{d}, {e}, {b}] ⋆ {c}))"
                using comp_assoc by simp
              also have "... = (({d} ⋆ {e \<Down> (b \<lfloor>\<star>\<rfloor> c)}) ⋅ ({d} ⋆ ({e} ⋆ {b \<Down> c}))) ⋅
                               a[{d}, {e}, {b} ⋆ {c}] ⋅ a[{d} ⋆ {e}, {b}, {c}]"
                using assms b c d e de pentagon
                by (simp add: eval_simps')
              also have "... = ({d} ⋆ {e \<Down> (b \<lfloor>\<star>\<rfloor> c)}) ⋅
                               (({d} ⋆ ({e} ⋆ {b \<Down> c})) ⋅ a[{d}, {e}, {b} ⋆ {c}]) ⋅
                               a[{d} ⋆ {e}, {b}, {c}]"
                using comp_assoc by simp
              also have "... = (({d} ⋆ {e \<lfloor>\<star>\<rfloor> b \<lfloor>\<star>\<rfloor> c}) ⋅ ({d} ⋆ {e \<Down> b \<lfloor>\<star>\<rfloor> c})) ⋅
                               (a[{d}, {e}, {b \<lfloor>\<star>\<rfloor> c}] ⋅ (({d} ⋆ {e}) ⋆ {b \<Down> c})) ⋅
                               a[{d} ⋆ {e}, {b}, {c}]"
                using assms d e de HcompNml_in_Hom red2_in_Hom Ide_HcompNml Nml_HcompNml
                      assoc_naturality [of "{d}" "{e}" "{b \<Down> c}"] comp_cod_arr [of "{d} ⋆ {e \<Down> b \<lfloor>\<star>\<rfloor> c}"]
                by (simp add: eval_simps')
              also have "... = (({d} ⋆ {e \<lfloor>\<star>\<rfloor> b \<lfloor>\<star>\<rfloor> c}) ⋅ ({d} ⋆ {e \<Down> b \<lfloor>\<star>\<rfloor> c}) ⋅
                                a[{d}, {e}, {b \<lfloor>\<star>\<rfloor> c}]) ⋅
                               (({d} ⋆ {e}) ⋆ {b \<Down> c}) ⋅ a[{d} ⋆ {e}, {b}, {c}]"
                using comp_assoc by simp
              also have "... = {(d \<star> e) \<Down> (b \<lfloor>\<star>\<rfloor> c)} ⋅ (({d} ⋆ {e}) ⋆ {b \<Down> c}) ⋅
                               a[{d} ⋆ {e}, {b}, {c}]"
              proof -
                have "{(d \<star> e) \<Down> (b \<lfloor>\<star>\<rfloor> c)}
                         = ({d} ⋆ {e \<lfloor>\<star>\<rfloor> (b \<lfloor>\<star>\<rfloor> c)}) ⋅ ({d} ⋆ {e \<Down> (b \<lfloor>\<star>\<rfloor> c)}) ⋅
                           a[{d}, {e}, {b \<lfloor>\<star>\<rfloor> c}]"
                proof -
                  have "(d \<star> e) \<Down> (b \<lfloor>\<star>\<rfloor> c)
                          = (d \<Down> (e \<lfloor>\<star>\<rfloor> \<lfloor>b \<lfloor>\<star>\<rfloor> c\<rfloor>)) \<cdot> (d \<star> (e \<Down> (b \<lfloor>\<star>\<rfloor> c))) \<cdot> \<a>[d, e, b \<lfloor>\<star>\<rfloor> c]"
                    using e 1 by (cases "b \<lfloor>\<star>\<rfloor> c") auto
                  also have "... = (d \<Down> (e \<lfloor>\<star>\<rfloor> (b \<lfloor>\<star>\<rfloor> c))) \<cdot> (d \<star> (e \<Down> (b \<lfloor>\<star>\<rfloor> c))) \<cdot>
                                   \<a>[d, e, b \<lfloor>\<star>\<rfloor> c]"
                    using assms Nml_HcompNml Nmlize_Nml by simp
                  also have "... = (d \<star> (e \<lfloor>\<star>\<rfloor> (b \<lfloor>\<star>\<rfloor> c))) \<cdot> (d \<star> (e \<Down> (b \<lfloor>\<star>\<rfloor> c))) \<cdot>
                                   \<a>[d, e, b \<lfloor>\<star>\<rfloor> c]"
                    using d 1
                    apply (cases "e \<lfloor>\<star>\<rfloor> b \<lfloor>\<star>\<rfloor> c", simp_all)
                    by (cases d, simp_all)
                  finally show ?thesis
                    using α_def by simp
                qed
                thus ?thesis by simp
              qed
              also have "... = ({(d \<star> e) \<Down> (b \<lfloor>\<star>\<rfloor> c)} ⋅ (({d} ⋆ {e}) ⋆ {b \<Down> c})) ⋅
                               a[{d} ⋆ {e}, {b}, {c}]"
                 using comp_assoc by simp
              finally show ?thesis by auto
            qed
          qed
        qed
        thus ?thesis using assms(1,4) by blast
      qed
      ultimately show ?thesis by blast
    qed

    lemma coherent_Assoc_Ide:
    assumes "Ide a" and "Ide b" and "Ide c" and "Src a = Trg b" and "Src b = Trg c"
    shows "coherent \<a>[a, b, c]"
    proof -
      have a: "Ide a ∧ Arr a ∧ Dom a = a ∧ Cod a = a ∧
               ide {a} ∧ ide {\<lfloor>a\<rfloor>} ∧ {a\<down>} ∈ hom {a} {\<lfloor>a\<rfloor>}"
        using assms Ide_in_Hom Ide_Nmlize_Ide ide_eval_Ide red_in_Hom eval_in_hom(2)
        by force
      have b: "Ide b ∧ Arr b ∧ Dom b = b ∧ Cod b = b ∧
               ide {b} ∧ ide {\<lfloor>b\<rfloor>} ∧ {b\<down>} ∈ hom {b} {\<lfloor>b\<rfloor>}"
        using assms Ide_in_Hom Ide_Nmlize_Ide ide_eval_Ide red_in_Hom(2)
              eval_in_hom(2) [of "b\<down>"]
        by auto
      have c: "Ide c ∧ Arr c ∧ Dom c = c ∧ Cod c = c ∧
               ide {c} ∧ ide {\<lfloor>c\<rfloor>} ∧ {c\<down>} ∈ hom {c} {\<lfloor>c\<rfloor>}"
        using assms Ide_in_Hom Ide_Nmlize_Ide red_in_Hom eval_in_hom(2) [of "c\<down>"]
              ide_eval_Ide
        by auto
      have "{Cod \<a>[a, b, c]\<down>} ⋅ {\<a>[a, b, c]}
              = ({\<lfloor>a\<rfloor> \<Down> (\<lfloor>b\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>c\<rfloor>)} ⋅ ({\<lfloor>a\<rfloor>} ⋆ {\<lfloor>b\<rfloor> \<Down> \<lfloor>c\<rfloor>}) ⋅ ({a\<down>} ⋆ {b\<down>} ⋆ {c\<down>})) ⋅
                a[{a}, {b}, {c}]"
        using assms a b c red_in_Hom red2_in_Hom Nml_Nmlize Ide_Nmlize_Ide
              α_def eval_red_Hcomp interchange [of "{\<lfloor>a\<rfloor>}" "{a\<down>}"] comp_cod_arr [of "{a\<down>}"]
        by (simp add: eval_simps')
      also have "... = (({\<lfloor>a\<rfloor> \<Down> (\<lfloor>b\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>c\<rfloor>)} ⋅ ({\<lfloor>a\<rfloor>} ⋆ {\<lfloor>b\<rfloor> \<Down> \<lfloor>c\<rfloor>})) ⋅ a[{\<lfloor>a\<rfloor>}, {\<lfloor>b\<rfloor>}, {\<lfloor>c\<rfloor>}]) ⋅
                       (({a\<down>} ⋆ {b\<down>}) ⋆ {c\<down>})"
        using assms red_in_Hom Ide_HcompNml assoc_naturality [of "{a\<down>}" "{b\<down>}" "{c\<down>}"] comp_assoc
        by (simp add: eval_simps')
      also have "... = ({(\<lfloor>a\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>b\<rfloor>) \<Down> \<lfloor>c\<rfloor>} ⋅ ({\<lfloor>a\<rfloor> \<Down> \<lfloor>b\<rfloor>} ⋆ {\<lfloor>c\<rfloor>})) ⋅ (({a\<down>} ⋆ {b\<down>}) ⋆ {c\<down>})"
        using assms Nml_Nmlize Ide_Nmlize_Ide coherence_key_fact by simp
      also have "... = {\<lfloor>\<a>[a, b, c]\<rfloor>} ⋅ {Dom \<a>[a, b, c]\<down>}"
        using assms a b c red_in_Hom red2_in_Hom Ide_Nmlize_Ide
              Nml_Nmlize eval_red_Hcomp HcompNml_assoc
              interchange [of "{\<lfloor>a\<rfloor> \<Down> \<lfloor>b\<rfloor>}" "{a\<down>} ⋆ {b\<down>}" "{\<lfloor>c\<rfloor>}" "{c\<down>}"]
              comp_cod_arr [of "{c\<down>}" "{\<lfloor>c\<rfloor>}"]
        apply (simp add: eval_simps')
      proof -
        have "seq {(\<lfloor>a\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>b\<rfloor>) \<Down> \<lfloor>c\<rfloor>} (({\<lfloor>a\<rfloor> \<Down> \<lfloor>b\<rfloor>} ⋆ {\<lfloor>c\<rfloor>}) ⋅ (({a\<down>} ⋆ {b\<down>}) ⋆ {c\<down>}))"
          using assms c red_in_Hom red2_in_Hom Nml_HcompNml Ide_Nmlize_Ide Ide_HcompNml
                Nml_Nmlize
          by (simp_all add: eval_simps')
        moreover have
            "cod ({(\<lfloor>a\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>b\<rfloor>) \<Down> \<lfloor>c\<rfloor>} ⋅ ({\<lfloor>a\<rfloor> \<Down> \<lfloor>b\<rfloor>} ⋆ {\<lfloor>c\<rfloor>}) ⋅ (({a\<down>} ⋆ {b\<down>}) ⋆ {c\<down>})) =
             {\<lfloor>a\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>b\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>c\<rfloor>}"
          using assms c red_in_Hom red2_in_Hom Nml_HcompNml Ide_Nmlize_Ide Ide_HcompNml
                Nml_Nmlize HcompNml_assoc
          by (simp add: eval_simps')
        ultimately
        show "({(\<lfloor>a\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>b\<rfloor>) \<Down> \<lfloor>c\<rfloor>} ⋅ ({\<lfloor>a\<rfloor> \<Down> \<lfloor>b\<rfloor>} ⋆ {\<lfloor>c\<rfloor>})) ⋅ (({a\<down>} ⋆ {b\<down>}) ⋆ {c\<down>}) =
              {\<lfloor>a\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>b\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>c\<rfloor>} ⋅
                {(\<lfloor>a\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>b\<rfloor>) \<Down> \<lfloor>c\<rfloor>} ⋅ ({\<lfloor>a\<rfloor> \<Down> \<lfloor>b\<rfloor>} ⋆ {\<lfloor>c\<rfloor>}) ⋅ (({a\<down>} ⋆ {b\<down>}) ⋆ {c\<down>})"
         using comp_cod_arr comp_assoc by simp
       qed
       finally show ?thesis by blast
    qed

    lemma coherent_Assoc'_Ide:
    assumes "Ide a" and "Ide b" and "Ide c" and "Src a = Trg b" and "Src b = Trg c"
    shows "coherent \<a>^-1[a, b, c]"
        using assms Ide_implies_Can coherent_Assoc_Ide Inv_Ide coherent_iff_coherent_Inv
              Can.simps(10) Inv.simps(10)
        by presburger

    lemma eval_red2_naturality:
    assumes "Nml t" and "Nml u" and "Src t = Trg u"
    shows "{Cod t \<Down> Cod u} ⋅ ({t} ⋆ {u}) = {t \<lfloor>\<star>\<rfloor> u} ⋅ {Dom t \<Down> Dom u}"
    proof -
      have *: "∧t u. Nml (t \<star> u) ==> arr {t} ∧ arr {u}"
        using Nml_implies_Arr Nml_HcompD
        by (metis eval_simps'(1))
      have "is_Prim₀ t ==> ?thesis"
        using assms Nml_implies_Arr is_Prim0_Trg l.naturality [of "{u}"]
        by (cases t) (simp_all add: eval_simps', cases "Trg t", simp_all)
      moreover have "¬ is_Prim₀ t ∧ is_Prim₀ u ==> ?thesis"
        using assms Nml_implies_Arr eval_red2_Nml_Prim₀ runit_naturality [of "{t}"]
        by (cases u) (simp_all add: eval_simps')
      moreover have "¬ is_Prim₀ t ∧ ¬ is_Prim₀ u ==> ?thesis"
        using assms * Nml_implies_Arr
        apply (induct t, simp_all)
      proof -
        fix f
        assume f: "C.arr f"
        assume "¬ is_Prim₀ u"
        hence u: "¬ is_Prim₀ u ∧
                  Nml u ∧ Nml (Dom u) ∧ Nml (Cod u) ∧ Ide (Dom u) ∧ Ide (Cod u) ∧
                  arr {u} ∧ arr {Dom u} ∧ arr {Cod u} ∧ ide {Dom u} ∧ ide {Cod u}"
          using assms(2) Nml_implies_Arr ide_eval_Ide by simp
        hence 1: "¬ is_Prim₀ (Dom u) ∧ ¬ is_Prim₀ (Cod u)"
          using u by (cases u) simp_all
        assume "\<langle>src_C f\<rangle>₀ = Trg u"
        hence "{\<langle>src_C f\<rangle>₀} = {Trg u}" by simp
        hence fu: "src (E f) = trg {u}"
          using f u preserves_src Nml_implies_Arr
          by (simp add: eval_simps')
        show "{\<langle>C.cod f\<rangle> \<Down> Cod u} ⋅ (E f ⋆ {u}) = (E f ⋆ {u}) ⋅ {\<langle>C.dom f\<rangle> \<Down> Dom u}"
        proof -
          have "{\<langle>C.cod f\<rangle> \<Down> Cod u} = E (C.cod f) ⋆ cod {u}"
            using f u 1 Nml_implies_Arr
            by (cases "Cod u", simp_all add: eval_simps')
          moreover have "{\<langle>C.dom f\<rangle> \<Down> Dom u} = E (C.dom f) ⋆ dom {u}"
            using f u 1 Nml_implies_Arr
            by (cases "Dom u", simp_all add: eval_simps')
          moreover have "«E f ⋆ {u} : E (C.dom f) ⋆ {Dom u} ==> E (C.cod f) ⋆ {Cod u}¬"
            using f u fu Nml_implies_Arr
            apply (intro hcomp_in_vhom)
              apply auto
            by (metis C.src_dom eval_simps(4) preserves_src trg_dom u)
          ultimately show ?thesis
            using f u comp_arr_dom comp_cod_arr
            by (simp add: fu)
        qed
        next
        fix v w
        assume I2: "[ ¬ is_Prim₀ w; Nml w ] ==>
                      {Cod w \<Down> Cod u} ⋅ ({w} ⋆ {u}) = {w \<lfloor>\<star>\<rfloor> u} ⋅ {Dom w \<Down> Dom u}"
        assume "¬ is_Prim₀ u"
        hence u: "¬ is_Prim₀ u ∧ Arr u ∧ Arr (Dom u) ∧ Arr (Cod u) ∧
                  Nml u ∧ Nml (Dom u) ∧ Nml (Cod u) ∧ Ide (Dom u) ∧ Ide (Cod u) ∧
                  arr {u} ∧ arr {Dom u} ∧ arr {Cod u} ∧ ide {Dom u} ∧ ide {Cod u}"
          using assms(2) Nml_implies_Arr ide_eval_Ide by simp
        assume vw: "Nml (v \<star> w)"
        assume wu: "Src w = Trg u"
        let ?f = "un_Prim v"
        have "v = \<langle>?f\<rangle> ∧ C.arr ?f"
          using vw by (metis Nml_HcompD(1) Nml_HcompD(2))
        hence "Arr v ∧ v = \<langle>un_Prim v\<rangle> ∧ C.arr ?f ∧ Nml v" by (cases v; simp)
        hence v: "v = \<langle>?f\<rangle> ∧ C.arr ?f ∧ Arr v ∧ Arr (Dom v) ∧ Arr (Cod v) ∧ Nml v ∧
                  Nml (Dom v) ∧ Nml (Cod v) ∧
                  arr {v} ∧ arr {Dom v} ∧ arr {Cod v} ∧ ide {Dom v} ∧ ide {Cod v}"
          using vw * by (cases v, simp_all)
        have "Nml w ∧ ¬ is_Prim₀ w"
          using vw v by (metis Nml.simps(3))
        hence w: "¬ is_Prim₀ w ∧ Arr w ∧ Arr (Dom w) ∧ Arr (Cod w) ∧
                  Nml w ∧ Nml (Dom w) ∧ Nml (Cod w) ∧
                  Ide (Dom w) ∧ Ide (Cod w) ∧
                  arr {w} ∧ arr {Dom w} ∧ arr {Cod w} ∧ ide {Dom w} ∧ ide {Cod w}"
          using vw * Nml_implies_Arr ide_eval_Ide by simp
        have u': "¬ is_Prim₀ (Dom u) ∧ ¬ is_Prim₀ (Cod u)"
          using u by (cases u, simp_all)
        have w': "¬ is_Prim₀ (Dom w) ∧ ¬ is_Prim₀ (Cod w)"
          using w by (cases w, simp_all)
        have vw': "Src v = Trg w"
          using vw Nml_HcompD(7) by simp
        have X: "Nml (Dom v \<star> (Dom w \<lfloor>\<star>\<rfloor> Dom u))"
          using u u' v w w' wu vw is_Hcomp_HcompNml Nml_HcompNml Nml_Dom
          by (metis Dom.simps(3) Nml.simps(3) term.distinct_disc(3))
        have Y: "Nml (Cod v \<star> (Cod w \<lfloor>\<star>\<rfloor> Cod u))"
          using u u' w w' wu vw is_Hcomp_HcompNml Nml_HcompNml Src_Cod Trg_Cod
          by (metis Cod.simps(3) Nml.simps(3) Nml_Cod term.distinct_disc(3) v)
        show "{(Cod v \<star> Cod w) \<Down> Cod u} ⋅ (({v} ⋆ {w}) ⋆ {u})
                = {(v \<star> w) \<lfloor>\<star>\<rfloor> u} ⋅ {(Dom v \<star> Dom w) \<Down> Dom u}"
        proof -
          have "{(Cod v \<star> Cod w) \<Down> Cod u} ⋅ (({v} ⋆ {w}) ⋆ {u})
                  = ({Cod v \<Down> (Cod w \<lfloor>\<star>\<rfloor> Cod u)} ⋅ ({Cod v} ⋆ {Cod w \<Down> Cod u}) ⋅
                    a[{Cod v}, {Cod w}, {Cod u}]) ⋅ (({v} ⋆ {w}) ⋆ {u})"
          proof -
            have "(Cod v \<star> Cod w) \<Down> Cod u
                    = (Cod v \<Down> (Cod w \<lfloor>\<star>\<rfloor> \<lfloor>Cod u\<rfloor>)) \<cdot> (Cod v \<star> Cod w \<Down> Cod u) \<cdot>
                      \<a>[Cod v, Cod w, Cod u]"
              using u v w by (cases u) simp_all
            hence "{(Cod v \<star> Cod w) \<Down> Cod u}
                     = {Cod v \<Down> (Cod w \<lfloor>\<star>\<rfloor> Cod u)} ⋅ ({Cod v} ⋆ {Cod w \<Down> Cod u}) ⋅
                       a[{Cod v}, {Cod w}, {Cod u}]"
              using u v w α_def by simp
            thus ?thesis by presburger
          qed
          also have "... = (({Cod v} ⋆ {Cod w \<lfloor>\<star>\<rfloor> Cod u}) ⋅ ({Cod v} ⋆ {Cod w \<Down> Cod u}) ⋅
                            a[{Cod v}, {Cod w}, {Cod u}]) ⋅ (({v} ⋆ {w}) ⋆ {u})"
            using u v w Y red2_Nml by simp
          also have "... = (({Cod v} ⋆ {Cod w \<Down> Cod u}) ⋅ a[{Cod v}, {Cod w}, {Cod u}]) ⋅
                           (({v} ⋆ {w}) ⋆ {u})"
            using u v w vw' wu comp_cod_arr red2_in_Hom HcompNml_in_Hom comp_reduce
           by (simp add: eval_simps')
          also have "... = ({Cod v} ⋆ {Cod w \<Down> Cod u}) ⋅ a[{Cod v}, {Cod w}, {Cod u}] ⋅
                           (({v} ⋆ {w}) ⋆ {u})"
            using comp_assoc by simp
          also have "... = ({Cod v} ⋆ {Cod w \<Down> Cod u}) ⋅ ({v} ⋆ {w} ⋆ {u}) ⋅
                           a[{Dom v}, {Dom w}, {Dom u}]"
            using u v w vw' wu assoc_naturality [of "{v}" "{w}" "{u}"]
            by (simp add: eval_simps')
          also have "... = (({Cod v} ⋆ {Cod w \<Down> Cod u}) ⋅ ({v} ⋆ {w} ⋆ {u})) ⋅
                           a[{Dom v}, {Dom w}, {Dom u}]"
            using comp_assoc by simp
          also have
            "... = ({v} ⋆ {w \<lfloor>\<star>\<rfloor> u} ⋅ {Dom w \<Down> Dom u}) ⋅ a[{Dom v}, {Dom w}, {Dom u}]"
            using v w u vw' wu I2 red2_in_Hom HcompNml_in_Hom comp_cod_arr
                  interchange [of "{Cod v}" "{v}" "{Cod w \<Down> Cod u}" "{w} ⋆ {u}"]
            by (simp add: eval_simps')
          also have "... = (({v} ⋆ {w \<lfloor>\<star>\<rfloor> u}) ⋅ ({Dom v} ⋆ {Dom w \<Down> Dom u})) ⋅
                           a[{Dom v}, {Dom w}, {Dom u}]"
            using v w u vw' wu red2_in_Hom HcompNml_in_Hom comp_arr_dom
                  interchange [of "{v}" "{Dom v}" "{w \<lfloor>\<star>\<rfloor> u}" "{Dom w \<Down> Dom u}"]
            by (simp add: eval_simps')
          also have "... = ({v} ⋆ {w \<lfloor>\<star>\<rfloor> u}) ⋅ ({Dom v} ⋆ {Dom w \<Down> Dom u}) ⋅
                           a[{Dom v}, {Dom w}, {Dom u}]"
            using comp_assoc by simp
          also have "... = {v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u} ⋅ ({Dom v} ⋆ {Dom w \<Down> Dom u}) ⋅
                           a[{Dom v}, {Dom w}, {Dom u}]"
            using u u' v w vw' wu is_Hcomp_HcompNml HcompNml_Prim [of "w \<lfloor>\<star>\<rfloor> u" ?f]
            by force
          also have "... = {v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u} ⋅ {Dom v \<lfloor>\<star>\<rfloor> Dom w \<lfloor>\<star>\<rfloor> Dom u} ⋅
                          ({Dom v} ⋆ {Dom w \<Down> Dom u}) ⋅ a[{Dom v}, {Dom w}, {Dom u}]"
          proof -
            have "{v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u} ⋅ ({Dom v} ⋆ {Dom w \<Down> Dom u}) ⋅
                    a[{Dom v}, {Dom w}, {Dom u}] =
                  ({v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u} ⋅ {Dom v \<lfloor>\<star>\<rfloor> Dom w \<lfloor>\<star>\<rfloor> Dom u}) ⋅
                    ({Dom v} ⋆ {Dom w \<Down> Dom u}) ⋅ a[{Dom v}, {Dom w}, {Dom u}]"
              using u v w vw' wu comp_arr_dom Nml_HcompNml HcompNml_in_Hom
              by (simp add: eval_simps')
            also have "... = {v \<lfloor>\<star>\<rfloor> w \<lfloor>\<star>\<rfloor> u} ⋅ {Dom v \<lfloor>\<star>\<rfloor> Dom w \<lfloor>\<star>\<rfloor> Dom u} ⋅
                               ({Dom v} ⋆ {Dom w \<Down> Dom u}) ⋅ a[{Dom v}, {Dom w}, {Dom u}]"
              using comp_assoc by simp
            finally show ?thesis by blast
          qed
          also have "... = {(v \<lfloor>\<star>\<rfloor> w) \<lfloor>\<star>\<rfloor> u} ⋅ {(Dom v \<star> Dom w) \<Down> Dom u}"
          proof -
            have "(Dom v \<star> Dom w) \<Down> Dom u
                     = (Dom v \<Down> (Dom w \<lfloor>\<star>\<rfloor> \<lfloor>Dom u\<rfloor>)) \<cdot> (Dom v \<star> (Dom w \<Down> Dom u)) \<cdot>
                       \<a>[Dom v, Dom w, Dom u]"
              using u u' v w vw' wu by (cases u, simp_all)
            hence
              "{(Dom v \<star> Dom w) \<Down> Dom u}
                     = {Dom v \<Down> (Dom w \<lfloor>\<star>\<rfloor> Dom u)} ⋅ ({Dom v} ⋆ {Dom w \<Down> Dom u}) ⋅
                       a[{Dom v}, {Dom w}, {Dom u}]"
              using u v w α_def by simp
            also have
              "... = {Dom v \<lfloor>\<star>\<rfloor> Dom w \<lfloor>\<star>\<rfloor> Dom u} ⋅ ({Dom v} ⋆ {Dom w \<Down> Dom u}) ⋅
                             a[{Dom v}, {Dom w}, {Dom u}]"
              using X HcompNml_Nml red2_Nml by presburger
            finally have
              "{(Dom v \<star> Dom w) \<Down> Dom u}
                   = {Dom v \<lfloor>\<star>\<rfloor> Dom w \<lfloor>\<star>\<rfloor> Dom u} ⋅ ({Dom v} ⋆ {Dom w \<Down> Dom u}) ⋅
                     a[{Dom v}, {Dom w}, {Dom u}]"
              by blast
            thus ?thesis
              using assms v w vw' wu HcompNml_assoc by presburger
          qed
          finally show ?thesis
            using vw HcompNml_Nml by simp
        qed
      qed
      ultimately show ?thesis by blast
    qed

    lemma coherent_Hcomp:
    assumes "Arr t" and "Arr u" and "Src t = Trg u" and "coherent t" and "coherent u"
    shows "coherent (t \<star> u)"
    proof -
      have t: "Arr t ∧ Ide (Dom t) ∧ Ide (Cod t) ∧ Ide \<lfloor>Dom t\<rfloor> ∧ Ide \<lfloor>Cod t\<rfloor> ∧
               arr {t} ∧ arr {Dom t} ∧ ide {Dom t} ∧ arr {Cod t} ∧ ide {Cod t}"
        using assms Ide_Nmlize_Ide ide_eval_Ide by auto
      have u: "Arr u ∧ Ide (Dom u) ∧ Ide (Cod u) ∧ Ide \<lfloor>Dom u\<rfloor> ∧ Ide \<lfloor>Cod u\<rfloor> ∧
               arr {u} ∧ arr {Dom u} ∧ ide {Dom u} ∧ arr {Cod u} ∧ ide {Cod u}"
        using assms Ide_Nmlize_Ide ide_eval_Ide by auto
      have "{Cod (t \<star> u)\<down>} ⋅ ({t} ⋆ {u})
              = ({\<lfloor>Cod t\<rfloor> \<Down> \<lfloor>Cod u\<rfloor>} ⋅ ({Cod t\<down>} ⋆ {Cod u\<down>})) ⋅ ({t} ⋆ {u})"
        using t u eval_red_Hcomp by simp
      also have "... = {\<lfloor>Cod t\<rfloor> \<Down> \<lfloor>Cod u\<rfloor>} ⋅ ({Cod t\<down>} ⋆ {Cod u\<down>}) ⋅ ({t} ⋆ {u})"
        using comp_assoc by simp
      also have "... = {\<lfloor>Cod t\<rfloor> \<Down> \<lfloor>Cod u\<rfloor>} ⋅ ({\<lfloor>t\<rfloor>} ⋆ {\<lfloor>u\<rfloor>}) ⋅ ({Dom t\<down>} ⋆ {Dom u\<down>})"
        using assms t u Nmlize_in_Hom red_in_Hom
              interchange [of "{Cod t\<down>}" "{t}" "{Cod u\<down>}" "{u}"]
              interchange [of "{\<lfloor>t\<rfloor>}" "{Dom t\<down>}" "{\<lfloor>u\<rfloor>}" "{Dom u\<down>}"]
        by (simp add: eval_simps')
      also have "... = ({\<lfloor>Cod t\<rfloor> \<Down> \<lfloor>Cod u\<rfloor>} ⋅ ({\<lfloor>t\<rfloor>} ⋆ {\<lfloor>u\<rfloor>})) ⋅ ({Dom t\<down>} ⋆ {Dom u\<down>})"
        using comp_assoc by simp
      also have "... = ({\<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor>} ⋅ {\<lfloor>Dom t\<rfloor> \<Down> \<lfloor>Dom u\<rfloor>}) ⋅ ({Dom t\<down>} ⋆ {Dom u\<down>})"
        using assms t u Nml_Nmlize Nmlize_in_Hom
              eval_red2_naturality [of "Nmlize t" "Nmlize u"]
        by simp
      also have "... = {\<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor>} ⋅ {\<lfloor>Dom t\<rfloor> \<Down> \<lfloor>Dom u\<rfloor>} ⋅ ({Dom t\<down>} ⋆ {Dom u\<down>})"
        using comp_assoc by simp
      also have "... = {\<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor>} ⋅ {(Dom t \<star> Dom u)\<down>}"
        using t u eval_red_Hcomp by simp
      finally have "{Cod (t \<star> u)\<down>} ⋅ ({t} ⋆ {u}) = {\<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor>} ⋅ {(Dom t \<star> Dom u)\<down>}"
        by blast
      thus ?thesis using t u by simp
    qed

    lemma coherent_Vcomp:
    assumes "Arr t" and "Arr u" and "Dom t = Cod u"
    and "coherent t" and "coherent u"
    shows "coherent (t \<cdot> u)"
    proof -
      have t: "Arr t ∧ Ide (Dom t) ∧ Ide (Cod t) ∧ Ide \<lfloor>Dom t\<rfloor> ∧ Ide \<lfloor>Cod t\<rfloor> ∧
               arr {t} ∧ arr {Dom t} ∧ ide {Dom t} ∧ arr {Cod t} ∧ ide {Cod t}"
        using assms Ide_Nmlize_Ide ide_eval_Ide by auto
      have u: "Arr u ∧ Ide (Dom u) ∧ Ide (Cod u) ∧ Ide \<lfloor>Dom u\<rfloor> ∧ Ide \<lfloor>Cod u\<rfloor> ∧
               arr {u} ∧ arr {Dom u} ∧ ide {Dom u} ∧ arr {Cod u} ∧ ide {Cod u}"
        using assms Ide_Nmlize_Ide ide_eval_Ide by auto
      have "{Cod (t \<cdot> u)\<down>} ⋅ {t \<cdot> u} = {Cod t\<down>} ⋅ {t} ⋅ {u}"
        using t u by simp
      also have "... = ({Cod t\<down>} ⋅ {t}) ⋅ {u}"
      proof -
        have "seq {Cod t\<down>} {t}"
          using assms t red_in_Hom
          by (intro seqI, auto simp add: eval_simps')
        moreover have "seq {t} {u}"
          using assms t u by (auto simp add: eval_simps')
        ultimately show ?thesis
          using comp_assoc by auto
      qed
      also have "... = {\<lfloor>t \<cdot> u\<rfloor>} ⋅ {Dom (t \<cdot> u)\<down>}"
        using t u assms red_in_Hom Nml_Nmlize comp_assoc
        by (simp add: eval_simps' Nml_implies_Arr eval_VcompNml)
      finally show "coherent (t \<cdot> u)" by blast
    qed

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

    theorem coherence:
    assumes "Arr t"
    shows "coherent t"
    proof -
      have "Arr t ==> coherent t"
      proof (induct t)
        show "∧a. Arr \<langle>a\<rangle>₀ ==> coherent \<langle>a\<rangle>₀" by simp
        show "∧μ. Arr \<langle>μ\<rangle> ==> coherent \<langle>μ\<rangle>" by simp
        fix u v
        show "[ Arr u ==> coherent u; Arr v ==> coherent v ] ==> Arr (u \<star> v)
                  ==> coherent (u \<star> v)"
          using coherent_Hcomp by simp
        show "[ Arr u ==> coherent u; Arr v ==> coherent v ] ==> Arr (u \<cdot> v)
                  ==> coherent (u \<cdot> v)"
          using coherent_Vcomp by simp
        next
        fix t
        assume I: "Arr t ==> coherent t"
        show Lunit: "Arr \<l>[t] ==> coherent \<l>[t]"
          using I Ide_Dom coherent_Lunit_Ide Ide_in_Hom
                coherent_Vcomp [of t "\<l>[Dom t]"] Nmlize_Vcomp_Arr_Dom
                eval_in_hom l.naturality1 [of "{t}"]
          by force
        show Runit: "Arr \<r>[t] ==> coherent \<r>[t]"
          using I Ide_Dom coherent_Runit_Ide Ide_in_Hom ide_eval_Ide
                coherent_Vcomp [of t "\<r>[Dom t]"] Nmlize_Vcomp_Arr_Dom r_ide_simp
                eval_in_hom r.naturality1 [of "{t}"]
          by force
        show "Arr \<l>^-1[t] ==> coherent \<l>^-1[t]"
        proof -
          assume "Arr \<l>^-1[t]"
          hence t: "Arr t" by simp
          have "coherent (\<l>^-1[Cod t] \<cdot> t)"
            using t I Ide_Cod coherent_Lunit'_Ide Ide_in_Hom coherent_Vcomp [of "\<l>^-1[Cod t]" t]
                  Arr.simps(6) Dom.simps(6) Dom_Cod Ide_implies_Arr
            by presburger
          moreover have "{\<l>^-1[t]} = {\<l>^-1[Cod t] \<cdot> t}"
            using t l'.naturality2 [of "{t}"]
            by (simp add: eval_simps(5))
          ultimately show ?thesis
            using t Nmlize_Vcomp_Cod_Arr by simp
        qed
        show "Arr \<r>^-1[t] ==> coherent \<r>^-1[t]"
        proof -
          assume "Arr \<r>^-1[t]"
          hence t: "Arr t" by simp
          have "coherent (\<r>^-1[Cod t] \<cdot> t)"
            using t I Ide_Cod coherent_Runit'_Ide Ide_in_Hom coherent_Vcomp [of "\<r>^-1[Cod t]" t]
                  Arr.simps(8) Dom.simps(8) Dom_Cod Ide_implies_Arr
            by presburger
          moreover have "{\<r>^-1[t]} = {\<r>^-1[Cod t] \<cdot> t}"
            using t r'.naturality2 [of "{t}"]
            by (simp add: eval_simps(5))
          ultimately show ?thesis
            using t Nmlize_Vcomp_Cod_Arr by simp
        qed
        next
        fix t u v
        assume I1: "Arr t ==> coherent t"
        assume I2: "Arr u ==> coherent u"
        assume I3: "Arr v ==> coherent v"
        show "Arr \<a>[t, u, v] ==> coherent \<a>[t, u, v]"
        proof -
          assume tuv: "Arr \<a>[t, u, v]"
          have t: "Arr t" using tuv by simp
          have u: "Arr u" using tuv by simp
          have v: "Arr v" using tuv by simp
          have tu: "Src t = Trg u" using tuv by simp
          have uv: "Src u = Trg v" using tuv by simp
          have "coherent ((t \<star> u \<star> v) \<cdot> \<a>[Dom t, Dom u, Dom v])"
          proof -
            have "Arr (t \<star> u \<star> v) ∧ coherent (t \<star> u \<star> v)"
              using t u v tu uv tuv I1 I2 I3 coherent_Hcomp Arr.simps(3) Trg.simps(3)
              by presburger
            moreover have "Arr \<a>[Dom t, Dom u, Dom v]"
              using t u v tu uv Ide_Dom by simp
            moreover have "coherent \<a>[Dom t, Dom u, Dom v]"
              using t u v tu uv Src_Dom Trg_Dom Ide_Dom coherent_Assoc_Ide by metis
            moreover have "Dom (t \<star> u \<star> v) = Cod \<a>[Dom t, Dom u, Dom v]"
              using t u v by simp
            ultimately show ?thesis
              using t u v coherent_Vcomp by blast
          qed
          moreover have "VPar \<a>[t, u, v] ((t \<star> u \<star> v) \<cdot> \<a>[Dom t, Dom u, Dom v])"
            using t u v tu uv Ide_Dom by simp
          moreover have "\<lfloor>\<a>[t, u, v]\<rfloor> = \<lfloor>(t \<star> u \<star> v) \<cdot> \<a>[Dom t, Dom u, Dom v]\<rfloor>"
          proof -
            have "(\<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>
                     = (\<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>) \<lfloor>\<cdot>\<rfloor> ((\<lfloor>Dom t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>Dom u\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>Dom v\<rfloor>)"
            proof -
              have 1: "Nml \<lfloor>t\<rfloor> ∧ Nml \<lfloor>u\<rfloor> ∧ Nml \<lfloor>v\<rfloor> ∧
                       Dom \<lfloor>t\<rfloor> = \<lfloor>Dom t\<rfloor> ∧ Dom \<lfloor>u\<rfloor> = \<lfloor>Dom u\<rfloor> ∧ Dom \<lfloor>v\<rfloor> = \<lfloor>Dom v\<rfloor>"
                using t u v Nml_Nmlize by blast
              moreover have "Nml (\<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor>)"
                using 1 t u tu Nmlize_Src Nmlize_Trg Nml_HcompNml(1)
                by presburger
              moreover have "∧t. Arr t ==> \<lfloor>t\<rfloor> \<lfloor>\<cdot>\<rfloor> \<lfloor>Dom t\<rfloor> = \<lfloor>t\<rfloor>"
                using t Nmlize_Vcomp_Arr_Dom by simp
              moreover have "Dom \<lfloor>\<a>[t, u, v]\<rfloor> = \<lfloor>Dom \<a>[t, u, v]\<rfloor>"
                using Nml_Nmlize tuv by blast
              ultimately show ?thesis
                using t u v tu uv tuv 1 HcompNml_assoc Nml_HcompNml
                      Nml_Nmlize VcompNml_Nml_Dom [of "(\<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>"]
                by auto
            qed
            thus ?thesis
              using t u v Nmlize_Vcomp_Arr_Dom VcompNml_HcompNml Nml_Nmlize
              by simp
          qed
          moreover have "{\<a>[t, u, v]} = {(t \<star> u \<star> v) \<cdot> \<a>[Dom t, Dom u, Dom v]}"
            using t u v tu uv Ide_Dom comp_cod_arr ide_eval_Ide α_def
            apply (simp add: eval_simps')
            using assoc_naturality1 arr_eval_Arr eval_simps'(2-4) by presburger
          ultimately show "coherent \<a>[t, u, v]" by argo
        qed
        show "Arr \<a>^-1[t, u, v] ==> coherent \<a>^-1[t, u, v]"
        proof -
          assume tuv: "Arr \<a>^-1[t, u, v]"
          have t: "Arr t" using tuv by simp
          have u: "Arr u" using tuv by simp
          have v: "Arr v" using tuv by simp
          have tu: "Src t = Trg u" using tuv by simp
          have uv: "Src u = Trg v" using tuv by simp
          have "coherent (((t \<star> u) \<star> v) \<cdot> \<a>^-1[Dom t, Dom u, Dom v])"
          proof -
            have "Arr ((t \<star> u) \<star> v) ∧ coherent ((t \<star> u) \<star> v)"
              using t u v tu uv tuv I1 I2 I3 coherent_Hcomp Arr.simps(3) Src.simps(3)
              by presburger
            moreover have "Arr \<a>^-1[Dom t, Dom u, Dom v]"
              using t u v tu uv Ide_Dom by simp
            moreover have "coherent \<a>^-1[Dom t, Dom u, Dom v]"
              using t u v tu uv Src_Dom Trg_Dom Ide_Dom coherent_Assoc'_Ide
              by metis
            moreover have "Dom ((t \<star> u) \<star> v) = Cod \<a>^-1[Dom t, Dom u, Dom v]"
              using t u v by simp
            ultimately show ?thesis
              using t u v coherent_Vcomp by metis
          qed
          moreover have "VPar \<a>^-1[t, u, v] (((t \<star> u) \<star> v) \<cdot> \<a>^-1[Dom t, Dom u, Dom v])"
            using t u v tu uv Ide_Dom by simp
          moreover have "\<lfloor>\<a>^-1[t, u, v]\<rfloor> = \<lfloor>((t \<star> u) \<star> v) \<cdot> \<a>^-1[Dom t, Dom u, Dom v]\<rfloor>"
            using t u v tu uv Nmlize_Vcomp_Arr_Dom VcompNml_HcompNml Nml_Nmlize
                  HcompNml_assoc Nml_HcompNml HcompNml_in_Hom
                  VcompNml_Nml_Dom [of "(\<lfloor>t\<rfloor> \<lfloor>\<star>\<rfloor> \<lfloor>u\<rfloor>) \<lfloor>\<star>\<rfloor> \<lfloor>v\<rfloor>"]
            using Nmlize.simps(3-4,10) by presburger
          moreover have "{\<a>^-1[t, u, v]} = {((t \<star> u) \<star> v) \<cdot> \<a>^-1[Dom t, Dom u, Dom v]}"
          proof -
            have 1: "VVV.arr ({t}, {u}, {v})"
              using tuv α'.preserves_reflects_arr arr_eval_Arr eval.simps(10)
              by (metis (no_types, lifting))
            have "{\<a>^-1[t, u, v]} = (({t} ⋆ {u}) ⋆ {v}) ⋅ a^-1[dom {t}, dom {u}, dom {v}]"
            proof -
              have "VVV.arr ({t}, {u}, {v})"
                using tuv α'.preserves_reflects_arr arr_eval_Arr eval.simps(10)
                by (metis (no_types, lifting))
              thus ?thesis
                using t u v α'.naturality1 [of "({t}, {u}, {v})"] HoHV_def a'_def
                      VVV.dom_simp
                by simp
            qed
            also have "... = {((t \<star> u) \<star> v) \<cdot> \<a>^-1[Dom t, Dom u, Dom v]}"
              by (simp add: eval_simps'(4) t u v a'_def)
            finally show ?thesis by blast
          qed
          ultimately show "coherent \<a>^-1[t, u, v]" by argo
        qed
      qed
      thus ?thesis using assms by blast
    qed

    corollary eval_eqI:
    assumes "VPar t u" and "\<lfloor>t\<rfloor> = \<lfloor>u\<rfloor>"
    shows "{t} = {u}"
      using assms coherence canonical_factorization by simp

    text ‹
      The following allows us to prove that two 1-cells in a bicategory are isomorphic
      simply by expressing them as the evaluations of terms having the same normalization.
      The benefits are: (1) we do not have to explicitly exhibit the isomorphism,
      which is canonical and is obtained by evaluating the reductions of the terms
      to their normalizations, and (2) the normalizations can be computed automatically
      by the simplifier.
    ›

    lemma canonically_isomorphicI:
    assumes "f = {t}" and "g = {u}" and "Ide t" and "Ide u" and "\<lfloor>t\<rfloor> = \<lfloor>u\<rfloor>"
    shows "f ≅ g"
    proof -
      have "f ≅ {t}"
        using assms isomorphic_reflexive ide_eval_Ide by blast
      also have "... ≅ {\<lfloor>t\<rfloor>}"
      proof -
        have "«{t\<down>} : {t} ==> {\<lfloor>t\<rfloor>}¬ ∧ iso {t\<down>}"
          using assms(1,3) Can_red iso_eval_Can red_in_Hom(2) eval_in_hom(2) by fastforce
        thus ?thesis
          using isomorphic_def by blast
      qed
      also have "... ≅ {\<lfloor>u\<rfloor>}"
        using assms isomorphic_reflexive
        by (simp add: Ide_Nmlize_Ide ide_eval_Ide)
      also have "... ≅ {u}"
      proof -
        have "«{u\<down>} : {u} ==> {\<lfloor>u\<rfloor>}¬ ∧ iso {u\<down>}"
          using assms(2,4) Can_red iso_eval_Can red_in_Hom(2) eval_in_hom(2) by fastforce
        thus ?thesis
          using isomorphic_def isomorphic_symmetric by blast
      qed
      also have "... ≅ g"
        using assms isomorphic_reflexive ide_eval_Ide by blast
      finally show ?thesis by simp
    qed

  end

end