Theory CanonicalIsos

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

section "Canonical Isomorphisms"

text ‹
  In this section we develop some technology for working with canonical isomorphisms in a bicategory,
  which permits them to be specified simply by giving syntactic terms that evaluate to the
  domain and codomain, rather than often-cumbersome formulas expressed in terms of unitors and
  associators.
›

theory CanonicalIsos
imports Coherence
begin

  context bicategory
  begin

    interpretation bicategorical_language ..
    interpretation E: self_evaluation_map V H 𝖺 𝗂 src trg ..
    notation E.eval ("⦃_⦄")

    text ‹
      The next definition defines ‹can u t›, which denotes the unique canonical isomorphism
      from ‹⦃t⦄› to ‹⦃u⦄›.  The ordering of the arguments of ‹can› has been chosen to be the
      opposite of what was used for ‹hom›.  Having the arguments to ‹can› this way makes it easier
      to see at a glance when canonical isomorphisms are composable.  It could probably be argued
      that ‹hom› should have been defined this way as well, but that choice is somewhat
      well-entrenched by now and the argument for ‹can› is stronger, as it denotes an arrow and
      therefore appears in expressions composed with other arrows, rather than just as a hypothesis
      or conclusion.
    ›

    definition can
    where "can u t ≡ ⦃Inv (u❙↓) ❙⋅ t❙↓⦄"

    subsection "Basic Properties"

    text ‹
      The following develop basic properties of ‹can›.
    ›

    lemma can_in_hom [intro]:
    assumes "Ide t" and "Ide u" and "❙⌊t❙⌋ = ❙⌊u❙⌋"
    shows "«can u t : ⦃t⦄ ⇒ ⦃u⦄»"
    proof -
      let ?v = "Inv (u❙↓) ❙⋅ t❙↓"
      have 1: "Can ?v ∧ Dom ?v = t ∧ Cod ?v = u"
        using assms red_in_Hom Can_red Inv_in_Hom Can_Inv(1) by simp
      show "«can u t : ⦃t⦄ ⇒ ⦃u⦄»"
        unfolding can_def using 1 E.eval_in_hom Can_implies_Arr
        by (metis (no_types, lifting))
    qed

    lemma can_simps [simp]:
    assumes "Ide t" and "Ide u" and "❙⌊t❙⌋ = ❙⌊u❙⌋"
    shows "arr (can u t)" and "dom (can u t) = ⦃t⦄" and "cod (can u t) = ⦃u⦄"
      using assms can_in_hom by auto

    lemma inverse_arrows_can:
    assumes "Ide t" and "Ide u" and "❙⌊t❙⌋ = ❙⌊u❙⌋"
    shows "iso (can u t)" and "inverse_arrows (can u t) (can t u)"
    proof -
      let ?v = "Inv (u❙↓) ❙⋅ t❙↓"
      have 1: "Can ?v ∧ Dom ?v = t ∧ Cod ?v = u"
        using assms red_in_Hom Can_red Inv_in_Hom Can_Inv(1) by simp
      show "iso (can u t)"
        unfolding can_def using 1 E.iso_eval_Can by blast
      show "inverse_arrows (can u t) (can t u)"
      proof (unfold can_def)
        show "inverse_arrows ⦃Inv (u❙↓) ❙⋅ t❙↓⦄ ⦃Inv (t❙↓) ❙⋅ u❙↓⦄"
        proof
          show "ide (⦃Inv (u❙↓) ❙⋅ t❙↓⦄ ⋅ ⦃Inv (t❙↓) ❙⋅ u❙↓⦄)"
          proof -
            have "⦃Inv (u❙↓) ❙⋅ t❙↓⦄ ⋅ ⦃Inv (t❙↓) ❙⋅ u❙↓⦄ = ⦃(Inv (u❙↓) ❙⋅ t❙↓) ❙⋅ (Inv (t❙↓) ❙⋅ u❙↓)⦄"
              by simp
            also have "... = ⦃u⦄"
            proof (intro E.eval_eqI)
              show 2: "VPar ((Inv (u❙↓) ❙⋅ t❙↓) ❙⋅ Inv (t❙↓) ❙⋅ u❙↓) u"
                using assms 1 red_in_Hom Inv_in_Hom Ide_implies_Can Can_Inv Can_implies_Arr
                      Can_red(1)
                by (simp add: Dom_Ide Cod_Ide)
              show "❙⌊(Inv (u❙↓) ❙⋅ t❙↓) ❙⋅ Inv (t❙↓) ❙⋅ u❙↓❙⌋ = ❙⌊u❙⌋"
              proof -
                have 3: "Can (Inv (t❙↓) ❙⋅ u❙↓)"
                  using Arr.simps(4) Can.simps(4) Can_Inv(1) Can_red(1) 2 assms(1) assms(2)
                  by presburger
                have "VSeq (Inv (u❙↓) ❙⋅ t❙↓) (Inv (t❙↓) ❙⋅ u❙↓)"
                  using 2 Arr.simps(4) by blast
                hence "Can (Inv (u❙↓) ❙⋅ t❙↓) ∧ Can (Inv (t❙↓) ❙⋅ u❙↓) ∧
                       Dom (Inv (u❙↓) ❙⋅ t❙↓) = Cod (Inv (t❙↓) ❙⋅ u❙↓)"
                  using 3 1 by metis
                thus ?thesis
                  by (metis (no_types) 2 Can.simps(4) Nmlize_Dom Dom_Ide Ide_Nmlize_Can
                      assms(2))
              qed
            qed
            finally have "⦃Inv (u❙↓) ❙⋅ t❙↓⦄ ⋅ ⦃Inv (t❙↓) ❙⋅ u❙↓⦄ = ⦃u⦄"
              by blast
            moreover have "ide ⦃u⦄"
              using assms E.ide_eval_Ide by simp
            ultimately show ?thesis by simp
          qed
          show "ide (⦃Inv (t❙↓) ❙⋅ u❙↓⦄ ⋅ ⦃Inv (u❙↓) ❙⋅ t❙↓⦄)"
          proof -
            have "⦃Inv (t❙↓) ❙⋅ u❙↓⦄ ⋅ ⦃Inv (u❙↓) ❙⋅ t❙↓⦄ = ⦃(Inv (t❙↓) ❙⋅ u❙↓) ❙⋅ (Inv (u❙↓) ❙⋅ t❙↓)⦄"
              by simp
            also have "... = ⦃t⦄"
            proof (intro E.eval_eqI)
              show 2: "VPar ((Inv (t❙↓) ❙⋅ u❙↓) ❙⋅ Inv (u❙↓) ❙⋅ t❙↓) t"
                using assms 1 red_in_Hom Inv_in_Hom Ide_implies_Can Can_Inv Can_implies_Arr
                      Can_red(1)
                by (simp add: Dom_Ide Cod_Ide)
              show "❙⌊(Inv (t❙↓) ❙⋅ u❙↓) ❙⋅ Inv (u❙↓) ❙⋅ t❙↓❙⌋ = ❙⌊t❙⌋"
                using assms 1 2
                by (metis (full_types) Arr.simps(4) Can.simps(4) Can_Inv(1) Can_red(1)
                    Nml_Nmlize(4) Dom_Ide Ide_Nmlize_Can)
            qed
            finally have "⦃Inv (t❙↓) ❙⋅ u❙↓⦄ ⋅ ⦃Inv (u❙↓) ❙⋅ t❙↓⦄ = ⦃t⦄"
              by blast
            moreover have "ide ⦃t⦄"
              using assms E.ide_eval_Ide by simp
            ultimately show ?thesis by simp
          qed
        qed
      qed
    qed

    lemma inv_can [simp]:
    assumes "Ide t" and "Ide u" and "❙⌊t❙⌋ = ❙⌊u❙⌋"
    shows "inv (can u t) = can t u"
      using assms inverse_arrows_can by (simp add: inverse_unique)

    lemma vcomp_can [simp]:
    assumes "Ide t" and "Ide u" and "Ide v" and "❙⌊t❙⌋ = ❙⌊u❙⌋" and "❙⌊u❙⌋ = ❙⌊v❙⌋"
    shows "can v u ⋅ can u t = can v t"
    proof (unfold can_def)
      have "⦃Inv (v❙↓) ❙⋅ u❙↓⦄ ⋅ ⦃Inv (u❙↓) ❙⋅ t❙↓⦄ = ⦃(Inv (v❙↓) ❙⋅ u❙↓) ❙⋅ (Inv (u❙↓) ❙⋅ t❙↓)⦄"
        using assms by simp
      also have "... = ⦃Inv (v❙↓) ❙⋅ t❙↓⦄"
      proof (intro E.eval_eqI)
        show "VPar ((Inv (v❙↓) ❙⋅ u❙↓) ❙⋅ Inv (u❙↓) ❙⋅ t❙↓) (Inv (v❙↓) ❙⋅ t❙↓)"
          using assms red_in_Hom Inv_in_Hom Ide_implies_Can
          by (simp add: Can_red(1))
        show "❙⌊(Inv (v❙↓) ❙⋅ u❙↓) ❙⋅ Inv (u❙↓) ❙⋅ t❙↓❙⌋ = ❙⌊Inv (v❙↓) ❙⋅ t❙↓❙⌋"
          using assms Can_red(1) Nml_Nmlize(1) Nmlize_Inv Ide_Nmlize_Can
              Ide_implies_Can ‹VPar ((Inv (v❙↓) ❙⋅ u❙↓) ❙⋅ Inv (u❙↓) ❙⋅ t❙↓) (Inv (v❙↓) ❙⋅ t❙↓)›
          apply simp
          by (metis red_simps(4) Nmlize_red Dom_Cod VcompNml_Nml_Dom)
      qed
      finally show "⦃Inv (v❙↓) ❙⋅ u❙↓⦄ ⋅ ⦃Inv (u❙↓) ❙⋅ t❙↓⦄ = ⦃Inv (v❙↓) ❙⋅ t❙↓⦄"
        by blast
    qed

    lemma hcomp_can [simp]:
    assumes "Ide t" and "Ide u" and "Ide v" and "Ide w" and "❙⌊t❙⌋ = ❙⌊u❙⌋" and "❙⌊v❙⌋ = ❙⌊w❙⌋"
    and "Src t = Trg v" and "Src u = Trg w"
    shows "can u t ⋆ can w v = can (u ❙⋆ w) (t ❙⋆ v)"
    proof (unfold can_def)
      have "⦃Inv (u❙↓) ❙⋅ t❙↓⦄ ⋆ ⦃Inv (w❙↓) ❙⋅ v❙↓⦄ = ⦃(Inv (u❙↓) ❙⋅ t❙↓) ❙⋆ (Inv (w❙↓) ❙⋅ v❙↓)⦄"
        using assms by simp
      also have "... = ⦃Inv ((u ❙⋆ w)❙↓) ❙⋅ (t ❙⋆ v)❙↓⦄"
      proof (intro E.eval_eqI)
        show "VPar (Inv (u❙↓) ❙⋅ t❙↓ ❙⋆ Inv (w❙↓) ❙⋅ v❙↓) (Inv ((u ❙⋆ w)❙↓) ❙⋅ (t ❙⋆ v)❙↓)"
        proof -
          have "Arr (Inv ((u ❙⋆ w)❙↓) ❙⋅ (t ❙⋆ v)❙↓)"
          proof -
            have "Ide (u ❙⋆ w)"
              using assms by simp
            hence "Can ((u ❙⋆ w)❙↓)"
              using assms Can_red by blast
            thus ?thesis
              using assms Can.simps(4) Can_Inv(1) Dom_Inv Can_implies_Arr Can_red(1)
                    red_simps(4) Nmlize.simps(3) Ide.simps(3)
              by presburger
          qed
          moreover have "Arr (Inv (u❙↓) ❙⋅ t❙↓ ❙⋆ Inv (w❙↓) ❙⋅ v❙↓)"
            using assms red_in_Hom Inv_in_Hom Ide_implies_Can
            by (simp add: Can_red(1))
          moreover have "Dom (Inv (u❙↓) ❙⋅ t❙↓ ❙⋆ Inv (w❙↓) ❙⋅ v❙↓) =
                         Dom (Inv ((u ❙⋆ w)❙↓) ❙⋅ (t ❙⋆ v)❙↓)"
            using assms red_in_Hom Inv_in_Hom Ide_implies_Can
            by (metis (no_types, lifting) Nml_HcompD(3-4) Dom.simps(3-4) red.simps(3)
                red_Nml)
          moreover have "Cod (Inv (u❙↓) ❙⋅ t❙↓ ❙⋆ Inv (w❙↓) ❙⋅ v❙↓) =
                         Cod (Inv ((u ❙⋆ w)❙↓) ❙⋅ (t ❙⋆ v)❙↓)"
            using assms red_in_Hom Inv_in_Hom Ide_implies_Can red_Nml
            by (simp add: Can_red(1) Cod_Ide)
          ultimately show ?thesis by simp
        qed
        show "❙⌊Inv (u❙↓) ❙⋅ t❙↓ ❙⋆ Inv (w❙↓) ❙⋅ v❙↓❙⌋ = ❙⌊Inv ((u ❙⋆ w)❙↓) ❙⋅ (t ❙⋆ v)❙↓❙⌋"
          using assms Inv_in_Hom Ide_implies_Can Nmlize_Inv Ide_Nmlize_Can Can_red
                red2_Nml
          apply auto
          using VcompNml_HcompNml [of u w u w]
             apply (metis red_simps(4) Nml_HcompD(3-4) Nmlize_Nml red_simps(3) red_Nml)
            apply (metis Nml_HcompD(3-4) Nmlize.simps(3) Nmlize_Nml
              red_simps(3) Ide.simps(3) VcompNml_Nml_Dom red_Nml)
           apply (metis Can_red2(1) red_simps(4) Nml_HcompD(3-4) Nmlize.simps(3)
              Nmlize_Nml VcompNml_Cod_Nml red_Nml)
          using red2_Nml Nmlize_red2 Can_red2(1) Nmlize_Hcomp Dom_Ide Ide_implies_Arr
            VcompNml_Nml_Dom Nml_Nmlize(1) Nml_Nmlize(2) Nml_Nmlize(3)
            Nmlize.simps(3)
          by metis
      qed
      finally show "⦃Inv (u❙↓) ❙⋅ t❙↓⦄ ⋆ ⦃Inv (w❙↓) ❙⋅ v❙↓⦄ = ⦃Inv ((u ❙⋆ w)❙↓) ❙⋅ (t ❙⋆ v)❙↓⦄"
        by blast
    qed

    subsection "Introduction Rules"

    text ‹
      To make the ‹can› notation useful, we need a way to introduce it.
      This is a bit tedious, because in general there can multiple ‹can›
      notations for the same isomorphism, and we have to use the right ones in the
      right contexts, otherwise we won't be able to compose them properly.
      Thankfully, we don't need the inverse versions of the theorems below,
      as they are easily provable from the non-inverse versions using ‹inv_can›.
    ›

    lemma canI_unitor_0:
    assumes "ide f"
    shows "𝗅[f] = can ❙⟨f❙⟩ (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩)"
    and "𝗋[f] = can ❙⟨f❙⟩ (❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0)"
    proof -
      have "can ❙⟨f❙⟩ (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩) = ⦃❙𝗅❙[❙⟨f❙⟩❙]⦄"
        unfolding can_def using assms by (intro E.eval_eqI, simp_all)
      thus 1: "𝗅[f] = can ❙⟨f❙⟩ (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩)"
        using assms by (simp add: 𝔩_ide_simp)
      have "can ❙⟨f❙⟩ (❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0) = ⦃❙𝗋❙[❙⟨f❙⟩❙]⦄"
        unfolding can_def using assms by (intro E.eval_eqI, simp_all)
      thus "𝗋[f] = can ❙⟨f❙⟩ (❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0)"
        using assms by (simp add: 𝔯_ide_simp)
    qed

    lemma canI_unitor_1:
    assumes "obj a"
    shows "𝗅[a] = can ❙⟨a❙⟩⇩0 (❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0)"
    and "𝗋[a] = can ❙⟨a❙⟩⇩0 (❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0)"
    proof -
      have "can ❙⟨a❙⟩⇩0 (❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0) = ⦃❙𝗅❙[❙⟨a❙⟩⇩0❙]⦄"
        unfolding can_def using assms by (intro E.eval_eqI, simp_all)
      thus 1: "𝗅[a] = can ❙⟨a❙⟩⇩0 (❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0)"
        using assms by (auto simp add: 𝔩_ide_simp)
      have "can ❙⟨a❙⟩⇩0 (❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0) = ⦃❙𝗋❙[❙⟨a❙⟩⇩0❙]⦄"
        unfolding can_def using assms by (intro E.eval_eqI, simp_all)
      thus "𝗋[a] = can ❙⟨a❙⟩⇩0 (❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0)"
        using assms by (auto simp add: 𝔯_ide_simp)
    qed

    lemma canI_associator_0:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "𝖺[f, g, h] = can (❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩) ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩)"
    proof -
      have "can (❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩) ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩) = ⦃❙𝖺❙[❙⟨f❙⟩, ❙⟨g❙⟩, ❙⟨h❙⟩❙]⦄"
        unfolding can_def using assms by (intro E.eval_eqI, simp_all)
      thus "𝖺[f, g, h] = can (❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩) ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩)"
        using assms by (simp add: α_def)
    qed

    lemma canI_associator_1:
    assumes "ide f" and "ide g" and "src f = trg g"
    shows "𝖺[trg f, f, g] = can (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ((❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩) ❙⋆ ❙⟨g❙⟩)"
    and "𝖺[f, src f, g] = can (❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0 ❙⋆ ❙⟨g❙⟩) ((❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0) ❙⋆ ❙⟨g❙⟩)"
    and "𝖺[f, g, src g] = can (❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨src g❙⟩⇩0) ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨src g❙⟩⇩0)"
    proof -
      show "𝖺[trg f, f, g] = can (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ((❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩) ❙⋆ ❙⟨g❙⟩)"
      proof -
        have "can (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ((❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩) ❙⋆ ❙⟨g❙⟩) = ⦃❙𝖺❙[❙⟨trg f❙⟩⇩0, ❙⟨f❙⟩, ❙⟨g❙⟩❙]⦄"
          unfolding can_def using assms by (intro E.eval_eqI, simp_all)
        thus ?thesis
          using assms α_def by simp
      qed
      show "𝖺[f, src f, g] = can (❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0 ❙⋆ ❙⟨g❙⟩) ((❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0) ❙⋆ ❙⟨g❙⟩)"
      proof -
        have "can (❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0 ❙⋆ ❙⟨g❙⟩) ((❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0) ❙⋆ ❙⟨g❙⟩) = ⦃❙𝖺❙[❙⟨f❙⟩, ❙⟨src f❙⟩⇩0, ❙⟨g❙⟩❙]⦄"
          unfolding can_def using assms by (intro E.eval_eqI, simp_all)
        thus ?thesis
          using assms α_def by simp
      qed
      show "𝖺[f, g, src g] = can (❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨src g❙⟩⇩0) ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨src g❙⟩⇩0)"
      proof -
        have "can (❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨src g❙⟩⇩0) ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨src g❙⟩⇩0) = ⦃❙𝖺❙[❙⟨f❙⟩, ❙⟨g❙⟩, ❙⟨src g❙⟩⇩0❙]⦄"
          unfolding can_def using assms by (intro E.eval_eqI, simp_all)
        thus ?thesis
          using assms α_def by simp
      qed
    qed

    lemma canI_associator_2:
    assumes "ide f"
    shows "𝖺[trg f, trg f, f] = can (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩) ((❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨trg f❙⟩⇩0) ❙⋆ ❙⟨f❙⟩)"
    and "𝖺[trg f, f, src f] = can (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0) ((❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩) ❙⋆ ❙⟨src f❙⟩⇩0)"
    and "𝖺[f, src f, src f] = can (❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0 ❙⋆ ❙⟨src f❙⟩⇩0) ((❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0) ❙⋆ ❙⟨src f❙⟩⇩0)"
    proof -
      show "𝖺[trg f, trg f, f] = can (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩) ((❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨trg f❙⟩⇩0) ❙⋆ ❙⟨f❙⟩)"
      proof -
        have "can (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩) ((❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨trg f❙⟩⇩0) ❙⋆ ❙⟨f❙⟩) = ⦃❙𝖺❙[❙⟨trg f❙⟩⇩0, ❙⟨trg f❙⟩⇩0, ❙⟨f❙⟩❙]⦄"
          unfolding can_def using assms by (intro E.eval_eqI, simp_all)
        thus ?thesis
          using assms α_def by simp
      qed
      show "𝖺[trg f, f, src f] = can (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0) ((❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩) ❙⋆ ❙⟨src f❙⟩⇩0)"
      proof -
        have "can (❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0) ((❙⟨trg f❙⟩⇩0 ❙⋆ ❙⟨f❙⟩) ❙⋆ ❙⟨src f❙⟩⇩0) = ⦃❙𝖺❙[❙⟨trg f❙⟩⇩0, ❙⟨f❙⟩, ❙⟨src f❙⟩⇩0❙]⦄"
          unfolding can_def using assms by (intro E.eval_eqI, simp_all)
        thus ?thesis
          using assms α_def by simp
      qed
      show "𝖺[f, src f, src f] = can (❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0 ❙⋆ ❙⟨src f❙⟩⇩0) ((❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0) ❙⋆ ❙⟨src f❙⟩⇩0)"
      proof -
        have "can (❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0 ❙⋆ ❙⟨src f❙⟩⇩0) ((❙⟨f❙⟩ ❙⋆ ❙⟨src f❙⟩⇩0) ❙⋆ ❙⟨src f❙⟩⇩0) =
              ⦃❙𝖺❙[❙⟨f❙⟩, ❙⟨src f❙⟩⇩0, ❙⟨src f❙⟩⇩0❙]⦄"
          unfolding can_def using assms by (intro E.eval_eqI, simp_all)
        thus ?thesis
          using assms α_def by simp
      qed
    qed

    lemma canI_associator_3:
    assumes "obj a"
    shows "𝖺[a, a, a] = can (❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0) ((❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0) ❙⋆ ❙⟨a❙⟩⇩0)"
    proof -
      have "can (❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0) ((❙⟨a❙⟩⇩0 ❙⋆ ❙⟨a❙⟩⇩0) ❙⋆ ❙⟨a❙⟩⇩0) = ⦃❙𝖺❙[❙⟨a❙⟩⇩0, ❙⟨a❙⟩⇩0, ❙⟨a❙⟩⇩0❙]⦄"
        unfolding can_def using assms by (intro E.eval_eqI, simp_all)
      thus ?thesis
        using assms α_def by auto
    qed

    lemma canI_associator_hcomp:
    assumes "ide f" and "ide g" and "ide h" and "ide k"
    and "src f = trg g" and "src g = trg h" and "src h = trg k"
    shows "𝖺[f ⋆ g, h, k] = can ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩ ❙⋆ ❙⟨k❙⟩) (((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩) ❙⋆ ❙⟨k❙⟩)"
    and "𝖺[f, g ⋆ h, k] = can (❙⟨f❙⟩ ❙⋆ (❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩) ❙⋆ ❙⟨k❙⟩) ((❙⟨f❙⟩ ❙⋆ (❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩)) ❙⋆ ❙⟨k❙⟩)"
    and "𝖺[f, g, h ⋆ k] = can (❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩ ❙⋆ ❙⟨k❙⟩) ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩ ❙⋆ ❙⟨k❙⟩)"
    proof -
      show "𝖺[f ⋆ g, h, k] = can ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩ ❙⋆ ❙⟨k❙⟩) (((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩) ❙⋆ ❙⟨k❙⟩)"
      proof -
        have "can ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩ ❙⋆ ❙⟨k❙⟩) (((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩) ❙⋆ ❙⟨k❙⟩) =
              (((f ⋆ g) ⋆ h ⋆ k) ⋅ (𝖺⇧-⇧1[f, g, h ⋆ k] ⋅ (f ⋆ g ⋆ h ⋆ k)) ⋅ (f ⋆ g ⋆ h ⋆ k)) ⋅
                ((f ⋆ g ⋆ h ⋆ k) ⋅ (f ⋆ (g ⋆ h ⋆ k) ⋅ (g ⋆ h ⋆ k) ⋅ 𝖺[g, h, k]) ⋅ 𝖺[f, g ⋆ h, k]) ⋅
                  (((f ⋆ g ⋆ h) ⋅ (f ⋆ g ⋆ h) ⋅ 𝖺[f, g, h]) ⋅ ((f ⋆ g) ⋆ h) ⋆ k)"
          unfolding can_def using assms α_def 𝖺'_def α'.map_ide_simp by simp
        also have "... = 𝖺⇧-⇧1[f, g, h ⋆ k] ⋅ (f ⋆ 𝖺[g, h, k]) ⋅ 𝖺[f, g ⋆ h, k] ⋅ (𝖺[f, g, h] ⋆ k)"
          using assms comp_arr_dom comp_cod_arr comp_assoc by simp
        also have "... = 𝖺[f ⋆ g, h, k]"
          using assms pentagon [of f g h k] invert_side_of_triangle(1) α_def α'.map_ide_simp
                assoc_simps(1,4-5) ideD(1) iso_assoc preserves_ide seqI
          by simp
        finally show ?thesis by simp
      qed
      show "𝖺[f, g ⋆ h, k] = can (❙⟨f❙⟩ ❙⋆ (❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩) ❙⋆ ❙⟨k❙⟩) ((❙⟨f❙⟩ ❙⋆ (❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩)) ❙⋆ ❙⟨k❙⟩)"
      proof -
        have "can (❙⟨f❙⟩ ❙⋆ (❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩) ❙⋆ ❙⟨k❙⟩) ((❙⟨f❙⟩ ❙⋆ (❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩)) ❙⋆ ❙⟨k❙⟩) =
              ((f ⋆ ((g ⋆ h) ⋆ k) ⋅ (𝖺⇧-⇧1[g, h, k] ⋅ (g ⋆ h ⋆ k)) ⋅ (g ⋆ h ⋆ k)) ⋅ (f ⋆ g ⋆ h ⋆ k)) ⋅
                ((f ⋆ g ⋆ h ⋆ k) ⋅ (f ⋆ (g ⋆ h ⋆ k) ⋅ (g ⋆ h ⋆ k) ⋅ 𝖺[g, h, k]) ⋅ 𝖺[f, g ⋆ h, k]) ⋅
                  ((f ⋆ g ⋆ h) ⋆ k)"
          unfolding can_def using assms α_def α'.map_ide_simp 𝖺'_def by simp
        also have "... = ((f ⋆ 𝖺⇧-⇧1[g, h, k]) ⋅ (f ⋆ 𝖺[g, h, k])) ⋅ 𝖺[f, g ⋆ h, k]"
          using assms comp_arr_dom comp_cod_arr comp_assoc by simp
        also have "... = 𝖺[f, g ⋆ h, k]"
          using assms comp_cod_arr whisker_left [of f "𝖺⇧-⇧1[g, h, k]" "𝖺[g, h, k]"]
                comp_assoc_assoc'
          by simp
        finally show ?thesis by simp
      qed
      show "𝖺[f, g, h ⋆ k] = can (❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩ ❙⋆ ❙⟨k❙⟩) ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩ ❙⋆ ❙⟨k❙⟩)"
      proof -
        have "can (❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩ ❙⋆ ❙⟨h❙⟩ ❙⋆ ❙⟨k❙⟩) ((❙⟨f❙⟩ ❙⋆ ❙⟨g❙⟩) ❙⋆ ❙⟨h❙⟩ ❙⋆ ❙⟨k❙⟩) =
              (f ⋆ g ⋆ h ⋆ k) ⋅ ((f ⋆ g ⋆ h ⋆ k) ⋅ (f ⋆ g ⋆ h ⋆ k) ⋅ 𝖺[f, g, h ⋆ k]) ⋅ ((f ⋆ g) ⋆ h ⋆ k)"
          unfolding can_def using assms α_def α'.map_ide_simp by simp
        also have "... = 𝖺[f, g, h ⋆ k]"
          using assms comp_arr_dom comp_cod_arr by simp
        finally show ?thesis by simp
      qed
    qed

    subsection "Rules for Eliminating `can'"

    text ‹
      The following rules are used for replacing ‹can› in an expression by terms expressed
      using unit and associativity isomorphisms.  They are not really expressed in the form
      of elimination rules, so the names are perhaps a bit misleading.  They are typically
      applied as simplifications.
    ›

    lemma canE_unitor:
    assumes "Ide f"
    shows "can f (f ❙⋆ Src f) = 𝗋[⦃f⦄]"
    and "can f (Trg f ❙⋆ f) = 𝗅[⦃f⦄]"
    and "can (f ❙⋆ Src f) f = 𝗋⇧-⇧1[⦃f⦄]"
    and "can (Trg f ❙⋆ f) f = 𝗅⇧-⇧1[⦃f⦄]"
    proof -
      show 1: "can f (f ❙⋆ Src f) = 𝗋[⦃f⦄]"
      proof -
        have f: "¬Nml (f ❙⋆ Src f)"
          using assms Nml_HcompD(5) is_Prim0_Src by blast
        have "can f (f ❙⋆ Src f) = ⦃Inv (f❙↓) ❙⋅ (❙⌊f❙⌋ ❙⇓ ❙⌊Src f❙⌋) ❙⋅ (f❙↓ ❙⋆ Src f❙↓)⦄"
          using assms f can_def by simp
        also have "... = ⦃❙𝗋❙[f❙]⦄"
        proof (intro E.eval_eqI)
          show "VPar (Inv (f❙↓) ❙⋅ (❙⌊f❙⌋ ❙⇓ ❙⌊Src f❙⌋) ❙⋅ (f❙↓ ❙⋆ Src f❙↓)) ❙𝗋❙[f❙]"
            using assms Nmlize_in_Hom red_in_Hom red2_in_Hom Inv_in_Hom Can_red Can_implies_Arr
                  Nml_Nmlize(1) Ide_implies_Can Nml_Src Nml_implies_Arr
                  HcompNml_Nml_Src Ide_Cod Obj_implies_Ide
            apply (simp add: Dom_Ide Cod_Ide)
            apply (intro conjI)
          proof -
            assume f: "Ide f"
            have 1: "Nml (Src f)"
            proof -
              have "Ide (Src f)"
                using f Obj_implies_Ide by simp
              thus ?thesis
                using f Obj_Src Nml_Nmlize(1) Nmlize_Src(2) Ide_implies_Arr
                by metis
            qed
            show "Arr (❙⌊f❙⌋ ❙⇓ ❙⌊Src f❙⌋)"
              using f 1 Can_red2 Ide_Nmlize_Ide Nml_Nmlize Obj_implies_Ide by simp
            show "Dom (❙⌊f❙⌋ ❙⇓ ❙⌊Src f❙⌋) = ❙⌊f❙⌋ ❙⋆ ❙⌊Src f❙⌋"
              using f 1 Nml_Nmlize red2_in_Hom Ide_Nmlize_Ide Obj_implies_Ide by auto
            show "❙⌊f❙⌋ = Cod (❙⌊f❙⌋ ❙⇓ ❙⌊Src f❙⌋)"
            proof -
              have "Src ❙⌊f❙⌋ = Trg ❙⌊Src f❙⌋"
                using f Nml_Nmlize Obj_implies_Ide by simp
              moreover have "❙⌊❙⌊f❙⌋ ❙⋆ ❙⌊Src f❙⌋❙⌋ = ❙⌊f❙⌋"
                using f 1 Nml_Nmlize Nmlize_Src HcompNml_Nml_Src Nml_Src
                by (auto simp add: HcompNml_Nml_Obj)
              thus ?thesis
                using f 1 Obj_Src red2_in_Hom [of "❙⌊f❙⌋" "❙⌊Src f❙⌋"] HcompNml_Nml_Src
                      Nml_Nmlize Ide_Nmlize_Ide Obj_implies_Ide
                by auto
            qed
          qed
          show "❙⌊Inv (f❙↓) ❙⋅ (❙⌊f❙⌋ ❙⇓ ❙⌊Src f❙⌋) ❙⋅ (f❙↓ ❙⋆ Src f❙↓)❙⌋ = ❙⌊❙𝗋❙[f❙]❙⌋"
            using assms f HcompNml_Nml_Src Nml_Nmlize Can_red Nmlize_Hcomp
                  Nmlize_Inv Nmlize_Src(1) Nmlize_red Nmlize_red2
                  Ide_Nmlize_Can VcompNml_Nml_Ide red_Src
            apply (simp add: HcompNml_Nml_Obj)
          proof -
            assume f: "Ide f"
            have "❙⌊❙⌊f❙⌋ ❙⇓ Src f❙⌋ = ❙⌊f❙⌋"
            proof -
              have "Obj (Src f)"
                using f Obj_Src by simp
              thus ?thesis
                using f apply (cases "Src f")
                by (simp_all add: Nml_Nmlize(1) Nml_Nmlize(2) Ide_Nmlize_Ide)
            qed
            thus "❙⌊f❙⌋ ❙⌊❙⋅❙⌋ ❙⌊❙⌊f❙⌋ ❙⇓ Src f❙⌋ ❙⌊❙⋅❙⌋ ❙⌊f❙⌋ = ❙⌊f❙⌋"
              by (metis Cod_Inv Can_red(1) Cod.simps(4) Nmlize.simps(4)
                  Nmlize.simps(7) Nmlize_Vcomp_Cod_Arr red_simps(3)
                  ‹VPar (Inv (f❙↓) ❙⋅ (❙⌊f❙⌋ ❙⇓ ❙⌊Src f❙⌋) ❙⋅ (f❙↓ ❙⋆ Src f❙↓)) ❙𝗋❙[f❙]› f)
          qed
        qed
        also have "... = 𝗋[⦃f⦄]"
          using assms E.eval_Runit_Ide by blast
        finally show ?thesis by simp
      qed
      show 2: "can f (Trg f ❙⋆ f) = 𝗅[⦃f⦄]"
      proof -
        have f: "¬Nml (Trg f ❙⋆ f)"
          using assms by (metis Nml.simps(4) Nml_HcompD(6))
        have "can f (Trg f ❙⋆ f) = ⦃Inv (f❙↓) ❙⋅ (❙⌊Trg f❙⌋ ❙⇓ ❙⌊f❙⌋) ❙⋅ (Trg f❙↓ ❙⋆ f❙↓)⦄"
          using assms f can_def by simp
        also have "... = ⦃❙𝗅❙[f❙]⦄"
        proof (intro E.eval_eqI)
          show "VPar (Inv (f❙↓) ❙⋅ (❙⌊Trg f❙⌋ ❙⇓ ❙⌊f❙⌋) ❙⋅ (Trg f❙↓ ❙⋆ f❙↓)) ❙𝗅❙[f❙]"
            using assms Nmlize_in_Hom red_in_Hom red2_in_Hom Inv_in_Hom Can_red Can_implies_Arr
                  Nml_Nmlize(1) Ide_implies_Can Nml_Trg Nml_implies_Arr
                  HcompNml_Trg_Nml Ide_Cod Nmlize_Trg(1) Obj_implies_Ide
            apply (simp add: Dom_Ide Cod_Ide)
            apply (intro conjI)
          proof -
            assume f: "Ide f"
            have 1: "Nml (Trg f)"
            proof -
              have "Ide (Trg f)"
                using f Obj_implies_Ide by simp
              thus ?thesis
                using f Obj_Trg Nml_Nmlize(1) Nmlize_Trg(2) Ide_implies_Arr
                by metis
            qed
            show "Arr (Trg f ❙⇓ ❙⌊f❙⌋)"
              using f 1 Can_red2 Ide_Nmlize_Ide Nml_Nmlize(1,3) Obj_implies_Ide by simp
            show "Dom (Trg f ❙⇓ ❙⌊f❙⌋) = Trg f ❙⋆ ❙⌊f❙⌋"
              using f Obj_Trg 1 Nml_Nmlize(1,3) red2_in_Hom Ide_Nmlize_Ide Obj_implies_Ide by auto
            show "❙⌊f❙⌋ = Cod (Trg f ❙⇓ ❙⌊f❙⌋)"
            proof -
              have "Src (Trg f) = Trg ❙⌊f❙⌋"
                using f Nml_Nmlize(3) by simp
              thus ?thesis
                using f 1 Obj_Trg HcompNml_Trg_Nml Nml_Nmlize(1) Ide_Nmlize_Ide Obj_implies_Ide
                by auto
            qed
          qed
          show "❙⌊Inv (f❙↓) ❙⋅ (❙⌊Trg f❙⌋ ❙⇓ ❙⌊f❙⌋) ❙⋅ (Trg f❙↓ ❙⋆ f❙↓)❙⌋ = ❙⌊❙𝗅❙[f❙]❙⌋"
            using assms f HcompNml_Nml_Src Nml_Nmlize Can_red Nmlize_Hcomp
                  Nmlize_Inv Nmlize_Trg(1) Nmlize_red Nmlize_red2
                  Ide_Nmlize_Can VcompNml_Nml_Ide red_Trg
            apply (simp add: HcompNml_Obj_Nml)
          proof -
            assume f: "Ide f"
            have "❙⌊Trg f ❙⇓ ❙⌊f❙⌋❙⌋ = ❙⌊f❙⌋"
            proof -
              have "Obj (Trg f)"
                using f Obj_Trg by simp
              thus ?thesis
                using f apply (cases "Trg f")
                by (simp_all add: Nml_Nmlize(1) Nml_Nmlize(2) Ide_Nmlize_Ide)
            qed
            thus "❙⌊f❙⌋ ❙⌊❙⋅❙⌋ ❙⌊Trg f ❙⇓ ❙⌊f❙⌋❙⌋ ❙⌊❙⋅❙⌋ ❙⌊f❙⌋ = ❙⌊f❙⌋"
              by (metis Cod_Inv Can_red(1) Cod.simps(4) Nmlize.simps(4)
                  Nmlize.simps(5) Nmlize_Vcomp_Cod_Arr red_simps(3)
                  ‹VPar (Inv (f❙↓) ❙⋅ (❙⌊Trg f❙⌋ ❙⇓ ❙⌊f❙⌋) ❙⋅ (Trg f❙↓ ❙⋆ f❙↓)) ❙𝗅❙[f❙]› f)
          qed
        qed
        also have "... = 𝗅[⦃f⦄]"
          using assms E.eval_Lunit_Ide by blast
        finally show ?thesis by simp
      qed
      show "can (f ❙⋆ Src f) f = 𝗋⇧-⇧1[⦃f⦄]"
        using assms 1 inv_can inv_inv
        by (metis (no_types, lifting) Nml_Nmlize(1) Nmlize.simps(3)
            Nmlize_Src(1) HcompNml_Nml_Src Ide.simps(3) Ide_implies_Arr
            Obj_Src Obj_implies_Ide Trg_Src)
      show "can (Trg f ❙⋆ f) f = 𝗅⇧-⇧1[⦃f⦄]"
        using assms 2 inv_can inv_inv
        by (metis (no_types, lifting) Nml_Nmlize(1) Nmlize.simps(3)
            Nmlize_Trg(1) HcompNml_Trg_Nml Ide.simps(3) Ide_implies_Arr
            Obj_Trg Obj_implies_Ide Src_Trg)
    qed

    lemma canE_associator:
    assumes "Ide f" and "Ide g" and "Ide h" and "Src f = Trg g" and "Src g = Trg h"
    shows "can (f ❙⋆ g ❙⋆ h) ((f ❙⋆ g) ❙⋆ h) = 𝖺[⦃f⦄, ⦃g⦄, ⦃h⦄]"
    and "can ((f ❙⋆ g) ❙⋆ h) (f ❙⋆ g ❙⋆ h) = 𝖺⇧-⇧1[⦃f⦄, ⦃g⦄, ⦃h⦄]"
    proof -
      show "can (f ❙⋆ g ❙⋆ h) ((f ❙⋆ g) ❙⋆ h) = 𝖺[⦃f⦄, ⦃g⦄, ⦃h⦄]"
      proof -
        have "can (f ❙⋆ g ❙⋆ h) ((f ❙⋆ g) ❙⋆ h) = ⦃Inv ((f ❙⋆ g ❙⋆ h)❙↓) ❙⋅ ((f ❙⋆ g) ❙⋆ h)❙↓⦄"
          using can_def by simp
        also have "... = ⦃❙𝖺❙[f, g, h❙]⦄"
        proof (intro E.eval_eqI)
          have 1: "Inv ((f ❙⋆ g ❙⋆ h)❙↓) ❙⋅ ((f ❙⋆ g) ❙⋆ h)❙↓ ∈ VHom ((f ❙⋆ g) ❙⋆ h) (f ❙⋆ g ❙⋆ h)"
            using assms Inv_in_Hom [of "(f ❙⋆ g ❙⋆ h)❙↓"] Can_red [of "f ❙⋆ g ❙⋆ h"]
                  red_in_Hom [of "f ❙⋆ g ❙⋆ h"] red_in_Hom [of "(f ❙⋆ g) ❙⋆ h"]
                  Nmlize_Hcomp_Hcomp Nmlize_Hcomp_Hcomp'
                  Ide_implies_Arr Nml_HcompNml Nmlize_Nml Ide_HcompNml
            by auto
          show par: "VPar (Inv ((f ❙⋆ g ❙⋆ h)❙↓) ❙⋅ ((f ❙⋆ g) ❙⋆ h)❙↓) ❙𝖺❙[f, g, h❙]"
            using assms 1 Inv_in_Hom red_in_Hom Ide_in_Hom by simp
          show "❙⌊Inv ((f ❙⋆ g ❙⋆ h)❙↓) ❙⋅ ((f ❙⋆ g) ❙⋆ h)❙↓❙⌋ = ❙⌊❙𝖺❙[f, g, h❙]❙⌋"
          proof -
            have "❙⌊Inv ((f ❙⋆ g ❙⋆ h)❙↓) ❙⋅ ((f ❙⋆ g) ❙⋆ h)❙↓❙⌋ = Dom ❙⌊Inv ((f ❙⋆ g ❙⋆ h)❙↓) ❙⋅ ((f ❙⋆ g) ❙⋆ h)❙↓❙⌋"
            proof -
              have "Can (Inv ((f ❙⋆ g ❙⋆ h)❙↓) ❙⋅ ((f ❙⋆ g) ❙⋆ h)❙↓)"
                (* Here presburger depends on par being at the end, not after assms. *)
                using assms Nmlize_Inv Can_Inv
                      Arr.simps(10) Arr.simps(4) Can.simps(4) Can_red(1) Ide.simps(3)
                      Src.simps(3) Trg.simps(3) par
                by presburger
              hence "Ide ❙⌊Inv ((f ❙⋆ g ❙⋆ h)❙↓) ❙⋅ ((f ❙⋆ g) ❙⋆ h)❙↓❙⌋"
                using Ide_Nmlize_Can by blast
              thus ?thesis
                using Ide_in_Hom Dom_Ide by presburger
            qed
            also have 6: "... = ❙⌊(f ❙⋆ g) ❙⋆ h❙⌋"
              using 1 Nmlize_Dom [of "Inv ((f ❙⋆ g ❙⋆ h)❙↓) ❙⋅ ((f ❙⋆ g) ❙⋆ h)❙↓"]
              by (metis (mono_tags, lifting) mem_Collect_eq)
            also have 5: "... = Dom ❙⌊❙𝖺❙[f, g, h❙]❙⌋"
              using assms 6 par Nmlize_Dom Nml_Nmlize(4) by metis
            also have "... = ❙⌊❙𝖺❙[f, g, h❙]❙⌋"
              using assms 5 Ide_in_Hom by auto
            finally show ?thesis by simp
          qed
        qed
        also have "... = 𝖺[⦃f⦄, ⦃g⦄, ⦃h⦄]"
          using assms E.eval_Assoc_Ide α_def by fastforce
        finally show ?thesis by simp
      qed
      show "can ((f ❙⋆ g) ❙⋆ h) (f ❙⋆ g ❙⋆ h) = 𝖺⇧-⇧1[⦃f⦄, ⦃g⦄, ⦃h⦄]"
      proof -
        have "can ((f ❙⋆ g) ❙⋆ h) (f ❙⋆ g ❙⋆ h) = ⦃Inv (((f ❙⋆ g) ❙⋆ h)❙↓) ❙⋅ (f ❙⋆ g ❙⋆ h)❙↓⦄"
          using can_def by simp
        also have "... = ⦃❙𝖺⇧-⇧1❙[f, g, h❙]⦄"
        proof (intro E.eval_eqI)
          have 1: "Inv (((f ❙⋆ g) ❙⋆ h)❙↓) ❙⋅ (f ❙⋆ g ❙⋆ h)❙↓ ∈ VHom (f ❙⋆ g ❙⋆ h) ((f ❙⋆ g) ❙⋆ h)"
            using assms Inv_in_Hom [of "((f ❙⋆ g) ❙⋆ h)❙↓"] Can_red [of "(f ❙⋆ g) ❙⋆ h"]
                  red_in_Hom [of "(f ❙⋆ g) ❙⋆ h"] red_in_Hom [of "f ❙⋆ g ❙⋆ h"]
                  Nmlize_Hcomp_Hcomp Nmlize_Hcomp_Hcomp'
                  Ide_implies_Arr Nml_HcompNml Nmlize_Nml Ide_HcompNml
            by auto
          show par: "VPar (Inv (((f ❙⋆ g) ❙⋆ h)❙↓) ❙⋅ (f ❙⋆ g ❙⋆ h)❙↓) ❙𝖺⇧-⇧1❙[f, g, h❙]"
            using assms 1 Inv_in_Hom red_in_Hom Ide_in_Hom by simp
          show "❙⌊Inv (((f ❙⋆ g) ❙⋆ h)❙↓) ❙⋅ (f ❙⋆ g ❙⋆ h)❙↓❙⌋ = ❙⌊❙𝖺⇧-⇧1❙[f, g, h❙]❙⌋"
          proof -
            have "❙⌊Inv (((f ❙⋆ g) ❙⋆ h)❙↓) ❙⋅ (f ❙⋆ g ❙⋆ h)❙↓❙⌋ = Dom ❙⌊Inv (((f ❙⋆ g) ❙⋆ h)❙↓) ❙⋅ (f ❙⋆ g ❙⋆ h)❙↓❙⌋"
            proof -
              have "Can (Inv (((f ❙⋆ g) ❙⋆ h)❙↓) ❙⋅ (f ❙⋆ g ❙⋆ h)❙↓)"
                using assms Nmlize_Inv Can_Inv
                      Arr.simps(10) Arr.simps(4) Can.simps(4) Can_red(1) Ide.simps(3)
                      Src.simps(3) Trg.simps(3) par
                by presburger
              hence "Ide ❙⌊Inv (((f ❙⋆ g) ❙⋆ h)❙↓) ❙⋅ (f ❙⋆ g ❙⋆ h)❙↓❙⌋"
                using Ide_Nmlize_Can by blast
              thus ?thesis
                using Ide_in_Hom Dom_Ide by presburger
            qed
            also have 6: "... = ❙⌊f ❙⋆ g ❙⋆ h❙⌋"
              using 1 Nmlize_Dom [of "Inv (((f ❙⋆ g) ❙⋆ h)❙↓) ❙⋅ (f ❙⋆ g ❙⋆ h)❙↓"]
              by (metis (mono_tags, lifting) mem_Collect_eq)
            also have 5: "... = Dom ❙⌊❙𝖺⇧-⇧1❙[f, g, h❙]❙⌋"
              using assms 6 par Nmlize_Dom Nml_Nmlize(4) by metis
            also have "... = ❙⌊❙𝖺⇧-⇧1❙[f, g, h❙]❙⌋"
              using assms 5 Ide_in_Hom by auto
            finally show ?thesis by simp
          qed
        qed
        also have "... = 𝖺⇧-⇧1[⦃f⦄, ⦃g⦄, ⦃h⦄]"
          using assms E.eval_Assoc'_Ide by fastforce
        finally show ?thesis by simp
      qed
    qed

    lemma can_Ide_self:
    assumes "Ide t"
    shows "can t t = ⦃t⦄"
    proof (unfold can_def)
      show "⦃Inv (t❙↓) ❙⋅ t❙↓⦄ = ⦃t⦄"
      proof (intro E.eval_eqI)
        show "VPar (Inv (t❙↓) ❙⋅ t❙↓) t"
          using assms red_in_Hom Inv_in_Hom Ide_implies_Can Can_Inv Can_red(1) Ide_in_Hom(2)
          by auto
        show "❙⌊Inv (t❙↓) ❙⋅ t❙↓❙⌋ = ❙⌊t❙⌋"
          using assms red_in_Hom Inv_in_Hom Ide_implies_Can Cod_Inv
          by (metis (mono_tags, lifting) Can_red(1) Nml_Nmlize(1) Nmlize.simps(4)
              Nmlize_Inv Ide_Nmlize_Ide Nmlize_red Inv_Ide VcompNml_Ide_Nml
              ‹VPar (Inv (t❙↓) ❙⋅ t❙↓) t›)
      qed
    qed

    subsection "Rules for Whiskering"

    lemma whisker_can_right_0:
    assumes "Ide t" and "Ide u" and "❙⌊t❙⌋ = ❙⌊u❙⌋" and "ide f" and "Src t = ❙⟨trg f❙⟩⇩0"
    shows "can u t ⋆ f = can (u ❙⋆ ❙⟨f❙⟩) (t ❙⋆ ❙⟨f❙⟩)"
    proof -
      have "f = can ❙⟨f❙⟩ ❙⟨f❙⟩"
        using assms can_Ide_self by simp
      thus ?thesis
        using assms Ide_implies_Arr hcomp_can
        by (metis Nml_Nmlize(2) Ide.simps(2) Trg.simps(2))
    qed

    lemma whisker_can_right_1:
    assumes "Ide t" and "Ide u" and "❙⌊t❙⌋ = ❙⌊u❙⌋" and "obj a" and "Src t = ❙⟨a❙⟩⇩0"
    shows "can u t ⋆ a = can (u ❙⋆ ❙⟨a❙⟩⇩0) (t ❙⋆ ❙⟨a❙⟩⇩0)"
    proof -
      have "a = can ❙⟨a❙⟩⇩0 ❙⟨a❙⟩⇩0"
        using assms can_Ide_self by auto
      thus ?thesis
        using assms Ide_implies_Arr hcomp_can
        by (metis Nml_Nmlize(2) Ide.simps(1) Trg.simps(1))
    qed

    lemma whisker_can_left_0:
    assumes "Ide t" and "Ide u" and "❙⌊t❙⌋ = ❙⌊u❙⌋" and "ide g" and "Trg t = ❙⟨src g❙⟩⇩0"
    shows "g ⋆ can u t = can (❙⟨g❙⟩ ❙⋆ u) (❙⟨g❙⟩ ❙⋆ t)"
    proof -
      have "g = can ❙⟨g❙⟩ ❙⟨g❙⟩"
        using assms can_Ide_self by simp
      thus ?thesis
        using assms Ide_implies_Arr hcomp_can
        by (metis Nml_Nmlize(3) Ide.simps(2) Src.simps(2))
    qed

    lemma whisker_can_left_1:
    assumes "Ide t" and "Ide u" and "❙⌊t❙⌋ = ❙⌊u❙⌋" and "obj b" and "Trg t = ❙⟨b❙⟩⇩0"
    shows "b ⋆ can u t = can (❙⟨b❙⟩⇩0 ❙⋆ u) (❙⟨b❙⟩⇩0 ❙⋆ t)"
    proof -
      have "b = can ❙⟨b❙⟩⇩0 ❙⟨b❙⟩⇩0"
        using assms can_Ide_self by auto
      thus ?thesis
        using assms Ide_implies_Arr hcomp_can
        by (metis Nml_Nmlize(3) Ide.simps(1) Src.simps(1))
    qed

  end

end