Theory Strictness

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

section "Strictness"

theory Strictness
imports Category3.ConcreteCategory Pseudofunctor CanonicalIsos
begin

  text ‹
    In this section we consider bicategories in which some or all of the canonical isomorphisms
    are assumed to be identities.  A \emph{normal} bicategory is one in which the unit
    isomorphisms are identities, so that unit laws for horizontal composition are satisfied
    ``on the nose''.
    A \emph{strict} bicategory (also known as a \emph{2-category}) is a bicategory in which both
    the unit and associativity isomoprhisms are identities, so that horizontal composition is
    strictly associative as well as strictly unital.

    From any given bicategory B› we may construct a related strict bicategory S›,
    its \emph{strictification}, together with a pseudofunctor that embeds B› in S›.
    The Strictness Theorem states that this pseudofunctor is an equivalence pseudofunctor,
    so that bicategory B› is biequivalent to its strictification.
    The Strictness Theorem is often used informally to justify suppressing canonical
    isomorphisms; which amounts to proving a theorem about 2-categories and asserting that
    it holds for all bicategories.  Here we are working formally, so we can't just wave
    our hands and mutter something about the Strictness Theorem when we want to avoid
    dealing with units and associativities.  However, in cases where we can establish that the
    property we would like to prove is reflected by the embedding of a bicategory in its
    strictification, then we can formally apply the Strictness Theorem to generalize to all
    bicategories a result proved for 2-categories.  We will apply this approach here to
    simplify the proof of some facts about internal equivalences in a bicategory.
  ›

  subsection "Normal and Strict Bicategories"

  text ‹
    A \emph{normal} bicategory is one in which the unit isomorphisms are identities,
    so that unit laws for horizontal composition are satisfied ``on the nose''.
  ›

  locale normal_bicategory =
    bicategory +
  assumes strict_lunit: "f. ide f  𝗅[f] = f"
  and strict_runit: "f. ide f  𝗋[f] = f"
  begin

    lemma strict_unit:
    assumes "obj a"
    shows "ide 𝗂[a]"
      using assms strict_runit unitor_coincidence(2) [of a] by auto

    lemma strict_lunit':
    assumes "ide f"
    shows "𝗅-1[f] = f"
      using assms strict_lunit by simp

    lemma strict_runit':
    assumes "ide f"
    shows "𝗋-1[f] = f"
      using assms strict_runit by simp

    lemma hcomp_obj_arr:
    assumes "obj b" and "arr f" and "b = trg f"
    shows "b  f = f"
      using assms strict_lunit
      by (metis comp_arr_dom comp_ide_arr ide_cod ide_dom lunit_naturality)

    lemma hcomp_arr_obj:
    assumes "arr f" and "obj a" and "src f = a"
    shows "f  a = f"
      using assms strict_runit
      by (metis comp_arr_dom comp_ide_arr ide_cod ide_dom runit_naturality)

  end

  text ‹
    A \emph{strict} bicategory is a normal bicategory in which the associativities are also
    identities, so that associativity of horizontal composition holds ``on the nose''.
  ›

  locale strict_bicategory =
    normal_bicategory +
  assumes strict_assoc: "f g h. ide f; ide g; ide h; src f = trg g; src g = trg h 
                                  ide 𝖺[f, g, h]"
  begin

    lemma strict_assoc':
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "ide 𝖺-1[f, g, h]"
      using assms strict_assoc by simp

    lemma hcomp_assoc:
    shows "(μ  ν)  τ = μ  ν  τ"
    proof (cases "hseq μ ν  hseq ν τ")
      show "¬ (hseq μ ν  hseq ν τ)  ?thesis"
        by (metis hseqE hseq_char' match_1 match_2)
      show "hseq μ ν  hseq ν τ  ?thesis"
      proof -
        assume 1: "hseq μ ν  hseq ν τ"
        have 2: "arr μ  arr ν  arr τ  src μ = trg ν  src ν = trg τ"
          using 1 by blast
        have "(μ  ν)  τ = 𝖺[cod μ, cod ν, cod τ]  ((μ  ν)  τ)"
          using 1 assoc_in_hom strict_assoc comp_cod_arr assoc_simps(4) hseq_char
          by simp
        also have "... = (μ  ν  τ)  𝖺[dom μ, dom ν, dom τ]"
          using 1 assoc_naturality by auto
        also have "... = μ  ν  τ"
          using 2 assoc_in_hom [of "dom μ" "dom ν" "dom τ"] strict_assoc comp_arr_dom
          by auto
        finally show ?thesis by simp
      qed
    qed

    text ‹
      In a strict bicategory, every canonical isomorphism is an identity.
    ›

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

    lemma ide_eval_Can:
    assumes "Can t"
    shows "ide t"
    proof -
      have 1: "u1 u2.  ide u1; ide u2; Arr u1; Arr u2; Dom u1 = Cod u2 
                            ide (u1  u2)"
        by (metis (no_types, lifting) E.eval_simps'(4-5) comp_ide_self ide_char)
      have "u. Can u  ide u"
      proof -
        fix u
        show "Can u  ide u"
          (* TODO: Rename 𝔩_ide_simp 𝔯_ide_simp to 𝔩_ide_eq 𝔯_ide_eq *)
          using 1 α_def 𝖺'_def strict_lunit strict_runit strict_assoc strict_assoc'
                𝔩_ide_simp 𝔯_ide_simp Can_implies_Arr comp_ide_arr E.eval_simps'(2-3)
          by (induct u) auto
      qed
      thus ?thesis
        using assms by simp
    qed

    lemma ide_can:
    assumes "Ide f" and "Ide g" and "f = g"
    shows "ide (can g f)"
      using assms Can_red Can_Inv red_in_Hom Inv_in_Hom can_def ide_eval_Can
            Can.simps(4) Dom_Inv red_simps(4)
      by presburger

  end

  context bicategory
  begin

    text ‹
      The following result gives conditions for strictness of a bicategory that are typically
      somewhat easier to verify than those used for the definition.
    ›

    lemma is_strict_if:
    assumes "f. ide f  f  src f = f"
    and "f. ide f  trg f  f = f"
    and "a. obj a  ide 𝗂[a]"
    and "f g h. ide f; ide g; ide h; src f = trg g; src g = trg h  ide 𝖺[f, g, h]"
    shows "strict_bicategory V H 𝖺 𝗂 src trg"
    proof
      show "f g h. ide f; ide g; ide h; src f = trg g; src g = trg h  ide 𝖺[f, g, h]"
        by fact
      fix f
      assume f: "ide f"
      show "𝗅[f] = f"
      proof -
        have "f = 𝗅[f]"
          using assms f unit_simps(5)
          by (intro lunit_eqI) (auto simp add: comp_arr_ide)
        thus ?thesis by simp
      qed
      show "𝗋[f] = f"
      proof -
        have "f = 𝗋[f]"
        proof (intro runit_eqI)
          show "ide f" by fact
          show "«f : f  src f  f»"
            using f assms(1) by auto
          show "f  src f = (f  𝗂[src f])  𝖺[f, src f, src f]"
          proof -
            have "(f  𝗂[src f])  𝖺[f, src f, src f] = (f  src f)  𝖺[f, src f, src f]"
              using f assms(2-3) unit_simps(5) by simp
            also have "... = (f  src f  src f)  𝖺[f, src f, src f]"
              using f assms(1-2) ideD(1) trg_src src.preserves_ide by metis
            also have "... = f  src f"
              using f comp_arr_ide assms(1,4) assoc_in_hom [of f "src f" "src f"] by auto
            finally show ?thesis by simp
          qed
        qed
        thus ?thesis by simp
      qed
    qed

  end

  subsection "Strictification"

  (*
   * TODO: Perhaps change the typeface used for a symbol that stands for a bicategory;
   * for example, to avoid the clashes here between B used as the name of a bicategory
   * and B used to denote a syntactic identity term.
   *)

  text ‹
    The Strictness Theorem asserts that every bicategory is biequivalent to a
    strict bicategory.  More specifically, it shows how to construct, given an arbitrary
    bicategory, a strict bicategory (its \emph{strictification}) that is biequivalent to it.
    Consequently, given a property P› of bicategories that is ``bicategorical''
    (\emph{i.e.}~respects biequivalence), if we want to show that P› holds for a bicategory B›
    then it suffices to show that P› holds for the strictification of B›, and if we want to show
    that P› holds for all bicategories, it is sufficient to show that it holds for all
    strict bicategories.  This is very useful, because it becomes quite tedious, even
    with the aid of a proof assistant, to do ``diagram chases'' with all the units and
    associativities fully spelled out.

    Given a bicategory B›, the strictification S› of B› may be constructed as the bicategory
    whose arrows are triples (A, B, μ)›, where X› and Y› are ``normal identity terms''
    (essentially, nonempty horizontally composable lists of 1-cells of B›) having the same
    syntactic source and target, and «μ : ⦃X⦄ ⇒ ⦃Y⦄»› in B›.
    Vertical composition in S› is given by composition of the underlying arrows in B›.
    Horizontal composition in S› is given by (A, B, μ) ⋆ (A', B', μ') = (AA', BB', ν)›,
    where AA'› and BB'› denote concatenations of lists and where ν› is defined as the
    composition can BB' (B  B') ⋅ (μ ⋆ μ') ⋅ can (A  A') AA'›, where can (A  A') AA'› and
    can BB' (B  B')› are canonical isomorphisms in B›.  The canonical isomorphism
    can (A  A') AA'› corresponds to taking a pair of lists A  A'› and
    ``shifting the parentheses to the right'' to obtain a single list AA'›.
    The canonical isomorphism can BB' (B  B')› corresponds to the inverse rearrangement.

    The bicategory B› embeds into its strictification S› via the functor UP› that takes
    each arrow μ› of B› to (dom μ, cod μ, μ)›, where dom μ and cod μ denote
    one-element lists.  This mapping extends to a pseudofunctor.
    There is also a pseudofunctor DN›, which maps (A, B, μ)› in S› to μ› in B›;
    this is such that DN o UP› is the identity on B› and UP o DN› is equivalent to the
    identity on S›, so we obtain a biequivalence between B› and S›.

    It seems difficult to find references that explicitly describe a strictification
    construction in elementary terms like this (in retrospect, it ought to have been relatively
    easy to rediscover such a construction, but my thinking got off on the wrong track).
    One reference that I did find useful was cite"unapologetic-strictification",
    which discusses strictification for monoidal categories.
  ›

  locale strictified_bicategory =
    B: bicategory VB HB 𝖺B 𝗂B srcB trgB
  for VB :: "'a comp"                  (infixr "B" 55)
  and HB :: "'a  'a  'a"           (infixr "B" 53)
  and 𝖺B :: "'a  'a  'a  'a"      ("𝖺B[_, _, _]")
  and 𝗂B :: "'a  'a"                  ("𝗂B[_]")
  and srcB :: "'a  'a"
  and trgB :: "'a  'a"
  begin

    sublocale E: self_evaluation_map VB HB 𝖺B 𝗂B srcB trgB ..

    notation B.in_hhom  ("«_ : _ B _»")
    notation B.in_hom  ("«_ : _ B _»")

    notation E.eval ("_")
    notation E.Nmlize ("_")

    text ‹
      The following gives the construction of a bicategory whose arrows are triples (A, B, μ)›,
      where Nml A ∧ Ide A›, Nml B ∧ Ide B›, Src A = Src B›, Trg A = Trg B›, and μ : ⦃A⦄ ⇒ ⦃B⦄›.
      We use @{locale concrete_category} to construct the vertical composition, so formally the
      arrows of the bicategory will be of the form MkArr A B μ›.
    ›

    text ‹
      The 1-cells of the bicategory correspond to normal, identity terms A›
      in the bicategorical language associated with B›.
    ›

    abbreviation IDE
    where "IDE  {A. E.Nml A  E.Ide A}"

    text ‹
      If terms A› and B› determine 1-cells of the strictification and have a
      common source and target, then the 2-cells between these 1-cells correspond
      to arrows μ› of the underlying bicategory such that «μ : ⦃A⦄ ⇒B ⦃B⦄»›.
    ›

    abbreviation HOM
    where "HOM A B  {μ. E.Src A = E.Src B  E.Trg A = E.Trg B  «μ : A B B»}"

    text ‹
      The map taking term A ∈ OBJ› to its evaluation ⦃A⦄ ∈ HOM A A› defines the
      embedding of 1-cells as identity 2-cells.
    ›

    abbreviation EVAL
    where "EVAL  E.eval"

    sublocale concrete_category IDE HOM EVAL λ_ _ _ μ ν. μ B ν
      using E.ide_eval_Ide B.comp_arr_dom B.comp_cod_arr B.comp_assoc
      by (unfold_locales, auto)

    lemma is_concrete_category:
    shows "concrete_category IDE HOM EVAL (λ_ _ _ μ ν. μ B ν)"
      ..

    abbreviation vcomp     (infixr "" 55)
    where "vcomp  COMP"

    lemma arr_char:
    shows "arr F 
           E.Nml (Dom F)  E.Ide (Dom F)  E.Nml (Cod F)  E.Ide (Cod F) 
           E.Src (Dom F) = E.Src (Cod F)  E.Trg (Dom F) = E.Trg (Cod F) 
           «Map F : Dom F B Cod F»  F  Null"
      using arr_char by auto

    lemma arrI (* [intro] *):
    assumes "E.Nml (Dom F)" and "E.Ide (Dom F)" and "E.Nml (Cod F)" and "E.Ide (Cod F)"
    and "E.Src (Dom F) = E.Src (Cod F)" and "E.Trg (Dom F) = E.Trg (Cod F)"
    and "«Map F : Dom F B Cod F»" and "F  Null"
    shows "arr F"
      using assms arr_char by blast

    lemma arrE [elim]:
    assumes "arr F"
    shows "( E.Nml (Dom F); E.Ide (Dom F); E.Nml (Cod F); E.Ide (Cod F);
              E.Src (Dom F) = E.Src (Cod F); E.Trg (Dom F) = E.Trg (Cod F);
              «Map F : Dom F B Cod F»; F  Null   T)  T"
      using assms arr_char by simp

    lemma ide_char:
    shows "ide F  endo F  B.ide (Map F)"
    proof
      show "ide F  endo F  B.ide (Map F)"
        using ide_charCC by (simp add: E.ide_eval_Ide)
      show "endo F  B.ide (Map F)  ide F"
        by (metis (no_types, lifting) B.ide_char B.in_homE arr_char ide_charCC
            mem_Collect_eq seq_char)
    qed

    lemma ideI [intro]:
    assumes "arr F" and "Dom F = Cod F" and "B.ide (Map F)"
    shows "ide F"
      using assms ide_char dom_char cod_char seq_char by presburger

    lemma ideE [elim]:
    assumes "ide F"
    shows "( arr F; Dom F = Cod F; B.ide (Map F); Map F = Dom F;
              Map F = Cod F   T)  T"
      using assms
      by (metis (no_types, lifting) Map_ide(2) ide_char seq_char)

    text ‹
      Source and target are defined by the corresponding syntactic operations on terms.
    ›

    definition src
    where "src F  if arr F then MkIde (E.Src (Dom F)) else null"

    definition trg
    where "trg F  if arr F then MkIde (E.Trg (Dom F)) else null"

    lemma src_simps [simp]:
    assumes "arr F"
    shows "Dom (src F) = E.Src (Dom F)" and "Cod (src F) = E.Src (Dom F)"
    and "Map (src F) = E.Src (Dom F)"
      using assms src_def arr_char by auto

    lemma trg_simps [simp]:
    assumes "arr F"
    shows "Dom (trg F) = E.Trg (Dom F)" and "Cod (trg F) = E.Trg (Dom F)"
    and "Map (trg F) = E.Trg (Dom F)"
      using assms trg_def arr_char by auto

    interpretation src: endofunctor vcomp src
      using src_def comp_char E.Obj_implies_Ide
      apply (unfold_locales)
          apply auto[4]
    proof -
      show "g f. seq g f  src (g  f) = src g  src f"
      proof -
        fix g f
        assume gf: "seq g f"
        have "src (g  f) = MkIde (E.Src (Dom (g  f)))"
          using gf src_def comp_char by simp
        also have "... = MkIde (E.Src (Dom f))"
          using gf by (simp add: seq_char)
        also have "... = MkIde (E.Src (Dom g))  MkIde (E.Src (Dom f))"
          using gf seq_char E.Obj_implies_Ide by auto
        also have "... = src g  src f"
          using gf src_def comp_char by auto
        finally show "src (g  f) = src g  src f" by blast
      qed
    qed

    interpretation trg: endofunctor vcomp trg
      using trg_def comp_char E.Obj_implies_Ide
      apply (unfold_locales)
          apply auto[4]
    proof -
      show "g f. seq g f  trg (g  f) = trg g  trg f"
      proof -
        fix g f
        assume gf: "seq g f"
        have "trg (g  f) = MkIde (E.Trg (Dom (g  f)))"
          using gf trg_def comp_char by simp
        also have "... = MkIde (E.Trg (Dom f))"
          using gf by (simp add: seq_char)
        also have "... = MkIde (E.Trg (Dom g))  MkIde (E.Trg (Dom f))"
          using gf seq_char E.Obj_implies_Ide by auto
        also have "... = trg g  trg f"
          using gf trg_def comp_char by auto
        finally show "trg (g  f) = trg g  trg f" by blast
      qed
    qed

    interpretation horizontal_homs vcomp src trg
      using src_def trg_def Cod_in_Obj Map_in_Hom E.Obj_implies_Ide
      by unfold_locales auto

    notation in_hhom  ("«_ : _  _»")

    definition hcomp    (infixr "" 53)
    where "μ  ν  if arr μ  arr ν  src μ = trg ν
                   then MkArr (Dom μ  Dom ν) (Cod μ  Cod ν)
                              (B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B
                                (Map μ B Map ν) B
                                B.can (Dom μ  Dom ν) (Dom μ  Dom ν))
                   else null"

    lemma arr_hcomp:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "arr (μ  ν)"
    proof -
      have 1: "E.Ide (Dom μ  Dom ν)  E.Nml (Dom μ  Dom ν) 
               E.Ide (Cod μ  Cod ν)  E.Nml (Cod μ  Cod ν)"
        using assms arr_char src_def trg_def E.Ide_HcompNml E.Nml_HcompNml(1) by auto
      moreover
      have "«B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B (Map μ B Map ν) B
               B.can (Dom μ  Dom ν) (Dom μ  Dom ν) :
                  Dom μ  Dom ν B Cod μ  Cod ν»"
      proof -
        have "«Map μ B Map ν : Dom μ  Dom ν B Cod μ  Cod ν»"
          using assms arr_char dom_char cod_char src_def trg_def E.eval_simps'(2-3)
          by auto
        moreover
        have "«B.can (Dom μ  Dom ν) (Dom μ  Dom ν) :
                  Dom μ  Dom ν B Dom μ  Dom ν» 
               «B.can (Cod μ  Cod ν) (Cod μ  Cod ν) :
                  Cod μ  Cod ν B Cod μ  Cod ν»"
          using assms 1 arr_char src_def trg_def
          apply (intro conjI B.in_homI) by auto
        ultimately show ?thesis by auto
      qed
      moreover have "E.Src (Dom μ  Dom ν) = E.Src (Cod μ  Cod ν) 
                     E.Trg (Dom μ  Dom ν) = E.Trg (Cod μ  Cod ν)"
        using assms arr_char src_def trg_def
        by (simp add: E.Src_HcompNml E.Trg_HcompNml)
      ultimately show ?thesis
        unfolding hcomp_def
        using assms by (intro arrI, auto)
    qed

    lemma src_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "src (μ  ν) = src ν"
      using assms arr_char hcomp_def src_def trg_def arr_hcomp E.Src_HcompNml by simp

    lemma trg_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "trg (hcomp μ ν) = trg μ"
      using assms arr_char hcomp_def src_def trg_def arr_hcomp E.Trg_HcompNml by simp

    lemma hseq_char:
    shows "arr (μ  ν)  arr μ  arr ν  src μ = trg ν"
      using arr_hcomp hcomp_def by simp

    lemma Dom_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "Dom (μ  ν) = Dom μ  Dom ν"
      using assms hcomp_def [of μ ν] by simp

    lemma Cod_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "Cod (μ  ν) = Cod μ  Cod ν"
      using assms hcomp_def [of μ ν] by simp

    lemma Map_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src μ = trg ν"
    shows "Map (μ  ν) = B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B
                           (Map μ B Map ν) B
                           B.can (Dom μ  Dom ν) (Dom μ  Dom ν)"
      using assms hcomp_def [of μ ν] by simp

    interpretation "functor" VV.comp vcomp λμν. hcomp (fst μν) (snd μν)
    proof
      show "f. ¬ VV.arr f  fst f  snd f = null"
        using hcomp_def by auto
      show A: "f. VV.arr f  arr (fst f  snd f)"
        using VV.arrE hseq_char by blast
      show "f. VV.arr f  dom (fst f  snd f) = fst (VV.dom f)  snd (VV.dom f)"
      proof -
        fix f
        assume f: "VV.arr f"
        have "dom (fst f  snd f) = MkIde (Dom (fst f)  Dom (snd f))"
          using f VV.arrE [of f] dom_char arr_hcomp hcomp_def by simp
        also have "... = fst (VV.dom f)  snd (VV.dom f)"
        proof -
          have "hcomp (fst (VV.dom f)) (snd (VV.dom f)) =
                MkArr (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f))
                      (B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f)) B
                        (Dom (fst f) B Dom (snd f)) B
                        B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f)))"
            using f VV.arrE [of f] arr_hcomp hcomp_def VV.dom_simp by simp
          moreover have "B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f)) B
                           (Dom (fst f) B Dom (snd f)) B
                              B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f)) =
                         Dom (fst f)  Dom (snd f)"
          proof -
            have 1: "E.Ide (Dom (fst f)  Dom (snd f))"
              using f VV.arr_charSbC arr_char dom_char
              apply simp
              by (metis (no_types, lifting) src_simps(1) trg_simps(1))
            have 2: "E.Ide (Dom (fst f)  Dom (snd f))"
              using f VV.arr_charSbC arr_char dom_char
              apply simp
              by (metis (no_types, lifting) E.Ide_HcompNml src_simps(1) trg_simps(1))
            have 3: "Dom (fst f)  Dom (snd f) = Dom (fst f)  Dom (snd f)"
              using f VV.arr_charSbC arr_char dom_char
              apply simp
              by (metis (no_types, lifting) E.Nml_HcompNml(1) E.Nmlize_Nml
                  src_simps(1) trg_simps(1))
            have "(Dom (fst f) B Dom (snd f)) B
                    B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f)) =
                  B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f))"
              using "1" "2" "3" B.comp_cod_arr by force
            thus ?thesis
              using 1 2 3 f VV.arr_charSbC B.can_Ide_self B.vcomp_can by simp
          qed
          ultimately show ?thesis by simp
        qed
        finally show "dom (fst f  snd f) = fst (VV.dom f)  snd (VV.dom f)"
          by simp
      qed
      show "f. VV.arr f  cod (fst f  snd f) = fst (VV.cod f)  snd (VV.cod f)"
      proof -
        fix f
        assume f: "VV.arr f"
        have "cod (fst f  snd f) = MkIde (Cod (fst f)  Cod (snd f))"
          using f VV.arrE [of f] cod_char arr_hcomp hcomp_def by simp
        also have "... = fst (VV.cod f)  snd (VV.cod f)"
        proof -
          have "hcomp (fst (VV.cod f)) (snd (VV.cod f)) =
                MkArr (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f))
                      (B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f)) B
                        (Cod (fst f) B Cod (snd f)) B
                        B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f)))"
            using f VV.arrE [of f] arr_hcomp hcomp_def VV.cod_simp by simp
          moreover have "B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f)) B
                           (Cod (fst f) B Cod (snd f)) B
                             B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f)) =
                         Cod (fst f)  Cod (snd f)"
          proof -
            have 1: "E.Ide (Cod (fst f)  Cod (snd f))"
              using f VV.arr_charSbC arr_char dom_char
              apply simp
              by (metis (no_types, lifting) src_simps(1) trg_simps(1))
            have 2: "E.Ide (Cod (fst f)  Cod (snd f))"
              using f VV.arr_charSbC arr_char dom_char
              apply simp
              by (metis (no_types, lifting) E.Ide_HcompNml src_simps(1) trg_simps(1))
            have 3: "Cod (fst f)  Cod (snd f) = Cod (fst f)  Cod (snd f)"
              using f VV.arr_charSbC arr_char dom_char
              apply simp
              by (metis (no_types, lifting) E.Nml_HcompNml(1) E.Nmlize_Nml
                  src_simps(1) trg_simps(1))
            have "(Cod (fst f) B Cod (snd f)) B
                    B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f)) =
                  B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f))"
              using "1" "2" "3" B.comp_cod_arr by force
            thus ?thesis
              using 1 2 3 f VV.arr_charSbC B.can_Ide_self B.vcomp_can by simp
          qed
          ultimately show ?thesis by simp
        qed
        finally show "cod (fst f  snd f) = fst (VV.cod f)  snd (VV.cod f)"
          by simp
      qed
      show "g f. VV.seq g f 
                   fst (VV.comp g f)  snd (VV.comp g f) = (fst g  snd g)  (fst f  snd f)"
      proof -
        fix f g
        assume fg: "VV.seq g f"
        have f: "arr (fst f)  arr (snd f)  src (fst f) = trg (snd f)"
          using fg VV.seq_charSbC VV.arr_charSbC by simp
        have g: "arr (fst g)  arr (snd g)  src (fst g) = trg (snd g)"
          using fg VV.seq_charSbC VV.arr_charSbC by simp
        have 1: "arr (fst (VV.comp g f))  arr (snd (VV.comp g f)) 
                 src (fst (VV.comp g f)) = trg (snd (VV.comp g f))"
          using fg VV.arrE by blast
        have 0: "VV.comp g f = (fst g  fst f, snd g  snd f)"
          using fg 1 VV.comp_char VxV.comp_char
          by (metis (no_types, lifting) VV.seq_charSbC VxV.seqEPC)
        let ?X = "MkArr (Dom (fst (VV.comp g f))  Dom (snd (VV.comp g f)))
                        (Cod (fst (VV.comp g f))  Cod (snd (VV.comp g f)))
                        (B.can (Cod (fst (VV.comp g f))  Cod (snd (VV.comp g f)))
                               (Cod (fst (VV.comp g f))  Cod (snd (VV.comp g f))) B
                           (Map (fst (VV.comp g f)) B Map (snd (VV.comp g f))) B
                           B.can (Dom (fst (VV.comp g f))  Dom (snd (VV.comp g f)))
                                 (Dom (fst (VV.comp g f))  Dom (snd (VV.comp g f))))"
        have 2: "fst (VV.comp g f)  snd (VV.comp g f) = ?X"
          unfolding hcomp_def using 1 by simp
        also have "... = (fst g  snd g)  (fst f  snd f)"
        proof -
          let ?GG = "MkArr (Dom (fst g)  Dom (snd g)) (Cod (fst g)  Cod (snd g))
                           (B.can (Cod (fst g)  Cod (snd g)) (Cod (fst g)  Cod (snd g)) B
                             (Map (fst g) B Map (snd g)) B
                             B.can (Dom (fst g)  Dom (snd g)) (Dom (fst g)  Dom (snd g)))"
          let ?FF = "MkArr (Dom (fst f)  Dom (snd f)) (Cod (fst f)  Cod (snd f))
                           (B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f)) B
                             (Map (fst f) B Map (snd f)) B
                             B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f)))"
          have 4: "arr ?FF  arr ?GG  Dom ?GG = Cod ?FF"
          proof -
            have "arr ?FF  arr ?GG"
              using f g fg VV.arr_charSbC VV.seqE hcomp_def A by presburger
            thus ?thesis
              using 0 1 by (simp add: fg seq_char)
          qed
          have "(fst g  snd g)  (fst f  snd f) = ?GG  ?FF"
            unfolding hcomp_def
            using 1 f g fg VV.arr_charSbC VV.seqE by simp
          also have "... = ?X"
          proof (intro arr_eqI)
            show "seq ?GG ?FF"
              using fg 4 seq_char by blast
            show "arr ?X"
              using fg 1 arr_hcomp hcomp_def by simp
            show "Dom (?GG  ?FF) = Dom ?X"
              using fg 0 1 4 seq_char by simp
            show "Cod (?GG  ?FF) = Cod ?X"
              using fg 0 1 4 seq_char by simp
            show "Map (?GG  ?FF) = Map ?X"
            proof -
              have "Map (?GG  ?FF) = Map ?GG B Map ?FF"
                using 4 by auto
              also have
                "... = (B.can (Cod (fst g)  Cod (snd g)) (Cod (fst g)  Cod (snd g)) B
                         (Map (fst g) B Map (snd g)) B
                         B.can (Dom (fst g)  Dom (snd g)) (Dom (fst g)  Dom (snd g))) B
                       (B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f)) B
                         (Map (fst f) B Map (snd f)) B
                         B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f)))"
                using fg by simp
              also have
                "... = B.can (Cod (fst g)  Cod (snd g)) (Cod (fst g)  Cod (snd g)) B
                         ((Map (fst g) B Map (snd g)) B (Map (fst f) B Map (snd f))) B
                         B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f))"
              proof -
                have "(B.can (Cod (fst g)  Cod (snd g)) (Cod (fst g)  Cod (snd g)) B
                        (Map (fst g) B Map (snd g)) B
                        B.can (Dom (fst g)  Dom (snd g)) (Dom (fst g)  Dom (snd g))) B
                        (B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f)) B
                        (Map (fst f) B Map (snd f)) B
                        B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f))) =
                      B.can (Cod (fst g)  Cod (snd g)) (Cod (fst g)  Cod (snd g)) B
                        ((Map (fst g) B Map (snd g)) B
                        (B.can (Dom (fst g)  Dom (snd g)) (Dom (fst g)  Dom (snd g)) B
                        B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f))) B
                        (Map (fst f) B Map (snd f))) B
                        B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f))"
                  using B.comp_assoc by simp
                also have "... = B.can (Cod (fst g)  Cod (snd g)) (Cod (fst g)  Cod (snd g)) B
                                  ((Map (fst g) B Map (snd g)) B (Map (fst f) B Map (snd f))) B
                                   B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f))"
                proof -
                  have "(B.can (Dom (fst g)  Dom (snd g)) (Dom (fst g)  Dom (snd g))) B
                          (B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f))) =
                        Cod (fst f)  Cod (snd f)"
                  proof -
                    have "(B.can (Dom (fst g)  Dom (snd g)) (Dom (fst g)  Dom (snd g))) B
                          (B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f))) =
                          B.can (Dom (fst g)  Dom (snd g)) (Cod (fst f)  Cod (snd f))"
                    proof -
                      have "E.Ide (Dom (fst g)  Dom (snd g))"
                        using g arr_char
                        by (metis (no_types, lifting) E.Ide.simps(3) src_simps(2) trg_simps(2))
                      moreover have "E.Ide (Dom (fst g)  Dom (snd g))"
                        using 4 by auto
                      moreover have "E.Ide (Cod (fst f)  Cod (snd f))"
                        using f arr_char
                        by (metis (no_types, lifting) E.Ide.simps(3) src_simps(2) trg_simps(2))
                      moreover have
                        "Dom (fst g)  Dom (snd g) = Dom (fst g)  Dom (snd g)"
                        using g E.Nml_HcompNml(1) calculation(1) by fastforce
                      moreover have
                        "Dom (fst g)  Dom (snd g) = Cod (fst f)  Cod (snd f)"
                        using g fg seq_char
                        by (metis (no_types, lifting) VV.seq_charSbC VxV.seqEPC calculation(4))
                      moreover have
                        "Dom (fst g)  Dom (snd g) = Cod (fst f)  Cod (snd f)"
                        using 0 1 by (simp add: seq_char)
                      ultimately show ?thesis
                        using B.vcomp_can by simp
                    qed
                    also have "... = Cod (fst f)  Cod (snd f)"
                    proof -
                      have "Dom (fst g)  Dom (snd g) = Cod (fst f)  Cod (snd f)"
                        using 0 f g fg seq_char VV.seq_charSbC VV.arr_charSbC
                        by simp
                      thus ?thesis
                        using f B.can_Ide_self [of "Dom (fst f)  Dom (snd f)"]
                        by (metis (no_types, lifting) B.can_Ide_self E.Ide.simps(3)
                            arrE src_simps(2) trg_simps(2))
                    qed
                    finally show ?thesis by simp
                  qed
                  hence "(B.can (Dom (fst g)  Dom (snd g)) (Dom (fst g)  Dom (snd g)) B
                           B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f))) B
                           (Map (fst f) B Map (snd f)) =
                         Cod (fst f)  Cod (snd f) B (Map (fst f) B Map (snd f))"
                    by simp
                  also have "... = Map (fst f) B Map (snd f)"
                  proof -
                    have 1: "p. arr p  map (cod p)  map p = map p"
                      by blast
                    have 3: "Cod (fst f) B Map (fst f) = Map (map (cod (fst f))  map (fst f))"
                      by (simp add: f)
                    have 4: "map (cod (fst f))  map (fst f) = fst f"
                      using 1 f map_simp by simp
                    show ?thesis
                    proof -
                      have 2: "Cod (snd f) B Map (snd f) = Map (snd f)"
                        using 1 f map_simp
                        by (metis (no_types, lifting) Dom_cod Map_cod Map_comp arr_cod)
                      have "B.seq Cod (snd f) (Map (snd f))"
                        using f 2 by auto
                      moreover have "B.seq Cod (fst f) (Map (fst f))"
                        using 4 f 3 by auto
                      moreover have
                        "Cod (fst f) B Map (fst f) B Cod (snd f) B Map (snd f) =
                         Map (fst f) B Map (snd f)"
                        using 2 3 4 by presburger
                      ultimately show ?thesis
                        by (simp add: B.interchange)
                    qed
                  qed
                  finally have
                    "(B.can (Dom (fst g)  Dom (snd g)) (Dom (fst g)  Dom (snd g)) B
                       B.can (Cod (fst f)  Cod (snd f)) (Cod (fst f)  Cod (snd f))) B
                       (Map (fst f) B Map (snd f)) =
                     Map (fst f) B Map (snd f)"
                    by simp
                  thus ?thesis
                    using fg B.comp_cod_arr by simp
                qed
                finally show ?thesis by simp
              qed
              also have "... = B.can (Cod (fst g)  Cod (snd g)) (Cod (fst g)  Cod (snd g)) B
                                 (Map (fst g  fst f) B Map (snd g  snd f)) B
                                 B.can (Dom (fst f)  Dom (snd f)) (Dom (fst f)  Dom (snd f))"
              proof -
                have 2: "Dom (fst g) = Cod (fst f)"
                  using 0 f g fg VV.seq_charSbC [of g f] VV.arr_charSbC arr_char seq_char
                  by (metis (no_types, lifting) fst_conv)
                hence "Map (fst g  fst f) = Map (fst g) B Map (fst f)"
                  using f g Map_comp [of "fst f" "fst g"] by simp
                moreover have "B.seq (Map (fst g)) (Map (fst f)) 
                               B.seq (Map (snd g)) (Map (snd f))"
                  using f g 0 1 2 arr_char
                  by (metis (no_types, lifting) B.seqI' prod.sel(2) seq_char)
                ultimately show ?thesis
                  using 0 1 seq_char Map_comp B.interchange by auto
              qed
              also have "... = Map ?X"
                using fg 0 1 by (simp add: seq_char)
              finally show ?thesis by simp
            qed
          qed
          finally show ?thesis by simp
        qed
        finally show "fst (VV.comp g f)  snd (VV.comp g f) = (fst g  snd g)  (fst f  snd f)"
          by simp
      qed
    qed

    interpretation horizontal_composition vcomp hcomp src trg
      using hseq_char by (unfold_locales, auto)

    lemma hcomp_assoc:
    assumes "arr μ" and "arr ν" and "arr τ"
    and "src μ = trg ν" and "src ν = trg τ"
    shows "(μ  ν)  τ = μ  ν  τ"
    proof (intro arr_eqI)
      have μν: "«Map μ B Map ν : Dom μ  Dom ν B Cod μ  Cod ν»"
        using assms src_def trg_def arr_char
        by (auto simp add: E.eval_simps'(2-3) Pair_inject)
      have ντ: "«Map ν B Map τ : Dom ν  Dom τ B Cod ν  Cod τ»"
        using assms src_def trg_def arr_char
        by (auto simp add: E.eval_simps'(2-3) Pair_inject)
      show "hseq (μ  ν) τ"
        using assms μν ντ by auto
      show "hseq μ (ν  τ)"
        using assms μν ντ by auto
      show "Dom ((μ  ν)  τ) = Dom (μ  ν  τ)"
      proof -
        have "E.Nml (Dom μ)  E.Nml (Dom ν)  E.Nml (Dom τ)"
          using assms by blast
        moreover have "E.Src (Dom μ) = E.Trg (Dom ν)  E.Src (Dom ν) = E.Trg (Dom τ)"
          using assms μν ντ
          by (metis (no_types, lifting) src_simps(2) trg_simps(2))
        ultimately show ?thesis
          using assms μν ντ E.HcompNml_assoc by simp
      qed
      show "Cod ((μ  ν)  τ) = Cod (μ  ν  τ)"
      proof -
        have "E.Nml (Cod μ)  E.Nml (Cod ν)  E.Nml (Cod τ)"
          using assms by blast
        moreover have "E.Src (Cod μ) = E.Trg (Cod ν)  E.Src (Cod ν) = E.Trg (Cod τ)"
          using assms μν ντ
          by (metis (no_types, lifting) arrE src_simps(2) trg_simps(2))
        ultimately show ?thesis
          using assms μν ντ E.HcompNml_assoc by simp
      qed
     show "Map ((μ  ν)  τ) = Map (μ  ν  τ)"
      proof -
        have "Map ((μ  ν)  τ) =
              B.can (Cod μ  Cod ν  Cod τ) (Cod μ  Cod ν  Cod τ) B
                (Map μ B Map ν B Map τ) B
                   B.can (Dom μ  Dom ν  Dom τ) (Dom μ  Dom ν  Dom τ)"
        proof -
          have 1: "Map ((μ  ν)  τ) =
                   B.can (Cod μ  Cod ν  Cod τ) ((Cod μ  Cod ν)  Cod τ) B
                     (B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B
                       (Map μ B Map ν) B
                         B.can (Dom μ  Dom ν) (Dom μ  Dom ν) B Map τ) B
                       B.can ((Dom μ  Dom ν)  Dom τ) (Dom μ  Dom ν  Dom τ)"
            using assms μν ντ hcomp_def E.HcompNml_assoc src_def trg_def arr_char
                  E.Nml_HcompNml E.Ide_HcompNml
            by auto (* 5 sec *)
          also have
            "... = B.can (Cod μ  Cod ν  Cod τ) ((Cod μ  Cod ν)  Cod τ) B
                     (B.can ((Cod μ  Cod ν)  Cod τ) (Cod μ  Cod ν  Cod τ) B
                       (Map μ B Map ν B Map τ) B
                         B.can (Dom μ  Dom ν  Dom τ) ((Dom μ  Dom ν)  Dom τ)) B
                       B.can ((Dom μ  Dom ν)  Dom τ) (Dom μ  Dom ν  Dom τ)"
          proof -
            have
              "B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B
                 (Map μ B Map ν) B B.can (Dom μ  Dom ν) (Dom μ  Dom ν) B Map τ =
               B.can ((Cod μ  Cod ν)  Cod τ) (Cod μ  Cod ν  Cod τ) B
                 (Map μ B Map ν B Map τ) B
                 B.can (Dom μ  Dom ν  Dom τ) ((Dom μ  Dom ν)  Dom τ)"
            proof -
              have "B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B
                      (Map μ B Map ν) B B.can (Dom μ  Dom ν) (Dom μ  Dom ν)
                         B Map τ =
                    (B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B B.can (Cod τ) (Cod τ)) B
                      ((Map μ B Map ν) B
                         B.can (Dom μ  Dom ν) (Dom μ  Dom ν) B Map τ)"
              proof -
                have "B.seq (B.can (Cod μ  Cod ν) (Cod μ  Cod ν))
                               ((Map μ B Map ν) B B.can (Dom μ  Dom ν) (Dom μ  Dom ν))"
                  by (metis (no_types, lifting) B.arrI Map_hcomp arrE arr_hcomp
                      assms(1) assms(2) assms(4))
                moreover have "B.seq (B.can (Cod τ) (Cod τ)) (Map τ)"
                  using B.can_in_hom assms(3) by blast
                moreover have "B.ide (B.can (Cod τ) (Cod τ))"
                  using B.can_Ide_self E.ide_eval_Ide arr_char assms(3) by presburger
                ultimately show ?thesis
                  by (metis (no_types) B.comp_ide_arr B.interchange)
              qed
              also have
                "... = (B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B B.can (Cod τ) (Cod τ)) B
                         ((Map μ B Map ν) B Map τ) B
                           (B.can (Dom μ  Dom ν) (Dom μ  Dom ν) B
                              B.can (Dom τ) (Dom τ))"
              proof -
                have "B.seq (Map μ B Map ν) (B.can (Dom μ  Dom ν) (Dom μ  Dom ν))"
                  by (metis (no_types, lifting) B.arrI B.null_is_zero(2) B.ext Map_hcomp
                      arrE arr_hcomp assms(1) assms(2) assms(4))
                moreover have "B.seq (Map τ) (B.can (Dom τ) (Dom τ))"
                  using assms(3) by fastforce
                ultimately show ?thesis
                  using B.interchange
                  by (metis (no_types, lifting) B.can_Ide_self B.comp_arr_ide E.ide_eval_Ide
                      arrE assms(3))
              qed
              also have
                "... = (B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B B.can (Cod τ) (Cod τ)) B
                         (B.can ((Cod μ  Cod ν)  Cod τ) (Cod μ  Cod ν  Cod τ) B
                           (Map μ B Map ν B Map τ) B
                             B.can (Dom μ  Dom ν  Dom τ) ((Dom μ  Dom ν)  Dom τ)) B
                           (B.can (Dom μ  Dom ν) (Dom μ  Dom ν) B
                              B.can (Dom τ) (Dom τ))"
              proof -
                have "(Map μ B Map ν) B Map τ =
                        B.𝖺' Cod μ Cod ν Cod τ B
                          (Map μ B Map ν B Map τ) B
                             𝖺B Dom μ Dom ν Dom τ"
                  using B.hcomp_reassoc(1)
                  by (metis (no_types, lifting) B.hcomp_in_vhomE B.in_homE μν ντ arrE
                      assms(1) assms(2) assms(3))
                also have "... = B.can ((Cod μ  Cod ν)  Cod τ) (Cod μ  Cod ν  Cod τ) B
                                   (Map μ B Map ν B Map τ) B
                                      B.can (Dom μ  Dom ν  Dom τ) ((Dom μ  Dom ν)  Dom τ)"
                  using assms arr_char src_def trg_def arr_char B.canE_associator by simp
               finally show ?thesis by simp
              qed
              also have
                "... = ((B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B B.can (Cod τ) (Cod τ)) B
                         (B.can ((Cod μ  Cod ν)  Cod τ) (Cod μ  Cod ν  Cod τ))) B
                       (Map μ B Map ν B Map τ) B
                       (B.can (Dom μ  Dom ν  Dom τ) ((Dom μ  Dom ν)  Dom τ) B
                          (B.can (Dom μ  Dom ν) (Dom μ  Dom ν) B
                             B.can (Dom τ) (Dom τ)))"
                using B.comp_assoc by simp
              also have
                "... = B.can ((Cod μ  Cod ν)  Cod τ) (Cod μ  Cod ν  Cod τ) B
                         (Map μ B Map ν B Map τ) B
                         B.can (Dom μ  Dom ν  Dom τ) ((Dom μ  Dom ν)  Dom τ)"
              proof -
                have "(B.can (Cod μ  Cod ν) (Cod μ  Cod ν) B B.can (Cod τ) (Cod τ)) B
                        (B.can ((Cod μ  Cod ν)  Cod τ) (Cod μ  Cod ν  Cod τ)) =
                      B.can ((Cod μ  Cod ν)  Cod τ) (Cod μ  Cod ν  Cod τ)"
                proof -
                  have "E.Ide (Cod μ  Cod ν)"
                    by (metis (no_types, lifting) E.Ide.simps(3) arrE assms(1-2,4)
                        src_simps(1) trg_simps(1))
                  moreover have "E.Ide (Cod μ  Cod ν)"
                    using E.Ide_HcompNml assms(1) assms(2) calculation by auto
                  moreover have "Cod μ  Cod ν = Cod μ  Cod ν"
                    using E.Nml_HcompNml(1) assms(1) assms(2) calculation(1) by fastforce
                  moreover have "E.Src (Cod μ  Cod ν) = E.Trg (Cod τ)"
                    by (metis (no_types, lifting) E.Src.simps(3) arrE assms(2-3,5)
                        src_simps(2) trg_simps(2))
                  moreover have "E.Src (Cod μ  Cod ν) = E.Trg (Cod τ)"
                    using E.Src_HcompNml assms(1) assms(2) calculation(1) calculation(4)
                    by fastforce
                  moreover have "Cod μ  Cod ν  Cod τ = (Cod μ  Cod ν)  Cod τ"
                    by (metis (no_types, lifting) E.Arr.simps(3) E.Nmlize_Hcomp_Hcomp
                        E.Nmlize_Hcomp_Hcomp' E.Ide_implies_Arr E.Src.simps(3) arrE assms(3)
                        calculation(1) calculation(4))
                  ultimately show ?thesis
                    using assms(3) B.hcomp_can B.vcomp_can by auto
                qed
                moreover have
                  "B.can (Dom μ  Dom ν  Dom τ) ((Dom μ  Dom ν)  Dom τ) B
                     (B.can (Dom μ  Dom ν) (Dom μ  Dom ν) B B.can (Dom τ) (Dom τ)) =
                   B.can (Dom μ  Dom ν  Dom τ) ((Dom μ  Dom ν)  Dom τ)"
                proof -
                  have "E.Ide (Dom μ  Dom ν)"
                    by (metis (no_types, lifting) E.Ide_HcompNml arrE assms(1-2,4)
                        src_simps(2) trg_simps(2))
                  moreover have "E.Ide (Dom μ  Dom ν)"
                    by (metis (no_types, lifting) E.Ide.simps(3) arrE assms(1-2,4)
                        src_simps(1) trg_simps(1))
                  moreover have "Dom μ  Dom ν = Dom μ  Dom ν"
                    using E.Nml_HcompNml(1) assms(1-2) calculation(2) by fastforce
                  moreover have "E.Src (Dom μ  Dom ν) = E.Trg (Dom τ)"
                    by (metis (no_types, lifting) E.Ide.simps(3) E.Src_HcompNml arrE
                        assms(1-3,5) calculation(2) src_simps(2) trg_simps(2))
                  moreover have "E.Src (Dom μ  Dom ν) = E.Trg (Dom τ)"
                    using E.Src_HcompNml assms(1-2) calculation(2) calculation(4)
                    by fastforce
                  moreover have "E.Ide ((Dom μ  Dom ν)  Dom τ)"
                    using E.Ide.simps(3) assms(3) calculation(2) calculation(5) by blast
                  moreover have "(Dom μ  Dom ν)  Dom τ = Dom μ  Dom ν  Dom τ"
                    using E.Nmlize_Hcomp_Hcomp calculation(6) by auto
                  ultimately show ?thesis
                    using assms(3) B.hcomp_can B.vcomp_can by auto
                qed
                ultimately show ?thesis by simp
              qed
              finally show ?thesis by simp
            qed
            thus ?thesis by simp
          qed
          also have
            "... = (B.can (Cod μ  Cod ν  Cod τ) ((Cod μ  Cod ν)  Cod τ) B
                     B.can ((Cod μ  Cod ν)  Cod τ) (Cod μ  Cod ν  Cod τ)) B
                       (Map μ B Map ν B Map τ) B
                         B.can (Dom μ  Dom ν  Dom τ) ((Dom μ  Dom ν)  Dom τ) B
                           B.can ((Dom μ  Dom ν)  Dom τ) (Dom μ  Dom ν  Dom τ)"
            using B.comp_assoc by simp
          also have "... = B.can (Cod μ  Cod ν  Cod τ) (Cod μ  Cod ν  Cod τ) B
                             (Map μ B Map ν B Map τ) B
                               B.can (Dom μ  Dom ν  Dom τ) (Dom μ  Dom ν  Dom τ)"
          proof -
            have "B.can (Cod μ  Cod ν  Cod τ) ((Cod μ  Cod ν)  Cod τ) B
                    B.can ((Cod μ  Cod ν)  Cod τ) (Cod μ  Cod ν  Cod τ) =
                  B.can (Cod μ  Cod ν  Cod τ) (Cod μ  Cod ν  Cod τ)"
            proof -
              have "E.Ide (Cod μ  Cod ν  Cod τ)"
                using assms src_def trg_def by fastforce
              moreover have "E.Ide ((Cod μ  Cod ν)  Cod τ)"
                using assms arr_char src_def trg_def E.Ide_HcompNml E.Src_HcompNml
                by auto
              moreover have "E.Ide (Cod μ  Cod ν  Cod τ)"
                using assms arr_char src_def trg_def
                by (simp add: E.Nml_HcompNml(1) E.Ide_HcompNml E.Trg_HcompNml)
              moreover have "Cod μ  Cod ν  Cod τ = (Cod μ  Cod ν)  Cod τ"
                using assms arr_char src_def trg_def E.Nml_HcompNml E.HcompNml_assoc by simp
              moreover have "(Cod μ  Cod ν)  Cod τ = Cod μ  Cod ν  Cod τ"
                using assms arr_char src_def trg_def E.Nml_HcompNml E.HcompNml_assoc
                by simp
              ultimately show ?thesis by simp
            qed
            moreover have
              "B.can (Dom μ  Dom ν  Dom τ) ((Dom μ  Dom ν)  Dom τ) B
                 B.can ((Dom μ  Dom ν)  Dom τ) (Dom μ  Dom ν  Dom τ) =
               B.can (Dom μ  Dom ν  Dom τ) (Dom μ  Dom ν  Dom τ)"
            proof -
              have "E.Ide (Dom μ  Dom ν  Dom τ)"
                using assms src_def trg_def by fastforce
              moreover have "E.Ide ((Dom μ  Dom ν)  Dom τ)"
                using assms arr_char src_def trg_def E.Ide_HcompNml E.Src_HcompNml
                by auto
              moreover have "E.Ide (Dom μ  Dom ν  Dom τ)"
                using assms arr_char src_def trg_def
                by (simp add: E.Nml_HcompNml(1) E.Ide_HcompNml E.Trg_HcompNml)
              moreover have "Dom μ  Dom ν  Dom τ = (Dom μ  Dom ν)  Dom τ"
                using assms arr_char src_def trg_def E.Nml_HcompNml E.HcompNml_assoc by simp
              moreover have
                "(Dom μ  Dom ν)  Dom τ = Dom μ  Dom ν  Dom τ"
                using assms arr_char src_def trg_def E.Nml_HcompNml E.HcompNml_assoc
                by simp
              ultimately show ?thesis by simp
            qed
            ultimately show ?thesis by simp
          qed
          finally show ?thesis by simp
        qed
        also have "... = Map (μ  ν  τ)"
        proof -
          have 1: "Map (μ  ν  τ) =
                   B.can (Cod μ  Cod ν  Cod τ) (Cod μ  Cod ν  Cod τ) B
                     (Map μ B B.can (Cod ν  Cod τ) (Cod ν  Cod τ) B
                                (Map ν B Map τ) B
                                  B.can (Dom ν  Dom τ) (Dom ν  Dom τ)) B
                        B.can (Dom μ  Dom ν  Dom τ) (Dom μ  Dom ν  Dom τ)"
            using assms Map_hcomp [of μ "ν  τ"] Map_hcomp [of ν τ] by simp
          also have
            "... = B.can (Cod μ  Cod ν  Cod τ) (Cod μ  Cod ν  Cod τ) B
                     ((B.can (Cod μ) (Cod μ) B B.can (Cod ν  Cod τ) (Cod ν  Cod τ)) B
                       (Map μ B Map ν B Map τ) B
                         (B.can (Dom μ) (Dom μ) B
                            B.can (Dom ν  Dom τ) (Dom ν  Dom τ))) B
                     B.can (Dom μ  Dom ν  Dom τ) (Dom μ  Dom ν  Dom τ)"
          proof -
            have "Map μ B B.can (Cod ν  Cod τ) (Cod ν  Cod τ) B
                            (Map ν B Map τ) B
                              B.can (Dom ν  Dom τ) (Dom ν  Dom τ) =
                    (B.can (Cod μ) (Cod μ) B B.can (Cod ν  Cod τ) (Cod ν  Cod τ)) B
                       (Map μ B (Map ν B Map τ) B
                          B.can (Dom ν  Dom τ) (Dom ν  Dom τ))"
              using assms B.interchange B.comp_cod_arr
              by (metis (no_types, lifting) B.can_Ide_self B.in_homE Map_hcomp arrE hseq_char)
            also have "... = (B.can (Cod μ) (Cod μ) B
                                 B.can (Cod ν  Cod τ) (Cod ν  Cod τ)) B
                               (Map μ B Map ν B Map τ) B
                                 (B.can (Dom μ) (Dom μ) B
                                    B.can (Dom ν  Dom τ) (Dom ν  Dom τ))"
              using assms B.interchange B.comp_arr_dom [of "Map μ" "B.can (Dom μ) (Dom μ)"]
              by (metis (no_types, lifting) B.can_Ide_self B.null_is_zero(2) B.ext B.in_homE
                  Map_hcomp arrE hseq_char)
            finally have
              "Map μ B B.can (Cod ν  Cod τ) (Cod ν  Cod τ) B
                 (Map ν B Map τ) B
                   B.can (Dom ν  Dom τ) (Dom ν  Dom τ) =
              (B.can (Cod μ) (Cod μ) B B.can (Cod ν  Cod τ) (Cod ν  Cod τ)) B
                (Map μ B Map ν B Map τ) B
                  (B.can (Dom μ) (Dom μ) B B.can (Dom ν  Dom τ) (Dom ν  Dom τ))"
              by simp
            thus ?thesis by simp
          qed
          also have
            "... = (B.can (Cod μ  Cod ν  Cod τ) (Cod μ  Cod ν  Cod τ) B
                     (B.can (Cod μ) (Cod μ) B B.can (Cod ν  Cod τ) (Cod ν  Cod τ))) B
                       (Map μ B Map ν B Map τ) B
                         ((B.can (Dom μ) (Dom μ) B
                             B.can (Dom ν  Dom τ) (Dom ν  Dom τ)) B
                           B.can (Dom μ  Dom ν  Dom τ) (Dom μ  Dom ν  Dom τ))"
            using B.comp_assoc by simp
          also have "... = B.can (Cod μ  Cod ν  Cod τ) (Cod μ  Cod ν  Cod τ) B
                             (Map μ B Map ν B Map τ) B
                                B.can (Dom μ  Dom ν  Dom τ) (Dom μ  Dom ν  Dom τ)"
            using assms μν ντ E.HcompNml_assoc src_def trg_def arr_char
                  E.Src_HcompNml E.Trg_HcompNml E.Nml_HcompNml E.Ide_HcompNml
            by simp
          finally show ?thesis by simp
        qed
        ultimately show ?thesis by metis
      qed
    qed

    lemma obj_char:
    shows "obj a  endo a  E.Obj (Dom a)  Map a = Dom a"
    proof
      assume a: "obj a"
      show "endo a  E.Obj (Dom a)  Map a = Dom a"
      proof (intro conjI)
        show "endo a"
          using a ide_char by blast
        show "E.Obj (Dom a)"
          using a ide_char src_def
          by (metis (no_types, lifting) E.Ide_implies_Arr E.Obj_Trg arrE obj_def
              trg_simps(1) trg_src) 
        show "Map a = Dom a"
          using a ide_char src_def by blast
      qed
      next
      assume a: "endo a  E.Obj (Dom a)  Map a = Dom a"
      show "obj a"
      proof -
        have "arr a" using a by auto
        moreover have "src a = a"
          using a E.Obj_in_Hom(1) seq_char by (intro arr_eqI, auto)
        ultimately show ?thesis
          using obj_def by simp
      qed
    qed

    lemma hcomp_obj_self:
    assumes "obj a"
    shows "a  a = a"
    proof (intro arr_eqI)
      show "hseq a a"
        using assms by auto
      show "arr a"
        using assms by auto
      show 1: "Dom (a  a) = Dom a"
        unfolding hcomp_def
        using assms arr_char E.HcompNml_Trg_Nml
        apply simp
        by (metis (no_types, lifting) objE obj_def trg_simps(1))
      show 2: "Cod (a  a) = Cod a"
        unfolding hcomp_def
        using assms 1 arr_char E.HcompNml_Trg_Nml
        apply simp
        by (metis (no_types, lifting) Dom_hcomp ideE objE)
      show "Map (a  a) = Map a"
        using "1" Map_ide(1) assms by fastforce
    qed

    lemma hcomp_ide_src:
    assumes "ide f"
    shows "f  src f = f"
    proof (intro arr_eqI)
      show "hseq f (src f)"
        using assms by simp
      show "arr f"
        using assms by simp
      show 1: "Dom (f  src f) = Dom f"
        unfolding hcomp_def
        using assms apply simp
        using assms ide_char arr_char E.HcompNml_Nml_Src
        by (metis (no_types, lifting) ideD(1))
      show "Cod (f  src f) = Cod f"
        unfolding hcomp_def
        using assms apply simp
        using assms ide_char arr_char E.HcompNml_Nml_Src
        by (metis (no_types, lifting) ideD(1))
      show "Map (f  src f) = Map f"
        by (simp add: "1" Map_ide(1) assms)
    qed

    lemma hcomp_trg_ide:
    assumes "ide f"
    shows "trg f  f = f"
    proof (intro arr_eqI)
      show "hseq (trg f) f"
        using assms by auto
      show "arr f"
        using assms by auto
      show 1: "Dom (trg f  f) = Dom f"
        unfolding hcomp_def
        using assms apply simp
        using assms ide_char arr_char E.HcompNml_Trg_Nml
        by (metis (no_types, lifting) ideD(1))
      show "Cod (trg f  f) = Cod f"
        unfolding hcomp_def
        using assms apply simp
        using assms ide_char arr_char E.HcompNml_Trg_Nml
        by (metis (no_types, lifting)  ideD(1))
      show "Map (trg f  f) = Map f"
        by (simp add: "1" Map_ide(1) assms)
    qed

    interpretation L: full_functor vcomp vcomp L
    proof
      fix a a' g
      assume a: "ide a" and a': "ide a'"
      assume g: "in_hom g (L a') (L a)"
      have a_eq: "a = MkIde (Dom a)"
        using a dom_char [of a] by simp
      have a'_eq: "a' = MkIde (Dom a')"
        using a' dom_char [of a'] by simp
      have 1: "Cod g = Dom a"
      proof -
        have "Dom (L a) = Dom a"
          by (simp add: a hcomp_trg_ide)
        thus ?thesis
          using g cod_char [of g]
          by (metis (no_types, lifting) Dom_cod in_homE)
      qed
      have 2: "Dom g = Dom a'"
        using a' g hcomp_trg_ide in_hom_char by auto
      let ?f = "MkArr (Dom a') (Cod a) (Map g)"
      have f: "in_hom ?f a' a"
        by (metis (no_types, lifting) "1" "2" MkArr_Map a a' g ideE in_hom_char)
      moreover have "L ?f = g"
      proof -
        have "L ?f =
              trg (MkArr (Dom a') (Cod a) (Map g))  MkArr (Dom a') (Cod a) (Map g)"
          using f by auto
        also have "... = MkIde (E.Trg (Cod a))  MkArr (Dom a') (Cod a) (Map g)"
          using a a' f trg_def [of a] vconn_implies_hpar by auto
        also have "... = MkArr (E.Trg (Cod a)  Dom a') (E.Trg (Cod a)  Cod a)
                               (B.can (E.Trg (Cod a)  Cod a) (E.Trg (Cod a)  Cod a) B
                                 (E.Trg (Cod a) B Map g) B
                                 B.can (E.Trg (Cod a)  Dom a') (E.Trg (Cod a)  Dom a'))"
          using hcomp_def
          apply simp
          by (metis (no_types, lifting) Cod.simps(1) arrE f in_homE src_trg trg.preserves_arr
              trg_def)
        also have "... = MkArr (Dom a') (Cod a)
                               (B.can (Cod a) (E.Trg (Cod a)  Cod a) B
                                 (trgB Cod a B Map g) B
                                 B.can (E.Trg (Cod a)  Dom a') (Dom a'))"
        proof -
          have "E.Trg (Cod a)  Dom a' = Dom a'"
            using a a' arr_char E.HcompNml_Trg_Nml
            by (metis (no_types, lifting) f ideE trg_simps(1) vconn_implies_hpar(4))
          moreover have "E.Trg (Cod a)  Cod a = Cod a"
            using a a' arr_char E.HcompNml_Trg_Nml by blast
          moreover have "E.Trg (Cod a) = trgB Cod a"
            using a a' arr_char E.eval_simps'(3) by fastforce
          ultimately show ?thesis by simp
        qed
        also have "... = MkArr (Dom a') (Cod a)
                           (B.lunit Cod a B (trgB Cod a B Map g) B B.lunit' Dom a')"
        proof -
          have "E.Trg (Cod a) = E.Trg (Dom a')"
            using a a' a_eq g ide_char arr_char src_def trg_def trg_hcomp
                  Cod g = Dom a Dom g = Dom a'
            by (metis (no_types, lifting) Cod.simps(1) in_homE)
          moreover have "B.can (Cod a) (E.Trg (Cod a)  Cod a) = B.lunit Cod a"
            using a ide_char arr_char B.canE_unitor(2) by blast
          moreover have "B.can (E.Trg (Dom a')  Dom a') (Dom a') = B.lunit' Dom a'"
            using a' ide_char arr_char B.canE_unitor(4) by blast
          ultimately show ?thesis by simp
        qed
        also have "... = MkArr (Dom g) (Cod g) (Map g)"
        proof -
          have "srcB Cod a = srcB (Map g)"
            using a f g ide_char arr_char src_def B.comp_cod_arr
            by (metis (no_types, lifting) B.vconn_implies_hpar(1) B.vconn_implies_hpar(3)
                Cod.simps(1) Map.simps(1) in_homE)
          moreover have
            "B.lunit Cod g B (trgB (Map g) B Map g) B B.lunit' Dom g = Map g"
          proof -
            have "B.lunit Cod g B (trgB (Map g) B Map g) B B.lunit' Dom g =
                  B.lunit Cod g B B.lunit' Cod g B Map g"
              using g ide_char arr_char B.lunit'_naturality
              by (metis (no_types, lifting) partial_composition_axioms B.in_homE
                  partial_composition.arrI)
            also have "... = (B.lunit Cod g B B.lunit' Cod g) B Map g"
              using B.comp_assoc by simp
            also have "... = Cod g B Map g"
              using g E.ide_eval_Ide B.comp_arr_inv' by fastforce
            also have "... = Map g"
              using g E.ide_eval_Ide B.comp_cod_arr by fastforce
            finally show ?thesis by simp
          qed
          ultimately have
            "B.lunit Cod a B (trgB Cod a B Map g) B B.lunit' Dom a' = Map g"
            using a a' 1 2 f g hcomp_def dom_char cod_char
            by (metis (no_types, lifting) B.null_is_zero(2) B.ext B.lunit_simps(2) B.lunit_simps(3)
                B.src.preserves_reflects_arr B.trg_vcomp B.vseq_implies_hpar(1) ideE)
          thus ?thesis
            using a 1 2 by auto
        qed
        also have "... = g"
          using g MkArr_Map by blast
        finally show ?thesis by simp
      qed
      ultimately show "f. in_hom f a' a  L f = g"
        by blast
    qed

    interpretation R: full_functor vcomp vcomp R
    proof
      fix a a' g
      assume a: "ide a" and a': "ide a'"
      assume g: "in_hom g (R a') (R a)"
      have a_eq: "a = MkIde (Dom a)"
        using a dom_char [of a] by simp
      have a'_eq: "a' = MkIde (Dom a')"
        using a' dom_char [of a'] by simp
      have 1: "Cod g = Dom a"
        using a g hcomp_ide_src in_hom_char by force
      have 2: "Dom g = Dom a'"
        using a' g hcomp_ide_src by auto
      let ?f = "MkArr (Dom a') (Cod a) (Map g)"
      have f: "in_hom ?f a' a"
      proof (intro in_homI)
        show 3: "arr (MkArr (Dom a') (Cod a) (Map g))"
          by (metis (no_types, lifting) "1" "2" Cod.simps(1) MkArr_Map a_eq g in_homE)
        show "dom (MkArr (Dom a') (Cod a) (Map g)) = a'"
          using a a' 3 dom_char by auto
        show "cod (MkArr (Dom a') (Cod a) (Map g)) = a"
          using a a' 3 cod_char by auto
      qed
      moreover have "R ?f = g"
      proof -
        have "R ?f =
               MkArr (Dom a') (Cod a) (Map g)  src (MkArr (Dom a') (Cod a) (Map g))"
          using f by auto
        also have "... = MkArr (Dom a') (Cod a) (Map g)  MkIde (E.Src (Cod a))"
          using a a' f src_def [of a] vconn_implies_hpar by auto
        also have "... = MkArr (Dom a'  E.Src (Cod a)) (Cod a  E.Src (Cod a))
                               (B.can (Cod a  E.Src (Cod a)) (Cod a  E.Src (Cod a)) B
                                 (Map g B E.Src (Cod a)) B
                                 B.can (Dom a'  E.Src (Cod a)) (Dom a'  E.Src (Cod a)))"
          using hcomp_def
          apply simp
          by (metis (no_types, lifting) Cod_cod arrE f in_homE trg_src src.preserves_arr src_def)
        also have "... = MkArr (Dom a') (Cod a)
                               (B.can (Cod a) (Cod a  E.Src (Cod a)) B
                                 (Map g B srcB Cod a) B
                                 B.can (Dom a'  E.Src (Cod a)) (Dom a'))"
        proof -
          have "Dom a'  E.Src (Cod a) = Dom a'"
            using a a' arr_char E.HcompNml_Nml_Src
            by (metis (no_types, lifting) f ideE src_simps(1) vconn_implies_hpar(3))
          moreover have "Cod a  E.Src (Cod a) = Cod a"
            using a a' arr_char E.HcompNml_Nml_Src by blast
          moreover have "E.Src (Cod a) = srcB Cod a"
            using a a' arr_char E.eval_simps'(2) by fastforce
          ultimately show ?thesis by simp
        qed
        also have "... = MkArr (Dom a') (Cod a)
                               (B.runit Cod a B (Map g B srcB Cod a) B B.runit' Dom a')"
          by (metis (no_types, lifting) B.canE_unitor(1) B.canE_unitor(3) a a' arrE f ideE
              src_simps(1) vconn_implies_hpar(3))
        also have "... = MkArr (Dom g) (Cod g) (Map g)"
        proof -
          have "srcB Cod a = srcB (Map g)"
            using a f g ide_char arr_char src_def B.comp_cod_arr
            by (metis (no_types, lifting) B.vconn_implies_hpar(1) B.vconn_implies_hpar(3)
                Cod.simps(1) Map.simps(1) in_homE)
          moreover have
            "B.runit Cod g B (Map g B srcB (Map g)) B B.runit' Dom g = Map g"
          proof -
            have "B.runit Cod g B (Map g B srcB (Map g)) B B.runit' Dom g =
                  B.runit Cod g B B.runit'Cod g B Map g"
              using g ide_char arr_char B.runit'_naturality [of "Map g"]
              by (metis (no_types, lifting) partial_composition_axioms B.in_homE
                  partial_composition.arrI)
            also have "... = (B.runit Cod g B B.runit' Cod g) B Map g"
              using B.comp_assoc by simp
            also have "... = Cod g B Map g"
              using g E.ide_eval_Ide B.comp_arr_inv' by fastforce
            also have "... = Map g"
              using g E.ide_eval_Ide B.comp_cod_arr by fastforce
            finally show ?thesis by simp
          qed
          ultimately have
            "B.runit Cod a B (Map g B srcB Cod a) B B.runit' Dom a' = Map g"
            using a a' 1 2 f g hcomp_def dom_char cod_char
            by (metis (no_types, lifting) ideE)
          thus ?thesis
            using a 1 2 by auto
        qed
        also have "... = g"
           using g MkArr_Map by blast
        finally show ?thesis by simp
      qed
      ultimately show "f. in_hom f a' a  R f = g"
        by blast
    qed

    interpretation L: faithful_functor vcomp vcomp L
    proof
      fix f f'
      assume par: "par f f'" and eq: "L f = L f'"
      show "f = f'"
      proof (intro arr_eqI)
        have 1: "Dom f = Dom f'  Cod f = Cod f'"
          using par dom_char cod_char by auto
        show "arr f"
          using par by simp
        show "arr f'"
          using par by simp
        show 2: "Dom f = Dom f'" and 3: "Cod f = Cod f'"
          using 1 by auto
        show "Map f = Map f'"
        proof -
          have "B.L (Map f) = trgB (Map f) B Map f"
            using par by auto
          also have "... = trgB (Map f') B Map f'"
          proof -
            have "E.Trg (Dom f) B Map f = E.Trg (Dom f') B Map f'"
            proof -
              have A: "«B.can (E.Trg (Dom f)  Dom f) (E.Trg (Dom f)  Dom f) :
                          E.Trg (Dom f)  Dom f B E.Trg (Dom f) B Dom f»"
                using par arr_char B.can_in_hom E.Ide_HcompNml
                      E.Ide_Nmlize_Ide E.Nml_Trg E.Nmlize_Nml E.HcompNml_Trg_Nml
                      src_def trg_def
                by (metis (no_types, lifting) E.eval_simps(3) E.ide_eval_Ide E.Ide_implies_Arr
                    B.canE_unitor(4) B.lunit'_in_vhom)
              have B: "«B.can (E.Trg (Dom f)  Cod f) (E.Trg (Dom f)  Cod f) :
                          E.Trg (Dom f) B Cod f B E.Trg (Dom f)  Cod f»"
                using par arr_char B.can_in_hom E.Ide_HcompNml
                      E.Ide_Nmlize_Ide E.Nml_Trg E.Nmlize_Nml E.HcompNml_Trg_Nml
                      src_def trg_def
                by (metis (no_types, lifting) E.Nmlize.simps(3) E.eval.simps(3) E.Ide.simps(3)
                    E.Ide_implies_Arr E.Src_Trg trg.preserves_arr trg_simps(2))
              have C: "«E.Trg (Dom f) B Map f :
                          E.Trg (Dom f) B Dom f B E.Trg (Dom f) B Cod f»"
                using par arr_char
                by (metis (no_types, lifting) E.eval_simps'(1) E.eval_simps(3) E.ide_eval_Ide
                    E.Ide_implies_Arr E.Obj_Trg E.Obj_implies_Ide B.hcomp_in_vhom
                    B.ide_in_hom(2) B.src_trg)
              have 3: "(E.Trg (Dom f) B Map f) B
                          B.can (E.Trg (Dom f)  Dom f) (E.Trg (Dom f)  Dom f) =
                        (E.Trg (Dom f') B Map f') B
                            B.can (E.Trg (Dom f')  Dom f') (E.Trg (Dom f')  Dom f')"
              proof -
                have 2: "B.can (E.Trg (Dom f)  Cod f) (E.Trg (Dom f)  Cod f) B
                          (E.Trg (Dom f) B Map f) B
                            B.can (E.Trg (Dom f)  Dom f) (E.Trg (Dom f)  Dom f) =
                         B.can (E.Trg (Dom f')  Cod f') (E.Trg (Dom f')  Cod f') B
                           (E.Trg (Dom f') B Map f') B
                             B.can (E.Trg (Dom f')  Dom f') (E.Trg (Dom f')  Dom f')"
                  using par eq hcomp_def trg_def src_trg trg.preserves_arr Map_hcomp
                        trg_simps(1) trg_simps(2) trg_simps(3)
                  by auto
                have "B.mono (B.can (E.Trg (Dom f)  Cod f) (E.Trg (Dom f)  Cod f))"
                  using par arr_char B.inverse_arrows_can B.iso_is_section B.section_is_mono
                        src_def trg_def E.Nmlize_Nml E.HcompNml_Trg_Nml E.Ide_implies_Arr
                        trg.preserves_arr trg_simps(1)
                  by auto
                moreover have
                  "B.seq (B.can (E.Trg (Dom f)  Cod f) (E.Trg (Dom f)  Cod f))
                     ((E.Trg (Dom f) B Map f) B
                       B.can (E.Trg (Dom f)  Dom f) (E.Trg (Dom f)  Dom f))"
                  using A B C by auto
                moreover have
                  "B.seq (B.can (E.Trg (Dom f)  Cod f) (E.Trg (Dom f)  Cod f))
                     ((E.Trg (Dom f') B Map f') B
                       B.can (E.Trg (Dom f')  Dom f') (E.Trg (Dom f')  Dom f'))"
                  using par 1 2 arr_char calculation(2) by auto
                moreover have "B.can (E.Trg (Dom f)  Cod f) (E.Trg (Dom f)  Cod f) =
                               B.can (E.Trg (Dom f')  Cod f') (E.Trg (Dom f')  Cod f')"
                  using par 1 arr_char by simp
                ultimately show ?thesis
                  using 2 B.monoE cod_char by auto
              qed
              show ?thesis
              proof -
                have "B.epi (B.can (E.Trg (Dom f)  Dom f) (E.Trg (Dom f)  Dom f))"
                  using par arr_char B.inverse_arrows_can B.iso_is_retraction
                        B.retraction_is_epi E.Nmlize_Nml E.HcompNml_Trg_Nml src_def trg_def
                        E.Ide_implies_Arr
                  by (metis (no_types, lifting) E.Nmlize.simps(3) E.Ide.simps(3) E.Src_Trg
                      trg.preserves_arr trg_simps(1))
                moreover have "B.seq (E.Trg (Dom f) B Map f)
                                     (B.can (E.Trg (Dom f)  Dom f) (E.Trg (Dom f)  Dom f))"
                  using A C by auto
                moreover have "B.seq (E.Trg (Dom f') B Map f')
                                     (B.can (E.Trg (Dom f)  Dom f) (E.Trg (Dom f)  Dom f))"
                  using 1 3 calculation(2) by auto
                ultimately show ?thesis
                  using par 1 3 arr_char B.epiE by simp
              qed
            qed
            moreover have "trgB (Map f) = E.Trg (Dom f) 
                           trgB (Map f') = E.Trg (Dom f')"
              using par arr_char trg_def E.Ide_implies_Arr B.comp_arr_dom
                    B.vseq_implies_hpar(2) E.eval_simps(3)
              by (metis (no_types, lifting) B.vconn_implies_hpar(2))
            ultimately show ?thesis by simp
          qed
          also have "... = B.L (Map f')"
            using par B.hseqE B.hseq_char' by auto
          finally have "B.L (Map f) = B.L (Map f')"
            by simp
          thus ?thesis
            using 2 3 par arr_char B.L.is_faithful
            by (metis (no_types, lifting) B.in_homE)
        qed
      qed
    qed

    interpretation R: faithful_functor vcomp vcomp R
    proof
      fix f f'
      assume par: "par f f'" and eq: "R f = R f'"
      show "f = f'"
      proof (intro arr_eqI)
        have 1: "Dom f = Dom f'  Cod f = Cod f'"
          using par dom_char cod_char by auto
        show "arr f"
          using par by simp
        show "arr f'"
          using par by simp
        show 2: "Dom f = Dom f'" and 3: "Cod f = Cod f'"
          using 1 by auto
        show "Map f = Map f'"
        proof -
          have "B.R (Map f) = Map f B srcB (Map f)"
            using par apply simp by (metis B.hseqE B.hseq_char')
          also have "... = Map f' B srcB (Map f')"
          proof -
            have "Map f B E.Src (Dom f) = Map f' B E.Src (Dom f')"
            proof -
              have 2: "E.Ide (Cod f  E.Src (Dom f))"
                using par arr_char src.preserves_arr by auto
              hence 3: "E.Ide (Cod f  E.Src (Dom f))"
                using par arr_char E.Nml_Src E.Ide_HcompNml calculation by auto
              have 4: "Cod f  E.Src (Dom f) = Cod f  E.Src (Dom f)"
                using par arr_char by (simp add: E.Nml_HcompNml(1))
              have A: "«B.can (Dom f  E.Src (Dom f)) (Dom f  E.Src (Dom f)) :
                          Dom f  E.Src (Dom f) B Dom f B E.Src (Dom f)»"
                using par arr_char B.can_in_hom E.Ide_HcompNml
                      E.Ide_Nmlize_Ide E.Nml_Src E.Nmlize_Nml E.HcompNml_Nml_Src
                      src_def trg_def
                by (metis (no_types, lifting) E.eval_simps(2) E.ide_eval_Ide E.Ide_implies_Arr
                    B.canE_unitor(3) B.runit'_in_vhom)
              have B: "«B.can (Cod f  E.Src (Dom f)) (Cod f  E.Src (Dom f)) :
                          Cod f B E.Src (Dom f) B Cod f  E.Src (Dom f)»"
                using 2 3 4 B.can_in_hom [of "Cod f  E.Src (Dom f)" "Cod f  E.Src (Dom f)"]
                by simp
              have C: "«Map f B E.Src (Dom f) :
                         Dom f B E.Src (Dom f) B Cod f B E.Src (Dom f)»"
                using par arr_char E.Ide_Nmlize_Ide E.Nml_Trg E.Nmlize_Nml E.HcompNml_Trg_Nml
                      src_def trg_def E.ide_eval_Ide E.Ide_implies_Arr E.Obj_implies_Ide
                apply (intro B.hcomp_in_vhom)
                  apply (simp add: B.ide_in_hom(2))
                 apply simp
                by (metis (no_types, lifting) A B.ideD(1) B.not_arr_null B.seq_if_composable
                    B.src.preserves_reflects_arr B.vconn_implies_hpar(3) E.HcompNml_Nml_Src)
              have 5: "(Map f B E.Src (Dom f)) B
                          B.can (Dom f  E.Src (Dom f)) (Dom f  E.Src (Dom f)) =
                        (Map f' B E.Src (Dom f')) B
                            B.can (Dom f'  E.Src (Dom f')) (Dom f'  E.Src (Dom f'))"
              proof -
                have 6: "B.can (Cod f  E.Src (Dom f)) (Cod f  E.Src (Dom f)) B
                           (Map f B E.Src (Dom f)) B
                             B.can (Dom f  E.Src (Dom f)) (Dom f  E.Src (Dom f)) =
                         B.can (Cod f'  E.Src (Dom f')) (Cod f'  E.Src (Dom f')) B
                           (Map f' B E.Src (Dom f')) B
                             B.can (Dom f'  E.Src (Dom f')) (Dom f'  E.Src (Dom f'))"
                  using par eq hcomp_def src_def trg_src src.preserves_arr Map_hcomp
                        src_simps(1) src_simps(2) src_simps(3)
                  by auto
                have "B.mono (B.can (Cod f  E.Src (Dom f)) (Cod f  E.Src (Dom f)))"
                  using 2 3 4 B.inverse_arrows_can(1) B.iso_is_section B.section_is_mono
                  by simp
                moreover have
                  "B.seq (B.can (Cod f  E.Src (Dom f)) (Cod f  E.Src (Dom f)))
                     ((Map f B E.Src (Dom f)) B
                       B.can (Dom f  E.Src (Dom f)) (Dom f  E.Src (Dom f)))"
                  using A B C by auto
                moreover have
                  "B.seq (B.can (Cod f  E.Src (Dom f)) (Cod f  E.Src (Dom f)))
                     ((Map f' B E.Src (Dom f')) B
                       B.can (Dom f'  E.Src (Dom f')) (Dom f'  E.Src (Dom f')))"
                  using par 1 6 arr_char calculation(2) by auto
                moreover have "B.can (Cod f  E.Src (Dom f)) (Cod f  E.Src (Dom f)) =
                               B.can (Cod f'  E.Src (Dom f')) (Cod f'  E.Src (Dom f'))"
                  using par 1 arr_char by simp
                ultimately show ?thesis
                  using 6 B.monoE cod_char by auto
              qed
              show ?thesis
              proof -
                have "B.epi (B.can (Dom f  E.Src (Dom f)) (Dom f  E.Src (Dom f)))"
                  using 2 3 4 B.inverse_arrows_can(1) B.iso_is_retraction B.retraction_is_epi
                  by (metis (no_types, lifting) E.Nml_Src E.Nmlize.simps(3) E.Nmlize_Nml
                      E.HcompNml_Nml_Src E.Ide.simps(3) par arrE)
                moreover have "B.seq (Map f B E.Src (Dom f))
                                   (B.can (Dom f  E.Src (Dom f)) (Dom f  E.Src (Dom f)))"
                  using A C by auto
                moreover have "B.seq (Map f' B E.Src (Dom f'))
                                   (B.can (Dom f  E.Src (Dom f)) (Dom f  E.Src (Dom f)))"
                  using 1 5 calculation(2) by auto
                ultimately show ?thesis
                  using par 1 5 arr_char B.epiE by simp
              qed
            qed
            moreover have "srcB (Map f) = E.Src (Dom f) 
                           srcB (Map f') = E.Src (Dom f')"
              using par arr_char src_def
              by (metis (no_types, lifting) B.vconn_implies_hpar(1) E.Nml_implies_Arr
                  E.eval_simps(2))
            ultimately show ?thesis by simp
          qed
          also have "... = B.R (Map f')"
            using par B.hseqE B.hseq_char' by auto
          finally have "B.R (Map f) = B.R (Map f')"
            by simp
          thus ?thesis
            using 2 3 par arr_char B.R.is_faithful
            by (metis (no_types, lifting) B.in_homE)
        qed
      qed
    qed

    definition 𝖺
    where "𝖺 τ μ ν  if VVV.arr (τ, μ, ν) then hcomp τ (hcomp μ ν) else null"

    interpretation natural_isomorphism VVV.comp vcomp HoHV HoVH
                     λτμν. 𝖺 (fst τμν) (fst (snd τμν)) (snd (snd τμν))
    proof
      show "τμν. ¬ VVV.arr τμν  𝖺 (fst τμν) (fst (snd τμν)) (snd (snd τμν)) = null"
        using 𝖺_def by simp
      show "τμν. VVV.arr τμν 
                  dom (𝖺 (fst τμν) (fst (snd τμν)) (snd (snd τμν))) = HoHV (VVV.dom τμν)"
        using VVV.arr_charSbC VV.arr_charSbC 𝖺_def hcomp_assoc HoHV_def VVV.dom_simp VV.dom_simp
        by force
      show 1: "τμν. VVV.arr τμν 
                     cod (𝖺 (fst τμν) (fst (snd τμν)) (snd (snd τμν))) = HoVH (VVV.cod τμν)"
        using VVV.arr_charSbC VV.arr_charSbC 𝖺_def HoVH_def VVV.cod_simp VV.cod_simp by force
      show "τμν. VVV.arr τμν 
                  HoVH τμν 
                    𝖺 (fst (VVV.dom τμν)) (fst (snd (VVV.dom τμν)))
                      (snd (snd (VVV.dom τμν))) =
                  𝖺 (fst τμν) (fst (snd τμν)) (snd (snd τμν))"
        using 𝖺_def HoVH.as_nat_trans.is_natural_1 HoVH_def by auto
      show "τμν. VVV.arr τμν 
                   𝖺 (fst (VVV.cod τμν)) (fst (snd (VVV.cod τμν)))
                     (snd (snd (VVV.cod τμν)))  HoHV τμν =
                   𝖺 (fst τμν) (fst (snd τμν)) (snd (snd τμν))"
      proof -
        fix τμν
        assume τμν: "VVV.arr τμν"
        have "HoHV τμν = 𝖺 (fst τμν) (fst (snd τμν)) (snd (snd τμν))"
          unfolding 𝖺_def HoHV_def
          using τμν HoHV.preserves_cod hcomp_assoc VVV.arr_charSbC VV.arr_charSbC
          by simp
        thus "𝖺 (fst (VVV.cod τμν)) (fst (snd (VVV.cod τμν))) (snd (snd (VVV.cod τμν))) 
                HoHV τμν =
              𝖺 (fst τμν) (fst (snd τμν)) (snd (snd τμν))"
          using 1 τμν comp_cod_arr 𝖺_def
          by (metis (no_types, lifting) HoVH_def HoHV.preserves_arr prod.collapse)
      qed
      show "fgh. VVV.ide fgh  iso (𝖺 (fst fgh) (fst (snd fgh)) (snd (snd fgh)))"
        using 𝖺_def HoVH.preserves_ide HoVH_def by auto
    qed

    definition 𝗂
    where "𝗂  λa. a"

    sublocale bicategory vcomp hcomp 𝖺 𝗂 src trg
      using hcomp_obj_self 𝖺_def hcomp_assoc VVV.arr_charSbC VV.arr_charSbC
      apply unfold_locales
      by (auto simp add: 𝗂_def ide_in_hom(2))

    lemma is_bicategory:
    shows "bicategory vcomp hcomp 𝖺 𝗂 src trg"
      ..

    sublocale strict_bicategory vcomp hcomp 𝖺 𝗂 src trg
    proof
      show "fgh. ide fgh  lunit fgh = fgh"
      proof -
        fix fgh
        assume fgh: "ide fgh"
        have "fgh = lunit fgh"
        proof (intro lunit_eqI)
          show "ide fgh" using fgh by simp
          show "«fgh : trg fgh  fgh  fgh»"
            using fgh hcomp_def hcomp_trg_ide by auto
          show "trg fgh  fgh = (𝗂 (trg fgh)  fgh)  𝖺' (trg fgh) (trg fgh) fgh"
          proof -
            have "(𝗂 (trg fgh)  fgh)  𝖺' (trg fgh) (trg fgh) fgh =
                  (trg fgh  fgh)  𝖺' (trg fgh) (trg fgh) fgh"
              using fgh 𝗂_def by metis
            also have "... = (trg fgh  fgh)  (trg fgh  trg fgh  fgh)"
              using fgh 𝖺_def by fastforce
            also have "... = trg fgh  fgh"
              using fgh hcomp_obj_self hcomp_assoc
              by (simp add: hcomp_trg_ide)
            finally show ?thesis by simp
          qed
        qed
        thus "lunit fgh = fgh" by simp
      qed
      show "fgh. ide fgh  runit fgh = fgh"
      proof -
        fix fgh
        assume fgh: "ide fgh"
        have "fgh = runit fgh"
        proof (intro runit_eqI)
          show "ide fgh" using fgh by simp
          show "«fgh : fgh  src fgh  fgh»"
            using fgh hcomp_def hcomp_ide_src by auto
          show "fgh  src fgh = (fgh  𝗂 (src fgh))  𝖺 fgh (src fgh) (src fgh)"
          proof -
            have "(fgh  𝗂 (src fgh))  𝖺 fgh (src fgh) (src fgh) =
                  (fgh  src fgh)  𝖺 fgh (src fgh) (src fgh)"
              using fgh 𝗂_def by metis
            also have "... = (fgh  src fgh)  (fgh  src fgh  src fgh)"
              using fgh 𝖺_def by fastforce
            also have "... = fgh  src fgh"
              using fgh comp_arr_dom hcomp_obj_self by simp
            finally show ?thesis by simp
          qed
        qed
        thus "runit fgh = fgh" by simp
      qed
      show "f g h.  ide f; ide g; ide h; src f = trg g; src g = trg h   ide (𝖺 f g h)"
        using 𝖺_def VV.arr_charSbC VVV.arr_charSbC by auto
    qed

    theorem is_strict_bicategory:
    shows "strict_bicategory vcomp hcomp 𝖺 𝗂 src trg"
      ..

    lemma iso_char:
    shows "iso μ  arr μ  B.iso (Map μ)"
    and "iso μ  inv μ = MkArr (Cod μ) (Dom μ) (B.inv (Map μ))"
    proof -
      have 1: "iso μ  arr μ  B.iso (Map μ)"
      proof -
        assume μ: "iso μ"
        obtain ν where ν: "inverse_arrows μ ν"
          using μ by auto
        have "B.inverse_arrows (Map μ) (Map ν)"
        proof
          show "B.ide (Map μ B Map ν)"
          proof -
            have "Map μ B Map ν = Map (μ  ν)"
              using μ ν inverse_arrows_def Map_comp arr_char seq_char
              by (metis (no_types, lifting) ide_compE)
            moreover have "B.ide ..."
              using ν ide_char by blast
            ultimately show ?thesis by simp
          qed
          show "B.ide (Map ν B Map μ)"
          proof -
            have "Map ν B Map μ = Map (ν  μ)"
              using μ ν inverse_arrows_def comp_char [of ν μ] by simp
            moreover have "B.ide ..."
              using ν ide_char by blast
            ultimately show ?thesis by simp
          qed
        qed
        thus "arr μ  B.iso (Map μ)"
          using μ by auto
      qed
      let  = "MkArr (Cod μ) (Dom μ) (B.inv (Map μ))"
      have 2: "arr μ  B.iso (Map μ)  iso μ  inv μ = "
      proof
        assume μ: "arr μ  B.iso (Map μ)"
        have ν: "« : cod μ  dom μ»"
          using μ arr_char dom_char cod_char by auto
        have 4: "inverse_arrows μ "
        proof
          show "ide (  μ)"
          proof -
            have "  μ = dom μ"
              using μ ν MkArr_Map comp_char seq_char B.comp_inv_arr' dom_char by auto
            thus ?thesis
              using μ by simp
          qed
          show "ide (μ  )"
          proof -
            have "μ   = cod μ"
              using μ ν MkArr_Map comp_char seq_char B.comp_arr_inv' cod_char by auto
            thus ?thesis
              using μ by simp
          qed
        qed
        thus "iso μ" by auto
        show "inv μ = "
          using 4 inverse_unique by simp
      qed
      have 3: "arr μ  B.iso (Map μ)  iso μ"
        using 2 by simp
      show "iso μ  arr μ  B.iso (Map μ)"
        using 1 3 by blast
      show "iso μ  inv μ = "
        using 1 2 by blast
    qed

    subsection "The Strictness Theorem"

    text ‹
      The Strictness Theorem asserts: ``Every bicategory is biequivalent to a strict bicategory.''
      This amounts to an equivalent (and perhaps more desirable) formulation of the
      Coherence Theorem.
      In this section we prove the Strictness Theorem by constructing an equivalence pseudofunctor
      from a bicategory to its strictification.
    ›

    text ‹
      We define a map UP› from the given bicategory B› to its strictification,
      and show that it is an equivalence pseudofunctor.
      The following auxiliary definition is not logically necessary, but it provides some
      terms that can be the targets of simplification rules and thereby enables some proofs
      to be done by simplification that otherwise could not be.  Trying to eliminate it
      breaks some short proofs below, so I have kept it.
    ›

    definition UP0
    where "UP0 a  if B.obj a then MkIde a0 else null"

    lemma obj_UP0 [simp]:
    assumes "B.obj a"
    shows "obj (UP0 a)"
      unfolding obj_def
      using assms UP0_def ide_MkIde [of "a0"] src_def by simp

    lemma UP0_in_hom [intro]:
    assumes "B.obj a"
    shows "«UP0 a : UP0 a  UP0 a»"
    and "«UP0 a : UP0 a  UP0 a»"
      using assms obj_UP0 by blast+

    lemma UP0_simps [simp]:
    assumes "B.obj a"
    shows "ide (UP0 a)" "arr (UP0 a)"
    and "src (UP0 a) = UP0 a" and "trg (UP0 a) = UP0 a"
    and "dom (UP0 a) = UP0 a" and "cod (UP0 a) = UP0 a"
      using assms obj_UP0
           apply blast
      using assms obj_UP0 obj_simps
      by simp_all

    definition UP
    where "UP μ  if B.arr μ then MkArr B.dom μ B.cod μ μ else null"

    lemma Dom_UP [simp]:
    assumes "B.arr μ"
    shows "Dom (UP μ) = B.dom μ"
      using assms UP_def by fastforce

    lemma Cod_UP [simp]:
    assumes "B.arr μ"
    shows "Cod (UP μ) = B.cod μ"
      using assms UP_def by fastforce

    lemma Map_UP [simp]:
    assumes "B.arr μ"
    shows "Map (UP μ) = μ"
      using assms UP_def by fastforce

    lemma arr_UP:
    assumes "B.arr μ"
    shows "arr (UP μ)"
      using assms UP_def
      by (intro arrI, fastforce+)

    lemma UP_in_hom [intro]:
    assumes "B.arr μ"
    shows "«UP μ : UP0 (srcB μ)  UP0 (trgB μ)»"
    and "«UP μ : UP (B.dom μ)  UP (B.cod μ)»"
      using assms arr_UP UP_def UP0_def dom_char cod_char src_def trg_def by auto

    lemma UP_simps [simp]:
    assumes "B.arr μ"
    shows "arr (UP μ)"
    and "src (UP μ) = UP0 (srcB μ)" and "trg (UP μ) = UP0 (trgB μ)"
    and "dom (UP μ) = UP (B.dom μ)" and "cod (UP μ) = UP (B.cod μ)"
      using assms arr_UP UP_in_hom by auto

    interpretation UP: "functor" VB vcomp UP
      using UP_def arr_UP UP_simps(4-5) arr_UP UP_def comp_char seq_char
      by unfold_locales auto

    interpretation UP: weak_arrow_of_homs VB srcB trgB vcomp src trg UP
    proof
      fix μ
      assume μ: "B.arr μ"
      show "isomorphic (UP (srcB μ)) (src (UP μ))"
      proof -
        let  = "MkArr srcB μ srcB μ0 (srcB μ)"
        have φ: "« : UP (srcB μ)  src (UP μ)»"
        proof
          show 1: "arr "
            using μ by (intro arrI, auto)
          show "dom  = UP (srcB μ)"
            using μ 1 dom_char UP_def by simp
          show "cod  = src (UP μ)"
            using μ 1 cod_char src_def by auto
        qed
        have "iso "
          using μ φ iso_char src_def by auto
        thus ?thesis
          using φ isomorphic_def by auto
      qed
      show "isomorphic (UP (trgB μ)) (trg (UP μ))"
      proof -
        let  = "MkArr trgB μ trgB μ0 (trgB μ)"
        have φ: "« : UP (trgB μ)  trg (UP μ)»"
        proof
          show 1: "arr "
            using μ by (intro arrI, auto)
          show "dom  = UP (trgB μ)"
            using μ 1 dom_char UP_def by simp
          show "cod  = trg (UP μ)"
            using μ 1 cod_char trg_def by auto
        qed
        have "iso "
          using μ φ iso_char trg_def by auto
        thus ?thesis
          using φ isomorphic_def by auto
      qed
    qed

    interpretation HoUP_UP: composite_functor B.VV.comp VV.comp vcomp
                              UP.FF λμν. hcomp (fst μν) (snd μν) ..
    interpretation UPoH: composite_functor B.VV.comp VB vcomp
                           λμν. fst μν B snd μν UP ..

    abbreviation Φo
    where "Φo fg  MkArr (fst fg  snd fg) fst fg B snd fg (fst fg B snd fg)"

    interpretation Φ: transformation_by_components
                        B.VV.comp vcomp HoUP_UP.map UPoH.map Φo
    proof
      fix fg
      assume fg: "B.VV.ide fg"
      show "«Φo fg : HoUP_UP.map fg  UPoH.map fg»"
      proof (intro in_homI)
        show 1: "arr (Φo fg)"
          using fg arr_char B.VV.ide_charSbC B.VV.arr_charSbC by auto
        show "dom (Φo fg) = HoUP_UP.map fg"
          using 1 fg UP.FF_def B.VV.arr_charSbC B.VV.ide_charSbC dom_char hcomp_def B.can_Ide_self
          by simp
        show "cod (Φo fg) = UPoH.map fg"
          using fg arr_char cod_char B.VV.ide_charSbC B.VV.arr_charSbC UP_def by auto
      qed
      next
      fix μν
      assume μν: "B.VV.arr μν"
      show "Φo (B.VV.cod μν)  HoUP_UP.map μν = UPoH.map μν  Φo (B.VV.dom μν)"
      proof -
        have "Φo (B.VV.cod μν)  HoUP_UP.map μν =
              MkArr (B.dom (fst μν)  B.dom (snd μν))
                    (B.cod (fst μν) B B.cod (snd μν))
                    (fst μν B snd μν)"
        proof -
          have "Φo (B.VV.cod μν)  HoUP_UP.map μν =
                MkArr (B.cod (fst μν)  B.cod (snd μν)) (B.cod (fst μν) B B.cod (snd μν))
                      (B.cod (fst μν) B B.cod (snd μν)) 
                MkArr (B.dom (fst μν)  B.dom (snd μν))
                      (B.cod (fst μν)  B.cod (snd μν))
                      (fst μν B snd μν)"
            using μν B.VV.arr_charSbC arr_char UP.FF_def hcomp_def UP_def B.VV.cod_simp
                  src_def trg_def B.can_in_hom B.can_Ide_self B.comp_arr_dom B.comp_cod_arr
            by auto
          also have "... = MkArr (B.dom (fst μν)  B.dom (snd μν))
                                 (B.cod (fst μν) B B.cod (snd μν))
                                 ((B.cod (fst μν) B B.cod (snd μν)) B (fst μν B snd μν))"
            using μν B.VV.arr_charSbC
            by (intro comp_MkArr arr_MkArr, auto)
          also have "... = MkArr (B.dom (fst μν)  B.dom (snd μν))
                                 (B.cod (fst μν) B B.cod (snd μν))
                                 (fst μν B snd μν)"
            using μν B.VV.arr_charSbC B.comp_cod_arr by auto
          finally show ?thesis by simp
        qed
        also have "... = UPoH.map μν  Φo (B.VV.dom μν)"
        proof -
          have "UPoH.map μν  Φo (B.VV.dom μν) =
                MkArr (B.dom (fst μν) B B.dom (snd μν))
                      (B.cod (fst μν) B B.cod (snd μν))
                      (fst μν B snd μν) 
                MkArr (B.dom (fst μν)  B.dom (snd μν))
                      (B.dom (fst μν) B B.dom (snd μν))
                      (B.dom (fst μν) B B.dom (snd μν))"
            using μν B.VV.arr_charSbC arr_char UP.FF_def hcomp_def UP_def B.VV.dom_simp
                  src_def trg_def B.can_in_hom B.can_Ide_self B.comp_arr_dom B.comp_cod_arr
            by auto
          also have "... = MkArr (B.dom (fst μν)  B.dom (snd μν))
                                 (B.cod (fst μν) B B.cod (snd μν))
                                 ((fst μν B snd μν) B (B.dom (fst μν) B B.dom (snd μν)))"
            using μν B.VV.arr_charSbC arr_MkArr
            apply (intro comp_MkArr arr_MkArr) by auto
          also have "... = MkArr (B.dom (fst μν)  B.dom (snd μν))
                                 (B.cod (fst μν) B B.cod (snd μν))
                                 (fst μν B snd μν)"
            using μν B.VV.arr_charSbC B.comp_arr_dom by auto
         finally show ?thesis by simp
        qed
        finally show ?thesis by simp
      qed
    qed

    abbreviation cmpUP
    where "cmpUP  Φ.map"

    lemma cmpUP_in_hom [intro]:
    assumes "B.arr (fst μν)" and "B.arr (snd μν)" and "srcB (fst μν) = trgB (snd μν)"
    shows "«cmpUP μν : UP0 (srcB (snd μν))  UP0 (trgB (fst μν))»"
    and "«cmpUP μν : UP (B.dom (fst μν))  UP (B.dom (snd μν))
                     UP (B.cod (fst μν) B B.cod (snd μν))»"
    proof -
      let  = "fst μν" and  = "snd μν"
      show 1: "«cmpUP μν :
                  UP (B.dom )  UP (B.dom )  UP (B.cod  B B.cod )»"
      proof
        show "arr (cmpUP μν)"
          using assms by auto
        show "dom (cmpUP μν) = UP (B.dom )  UP (B.dom )"
        proof -
          have "B.VV.in_hom (, ) (B.dom , B.dom ) (B.cod , B.cod )"
            using assms B.VV.in_hom_charSbC B.VV.arr_charSbC by auto
          hence "dom (cmpUP μν) = HoUP_UP.map (B.dom , B.dom )"
            by auto
          also have "... = UP (B.dom )  UP (B.dom )"
            using assms UP.FF_def by fastforce
          finally show ?thesis by simp
        qed
        show "cod (cmpUP μν) = UP (B.cod  B B.cod )"
          using assms B.VV.in_hom_charSbC B.VV.arr_charSbC B.VV.cod_simp by auto
      qed
      show "«cmpUP μν : UP0 (srcB )  UP0 (trgB )»"
        using assms 1 src_dom [of "cmpUP μν"] trg_dom [of "cmpUP μν"] by fastforce
    qed

    lemma cmpUP_simps [simp]:
    assumes "B.arr (fst μν)" and "B.arr (snd μν)" and "srcB (fst μν) = trgB (snd μν)"
    shows "arr (cmpUP μν)"
    and "src (cmpUP μν) = UP0 (srcB (snd μν))" and "trg (cmpUP μν) = UP0 (trgB (fst μν))"
    and "dom (cmpUP μν) = UP (B.dom (fst μν))  UP (B.dom (snd μν))"
    and "cod (cmpUP μν) = UP (B.cod (fst μν) B B.cod (snd μν))"
      using assms cmpUP_in_hom [of μν] by auto

    lemma cmpUP_ide_simps [simp]:
    assumes "B.ide (fst fg)" and "B.ide (snd fg)" and "srcB (fst fg) = trgB (snd fg)"
    shows "Dom (cmpUP fg) = fst fg  snd fg"
    and "Cod (cmpUP fg) = fst fg B snd fg"
    and "Map (cmpUP fg) = fst fg B snd fg"
      using assms B.VV.ide_charSbC B.VV.arr_charSbC by auto

    interpretation Φ: natural_isomorphism
                        B.VV.comp vcomp HoUP_UP.map UPoH.map cmpUP
    proof
      fix fg
      assume fg: "B.VV.ide fg"
      have "arr (cmpUP fg)"
        using fg Φ.preserves_reflects_arr [of fg] by simp
      thus "iso (cmpUP fg)"
        using fg iso_char by simp
    qed

    lemma cmpUP_ide_simp:
    assumes "B.ide f" and "B.ide g" and "srcB f = trgB g"
    shows "cmpUP (f, g) = MkArr (f  g) f B g (f B g)"
      using assms B.VV.ide_charSbC B.VV.arr_charSbC by simp

    lemma cmpUP'_ide_simp:
    assumes "B.ide f" and "B.ide g" and "srcB f = trgB g"
    shows "inv (cmpUP (f, g)) = MkArr f B g (f  g) (f B g)"
      using assms cmpUP_ide_simp iso_char Φ.components_are_iso [of "(f, g)"]
            B.VV.ide_charSbC B.VV.arr_charSbC
      by simp

    interpretation UP: pseudofunctor
                         VB HB 𝖺B 𝗂B srcB trgB vcomp hcomp 𝖺 𝗂 src trg UP cmpUP
    proof
      fix f g h
      assume f: "B.ide f" and g: "B.ide g" and h: "B.ide h"
      and fg: "srcB f = trgB g" and gh: "srcB g = trgB h"
      show "UP 𝖺B[f, g, h]  cmpUP (f B g, h)  (cmpUP (f, g)  UP h) =
            cmpUP (f, g B h)  (UP f  cmpUP (g, h))  𝖺 (UP f) (UP g) (UP h)"
      proof -
        have "UP 𝖺B[f, g, h]  cmpUP (f B g, h)  (cmpUP (f, g)  UP h) =
              MkArr (f  g  h) f B g B h (f B g B h)"
        proof -
          have 1: "UP.hseqD (MkIde f) (MkIde g)"
            using f g fg hseq_char src_def trg_def arr_char by auto
          have 2: "UP.hseqD (MkArr (f  g) f B g (f B g)  MkIde (f  g))
                            (MkIde h)"
          proof -
            have "MkArr (f  g) f B g (f B g)  MkIde (f  g) =
                  MkArr (f  g) f B g (f B g)"
            proof -
              have "MkArr (f  g) f B g (f B g)  MkIde (f  g) =
                    MkArr (f  g) f B g (f B g)  MkArr (f  g) (f  g) (f B g)"
                using f g fg by simp
              also have "... = MkArr (f  g) f B g ((f B g) B (f B g))"
                using f g fg by (intro comp_MkArr arr_MkArr, auto)
              also have "... = MkArr (f  g) f B g (f B g)"
                using f g fg by simp
              finally show ?thesis by blast
            qed
            thus ?thesis
              using f g h fg gh arr_char src_def trg_def by auto
          qed
          have "UP 𝖺B[f, g, h] = MkArr (f B g) B h f B g B h 𝖺B[f, g, h]"
            using f g h fg gh UP_def B.HoHV_def B.HoVH_def B.VVV.arr_charSbC B.VV.arr_charSbC
                  B.VVV.dom_charSbC B.VVV.cod_charSbC
            by simp
          moreover have
            "cmpUP (f B g, h) = MkArr (f B g  h) (f B g) B h ((f B g) B h) 
                                  MkArr (f B g  h) (f B g  h) ((f B g) B h)"
            using f g h fg gh Φ.map_simp_ide Φ.map_def B.VV.arr_charSbC UP.FF_def B.VV.cod_simp
                  hcomp_def B.can_Ide_self
            by simp
          moreover have "cmpUP (f, g)  UP h =
                         MkArr (f  g  h) (f B g  h) (B.inv 𝖺B[f, g, h])"
          proof -
            have "MkArr (f  g) (f  g)
                        (B.can (f  g) (f  g) B (f B g) B B.can (f  g) (f  g)) =
                  MkArr (f  g) (f  g) (f B g)"
              using f g fg B.can_Ide_self B.comp_arr_dom B.comp_cod_arr by simp
            moreover have "MkArr (f  g) f B g (f B g) 
                             MkArr (f  g) (f  g) (f B g) =
                           MkArr (f  g) f B g (f B g)"
              by (metis (no_types, lifting) 2 B.ideD(1) E.eval.simps(2-3) cod_MkArr
                  comp_arr_ide f g ide_char' seq_char)
            moreover have "B.can ((f  g)  h) (f  g  h) = B.inv 𝖺B[f, g, h]"
              using f g h fg gh B.canI_associator_0 B.inverse_arrows_can by simp
            ultimately show ?thesis
              using 1 2 f g h fg gh Φ.map_def UP_def hcomp_def UP.FF_def
                    B.VV.arr_charSbC B.can_Ide_self B.comp_cod_arr B.VV.cod_simp
              by simp
          qed
          ultimately have "UP 𝖺B[f, g, h]  cmpUP (f B g, h)  (cmpUP (f, g)  UP h) =
                           MkArr (f B g) B h f B g B h 𝖺B[f, g, h] 
                             MkArr (f B g  h) (f B g) B h ((f B g) B h) 
                               MkArr (f B g  h) (f B g  h) ((f B g) B h) 
                                 MkArr (f  g  h) (f B g  h) (B.inv 𝖺B[f, g, h])"
            using comp_assoc by presburger
          also have "... = MkArr (f  g  h) f B g B h
                                 (𝖺B[f, g, h] B ((f B g) B h) B ((f B g) B h) B
                                   B.inv 𝖺B[f, g, h])"
          proof -
            have "Arr (MkArr (f  g  h) (f B g  h) (B.inv 𝖺B[f, g, h])) 
                     Arr (MkArr (f B g  h) (f B g  h) ((f B g) B h)) 
                     Arr (MkArr (f  g  h) (f B g  h)
                                (((f B g) B h) B B.inv 𝖺B[f, g, h])) 
                     Arr (MkArr (f B g  h) (f B g) B h ((f B g) B h)) 
                     Arr (MkArr (f  g  h) (f B g) B h
                          (((f B g) B h) B ((f B g) B h) B B.inv 𝖺B[f, g, h])) 
                     Arr (MkArr (f B g) B h f B g B h 𝖺B[f, g, h])"
              using f g h fg gh B.α.preserves_hom B.HoHV_def B.HoVH_def by auto
            thus ?thesis
              using f g h fg gh comp_def B.comp_arr_dom B.comp_cod_arr by simp
          qed
          also have "... = MkArr (f  g  h) f B g B h (f B g B h)"
            using B.comp_cod_arr B.comp_arr_inv'
            by (auto simp add: f fg g gh h)
          finally show ?thesis by simp
        qed
        also have "... = cmpUP (f, g B h)  (UP f  cmpUP (g, h))  𝖺 (UP f) (UP g) (UP h)"
        proof -
          have "cmpUP (f, g B h)  (UP f  cmpUP (g, h))  𝖺 (UP f) (UP g) (UP h) =
                cmpUP (f, g B h)  (MkIde f  cmpUP (g, h)) 
                (MkIde f  MkIde g  MkIde h)"
            using f g h fg gh VVV.arr_charSbC VV.arr_charSbC arr_char src_def trg_def UP_def 𝖺_def
            by auto
          also have "... = MkArr (f  g B h) f B g B h (f B g B h) 
                            MkArr (f  g B h) (f  g B h) (f B g B h) 
                             MkArr (f  g  h) (f  g B h) (f B g B h) 
                              MkArr (f  g  h) (f  g  h) (f B g B h)"
          proof -
            have "cmpUP (f, g B h) = MkArr (f  g B h) f B g B h (f B g B h) 
                                  MkArr (f  g B h) (f  g B h) (f B g B h)"
              using f g h fg gh Φ.map_simp_ide Φ.map_def UP.FF_def UP_def hcomp_def
                    B.VV.arr_charSbC B.can_Ide_self B.comp_arr_dom B.comp_cod_arr src_def trg_def
                    arr_char B.VV.cod_simp
              by auto
            moreover
            have "cmpUP (g, h) = MkArr (g  h) g B h (g B h)"
              using g h gh cmpUP_ide_simp by blast
            moreover have "MkIde f  MkArr (g  h) g B h (g B h) =
                           MkArr (f  g  h) (f  g B h) (f B g B h)"
              using f g h fg gh hcomp_def arr_char src_def trg_def B.can_Ide_self
                    B.comp_arr_dom B.comp_cod_arr
              by auto
            moreover
            have "MkIde f  MkIde g  MkIde h =
                  MkArr (f  g  h) (f  g  h) (f B g B h)"
            proof -
              have "«f : f B f»  «g : g B g»  «h : h B h»"
                using f g h by auto
              thus ?thesis
                using f g h fg gh hcomp_def arr_char src_def trg_def B.can_Ide_self
                      B.comp_arr_dom B.comp_cod_arr
                by auto
            qed
            ultimately show ?thesis
              using comp_assoc by auto
          qed
          also have "... = MkArr (f  g  h) f B g B h (f B g B h)"
          proof -
            have "Arr (MkArr (f  g  h) (f  g  h) (f B g B h)) 
                  Arr (MkArr (f  g  h) (f  g B h) (f B g B h)) 
                  Arr (MkArr (f  g B h) (f  g B h) (f B g B h)) 
                  Arr (MkArr (f  g B h) f B g B h (f B g B h))"
              using f g h fg gh by auto
            thus ?thesis
              using f g h fg gh comp_def by auto
          qed
          finally show ?thesis by simp
        qed
        finally show ?thesis by blast
      qed
    qed

    lemma UP_is_pseudofunctor:
    shows "pseudofunctor VB HB 𝖺B 𝗂B srcB trgB vcomp hcomp 𝖺 𝗂 src trg UP cmpUP" ..

    lemma UP_map0_obj [simp]:
    assumes "B.obj a"
    shows "UP.map0 a = UP0 a"
      using assms UP.map0_def by auto

    interpretation UP: full_functor VB vcomp UP
    proof
      fix μ f g
      assume f: "B.ide f" and g: "B.ide g"
      assume μ: "«μ : UP f  UP g»"
      show "ν. «ν : f B g»  UP ν = μ"
      proof -
        have 1: "«Map μ : f B g»"
          using f g μ UP_def arr_char in_hom_char by auto
        moreover have "UP (Map μ) = μ"
        proof -
          have "μ = MkArr (Dom μ) (Cod μ) (Map μ)"
            using μ MkArr_Map by auto
          also have "... = UP (Map μ)"
            using "1" B.arrI UP.as_nat_trans.preserves_hom UP_def μ in_hom_char by force
          finally show ?thesis by auto
        qed
        ultimately show ?thesis by blast
      qed
    qed

    interpretation UP: faithful_functor VB vcomp UP
      using arr_char UP_def
      by (unfold_locales, simp_all)

    interpretation UP: fully_faithful_functor VB vcomp UP ..

    lemma UP_is_fully_faithful_functor:
    shows "fully_faithful_functor VB vcomp UP"
      ..

    no_notation B.in_hom  ("«_ : _ B _»")   (* Inherited from functor, I think. *)

    lemma Map_reflects_hhom:
    assumes "B.obj a" and "B.obj b" and "ide g"
    and "«g : UP.map0 a  UP.map0 b»"
    shows "«Map g : a B b»"
    proof
      have 1: "B.ide (Map g)"
        using assms ide_char by blast
      show "B.arr (Map g)"
        using 1 by simp
      show "srcB (Map g) = a"
      proof -
        have "srcB (Map g) = Map (src g)"
          using assms src_def apply simp
          by (metis (no_types, lifting) E.eval_simps(2) E.Ide_implies_Arr arr_char ideE)
        also have "... = Map (UP.map0 a)"
          using assms by (metis (no_types, lifting) in_hhomE)
        also have "... = a"
          using assms UP.map0_def UP_def [of a] src_def by auto
        finally show ?thesis by simp
      qed
      show "trgB (Map g) = b"
      proof -
        have "trgB (Map g) = Map (trg g)"
          using assms trg_def apply simp
          by (metis (no_types, lifting) E.eval_simps(3) E.Ide_implies_Arr arr_char ideE)
        also have "... = Map (UP.map0 b)"
          using assms by (metis (no_types, lifting) in_hhomE)
        also have "... = b"
          using assms UP.map0_def UP_def [of b] src_def by auto
        finally show ?thesis by simp
      qed
    qed

    lemma eval_Dom_ide [simp]:
    assumes "ide g"
    shows "Dom g = Map g"
      using assms dom_char ideD by auto

    lemma Cod_ide:
    assumes "ide f"
    shows "Cod f = Dom f"
      using assms dom_char by auto

    lemma Map_preserves_objects:
    assumes "obj a"
    shows "B.obj (Map a)"
    proof -
      have "srcB (Map a) = Map (src a)"
        using assms src_def apply simp
        using E.eval_simps(2) E.Ide_implies_Arr arr_char ideE
        by (metis (no_types, lifting) objE)
      also have 1: "... = E.Src (Dom a)"
        using assms src_def by auto
      also have "... = Map a0"
        using assms B.src.is_extensional 1 obj_simps(2) by force
      also have "... = Map a"
        using assms by auto
      finally have "srcB (Map a) = Map a" by simp
      moreover have "B.arr (Map a)"
        using assms B.ideD arr_char by auto
      ultimately show ?thesis
        using B.obj_def by simp
    qed

    interpretation UP: equivalence_pseudofunctor
                         VB HB 𝖺B 𝗂B srcB trgB vcomp hcomp 𝖺 𝗂 src trg UP cmpUP
    proof
      (* UP is full, hence locally full. *)
      show "f f' ν.  B.ide f; B.ide f'; srcB f = srcB f'; trgB f = trgB f';
                       «ν : UP f  UP f'»   μ. «μ : f B f'»  UP μ = ν"
        using UP.is_full by simp
      (* UP is biessentially surjective on objects. *)
      show "b. obj b  a. B.obj a  equivalent_objects (UP.map0 a) b"
      proof -
        fix b
        assume b: "obj b"
        have 1: "B.obj (Map b)"
          using b Map_preserves_objects by simp
        have 3: "UP.map0 (Map b) = MkArr Map b0 Map b0 (Map b)"
          using b 1 UP.map0_def [of "Map b"] UP_def src_def arr_char by auto
        have 4: "b = MkArr (Dom b) (Dom b) (Map b)"
          using b objE eval_Dom_ide
          by (metis (no_types, lifting) dom_char ideD(2) obj_def)
        let  = "MkArr Map b0 (Dom b) (Map b)"
        have φ: "arr "
        proof -
          have 2: "E.Obj (Dom b)"
            using b obj_char by blast
          have "E.Nml Map b0  E.Ide Map b0"
            using 1 by auto
          moreover have "E.Nml (Dom b)  E.Ide (Dom b)"
            using b arr_char [of b] by auto
          moreover have "E.Src Map b0 = E.Src (Dom b)"
            using b 1 2
            apply (cases "Dom b")
                     apply simp_all
            by fastforce
          moreover have "E.Trg Map b0 = E.Trg (Dom b)"
            using b 1 2
            apply (cases "Dom b")
                     apply simp_all
            by fastforce
          moreover have "«Map b : Map b0 B Dom b»"
            using b 1 by (elim objE, auto)
          ultimately show ?thesis
            using arr_char E.Nml Map b0  E.Ide Map b0 by auto
        qed
        hence "iso "
          using 1 iso_char by auto
        moreover have "dom  = UP.map0 (Map b)"
          using φ dom_char b 1 3 B.objE UP.map0_def UP_def src_def by auto
        moreover have "cod  = b"
          using φ cod_char b 4 1 by auto
        ultimately have "isomorphic (UP.map0 (Map b)) b"
          using φ 3 4 isomorphic_def by blast
        moreover have 5: "obj (UP.map0 (Map b))"
          using 1 UP.map0_simps(2) by simp
        ultimately have 6: "UP.map0 (Map b) = b"
          using b isomorphic_objects_are_equal by simp
        have "equivalent_objects (UP.map0 (Map b)) b"
          using b 6 equivalent_objects_reflexive [of b] by simp
        thus "a. B.obj a  equivalent_objects (UP.map0 a) b"
          using 1 6 by auto
      qed
      (* UP is locally essentially surjective. *)
      show "a b g.  B.obj a; B.obj b; «g : UP.map0 a  UP.map0 b»; ide g  
                        f. «f : a B b»  B.ide f  isomorphic (UP f) g"
      proof -
        fix a b g
        assume a: "B.obj a" and b: "B.obj b"
        assume g_in_hhom: "«g : UP.map0 a  UP.map0 b»"
        assume ide_g: "ide g"
        have 1: "B.ide (Map g)"
          using ide_g ide_char by blast
        have "arr (UP a)"
          using a by auto
        have "arr (UP b)"
          using b by auto
        have Map_g_eq: "Map g = Dom g"
          using ide_g by simp
        have Map_g_in_hhom: "«Map g : a B b»"
          using a b ide_g g_in_hhom Map_reflects_hhom by simp

        let  = "MkArr Map g (Dom g) (Map g)"
        have φ: "arr "
        proof -
          have "«Map  : Dom  B Cod »"
            using 1 Map_g_eq by auto
          moreover have "E.Ide Map g  E.Nml Map g"
            using 1 by simp
          moreover have "E.Ide (Dom g)  E.Nml (Dom g)"
            using ide_g arr_char ide_char by blast
          moreover have "E.Src Map g = E.Src (Dom g)"
            using ide_g g_in_hhom src_def Map_g_in_hhom
            by (metis (no_types, lifting) B.ideD(2) B.in_hhom_def B.objE B.obj_def'
                Dom.simps(1) E.Src.simps(2) UP.map0_def arr (UP a) a in_hhomE UP_def)
          moreover have "E.Trg Map g = E.Trg (Dom g)"
          proof -
            have "E.Trg Map g = b0"
              using Map_g_in_hhom by auto
            also have "... = E.Trg (Dom g)"
            proof -
              have "E.Trg (Dom g) = Dom (trg g)"
                using ide_g trg_def by simp
              also have "... = Dom (UP.map0 b)"
                using g_in_hhom by auto
              also have "... = b0"
                using b arr (UP b) UP.map0_def src_def UP_def B.objE by auto
              finally show ?thesis by simp
            qed
            finally show ?thesis by simp
          qed
          ultimately show ?thesis
            using arr_char by simp
        qed
        have "« : UP (Map g)  g»"
          by (simp add: "1" φ ide_g in_hom_char)
        moreover have "iso "
          using φ 1 iso_char by simp
        ultimately have "isomorphic (UP (Map g)) g"
          using isomorphic_def by auto
        thus "f. «f : a B b»  B.ide f  isomorphic (UP f) g"
          using 1 Map_g_in_hhom by auto
      qed
    qed

    theorem UP_is_equivalence_pseudofunctor:
    shows "equivalence_pseudofunctor VB HB 𝖺B 𝗂B srcB trgB vcomp hcomp 𝖺 𝗂 src trg
             UP cmpUP"
      ..

    text ‹
      Next, we work out the details of the equivalence pseudofunctor DN› in the
      converse direction.
    ›

    definition DN
    where "DN μ  if arr μ then Map μ else B.null"

    lemma DN_in_hom [intro]:
    assumes "arr μ"
    shows "«DN μ : DN (src μ) B DN (trg μ)»"
    and "«DN μ : DN (dom μ) B DN (cod μ)»"
      using assms DN_def arr_char [of μ] B.vconn_implies_hpar(1-2) E.eval_in_hom(1)
            B.in_hhom_def
      by auto

    lemma DN_simps [simp]:
    assumes "arr μ"
    shows "B.arr (DN μ)"
    and "srcB (DN μ) = DN (src μ)" and "trgB (DN μ) = DN (trg μ)"
    and "B.dom (DN μ) = DN (dom μ)" and "B.cod (DN μ) = DN (cod μ)"
      using assms DN_in_hom by auto

    interpretation "functor" vcomp VB DN
      using DN_def seqE Map_comp seq_char
      by unfold_locales auto

    interpretation DN: weak_arrow_of_homs vcomp src trg VB srcB trgB DN
    proof
      fix μ
      assume μ: "arr μ"
      show "B.isomorphic (DN (src μ)) (srcB (DN μ))"
      proof -
        have "DN (src μ) = srcB (DN μ)"
          using B.src.is_extensional DN_def DN_simps(2) by auto
        moreover have "B.ide (DN (src μ))"
          using μ by simp
        ultimately show ?thesis
          using μ B.isomorphic_reflexive by auto
      qed
      show "B.isomorphic (DN (trg μ)) (trgB (DN μ))"
      proof -
        have "DN (trg μ) = trgB (DN μ)"
          using B.isomorphic (DN (src μ)) (srcB (DN μ)) by fastforce
        moreover have "B.ide (DN (trg μ))"
          using μ by simp
        ultimately show ?thesis
          using B.isomorphic_reflexive by auto
      qed
    qed

    interpretation "functor" VV.comp B.VV.comp DN.FF
      using DN.functor_FF by auto
    interpretation HoDN_DN: composite_functor VV.comp B.VV.comp VB
                      DN.FF λμν. HB (fst μν) (snd μν) ..
    interpretation DNoH: composite_functor VV.comp vcomp VB
                      λμν. fst μν  snd μν DN ..

    abbreviation Ψo
    where "Ψo fg  B.can (Dom (fst fg)  Dom (snd fg)) (Dom (fst fg)  Dom (snd fg))"

    abbreviation Ψo'
    where "Ψo' fg  B.can (Dom (fst fg)  Dom (snd fg)) (Dom (fst fg)  Dom (snd fg))"

    lemma Ψo_in_hom:
    assumes "VV.ide fg"
    shows "«Ψo fg : Map (fst fg) B Map (snd fg) B Dom (fst fg)  Dom (snd fg)»"
    and "«Ψo' fg : Dom (fst fg)  Dom (snd fg) B Map (fst fg) B Map (snd fg)»"
    and "B.inverse_arrows (Ψo fg) (Ψo' fg)"
    proof -
      have 1: "E.Ide (Dom (fst fg)  Dom (snd fg))"
        unfolding E.Ide.simps(3)
        apply (intro conjI)
        using assms VV.ide_char VV.arr_charSbC arr_char
          apply simp
        using VV.arr_charSbC VV.ideD(1) assms
         apply blast
        by (metis (no_types, lifting) VV.arrE VV.ideD(1) assms src_simps(1) trg_simps(1))
      have 2: "E.Ide (Dom (fst fg)  Dom (snd fg))"
        using 1
        by (meson E.Ide.simps(3) E.Ide_HcompNml VV.arr_charSbC VV.ideD(1) arr_char assms)
      have 3: "Dom (fst fg)  Dom (snd fg) = Dom (fst fg)  Dom (snd fg)"
        by (metis (no_types, lifting) E.Ide.simps(3) E.Nml_HcompNml(1) E.Nmlize.simps(3)
            E.Nmlize_Nml VV.arr_charSbC VV.ideD(1) arr_char assms 1)
      have 4: "Dom (fst fg)  Dom (snd fg) = Map (fst fg) B Map (snd fg)"
        using assms VV.ide_charSbC VV.arr_charSbC arr_char by simp
      show "«Ψo fg : Map (fst fg) B Map (snd fg) B Dom (fst fg)  Dom (snd fg)»"
        using 1 2 3 4 by auto
      show "«Ψo' fg : Dom (fst fg)  Dom (snd fg) B Map (fst fg) B Map (snd fg)»"
        using 1 2 3 4 by auto
      show "B.inverse_arrows (Ψo fg) (Ψo' fg)"
        using 1 2 3 B.inverse_arrows_can by blast
    qed

    interpretation Ψ: transformation_by_components
                         VV.comp VB HoDN_DN.map DNoH.map Ψo
    proof
      fix fg
      assume fg: "VV.ide fg"
      have 1: "Dom (fst fg)  Dom (snd fg) = Map (fst fg) B Map (snd fg)"
        using fg VV.ide_charSbC VV.arr_charSbC arr_char by simp
      show "«Ψo fg : HoDN_DN.map fg B DNoH.map fg»"
      proof
        show "B.arr (Ψo fg)"
          using fg Ψo_in_hom by blast
        show "B.dom (Ψo fg) = HoDN_DN.map fg"
        proof -
          have "B.dom (Ψo fg) = Map (fst fg) B Map (snd fg)"
            using fg Ψo_in_hom by blast
          also have "... = HoDN_DN.map fg"
            using fg DN.FF_def DN_def VV.arr_charSbC src_def trg_def VV.ide_charSbC by auto
          finally show ?thesis by simp
        qed
        show "B.cod (Ψo fg) = DNoH.map fg"
        proof -
          have "B.cod (Ψo fg) = Dom (fst fg)  Dom (snd fg)"
            using fg Ψo_in_hom by blast
          also have "... = DNoH.map fg"
          proof -
            have "DNoH.map fg = 
                  B.can (Cod (fst fg)  Cod (snd fg)) (Cod (fst fg)  Cod (snd fg)) B
                    (Map (fst fg) B Map (snd fg)) B
                      B.can (Dom (fst fg)  Dom (snd fg)) (Dom (fst fg)  Dom (snd fg))"
              using fg DN_def Map_hcomp VV.arr_charSbC
              apply simp
              using VV.ideD(1) by blast
            also have "... =
                       B.can (Cod (fst fg)  Cod (snd fg)) (Cod (fst fg)  Cod (snd fg)) B
                         B.can (Dom (fst fg)  Dom (snd fg)) (Dom (fst fg)  Dom (snd fg))"
            proof -
              have "(Map (fst fg) B Map (snd fg)) B
                      B.can (Dom (fst fg)  Dom (snd fg)) (Dom (fst fg)  Dom (snd fg)) =
                    B.can (Dom (fst fg)  Dom (snd fg)) (Dom (fst fg)  Dom (snd fg))"
                using fg 1 Ψo_in_hom B.comp_cod_arr by blast
              thus ?thesis by simp
            qed
            also have "... = Dom (fst fg)  Dom (snd fg)"
            proof -
              have "B.can (Cod (fst fg)  Cod (snd fg)) (Cod (fst fg)  Cod (snd fg)) = Ψo fg"
                using fg VV.ide_charSbC Cod_ide by simp
              thus ?thesis
                using fg 1 Ψo_in_hom [of fg] B.comp_arr_inv' by fastforce
            qed
            finally show ?thesis by simp
          qed
          finally show ?thesis by blast
        qed
      qed
      next
      show "f. VV.arr f 
                   Ψo (VV.cod f) B HoDN_DN.map f = DNoH.map f B Ψo (VV.dom f)"
      proof -
        fix μν
        assume μν: "VV.arr μν"
        show "Ψo (VV.cod μν) B HoDN_DN.map μν = DNoH.map μν B Ψo (VV.dom μν)"
        proof -
          have 1: "E.Ide (Dom (fst μν)  Dom (snd μν))"
            unfolding E.Ide.simps(3)
            by (metis (no_types, lifting) VV.arrE μν arrE src_simps(2) trg_simps(2))
          have 2: "E.Ide (Dom (fst μν)  Dom (snd μν))"
            using 1
            by (meson E.Ide.simps(3) E.Ide_HcompNml VV.arr_charSbC VV.ideD(1) arr_char μν)
          have 3: "Dom (fst μν)  Dom (snd μν) = Dom (fst μν)  Dom (snd μν)"
            by (metis (no_types, lifting) E.Ide.simps(3) E.Nml_HcompNml(1) E.Nmlize.simps(3)
               E.Nmlize_Nml VV.arr_charSbC arr_char μν 1)
          have 4: "E.Ide (Cod (fst μν)  Cod (snd μν))"
            unfolding E.Ide.simps(3)
            by (metis (no_types, lifting) "1" E.Ide.simps(3) VV.arrE μν arr_char)
          have 5: "E.Ide (Cod (fst μν)  Cod (snd μν))"
            using 4
            by (meson E.Ide.simps(3) E.Ide_HcompNml VV.arr_charSbC VV.ideD(1) arr_char μν)
          have 6: "Cod (fst μν)  Cod (snd μν) = Cod (fst μν)  Cod (snd μν)"
            by (metis (no_types, lifting) E.Ide.simps(3) E.Nml_HcompNml(1) E.Nmlize.simps(3)
               E.Nmlize_Nml VV.arr_charSbC arr_char μν 1)
          have A: "«Ψo' μν : Dom (fst μν)  Dom (snd μν)
                                 B Dom (fst μν)  Dom (snd μν)»"
            using 1 2 3 by auto
          have B: "«Map (fst μν) B Map (snd μν) :
                     Dom (fst μν)  Dom (snd μν) B Cod (fst μν)  Cod (snd μν)»"
            using μν VV.arr_charSbC arr_char src_def trg_def E.Nml_implies_Arr E.eval_simps'(2-3)
            by auto
          have C: "«B.can (Cod (fst μν)  Cod (snd μν)) (Cod (fst μν)  Cod (snd μν)) :
                     Cod (fst μν)  Cod (snd μν) B Cod (fst μν)  Cod (snd μν)»"
            using 4 5 6 by auto
          have "Ψo (VV.cod μν) B HoDN_DN.map μν =
                B.can (Cod (fst μν)  Cod (snd μν)) (Cod (fst μν)  Cod (snd μν)) B
                  (Map (fst μν) B Map (snd μν))"
            using μν VV.arr_charSbC VV.cod_charSbC arr_char src_def trg_def cod_char DN.FF_def DN_def
            by auto
          also have "... = B.can (Cod (fst μν)  Cod (snd μν))
                                 (Cod (fst μν)  Cod (snd μν)) B
                             (Map (fst μν) B Map (snd μν)) B Ψo' μν B Ψo μν"
            using B μν VV.arr_charSbC arr_char src_def trg_def
                  E.Ide_HcompNml E.Nml_HcompNml(1) B.can_Ide_self B.comp_arr_dom
            by auto
          also have "... = DNoH.map μν B Ψo (VV.dom μν)"
          proof -
            have "DNoH.map μν B Ψo (VV.dom μν) =
                  B.can (Cod (fst μν)  Cod (snd μν)) (Cod (fst μν)  Cod (snd μν)) B
                    (Map (fst μν) B Map (snd μν)) B Ψo' μν B Ψo (VV.dom μν)"
              using μν DN_def VV.arr_charSbC B.comp_assoc by simp
            moreover have "Ψo (VV.dom μν) = Ψo μν"
              using μν VV.dom_charSbC VV.arr_charSbC by auto
            ultimately show ?thesis
              using B.comp_assoc by simp
          qed
          finally show ?thesis by blast
        qed
      qed
    qed

    abbreviation cmpDN
    where "cmpDN  Ψ.map"

    interpretation Ψ: natural_isomorphism VV.comp VB HoDN_DN.map DNoH.map cmpDN
      using Ψo_in_hom B.iso_def Ψ.map_simp_ide
      apply unfold_locales
        apply auto
      by blast

    no_notation B.in_hom  ("«_ : _ B _»")

    lemma cmpDN_in_hom [intro]:
    assumes "arr (fst μν)" and "arr (snd μν)" and "src (fst μν) = trg (snd μν)"
    shows "«cmpDN μν : DN (src (snd μν)) B DN (trg (fst μν))»"
    and "«cmpDN μν : DN (dom (fst μν)) B DN (dom (snd μν))
                    B DN (cod (fst μν)  cod (snd μν))»"
    proof -
      have 1: "VV.arr μν"
        using assms VV.arr_charSbC by simp
      show 2: "«cmpDN μν : DN (dom (fst μν)) B DN (dom (snd μν))
                          B DN (cod (fst μν)  cod (snd μν))»"
      proof -
        have "HoDN_DN.map (VV.dom μν) = DN (dom (fst μν)) B DN (dom (snd μν))"
          using assms 1 DN.FF_def VV.dom_simp by auto
        moreover have "DNoH.map (VV.cod μν) = DN (cod (fst μν)  cod (snd μν))"
          using assms 1 VV.cod_simp by simp
        ultimately show ?thesis
          using assms 1 Ψ.preserves_hom by auto
      qed
      show "«cmpDN μν : DN (src (snd μν)) B DN (trg (fst μν))»"
        using assms 2 B.src_dom [of "cmpDN μν"] B.trg_dom [of "cmpDN μν"]
        by (elim B.in_homE, intro B.in_hhomI) auto
    qed

    lemma cmpDN_simps [simp]:
    assumes "arr (fst μν)" and "arr (snd μν)" and "src (fst μν) = trg (snd μν)"
    shows "B.arr (cmpDN μν)"
    and "srcB (cmpDN μν) = DN (src (snd μν))" and "trgB (cmpDN μν) = DN (trg (fst μν))"
    and "B.dom (cmpDN μν) = DN (dom (fst μν)) B DN (dom (snd μν))"
    and "B.cod (cmpDN μν) = DN (cod (fst μν)  cod (snd μν))"
    proof
      show "VV.arr μν"
        using assms by blast
      have 1: "«cmpDN μν : DN (src (snd μν)) B DN (trg (fst μν))»"
        using assms by blast
      show "srcB (cmpDN μν) = DN (src (snd μν))"
        using 1 by fast
      show "trgB (cmpDN μν) = DN (trg (fst μν))"
        using 1 by fast
      have 2: "«cmpDN μν : DN (dom (fst μν)) B DN (dom (snd μν))
                          B DN (cod (fst μν)  cod (snd μν))»"
        using assms by blast
      show "B.dom (cmpDN μν) = DN (dom (fst μν)) B DN (dom (snd μν))"
        using 2 by fast
      show "B.cod (cmpDN μν) = DN (cod (fst μν)  cod (snd μν))"
        using 2 by fast
    qed

    interpretation DN: pseudofunctor vcomp hcomp 𝖺 𝗂 src trg VB HB 𝖺B 𝗂B srcB trgB
                         DN cmpDN
    proof
      show "f g h.  ide f; ide g; ide h; src f = trg g; src g = trg h  
                       DN (𝖺 f g h) B cmpDN (f  g, h) B (cmpDN (f, g) B DN h) =
                       cmpDN (f, g  h) B (DN f B cmpDN (g, h)) B 𝖺B[DN f, DN g, DN h]"
      proof -
        fix f g h
        assume f: "ide f" and g: "ide g" and h: "ide h"
        and fg: "src f = trg g" and gh: "src g = trg h"
        show "DN (𝖺 f g h) B cmpDN (f  g, h) B (cmpDN (f, g) B DN h) =
              cmpDN (f, g  h) B (DN f B cmpDN (g, h)) B 𝖺B[DN f, DN g, DN h]"
        proof -
          have 1: "E.Trg (Dom g) = E.Trg (Dom g  Dom h) 
                   E.Trg (Dom g) = E.Trg (Dom g  Dom h)"
            using f g h fg gh arr_char src_def trg_def E.Trg_HcompNml
            by (metis (no_types, lifting) ideD(1) src_simps(2) trg_simps(2))
          have 2: "arr (MkArr (Dom f  Dom g  Dom h) (Cod f  Cod g  Cod h)
                       (B.can (Cod f  Cod g  Cod h) (Cod f  Cod g  Cod h) B
                          (Map f B B.can (Cod g  Cod h) (Cod g  Cod h) B
                          (Map g B Map h) B B.can (Dom g  Dom h) (Dom g  Dom h)) B
                          B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h)))"
          proof -
            have "«B.can (Cod f  Cod g  Cod h) (Cod f  Cod g  Cod h) B
                     (Map f B
                        B.can (Cod g  Cod h) (Cod g  Cod h) B
                          (Map g B Map h) B B.can (Dom g  Dom h) (Dom g  Dom h)) B
                          B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) :
                     EVAL (Dom f  Dom g  Dom h)
                       B EVAL (Cod f  Cod g  Cod h)»"
            proof (intro B.comp_in_homI)
              show 2: "«B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) :
                          EVAL (Dom f  Dom g  Dom h) B
                            EVAL (Dom f  Dom g  Dom h)»"
                using f g h fg gh 1
                apply (intro B.can_in_hom)
                  apply (metis (no_types, lifting) E.Ide_HcompNml E.Nml_HcompNml(1)
                    arr_char ideD(1) src_simps(1) trg_simps(1))
                 apply (metis (no_types, lifting) E.Ide.simps(3) E.Ide_HcompNml ideD(1)
                    arr_char src_simps(1) trg_simps(1))
                by (metis (no_types, lifting) E.Nml_HcompNml(1) E.Nmlize.simps(3)
                    E.Nmlize_Nml ideD(1) arr_char src_simps(1) trg_simps(1))
              show "«B.can (Cod f  Cod g  Cod h) (Cod f  Cod g  Cod h) :
                       EVAL (Cod f  Cod g  Cod h) B
                         EVAL (Cod f  Cod g  Cod h)»"
              proof -
                have "E.Ide (Cod f  Cod g  Cod h)"
                  using f g h fg gh 1 Cod_ide E.Ide_HcompNml arr_char
                  apply simp
                  by (metis (no_types, lifting) ideD(1) src_simps(1) trg_simps(1))
                moreover have "E.Ide (Cod f  Cod g  Cod h)"
                  using f g h fg gh
                  by (metis (no_types, lifting) E.Ide.simps(3) E.Ide_HcompNml E.Nml_HcompNml(1)
                      arr_char calculation ideD(1) src_simps(1) trg_simps(1))
                moreover have "E.Nmlize (Cod f  Cod g  Cod h) =
                               E.Nmlize (Cod f  Cod g  Cod h)"
                  using f g h fg gh
                  by (metis (no_types, lifting) E.Ide.simps(3) E.Nml_HcompNml(1) E.Nmlize.simps(3)
                      E.Nmlize_Nml arr_char calculation(1) ideD(1) src_simps(1) trg_simps(1))
                ultimately show ?thesis
                  using B.can_in_hom [of "Cod f  Cod g  Cod h" "Cod f  Cod g  Cod h"]
                  by blast
              qed
              show "«Map f B B.can (Cod g  Cod h) (Cod g  Cod h) B
                     (Map g B Map h) B B.can (Dom g  Dom h) (Dom g  Dom h) :
                       EVAL (Dom f  Dom g  Dom h) B EVAL (Cod f  Cod g  Cod h)»"
                using f g h fg gh B.can_in_hom
                apply simp
              proof (intro B.hcomp_in_vhom B.comp_in_homI)
                show 1: "«B.can (Dom g  Dom h) (Dom g  Dom h) :
                            EVAL (Dom g  Dom h) B EVAL (Dom g  Dom h)»"
                  using g h gh B.can_in_hom
                  by (metis (no_types, lifting) E.Ide.simps(3) E.Ide_HcompNml E.Nml_HcompNml(1)
                      E.Nmlize.simps(3) E.Nmlize_Nml arr_char ideD(1) src_simps(1) trg_simps(1))
                show "«B.can (Cod g  Cod h) (Cod g  Cod h) :
                         EVAL (Cod g  Cod h) B EVAL (Cod g  Cod h)»"
                  using g h gh B.can_in_hom
                  by (metis (no_types, lifting) Cod_ide E.Ide.simps(3) E.Ide_HcompNml
                      E.Nml_HcompNml(1) E.Nmlize.simps(3) E.Nmlize_Nml arr_char ideD(1)
                      src_simps(2) trg_simps(2))
                show "«Map g B Map h : EVAL (Dom g  Dom h) B EVAL (Cod g  Cod h)»"
                proof
                  show 2: "B.hseq (Map g) (Map h)"
                    using g h gh
                    by (metis (no_types, lifting) B.null_is_zero(1-2) B.hseq_char'
                        B.ideD(1) Map_hcomp ideE ide_hcomp)
                  show "B.dom (Map g B Map h) = EVAL (Dom g  Dom h)"
                    using g h gh 2 by fastforce
                  show "B.cod (Map g B Map h) = EVAL (Cod g  Cod h)"
                    using g h gh 2 by fastforce
                qed
                show "«Map f : Map f B EVAL (Cod f)»"
                  using f arr_char Cod_ide by auto
                show "srcB (Map f) = trgB Dom g  Dom h"
                  using f g h fg gh 1 2 src_def trg_def B.arrI B.hseqE B.not_arr_null
                        B.trg.is_extensional B.trg.preserves_hom B.vconn_implies_hpar(2)
                        B.vconn_implies_hpar(4) E.eval.simps(3)
                  by (metis (no_types, lifting) Map_ide(1))
              qed
            qed
            thus ?thesis
              using f g h fg gh arr_char src_def trg_def E.Nml_HcompNml E.Ide_HcompNml
                    ideD(1)
              apply (intro arr_MkArr) by auto
          qed
          have 3: "E.Ide (Dom g  Dom h)"
            using g h gh ide_char arr_char src_def trg_def E.Ide_HcompNml Cod_ide
            by (metis (no_types, lifting) ideD(1) src_simps(2) trg_simps(2))
          have 4: "E.Ide (Dom g  Dom h)"
            by (metis (no_types, lifting) E.Ide.simps(3) arrE g gh h ideE src_simps(1) trg_simps(1))
          have 5: "E.Nmlize (Dom g  Dom h) = E.Nmlize (Dom g  Dom h)"
            using g h gh ide_char arr_char src_def trg_def E.Nml_HcompNml
            by (metis (no_types, lifting) 4 E.Ide.simps(3) E.Nmlize.simps(3) E.Nmlize_Nml
                ideD(1))
          have 6: "E.Ide (Dom f  Dom g  Dom h)"
            using f g h fg gh arr_char src_def trg_def
            by (metis (no_types, lifting) 1 E.Nml_HcompNml(1) E.Ide_HcompNml ideD(1)
                src_simps(2) trg_simps(2))
          have 7: "E.Ide (Dom f  Dom g  Dom h)"
            using f g h fg gh arr_char src_def trg_def
            by (metis (no_types, lifting) 1 3 E.Ide.simps(3) ideD(1) src_simps(2) trg_simps(2))
          have 8: "E.Nmlize (Dom f  Dom g  Dom h) =
                   E.Nmlize (Dom f  Dom g  Dom h)"
            using f g h fg gh arr_char src_def trg_def
                  7 E.Nml_HcompNml(1) ideD(1)
            by auto
          have "DN (𝖺 f g h) B cmpDN (f  g, h) B (cmpDN (f, g) B DN h) =
                B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h)"
          proof -
            have 9: "VVV.arr (f, g, h)"
              using f g h fg gh VVV.arr_charSbC VV.arr_charSbC arr_char ideD by simp
            have 10: "VV.ide (f, g)"
              using f g fg VV.ide_charSbC by auto
            have 11: "VV.ide (hcomp f g, h)"
              using f g h fg gh VV.ide_charSbC VV.arr_charSbC by simp
            have 12: "arr (MkArr (Dom g  Dom h) (Cod g  Cod h)
                                (B.can (Cod g  Cod h) (Cod g  Cod h) B
                                  (Map g B Map h) B
                                  B.can (Dom g  Dom h) (Dom g  Dom h)))"
            proof (intro arr_MkArr)
              show "Dom g  Dom h  IDE"
                using g h gh
                by (metis (no_types, lifting) 3 E.Nml_HcompNml(1) arr_char ideD(1)
                    mem_Collect_eq src_simps(2) trg_simps(2))
              show "Cod g  Cod h  IDE"
                using g h gh Cod_ide Dom g  Dom h  IDE by auto
              show "B.can (Cod g  Cod h) (Cod g  Cod h) B
                      (Map g B Map h) B
                      B.can (Dom g  Dom h) (Dom g  Dom h)
                     HOM (Dom g  Dom h) (Cod g  Cod h)"
              proof
                show "E.Src (Dom g  Dom h) = E.Src (Cod g  Cod h) 
                      E.Trg (Dom g  Dom h) = E.Trg (Cod g  Cod h) 
                      «B.can (Cod g  Cod h) (Cod g  Cod h) B
                         (Map g B Map h) B B.can (Dom g  Dom h) (Dom g  Dom h) :
                         Dom g  Dom h B Cod g  Cod h»"
                proof (intro conjI)
                  show "E.Src (Dom g  Dom h) = E.Src (Cod g  Cod h)"
                    using g h gh Cod_ide by simp
                  show "E.Trg (Dom g  Dom h) = E.Trg (Cod g  Cod h)"
                    using g h gh Cod_ide by simp
                  show "«B.can (Cod g  Cod h) (Cod g  Cod h) B
                           (Map g B Map h) B B.can (Dom g  Dom h) (Dom g  Dom h) :
                           Dom g  Dom h B Cod g  Cod h»"
                  proof (intro B.comp_in_homI)
                    show "«B.can (Dom g  Dom h) (Dom g  Dom h) :
                             Dom g  Dom h B Dom g  Dom h»"
                      using 3 4 5 by blast
                    show "«Map g B Map h : Dom g  Dom h B Cod g  Cod h»"
                      using g h gh
                      by (metis (no_types, lifting) 4 B.ide_in_hom(2) Cod_ide E.eval.simps(3)
                          E.ide_eval_Ide Map_ide(2))
                    show "«B.can (Cod g  Cod h) (Cod g  Cod h) :
                            Cod g  Cod h B Cod g  Cod h»"
                      using 3 4 5 Cod_ide g h by auto
                  qed
                qed
              qed
            qed
            have "DN (𝖺 f g h) = Dom f  Dom g  Dom h"
            proof -
              have "DN (𝖺 f g h) =
                    (B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) B
                      ((Map f B B.can (Dom g  Dom h) (Dom g  Dom h) B
                         (Map g B Map h) B B.can (Dom g  Dom h) (Dom g  Dom h))) B
                      B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h))"
                using f g h fg gh 1 2 9 12 DN_def 𝖺_def Cod_ide by simp
              also have
                "... = B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) B
                         (Map f B Dom g  Dom h) B
                           B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h)"
              proof -
                have "«B.can (Dom g  Dom h) (Dom g  Dom h) :
                                    Dom g  Dom h B Map g B Map h»"
                  using g h 3 4 5 B.can_in_hom [of "Dom g  Dom h" "Dom g  Dom h"]
                  by simp
                hence "Map f B B.can (Dom g  Dom h) (Dom g  Dom h) B
                                 (Map g B Map h) B B.can (Dom g  Dom h) (Dom g  Dom h) =
                       Map f B B.can (Dom g  Dom h) (Dom g  Dom h) B
                                 B.can (Dom g  Dom h) (Dom g  Dom h)"
                  using B.comp_cod_arr by auto
                also have "... = Map f B Dom g  Dom h"
                  using f g h fg gh 3 4 5 B.can_Ide_self by auto
                finally have "Map f B B.can (Dom g  Dom h) (Dom g  Dom h) B
                                 (Map g B Map h) B B.can (Dom g  Dom h) (Dom g  Dom h) =
                              Map f B Dom g  Dom h"
                  by simp
                thus ?thesis by simp
              qed
              also have
                "... = B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) B
                         B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h)"
              proof -
                have "«B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) :
                               Dom f  Dom g  Dom h B Map f B Dom g  Dom h»"
                  using f g h 6 7 8
                        B.can_in_hom [of "Dom f  Dom g  Dom h" "Dom f  Dom g  Dom h"]
                  by simp
                hence "(Map f B Dom g  Dom h) B
                         B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) =
                       B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h)"
                  using B.comp_cod_arr by auto
                thus ?thesis by simp
              qed
              also have
                "... = B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h)"
                using f g h fg gh 6 7 8 by auto
              also have "... = Dom f  Dom g  Dom h"
                using f g h fg gh 6 B.can_Ide_self by blast
              finally show ?thesis by simp
            qed
            have "DN (𝖺 f g h) B cmpDN (f  g, h) B (cmpDN (f, g) B DN h) =
                  B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h) B
                  B.can ((Dom f  Dom g)  Dom h) ((Dom f  Dom g)  Dom h) B
                    (B.can (Dom f  Dom g) (Dom f  Dom g) B Map h)"
            proof -
              have "DN (𝖺 f g h) =
                    B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h)"
                using f g h fg gh DN_def 1 4 6 7 B.can_Ide_self E.HcompNml_assoc
                      E.Ide.simps(3) DN (𝖺 f g h) = Dom f  Dom g  Dom h ide_char
                by (metis (no_types, lifting) arr_char ideD(1))
              thus ?thesis
                using f g h fg gh 10 11 DN_def Ψ.map_simp_ide by simp
            qed
            also have
              "... = (B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h) B
                       B.can ((Dom f  Dom g)  Dom h) ((Dom f  Dom g)  Dom h)) B
                        (B.can (Dom f  Dom g) (Dom f  Dom g) B Map h)"
              using B.comp_assoc by simp
            also have
              "... = B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h) B
                       B.can ((Dom f  Dom g)  Dom h) ((Dom f  Dom g)  Dom h)"
            proof -
              have "B.can (Dom f  Dom g) (Dom f  Dom g) B Map h =
                    B.can ((Dom f  Dom g)  Dom h) ((Dom f  Dom g)  Dom h)"
              proof -
                have "B.can (Dom f  Dom g) (Dom f  Dom g) B Map h =
                      B.can (Dom f  Dom g) (Dom f  Dom g) B B.can (Dom h) (Dom h)"
                  using h B.can_Ide_self by fastforce
                also have "... = B.can ((Dom f  Dom g)  Dom h) ((Dom f  Dom g)  Dom h)"
                  using f g h 1 4 7 arr_char E.Nml_HcompNml(1) E.Src_HcompNml
                        B.hcomp_can [of "Dom f  Dom g" "Dom f  Dom g" "Dom h" "Dom h"]
                  by (metis (no_types, lifting) E.Nmlize.simps(3) E.Nmlize_Nml
                      E.Ide.simps(3) E.Ide_HcompNml E.Src.simps(3) arrE ideD(1))
                finally show ?thesis by simp
              qed
              moreover have
                "B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h) B
                   B.can ((Dom f  Dom g)  Dom h) ((Dom f  Dom g)  Dom h) =
                     B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h)"
              proof -
                have "E.Ide ((Dom f  Dom g)  Dom h)"
                  using f g h 1 4 7
                  by (metis (no_types, lifting) E.Ide.simps(3) E.Ide_HcompNml E.Src_HcompNml
                      arrE ideD(1))
                moreover have "E.Ide ((Dom f  Dom g)  Dom h)"
                  using f g h 1 7 E.Ide_HcompNml E.Nml_HcompNml(1) arr_char calculation
                        ideD(1)
                  by auto
                moreover have "E.Ide (Dom f  Dom g  Dom h)"
                  using f g h 1 4 6 by blast
                moreover have "E.Nmlize ((Dom f  Dom g)  Dom h) =
                               E.Nmlize ((Dom f  Dom g)  Dom h)"
                  using f g h 1 4 7
                  by (metis (no_types, lifting) E.Nml_HcompNml(1) E.Nmlize.simps(3)
                      E.Nmlize_Nml E.Ide.simps(3) arrE calculation(1) ideD(1))
                moreover have "E.Nmlize ((Dom f  Dom g)  Dom h) =
                               E.Nmlize (Dom f  Dom g  Dom h)"
                  using f g h 1 4 7 E.HcompNml_assoc by fastforce
                ultimately show ?thesis
                  using B.vcomp_can by simp
              qed
              ultimately show ?thesis by simp
            qed
            also have "... = B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h)"
            proof -
              have "E.Ide ((Dom f  Dom g)  Dom h)"
                using 1 4 7 by simp
              moreover have "E.Ide ((Dom f  Dom g)  Dom h)"
                using f g 1 4 7
                by (metis (no_types, lifting) E.Ide.simps(3) E.Ide_HcompNml E.Src_HcompNml
                    arrE ideD(1))
              moreover have "E.Ide (Dom f  Dom g  Dom h)"
                using f g h 6 by blast
              moreover have "E.Nmlize ((Dom f  Dom g)  Dom h) =
                             E.Nmlize ((Dom f  Dom g)  Dom h)"
                using f g h 1 7 E.Nml_HcompNml(1) by fastforce
              moreover have "E.Nmlize ((Dom f  Dom g)  Dom h) =
                             E.Nmlize (Dom f  Dom g  Dom h)"
                using f g h 1 4 7
                by (metis (no_types, lifting) E.Nml_HcompNml(1) E.Nmlize.simps(3)
                    E.Nmlize_Nml E.HcompNml_assoc E.Ide.simps(3) arrE ideD(1))
              ultimately show ?thesis
                using B.vcomp_can by simp
            qed
            finally show ?thesis by simp
          qed
          also have "... = cmpDN (f, g  h) B (DN f B cmpDN (g, h)) B
                           𝖺B[DN f, DN g, DN h]"
          proof -
            have "cmpDN (f, g  h) B (DN f B cmpDN (g, h)) B 𝖺B[DN f, DN g, DN h] =
                  (cmpDN (f, g  h) B (DN f B cmpDN (g, h))) B 𝖺B[DN f, DN g, DN h]"
              using B.comp_assoc by simp
            also have
              "... = B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) B
                       B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h)"
            proof -
              have "cmpDN (f, g  h) B (DN f B cmpDN (g, h)) =
                    B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h)"
              proof -
                have "cmpDN (f, g  h) B (DN f B cmpDN (g, h)) =
                      B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) B
                            (Map f B B.can (Dom g  Dom h) (Dom g  Dom h))"
                  using f g h fg gh VV.ide_charSbC VV.arr_charSbC DN_def by simp
                also have
                  "... = B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) B
                           (B.can (Dom f) (Dom f) B B.can (Dom g  Dom h) (Dom g  Dom h))"
                proof -
                  have "Map f = B.can (Dom f) (Dom f)"
                    using f arr_char B.can_Ide_self [of "Dom f"] Map_ide
                    by (metis (no_types, lifting) ide_char')
                  thus ?thesis by simp
                qed
                also have
                  "... = B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h) B
                         B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h)"
                  using 1 4 5 7 B.hcomp_can by auto
                also have "... = B.can (Dom f  Dom g  Dom h) (Dom f  Dom g  Dom h)"
                  using 1 4 5 6 7 8 B.vcomp_can by auto
                finally show ?thesis by simp
              qed
              moreover have "𝖺B[DN f, DN g, DN h] =
                             B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h)"
                using f g h 1 4 7 DN_def B.canE_associator(1) by auto
              ultimately show ?thesis by simp
            qed
            also have  "... = B.can (Dom f  Dom g  Dom h) ((Dom f  Dom g)  Dom h)"
              using 1 4 5 6 7 8 E.Nmlize_Hcomp_Hcomp B.vcomp_can by simp
            finally show ?thesis by simp
          qed
          finally show ?thesis by blast
        qed
      qed
    qed

    lemma DN_is_pseudofunctor:
    shows "pseudofunctor vcomp hcomp 𝖺 𝗂 src trg VB HB 𝖺B 𝗂B srcB trgB DN cmpDN"
      ..

    interpretation faithful_functor vcomp VB DN
      using arr_char dom_char cod_char DN_def
      apply unfold_locales
      by (metis (no_types, lifting) Cod_dom Dom_cod MkArr_Map)

    no_notation B.in_hom  ("«_ : _ B _»")

    lemma DN_UP:
    assumes "B.arr μ"
    shows "DN (UP μ) = μ"
      using assms UP_def DN_def arr_UP by auto

    interpretation DN: equivalence_pseudofunctor
                         vcomp hcomp 𝖺 𝗂 src trg VB HB 𝖺B 𝗂B srcB trgB DN cmpDN
    proof
      (* DN is locally (but not globally) full. *)
      show "f f' ν.  ide f; ide f'; src f = src f'; trg f = trg f'; «ν : DN f B DN f'» 
                          μ. «μ : f  f'»  DN μ = ν"
      proof -
        fix f f' ν
        assume f: "ide f" and f': "ide f'"
        and eq_src: "src f = src f'" and eq_trg: "trg f = trg f'"
        and ν: "«ν : DN f B DN f'»"
        show "μ. «μ : f  f'»  DN μ = ν"
        proof -
          let  = "MkArr (Dom f) (Dom f') ν"
          have μ: "« : f  f'»"
          proof
            have "Map f = Dom f"
              using f by simp
            have "Map f' = Dom f'"
              using f' by simp
            have "Dom f' = Cod f'"
              using f' Cod_ide by simp
            show μ: "arr "
            proof -
              have "E.Nml (Dom )  E.Ide (Dom )"
              proof -
                have "E.Nml (Dom f)  E.Ide (Dom f)"
                  using f ide_char arr_char by blast
                thus ?thesis
                  using f by simp
              qed
              moreover have "E.Nml (Cod )  E.Ide (Cod )"
              proof -
                have "E.Nml (Dom f')  E.Ide (Dom f')"
                  using f' ide_char arr_char by blast
                thus ?thesis
                  using f' by simp
              qed
              moreover have "E.Src (Dom ) = E.Src (Cod )"
                using f f' ν arr_char src_def eq_src ideD(1) by auto
              moreover have "E.Trg (Dom ) = E.Trg (Cod )"
                using f f' ν arr_char trg_def eq_trg ideD(1) by auto
              moreover have "«Map  : Dom  B Cod »"
              proof -
                have "«ν : Dom f B Dom f'»"
                  using f f' ν ide_char arr_char DN_def Cod_ide Map_ide
                  by (metis (no_types, lifting) ideD(1))
                thus ?thesis by simp
              qed
              ultimately show ?thesis
                using f f' ν ide_char arr_char by blast
            qed
            show "dom  = f"
              using f μ dom_char MkArr_Map MkIde_Dom' by simp
            show "cod  = f'"
            proof -
              have "cod  = MkIde (Dom f')"
                using μ cod_char by simp
              also have "... = MkArr (Dom f') (Cod f') (Map f')"
                using f' by auto
              also have "... = f'"
                using f' MkArr_Map by simp
              finally show ?thesis by simp
            qed
          qed
          moreover have "DN  = ν"
            using μ DN_def by auto
          ultimately show ?thesis by blast
        qed
      qed
      (* DN is biessentially surjective on objects. *)
      show "a'. B.obj a'  a. obj a  B.equivalent_objects (DN.map0 a) a'"
      proof -
        fix a'
        assume a': "B.obj a'"
        have "obj (UP.map0 a')"
          using a' UP.map0_simps(1) by simp
        moreover have "B.equivalent_objects (DN.map0 (UP.map0 a')) a'"
        proof -
          have "arr (MkArr a' a' a')"
            using a' UP_def [of a'] UP.preserves_reflects_arr [of a'] by auto
          moreover have "arr (MkArr a'0 a'0 a')"
            using a' arr_char obj_simps by auto
          ultimately have "DN.map0 (UP.map0 a') = a'"
            using a' UP.map0_def DN.map0_def DN_def src_def by auto
          thus ?thesis
            using a' B.equivalent_objects_reflexive by simp
        qed
        ultimately show "a. obj a  B.equivalent_objects (DN.map0 a) a'"
          by blast
      qed
      (* DN is locally essentially surjective. *)
      show "a b g.  obj a; obj b; «g : DN.map0 a B DN.map0 b»; B.ide g  
                       f. «f : a  b»  ide f  B.isomorphic (DN f) g"
      proof -
        fix a b g
        assume a: "obj a" and b: "obj b"
        and g: "«g : DN.map0 a B DN.map0 b»" and ide_g: "B.ide g"
        have "ide (UP g)"
          using ide_g UP.preserves_ide by simp
        moreover have "B.isomorphic (DN (UP g)) g"
          using ide_g DN_UP B.isomorphic_reflexive by simp
        moreover have "«UP g : a  b»"
        proof
          show "arr (UP g)"
            using g UP.preserves_reflects_arr by auto
          show "src (UP g) = a"
          proof -
            have "src (UP g) = MkArr srcB g0 srcB g0 (srcB g)"
              using ide_g src_def UP_def UP.preserves_reflects_arr [of g] B.ideD(1) by simp
            also have "... = a"
            proof -
              have "srcB g = srcB (DN.map0 a)"
                using a g B.in_hhom_def by simp
              also have "... = Map a"
                using a Map_preserves_objects DN.map0_def DN_def B.src_src B.obj_simps
                by auto
              finally have "srcB g = Map a" by simp
              hence "MkArr srcB g0 srcB g0 (srcB g) = MkArr Map a0 Map a0 (Map a)"
                by simp
              also have "... = a"
                using a obj_char [of a] MkIde_Dom [of a]
                apply (cases "Dom a")
                         apply force
                by simp_all
              finally show ?thesis by simp
            qed
            finally show ?thesis by simp
          qed
          show "trg (UP g) = b"
          proof -
            have "trg (UP g) = MkArr trgB g0 trgB g0 (trgB g)"
              using ide_g trg_def UP_def UP.preserves_reflects_arr [of g] B.ideD(1) by simp
            also have "... = b"
            proof -
              have "trgB g = trgB (DN.map0 b)"
                using b g B.in_hhom_def by simp
              also have "... = Map b"
                using b Map_preserves_objects DN.map0_def DN_def B.src_src B.obj_simps
                by auto
              finally have "trgB g = Map b" by simp
              hence "MkArr trgB g0 trgB g0 (trgB g) = MkArr Map b0 Map b0 (Map b)"
                by simp
              also have "... = b"
                using b obj_char [of b] MkIde_Dom [of b]
                apply (cases "Dom b")
                         apply force
                by simp_all
              finally show ?thesis by simp
            qed
            finally show ?thesis by simp
          qed
        qed
        ultimately show "f. «f : a  b»  ide f  B.isomorphic (DN f) g"
          by blast
      qed
    qed

    theorem DN_is_equivalence_pseudofunctor:
    shows "equivalence_pseudofunctor vcomp hcomp 𝖺 𝗂 src trg VB HB 𝖺B 𝗂B srcB trgB
             DN cmpDN"
      ..

    text ‹
      The following gives an explicit formula for a component of the unit isomorphism of
      the pseudofunctor UP› from a bicategory to its strictification.
      It is not currently being used -- I originally proved it in order to establish something
      that I later proved in a more abstract setting -- but it might be useful at some point.
    ›
    interpretation UP: equivalence_pseudofunctor
                         VB HB 𝖺B 𝗂B srcB trgB vcomp hcomp 𝖺 𝗂 src trg UP cmpUP
      using UP_is_equivalence_pseudofunctor by auto

    lemma UP_unit_char:
    assumes "B.obj a"
    shows "UP.unit a = MkArr a0 a a"
    proof -
      have " MkArr a0 a a = UP.unit a"
      proof (intro UP.unit_eqI)
        show "B.obj a"
          using assms by simp
        have 0: "«a : a B a»"
          using assms by auto
        have 1: "arr (MkArr a0 a a)"
          apply (unfold arr_char, intro conjI)
          using assms by auto
        have 2: "arr (MkArr a a a)"
          apply (unfold arr_char, intro conjI)
          using assms by auto
        have 3: "arr (MkArr a0 a0 a)"
          apply (unfold arr_char, intro conjI)
          using assms by auto
        show "«MkArr a0 a a : UP.map0 a  UP a»"
        proof
          show "arr (MkArr a0 a a)" by fact
          show "dom (MkArr a0 a a) = UP.map0 a"
            using assms 1 2 dom_char UP.map0_def UP_def src_def by auto
          show "cod (MkArr a0 a a) = UP a"
            using assms 1 2 cod_char UP.map0_def UP_def src_def by auto
        qed
        show "iso (MkArr a0 a a)"
          using assms 1 iso_char by auto
        show "MkArr a0 a a  𝗂 (UP.map0 a) =
              (UP 𝗂B[a]  cmpUP (a, a))  (MkArr a0 a a  MkArr a0 a a)"
        proof -
          have "MkArr a0 a a  𝗂 (UP.map0 a) = MkArr a0 a a"
            unfolding 𝗂_def UP.map0_def UP_def
            using assms 0 1 2 src_def by auto
          also have "... = (UP 𝗂B[a]  cmpUP (a, a))  (MkArr a0 a a  MkArr a0 a a)"
          proof -
            have "(UP 𝗂B[a]  cmpUP (a, a))  (MkArr a0 a a  MkArr a0 a a) =
                  (MkArr a B a a 𝗂B[a]  MkArr (a  a) a B a (a B a))
                      (MkArr a0 a a  MkArr a0 a a)"
              using assms UP_def cmpUP_ide_simp by auto
            also have "... = (MkArr a B a a 𝗂B[a]  MkArr (a  a) a B a (a B a))
                                MkArr a0 (a  a) (B.runit' a)"
              using assms 0 1 2 3 hcomp_def B.comp_cod_arr src_def trg_def
                    B.can_Ide_self B.canE_unitor [of "a0"] B.comp_cod_arr
              by auto
            also have "... = MkArr a0 a ((𝗂B[a] B (a B a)) B B.runit' a)"
            proof -
              have "MkArr a B a a 𝗂B[a]  MkArr (a  a) a B a (a B a) =
                    MkArr (a  a) a (𝗂B[a] B (a B a))"
                using assms
                by (intro comp_MkArr arr_MkArr) auto
              moreover have "MkArr (a  a) a (𝗂B[a] B (a B a))
                                MkArr a0 (a  a) (B.runit' a) =
                             MkArr a0 a ((𝗂B[a] B (a B a)) B B.runit' a)"
                using assms 0 B.comp_arr_dom
                by (intro comp_MkArr arr_MkArr, auto)
              ultimately show ?thesis by argo
            qed
            also have "... = MkArr a0 a a"
              using assms B.comp_arr_dom B.comp_arr_inv' B.iso_unit B.unitor_coincidence(2)
              by simp
            finally show ?thesis by argo
          qed
          finally show ?thesis by simp
        qed
      qed
      thus ?thesis by simp
    qed

  end

  subsection "Pseudofunctors into a Strict Bicategory"

  text ‹
    In the special case of a pseudofunctor into a strict bicategory, we can obtain
    explicit formulas for the images of the units and associativities under the pseudofunctor,
    which only involve the structure maps of the pseudofunctor, since the units and associativities
    in the target bicategory are all identities.  This is useful in applying strictification.
  ›

  locale pseudofunctor_into_strict_bicategory =
    pseudofunctor +
    D: strict_bicategory VD HD 𝖺D 𝗂D srcD trgD
  begin

    lemma image_of_unitor:
    assumes "C.ide g"
    shows "F 𝗅C[g] = (D.inv (unit (trgC g)) D F g) D D.inv (Φ (trgC g, g))"
    and "F 𝗋C[g] = (F g D D.inv (unit (srcC g))) D D.inv (Φ (g, srcC g))"
    and "F (C.lunit' g) = Φ (trgC g, g) D (unit (trgC g) D F g)"
    and "F (C.runit' g) = Φ (g, srcC g) D (F g D unit (srcC g))"
    proof -
      show A: "F 𝗅C[g] = (D.inv (unit (trgC g)) D F g) D D.inv (Φ (trgC g, g))"
      proof -
        have 1: "«(D.inv (unit (trgC g)) D F g) D D.inv (Φ (trgC g, g)) :
                     F (trgC g C g) D F g»"
        proof
          show "«D.inv (unit (trgC g)) D F g : F (trgC g) D F g D F g»"
            using assms unit_char by (auto simp add: D.hcomp_obj_arr)
          show "«D.inv (Φ (trgC g, g)) : F (trgC g C g) D F (trgC g) D F g»"
            using assms cmp_in_hom(2) D.inv_is_inverse by simp
        qed
        have "(D.inv (unit (trgC g)) D F g) D D.inv (Φ (trgC g, g)) =
              F g D (D.inv (unit (trgC g)) D F g) D D.inv (Φ (trgC g, g))"
          using 1 D.comp_cod_arr by auto
        also have "... = (F 𝗅C[g] D Φ (trgC g, g) D (unit (trgC g) D F g)) D
                           (D.inv (unit (trgC g)) D F g) D D.inv (Φ (trgC g, g))"
          using assms lunit_coherence [of g] D.strict_lunit by simp
        also have "... = F 𝗅C[g] D Φ (trgC g, g) D
                                    ((unit (trgC g) D F g) D (D.inv (unit (trgC g)) D F g)) D
                                   D.inv (Φ (trgC g, g))"
          using D.comp_assoc by simp
        also have "... = F 𝗅C[g]"
        proof -
          have "(unit (trgC g) D F g) D (D.inv (unit (trgC g)) D F g) = F (trgC g) D F g"
            using assms unit_char D.whisker_right
            by (metis C.ideD(1) C.obj_trg C.trg.preserves_reflects_arr D.comp_arr_inv'
                unit_simps(5) preserves_arr preserves_ide)
          moreover have "Φ (trgC g, g) D D.inv (Φ (trgC g, g)) = F (trgC g C g)"
            using assms D.comp_arr_inv D.inv_is_inverse by simp
          ultimately show ?thesis
            using assms D.comp_arr_dom D.comp_cod_arr unit_char by auto
        qed
        finally show ?thesis by simp
      qed
      show B: "F 𝗋C[g] = (F g D D.inv (unit (srcC g))) D D.inv (Φ (g, srcC g))"
      proof -
        have 1: "«(F g D D.inv (unit (srcC g))) D D.inv (Φ (g, srcC g)) :
                    F (g C srcC g) D F g»"
        proof
          show "«F g D D.inv (unit (srcC g)) : F g D F (srcC g) D F g»"
            using assms unit_char by (auto simp add: D.hcomp_arr_obj)
          show "«D.inv (Φ (g, srcC g)) : F (g C srcC g) D F g D F (srcC g)»"
            using assms cmp_in_hom(2) by simp
        qed
        have "(F g D D.inv (unit (srcC g))) D D.inv (Φ (g, srcC g)) =
              F g D (F g D D.inv (unit (srcC g))) D D.inv (Φ (g, srcC g))"
          using 1 D.comp_cod_arr by auto
        also have "... = (F 𝗋C[g] D Φ (g, srcC g) D (F g D unit (srcC g))) D
                           (F g D D.inv (unit (srcC g))) D D.inv (Φ (g, srcC g))"
           using assms runit_coherence [of g] D.strict_runit by simp
        also have "... = F 𝗋C[g] D (Φ (g, srcC g) D ((F g D unit (srcC g)) D
                           (F g D D.inv (unit (srcC g))))) D D.inv (Φ (g, srcC g))"
           using D.comp_assoc by simp
        also have "... = F 𝗋C[g]"
        proof -
          have "(F g D unit (srcC g)) D (F g D D.inv (unit (srcC g))) = F g D F (srcC g)"
            using assms D.whisker_left unit_char
            by (metis C.ideD(1) C.obj_src C.src.preserves_ide D.comp_arr_inv' D.ideD(1)
                unit_simps(5) preserves_ide)
          moreover have "Φ (g, srcC g) D D.inv (Φ (g, srcC g)) = F (g C srcC g)"
            using assms D.comp_arr_inv D.inv_is_inverse by simp
          ultimately show ?thesis
            using assms D.comp_arr_dom D.comp_cod_arr unit_char cmp_in_hom(2) [of g "srcC g"]
            by auto
        qed
        finally show ?thesis by simp
      qed
      show "F (C.lunit' g) = Φ (trgC g, g) D (unit (trgC g) D F g)"
      proof -
        have "F (C.lunit' g) = D.inv (F 𝗅C[g])"
          using assms C.iso_lunit preserves_inv by simp
        also have "... = D.inv ((D.inv (unit (trgC g)) D F g) D D.inv (Φ (trgC g, g)))"
          using A by simp
        also have "... = Φ (trgC g, g) D (unit (trgC g) D F g)"
        proof -
          have "D.iso (D.inv (Φ (trgC g, g)))  D.inv (D.inv (Φ (trgC g, g))) = Φ (trgC g, g)"
            using assms by simp
          moreover have "D.iso (D.inv (unit (trgC g)) D F g) 
                         D.inv (D.inv (unit (trgC g)) D F g) = unit (trgC g) D F g"
            using assms unit_char by simp
          moreover have "D.seq (D.inv (unit (trgC g)) D F g) (D.inv (Φ (trgC g, g)))"
            using assms unit_char by (metis A C.lunit_simps(1) preserves_arr)
          ultimately show ?thesis
            using D.inv_comp by simp
        qed
        finally show ?thesis by simp
      qed
      show "F (C.runit' g) = Φ (g, srcC g) D (F g D unit (srcC g))"
      proof -
        have "F (C.runit' g) = D.inv (F 𝗋C[g])"
          using assms C.iso_runit preserves_inv by simp
        also have "... = D.inv ((F g D D.inv (unit (srcC g))) D D.inv (Φ (g, srcC g)))"
          using B by simp
        also have "... = Φ (g, srcC g) D (F g D unit (srcC g))"
        proof -
          have "D.iso (D.inv (Φ (g, srcC g)))  D.inv (D.inv (Φ (g, srcC g))) = Φ (g, srcC g)"
            using assms by simp
          moreover have "D.iso (F g D D.inv (unit (srcC g))) 
                         D.inv (F g D D.inv (unit (srcC g))) = F g D unit (srcC g)"
            using assms unit_char by simp
          moreover have "D.seq (F g D D.inv (unit (srcC g))) (D.inv (Φ (g, srcC g)))"
            using assms unit_char by (metis B C.runit_simps(1) preserves_arr)
          ultimately show ?thesis
            using D.inv_comp by simp
        qed
        finally show ?thesis by simp
      qed
    qed

    lemma image_of_associator:
    assumes "C.ide f" and "C.ide g" and "C.ide h" and "srcC f = trgC g" and "srcC g = trgC h"
    shows "F 𝖺C[f, g, h] = Φ (f, g C h) D (F f D Φ (g, h)) D
                             (D.inv (Φ (f, g)) D F h) D D.inv (Φ (f C g, h))"
    and "F (C.𝖺' f g h) = Φ (f C g, h) D (Φ (f, g) D F h) D
                                (F f D D.inv (Φ (g, h))) D D.inv (Φ (f, g C h))"
    proof -
      show 1: "F 𝖺C[f, g, h] = Φ (f, g C h) D (F f D Φ (g, h)) D
                                 (D.inv (Φ (f, g)) D F h) D D.inv (Φ (f C g, h))"
      proof -
        have 2: "D.seq (Φ (f, g C h)) ((F f D Φ (g, h)) D 𝖺D[F f, F g, F h])"
          using assms D.assoc_in_hom(2) [of "F f" "F g" "F h"] cmp_simps(1,4) C.VV.cod_simp
          by (intro D.seqI) auto
        moreover have 3: "F 𝖺C[f, g, h] D Φ (f C g, h) D (Φ (f, g) D F h) =
                          Φ (f, g C h) D (F f D Φ (g, h)) D 𝖺D[F f, F g, F h]"
          using assms assoc_coherence [of f g h] by blast
        moreover have "D.iso (Φ (f C g, h) D (Φ (f, g) D F h))"
          using assms 2 3 C.VV.arr_charSbC C.VV.dom_charSbC C.VV.cod_charSbC FF_def D.isos_compose
          by auto
        ultimately have "F 𝖺C[f, g, h] =
                         (Φ (f, g C h) D ((F f D Φ (g, h)) D 𝖺D[F f, F g, F h])) D
                           D.inv (Φ (f C g, h) D (Φ (f, g) D F h))"
          using D.invert_side_of_triangle(2)
                  [of "Φ (f, g C h) D (F f D Φ (g, h)) D 𝖺D[F f, F g, F h]"
                      "F 𝖺C[f, g, h]" "Φ (f C g, h) D (Φ (f, g) D F h)"]
          by presburger
        also have "... = Φ (f, g C h) D (F f D Φ (g, h)) D
                            (D.inv (Φ (f, g)) D F h) D D.inv (Φ (f C g, h))"
        proof -
          have "D.inv (Φ (f C g, h) D (Φ (f, g) D F h)) =
                (D.inv (Φ (f, g)) D F h) D D.inv (Φ (f C g, h))"
          proof -
            have "D.seq (Φ (f C g, h)) (Φ (f, g) D F h)"
              using assms by fastforce
            thus ?thesis
              using assms D.inv_comp by simp
          qed
          moreover have "(F f D Φ (g, h)) D 𝖺D[F f, F g, F h] = (F f D Φ (g, h))"
            using assms D.comp_arr_dom D.assoc_in_hom [of "F f" "F g" "F h"] cmp_in_hom
            by (metis "2" "3" D.comp_arr_ide D.hseq_char D.seqE D.strict_assoc
                cmp_simps(2) cmp_simps(3) preserves_ide)
          ultimately show ?thesis
            using D.comp_assoc by simp
        qed
        finally show ?thesis
          by simp
      qed
      show "F (C.𝖺' f g h) = Φ (f C g, h) D (Φ (f, g) D F h) D
                               (F f D D.inv (Φ (g, h))) D D.inv (Φ (f, g C h))"
      proof -
        have "F (C.𝖺' f g h) = D.inv (F 𝖺C[f, g, h])"
          using assms preserves_inv by simp
        also have "... = D.inv (Φ (f, g C h) D (F f D Φ (g, h)) D
                                  (D.inv (Φ (f, g)) D F h) D D.inv (Φ (f C g, h)))"
          using 1 by simp
        also have "... = Φ (f C g, h) D (Φ (f, g) D F h) D
                                   (F f D D.inv (Φ (g, h))) D D.inv (Φ (f, g C h))"
          using assms C.VV.arr_charSbC FF_def D.hcomp_assoc D.comp_assoc
                C.VV.dom_simp C.VV.cod_simp
          (* OK, this is pretty cool, but not as cool as if I didn't have to direct it. *)
          by (simp add: D.inv_comp D.isos_compose)
        finally show ?thesis by simp
      qed
    qed

  end

  subsection "Internal Equivalences in a Strict Bicategory"

  text ‹
    In this section we prove a useful fact about internal equivalences in a strict bicategory:
    namely, that if the ``right'' triangle identity holds for such an equivalence then the
    ``left'' does, as well.  Later we will dualize this property, and use strictification to
    extend it to arbitrary bicategories.
  ›

  locale equivalence_in_strict_bicategory =
    strict_bicategory +
    equivalence_in_bicategory
  begin

    lemma triangle_right_implies_left:
    shows "(g  ε)  (η  g) = g  (ε  f)  (f  η) = f"
    proof -
      text ‹
        The formal proof here was constructed following the string diagram sketch below,
        which appears in cite"nlab-zigzag-diagram"
        (see it also in context in cite"nlab-adjoint-equivalence").
        The diagram is reproduced here by permission of its author, Mike Shulman,
        who says (private communication):
        ``Just don't give the impression that the proof itself is due to me, because it's not.
        I don't know who first gave that proof; it's probably folklore.''
        \begin{figure}[h]
          \includegraphics[width=6.5in]{triangle_right_implies_left.png}
        \end{figure}
      ›
      assume 1: "(g  ε)  (η  g) = g"
      have 2: "(inv η  g)  (g  inv ε) = g"
      proof -
        have "(inv η  g)  (g  inv ε) = inv ((g  ε)  (η  g))"
          using antipar inv_comp hcomp_assoc by simp
        also have "... = g"
          using 1 by simp
        finally show ?thesis by blast
      qed
      have "(ε  f)  (f  η) = (ε  f)  (f  (inv η  g)  (g  inv ε)  f)  (f  η)"
      proof -
        have "(f  (inv η  g)  (g  inv ε)  f)  (f  η) = f  η"
          using 2 ide_left ide_right antipar whisker_left
          by (metis comp_cod_arr unit_simps(1) unit_simps(3))
        thus ?thesis by simp
      qed
      also have "... = (ε  f)  (f  (inv η  g)  (g  inv ε)  f)  (f  η)  (inv η  η)"
      proof -
        have "inv η  η = src f"
          by (simp add: comp_inv_arr')
        thus ?thesis
          by (metis antipar(1) antipar(2) arrI calculation
              comp_ide_arr hcomp_arr_obj ideD(1) ide_left ide_right obj_src seqE
              strict_assoc' triangle_in_hom(1) vconn_implies_hpar(1))
      qed
      also have "... = (ε  (f  (inv η  g)  (g  inv ε))  ((f  inv η)  (f  η)))  (f  η)"
        using ide_left ide_right antipar unit_is_iso
        by (metis "2" arr_inv calculation comp_arr_dom comp_inv_arr' counit_simps(1)
            counit_simps(2) dom_inv hcomp_arr_obj ideD(1) unit_simps(1) unit_simps(2)
            unit_simps(5) obj_trg seqI whisker_left)
      also have "... = (ε  (f  (inv η  g)  (g  inv ε)) 
                         ((f  inv η)  ((inv ε  f)  (ε  f))  (f  η)))  (f  η)"
      proof -
        have "(inv ε  f)  (ε  f) = (f  g)  f"
          using whisker_right [of f "inv ε" ε] counit_in_hom
          by (simp add: antipar(1) comp_inv_arr')
        thus ?thesis
          using hcomp_assoc comp_arr_dom
          by (metis comp_cod_arr ide_left local.unit_simps(1) local.unit_simps(3)
              whisker_left)
      qed
      also have "... = (((ε  (f  (inv η  g)  (g  inv ε)))  (f  g)) 
                         (((f  inv η)  (inv ε  f))  (ε  f)  (f  η))) 
                           (f  η)"
        using ide_left ide_right antipar comp_assoc whisker_right comp_cod_arr
        by (metis "2" comp_arr_dom counit_simps(1-2))
      also have "... = (((ε  (f  (inv η  g)  (g  inv ε)))  ((f  inv η)  (inv ε  f))) 
                         ((f  g)  (ε  f)  (f  η))) 
                           (f  η)"
      proof -
        have 3: "seq (ε  (f  (inv η  g)  (g  inv ε))) (f  g)"
          using 2 antipar by auto
        moreover have 4: "seq ((f  inv η)  (inv ε  f)) ((ε  f)  (f  η))"
          using antipar hcomp_assoc by auto
        ultimately show ?thesis
          using interchange by simp
      qed
      also have "... = ((ε  (f  (inv η  g)  (g  inv ε)))  ((f  inv η)  (inv ε  f))) 
                        ((f  g)  (ε  f)  (f  η))  (f  η)"
        using comp_assoc by presburger
      also have "... = ((ε  (f  inv η)  (inv ε  f)) 
                         ((f  (inv η  g)  (g  inv ε))  f)) 
                           (f  (g  ε)  (η  g)  f)  (f  η)"
      proof -
        have "(ε  (f  (inv η  g)  (g  inv ε)))  ((f  inv η)  (inv ε  f)) =
              (ε  (f  inv η)  (inv ε  f))  ((f  (inv η  g)  (g  inv ε))  f)"
        proof -
          have "seq ε (f  (inv η  g)  (g  inv ε))"
            using 2 antipar by simp
          moreover have "seq ((f  inv η)  (inv ε  f)) f"
            using antipar hcomp_assoc hcomp_obj_arr by auto
          ultimately show ?thesis
            using comp_assoc comp_arr_dom hcomp_obj_arr
                  interchange [of ε "f  (inv η  g)  (g  inv ε)" "(f  inv η)  (inv ε  f)" f]
            by simp
        qed
        moreover have "((f  g)  (ε  f)  (f  η))  (f  η) =
                       (f  (g  ε)  (η  g)  f)  (f  η)"
        proof -
          have "((f  g)  (ε  f)  (f  η))  (f  η) =
                (f  g  ε  f)  (f  (g  f)  η)  (f  η  src f)"
            using antipar comp_assoc hcomp_assoc whisker_left hcomp_arr_obj by simp
          also have "... = (f  g  ε  f)  (f  ((g  f)  η)  (η  src f))"
            using antipar comp_arr_dom whisker_left hcomp_arr_obj by simp
          also have "... = (f  g  ε  f)  (f  η  η)"
            using antipar comp_arr_dom comp_cod_arr hcomp_arr_obj
                  interchange [of "g  f" η η "src f"]
            by simp
          also have "... = (f  g  ε  f)  (f  η  g  f)  (f  src f  η)"
            using antipar comp_arr_dom comp_cod_arr whisker_left
                  interchange [of η "src f" "g  f" η]
            by simp
          also have "... = ((f  g  ε  f)  (f  η  g  f))  (f  η)"
            using antipar comp_assoc by (simp add: hcomp_obj_arr)
          also have "... = (f  (g  ε)  (η  g)  f)  (f  η)"
            using antipar comp_assoc whisker_left whisker_right hcomp_assoc by simp
          finally show ?thesis by blast
        qed
        ultimately show ?thesis by simp
      qed
      also have "... = (ε  (f  inv η)  (inv ε  f)) 
                         ((f  (inv η  g)  (g  inv ε)  f) 
                           (f  (g  ε)  (η  g)  f))  (f  η)"
        using comp_assoc hcomp_assoc antipar(1) antipar(2) by auto
      also have "... = (ε  (f  inv η)  (inv ε  f)) 
                         ((f  (inv η  g)  (g  inv ε)  (g  ε)  (η  g)  f)) 
                           (f  η)"
        using ide_left ide_right antipar comp_cod_arr comp_assoc whisker_left
        by (metis "1" "2" comp_ide_self unit_simps(1) unit_simps(3))
      also have "... = (ε  (f  inv η)  (inv ε  f))  (f  η)"
      proof -
        have "(inv η  g)  (g  inv ε)  (g  ε)  (η  g) = g"
          using ide_left ide_right antipar comp_arr_dom comp_assoc
          by (metis "1" "2" comp_ide_self)
        thus ?thesis
          using antipar comp_cod_arr by simp
      qed
      also have "... = (f  inv η)  ((inv ε  f)  (ε  f))  (f  η)"
      proof -
        have "(ε  (f  inv η)  (inv ε  f))  (f  η) =
              (trg f  ε  (f  inv η)  (inv ε  f))  (f  η)"
          using hcomp_obj_arr comp_cod_arr by simp
        also have "... = ((trg f  f  inv η)  (ε  inv ε  f))  (f  η)"
          using antipar hcomp_arr_obj hcomp_assoc interchange by auto
        also have "... = (f  inv η)  ((inv ε  f)  (ε  f))  (f  η)"
        proof -
          have "(inv ε  f)  (ε  f) = (trg f  inv ε  f)  (ε  trg f  f)"
            using hseqI' by (simp add: hcomp_obj_arr)
          also have "... = ε  inv ε  f"
            using antipar comp_arr_dom comp_cod_arr
                  interchange [of "trg f" ε "inv ε  f" "trg f  f"]
            by force
          finally have "(inv ε  f)  (ε  f) = ε  inv ε  f" by simp
          moreover have "trg f  f  inv η = f  inv η"
            using hcomp_obj_arr [of "trg f" "f  inv η"] by fastforce
          ultimately have "((trg f  f  inv η)  (ε  inv ε  f))  (f  η) =
                           ((f  inv η)  ((inv ε  f)  (ε  f)))  (f  η)"
            by simp
          thus ?thesis
            using comp_assoc by simp
        qed
        finally show ?thesis by simp
      qed
      also have "... = f  inv η  η"
      proof -
        have "(inv ε  f)  (ε  f) = f  g  f"
          using ide_left ide_right antipar counit_is_iso whisker_right hcomp_assoc
          by (metis comp_arr_dom comp_inv_arr' counit_simps(1) counit_simps(2) seqE)
        thus ?thesis
          using ide_left ide_right antipar unit_is_iso comp_cod_arr
          by (metis arr_inv dom_inv unit_simps(1) unit_simps(3) seqI whisker_left)
      qed
      also have "... = f  src f"
        using antipar by (simp add: comp_inv_arr')
      also have "... = f"
        using hcomp_arr_obj by simp
      finally show ?thesis by simp
    qed

  end

  text ‹
    Now we use strictification to generalize the preceding result to arbitrary bicategories.
    I originally attempted to generalize this proof directly from the strict case, by filling
    in the necessary canonical isomorphisms, but it turned out to be too daunting.
    The proof using strictification is still fairly tedious, but it is manageable.
  ›

  context equivalence_in_bicategory
  begin

    interpretation S: strictified_bicategory V H 𝖺 𝗂 src trg ..

    notation S.vcomp  (infixr "S" 55)
    notation S.hcomp  (infixr "S" 53)
    notation S.in_hom  ("«_ : _ S _»")
    notation S.in_hhom  ("«_ : _ S _»")

    interpretation UP: equivalence_pseudofunctor V H 𝖺 𝗂 src trg
                          S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg S.UP S.cmpUP
      using S.UP_is_equivalence_pseudofunctor by auto
    interpretation UP: pseudofunctor_into_strict_bicategory V H 𝖺 𝗂 src trg
                          S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg S.UP S.cmpUP
      ..
    interpretation E: equivalence_in_bicategory S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg
                        S.UP f S.UP g
                        S.inv (S.cmpUP (g, f)) S S.UP η S UP.unit (src f)
                        S.inv (UP.unit (trg f)) S S.UP ε S S.cmpUP (f, g)
      using equivalence_in_bicategory_axioms UP.preserves_equivalence [of f g η ε] by auto
    interpretation E: equivalence_in_strict_bicategory S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg
                        S.UP f S.UP g
                        S.inv (S.cmpUP (g, f)) S S.UP η S UP.unit (src f)
                        S.inv (UP.unit (trg f)) S S.UP ε S S.cmpUP (f, g)
      ..

    lemma UP_triangle:
    shows "S.UP ((g  ε)  𝖺[g, f, g]  (η  g)) =
            S.cmpUP (g, src g) S (S.UP g S S.UP ε S S.cmpUP (f, g)) S
              (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g) S S.inv (S.cmpUP (trg g, g))"
    and "S.UP (𝗋-1[g]  𝗅[g]) =
            (S.cmpUP (g, src g) S (S.UP g S UP.unit (src g))) S
               (S.inv (UP.unit (trg g)) S S.UP g) S S.inv (S.cmpUP (trg g, g))"
    and "S.UP ((ε  f)  𝖺-1[f, g, f]  (f  η)) =
            S.cmpUP (trg f, f) S (S.UP ε S S.cmpUP (f, g) S S.UP f) S
              (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) S S.inv (S.cmpUP (f, src f))"
    and "S.UP (𝗅-1[f]  𝗋[f]) =
            (S.cmpUP (trg f, f) S (UP.unit (trg f) S S.UP f)) S
              (S.UP f S S.inv (UP.unit (src f))) S S.inv (S.cmpUP (f, src f))"
    and "(g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g] 
            S.cmpUP (trg f, f) S (S.UP ε S S.cmpUP (f, g) S S.UP f) S
                 (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) S S.inv (S.cmpUP (f, src f)) =
               (S.cmpUP (trg f, f) S (UP.unit (trg f) S S.UP f)) S
                 (S.UP f S S.inv (UP.unit (src f))) S S.inv (S.cmpUP (f, src f))"
    proof -
      show T1: "S.UP ((g  ε)  𝖺[g, f, g]  (η  g)) =
                S.cmpUP (g, src g) S (S.UP g S S.UP ε S S.cmpUP (f, g)) S
                  (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g) S S.inv (S.cmpUP (trg g, g))"
      proof -
        have "S.UP ((g  ε)  𝖺[g, f, g]  (η  g)) =
                S.UP (g  ε) S S.UP 𝖺[g, f, g] S S.UP (η  g)"
          using antipar by simp
        also have "... =
                   (S.cmpUP (g, src g) S (S.UP g S S.UP ε) S
                   ((S.inv (S.cmpUP (g, f  g)) S S.cmpUP (g, f  g)) S
                     (S.UP g S S.cmpUP (f, g))) S
                   (((S.inv (S.cmpUP (g, f)) S S.UP g) S (S.inv (S.cmpUP (g  f, g)))) S
                   S.cmpUP (g  f, g)) S (S.UP η S S.UP g)) S S.inv (S.cmpUP (trg g, g))"
        proof -
          have "S.UP 𝖺[g, f, g] =
                S.cmpUP (g, f  g) S (S.UP g S S.cmpUP (f, g)) S
                (S.inv (S.cmpUP (g, f)) S S.UP g) S S.inv (S.cmpUP (g  f, g))"
            using ide_left ide_right antipar UP.image_of_associator [of g f g] by simp
          moreover have
            "S.UP (g  ε) =
             S.cmpUP (g, src g) S (S.UP g S S.UP ε) S S.inv (S.cmpUP (g, f  g))"
          proof -
            have "S.seq (S.cmpUP (g, src g)) (S.UP g S S.UP ε)"
              using antipar UP.FF_def UP.cmp_in_hom [of g "src g"]
              apply (intro S.seqI) by auto
            moreover have
              "S.UP (g  ε) S S.cmpUP (g, f  g) = S.cmpUP (g, src g) S (S.UP g S S.UP ε)"
              using antipar UP.Φ.naturality [of "(g, ε)"] UP.FF_def VV.arr_charSbC
                    VV.dom_simp VV.cod_simp
              by simp
            moreover have "S.iso (S.cmpUP (g, f  g))"
              using antipar by simp
            ultimately show ?thesis
              using S.invert_side_of_triangle(2)
                      [of "S.cmpUP (g, src g) S (S.UP g S S.UP ε)" "S.UP (g  ε)"
                          "S.cmpUP (g, f  g)"] S.comp_assoc
              by presburger
          qed
          moreover have "S.UP (η  g) =
                         (S.cmpUP (g  f, g) S (S.UP η S S.UP g)) S S.inv (S.cmpUP (trg g, g))"
          proof -
            have "S.UP (η  g) S S.cmpUP (trg g, g) =
                  S.cmpUP (g  f, g) S (S.UP η S S.UP g)"
              using antipar UP.Φ.naturality [of "(η, g)"] UP.FF_def VV.arr_charSbC
                    VV.dom_simp VV.cod_simp
              by simp
            moreover have "S.seq (S.cmpUP (g  f, g)) (S.UP η S S.UP g)"
              using antipar UP.cmp_in_hom(2) by (intro S.seqI, auto)
            ultimately show ?thesis
              using antipar S.invert_side_of_triangle(2) by simp
          qed
          ultimately show ?thesis
            using S.comp_assoc by simp
        qed
        also have "... = S.cmpUP (g, src g) S
                           ((S.UP g S S.UP ε) S (S.UP g S S.cmpUP (f, g))) S
                           ((S.inv (S.cmpUP (g, f)) S S.UP g) S (S.UP η S S.UP g)) S
                           S.inv (S.cmpUP (trg g, g))"
        proof -
          have "(S.inv (S.cmpUP (g  f, g)) S S.cmpUP (g  f, g)) S (S.UP η S S.UP g) =
                (S.UP η S S.UP g)"
            using antipar S.comp_inv_arr' S.comp_cod_arr by auto
          moreover have "(S.inv (S.cmpUP (g, f  g)) S S.cmpUP (g, f  g)) S
                         (S.UP g S S.cmpUP (f, g))
                           = (S.UP g S S.cmpUP (f, g))"
          proof -
            have "S.inv (S.cmpUP (g, f  g)) S S.cmpUP (g, f  g) = S.UP g S S.UP (f  g)"
              using antipar S.comp_inv_arr' UP.cmp_in_hom by auto
            thus ?thesis
              using antipar VV.arr_charSbC S.comp_cod_arr by simp
          qed
          ultimately show ?thesis
            using S.comp_assoc by simp
        qed
        also have "... = S.cmpUP (g, src g) S (S.UP g S S.UP ε S S.cmpUP (f, g)) S
                           (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g) S
                           S.inv (S.cmpUP (trg g, g))"
            using antipar VV.arr_charSbC S.whisker_left S.whisker_right by auto
        finally show ?thesis by simp
      qed
      show T2: "S.UP (𝗋-1[g]  𝗅[g]) =
                (S.cmpUP (g, src g) S (S.UP g S UP.unit (src g))) S
                   (S.inv (UP.unit (trg g)) S S.UP g) S S.inv (S.cmpUP (trg g, g))"
        using UP.image_of_unitor by simp
      show "S.UP ((ε  f)  𝖺-1[f, g, f]  (f  η)) =
            S.cmpUP (trg f, f) S (S.UP ε S S.cmpUP (f, g) S S.UP f) S
              (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) S S.inv (S.cmpUP (f, src f))"
      proof -
        have "S.UP ((ε  f)  𝖺-1[f, g, f]  (f  η)) =
                 S.UP (ε  f) S S.UP 𝖺-1[f, g, f] S S.UP (f  η)"
          using antipar by simp
        also have "... = S.cmpUP (trg f, f) S (S.UP ε S S.UP f) S
                          (S.inv (S.cmpUP (f  g, f)) S S.cmpUP (f  g, f) S
                           (S.cmpUP (f, g) S S.UP f)) S
                         (S.UP f S S.inv (S.cmpUP (g, f))) S (S.inv (S.cmpUP (f, g  f)) S
                         S.cmpUP (f, g  f) S (S.UP f S S.UP η)) S S.inv (S.cmpUP (f, src f))"
        proof -
          have "S.UP 𝖺-1[f, g, f] =
                S.cmpUP (f  g, f) S (S.cmpUP (f, g) S S.UP f) S (S.UP f S S.inv (S.cmpUP (g, f))) S
                   S.inv (S.cmpUP (f, g  f))"
            using ide_left ide_right antipar UP.image_of_associator by simp
          moreover have "S.UP (ε  f) =
                         S.cmpUP (trg f, f) S (S.UP ε S S.UP f) S S.inv (S.cmpUP (f  g, f))"
          proof -
            have "S.seq (S.cmpUP (trg f, f)) (S.UP ε S S.UP f)"
              using antipar UP.FF_def VV.ide_charSbC VV.arr_charSbC UP.cmp_in_hom [of "trg f" f]
              apply (intro S.seqI) by auto
            moreover have
              "S.cmpUP (trg f, f) S (S.UP ε S S.UP f) = S.UP (ε  f) S S.cmpUP (f  g, f)"
              using antipar UP.Φ.naturality [of "(ε, f)"] UP.FF_def VV.arr_charSbC
                    VV.dom_simp VV.cod_simp
              by simp
            moreover have "S.iso (S.cmpUP (f  g, f))"
              using antipar by simp
            ultimately show ?thesis
              using antipar S.comp_assoc
                    S.invert_side_of_triangle(2)
                      [of "S.cmpUP (trg f, f) S (S.UP ε S S.UP f)" "S.UP (ε  f)"
                          "S.cmpUP (f  g, f)"]
              by metis
          qed
          moreover have "S.UP (f  η) =
                        (S.cmpUP (f, g  f) S (S.UP f S S.UP η)) S S.inv (S.cmpUP (f, src f))"
          proof -
            have "S.cmpUP (f, g  f) S (S.UP f S S.UP η) =
                  S.UP (f  η) S S.cmpUP (f, src f)"
              using antipar UP.Φ.naturality [of "(f, η)"] UP.FF_def VV.arr_charSbC
                    VV.dom_simp VV.cod_simp
              by simp
            moreover have "S.seq (S.cmpUP (f, g  f)) (S.UP f S S.UP η)"
              using antipar by (intro S.seqI, auto)
            ultimately show ?thesis
              using antipar S.invert_side_of_triangle(2) by auto
          qed
          ultimately show ?thesis
            using S.comp_assoc by simp
        qed
        also have "... = S.cmpUP (trg f, f) S
                           ((S.UP ε S S.UP f) S (S.cmpUP (f, g) S S.UP f)) S
                           ((S.UP f S S.inv (S.cmpUP (g, f))) S (S.UP f S S.UP η)) S
                           S.inv (S.cmpUP (f, src f))"
        proof -
          have "(S.inv (S.cmpUP (f  g, f)) S S.cmpUP (f  g, f)) S (S.cmpUP (f, g) S S.UP f) =
                (S.cmpUP (f, g) S S.UP f)"
            using antipar S.comp_cod_arr VV.arr_charSbC S.comp_inv_arr' by auto
          moreover have "(S.inv (S.cmpUP (f, g  f)) S S.cmpUP (f, g  f)) S
                         (S.UP f S S.UP η)
                         = (S.UP f S S.UP η)"
            using antipar S.comp_inv_arr' S.comp_cod_arr by auto
          ultimately show ?thesis
            using S.comp_assoc by simp
        qed
        also have "... = S.cmpUP (trg f, f) S (S.UP ε S S.cmpUP (f, g) S S.UP f) S
                           (S.UP f S
                              S.inv (S.cmpUP (g, f)) S S.UP η) S S.inv (S.cmpUP (f, src f))"
            using antipar VV.arr_charSbC S.whisker_left S.whisker_right by auto
        finally show ?thesis by simp
      qed
      show "S.UP (𝗅-1[f]  𝗋[f]) =
            (S.cmpUP (trg f, f) S (UP.unit (trg f) S S.UP f)) S
              (S.UP f S S.inv (UP.unit (src f))) S S.inv (S.cmpUP (f, src f))"
        using UP.image_of_unitor by simp
      show "(g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g] 
              S.cmpUP (trg f, f) S (S.UP ε S S.cmpUP (f, g) S S.UP f) S
                  (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) S S.inv (S.cmpUP (f, src f)) =
              (S.cmpUP (trg f, f) S (UP.unit (trg f) S S.UP f)) S
                  (S.UP f S S.inv (UP.unit (src f))) S S.inv (S.cmpUP (f, src f))"
      proof -
        assume A: "(g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g]"
        have B: "(S.UP g S S.inv (UP.unit (src g)) S S.UP ε S S.cmpUP (f, g)) S
                   (S.inv (S.cmpUP (g, f)) S S.UP η S UP.unit (trg g) S S.UP g) = S.UP g"
        proof -
          show "(S.UP g S S.inv (UP.unit (src g)) S S.UP ε S S.cmpUP (f, g)) S
                (S.inv (S.cmpUP (g, f)) S S.UP η S UP.unit (trg g) S S.UP g) = S.UP g"
          proof -
            have 2: "S.cmpUP (g, src g) S (S.UP g S S.UP ε S S.cmpUP (f, g)) S
                       (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g) S
                       S.inv (S.cmpUP (trg g, g))
                     = (S.cmpUP (g, src g) S (S.UP g S UP.unit (src g))) S
                         (S.inv (UP.unit (trg g)) S S.UP g) S S.inv (S.cmpUP (trg g, g))"
              using A T1 T2 by simp
            show ?thesis
            proof -
              have 8: "S.seq (S.cmpUP (g, src g))
                             ((S.UP g S S.UP ε S S.cmpUP (f, g)) S
                               (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g) S
                               S.inv (S.cmpUP (trg g, g)))"
                using antipar VV.arr_charSbC S.hcomp_assoc
                by (metis (no_types, lifting) S.arr_UP T1 arrI triangle_in_hom(2))
              have 7: "S.seq (S.cmpUP (g, src g))
                             ((S.UP g S UP.unit (src g)) S (S.inv (UP.unit (trg g)) S S.UP g) S
                               S.inv (S.cmpUP (trg g, g)))"
                using antipar 2 8 S.comp_assoc by auto
              have 5: "(S.UP g S S.UP ε S S.cmpUP (f, g)) S
                         (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g) =
                       (S.UP g S UP.unit (src g)) S (S.inv (UP.unit (trg g)) S S.UP g)"
              proof -
                have "((S.UP g S S.UP ε S S.cmpUP (f, g)) S (S.inv (S.cmpUP (g, f)) S
                        S.UP η S S.UP g)) S S.inv (S.cmpUP (trg g, g)) =
                      ((S.UP g S UP.unit (src g)) S (S.inv (UP.unit (trg g)) S S.UP g)) S
                        S.inv (S.cmpUP (trg g, g))"
                proof -
                  have "S.mono (S.cmpUP (g, src g))"
                    using antipar S.iso_is_section S.section_is_mono by simp
                  thus ?thesis
                    using 2 8 7 S.monoE S.comp_assoc by presburger
                qed
                moreover have "S.epi (S.inv (S.cmpUP (trg g, g)))"
                  using antipar S.iso_is_retraction S.retraction_is_epi by simp
                moreover have "S.seq ((S.UP g S S.UP ε S S.cmpUP (f, g)) S
                                      (S.inv (S.cmpUP (g, f)) S
                                      S.UP η S S.UP g))
                                     (S.inv (S.cmpUP (trg g, g)))"
                  using S.comp_assoc S.seq_char 8 by presburger
                moreover have
                  "S.seq ((S.UP g S UP.unit (src g)) S (S.inv (UP.unit (trg g)) S S.UP g))
                         (S.inv (S.cmpUP (trg g, g)))"
                  using antipar calculation(1,3) by presburger
                ultimately show ?thesis
                  using 2 S.epiE by blast
              qed
              have 6: "S.seq (S.UP g S S.UP ε S S.cmpUP (f, g))
                             (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g)"
                using antipar VV.arr_charSbC S.hcomp_assoc by auto
              have 3: "(S.UP g S S.inv (UP.unit (src g))) S (S.UP g S S.UP ε S S.cmpUP (f, g)) S
                       (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g) =
                       (S.inv (UP.unit (trg g)) S S.UP g)"
              proof -
                have "S.seq (S.UP g S S.UP ε S S.cmpUP (f, g))
                            (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g)"
                  using 6 by simp
                moreover have "(S.UP g S UP.unit (src g)) S (S.inv (UP.unit (trg g)) S S.UP g) =
                               (S.UP g S S.UP ε S S.cmpUP (f, g)) S
                                 (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g)"
                  using 5 by argo
                moreover have "S.iso (S.UP g S UP.unit (src g))"
                  using antipar UP.unit_char S.UP_map0_obj by simp
                moreover have "S.inv (S.UP g S UP.unit (src g)) =
                               S.UP g S S.inv (UP.unit (src g))"
                  using antipar UP.unit_char S.UP_map0_obj by simp
                ultimately show ?thesis
                  using S.invert_side_of_triangle(1)
                          [of "(S.UP g S S.UP ε S S.cmpUP (f, g)) S
                                 (S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g)"
                              "S.UP g S UP.unit (src g)" "S.inv (UP.unit (trg g)) S S.UP g"]
                  by presburger
              qed
              have 4: "((S.UP g S S.inv (UP.unit (src g))) S
                         (S.UP g S S.UP ε S S.cmpUP (f, g))) S
                         ((S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g)) S
                         (UP.unit (trg g) S S.UP g)
                       = S.UP g"
              proof -
                have "(((S.UP g S S.inv (UP.unit (src g))) S (S.UP g S S.UP ε S S.cmpUP (f, g))) S
                         ((S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g)) S
                         (UP.unit (trg g) S S.UP g)) =
                      (((S.UP g S S.inv (UP.unit (src g))) S
                         (S.UP g S S.UP ε S S.cmpUP (f, g))) S
                         ((S.inv (S.cmpUP (g, f)) S S.UP η S S.UP g))) S
                         (UP.unit (trg g) S S.UP g)"
                  using S.comp_assoc by simp
                also have "... =
                           (S.inv (UP.unit (trg g)) S S.UP g) S (UP.unit (trg g) S S.UP g)"
                  using 3 S.comp_assoc by auto
                also have "... = S.inv (UP.unit (trg g)) S UP.unit (trg g) S S.UP g"
                  using UP.unit_char(2) S.whisker_right by auto
                also have "... = UP.map0 (trg g) S S.UP g"
                  using UP.unit_char [of "trg g"] S.comp_inv_arr S.inv_is_inverse by simp
                also have "... = S.UP g"
                  using S.UP_map0_obj by (simp add: S.hcomp_obj_arr)
                finally show ?thesis by blast
              qed
              thus ?thesis
                using antipar S.whisker_left S.whisker_right UP.unit_char S.comp_assoc by simp
            qed
          qed
        qed
        show "S.cmpUP (trg f, f) S (S.UP ε S S.cmpUP (f, g) S S.UP f) S
                (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) S S.inv (S.cmpUP (f, src f)) =
              (S.cmpUP (trg f, f) S (UP.unit (trg f) S S.UP f)) S
                (S.UP f S S.inv (UP.unit (src f))) S S.inv (S.cmpUP (f, src f))"
        proof -
          have "(S.UP ε S S.cmpUP (f, g) S S.UP f) S (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) =
                   (UP.unit (trg f) S S.UP f) S (S.UP f S S.inv (UP.unit (src f)))"
          proof -
            have 2: "(S.inv (UP.unit (trg f)) S S.UP f) S
                        ((S.UP ε S S.cmpUP (f, g) S S.UP f) S
                          (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η)) S
                        (S.UP f S UP.unit (src f)) =
                     S.UP f"
            proof -
              have "S.UP f = (S.inv (UP.unit (trg f)) S S.UP ε S 
                               S.cmpUP (f, g) S S.UP f) S
                               (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η S UP.unit (src f))"
                using B antipar E.triangle_right_implies_left by argo
              also have "... = (S.inv (UP.unit (trg f)) S S.UP f) S
                                 ((S.UP ε S S.cmpUP (f, g) S S.UP f) S
                                    (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η)) S
                                 (S.UP f S UP.unit (src f))"
              proof -
                have "S.inv (UP.unit (trg f)) S S.UP ε S S.cmpUP (f, g) S S.UP f =
                        (S.inv (UP.unit (trg f)) S S.UP f) S
                        (S.UP ε S S.cmpUP (f, g) S S.UP f)"
                  using UP.unit_char S.whisker_right by simp
                moreover have "S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η S UP.unit (src f) =
                                 (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) S
                                   (S.UP f S UP.unit (src f))"
                  using antipar UP.unit_char S.whisker_left S.comp_assoc by simp
                ultimately show ?thesis
                  using S.comp_assoc by presburger
              qed
              finally show ?thesis by argo
            qed
            show ?thesis
            proof -
              have "((S.UP ε S S.cmpUP (f, g) S S.UP f) S
                        (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η)) S
                        (S.UP f S UP.unit (src f)) =
                     (UP.unit (trg f) S S.UP f)"
              proof -
                have "S.inv (S.inv (UP.unit (trg f)) S S.UP f) S S.UP f =
                      UP.unit (trg f) S S.UP f"
                  using UP.unit_char S.comp_arr_dom S.UP_map0_obj
                  by (simp add: S.hcomp_obj_arr)
                moreover have "S.arr (S.UP f)"
                  by simp
                moreover have "S.iso (S.inv (UP.unit (trg f)) S S.UP f)"
                  using S.UP_map0_obj by (simp add: UP.unit_char(2))
                ultimately show ?thesis
                  using 2 S.invert_side_of_triangle(1)
                            [of "S.UP f" "S.inv (UP.unit (trg f)) S S.UP f"
                                "((S.UP ε S S.cmpUP (f, g) S S.UP f) S
                                   (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η)) S
                                 (S.UP f S UP.unit (src f))"]
                  by presburger
              qed
              moreover have "S.hseq (UP.unit (trg f)) (S.UP f) 
                             S.iso (S.UP f S UP.unit (src f)) 
                             S.inv (S.UP f S UP.unit (src f)) = S.UP f S S.inv (UP.unit (src f))"
                using UP.unit_char S.UP_map0_obj by simp
              ultimately show ?thesis
                using S.invert_side_of_triangle(2)
                        [of "UP.unit (trg f) S S.UP f"
                            "(S.UP ε S S.cmpUP (f, g) S S.UP f) S
                               (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η)"
                            "S.UP f S UP.unit (src f)"]
                by presburger
            qed
          qed
          hence "S.cmpUP (trg f, f) S ((S.UP ε S S.cmpUP (f, g) S S.UP f) S
                   (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η)) S S.inv (S.cmpUP (f, src f)) =
                 S.cmpUP (trg f, f) S ((UP.unit (trg f) S S.UP f) S
                   (S.UP f S S.inv (UP.unit (src f)))) S S.inv (S.cmpUP (f, src f))"
            by simp
          thus ?thesis
            using S.comp_assoc by simp
        qed
      qed
    qed

    lemma triangle_right_implies_left:
    assumes "(g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g]"
    shows "(ε  f)  𝖺-1[f, g, f]  (f  η) = 𝗅-1[f]  𝗋[f]"
    proof -
      have "par ((ε  f)  𝖺-1[f, g, f]  (f  η)) (𝗅-1[f]  𝗋[f])"
        using antipar by simp
      moreover have "S.UP ((ε  f)  𝖺-1[f, g, f]  (f  η)) = S.UP (𝗅-1[f]  𝗋[f])"
        using assms UP_triangle(3-5) by simp
      ultimately show "(ε  f)  𝖺-1[f, g, f]  (f  η) = 𝗅-1[f]  𝗋[f]"
        using UP.is_faithful by blast
    qed

    text ‹
      We \emph{really} don't want to go through the ordeal of proving a dual version of
      UP_triangle(5)›, do we?  So let's be smart and dualize via the opposite bicategory.
    ›

    lemma triangle_left_implies_right:
    assumes "(ε  f)  𝖺-1[f, g, f]  (f  η) = 𝗅-1[f]  𝗋[f]"
    shows "(g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g]"
    proof -
      interpret Cop: op_bicategory V H 𝖺 𝗂 src trg ..
      interpret Eop: equivalence_in_bicategory V Cop.H Cop.𝖺 𝗂 Cop.src Cop.trg g f η ε
        using antipar unit_in_hom counit_in_hom
        by (unfold_locales) simp_all
      have "(ε  f)  𝖺-1[f, g, f]  (f  η) = 𝗅-1[f]  𝗋[f] 
            (g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g]"
        using antipar Cop.lunit_ide_simp Cop.runit_ide_simp Cop.assoc_ide_simp
              VVV.ide_char VVV.arr_charSbC VV.arr_charSbC Eop.triangle_right_implies_left
        by simp
      thus ?thesis
        using assms by simp
    qed

    lemma triangle_left_iff_right:
    shows "(ε  f)  𝖺-1[f, g, f]  (f  η) = 𝗅-1[f]  𝗋[f] 
           (g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g]"
      using triangle_left_implies_right triangle_right_implies_left by auto

  end

  text ‹
    We might as well specialize the dual result back to the strict case while we are at it.
  ›

  context equivalence_in_strict_bicategory
  begin

    lemma triangle_left_iff_right:
    shows "(ε  f)  (f  η) = f  (g  ε)  (η  g) = g"
    proof -
      have "(ε  f)  (f  η) = f  (ε  f)  𝖺-1[f, g, f]  (f  η) = 𝗅-1[f]  𝗋[f]"
      proof -
        have "𝗅-1[f]  𝗋[f] = f"
          using strict_lunit strict_runit by simp
        moreover have "(ε  f)  𝖺-1[f, g, f]  (f  η) = (ε  f)  (f  η)"
          using antipar strict_assoc assoc'_in_hom(2) [of f g f] comp_cod_arr
          by auto
        ultimately show ?thesis by simp
      qed
      also have "...  (g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g]"
        using triangle_left_iff_right by blast
      also have "...  (g  ε)  (η  g) = g"
      proof -
        have "𝗋-1[g]  𝗅[g] = g"
          using strict_lunit strict_runit by simp
        moreover have "(g  ε)  𝖺[g, f, g]  (η  g) = (g  ε)  (η  g)"
          using antipar strict_assoc assoc_in_hom(2) [of g f g] comp_cod_arr
          by auto
        ultimately show ?thesis by simp
      qed
      finally show ?thesis by simp
    qed

  end

end