Theory InternalAdjunction

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

section "Adjunctions in a Bicategory"

theory InternalAdjunction
imports CanonicalIsos Strictness
begin

  text ‹
    An \emph{internal adjunction} in a bicategory is a four-tuple (f, g, η, ε)›,
    where f› and g› are antiparallel 1-cells and «η : src f ⇒ g ⋆ f»› and
    «ε : f ⋆ g ⇒ src g»› are 2-cells, such that the familiar ``triangle''
    (or ``zig-zag'') identities are satisfied.  We state the triangle identities
    in two equivalent forms, each of which is convenient in certain situations.
  ›

  locale adjunction_in_bicategory =
    adjunction_data_in_bicategory +
  assumes triangle_left: "(ε  f)  𝖺-1[f, g, f]  (f  η) = 𝗅-1[f]  𝗋[f]"
  and triangle_right: "(g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g]"
  begin

    lemma triangle_left':
    shows "𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f] = f"
      using triangle_left triangle_equiv_form by simp

    lemma triangle_right':
    shows "𝗋[g]  (g  ε)  𝖺[g, f, g]  (η  g)  𝗅-1[g] = g"
      using triangle_right triangle_equiv_form by simp

  end

  text ‹
    Internal adjunctions have a number of properties, which we now develop,
    that generalize those of ordinary adjunctions involving functors and
    natural transformations.
  ›

  context bicategory
  begin

    lemma adjunction_unit_determines_counit:
    assumes "adjunction_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε"
    and "adjunction_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε'"
    shows "ε = ε'"
    proof -
      interpret E: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using assms(1) by auto
      interpret E': adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε'
        using assms(2) by auto
      text ‹
        Note that since we want to prove the the result for an arbitrary bicategory,
        not just in for a strict bicategory, the calculation is a little more involved
        than one might expect from a treatment that suppresses canonical isomorphisms.
      ›
      have "ε = ε  (f  𝗋[g]  (g  ε')  𝖺[g, f, g]  (η  g)  𝗅-1[g])"
        using E'.triangle_right' comp_arr_dom by simp
      also have "... = ε  (f  𝗋[g])  (f  g  ε')  (f  𝖺[g, f, g])  (f  η  g)  (f  𝗅-1[g])"
        using E.antipar whisker_left by simp
      also have "... = ε  ((f  𝗋[g])  (f  g  ε'))  (f  𝖺[g, f, g])  (f  η  g)  (f  𝗅-1[g])"
        using comp_assoc by simp
      also have "... = ε  𝗋[f  g]  (𝖺-1[f, g, src g]  (f  g  ε')) 
                         (f  𝖺[g, f, g])  (f  η  g)  (f  𝗅-1[g])"
      proof -
        have "f  𝗋[g] = 𝗋[f  g]  𝖺-1[f, g, src g]"
          using E.antipar(1) runit_hcomp(3) by auto
        thus ?thesis
          using comp_assoc by simp
      qed
      also have "... = (ε  𝗋[f  g])  ((f  g)  ε')  𝖺-1[f, g, f  g] 
                         (f  𝖺[g, f, g])  (f  η  g)  (f  𝗅-1[g])"
          using E.antipar E'.counit_in_hom assoc'_naturality [of f g ε'] comp_assoc by simp
      also have "... = 𝗋[trg f]  ((ε  trg f)  ((f  g)  ε'))  𝖺-1[f, g, f  g] 
                         (f  𝖺[g, f, g])  (f  η  g)  (f  𝗅-1[g])"
        using E.antipar E.counit_in_hom runit_naturality [of ε] comp_assoc by simp
      also have "... = (𝗅[src g]  (src g  ε'))  (ε  f  g)  𝖺-1[f, g, f  g] 
                         (f  𝖺[g, f, g])  (f  η  g)  (f  𝗅-1[g])"
      proof -
        have "(ε  trg f)  ((f  g)  ε') = (src g  ε')  (ε  f  g)"
          using E.antipar interchange E.counit_in_hom comp_arr_dom comp_cod_arr
          by (metis E'.counit_simps(1-3) E.counit_simps(1-3))
        thus ?thesis
          using E.antipar comp_assoc unitor_coincidence by simp
      qed
      also have "... = ε'  𝗅[f  g]  (ε  f  g)  𝖺-1[f, g, f  g] 
                         (f  𝖺[g, f, g])  (f  η  g)  (f  𝗅-1[g])"
      proof -
        have "𝗅[src g]  (src g  ε') = ε'  𝗅[f  g]"
          using E.antipar lunit_naturality [of ε'] by simp
        thus ?thesis
          using comp_assoc by simp
      qed
      also have "... = ε'  (𝗅[f]  g)  (𝖺-1[trg f, f, g]  (ε  f  g))  𝖺-1[f, g, f  g] 
                         (f  𝖺[g, f, g])  (f  η  g)  (f  𝗅-1[g])"
        using E.antipar lunit_hcomp comp_assoc by simp
      also have "... = ε'  (𝗅[f]  g)  ((ε  f)  g)  (𝖺-1[f  g, f, g]  𝖺-1[f, g, f  g] 
                         (f  𝖺[g, f, g]))  (f  η  g)  (f  𝗅-1[g])"
        using E.antipar assoc'_naturality [of ε f g] comp_assoc by simp
      also have "... = ε'  (𝗅[f]  g)  ((ε  f)  g)  (𝖺-1[f, g, f]  g) 
                         (𝖺-1[f, g  f, g]  (f  η  g))  (f  𝗅-1[g])"
      proof -
        have "𝖺-1[f  g, f, g]  𝖺-1[f, g, f  g]  (f  𝖺[g, f, g]) =
              (𝖺-1[f, g, f]  g)  𝖺-1[f, g  f, g]"
          using E.antipar iso_assoc' pentagon' comp_assoc
                invert_side_of_triangle(2)
                  [of "𝖺-1[f  g, f, g]  𝖺-1[f, g, f  g]"
                      "(𝖺-1[f, g, f]  g)  𝖺-1[f, g  f, g]" "f  𝖺-1[g, f, g]"]
          by simp
        thus ?thesis
          using comp_assoc by simp
      qed
      also have "... = ε'  (𝗅[f]  g)  ((ε  f)  g)  (𝖺-1[f, g, f]  g) 
                         ((f  η)  g)  𝖺-1[f, trg g, g]  (f  𝗅-1[g])"
        using E.antipar assoc'_naturality [of f η g] comp_assoc by simp
      also have "... = ε'  (𝗅[f]  g)  ((ε  f)  g)  (𝖺-1[f, g, f]  g) 
                         ((f  η)  g)  (𝗋-1[f]  g)"
      proof -
        have "𝖺-1[f, trg g, g]  (f  𝗅-1[g]) = 𝗋-1[f]  g"
        proof -
          have "𝗋-1[f]  g = inv (𝗋[f]  g)"
            using E.antipar by simp
          also have "... = inv ((f  𝗅[g])  𝖺[f, trg g, g])"
            using E.antipar by (simp add: triangle)
          also have "... = 𝖺-1[f, trg g, g]  (f  𝗅-1[g])"
            using E.antipar inv_comp by simp
          finally show ?thesis by simp
        qed
        thus ?thesis by simp
      qed
      also have "... = ε'  (𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f]  g)"
        using E.antipar whisker_right by simp
      also have "... = ε'"
        using E.triangle_left' comp_arr_dom by simp
      finally show ?thesis by simp
    qed

  end

  subsection "Adjoint Transpose"

  context adjunction_in_bicategory
  begin

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

    text ‹
      Just as for an ordinary adjunction between categories, an adjunction in a bicategory
      determines bijections between hom-sets.  There are two versions of this relationship:
      depending on whether the transposition is occurring on the left (\emph{i.e.}~``output'')
      side or the right (\emph{i.e.}~``input'') side.
    ›

    definition trnlη
    where "trnlη v μ  (g  μ)  𝖺[g, f, v]  (η  v)  𝗅-1[v]"

    definition trnlε
    where "trnlε u ν  𝗅[u]  (ε  u)  𝖺-1[f, g, u]  (f  ν)"

    lemma adjoint_transpose_left:
    assumes "ide u" and "ide v" and "src f = trg v" and "src g = trg u"
    shows "trnlη v  hom (f  v) u  hom v (g  u)"
    and "trnlε u  hom v (g  u)  hom (f  v) u"
    and "«μ : f  v  u»  trnlε u (trnlη v μ) = μ"
    and "«ν : v  g  u»  trnlη v (trnlε u ν) = ν"
    and "bij_betw (trnlη v) (hom (f  v) u) (hom v (g  u))"
    and "bij_betw (trnlε u) (hom v (g  u)) (hom (f  v) u)"
    proof -
      show A: "trnlη v  hom (f  v) u  hom v (g  u)"
        using assms antipar trnlη_def by fastforce
      show B: "trnlε u  hom v (g  u)  hom (f  v) u"
        using assms antipar trnlε_def by fastforce
      show C: "μ. «μ : f  v  u»  trnlε u (trnlη v μ) = μ"
      proof -
        fix μ
        assume μ: "«μ : f  v  u»"
        have "trnlε u (trnlη v μ) =
              𝗅[u]  (ε  u)  𝖺-1[f, g, u]  (f  (g  μ)  𝖺[g, f, v]  (η  v)  𝗅-1[v])"
          using trnlη_def trnlε_def by simp
        also have "... = 𝗅[u]  (ε  u)  (𝖺-1[f, g, u]  (f  g  μ))  (f  𝖺[g, f, v]) 
                           (f  η  v)  (f  𝗅-1[v])"
          using assms μ antipar whisker_left comp_assoc by auto
        also have "... = 𝗅[u]  ((ε  u)  ((f  g)  μ))  𝖺-1[f, g, f  v]  (f  𝖺[g, f, v]) 
                           (f  η  v)  (f  𝗅-1[v])"
          using assms μ antipar assoc'_naturality [of f g μ] comp_assoc by fastforce
        also have "... = 𝗅[u]  (trg u  μ) 
                           (ε  f  v)  𝖺-1[f, g, f  v]  (f  𝖺[g, f, v]) 
                             (f  η  v)  (f  𝗅-1[v])"
        proof -
          have "(ε  u)  ((f  g)  μ) = (trg u  μ)  (ε  f  v)"
            using assms μ antipar comp_cod_arr comp_arr_dom
                  interchange [of "trg u" ε μ "f  v"] interchange [of ε "f  g" u μ]
            by auto
          thus ?thesis
            using comp_assoc by simp
        qed
        also have "... = 𝗅[u]  (trg u  μ)  𝖺[trg f, f, v] 
                           ((ε  f)  𝖺-1[f, g, f]  (f  η)  v) 
                             𝖺-1[f, trg v, v]  (f  𝗅-1[v])"
        proof -
          have 1: "(ε  f  v)  𝖺-1[f, g, f  v]  (f  𝖺[g, f, v])  (f  η  v) =
                   𝖺[trg f, f, v]  ((ε  f)  𝖺-1[f, g, f]  (f  η)  v)  𝖺-1[f, trg v, v]"
          proof -
            have "(ε  f  v)  𝖺-1[f, g, f  v]  (f  𝖺[g, f, v])  (f  η  v) =
                   (ε  f  v) 
                     𝖺[f  g, f, v]  (𝖺-1[f, g, f]  v)  𝖺-1[f, g  f, v] 
                       (f  η  v)"
            proof -
              have "(ε  f  v)  𝖺-1[f, g, f  v]  (f  𝖺[g, f, v])  (f  η  v) =
                    (ε  f  v)  (𝖺-1[f, g, f  v]  (f  𝖺[g, f, v]))  (f  η  v)"
                using comp_assoc by simp
              also have "... = (ε  f  v) 
                                 𝖺[f  g, f, v]  (𝖺-1[f, g, f]  v)  𝖺-1[f, g  f, v] 
                                   (f  η  v)"
              proof -
                have "𝖺-1[f, g, f  v]  (f  𝖺[g, f, v]) =
                       𝖺[f  g, f, v]  (𝖺-1[f, g, f]  v)  𝖺-1[f, g  f, v]"
                  using assms antipar canI_associator_0 whisker_can_left_0 whisker_can_right_0
                        canI_associator_hcomp(1-3)
                  by simp
                thus ?thesis
                  using comp_assoc by simp
              qed
              finally show ?thesis by blast
            qed
            also have "... = ((ε  f  v)  𝖺[f  g, f, v]) 
                               (𝖺-1[f, g, f]  v)  ((f  η)  v) 
                                 𝖺-1[f, trg v, v]"
              using assms μ antipar assoc'_naturality [of f η v] comp_assoc by simp
            also have "... = (𝖺[trg f, f, v]  ((ε  f)  v))  (𝖺-1[f, g, f]  v)  ((f  η)  v) 
                                 𝖺-1[f, trg v, v]"
              using assms μ antipar assoc_naturality [of ε f v] by simp
            also have "... = 𝖺[trg f, f, v] 
                               (((ε  f)  v)  (𝖺-1[f, g, f]  v)  ((f  η)  v)) 
                                 𝖺-1[f, trg v, v]"
              using comp_assoc by simp
            also have "... = 𝖺[trg f, f, v]  ((ε  f)  𝖺-1[f, g, f]  (f  η)  v)  𝖺-1[f, trg v, v]"
              using assms μ antipar whisker_right by simp
            finally show ?thesis by simp
          qed
          show ?thesis
            using 1 comp_assoc by metis
        qed
        also have "... = 𝗅[u]  (trg u  μ) 
                           𝖺[trg f, f, v]  (𝗅-1[f]  𝗋[f]  v)  𝖺-1[f, trg v, v]  (f  𝗅-1[v])"
          using assms μ antipar triangle_left by simp
        also have "... = 𝗅[u]  (trg u  μ)  can (trg u0  f  v) (f  v)"
          using assms μ antipar canI_unitor_0 canI_associator_1
                canI_associator_1(1-2) [of f v] whisker_can_right_0 whisker_can_left_0
          by simp
        also have "... = 𝗅[u]  (trg u  μ)  𝗅-1[f  v]"
          unfolding can_def using assms antipar comp_arr_dom comp_cod_arr 𝔩_ide_simp
          by simp
        also have "... = (𝗅[u]  𝗅-1[u])  μ"
          using assms μ lunit'_naturality [of μ] comp_assoc by auto
        also have "... = μ"
          using assms μ comp_cod_arr iso_lunit comp_arr_inv inv_is_inverse by auto
        finally show "trnlε u (trnlη v μ) = μ" by simp
      qed
      show D: "ν. «ν : v  g  u»  trnlη v (trnlε u ν) = ν"
      proof -
        fix ν
        assume ν: "«ν : v  g  u»"
        have "trnlη v (trnlε u ν) =
              (g  𝗅[u]  (ε  u)  𝖺-1[f, g, u]  (f  ν))  𝖺[g, f, v]  (η  v)  𝗅-1[v]"
          using trnlη_def trnlε_def by simp
        also have "... = (g  𝗅[u])  (g  ε  u)  (g  𝖺-1[f, g, u])  (g  f  ν) 
                           𝖺[g, f, v]  (η  v)  𝗅-1[v]"
          using assms ν antipar interchange [of g "g  g  g"] comp_assoc by auto
        also have "... = ((g  𝗅[u])  (g  ε  u)  (g  𝖺-1[f, g, u]) 
                           𝖺[g, f, g  u]  (η  g  u))  (trg v  ν)  𝗅-1[v]"
        proof -
          have "(g  f  ν)  𝖺[g, f, v]  (η  v)  𝗅-1[v] =
                𝖺[g, f, g  u]  (η  g  u)  (trg v  ν)  𝗅-1[v]"
          proof -
            have "(g  f  ν)  𝖺[g, f, v]  (η  v)  𝗅-1[v] =
                  𝖺[g, f, g  u]  ((g  f)  ν)  (η  v)  𝗅-1[v]"
            proof -
              have "(g  f  ν)  𝖺[g, f, v] = 𝖺[g, f, g  u]  ((g  f)  ν)"
                using assms ν antipar assoc_naturality [of g f ν] by auto
              thus ?thesis
                using assms comp_assoc by metis
            qed
            also have "... = 𝖺[g, f, g  u]  (η  g  u)  (trg v  ν)  𝗅-1[v]"
            proof -
              have "((g  f)  ν)  (η  v) = (η  g  u)  (trg v  ν)"
                using assms ν antipar comp_arr_dom comp_cod_arr
                      interchange [of "g  f" η ν v] interchange [of η "trg v" "g  u" ν]
                by auto
              thus ?thesis
                using comp_assoc by metis
            qed
            finally show ?thesis by blast
          qed
          thus ?thesis using comp_assoc by simp
        qed
        also have "... = 𝗅[g  u]  (trg v  ν)  𝗅-1[v]"
        proof -
          have "(g  𝗅[u])  (g  ε  u)  (g  𝖺-1[f, g, u])  𝖺[g, f, g  u]  (η  g  u) =
                𝗅[g  u]"
          proof -
            have "(g  𝗅[u])  (g  ε  u)  (g  𝖺-1[f, g, u])  𝖺[g, f, g  u]  (η  g  u) =
                  (g  𝗅[u])  𝖺[g, trg u, u] 
                     ((g  ε)  𝖺[g, f, g]  (η  g)  u) 
                        𝖺-1[trg v, g, u]"
            proof -
              have "(g  𝗅[u])  (g  ε  u)  (g  𝖺-1[f, g, u])  𝖺[g, f, g  u]  (η  g  u) =
                    (g  𝗅[u])  (g  ε  u)  (g  𝖺-1[f, g, u])  𝖺[g, f, g  u] 
                       ((η  g  u)  𝖺[trg v, g, u])  𝖺-1[trg v, g, u]"
                using assms antipar comp_arr_dom comp_assoc comp_assoc_assoc'(1) by simp
              also have "... = (g  𝗅[u])  (g  ε  u)  (g  𝖺-1[f, g, u])  𝖺[g, f, g  u] 
                                 (𝖺[g  f, g, u]  ((η  g)  u))  𝖺-1[trg v, g, u]"
                using assms antipar assoc_naturality [of η g u] by simp
              also have "... = (g  𝗅[u])  (g  ε  u) 
                                 ((g  𝖺-1[f, g, u])  𝖺[g, f, g  u]  𝖺[g  f, g, u]) 
                                   ((η  g)  u)  𝖺-1[trg v, g, u]"
                using comp_assoc by simp
              also have "... = (g  𝗅[u])  ((𝖺[g, trg u, u]  𝖺-1[g, trg u, u])  (g  ε  u)) 
                                 ((g  𝖺-1[f, g, u])  𝖺[g, f, g  u]  𝖺[g  f, g, u]) 
                                   ((η  g)  u)  𝖺-1[trg v, g, u]"
              proof -
                have "(𝖺[g, trg u, u]  𝖺-1[g, trg u, u])  (g  ε  u) = g  ε  u"
                  using assms antipar comp_cod_arr comp_assoc_assoc'(1) by simp
                thus ?thesis
                  using comp_assoc by simp
              qed
              also have "... = (g  𝗅[u])  𝖺[g, trg u, u]  (𝖺-1[g, trg u, u]  (g  ε  u)) 
                                 (g  𝖺-1[f, g, u])  𝖺[g, f, g  u]  𝖺[g  f, g, u] 
                                   ((η  g)  u)  𝖺-1[trg v, g, u]"
                using comp_assoc by simp
              also have "... = (g  𝗅[u])  𝖺[g, trg u, u]  (((g  ε)  u)  (𝖺-1[g, f  g, u] 
                                 (g  𝖺-1[f, g, u])  𝖺[g, f, g  u]  𝖺[g  f, g, u]) 
                                   ((η  g)  u))  𝖺-1[trg v, g, u]"
                using assms antipar assoc'_naturality [of g ε u] comp_assoc by simp
              also have "... = (g  𝗅[u])  𝖺[g, trg u, u] 
                                 ((g  ε)  𝖺[g, f, g]  (η  g)  u) 
                                   𝖺-1[trg v, g, u]"
              proof -
                have "𝖺-1[g, f  g, u]  (g  𝖺-1[f, g, u])  𝖺[g, f, g  u]  𝖺[g  f, g, u] =
                      𝖺[g, f, g]  u"
                  using assms antipar canI_associator_0 whisker_can_left_0 whisker_can_right_0
                        canI_associator_hcomp
                  by simp
                hence "((g  ε)  u) 
                          (𝖺-1[g, f  g, u]  (g  𝖺-1[f, g, u])  𝖺[g, f, g  u]  𝖺[g  f, g, u]) 
                             ((η  g)  u) =
                       (g  ε)  𝖺[g, f, g]  (η  g)  u"
                  using assms antipar whisker_right by simp
                thus ?thesis by simp
              qed
              finally show ?thesis by blast
            qed
            also have "... = (g  𝗅[u])  𝖺[g, trg u, u]  (𝗋-1[g]  𝗅[g]  u)  𝖺-1[trg g, g, u]"
              using assms antipar triangle_right by simp
            also have "... = can (g  u) (trg g0  g  u)"
            proof -
              have "(g  𝗅[u])  𝖺[g, trg u, u]  (𝗋-1[g]  𝗅[g]  u)  𝖺-1[trg g, g, u] =
                    ((g  𝗅[u])  𝖺[g, trg u, u]  (𝗋-1[g]  𝗅[g]  u)  𝖺-1[trg g, g, u])"
                using comp_assoc by simp
              moreover have "... = can (g  u) (trg g0  g  u)"
                using assms antipar canI_unitor_0 canI_associator_1 [of g u] inv_can
                  whisker_can_left_0 whisker_can_right_0
                by simp
              ultimately show ?thesis by simp
            qed
            also have "... = 𝗅[g  u]"
              unfolding can_def using assms comp_arr_dom comp_cod_arr 𝔩_ide_simp by simp
            finally show ?thesis by simp
          qed
          thus ?thesis by simp
        qed
        also have "... = (𝗅[g  u]  𝗅-1[g  u])  ν"
          using assms ν lunit'_naturality comp_assoc by auto
        also have "... = ν"
          using assms ν comp_cod_arr iso_lunit comp_arr_inv inv_is_inverse by auto
        finally show "trnlη v (trnlε u ν) = ν" by simp
      qed
      show "bij_betw (trnlη v) (hom (f  v) u) (hom v (g  u))"
        using A B C D by (intro bij_betwI) auto
      show "bij_betw (trnlε u) (hom v (g  u)) (hom (f  v) u)"
        using A B C D by (intro bij_betwI) auto
    qed

    lemma trnlε_comp:
    assumes "ide u" and "seq μ ν" and "src f = trg μ"
    shows "trnlε u (μ  ν) = trnlε u μ  (f  ν)"
      using assms trnlε_def whisker_left [of f μ ν] comp_assoc by auto

    definition trnrη
    where "trnrη v μ  (μ  f)  𝖺-1[v, g, f]  (v  η)  𝗋-1[v]"

    definition trnrε
    where "trnrε u ν  𝗋[u]  (u  ε)  𝖺[u, f, g]  (ν  g)"

    lemma adjoint_transpose_right:
    assumes "ide u" and "ide v" and "src v = trg g" and "src u = trg f"
    shows "trnrη v  hom (v  g) u  hom v (u  f)"
    and "trnrε u  hom v (u  f)  hom (v  g) u"
    and "«μ : v  g  u»  trnrε u (trnrη v μ) = μ"
    and "«ν : v  u  f»  trnrη v (trnrε u ν) = ν"
    and "bij_betw (trnrη v) (hom (v  g) u) (hom v (u  f))"
    and "bij_betw (trnrε u) (hom v (u  f)) (hom (v  g) u)"
    proof -
      show A: "trnrη v  hom (v  g) u  hom v (u  f)"
        using assms antipar trnrη_def by fastforce
      show B: "trnrε u  hom v (u  f)  hom (v  g) u"
        using assms antipar trnrε_def by fastforce
      show C: "μ. «μ : v  g  u»  trnrε u (trnrη v μ) = μ"
      proof -
        fix μ
        assume μ: "«μ : v  g  u»"
        have "trnrε u (trnrη v μ) =
              𝗋[u]  (u  ε)  𝖺[u, f, g]  ((μ  f)  𝖺-1[v, g, f]  (v  η)  𝗋-1[v]  g)"
          unfolding trnrε_def trnrη_def by simp
        also have "... = 𝗋[u]  (u  ε)  (𝖺[u, f, g]  ((μ  f)  g)) 
                           (𝖺-1[v, g, f]  g)  ((v  η)  g)  (𝗋-1[v]  g)"
          using assms μ antipar whisker_right comp_assoc by auto
        also have "... = 𝗋[u]  (u  ε)  ((μ  f  g)  𝖺[v  g, f, g]) 
                           (𝖺-1[v, g, f]  g)  ((v  η)  g)  (𝗋-1[v]  g)"
          using assms μ antipar assoc_naturality [of μ f g] by auto
        also have "... = 𝗋[u]  ((u  ε)  (μ  f  g))  𝖺[v  g, f, g] 
                           (𝖺-1[v, g, f]  g)  ((v  η)  g)  (𝗋-1[v]  g)"
          using comp_assoc by auto
        also have "... = 𝗋[u]  (μ  src u)  ((v  g)  ε)  𝖺[v  g, f, g] 
                           (𝖺-1[v, g, f]  g)  ((v  η)  g)  (𝗋-1[v]  g)"
        proof -
          have "(u  ε)  (μ  f  g) = (μ  src u)  ((v  g)  ε)"
            using assms μ antipar comp_arr_dom comp_cod_arr
                  interchange [of μ "v  g" "src u" ε] interchange [of u μ ε "f  g"]
            by auto
          thus ?thesis
            using comp_assoc by simp
        qed
        also have "... = 𝗋[u]  (μ  src u) 
                           (((v  g)  ε)  𝖺[v  g, f, g]  (𝖺-1[v, g, f]  g)  ((v  η)  g)) 
                             (𝗋-1[v]  g)"
          using comp_assoc by simp
        also have "... = 𝗋[u]  (μ  src u) 
                           (𝖺-1[v, g, src u]  (v  (g  ε)  𝖺[g, f, g]  (η  g)) 
                             𝖺[v, src v, g])  (𝗋-1[v]  g)"
        proof -
          have "((v  g)  ε)  𝖺[v  g, f, g]  (𝖺-1[v, g, f]  g)  ((v  η)  g) =
                  𝖺-1[v, g, src u]  (v  (g  ε)  𝖺[g, f, g]  (η  g))  𝖺[v, src v, g]"
          proof -
            have "((v  g)  ε)  𝖺[v  g, f, g]  (𝖺-1[v, g, f]  g)  ((v  η)  g) =
                    ((𝖺-1[v, g, src u]  𝖺[v, g, src u])  ((v  g)  ε)) 
                      𝖺[v  g, f, g]  (𝖺-1[v, g, f]  g)  ((v  η)  g)"
            proof -
              have "arr v  dom v = v  cod v = v"
                using assms(2) ide_char by blast
              moreover have "arr g  dom g = g  cod g = g"
                using ide_right ide_char by blast
              ultimately show ?thesis
                by (metis (no_types) antipar(2) assms(3-4) assoc_naturality
                    counit_simps(1,3,5) hcomp_reassoc(1) comp_assoc)
            qed
            also have "... = 𝖺-1[v, g, src u]  (𝖺[v, g, src u]  ((v  g)  ε)) 
                               𝖺[v  g, f, g]  (𝖺-1[v, g, f]  g)  ((v  η)  g)"
              using comp_assoc by simp
            also have "... = 𝖺-1[v, g, src u]  ((v  g  ε)  𝖺[v, g, f  g]) 
                               𝖺[v  g, f, g]  (𝖺-1[v, g, f]  g) 
                                 (𝖺-1[v, g  f, g]  𝖺[v, g  f, g])  ((v  η)  g)"
            proof -
              have "𝖺[v, g, src u]  ((v  g)  ε) = (v  g  ε)  𝖺[v, g, f  g]"
                using assms antipar assoc_naturality [of v g ε] by simp
              moreover have "(𝖺-1[v, g  f, g]  𝖺[v, g  f, g])  ((v  η)  g) = (v  η)  g"
                using assms antipar comp_cod_arr comp_assoc_assoc'(2) by simp
              ultimately show ?thesis by simp
            qed
            also have "... = 𝖺-1[v, g, src u]  (v  g  ε) 
                               𝖺[v, g, f  g]  𝖺[v  g, f, g]  (𝖺-1[v, g, f]  g) 
                                 𝖺-1[v, g  f, g]  𝖺[v, g  f, g]  ((v  η)  g)"
              using comp_assoc by simp
            also have "... = 𝖺-1[v, g, src u]  ((v  g  ε) 
                               (𝖺[v, g, f  g]  𝖺[v  g, f, g]  (𝖺-1[v, g, f]  g) 
                                 𝖺-1[v, g  f, g])  (v  η  g))  𝖺[v, src v, g]"
              using assms antipar assoc_naturality [of v η g] comp_assoc by simp
            also have "... = 𝖺-1[v, g, src u] 
                               ((v  g  ε)  (v  𝖺[g, f, g])  (v  η  g)) 
                                 𝖺[v, src v, g]"
            proof -
              have "𝖺[v, g, f  g]  𝖺[v  g, f, g]  (𝖺-1[v, g, f]  g)  𝖺-1[v, g  f, g] =
                    v  𝖺[g, f, g]"
                using assms antipar canI_associator_0 canI_associator_hcomp
                      whisker_can_left_0 whisker_can_right_0
                by simp
              thus ?thesis
                using assms antipar whisker_left by simp
            qed
            also have "... = 𝖺-1[v, g, src u] 
                               (v  (g  ε)  𝖺[g, f, g]  (η  g)) 
                                 𝖺[v, src v, g]"
              using assms antipar whisker_left by simp
            finally show ?thesis by simp
          qed
          thus ?thesis by auto
        qed
        also have "... = 𝗋[u]  (μ  src u) 
                          𝖺-1[v, g, src u]  (v  𝗋-1[g]  𝗅[g]) 
                            𝖺[v, src v, g]  (𝗋-1[v]  g)"
              using triangle_right comp_assoc by simp
        also have "... = 𝗋[u]  (μ  src u)  𝗋-1[v  g]"
        proof -
          have "𝖺-1[v, g, src u]  (v  𝗋-1[g]  𝗅[g])  𝖺[v, src v, g]  (𝗋-1[v]  g) = 𝗋-1[v  g]"
          proof -
            have "𝖺-1[v, g, src u]  (v  𝗋-1[g]  𝗅[g])  𝖺[v, src v, g]  (𝗋-1[v]  g) =
                  𝖺-1[v, g, trg f]  can (v  g  src g0) (v  g)"
              using assms canI_unitor_0 canI_associator_1(2-3) whisker_can_left_0(1)
                whisker_can_right_0
              by simp
            also have "... = 𝖺-1[v, g, src g]  can (v  g  src g0) (v  g)"
              using antipar by simp
            (* TODO: There should be an alternate version of whisker_can_left for this. *)
            also have "... = 𝖺-1[v, g, src g]  (v  can (g  src g0) g)"
              using assms canI_unitor_0(2) whisker_can_left_0 by simp
            also have "... = 𝖺-1[v, g, src g]  (v  𝗋-1[g])"
              using assms canI_unitor_0(2) by simp
            also have "... = 𝗋-1[v  g]"
              using assms runit_hcomp(2) by simp
            finally have "𝖺-1[v, g, src u]  (v  𝗋-1[g]  𝗅[g])  𝖺[v, src v, g]  (𝗋-1[v]  g) =
                          𝗋-1[v  g]"
              by simp
            thus ?thesis by simp
          qed
          thus ?thesis by simp
        qed
        also have "... = (𝗋[u]  𝗋-1[u])  μ"
          using assms μ runit'_naturality [of μ] comp_assoc by auto
        also have "... = μ"
          using μ comp_cod_arr iso_runit inv_is_inverse comp_arr_inv by auto
        finally show "trnrε u (trnrη v μ) = μ" by simp
      qed
      show D: "ν. «ν : v  u  f»  trnrη v (trnrε u ν) = ν"
      proof -
        fix ν
        assume ν: "«ν : v  u  f»"
        have "trnrη v (trnrε u ν) =
              (𝗋[u]  (u  ε)  𝖺[u, f, g]  (ν  g)  f)  𝖺-1[v, g, f]  (v  η)  𝗋-1[v]"
          unfolding trnrη_def trnrε_def by simp
        also have "... = (𝗋[u]  f)  ((u  ε)  f)  (𝖺[u, f, g]  f) 
                          (((ν  g)  f)  𝖺-1[v, g, f])  (v  η)  𝗋-1[v]"
          using assms ν antipar whisker_right comp_assoc by auto
        also have "... = (𝗋[u]  f)  ((u  ε)  f)  (𝖺[u, f, g]  f) 
                          (𝖺-1[u  f, g, f]  (ν  g  f))  (v  η)  𝗋-1[v]"
          using assms ν antipar assoc'_naturality [of ν g f] by auto
        also have "... = (𝗋[u]  f)  ((u  ε)  f)  (𝖺[u, f, g]  f) 
                          𝖺-1[u  f, g, f]  ((ν  g  f)  (v  η))  𝗋-1[v]"
          using comp_assoc by simp
        also have "... = (𝗋[u]  f)  ((u  ε)  f)  (𝖺[u, f, g]  f) 
                          𝖺-1[u  f, g, f]  (((u  f)  η)  (ν  src v))  𝗋-1[v]"
        proof -
          have "(ν  g  f)  (v  η) = ((u  f)  η)  (ν  src v)"
            using assms ν antipar interchange [of "u  f" ν η "src v"]
                  interchange [of ν v "g  f" η] comp_arr_dom comp_cod_arr
            by auto
          thus ?thesis by simp
        qed
        also have "... = ((𝗋[u]  f)  ((u  ε)  f) 
                           ((𝖺[u, f, g]  f)  𝖺-1[u  f, g, f]) 
                             ((u  f)  η))  (ν  src v)  𝗋-1[v]"
          using comp_assoc by simp
        also have "... = ((𝗋[u]  f)  ((u  ε)  f) 
                           (𝖺-1[u, f  g, f]  (u  𝖺-1[f, g, f])  𝖺[u, f, g  f]) 
                             ((u  f)  η))  (ν  src v)  𝗋-1[v]"
          using assms antipar canI_associator_hcomp canI_associator_0 whisker_can_left_0
                whisker_can_right_0
          by simp
        also have "... = ((𝗋[u]  f)  (((u  ε)  f) 
                           𝖺-1[u, f  g, f])  (u  𝖺-1[f, g, f])  (𝖺[u, f, g  f]) 
                             ((u  f)  η))  (ν  src v)  𝗋-1[v]"
          using comp_assoc by simp
        also have "... = ((𝗋[u]  f)  (𝖺-1[u, src u, f]  (u  ε  f)) 
                           (u  𝖺-1[f, g, f])  ((u  f  η)  𝖺[u, f, src f])) 
                             (ν  src v)  𝗋-1[v]"
          using assms antipar assoc'_naturality [of u ε f] assoc_naturality [of u f η]
          by auto
        also have "... = (𝗋[u]  f)  𝖺-1[u, src u, f] 
                           ((u  ε  f)  (u  𝖺-1[f, g, f])  (u  f  η))  𝖺[u, f, src f] 
                             (ν  src v)  𝗋-1[v]"
          using comp_assoc by simp
        also have "... = (𝗋[u]  f)  𝖺-1[u, src u, f] 
                           (u  (ε  f)  𝖺-1[f, g, f]  (f  η))  𝖺[u, f, src f] 
                             (ν  src v)  𝗋-1[v]"
          using assms antipar whisker_left by auto
        also have "... = ((𝗋[u]  f)  (𝖺-1[u, src u, f]  (u  𝗅-1[f]  𝗋[f])  𝖺[u, f, src f])) 
                           (ν  src v)  𝗋-1[v]"
          using assms antipar triangle_left comp_assoc by simp
        also have "... = 𝗋[u  f]  (ν  src v)  𝗋-1[v]"
        proof -
          have "(𝗋[u]  f)  𝖺-1[u, src u, f]  (u  𝗅-1[f]  𝗋[f])  𝖺[u, f, src f] =
                ((u  𝗅[f])  (𝖺[u, src u, f]  𝖺-1[u, src u, f])) 
                  (u  𝗅-1[f]  𝗋[f])  𝖺[u, f, src f]"
            using assms ide_left ide_right antipar triangle comp_assoc by metis
          also have "... = (u  𝗋[f])  𝖺[u, f, src f]"
            using assms antipar canI_associator_1 canI_unitor_0 whisker_can_left_0
                  whisker_can_right_0 canI_associator_1
            by simp
          also have "... = 𝗋[u  f]"
            using assms antipar runit_hcomp by simp
          finally show ?thesis by simp
        qed
        also have "... = (𝗋[u  f]  𝗋-1[u  f])  ν"
          using assms ν runit'_naturality [of ν] comp_assoc by auto
        also have "... = ν"
          using assms ν comp_cod_arr comp_arr_inv inv_is_inverse iso_runit by auto
        finally show "trnrη v (trnrε u ν) = ν" by auto
      qed
      show "bij_betw (trnrη v) (hom (v  g) u) (hom v (u  f))"
        using A B C D by (intro bij_betwI, auto)
      show "bij_betw (trnrε u) (hom v (u  f)) (hom (v  g) u)"
        using A B C D by (intro bij_betwI, auto)
    qed

    lemma trnrη_comp:
    assumes "ide v" and "seq μ ν" and "src μ = trg f"
    shows "trnrη v (μ  ν) = (μ  f)  trnrη v ν"
      using assms trnrη_def whisker_right comp_assoc by auto

  end

  text ‹
    It is useful to have at hand the simpler versions of the preceding results that
    hold in a normal bicategory and in a strict bicategory.
  ›

  locale adjunction_in_normal_bicategory =
    normal_bicategory +
    adjunction_in_bicategory
  begin

    lemma triangle_left:
    shows "(ε  f)  𝖺-1[f, g, f]  (f  η) = f"
      using triangle_left strict_lunit strict_runit by simp

    lemma triangle_right:
    shows "(g  ε)  𝖺[g, f, g]  (η  g) = g"
      using triangle_right strict_lunit strict_runit by simp

    lemma trnrη_eq:
    assumes "ide u" and "ide v"
    and "src v = trg g" and "src u = trg f"
    and "μ  hom (v  g) u"
    shows "trnrη v μ = (μ  f)  𝖺-1[v, g, f]  (v  η)"
      unfolding trnrη_def
      using assms antipar strict_runit' comp_arr_ide [of "𝗋-1[v]" "v  η"] hcomp_arr_obj
      by auto

    lemma trnrε_eq:
    assumes "ide u" and "ide v"
    and "src v = trg g" and "src u = trg f"
    and "ν  hom v (u  f)"
    shows "trnrε u ν = (u  ε)  𝖺[u, f, g]  (ν  g)"
      unfolding trnrε_def
      using assms antipar strict_runit comp_ide_arr hcomp_arr_obj by auto

    lemma trnlη_eq:
    assumes "ide u" and "ide v"
    and "src f = trg v" and "src g = trg u"
    and "μ  hom (f  v) u"
    shows "trnlη v μ = (g  μ)  𝖺[g, f, v]  (η  v)"
      using assms trnlη_def antipar strict_lunit comp_arr_dom hcomp_obj_arr by auto

    lemma trnlε_eq:
    assumes "ide u" and "ide v"
    and "src f = trg v" and "src g = trg u"
    and "ν  hom v (g  u)"
    shows "trnlε u ν = (ε  u)  𝖺-1[f, g, u]  (f  ν)"
      using assms trnlε_def antipar strict_lunit comp_cod_arr hcomp_obj_arr by auto

  end

  locale adjunction_in_strict_bicategory =
    strict_bicategory +
    adjunction_in_normal_bicategory
  begin

    lemma triangle_left:
    shows "(ε  f)  (f  η) = f"
      using ide_left ide_right antipar triangle_left strict_assoc' comp_cod_arr
      by (metis dom_eqI ideD(1) seqE)

    lemma triangle_right:
    shows "(g  ε)  (η  g) = g"
      using ide_left ide_right antipar triangle_right strict_assoc comp_cod_arr
      by (metis ideD(1) ideD(2) seqE)

    lemma trnrη_eq:
    assumes "ide u" and "ide v"
    and "src v = trg g" and "src u = trg f"
    and "μ  hom (v  g) u"
    shows "trnrη v μ = (μ  f)  (v  η)"
      using assms antipar trnrη_eq strict_assoc' comp_ide_arr [of "𝖺-1[v, g, f]" "v  η"]
      by force

    lemma trnrε_eq:
    assumes "ide u" and "ide v"
    and "src v = trg g" and "src u = trg f"
    and "ν  hom v (u  f)"
    shows "trnrε u ν = (u  ε)  (ν  g)"
      using assms antipar trnrε_eq strict_assoc comp_ide_arr [of "𝖺[u, f, g]" "ν  g"]
      by force

    lemma trnlη_eq:
    assumes "ide u" and "ide v"
    and "src f = trg v" and "src g = trg u"
    and "μ  hom (f  v) u"
    shows "trnlη v μ = (g  μ)  (η  v)"
      using assms antipar trnlη_eq strict_assoc comp_ide_arr [of "𝖺[g, f, v]" "η  v"]
      by force

    lemma trnlε_eq:
    assumes "ide u" and "ide v"
    and "src f = trg v" and "src g = trg u"
    and "ν  hom v (g  u)"
    shows "trnlε u ν = (ε  u)  (f  ν)"
      using assms antipar trnlε_eq strict_assoc' comp_ide_arr [of "𝖺-1[f, g, u]" "f  ν"]
      by fastforce

  end

  subsection "Preservation Properties for Adjunctions"

  text ‹
    Here we show that adjunctions are preserved under isomorphisms of the
    left and right adjoints.
  ›

  context bicategory
  begin

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

    definition adjoint_pair
    where "adjoint_pair f g  η ε. adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"

    (* These would normally be called "maps", but that name is too heavily used already. *)
    abbreviation is_left_adjoint
    where "is_left_adjoint f  g. adjoint_pair f g"

    abbreviation is_right_adjoint
    where "is_right_adjoint g  f. adjoint_pair f g"

    lemma adjoint_pair_antipar:
    assumes "adjoint_pair f g"
    shows "ide f" and "ide g" and "src f = trg g" and "src g = trg f"
    proof -
      obtain η ε where A: "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
        using assms adjoint_pair_def by auto
      interpret A: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using A by auto
      show "ide f" by simp
      show "ide g" by simp
      show "src f = trg g" using A.antipar by simp
      show "src g = trg f" using A.antipar by simp
    qed

    lemma left_adjoint_is_ide:
    assumes "is_left_adjoint f"
    shows "ide f"
      using assms adjoint_pair_antipar by auto

    lemma right_adjoint_is_ide:
    assumes "is_right_adjoint f"
    shows "ide f"
      using assms adjoint_pair_antipar by auto

    lemma adjunction_preserved_by_iso_right:
    assumes "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
    and "«φ : g  g'»" and "iso φ"
    shows "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g' ((φ  f)  η) (ε  (f  inv φ))"
    proof
      interpret A: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using assms by auto
      show "ide f" by simp
      show "ide g'"
        using assms(2) isomorphic_def by auto
      show "«(φ  f)  η : src f  g'  f»"
        using assms A.antipar by fastforce
      show "«ε  (f  inv φ) : f  g'  src g'»"
        using assms A.antipar A.counit_in_hom by auto
      show "(ε  (f  inv φ)  f)  𝖺-1[f, g', f]  (f  (φ  f)  η) = 𝗅-1[f]  𝗋[f]"
      proof -
        have "(ε  (f  inv φ)  f)  𝖺-1[f, g', f]  (f  (φ  f)  η) =
              (ε  f)  (((f  inv φ)  f)  𝖺-1[f, g', f])  (f  φ  f)  (f  η)"
          using assms A.antipar whisker_right whisker_left comp_assoc by auto
        also have "... = (ε  f)  (𝖺-1[f, g, f]  (f  inv φ  f))  (f  φ  f)  (f  η)"
          using assms A.antipar assoc'_naturality [of f "inv φ" f] by auto
        also have "... = (ε  f)  𝖺-1[f, g, f]  ((f  inv φ  f)  (f  φ  f))  (f  η)"
          using comp_assoc by simp
        also have "... = (ε  f)  𝖺-1[f, g, f]  (f  g  f)  (f  η)"
          using assms A.antipar comp_inv_arr inv_is_inverse whisker_left
                whisker_right [of f "inv φ" φ]
          by auto
        also have "... = (ε  f)  𝖺-1[f, g, f]  (f  η)"
          using assms A.antipar comp_cod_arr by simp
        also have "... = 𝗅-1[f]  𝗋[f]"
          using A.triangle_left by simp
        finally show ?thesis by simp
      qed
      show "(g'  ε  (f  inv φ))  𝖺[g', f, g']  ((φ  f)  η  g') = 𝗋-1[g']  𝗅[g']"
      proof -
        have "(g'  ε  (f  inv φ))  𝖺[g', f, g']  ((φ  f)  η  g') =
              (g'  ε)  ((g'  f  inv φ)  𝖺[g', f, g'])  ((φ  f)  g')  (η  g')"
            using assms A.antipar whisker_left whisker_right comp_assoc by auto
        also have "... = (g'  ε)  (𝖺[g', f, g]  ((g'  f)  inv φ))  ((φ  f)  g')  (η  g')"
          using assms A.antipar assoc_naturality [of g' f "inv φ"] by auto
        also have "... = (g'  ε)  𝖺[g', f, g]  (((g'  f)  inv φ)  ((φ  f)  g'))  (η  g')"
          using comp_assoc by simp
        also have "... = (g'  ε)  (𝖺[g', f, g]  ((φ  f)  g))  ((g  f)  inv φ)  (η  g')"
        proof -
          have "((g'  f)  inv φ)  ((φ  f)  g') = (φ  f)  inv φ"
            using assms A.antipar comp_arr_dom comp_cod_arr
                  interchange [of "g'  f" "φ  f" "inv φ" g']
            by auto
          also have "... = ((φ  f)  g)  ((g  f)  inv φ)"
            using assms A.antipar comp_arr_dom comp_cod_arr
                  interchange [of "φ  f" "g  f" g "inv φ"]
            by auto
          finally show ?thesis
            using comp_assoc by simp
        qed
        also have "... = ((g'  ε)  (φ  f  g))  𝖺[g, f, g]  (η  g)  (trg g  inv φ)"
        proof -
          have "𝖺[g', f, g]  ((φ  f)  g) = (φ  f  g)  𝖺[g, f, g]"
            using assms A.antipar assoc_naturality [of φ f g] by auto
          moreover have "((g  f)  inv φ)  (η  g') = (η  g)  (trg g  inv φ)"
            using assms A.antipar comp_arr_dom comp_cod_arr
                  interchange [of "g  f" η "inv φ" g'] interchange [of η "trg g" g "inv φ"]
            by auto
          ultimately show ?thesis
            using comp_assoc by simp
        qed
        also have "... = ((φ  src g)  (g  ε))  𝖺[g, f, g]  (η  g)  (trg g  inv φ)"
          using assms A.antipar comp_arr_dom comp_cod_arr
                interchange [of g' φ ε "f  g"] interchange [of φ g "src g" ε]
          by (metis A.counit_simps(1) A.counit_simps(2) A.counit_simps(3) in_homE)
        also have "... = (φ  src g)  ((g  ε)  𝖺[g, f, g]  (η  g))  (trg g  inv φ)"
          using comp_assoc by simp
        also have "... = ((φ  src g)  𝗋-1[g])  𝗅[g]  (trg g  inv φ)"
          using assms A.antipar A.triangle_right comp_cod_arr comp_assoc
          by simp
        also have "... = (𝗋-1[g']  φ)  inv φ  𝗅[g']"
          using assms A.antipar runit'_naturality [of φ] lunit_naturality [of "inv φ"]
          by auto
        also have "... = 𝗋-1[g']  (φ  inv φ)  𝗅[g']"
          using comp_assoc by simp
        also have "... = 𝗋-1[g']  𝗅[g']"
          using assms comp_cod_arr comp_arr_inv' by auto
        finally show ?thesis by simp
      qed
    qed

    lemma adjunction_preserved_by_iso_left:
    assumes "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
    and "«φ : f  f'»" and "iso φ"
    shows "adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g ((g  φ)  η) (ε  (inv φ  g))"
    proof
      interpret A: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using assms by auto
      show "ide g" by simp
      show "ide f'"
        using assms(2) isomorphic_def by auto
      show "«(g  φ)  η : src f'  g  f'»"
        using assms A.antipar A.unit_in_hom by force
      show "«ε  (inv φ  g) : f'  g  src g»"
        using assms A.antipar by force
      show "(g  ε  (inv φ  g))  𝖺[g, f', g]  ((g  φ)  η  g) = 𝗋-1[g]  𝗅[g]"
      proof -
        have "(g  ε  (inv φ  g))  𝖺[g, f', g]  ((g  φ)  η  g) =
              (g  ε)  ((g  inv φ  g)  𝖺[g, f', g])  ((g  φ)  g)  (η  g)"
          using assms A.antipar whisker_left whisker_right comp_assoc by auto
        also have "... = (g  ε)  (𝖺[g, f, g]  ((g  inv φ)  g))  ((g  φ)  g)  (η  g)"
          using assms A.antipar assoc_naturality [of g "inv φ" g] by auto
        also have "... = (g  ε)  𝖺[g, f, g]  (((g  inv φ)  g)  ((g  φ)  g))  (η  g)"
          using comp_assoc by simp
        also have "... = (g  ε)  𝖺[g, f, g]  ((g  f)  g)  (η  g)"
          using assms A.antipar comp_inv_arr inv_is_inverse whisker_right
                whisker_left [of g "inv φ" φ]
          by auto
        also have "... = (g  ε)  𝖺[g, f, g]  (η  g)"
          using assms A.antipar comp_cod_arr by simp
        also have "... = 𝗋-1[g]  𝗅[g]"
          using A.triangle_right by simp
        finally show ?thesis by simp
      qed
      show "(ε  (inv φ  g)  f')  𝖺-1[f', g, f']  (f'  (g  φ)  η) = 𝗅-1[f']  𝗋[f']"
      proof -
        have "(ε  (inv φ  g)  f')  𝖺-1[f', g, f']  (f'  (g  φ)  η) =
              (ε  f')  (((inv φ  g)  f')  𝖺-1[f', g, f'])  (f'  g  φ)  (f'  η)"
          using assms A.antipar whisker_right whisker_left comp_assoc
          by auto
        also have "... = (ε  f')  (𝖺-1[f, g, f']  (inv φ  g  f'))  (f'  g  φ)  (f'  η)"
          using assms A.antipar assoc'_naturality [of "inv φ" g f'] by auto
        also have "... = (ε  f')  𝖺-1[f, g, f']  ((inv φ  g  f')  (f'  g  φ))  (f'  η)"
          using comp_assoc by simp
        also have "... = (ε  f')  (𝖺-1[f, g, f']  (f  g  φ))  (inv φ  g  f)  (f'  η)"
        proof -
          have "(inv φ  g  f')  (f'  g  φ) = (f  g  φ)  (inv φ  g  f)"
            using assms(2-3) A.antipar comp_arr_dom comp_cod_arr
                  interchange [of "inv φ" f' "g  f'" "g  φ"]
                  interchange [of f "inv φ" "g  φ" "g  f"]
            by auto
          thus ?thesis
            using comp_assoc by simp
        qed
        also have "... = ((ε  f')  ((f  g)  φ))  𝖺-1[f, g, f]  (f  η)  (inv φ  src f)"
        proof -
          have "𝖺-1[f, g, f']  (f  g  φ) = ((f  g)  φ)  𝖺-1[f, g, f]"
            using assms A.antipar assoc'_naturality [of f g φ] by auto
          moreover have "(inv φ  g  f)  (f'  η) = (f  η)  (inv φ  src f)"
            using assms A.antipar comp_arr_dom comp_cod_arr
                  interchange [of "inv φ" f' "g  f" η] interchange [of f "inv φ" η "src f"]
            by auto
          ultimately show ?thesis
            using comp_assoc by simp
        qed
        also have "... = ((trg f  φ)  (ε  f))  𝖺-1[f, g, f]  (f  η)  (inv φ  src f)"
          using assms A.antipar comp_arr_dom comp_cod_arr
                interchange [of ε "f  g" f' φ] interchange [of "trg f" ε φ f]
          by (metis A.counit_simps(1) A.counit_simps(2) A.counit_simps(3) in_homE)
        also have "... = (trg f  φ)  ((ε  f)  𝖺-1[f, g, f]  (f  η))  (inv φ  src f)"
          using comp_assoc by simp
        also have "... = ((trg f  φ)  𝗅-1[f])  𝗋[f]  (inv φ  src f)"
          using assms A.antipar A.triangle_left comp_cod_arr comp_assoc
          by simp
        also have "... = (𝗅-1[f']  φ)  inv φ  𝗋[f']"
          using assms A.antipar lunit'_naturality runit_naturality [of "inv φ"] by auto
        also have "... = 𝗅-1[f']  (φ  inv φ)  𝗋[f']"
          using comp_assoc by simp
        also have "... =  𝗅-1[f']  𝗋[f']"
          using assms comp_cod_arr comp_arr_inv inv_is_inverse by auto
        finally show ?thesis by simp
      qed
    qed

    lemma adjoint_pair_preserved_by_iso:
    assumes "adjoint_pair f g"
    and "«φ : f  f'»" and "iso φ"
    and "«ψ : g  g'»" and "iso ψ"
    shows "adjoint_pair f' g'"
      using assms adjoint_pair_def adjunction_preserved_by_iso_left
            adjunction_preserved_by_iso_right
      by metis

    lemma left_adjoint_preserved_by_iso:
    assumes "is_left_adjoint f"
    and "«φ : f  f'»" and "iso φ"
    shows "is_left_adjoint f'"
    proof -
      obtain g where g: "adjoint_pair f g"
        using assms by auto
      have "adjoint_pair f' g"
        using assms g adjoint_pair_preserved_by_iso [of f g φ f' g g]
              adjoint_pair_antipar [of f g]
        by auto
      thus ?thesis by auto
    qed

    lemma right_adjoint_preserved_by_iso:
    assumes "is_right_adjoint g"
    and "«φ : g  g'»" and "iso φ"
    shows "is_right_adjoint g'"
    proof -
      obtain f where f: "adjoint_pair f g"
        using assms by auto
      have "adjoint_pair f g'"
        using assms f adjoint_pair_preserved_by_iso [of f g f f φ g']
              adjoint_pair_antipar [of f g]
        by auto
      thus ?thesis by auto
    qed

    lemma left_adjoint_preserved_by_iso':
    assumes "is_left_adjoint f" and "f  f'"
    shows "is_left_adjoint f'"
      using assms isomorphic_def left_adjoint_preserved_by_iso by blast

    lemma right_adjoint_preserved_by_iso':
    assumes "is_right_adjoint g" and "g  g'"
    shows "is_right_adjoint g'"
      using assms isomorphic_def right_adjoint_preserved_by_iso by blast

    lemma obj_self_adjunction:
    assumes "obj a"
    shows "adjunction_in_bicategory V H 𝖺 𝗂 src trg a a 𝗅-1[a] 𝗋[a]"
    proof
      show 1: "ide a"
        using assms by auto
      show "«𝗅-1[a] : src a  a  a»"
        using assms 1 by auto
      show "«𝗋[a] : a  a  src a»"
        using assms 1 by fastforce
      show "(𝗋[a]  a)  𝖺-1[a, a, a]  (a  𝗅-1[a]) = 𝗅-1[a]  𝗋[a]"
        using assms 1 canI_unitor_1 canI_associator_1(2) canI_associator_3
              whisker_can_right_1 whisker_can_left_1 can_Ide_self obj_simps
        by simp
      show "(a  𝗋[a])  𝖺[a, a, a]  (𝗅-1[a]  a) = 𝗋-1[a]  𝗅[a]"
        using assms 1 canI_unitor_1 canI_associator_1(2) canI_associator_3
              whisker_can_right_1 whisker_can_left_1 can_Ide_self
        by simp
    qed

    lemma obj_is_self_adjoint:
    assumes "obj a"
    shows "adjoint_pair a a" and "is_left_adjoint a" and "is_right_adjoint a"
      using assms obj_self_adjunction adjoint_pair_def by auto

  end

  subsection "Pseudofunctors and Adjunctions"

  context pseudofunctor
  begin

    lemma preserves_adjunction:
    assumes "adjunction_in_bicategory VC HC 𝖺C 𝗂C srcC trgC f g η ε"
    shows "adjunction_in_bicategory VD HD 𝖺D 𝗂D srcD trgD (F f) (F g)
             (D.inv (Φ (g, f)) D F η D unit (srcC f))
             (D.inv (unit (trgC f)) D F ε D Φ (f, g))"
    proof -
      interpret adjunction_in_bicategory VC HC 𝖺C 𝗂C srcC trgC f g η ε
        using assms by auto
      interpret A: adjunction_data_in_bicategory VD HD 𝖺D 𝗂D srcD trgD
                     F f F g D.inv (Φ (g, f)) D F η D unit (srcC f)
                     D.inv (unit (trgC f)) D F ε D Φ (f, g)
        using adjunction_data_in_bicategory_axioms preserves_adjunction_data by auto
      show "adjunction_in_bicategory VD HD 𝖺D 𝗂D srcD trgD (F f) (F g)
              (D.inv (Φ (g, f)) D F η D unit (srcC f))
              (D.inv (unit (trgC f)) D F ε D Φ (f, g))"
      proof
        show "(D.inv (unit (trgC f)) D F ε D Φ (f, g) D F f) D 𝖺D-1[F f, F g, F f] D
                (F f D D.inv (Φ (g, f)) D F η D unit (srcC f)) =
              D.lunit' (F f) D 𝗋D[F f]"
        proof -
          have 1: "D.iso (Φ (f, g C f) D (F f D Φ (g, f)))"
            using antipar C.VV.ide_charSbC C.VV.arr_charSbC D.iso_is_arr FF_def
            by (intro D.isos_compose D.seqI, simp_all)
          have "(D.inv (unit (trgC f)) D F ε D Φ (f, g) D F f) D 𝖺D-1[F f, F g, F f] D
                    (F f D D.inv (Φ (g, f)) D F η D unit (srcC f)) =
                 (D.inv (unit (trgC f)) D F ε D Φ (f, g) D F f) D
                   (D.inv (Φ (f, g)) D F f) D D.inv (Φ (f C g, f)) D
                   F 𝖺C-1[f, g, f] D
                   Φ (f, g C f) D (F f D Φ (g, f)) D
                   (F f D D.inv (Φ (g, f)) D F η D unit (srcC f))"
          proof -
            have "𝖺D-1[F f, F g, F f] =
                  (D.inv (Φ (f, g)) D F f) D D.inv (Φ (f C g, f)) D F 𝖺C-1[f, g, f] D
                    Φ (f, g C f) D (F f D Φ (g, f))"
            proof -
              have "𝖺D-1[F f, F g, F f] D D.inv (Φ (f, g C f) D (F f D Φ (g, f))) =
                    D.inv (F 𝖺C[f, g, f] D Φ (f C g, f) D (Φ (f, g) D F f))"
              proof -
                have "D.inv (Φ (f, g C f) D (F f D Φ (g, f)) D 𝖺D[F f, F g, F f]) =
                      D.inv (F 𝖺C[f, g, f] D Φ (f C g, f) D (Φ (f, g) D F f))"
                  using antipar assoc_coherence by simp
                moreover
                have "D.inv (Φ (f, g C f) D (F f D Φ (g, f)) D 𝖺D[F f, F g, F f]) =
                      𝖺D-1[F f, F g, F f] D D.inv (Φ (f, g C f) D (F f D Φ (g, f)))"
                proof -
                  have "D.seq (Φ (f, g C f) D (F f D Φ (g, f))) 𝖺D[F f, F g, F f]"
                    using antipar by fastforce
                  thus ?thesis
                    using 1 antipar D.comp_assoc
                          D.inv_comp [of "𝖺D[F f, F g, F f]" "Φ (f, g C f) D (F f D Φ (g, f))"]
                    by auto
                qed
                ultimately show ?thesis by simp
              qed
              moreover have 2: "D.iso (F 𝖺C[f, g, f] D Φ (f C g, f) D (Φ (f, g) D F f))"
                using antipar D.isos_compose C.VV.ide_charSbC C.VV.arr_charSbC cmp_simps(4)
                by simp
              ultimately have "𝖺D-1[F f, F g, F f] =
                               D.inv (F 𝖺C[f, g, f] D Φ (f C g, f) D (Φ (f, g) D F f)) D
                                 (Φ (f, g C f) D (F f D Φ (g, f)))"
                using 1 2 antipar D.invert_side_of_triangle(2) D.inv_inv D.iso_inv_iso D.arr_inv
                by metis
              moreover have "D.inv (F 𝖺C[f, g, f] D Φ (f C g, f) D (Φ (f, g) D F f)) =
                             (D.inv (Φ (f, g)) D F f) D D.inv (Φ (f C g, f)) D F 𝖺C-1[f, g, f]"
              proof -
                have "D.inv (F 𝖺C[f, g, f] D Φ (f C g, f) D (Φ (f, g) D F f)) =
                       D.inv (Φ (f C g, f) D (Φ (f, g) D F f)) D F 𝖺C-1[f, g, f]"
                  using antipar D.isos_compose C.VV.arr_charSbC cmp_simps(4)
                        preserves_inv D.inv_comp C.VV.cod_charSbC
                  by simp
                also have "... = (D.inv (Φ (f, g) D F f) D D.inv (Φ (f C g, f))) D
                                 F 𝖺C-1[f, g, f]"
                  using antipar D.inv_comp C.VV.ide_charSbC C.VV.arr_charSbC cmp_simps(4)
                  by simp
                also have "... = ((D.inv (Φ (f, g)) D F f) D D.inv (Φ (f C g, f))) D
                                 F 𝖺C-1[f, g, f]"
                  using antipar C.VV.ide_charSbC C.VV.arr_charSbC by simp
                also have "... = (D.inv (Φ (f, g)) D F f) D D.inv (Φ (f C g, f)) D
                                 F 𝖺C-1[f, g, f]"
                  using D.comp_assoc by simp
                finally show ?thesis by simp
              qed
              ultimately show ?thesis
                using D.comp_assoc by simp
            qed
            thus ?thesis
              using D.comp_assoc by simp
          qed
          also have "... = (D.inv (unit (trgC f)) D F ε D F f) D
                             D.inv (Φ (f C g, f)) D
                             F 𝖺C-1[f, g, f] D
                             Φ (f, g C f) D
                             (F f D F η D unit (srcC f))"
          proof -
            have "... = ((D.inv (unit (trgC f)) D F ε D F f) D (Φ (f, g) D F f)) D
                          (D.inv (Φ (f, g)) D F f) D D.inv (Φ (f C g, f)) D
                          F 𝖺C-1[f, g, f] D
                          Φ (f, g C f) D (F f D Φ (g, f)) D
                          ((F f D D.inv (Φ (g, f))) D (F f D F η D unit (srcC f)))"
            proof -
              have "D.inv (unit (trgC f)) D F ε D Φ (f, g) D F f =
                    (D.inv (unit (trgC f)) D F ε D F f) D (Φ (f, g) D F f)"
                using ide_left ide_right antipar D.whisker_right unit_char(2)
                by (metis A.counit_simps(1) A.ide_left D.comp_assoc)
              moreover have "F f D D.inv (Φ (g, f)) D F η D unit (srcC f) =
                             (F f D D.inv (Φ (g, f))) D (F f D F η D unit (srcC f))"
                using antipar unit_char(2) D.whisker_left by simp
              ultimately show ?thesis by simp
            qed
            also have "... = (D.inv (unit (trgC f)) D F ε D F f) D
                               (((Φ (f, g) D F f) D (D.inv (Φ (f, g)) D F f)) D
                               D.inv (Φ (f C g, f))) D F 𝖺C-1[f, g, f] D Φ (f, g C f) D
                               (((F f D Φ (g, f)) D (F f D D.inv (Φ (g, f)))) D
                               (F f D F η D unit (srcC f)))"
              using D.comp_assoc by simp
            also have "... = (D.inv (unit (trgC f)) D F ε D F f) D
                             D.inv (Φ (f C g, f)) D
                             F 𝖺C-1[f, g, f] D
                             Φ (f, g C f) D
                             (F f D F η D unit (srcC f))"
            proof -
              have "((F f D Φ (g, f)) D (F f D D.inv (Φ (g, f)))) D
                      (F f D F η D unit (srcC f)) =
                    F f D F η D unit (srcC f)"
              proof -
                have "(F f D Φ (g, f)) D (F f D D.inv (Φ (g, f))) = F f D F (g C f)"
                  using antipar unit_char(2) D.comp_arr_inv D.inv_is_inverse
                        D.whisker_left [of "F f" "Φ (g, f)" "D.inv (Φ (g, f))"]
                  by simp
                moreover have "D.seq (F f D F (g C f)) (F f D F η D unit (srcC f))"
                  using antipar by fastforce
                ultimately show ?thesis
                  using D.comp_cod_arr by auto
              qed
              moreover have "((Φ (f, g) D F f) D (D.inv (Φ (f, g)) D F f)) D
                               D.inv (Φ (f C g, f)) =
                             D.inv (Φ (f C g, f))"
                using antipar D.comp_arr_inv D.inv_is_inverse D.comp_cod_arr
                      D.whisker_right [of "F f" "Φ (f, g)" "D.inv (Φ (f, g))"]
                by simp
              ultimately show ?thesis by simp
            qed
            finally show ?thesis by simp
          qed
          also have "... = (D.inv (unit (trgC f)) D F f) D
                             D.inv (Φ (trgC f, f)) D F (ε C f) D
                             ((Φ (f C g, f) D D.inv (Φ (f C g, f))) D
                                F 𝖺C-1[f, g, f]) D
                             ((Φ (f, g C f) D D.inv (Φ (f, g C f))) D F (f C η)) D
                             Φ (f, srcC f) D (F f D unit (srcC f))"
          proof -
            have "(D.inv (unit (trgC f)) D F ε D F f) D
                    D.inv (Φ (f C g, f)) D
                    F 𝖺C-1[f, g, f] D
                    Φ (f, g C f) D
                    (F f D F η D unit (srcC f)) =
                  ((D.inv (unit (trgC f)) D F f) D (F ε D F f)) D
                    D.inv (Φ (f C g, f)) D
                    F 𝖺C-1[f, g, f] D
                    Φ (f, g C f) D
                    ((F f D F η) D (F f D unit (srcC f)))"
                using antipar D.comp_assoc D.whisker_left D.whisker_right unit_char(2)
                by simp
            moreover have "F ε D F f = D.inv (Φ (trgC f, f)) D F (ε C f) D Φ (f C g, f)"
              using antipar Φ.naturality [of "(ε, f)"] C.VV.arr_charSbC FF_def
                    D.invert_side_of_triangle(1) C.VV.dom_charSbC C.VV.cod_charSbC
              by simp
            moreover have "F f D F η = D.inv (Φ (f, g C f)) D F (f C η) D Φ (f, srcC f)"
              using antipar Φ.naturality [of "(f, η)"] C.VV.arr_charSbC FF_def
                    D.invert_side_of_triangle(1) C.VV.dom_charSbC C.VV.cod_charSbC
              by simp
            ultimately show ?thesis
              using D.comp_assoc by simp
          qed
          also have "... = ((D.inv (unit (trgC f)) D F f) D D.inv (Φ (trgC f, f))) D
                             (F (ε C f) D
                             (F ((f C g) C f) D F 𝖺C-1[f, g, f] D F (f C g C f)) D
                             F (f C η)) D
                             Φ (f, srcC f) D (F f D unit (srcC f))"
            using antipar D.comp_arr_inv' D.comp_assoc by simp
          also have "... = ((D.inv (unit (trgC f)) D F f) D D.inv (Φ (trgC f, f))) D
                             (F (ε C f) D F 𝖺C-1[f, g, f] D F (f C η)) D
                             Φ (f, srcC f) D (F f D unit (srcC f))"
          proof -
            have "F ((f C g) C f) D F 𝖺C-1[f, g, f] D F (f C g C f) = F 𝖺C-1[f, g, f]"
              using antipar D.comp_arr_dom D.comp_cod_arr by simp
            thus ?thesis by simp
          qed
          also have "... = D.inv (Φ (trgC f, f) D (unit (trgC f) D F f)) D
                             F ((ε C f) C 𝖺C-1[f, g, f] C (f C η)) D
                             Φ (f, srcC f) D (F f D unit (srcC f))"
          proof -
            have "(D.inv (unit (trgC f)) D F f) D D.inv (Φ (trgC f, f)) =
                  D.inv (Φ (trgC f, f) D (unit (trgC f) D F f))"
            proof -
              have "D.iso (Φ (trgC f, f))"
                using antipar by simp
              moreover have "D.iso (unit (trgC f) D F f)"
                using antipar unit_char(2) by simp
              moreover have "D.seq (Φ (trgC f, f)) (unit (trgC f) D F f)"
                using antipar D.iso_is_arr calculation(2)
                apply (intro D.seqI D.hseqI) by auto
              ultimately show ?thesis
                using antipar D.inv_comp unit_char(2) by simp
            qed
            moreover have "F (ε C f) D F 𝖺C-1[f, g, f] D F (f C η) =
                           F ((ε C f) C 𝖺C-1[f, g, f] C (f C η))"
              using antipar by simp
            ultimately show ?thesis by simp
          qed
          also have "... = (D.lunit' (F f) D F 𝗅C[f]) D
                             F (C.lunit' f C 𝗋C[f]) D
                             (D.inv (F 𝗋C[f]) D 𝗋D[F f])"
          proof -
            have "F ((ε C f) C 𝖺C-1[f, g, f] C (f C η)) = F (C.lunit' f C 𝗋C[f])"
              using triangle_left by simp
            moreover have "D.inv (Φ (trgC f, f) D (unit (trgC f) D F f)) =
                           D.lunit' (F f) D F 𝗅C[f]"
            proof -
              have 0: "D.iso (Φ (trgC f, f) D (unit (trgC f) D F f))"
                using unit_char(2)
                apply (intro D.isos_compose D.seqI) by auto
              show ?thesis
              proof -
                have 1: "D.iso (F 𝗅C[f])"
                  using C.iso_lunit preserves_iso by auto
                moreover have "D.iso (F 𝗅C[f] D Φ (trgC f, f) D (unit (trgC f) D F f))"
                  by (metis (no_types) A.ide_left D.iso_lunit ide_left lunit_coherence)
                moreover have "D.inv (D.inv (F 𝗅C[f])) = F 𝗅C[f]"
                  using 1 D.inv_inv by blast
                ultimately show ?thesis
                  by (metis 0 D.inv_comp D.invert_side_of_triangle(2) D.iso_inv_iso
                      D.iso_is_arr ide_left lunit_coherence)
              qed
            qed
            moreover have "Φ (f, srcC f) D (F f D unit (srcC f)) = D.inv (F 𝗋C[f]) D 𝗋D[F f]"
              using ide_left runit_coherence preserves_iso C.iso_runit D.invert_side_of_triangle(1)
              by (metis A.ide_left D.runit_simps(1))
            ultimately show ?thesis by simp
          qed
          also have "... = D.lunit' (F f) D
                             ((F 𝗅C[f] D F (C.lunit' f)) D (F 𝗋C[f] D D.inv (F 𝗋C[f]))) D
                             𝗋D[F f]"
            using D.comp_assoc by simp
          also have "... = D.lunit' (F f) D 𝗋D[F f]"
            using D.comp_cod_arr C.iso_runit C.iso_lunit preserves_iso D.comp_arr_inv'
                  preserves_inv
            by force
          finally show ?thesis by blast
        qed
        show "(F g D D.inv (unit (trgC f)) D F ε D Φ (f, g)) D
                𝖺D[F g, F f, F g] D (D.inv (Φ (g, f)) D F η D unit (srcC f) D F g) =
              D.runit' (F g) D 𝗅D[F g]"
        proof -
          have "𝖺D[F g, F f, F g] =
                D.inv (Φ (g, f C g) D (F g D Φ (f, g))) D
                  F 𝖺C[g, f, g] D Φ (g C f, g) D (Φ (g, f) D F g)"
          proof -
            have "D.iso (Φ (g, f C g) D (F g D Φ (f, g)))"
              using antipar D.iso_is_arr
              apply (intro D.isos_compose, auto)
              by (metis C.iso_assoc D.comp_assoc D.seqE ide_left ide_right
                  preserves_assoc(1) preserves_iso)
            moreover have "F 𝖺C[g, f, g] D Φ (g C f, g) D (Φ (g, f) D F g) =
                           Φ (g, f C g) D (F g D Φ (f, g)) D 𝖺D[F g, F f, F g]"
              using antipar assoc_coherence by simp
            moreover have "D.seq (F 𝖺C[g, f, g]) (Φ (g C f, g) D (Φ (g, f) D F g))"
              using antipar C.VV.arr_charSbC C.VV.dom_charSbC C.VV.cod_charSbC FF_def
              by (intro D.seqI D.hseqI') auto
            ultimately show ?thesis
              using D.invert_side_of_triangle(1) D.comp_assoc by auto
            qed
            hence "(F g D D.inv (unit (trgC f)) D F ε D Φ (f, g)) D
                     𝖺D[F g, F f, F g] D
                     (D.inv (Φ (g, f)) D F η D unit (srcC f) D F g) =
                   (F g D (D.inv (unit (trgC f)) D F ε) D Φ (f, g)) D
                     D.inv (Φ (g, f C g) D (F g D Φ (f, g))) D
                     F 𝖺C[g, f, g] D
                     Φ (g C f, g) D (Φ (g, f) D F g) D
                     (D.inv (Φ (g, f)) D F η D unit (srcC f) D F g)"
              using D.comp_assoc by simp
            also have "... = ((F g D D.inv (unit (trgC f)) D F ε) D (F g D Φ (f, g))) D
                               D.inv (Φ (g, f C g) D (F g D Φ (f, g))) D
                               F 𝖺C[g, f, g] D Φ (g C f, g) D
                               (Φ (g, f) D F g) D ((D.inv (Φ (g, f)) D F g) D
                               (F η D unit (srcC f) D F g))"
            proof -
              have "F g D (D.inv (unit (trgC f)) D F ε) D Φ (f, g) =
                    (F g D D.inv (unit (trgC f)) D F ε) D (F g D Φ (f, g))"
              proof -
                have "D.seq (D.inv (unit (trgC f)) D F ε) (Φ (f, g))"
                  using antipar D.comp_assoc by simp
                thus ?thesis
                  using antipar D.whisker_left by simp
              qed
              moreover have "D.inv (Φ (g, f)) D F η D unit (srcC f) D F g =
                             (D.inv (Φ (g, f)) D F g) D (F η D unit (srcC f) D F g)"
                using antipar D.whisker_right by simp
              ultimately show ?thesis
                using D.comp_assoc by simp
           qed
           also have "... = (F g D D.inv (unit (trgC f)) D F ε) D
                              (((F g D Φ (f, g)) D D.inv (F g D Φ (f, g))) D
                              D.inv (Φ (g, f C g))) D F 𝖺C[g, f, g] D Φ (g C f, g) D
                              ((Φ (g, f) D F g) D (D.inv (Φ (g, f)) D F g)) D
                              (F η D unit (srcC f) D F g)"
           proof -
             have "D.inv (Φ (g, f C g) D (F g D Φ (f, g))) =
                   D.inv (F g D Φ (f, g)) D D.inv (Φ (g, f C g))"
             proof -
              have "D.iso (Φ (g, f C g))"
                using antipar by simp
              moreover have "D.iso (F g D Φ (f, g))"
                using antipar by simp
              moreover have "D.seq (Φ (g, f C g)) (F g D Φ (f, g))"
                using antipar cmp_in_hom A.ide_right D.iso_is_arr
                by (intro D.seqI) auto
              ultimately show ?thesis
                using antipar D.inv_comp by simp
            qed
            thus ?thesis
              using D.comp_assoc by simp
          qed
          also have "... = (F g D D.inv (unit (trgC f)) D F ε) D
                             D.inv (Φ (g, f C g)) D F 𝖺C[g, f, g] D Φ (g C f, g) D
                             (F η D unit (srcC f) D F g)"
          proof -
            have "((Φ (g, f) D F g) D (D.inv (Φ (g, f)) D F g)) D
                    (F η D unit (srcC f) D F g) =
                  (F η D unit (srcC f) D F g)"
            proof -
              have "(Φ (g, f) D F g) D (D.inv (Φ (g, f)) D F g) = F (g C f) D F g"
                using antipar D.comp_arr_inv'
                      D.whisker_right [of "F g" "Φ (g, f)" "D.inv (Φ (g, f))"]
                by simp
              thus ?thesis
                using antipar D.comp_cod_arr D.whisker_right by simp
            qed
            moreover have "((F g D Φ (f, g)) D D.inv (F g D Φ (f, g))) D
                             D.inv (Φ (g, f C g)) =
                           D.inv (Φ (g, f C g))"
              using antipar D.comp_arr_inv' D.comp_cod_arr
                    D.whisker_left [of "F g" "Φ (f, g)" "D.inv (Φ (f, g))"]
              by simp
            ultimately show ?thesis by simp
          qed
          also have "... = (F g D D.inv (unit (trgC f))) D
                             ((F g D F ε) D D.inv (Φ (g, f C g))) D
                             F 𝖺C[g, f, g] D
                             (Φ (g C f, g) D (F η D F g)) D
                             (unit (srcC f) D F g)"
            using antipar D.whisker_left D.whisker_right unit_char(2) D.comp_assoc by simp
          also have "... = (F g D D.inv (unit (trgC f))) D D.inv (Φ (g, srcC g)) D
                             (F (g C ε) D F 𝖺C[g, f, g] D F (η C g)) D
                             Φ (trgC g, g) D (unit (srcC f) D F g)"
          proof -
            have "(F g D F ε) D D.inv (Φ (g, f C g)) = D.inv (Φ (g, srcC g)) D F (g C ε)"
              using antipar C.VV.arr_charSbC Φ.naturality [of "(g, ε)"] FF_def
                    D.invert_opposite_sides_of_square C.VV.dom_charSbC C.VV.cod_charSbC
              by simp
            moreover have "Φ (g C f, g) D (F η D F g) = F (η C g) D Φ (trgC g, g)"
              using antipar C.VV.arr_charSbC Φ.naturality [of "(η, g)"] FF_def
                    C.VV.dom_charSbC C.VV.cod_charSbC
              by simp
            ultimately show ?thesis
              using D.comp_assoc by simp
          qed
          also have "... = ((F g D D.inv (unit (trgC f))) D D.inv (Φ (g, srcC g)) D
                             F (C.runit' g)) D (F 𝗅C[g] D Φ (trgC g, g) D (unit (srcC f) D F g))"
          proof -
            have "F (g C ε) D F 𝖺C[g, f, g] D F (η C g) = F (C.runit' g) D F 𝗅C[g]"
              using ide_left ide_right antipar triangle_right
              by (metis C.comp_in_homE C.seqI' preserves_comp triangle_in_hom(2))
            thus ?thesis
              using D.comp_assoc by simp
          qed
          also have "... = D.runit' (F g) D 𝗅D[F g]"
          proof -
            have "D.inv 𝗋D[F g] =
                  (F g D D.inv (unit (trgC f))) D D.inv (Φ (g, srcC g)) D F (C.runit' g)"
            proof -
              have "D.runit' (F g) = D.inv (F 𝗋C[g] D Φ (g, srcC g) D (F g D unit (srcC g)))"
                using runit_coherence by simp
              also have
                "... = (F g D D.inv (unit (trgC f))) D D.inv (Φ (g, srcC g)) D F (C.runit' g)"
              proof -
                have "D.inv (F 𝗋C[g] D Φ (g, srcC g) D (F g D unit (srcC g))) =
                       D.inv (F g D unit (srcC g)) D D.inv (Φ (g, srcC g)) D F (C.runit' g)"
                proof -
                  have "D.iso (F 𝗋C[g])"
                    using preserves_iso by simp
                  moreover have 1: "D.iso (Φ (g, srcC g) D (F g D unit (srcC g)))"
                    using preserves_iso unit_char(2) D.arrI D.seqE ide_right runit_coherence
                    by (intro D.isos_compose D.seqI, auto)
                  moreover have "D.seq (F 𝗋C[g]) (Φ (g, srcC g) D (F g D unit (srcC g)))"
                    using ide_right A.ide_right D.runit_simps(1) runit_coherence by metis
                  ultimately have "D.inv (F 𝗋C[g] D Φ (g, srcC g) D (F g D unit (srcC g))) =
                                   D.inv (Φ (g, srcC g) D (F g D unit (srcC g))) D F (C.runit' g)"
                    using C.iso_runit preserves_inv D.inv_comp by simp
                  moreover have "D.inv (Φ (g, srcC g) D (F g D unit (srcC g))) =
                                 D.inv (F g D unit (srcC g)) D D.inv (Φ (g, srcC g))"
                  proof -
                    have "D.seq (Φ (g, srcC g)) (F g D unit (srcC g))"
                      using 1 antipar preserves_iso unit_char(2) by fast
                      (*
                       * TODO: The fact that auto cannot do this step is probably what is blocking
                       * the whole thing from being done by auto.
                       *)
                    thus ?thesis
                      using 1 antipar preserves_iso unit_char(2) D.inv_comp by auto
                  qed
                  ultimately show ?thesis
                    using D.comp_assoc by simp
                qed
                thus ?thesis
                  using antipar unit_char(2) preserves_iso by simp
              qed
              finally show ?thesis by simp
            qed
            thus ?thesis
              using antipar lunit_coherence by simp
          qed
          finally show ?thesis by simp
        qed
      qed
    qed

    lemma preserves_adjoint_pair:
    assumes "C.adjoint_pair f g"
    shows "D.adjoint_pair (F f) (F g)"
      using assms C.adjoint_pair_def D.adjoint_pair_def preserves_adjunction by blast

    lemma preserves_left_adjoint:
    assumes "C.is_left_adjoint f"
    shows "D.is_left_adjoint (F f)"
      using assms preserves_adjoint_pair by auto

    lemma preserves_right_adjoint:
    assumes "C.is_right_adjoint g"
    shows "D.is_right_adjoint (F g)"
      using assms preserves_adjoint_pair by auto

  end

  context equivalence_pseudofunctor
  begin

    lemma reflects_adjunction:
    assumes "C.ide f" and "C.ide g"
    and "«η : srcC f C g C f»" and "«ε : f C g C srcC g»"
    and "adjunction_in_bicategory VD HD 𝖺D 𝗂D srcD trgD (F f) (F g)
           (D.inv (Φ (g, f)) D F η D unit (srcC f))
           (D.inv (unit (trgC f)) D F ε D Φ (f, g))"
    shows "adjunction_in_bicategory VC HC 𝖺C 𝗂C srcC trgC f g η ε"
    proof -
      let ?η' = "D.inv (Φ (g, f)) D F η D unit (srcC f)"
      let ?ε' = "D.inv (unit (trgC f)) D F ε D Φ (f, g)"
      interpret A': adjunction_in_bicategory VD HD 𝖺D 𝗂D srcD trgD F f F g ?η' ?ε'
        using assms(5) by auto
      interpret A: adjunction_data_in_bicategory VC HC 𝖺C 𝗂C srcC trgC f g η ε
        using assms(1-4) by (unfold_locales, auto)
      show ?thesis
      proof
        show "(ε C f) C 𝖺C-1[f, g, f] C (f C η) = 𝗅C-1[f] C 𝗋C[f]"
        proof -
          have 1: "C.par ((ε C f) C 𝖺C-1[f, g, f] C (f C η)) (𝗅C-1[f] C 𝗋C[f])"
            using assms A.antipar by simp
          moreover have "F ((ε C f) C 𝖺C-1[f, g, f] C (f C η)) = F (𝗅C-1[f] C 𝗋C[f])"
          proof -
            have "F ((ε C f) C 𝖺C-1[f, g, f] C (f C η)) =
                  F (ε C f) D F 𝖺C-1[f, g, f] D F (f C η)"
              using 1 by (metis C.seqE preserves_comp)
            also have "... =
                       (F (ε C f) D Φ (f C g, f)) D
                         (Φ (f, g) D F f) D 𝖺D-1[F f, F g, F f] D (F f D D.inv (Φ (g, f))) D
                         (D.inv (Φ (f, g C f)) D F (f C η))"
              using assms A.antipar preserves_assoc(2) D.comp_assoc by auto
            also have "... = Φ (trgC f, f) D ((F ε D F f) D (Φ (f, g) D F f)) D
                               𝖺D-1[F f, F g, F f] D
                               ((F f D D.inv (Φ (g, f))) D (F f D F η)) D
                               D.inv (Φ (f, srcC f))"
            proof -
              have "F (ε C f) D Φ (f C g, f) = Φ (trgC f, f) D (F ε D F f)"
                using assms Φ.naturality [of "(ε, f)"] FF_def C.VV.arr_charSbC
                      C.VV.dom_charSbC C.VV.cod_charSbC
                by simp
              moreover have "D.inv (Φ (f, g C f)) D F (f C η) =
                             (F f D F η) D D.inv (Φ (f, srcC f))"
              proof -
                have "F (f C η) D Φ (f, srcC f) = Φ (f, g C f) D (F f D F η)"
                  using assms Φ.naturality [of "(f, η)"] FF_def C.VV.arr_charSbC A.antipar
                        C.VV.dom_charSbC C.VV.cod_charSbC
                  by simp
                thus ?thesis
                  using assms A.antipar cmp_components_are_iso C.VV.arr_charSbC cmp_in_hom
                        FF_def C.VV.dom_simp C.VV.cod_simp
                        D.invert_opposite_sides_of_square
                          [of "Φ (f, g C f)" "F f D F η" "F (f C η)" "Φ (f, srcC f)"]
                  by fastforce
              qed
              ultimately show ?thesis
                using D.comp_assoc by simp
            qed
            also have "... = Φ (trgC f, f) D (F ε D Φ (f, g) D F f) D
                               𝖺D-1[F f, F g, F f] D
                               (F f D D.inv (Φ (g, f)) D F η) D D.inv (Φ (f, srcC f))"
              using assms A.antipar cmp_in_hom A.ide_left A.ide_right A'.ide_left A'.ide_right
                    D.whisker_left [of "F f" "D.inv (Φ (g, f))" "F η"]
                    D.whisker_right [of "F f" "F ε" "Φ (f, g)"]
              by (metis A'.counit_in_vhom A'.unit_simps(1)D.arrI D.comp_assoc
                  D.src.preserves_reflects_arr D.src_vcomp D.vseq_implies_hpar(1) cmp_simps(2))
            also have "... = Φ (trgC f, f) D (unit (trgC f) D ?ε' D F f) D
                               𝖺D-1[F f, F g, F f] D
                               (F f D ?η' D D.inv (unit (srcC f))) D D.inv (Φ (f, srcC f))"
            proof -
              have "F ε D Φ (f, g) = unit (trgC f) D ?ε'"
              proof -
                have "D.iso (unit (trgC f))"
                  using A.ide_left C.ideD(1) unit_char(2) by blast
                thus ?thesis
                  by (metis A'.counit_simps(1) D.comp_assoc D.comp_cod_arr D.inv_is_inverse
                      D.seqE D.comp_arr_inv)
              qed
              moreover have "D.inv (Φ (g, f)) D F η = ?η' D D.inv (unit (srcC f))"
                using assms(2) unit_char D.comp_arr_inv D.inv_is_inverse D.comp_assoc D.comp_cod_arr
                by (metis A'.unit_simps(1) A.antipar(1) C.ideD(1) C.obj_trg
                    D.invert_side_of_triangle(2))
              ultimately show ?thesis by simp
            qed
            also have "... = Φ (trgC f, f) D ((unit (trgC f) D F f) D
                               (?ε' D F f)) D 𝖺D-1[F f, F g, F f] D ((F f D ?η') D
                               (F f D D.inv (unit (srcC f)))) D D.inv (Φ (f, srcC f))"
              using assms A.antipar A'.antipar unit_char D.whisker_left D.whisker_right
              by simp
            also have "... = Φ (trgC f, f) D (unit (trgC f) D F f) D
                               ((?ε' D F f) D 𝖺D-1[F f, F g, F f] D (F f D ?η')) D
                               (F f D D.inv (unit (srcC f))) D D.inv (Φ (f, srcC f))"
              using D.comp_assoc by simp
            also have "... = (Φ (trgC f, f) D (unit (trgC f) D F f) D 𝗅D-1[F f]) D
                               𝗋D[F f] D (F f D D.inv (unit (srcC f))) D D.inv (Φ (f, srcC f))"
              using A'.triangle_left D.comp_assoc by simp
            also have "... = F 𝗅C-1[f] D F 𝗋C[f]"
              using assms A.antipar preserves_lunit(2) preserves_runit(1) by simp
            also have "... = F (𝗅C-1[f] C 𝗋C[f])"
              using assms by simp
            finally show ?thesis by simp
          qed
          ultimately show ?thesis
            using is_faithful by blast
        qed
        show "(g C ε) C 𝖺C[g, f, g] C (η C g) = 𝗋C-1[g] C 𝗅C[g]"
        proof -
          have 1: "C.par ((g C ε) C 𝖺C g f g C (η C g)) (𝗋C-1[g] C 𝗅C[g])"
            using assms A.antipar by auto
          moreover have "F ((g C ε) C 𝖺C[g, f, g] C (η C g)) = F (𝗋C-1[g] C 𝗅C[g])"
          proof -
            have "F ((g C ε) C 𝖺C g f g C (η C g)) =
                  F (g C ε) D F 𝖺C[g, f, g] D F (η C g)"
              using 1 by auto
            also have "... = (F (g C ε) D Φ (g, f C g)) D (F g D Φ (f, g)) D
                             𝖺D[F g, F f, F g] D
                             (D.inv (Φ (g, f)) D F g) D (D.inv (Φ (g C f, g)) D F (η C g))"
              using assms A.antipar preserves_assoc(1) [of g f g] D.comp_assoc by auto
            also have "... = Φ (g, srcC g) D ((F g D F ε) D (F g D Φ (f, g))) D
                             𝖺D[F g, F f, F g] D
                             ((D.inv (Φ (g, f)) D F g) D (F η D F g)) D D.inv (Φ (trgC g, g))"
            proof -
              have "F (g C ε) D Φ (g, f C g) = Φ (g, srcC g) D (F g D F ε)"
                using assms Φ.naturality [of "(g, ε)"] FF_def C.VV.arr_charSbC
                      C.VV.dom_simp C.VV.cod_simp
                by auto
              moreover have "D.inv (Φ (g C f, g)) D F (η C g) =
                             (F η D F g) D D.inv (Φ (trgC g, g))"
              proof -
                have "F (η C g) D Φ (trgC g, g) = Φ (g C f, g) D (F η D F g)"
                  using assms Φ.naturality [of "(η, g)"] FF_def C.VV.arr_charSbC A.antipar
                        C.VV.dom_simp C.VV.cod_simp
                  by auto
                thus ?thesis
                  using assms A.antipar cmp_components_are_iso C.VV.arr_charSbC FF_def
                        C.VV.dom_simp C.VV.cod_simp
                        D.invert_opposite_sides_of_square
                          [of "Φ (g C f, g)" "F η D F g" "F (η C g)" "Φ (trgC g, g)"]
                  by fastforce
              qed
              ultimately show ?thesis
                using D.comp_assoc by simp
            qed
            also have " ... = Φ (g, srcC g) D (F g D F ε D Φ (f, g)) D
                              𝖺D[F g, F f, F g] D
                              (D.inv (Φ (g, f)) D F η D F g) D D.inv (Φ (trgC g, g))"
            proof -
              have "(F g D F ε) D (F g D Φ (f, g)) = F g D F ε D Φ (f, g)"
                using assms A.antipar D.whisker_left
                by (metis A'.counit_simps(1) A'.ide_right D.seqE)
              moreover have "(D.inv (Φ (g, f)) D F g) D (F η D F g) =
                             D.inv (Φ (g, f)) D F η D F g"
                using assms A.antipar D.whisker_right by simp
              ultimately show ?thesis by simp
            qed
            also have "... = Φ (g, srcC g) D (F g D unit (trgC f) D ?ε') D
                             𝖺D[F g, F f, F g] D
                             (?η' D D.inv (unit (srcC f)) D F g) D D.inv (Φ (trgC g, g))"
            proof -
              have "F ε D Φ (f, g) = unit (trgC f) D ?ε'"
                using unit_char D.comp_arr_inv D.inv_is_inverse D.comp_assoc D.comp_cod_arr
                by (metis A'.counit_simps(1) C.ideD(1) C.obj_trg D.seqE assms(1))
              moreover have "D.inv (Φ (g, f)) D F η = ?η' D D.inv (unit (srcC f))"
                using unit_char D.comp_arr_inv D.inv_is_inverse D.comp_assoc D.comp_cod_arr
                by (metis A'.unit_simps(1) A.unit_simps(1) A.unit_simps(5)
                    C.obj_trg D.invert_side_of_triangle(2))
              ultimately show ?thesis by simp
            qed
            also have "... = Φ (g, srcC g) D (F g D unit (trgC f)) D
                             ((F g D ?ε') D 𝖺D[F g, F f, F g] D (?η' D F g)) D
                             (D.inv (unit (srcC f)) D F g) D D.inv (Φ (trgC g, g))"
              using assms A.antipar unit_char D.whisker_left D.whisker_right D.comp_assoc
              by simp
            also have "... = Φ (g, srcC g) D (F g D unit (trgC f)) D 𝗋D-1[F g] D
                             𝗅D[F g] D (D.inv (unit (srcC f)) D F g) D D.inv (Φ (trgC g, g))"
              using A'.triangle_right D.comp_assoc by simp
            also have "... = F 𝗋C-1[g] D F 𝗅C[g]"
                using assms A.antipar preserves_lunit(1) preserves_runit(2) D.comp_assoc
                by simp
            also have "... = F (𝗋C-1[g] C 𝗅C[g])"
              using assms by simp
            finally show ?thesis by simp
          qed
          ultimately show ?thesis
            using is_faithful by blast
        qed
      qed
    qed

    lemma reflects_adjoint_pair:
    assumes "C.ide f" and "C.ide g"
    and "srcC f = trgC g" and "srcC g = trgC f"
    and "D.adjoint_pair (F f) (F g)"
    shows "C.adjoint_pair f g"
    proof -
      obtain η' ε' where A': "adjunction_in_bicategory VD HD 𝖺D 𝗂D srcD trgD (F f) (F g) η' ε'"
        using assms D.adjoint_pair_def by auto
      interpret A': adjunction_in_bicategory VD HD 𝖺D 𝗂D srcD trgD F f F g η' ε'
        using A' by auto
      have 1: "«Φ (g, f) D η' D D.inv (unit (srcC f)) : F (srcC f) D F (g C f)»"
        using assms unit_char [of "srcC f"] A'.unit_in_hom
        by (intro D.comp_in_homI, auto)
      have 2: "«unit (trgC f) D ε' D D.inv (Φ (f, g)): F (f C g) D F (trgC f)»"
        using assms cmp_in_hom [of f g] unit_char [of "trgC f"] A'.counit_in_hom
        by (intro D.comp_in_homI, auto)
      obtain η where η: "«η : srcC f C g C f» 
                         F η = Φ (g, f) D η' D D.inv (unit (srcC f))"
        using assms 1 A'.unit_in_hom cmp_in_hom locally_full by fastforce
      have η': "η' = D.inv (Φ (g, f)) D F η D unit (srcC f)"
        using assms 1 η cmp_in_hom D.iso_inv_iso cmp_components_are_iso unit_char(2)
              D.invert_side_of_triangle(1) [of "F η" "Φ (g, f)" "η' D D.inv (unit (srcC f))"]
              D.invert_side_of_triangle(2) [of "D.inv (Φ (g, f)) D F η" η' "D.inv (unit (srcC f))"]
        by (metis (no_types, lifting) C.ideD(1) C.obj_trg D.arrI D.comp_assoc D.inv_inv)
      obtain ε where ε: "«ε : f C g C trgC f» 
                         F ε = unit (trgC f) D ε' D D.inv (Φ (f, g))"
        using assms 2 A'.counit_in_hom cmp_in_hom locally_full by fastforce
      have ε': "ε' = D.inv (unit (trgC f)) D F ε D Φ (f, g)"
        using assms 2 ε cmp_in_hom D.iso_inv_iso unit_char(2) D.comp_assoc
              D.invert_side_of_triangle(1) [of "F ε" "unit (trgC f)" "ε' D D.inv (Φ (f, g))"]
              D.invert_side_of_triangle(2) [of "D.inv (unit (trgC f)) D F ε" ε' "D.inv (Φ (f, g))"]
        by (metis (no_types, lifting) C.arrI C.ideD(1) C.obj_trg D.inv_inv cmp_components_are_iso
            preserves_arr)
      have "adjunction_in_bicategory VD HD 𝖺D 𝗂D srcD trgD (F f) (F g)
              (D.inv (Φ (g, f)) D F η D unit (srcC f))
              (D.inv (unit (trgC f)) D F ε D Φ (f, g))"
        using A'.adjunction_in_bicategory_axioms η' ε' by simp
      hence "adjunction_in_bicategory VC HC 𝖺C 𝗂C srcC trgC f g η ε"
        using assms η ε reflects_adjunction by simp
      thus ?thesis
        using C.adjoint_pair_def by auto
    qed

    lemma reflects_left_adjoint:
    assumes "C.ide f" and "D.is_left_adjoint (F f)"
    shows "C.is_left_adjoint f"
    proof -
      obtain g' where g': "D.adjoint_pair (F f) g'"
        using assms D.adjoint_pair_def by auto
      obtain g where g: "«g : trgC f C srcC f»  C.ide g  D.isomorphic (F g) g'"
        using assms g' locally_essentially_surjective [of "trgC f" "srcC f" g']
              D.adjoint_pair_antipar [of "F f" g']
        by auto
      obtain φ where φ: "«φ : g' D F g»  D.iso φ"
        using g D.isomorphic_def D.isomorphic_symmetric by metis
      have "D.adjoint_pair (F f) (F g)"
        using assms g g' φ D.adjoint_pair_preserved_by_iso [of "F f" g' "F f" "F f" φ "F g"]
        by auto
      thus ?thesis
        using assms g reflects_adjoint_pair [of f g] D.adjoint_pair_antipar C.in_hhom_def
        by auto
    qed

    lemma reflects_right_adjoint:
    assumes "C.ide g" and "D.is_right_adjoint (F g)"
    shows "C.is_right_adjoint g"
    proof -
      obtain f' where f': "D.adjoint_pair f' (F g)"
        using assms D.adjoint_pair_def by auto
      obtain f where f: "«f : trgC g C srcC g»  C.ide f  D.isomorphic (F f) f'"
        using assms f' locally_essentially_surjective [of "trgC g" "srcC g" f']
              D.adjoint_pair_antipar [of f' "F g"]
        by auto
      obtain φ where φ: "«φ : f' D F f»  D.iso φ"
        using f D.isomorphic_def D.isomorphic_symmetric by metis
      have "D.adjoint_pair (F f) (F g)"
        using assms f f' φ D.adjoint_pair_preserved_by_iso [of f' "F g" φ "F f" "F g" "F g"]
        by auto
      thus ?thesis
        using assms f reflects_adjoint_pair [of f g] D.adjoint_pair_antipar C.in_hhom_def
        by auto
    qed      

  end

  subsection "Composition of Adjunctions"

  text ‹
    We first consider the strict case, then extend to all bicategories using strictification.
  ›

  locale composite_adjunction_in_strict_bicategory =
    strict_bicategory V H 𝖺 𝗂 src trg +
    fg: adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg f g ζ ξ +
    hk: adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg h k σ τ
  for V :: "'a  'a  'a"        (infixr  55)
  and H :: "'a  'a  'a"        (infixr  53)
  and 𝖺 :: "'a  'a  'a  'a"  (𝖺[_, _, _])
  and 𝗂 :: "'a  'a"              (𝗂[_])
  and src :: "'a  'a"
  and trg :: "'a  'a"
  and f :: "'a"
  and g :: "'a"
  and ζ :: "'a"
  and ξ :: "'a"
  and h :: "'a"
  and k :: "'a"
  and σ :: "'a"
  and τ :: "'a" +
  assumes composable: "src h = trg f"
  begin

    abbreviation η
    where "η  (g  σ  f)  ζ"

    abbreviation ε
    where "ε  τ  (h  ξ  k)"

    interpretation adjunction_data_in_bicategory V H 𝖺 𝗂 src trg h  f g  k η ε
    proof
      show "ide (h  f)"
        using composable by simp
      show "ide (g  k)"
        using fg.antipar hk.antipar composable by simp
      show "«η : src (h  f)  (g  k)  h  f»"
      proof
        show "«ζ : src (h  f)  g  f»"
          using fg.antipar hk.antipar composable ide (h  f) by auto
        show "«g  σ  f : g  f  (g  k)  h  f»"
        proof -
          have "«g  σ  f : g  trg f  f  g  (k  h)  f»"
            using fg.antipar hk.antipar composable hk.unit_in_hom
            apply (intro hcomp_in_vhom) by auto
          thus ?thesis
            using hcomp_obj_arr hcomp_assoc by fastforce
        qed
      qed
      show "«ε : (h  f)  g  k  src (g  k)»"
      proof
        show "«h  ξ  k : (h  f)  g  k  h  k»"
        proof -
          have "«h  ξ  k : h  (f  g)  k  h  trg f  k»"
            using composable fg.antipar(1-2) hk.antipar(1) by fastforce
          thus ?thesis
            using fg.antipar hk.antipar composable hk.unit_in_hom hcomp_obj_arr hcomp_assoc
            by simp
        qed
        show "«τ : h  k  src (g  k)»"
          using fg.antipar hk.antipar composable hk.unit_in_hom by auto
      qed
    qed

    sublocale adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg h  f g  k η ε
    proof
      show "(ε  h  f)  𝖺-1[h  f, g  k, h  f]  ((h  f)  η) = 𝗅-1[h  f]  𝗋[h  f]"
      proof -
        have "(ε  h  f)  𝖺-1[h  f, g  k, h  f]  ((h  f)  η) =
              (τ  (h  ξ  k)  h  f)  ((h  f)  (g  σ  f)  ζ)"
          using fg.antipar hk.antipar composable strict_assoc comp_ide_arr
                ide_left ide_right antipar(1) antipar(2)
          by (metis arrI seqE strict_assoc' triangle_in_hom(1))
        also have "... = (τ  h  f)  ((h  ξ  (k  h)  f)  (h  (f  g)  σ  f))  (h  f  ζ)"
          using fg.antipar hk.antipar composable whisker_left [of "h  f"] whisker_right
            comp_assoc hcomp_assoc
          by simp
        also have "... = (τ  h  f)  (h  (ξ  (k  h))  ((f  g)  σ)  f)  (h  f  ζ)"
          using fg.antipar hk.antipar composable whisker_left whisker_right hcomp_assoc
          by simp
        also have "... = (τ  h  f)  (h  (trg f  σ)  (ξ  trg f)  f)  (h  f  ζ)"
          using fg.antipar hk.antipar composable comp_arr_dom comp_cod_arr
                interchange [of ξ "f  g" "k  h" σ] interchange [of "trg f" ξ σ "trg f"]
          by (metis fg.counit_simps(1) fg.counit_simps(2) fg.counit_simps(3)
              hk.unit_simps(1) hk.unit_simps(2) hk.unit_simps(3))
        also have "... = (τ  h  f)  (h  σ  ξ  f)  (h  f  ζ)"
          using fg.antipar hk.antipar composable hcomp_obj_arr hcomp_arr_obj
          by (metis fg.counit_simps(1) fg.counit_simps(4) hk.unit_simps(1) hk.unit_simps(5)
              obj_src)
        also have "... = ((τ  h  f)  (h  σ  f))  ((h  ξ  f)  (h  f  ζ))"
          using fg.antipar hk.antipar composable whisker_left whisker_right comp_assoc
          by simp
        also have "... = ((τ  h)  (h  σ)  f)  (h  (ξ  f)  (f  ζ))"
          using fg.antipar hk.antipar composable whisker_left whisker_right hcomp_assoc
          by simp
        also have "... = h  f"
          using fg.antipar hk.antipar composable fg.triangle_left hk.triangle_left
          by simp
        also have "... = 𝗅-1[h  f]  𝗋[h  f]"
          using fg.antipar hk.antipar composable strict_lunit' strict_runit by simp
        finally show ?thesis by simp
      qed
      show "((g  k)  ε)  𝖺[g  k, h  f, g  k]  (η  g  k) = 𝗋-1[g  k]  𝗅[g  k]"
      proof -
        have "((g  k)  ε)  𝖺[g  k, h  f, g  k]  (η  g  k) =
              ((g  k)  τ  (h  ξ  k))  ((g  σ  f)  ζ  g  k)"
          using fg.antipar hk.antipar composable strict_assoc comp_ide_arr
                ide_left ide_right
          by (metis antipar(1) antipar(2) arrI seqE triangle_in_hom(2))
        also have "... = (g  k  τ)  ((g  (k  h)  ξ  k)  (g  σ  (f  g)  k))  (ζ  g  k)"
          using fg.antipar hk.antipar composable whisker_left [of "g  k"] whisker_right
            comp_assoc hcomp_assoc
          by simp
        also have "... = (g  k  τ)  (g  ((k  h)  ξ)  (σ  f  g)  k)  (ζ  g  k)"
            using fg.antipar hk.antipar composable whisker_left whisker_right hcomp_assoc
            by simp
        also have "... = (g  k  τ)  (g  (σ  src g)  (src g  ξ)  k)  (ζ  g  k)"
          using fg.antipar hk.antipar composable interchange [of "k  h" σ ξ "f  g"]
                interchange [of σ "src g" "src g" ξ] comp_arr_dom comp_cod_arr
          by (metis fg.counit_simps(1) fg.counit_simps(2) fg.counit_simps(3)
              hk.unit_simps(1) hk.unit_simps(2) hk.unit_simps(3))
        also have "... = (g  k  τ)  (g  σ  ξ  k)  (ζ  g  k)"
          using fg.antipar hk.antipar composable hcomp_obj_arr [of "src g" ξ]
                hcomp_arr_obj [of σ "src g"]
          by simp
        also have "... = ((g  k  τ)  (g  σ  k))  (g  ξ  k)  (ζ  g  k)"
          using fg.antipar hk.antipar composable whisker_left whisker_right comp_assoc
          by simp
        also have "... = (g  (k  τ)  (σ  k))  ((g  ξ)  (ζ  g)  k)"
          using fg.antipar hk.antipar composable whisker_left whisker_right hcomp_assoc
          by simp
        also have "... = g  k"
          using fg.antipar hk.antipar composable fg.triangle_right hk.triangle_right
          by simp
        also have "... = 𝗋-1[g  k]  𝗅[g  k]"
          using fg.antipar hk.antipar composable strict_lunit strict_runit' by simp
        finally show ?thesis by simp
      qed
    qed

    lemma is_adjunction_in_strict_bicategory:
    shows "adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg (h  f) (g  k) η ε"
      ..

  end

  context strict_bicategory
  begin

    lemma left_adjoints_compose:
    assumes "is_left_adjoint f" and "is_left_adjoint f'" and "src f' = trg f"
    shows "is_left_adjoint (f'  f)"
    proof -
      obtain g η ε where fg: "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
        using assms adjoint_pair_def by auto
      interpret fg: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using fg by auto
      obtain g' η' ε' where f'g': "adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g' η' ε'"
        using assms adjoint_pair_def by auto
      interpret f'g': adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g' η' ε'
        using f'g' by auto
      interpret f'fgg': composite_adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg
                          f g η ε f' g' η' ε'
        using assms apply unfold_locales by simp
      have "adjoint_pair (f'  f) (g  g')"
        using adjoint_pair_def f'fgg'.adjunction_in_bicategory_axioms by auto
      thus ?thesis by auto
    qed

    lemma right_adjoints_compose:
    assumes "is_right_adjoint g" and "is_right_adjoint g'" and "src g = trg g'"
    shows "is_right_adjoint (g  g')"
    proof -
      obtain f η ε where fg: "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
        using assms adjoint_pair_def by auto
      interpret fg: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using fg by auto
      obtain f' η' ε' where f'g': "adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g' η' ε'"
        using assms adjoint_pair_def by auto
      interpret f'g': adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g' η' ε'
        using f'g' by auto
      interpret f'fgg': composite_adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg
                          f g η ε f' g' η' ε'
        using assms fg.antipar f'g'.antipar apply unfold_locales by simp
      have "adjoint_pair (f'  f) (g  g')"
        using adjoint_pair_def f'fgg'.adjunction_in_bicategory_axioms by auto
      thus ?thesis by auto
    qed

  end

  text ‹
    We now use strictification to extend the preceding results to an arbitrary bicategory.
    We only prove that ``left adjoints compose'' and ``right adjoints compose'';
    I did not work out formulas for the unit and counit of the composite adjunction in the
    non-strict case.
  ›

  context 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: fully_faithful_functor V S.vcomp S.UP
      using S.UP_is_fully_faithful_functor by auto
    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

    lemma left_adjoints_compose:
    assumes "is_left_adjoint f" and "is_left_adjoint f'" and "src f = trg f'"
    shows "is_left_adjoint (f  f')"
    proof -
      have "S.is_left_adjoint (S.UP f)  S.is_left_adjoint (S.UP f')"
        using assms UP.preserves_left_adjoint by simp
      moreover have "S.src (S.UP f) = S.trg (S.UP f')"
        using assms left_adjoint_is_ide by simp
      ultimately have "S.is_left_adjoint (S.hcomp (S.UP f) (S.UP f'))"
        using S.left_adjoints_compose by simp
      moreover have "S.isomorphic (S.hcomp (S.UP f) (S.UP f')) (S.UP (f  f'))"
      proof -
        have "«S.cmpUP (f, f') : S.hcomp (S.UP f) (S.UP f') S S.UP (f  f')»"
          using assms left_adjoint_is_ide UP.cmp_in_hom by simp
        moreover have "S.iso (S.cmpUP (f, f'))"
          using assms left_adjoint_is_ide by simp
        ultimately show ?thesis
          using S.isomorphic_def by blast
      qed
      ultimately have "S.is_left_adjoint (S.UP (f  f'))"
        using S.left_adjoint_preserved_by_iso S.isomorphic_def by blast
      thus "is_left_adjoint (f  f')"
        using assms left_adjoint_is_ide UP.reflects_left_adjoint by simp
    qed

    lemma right_adjoints_compose:
    assumes "is_right_adjoint g" and "is_right_adjoint g'" and "src g' = trg g"
    shows "is_right_adjoint (g'  g)"
    proof -
      have "S.is_right_adjoint (S.UP g)  S.is_right_adjoint (S.UP g')"
        using assms UP.preserves_right_adjoint by simp
      moreover have "S.src (S.UP g') = S.trg (S.UP g)"
        using assms right_adjoint_is_ide by simp
      ultimately have "S.is_right_adjoint (S.hcomp (S.UP g') (S.UP g))"
        using S.right_adjoints_compose by simp
      moreover have "S.isomorphic (S.hcomp (S.UP g') (S.UP g)) (S.UP (g'  g))"
      proof -
        have "«S.cmpUP (g', g) : S.hcomp (S.UP g') (S.UP g) S S.UP (g'  g)»"
          using assms right_adjoint_is_ide UP.cmp_in_hom by simp
        moreover have "S.iso (S.cmpUP (g', g))"
          using assms right_adjoint_is_ide by simp
        ultimately show ?thesis
          using S.isomorphic_def by blast
      qed
      ultimately have "S.is_right_adjoint (S.UP (g'  g))"
        using S.right_adjoint_preserved_by_iso S.isomorphic_def by blast
      thus "is_right_adjoint (g'  g)"
        using assms right_adjoint_is_ide UP.reflects_right_adjoint by simp
    qed

  end

  subsection "Choosing Right Adjoints"

  text ‹
    It will be useful in various situations to suppose that we have made a choice of
    right adjoint for each left adjoint ({\it i.e.} each ``map'') in a bicategory.
  ›

  locale chosen_right_adjoints =
    bicategory
  begin

    unbundle no rtrancl_syntax

    definition some_right_adjoint  (‹_* [1000] 1000)
    where "f*  SOME g. adjoint_pair f g"

    definition some_unit
    where "some_unit f  SOME η. ε. adjunction_in_bicategory V H 𝖺 𝗂 src trg f f* η ε"

    definition some_counit
    where "some_counit f 
           SOME ε. adjunction_in_bicategory V H 𝖺 𝗂 src trg f f* (some_unit f) ε"

    lemma left_adjoint_extends_to_adjunction:
    assumes "is_left_adjoint f"
    shows "adjunction_in_bicategory V H 𝖺 𝗂 src trg f f* (some_unit f) (some_counit f)"
      using assms some_right_adjoint_def adjoint_pair_def some_unit_def some_counit_def
            someI_ex [of "λg. adjoint_pair f g"]
            someI_ex [of "λη. ε. adjunction_in_bicategory V H 𝖺 𝗂 src trg f f* η ε"]
            someI_ex [of "λε. adjunction_in_bicategory V H 𝖺 𝗂 src trg f f* (some_unit f) ε"]
      by auto

    lemma left_adjoint_extends_to_adjoint_pair:
    assumes "is_left_adjoint f"
    shows "adjoint_pair f f*"
      using assms adjoint_pair_def left_adjoint_extends_to_adjunction by blast

    lemma right_adjoint_in_hom [intro]:
    assumes "is_left_adjoint f"
    shows "«f* : trg f  src f»"
    and "«f* : f*  f*»"
      using assms left_adjoint_extends_to_adjoint_pair adjoint_pair_antipar [of f "f*"]
      by auto

    lemma right_adjoint_simps [simp]:
    assumes "is_left_adjoint f"
    shows "ide f*"
    and "src f* = trg f" and "trg f* = src f"
    and "dom f* = f*" and "cod f* = f*"
      using assms right_adjoint_in_hom left_adjoint_extends_to_adjoint_pair apply auto
      using assms right_adjoint_is_ide [of "f*"] by blast

  end

  locale map_in_bicategory =
    bicategory + chosen_right_adjoints +
  fixes f :: 'a
  assumes is_map: "is_left_adjoint f"
  begin

    abbreviation η
      where "η  some_unit f"

    abbreviation ε
      where "ε  some_counit f"

    sublocale adjunction_in_bicategory V H 𝖺 𝗂 src trg f f* η ε
      using is_map left_adjoint_extends_to_adjunction by simp

  end

  subsection "Equivalences Refine to Adjoint Equivalences"

  text ‹
    In this section, we show that, just as an equivalence between categories can always
    be refined to an adjoint equivalence, an internal equivalence in a bicategory can also
    always be so refined.
    The proof, which follows that of Theorem 3.3 from cite"nlab-adjoint-equivalence",
    makes use of the fact that if an internal equivalence satisfies one of the triangle
    identities, then it also satisfies the other.
  ›

  locale adjoint_equivalence_in_bicategory =
    equivalence_in_bicategory +
    adjunction_in_bicategory
  begin

    lemma dual_adjoint_equivalence:
    shows "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg g f (inv ε) (inv η)"
    proof -
      interpret gf: equivalence_in_bicategory V H 𝖺 𝗂 src trg g f inv ε inv η
        using dual_equivalence by simp
      show ?thesis
      proof
        show "(inv η  g)  𝖺-1[g, f, g]  (g  inv ε) = 𝗅-1[g]  𝗋[g]"
        proof -
          have "(inv η  g)  𝖺-1[g, f, g]  (g  inv ε) =
                inv ((g  ε)  𝖺[g, f, g]  (η  g))"
            using antipar inv_comp isos_compose comp_assoc by simp
          also have "... = inv (𝗋-1[g]  𝗅[g])"
            using triangle_right by simp
          also have "... = 𝗅-1[g]  𝗋[g]"
            using inv_comp by simp
          finally show ?thesis
            by blast
        qed
        show "(f  inv η)  𝖺[f, g, f]  (inv ε  f) = 𝗋-1[f]  𝗅[f]"
        proof -
          have "(f  inv η)  𝖺[f, g, f]  (inv ε  f) =
                inv ((ε  f)  𝖺-1[f, g, f]  (f  η))"
            using antipar inv_comp isos_compose comp_assoc by simp
          also have "... = inv (𝗅-1[f]  𝗋[f])"
            using triangle_left by simp
          also have "... = 𝗋-1[f]  𝗅[f]"
            using inv_comp by simp
          finally show ?thesis by blast
        qed
      qed
    qed

  end

  context bicategory
  begin

    lemma adjoint_equivalence_preserved_by_iso_right:
    assumes "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
    and "«φ : g  g'»" and "iso φ"
    shows "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' ((φ  f)  η) (ε  (f  inv φ))"
    proof -
      interpret fg: adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using assms by simp
      interpret fg': adjunction_in_bicategory V H 𝖺 𝗂 src trg f g' (φ  f)  η ε  (f  inv φ)
        using assms fg.adjunction_in_bicategory_axioms adjunction_preserved_by_iso_right
        by simp
      interpret fg': equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' (φ  f)  η ε  (f  inv φ)
        using assms fg.equivalence_in_bicategory_axioms equivalence_preserved_by_iso_right
        by simp
      show ?thesis ..
    qed

    lemma adjoint_equivalence_preserved_by_iso_left:
    assumes "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
    and "«φ : f  f'»" and "iso φ"
    shows "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f' g ((g  φ)  η) (ε  (inv φ  g))"
    proof -
      interpret fg: adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using assms by simp
      interpret fg': adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g (g  φ)  η ε  (inv φ  g)
        using assms fg.adjunction_in_bicategory_axioms adjunction_preserved_by_iso_left
        by simp
      interpret fg': equivalence_in_bicategory V H 𝖺 𝗂 src trg f' g (g  φ)  η ε  (inv φ  g)
        using assms fg.equivalence_in_bicategory_axioms equivalence_preserved_by_iso_left
        by simp
      show ?thesis ..
    qed

  end

  context strict_bicategory
  begin

    notation isomorphic  (infix  50)

    lemma equivalence_refines_to_adjoint_equivalence:
    assumes "equivalence_map f" and "«g : trg f  src f»" and "ide g"
    and "«η : src f  g  f»" and "iso η"
    shows "∃!ε. adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
    proof -
      obtain g' η' ε' where E': "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' η' ε'"
        using assms equivalence_map_def by auto
      interpret E': equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' η' ε'
        using E' by auto
      let ?a = "src f" and ?b = "trg f"
      (* TODO: in_homE cannot be applied automatically to a conjunction.  Must break down! *)
      have f_in_hhom: "«f : ?a  ?b»" and ide_f: "ide f"
        using assms equivalence_map_def by auto
      have g_in_hhom: "«g : ?b  ?a»" and ide_g: "ide g"
        using assms by auto
      have g'_in_hhom: "«g' : ?b  ?a»" and ide_g': "ide g'"
        using assms f_in_hhom E'.antipar by auto
      have η_in_hom: "«η : ?a  g  f»" and iso_η: "iso η"
        using assms by auto
      have a: "obj ?a" and b: "obj ?b"
        using f_in_hhom by auto
      have η_in_hhom: "«η : ?a  ?a»"
        using a η_in_hom
        by (metis arrI in_hhom_def obj_simps(2-3) vconn_implies_hpar(1-2))
      text ‹
        The following is quoted from cite"nlab-adjoint-equivalence":
        \begin{quotation}
          ``Since g ≅ gfg' ≅ g'›, the isomorphism fg' ≅ 1› also induces an isomorphism fg ≅ 1›,
          which we denote ξ›.  Now η› and ξ› may not satisfy the zigzag identities, but if we
          define ε› by ξ ⋅ (f ⋆ η-1) ⋅ (f ⋆ g ⋆ ξ-1) : f ⋆ g ⇒ 1›, then we can verify,
          using string diagram notation as above,
          that ε› satisfies one zigzag identity, and hence (by the previous lemma) also the other.

          Finally, if ε': fg ⇒ 1› is any other isomorphism satisfying the zigzag identities
          with η›, then we have:
          \[
              ε' = ε' ⋅ (ε f g) ⋅ (f η g) = ε ⋅ (f g ε') ⋅ (f η g) = ε›
          \]
          using the interchange law and two zigzag identities.  This shows uniqueness.''
        \end{quotation}
      ›
      have 1: "g  g'"
      proof -
        have "g  g  ?b"
          using assms hcomp_arr_obj isomorphic_reflexive by auto
        also have "...  g  f  g'"
          using assms f_in_hhom g_in_hhom g'_in_hhom E'.counit_in_vhom E'.counit_is_iso
                isomorphic_def hcomp_ide_isomorphic isomorphic_symmetric
          by (metis E'.counit_simps(5) in_hhomE trg_trg)
        also have "...  ?a  g'"
          using assms f_in_hhom g_in_hhom g'_in_hhom ide_g' E'.unit_in_vhom E'.unit_is_iso
                isomorphic_def hcomp_isomorphic_ide isomorphic_symmetric
          by (metis hcomp_assoc hcomp_isomorphic_ide in_hhomE src_src)
        also have "...  g'"
          using assms
          by (simp add: E'.antipar(1) hcomp_obj_arr isomorphic_reflexive)
        finally show ?thesis by blast
      qed
      have "f  g'  ?b"
        using E'.counit_is_iso isomorphicI [of ε'] by auto
      hence 2: "f  g  ?b"
        using assms 1 ide_f hcomp_ide_isomorphic [of f g g'] isomorphic_transitive
              isomorphic_symmetric
        by (metis in_hhomE)
      obtain ξ where ξ: "«ξ : f  g  ?b»  iso ξ"
        using 2 by auto
      have ξ_in_hom: "«ξ : f  g  ?b»" and iso_ξ: "iso ξ"
        using ξ by auto
      have ξ_in_hhom: "«ξ : ?b  ?b»"
        using b ξ_in_hom
        by (metis ξ in_hhom_def iso_is_arr obj_simps(2-3) vconn_implies_hpar(1-4))
      text ‹
        At the time of this writing, the definition of ε› given on nLab
        cite"nlab-adjoint-equivalence" had an apparent typo:
        the expression f ⋆ g ⋆ ξ-1 should read ξ-1 ⋆ f ⋆ g›, as we have used here.
      ›
      let  = "ξ  (f  inv η  g)  (inv ξ  f  g)"
      have ε_in_hom: "« : f  g  ?b»"
      proof (intro comp_in_homI)
        show "«f  inv η  g : f  g  f  g  f  g»"
        proof -
          have "«f  inv η  g : f  (g  f)  g  f  g»"
          proof -
            have "«f  inv η  g : f  (g  f)  g  f  ?a  g»"
              using assms η_in_hom iso_η by (intro hcomp_in_vhom) auto
            thus ?thesis
              using assms f_in_hhom hcomp_obj_arr by (metis in_hhomE)
          qed
          moreover have "f  (g  f)  g = f  g  f  g"
            using hcomp_assoc by simp
          ultimately show ?thesis by simp
        qed
        show "«inv ξ  f  g : f  g  f  g  f  g»"
        proof -
          have "«inv ξ  f  g : ?b  f  g  (f  g)  f  g»"
            using assms ξ_in_hom iso_ξ by (intro hcomp_in_vhom, auto)
          thus ?thesis
            using hcomp_assoc f_in_hhom g_in_hhom b hcomp_obj_arr [of ?b "f  g"]
            by fastforce
        qed
        show "«ξ : f  g  ?b»"
          using ξ_in_hom by blast
      qed
      have "iso "
        using f_in_hhom g_in_hhom η_in_hhom ide_f ide_g η_in_hom iso_η ξ_in_hhom ξ_in_hom iso_ξ
              iso_inv_iso isos_compose
        by (metis ε_in_hom arrI hseqE ide_is_iso iso_hcomp seqE)
      have 4: "«inv ξ  f : ?b  f  f  g  f»"
      proof -
        have "«inv ξ  f : ?b  f  (f  g)  f»"
          using ξ_in_hom iso_ξ f_in_hhom
          by (intro hcomp_in_vhom, auto)
        thus ?thesis
          using hcomp_assoc by simp
      qed
      text ‹
        First show ?ε› and η› satisfy the ``left'' triangle identity.
      ›
      have triangle_left: "(  f)  (f  η) = f"
      proof -
        have "(  f)  (f  η) = (ξ  f)  (f  inv η  g  f)  (inv ξ  f  g  f)  (?b  f  η)"
        proof -
          have "f  η = ?b  f  η"
            using b η_in_hhom hcomp_obj_arr [of ?b "f  η"] by fastforce
          moreover have "ξ  (f  inv η  g)  (inv ξ  f  g)  f =
                         (ξ  f)  ((f  inv η  g)  f)  ((inv ξ  f  g)  f)"
            using ide_f ide_g ξ_in_hhom ξ_in_hom iso_ξ η_in_hhom η_in_hom iso_η whisker_right
            by (metis ε_in_hom arrI seqE)
          moreover have "... = (ξ  f)  (f  inv η  g  f)  (inv ξ  f  g  f)"
            using hcomp_assoc by simp
          ultimately show ?thesis
            using comp_assoc by simp
        qed
        also have "... = (ξ  f)  ((f  inv η  g  f)  (f  g  f  η))  (inv ξ  f)"
        proof -
          have "(inv ξ  f  g  f)  (?b  f  η) = ((inv ξ  f)  (g  f))  ((?b  f)  η)"
            using hcomp_assoc by simp
          also have "... = (inv ξ  f)  (?b  f)  (g  f)  η"
          proof -
            have "seq (inv ξ  f) (?b  f)"
              using a b 4 ide_f ide_g ξ_in_hhom ξ_in_hom iso_ξ by blast
            moreover have "seq (g  f) η"
              using f_in_hhom g_in_hhom ide_g ide_f η_in_hom by fast
            ultimately show ?thesis
              using interchange [of "inv ξ  f" "?b  f" "g  f" η] by simp
          qed
          also have "... = inv ξ  f  η"
            using 4 comp_arr_dom comp_cod_arr η_in_hom hcomp_assoc by (metis in_homE)
          also have "... = (f  g)  inv ξ  (f  η)  (f  ?a)"
          proof -
            have "(f  g)  inv ξ = inv ξ"
              using ξ_in_hom iso_ξ comp_cod_arr by auto
            moreover have "(f  η)  (f  ?a) = f  η"
            proof -
              have "«f  η : f  ?a  f  g  f»"
                using η_in_hom by fastforce
              thus ?thesis
                using comp_arr_dom by blast
            qed
            ultimately show ?thesis by argo
          qed
          also have "... = ((f  g)  (f  η))  (inv ξ  (f  ?a))"
          proof -
            have "seq (f  g) (inv ξ)"
              using ξ_in_hom iso_ξ comp_cod_arr by auto
            moreover have "seq (f  η) (f  ?a)"
              using f_in_hhom η_in_hom by force
            ultimately show ?thesis
              using interchange by simp
          qed
          also have "... = (f  g  f  η)  (inv ξ  f)"
            using hcomp_arr_obj hcomp_assoc by auto
          finally have "(inv ξ  f  g  f)  (?b  f  η) = (f  g  f  η)  (inv ξ  f)"
            by simp
          thus ?thesis
            using comp_assoc by simp
        qed
        also have "... = (ξ  f)  ((f  ?a  η)  (f  inv η  ?a))  (inv ξ  f)"
        proof -
          have "(f  inv η  g  f)  (f  (g  f)  η) = f  (inv η  g  f)  ((g  f)  η)"
          proof -
            have "(f  (inv η  g)  f)  (f  (g  f)  η) = f  ((inv η  g)  f)  ((g  f)  η)"
            proof -
              have "seq ((inv η  g)  f) ((g  f)  η)"
              proof -
                have "seq (inv η  g  f) ((g  f)  η)"
                  using f_in_hhom ide_f g_in_hhom ide_g η_in_hhom η_in_hom iso_η
                  apply (intro seqI hseqI')
                            apply auto
                    by fastforce+
                thus ?thesis
                  using hcomp_assoc by simp
              qed
              thus ?thesis
                using whisker_left by simp
            qed
            thus ?thesis
              using hcomp_assoc by simp
          qed
          also have "... = f  (?a  η)  (inv η  ?a)"
          proof -
            have "(inv η  g  f)  ((g  f)  η) = (?a  η)  (inv η  ?a)"
            proof -
              have "(inv η  g  f)  ((g  f)  η) = inv η  (g  f)  (g  f)  η"
                using g_in_hhom ide_g η_in_hom iso_η
                      interchange [of "inv η" "g  f" "g  f" η]
                by force
              also have "... = inv η  η"
                using η_in_hom iso_η comp_arr_dom comp_cod_arr by auto
              also have "... = ?a  inv η  η  ?a"
                using η_in_hom iso_η comp_arr_dom comp_cod_arr by auto
              also have "... = (?a  η)  (inv η  ?a)"
                using a η_in_hom iso_η interchange [of ?a "inv η" η ?a] by blast
              finally show ?thesis by simp
            qed
            thus ?thesis by argo
          qed
          also have "... = (f  ?a  η)  (f  inv η  ?a)"
          proof -
            have "seq (?a  η) (inv η  ?a)"
            proof (intro seqI')
              show "«inv η  ?a : (g  f)  ?a  ?a  ?a»"
                using a g_in_hhom η_in_hom iso_η hseqI ide_f ide_g
                by (intro hcomp_in_vhom) auto
              show "«?a  η : ?a  ?a  ?a  g  f»"
                using a η_in_hom hseqI by (intro hcomp_in_vhom) auto
            qed
            thus ?thesis
              using whisker_left by simp
          qed
          finally show ?thesis
            using hcomp_assoc by simp
        qed
        also have "... = (ξ  f)  ((f  η)  (f  inv η))  (inv ξ  f)"
          using a η_in_hhom iso_η hcomp_obj_arr [of ?a η] hcomp_arr_obj [of "inv η" ?a] by auto
        also have "... = (ξ  f)  (inv ξ  f)"
        proof -
          have "((f  η)  (f  inv η))  (inv ξ  f) = (f  η  inv η)  (inv ξ  f)"
            using η_in_hhom iso_η whisker_left inv_in_hom by auto
          also have "... = (f  g  f)  (inv ξ  f)"
            using η_in_hom iso_η comp_arr_inv inv_is_inverse by auto
          also have "... = inv ξ  f"
            using 4 comp_cod_arr by blast
          ultimately show ?thesis by simp
        qed
        also have "... = f"
        proof -
          have "(ξ  f)  (inv ξ  f) = ξ  inv ξ  f"
            using ξ_in_hhom iso_ξ whisker_right by auto
          also have "... = ?b  f"
            using ξ_in_hom iso_ξ comp_arr_inv' by auto
          also have "... = f"
            using hcomp_obj_arr by auto
          finally show ?thesis by blast
        qed
        finally show ?thesis by blast
      qed

      (* TODO: Putting this earlier breaks some steps in the proof. *)
      interpret E: equivalence_in_strict_bicategory V H 𝖺 𝗂 src trg f g η 
        using ide_g η_in_hom ε_in_hom g_in_hhom iso η iso 
        by (unfold_locales, auto)

      text ‹
        Apply ``triangle left if and only iff right'' to show the ``right'' triangle identity.
      ›
      have triangle_right: "((g  ξ  (f  inv η  g)  (inv ξ  f  g))  (η  g) = g)"
        using triangle_left E.triangle_left_iff_right by simp

      text ‹
        Use the two triangle identities to establish an adjoint equivalence and show that
        there is only one choice for the counit.
      ›
      show "∃!ε. adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
      proof -
        have "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η "
        proof
          show "(  f)  𝖺-1[f, g, f]  (f  η) = 𝗅-1[f]  𝗋[f]"
          proof -
            have "(  f)  𝖺-1[f, g, f]  (f  η) = (  f)  (f  η)"
            proof -
              have "seq 𝖺-1[f, g, f] (f  η)"
                using E.antipar
                by (intro seqI, auto)
              hence "𝖺-1[f, g, f]  (f  η) = f  η"
                using ide_f ide_g E.antipar triangle_right strict_assoc' comp_ide_arr
                by presburger
              thus ?thesis by simp
            qed
            also have "... = f"
              using triangle_left by simp
            also have "... = 𝗅-1[f]  𝗋[f]"
              using strict_lunit strict_runit by simp
            finally show ?thesis by simp
          qed
          show "(g  )  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g]"
          proof -
            have "(g  )  𝖺[g, f, g]  (η  g) = (g  )  (η  g)"
            proof -
              have "seq 𝖺[g, f, g] (η  g)"
                using E.antipar
                by (intro seqI, auto)
              hence "𝖺[g, f, g]  (η  g) = η  g"
                using ide_f ide_g E.antipar triangle_right strict_assoc comp_ide_arr
                by presburger
              thus ?thesis by simp
            qed
            also have "... = g"
              using triangle_right by simp
            also have "... = 𝗋-1[g]  𝗅[g]"
              using strict_lunit strict_runit by simp
            finally show ?thesis by blast
          qed
        qed
        moreover have "ε ε'.  adjoint_equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε;
                                adjoint_equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε' 
                                    ε = ε'"
          using adjunction_unit_determines_counit
          by (meson adjoint_equivalence_in_bicategory.axioms(2))
        ultimately show ?thesis by auto
      qed
    qed

  end

  text ‹
    We now apply strictification to generalize the preceding result to an arbitrary bicategory.
  ›

  context 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: fully_faithful_functor V S.vcomp S.UP
      using S.UP_is_fully_faithful_functor by auto
    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
      ..

    lemma equivalence_refines_to_adjoint_equivalence:
    assumes "equivalence_map f" and "«g : trg f  src f»" and "ide g"
    and "«η : src f  g  f»" and "iso η"
    shows "∃!ε. adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
    proof -
      text ‹
        To unpack the consequences of the assumptions, we need to obtain an
        interpretation of @{locale equivalence_in_bicategory}, even though we don't
        need the associated data other than f›, a›, and b›.
      ›
      obtain g' φ ψ where E: "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' φ ψ"
        using assms equivalence_map_def by auto
      interpret E: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g' φ ψ
        using E by auto
      let ?a = "src f" and ?b = "trg f"
      have ide_f: "ide f" by simp
      have f_in_hhom: "«f : ?a  ?b»" by simp
      have a: "obj ?a" and b: "obj ?b" by auto
      have 1: "S.equivalence_map (S.UP f)"
        using assms UP.preserves_equivalence_maps by simp
      let ?η' = "S.inv (S.cmpUP (g, f)) S S.UP η S UP.unit ?a"
      have 2: "«S.UP η : S.UP ?a S S.UP (g  f)»"
        using assms UP.preserves_hom [of η "src f" "g  f"] by auto
      have 3: "«?η' : UP.map0 ?a S S.UP g S S.UP f»  S.iso ?η'"
      proof (intro S.comp_in_homI conjI)
        show "«S.inv (S.cmpUP (g, f)) : S.UP (g  f) S S.UP g S S.UP f»"
          using assms UP.cmp_in_hom(2) by auto
        moreover show "«UP.unit ?a : UP.map0 ?a S S.UP ?a»" by auto
        moreover show "«S.UP η : S.UP ?a S S.UP (g  f)»"
          using 2 by simp
        ultimately show "S.iso (S.inv (S.cmpUP (g, f)) S S.UP η S UP.unit ?a)"
          using assms UP.cmp_components_are_iso UP.unit_char(2)
          by (intro S.isos_compose) auto
      qed
      have ex_un_ξ': "∃!ξ'. adjoint_equivalence_in_bicategory S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg
                               (S.UP f) (S.UP g) ?η' ξ'"
      proof -
        have "«S.UP g : S.trg (S.UP f) S S.src (S.UP f)»"
          using assms(2) by auto
        moreover have "S.ide (S.UP g)"
          by (simp add: assms(3))
        ultimately show ?thesis
          using 1 3 S.equivalence_refines_to_adjoint_equivalence S.UP_map0_obj by simp
      qed
      obtain ξ' where ξ': "adjoint_equivalence_in_bicategory S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg
                             (S.UP f) (S.UP g) ?η' ξ'"
        using ex_un_ξ' by auto
      interpret E': adjoint_equivalence_in_bicategory S.vcomp S.hcomp S.𝖺 S.𝗂 S.src S.trg
                      S.UP f S.UP g ?η' ξ'
        using ξ' by auto
      let ?ε' = "UP.unit ?b S ξ' S S.inv (S.cmpUP (f, g))"
      have ε': "«?ε' : S.UP (f  g) S S.UP ?b»"
        using assms(2-3) by auto
      have ex_un_ε: "∃!ε. «ε : f  g  ?b»  S.UP ε = ?ε'"
      proof -
        have "ε. «ε : f  g  ?b»  S.UP ε = ?ε'"
        proof -
          have "src (f  g) = src ?b  trg (f  g) = trg ?b"
            using assms(2) f_in_hhom by auto
          moreover have "ide (f  g)"
            using assms(2-3) by auto
          ultimately show ?thesis
            using ε' UP.locally_full by auto
        qed
        moreover have
          "μ ν.  «μ : f  g  ?b»; S.UP μ = ?ε'; «ν : f  g  ?b»; S.UP ν = ?ε' 
                      μ = ν"
        proof -
          fix μ ν
          assume μ: "«μ : f  g  ?b»" and ν: "«ν : f  g  ?b»"
          and 1: "S.UP μ = ?ε'" and 2: "S.UP ν = ?ε'"
          have "par μ ν"
            using μ ν by fastforce
          thus "μ = ν"
            using 1 2 UP.is_faithful [of μ ν] by simp
        qed
        ultimately show ?thesis by auto
      qed
      have iso_ε': "S.iso ?ε'"
      proof (intro S.isos_compose)
        show "S.iso (S.inv (S.cmpUP (f, g)))"
          using assms UP.cmp_components_are_iso by auto
        show "S.iso ξ'"
          using E'.counit_is_iso by blast
        show "S.iso (UP.unit ?b)"
          using b UP.unit_char(2) by simp
        show "S.seq (UP.unit ?b) (ξ' S S.inv (S.cmpUP (f, g)))"
        proof (intro S.seqI')
          show "«UP.unit ?b : UP.map0 ?b S S.UP ?b»"
            using b UP.unit_char by simp
          show "«ξ' S S.inv (S.cmpUP (f, g)) : S.UP (f  g) S UP.map0 ?b»"
            using assms by auto
        qed
        thus "S.seq ξ' (S.inv (S.cmpUP (f, g)))" by auto
      qed
      obtain ε where ε: "«ε : f  g  ?b»  S.UP ε = ?ε'"
        using ex_un_ε by auto
      interpret E'': equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using assms(1,3-5)
        apply unfold_locales
             apply simp_all
        using assms(2) ε
         apply auto[1]
        using ε iso_ε' UP.reflects_iso [of ε]
        by auto
      interpret E'': adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
      proof
        show "(ε  f)  𝖺-1[f, g, f]  (f  η) = 𝗅-1[f]  𝗋[f]"
        proof -
          have "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))"
            using E''.UP_triangle(3) by simp
          also have "... = S.cmpUP (trg f, f) S
                           (UP.unit ?b S ξ' S S.inv (S.cmpUP (f, g)) 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 ε S.comp_assoc by simp
          also have "... = S.cmpUP (trg f, f) S (UP.unit ?b S ξ' 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 S.inv (S.cmpUP (f, g)) S S.cmpUP (f, g) = ξ'"
            proof -
              have "S.iso (S.cmpUP (f, g))"
                using assms by auto
              moreover have "S.dom (S.cmpUP (f, g)) = S.UP f S S.UP g"
                using assms by auto
              ultimately have "S.inv (S.cmpUP (f, g)) S S.cmpUP (f, g) = S.UP f S S.UP g"
                using S.comp_inv_arr' by simp
              thus ?thesis
                using S.comp_arr_dom E'.counit_in_hom(2) by simp
            qed
            thus ?thesis by argo
          qed
          also have
            "... = S.cmpUP (trg f, f) S (UP.unit ?b S S.UP f) S
                     ((ξ' 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 "UP.unit ?b S ξ' S S.UP f = (UP.unit ?b S S.UP f) S (ξ' S S.UP f)"
              using assms b UP.unit_char S.whisker_right S.UP_map0_obj by auto
            moreover have "S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η =
                           (S.UP f S S.inv (S.cmpUP (g, f))) S (S.UP f S S.UP η)"
              using assms S.whisker_left by auto
            ultimately show ?thesis
              using S.comp_assoc by simp
          qed
          also have "... = (S.cmpUP (trg f, f) S (UP.unit ?b 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 S.UP f) S (S.UP f S S.inv (S.cmpUP (g, f))) S (S.UP f S S.UP η)
                    = (S.UP f S S.inv (UP.unit (src f)))"
            proof -
              have "(S.UP f S S.inv (S.cmpUP (g, f))) S (S.UP f S S.UP η) =
                      S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η"
                using assms S.whisker_left by auto
              hence "((ξ' S S.UP f) S (S.UP f S S.inv (S.cmpUP (g, f))) S (S.UP f S S.UP η))
                       = ((ξ' S S.UP f) S (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η))"
                by simp
              also have "... = ((ξ' S S.UP f) S S.𝖺' (S.UP f) (S.UP g) (S.UP f)) S
                                 (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η)"
              proof -
                have "(ξ' S S.UP f) S S.𝖺' (S.UP f) (S.UP g) (S.UP f) = ξ' S S.UP f"
                proof -
                  have "«ξ' S S.UP f :
                          (S.UP f S S.UP g) S S.UP f S S.trg (S.UP f) S S.UP f»"
                    using assms by auto
                  moreover have "«S.𝖺' (S.UP f) (S.UP g) (S.UP f) :
                                    S.UP f S S.UP g S S.UP f S (S.UP f S S.UP g) S S.UP f»"
                    using assms S.assoc'_in_hom by auto
                  ultimately show ?thesis
                    using assms S.strict_assoc' S.iso_assoc S.hcomp_assoc E'.antipar
                          S.comp_arr_ide S.seqI'
                    by (metis (no_types, lifting) E'.ide_left E'.ide_right)
                qed
                thus ?thesis
                  using S.comp_assoc by simp
              qed
              also have "... = ((ξ' S S.UP f) S S.𝖺' (S.UP f) (S.UP g) (S.UP f) S
                                 (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η))"
                using S.comp_assoc by simp
              also have "... = (S.UP f S S.inv (UP.unit (src f)))"
              proof -
                have "(ξ' S S.UP f) S S.𝖺' (S.UP f) (S.UP g) (S.UP f) S
                        (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) =
                      (S.UP f S S.inv (UP.unit (src f)))"
                proof -
                  have "(ξ' S S.UP f) S S.𝖺' (S.UP f) (S.UP g) (S.UP f) S
                          (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) S
                          (S.UP f S UP.unit ?a) =
                        S.lunit' (S.UP f) S S.runit (S.UP f)"
                  proof -
                    have "(ξ' S S.UP f) S S.𝖺' (S.UP f) (S.UP g) (S.UP f) S
                            (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) S
                            (S.UP f S UP.unit ?a) =
                          (ξ' S S.UP f) S S.𝖺' (S.UP f) (S.UP g) (S.UP f) S
                            (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η S UP.unit ?a)"
                    proof -
                      have "S.seq (S.inv (S.cmpUP (g, f)) S S.UP η) (UP.unit ?a)"
                        using assms UP.unit_char UP.cmp_components_are_iso
                              E'.unit_simps(1) S.comp_assoc
                        by presburger 
                      hence "(S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) S
                               (S.UP f S UP.unit ?a) =
                             S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η S UP.unit ?a"
                        using assms UP.unit_char UP.cmp_components_are_iso S.comp_assoc
                              S.whisker_left [of "S.UP f" "S.inv (S.cmpUP (g, f)) S S.UP η" "UP.unit ?a"]
                        by simp
                      thus ?thesis by simp
                    qed
                    thus ?thesis
                      using assms E'.triangle_left UP.cmp_components_are_iso UP.unit_char
                      by argo
                  qed
                  also have "... = S.UP f"
                    using S.strict_lunit' S.strict_runit by simp
                  finally have 1: "((ξ' S S.UP f) S S.𝖺' (S.UP f) (S.UP g) (S.UP f) S
                                     (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η)) S
                                     (S.UP f S UP.unit ?a) = S.UP f"
                    using S.comp_assoc by simp
                  have "(ξ' S S.UP f) S S.𝖺' (S.UP f) (S.UP g) (S.UP f) S
                           (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η) =
                         S.UP f S (S.UP f S S.inv (UP.unit ?a))"
                  proof -
                    have "S.arr (S.UP f)"
                      using assms by simp
                    moreover have "S.iso (S.UP f S UP.unit ?a)"
                      using assms UP.unit_char S.UP_map0_obj by auto
                    moreover have "S.inv (S.UP f S UP.unit ?a) =
                                   S.UP f S S.inv (UP.unit ?a)"
                      using assms a UP.unit_char S.UP_map0_obj by auto
                    ultimately show ?thesis
                      using assms 1 UP.unit_char UP.cmp_components_are_iso
                            S.invert_side_of_triangle(2)
                              [of "S.UP f" "(ξ' S S.UP f) S S.𝖺' (S.UP f) (S.UP g) (S.UP f) S
                                              (S.UP f S S.inv (S.cmpUP (g, f)) S S.UP η)"
                                  "S.UP f S UP.unit ?a"]
                      by presburger
                  qed
                  also have "... = S.UP f S S.inv (UP.unit ?a)"
                  proof -
                    have "«S.UP f S S.inv (UP.unit ?a) :
                             S.UP f S S.UP ?a S S.UP f S UP.map0 ?a»"
                      using assms ide_f f_in_hhom UP.unit_char [of ?a] S.inv_in_hom
                      apply (intro S.hcomp_in_vhom)
                        apply auto[1]
                       apply blast
                      by auto
                    moreover have "S.UP f S UP.map0 ?a = S.UP f"
                      using a S.hcomp_arr_obj S.UP_map0_obj by auto
                    finally show ?thesis
                      using S.comp_cod_arr by blast
                  qed
                  finally show ?thesis by auto
                qed
                thus ?thesis
                  using S.comp_assoc by simp
              qed
              finally show ?thesis by simp
            qed
            thus ?thesis
              using S.comp_assoc by simp
          qed
          also have "... = S.UP 𝗅-1[f] S S.UP 𝗋[f]"
          proof -
             have "S.cmpUP (trg f, f) S (UP.unit ?b S S.UP f) = S.UP 𝗅-1[f]"
             proof -
               have "S.UP f = S.UP 𝗅[f] S S.cmpUP (trg f, f) S (UP.unit (trg f) S S.UP f)"
                 using UP.lunit_coherence iso_lunit S.strict_lunit by simp
               thus ?thesis
                 using UP.image_of_unitor(3) ide_f by presburger
             qed
             moreover have "(S.UP f S S.inv (UP.unit (src f))) S S.inv (S.cmpUP (f, src f))
                              = S.UP 𝗋[f]"
             proof -
               have "S.UP 𝗋[f] S S.cmpUP (f, src f) S (S.UP f S UP.unit (src f)) = S.UP f"
                 using UP.runit_coherence [of f] S.strict_runit by simp
               moreover have "S.iso (S.cmpUP (f, src f) S (S.UP f S UP.unit (src f)))"
                 using UP.unit_char UP.cmp_components_are_iso VV.arr_charSbC S.UP_map0_obj
                 by (intro S.isos_compose) auto
               ultimately have
                 "S.UP 𝗋[f] = S.UP f S S.inv (S.cmpUP (f, src f) S (S.UP f S UP.unit (src f)))"
                 using S.invert_side_of_triangle(2)
                         [of "S.UP f" "S.UP 𝗋[f]" "S.cmpUP (f, src f) S (S.UP f S UP.unit (src f))"]
                       ideD(1) ide_f by blast
               thus ?thesis
                 using ide_f UP.image_of_unitor(2) [of f] by argo
             qed
             ultimately show ?thesis
               using S.comp_assoc by simp
          qed
          also have "... = S.UP (𝗅-1[f]  𝗋[f])"
            by simp
          finally have "S.UP ((ε  f)  𝖺-1[f, g, f]  (f  η)) = S.UP (𝗅-1[f]  𝗋[f])"
            by simp
          moreover have "par ((ε  f)  𝖺-1[f, g, f]  (f  η)) (𝗅-1[f]  𝗋[f])"
          proof -
            have "«(ε  f)  𝖺-1[f, g, f]  (f  η) : f  src f  trg f  f»"
              using E''.triangle_in_hom(1) by simp
            moreover have "«𝗅-1[f]  𝗋[f] : f  src f  trg f  f»" by auto
            ultimately show ?thesis
              by (metis in_homE)
          qed
          ultimately show ?thesis
            using UP.is_faithful by blast
        qed
        thus "(g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g]"
          using E''.triangle_left_implies_right by simp
      qed
      show ?thesis
        using E''.adjoint_equivalence_in_bicategory_axioms E''.adjunction_in_bicategory_axioms
             adjunction_unit_determines_counit adjoint_equivalence_in_bicategory_def
        by metis
    qed

    lemma equivalence_map_extends_to_adjoint_equivalence:
    assumes "equivalence_map f"
    shows "g η ε. adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
    proof -
      obtain g η ε' where E: "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε'"
        using assms equivalence_map_def by auto
      interpret E: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε'
        using E by auto
      obtain ε where A: "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
        using assms equivalence_refines_to_adjoint_equivalence [of f g η]
              E.antipar E.unit_is_iso E.unit_in_hom by auto
      show ?thesis
        using E A by blast
    qed

  end

  subsection "Uniqueness of Adjoints"

  text ‹
    Left and right adjoints determine each other up to isomorphism.
  ›

  context strict_bicategory
  begin

    lemma left_adjoint_determines_right_up_to_iso:
    assumes "adjoint_pair f g" and "adjoint_pair f g'"
    shows "g  g'"
    proof -
      obtain η ε where A: "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
        using assms adjoint_pair_def by auto
      interpret A: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using A by auto
      interpret A: adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg f g η ε ..
      obtain η' ε' where A': "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g' η' ε'"
        using assms adjoint_pair_def by auto
      interpret A': adjunction_in_bicategory V H 𝖺 𝗂 src trg f g' η' ε'
        using A' by auto
      interpret A': adjunction_in_strict_bicategory V H 𝖺 𝗂 src trg f g' η' ε' ..
      let  = "A'.trnlη g ε"
      have "«: g  g'»"
        using A'.trnlη_eq A'.adjoint_transpose_left(1) [of "trg f" g] A.antipar A'.antipar
              hcomp_arr_obj
        by auto
      moreover have "iso "
      proof (intro isoI)
        let  = "A.trnlη g' ε'"
        show "inverse_arrows  "
        proof
          show "ide (  )"
          proof -
            have 1: "ide (trg f)  trg (trg f) = trg f"
              by simp
            have "   = (g'  ε)  ((η'  g)  (g  ε'))  (η  g')"
              using 1 A.antipar A'.antipar A.trnlη_eq [of "trg f" g' ε']
                    A'.trnlη_eq [of "trg f" g ε] comp_assoc A.counit_in_hom A'.counit_in_hom
              by simp
            also have "... = ((g'  ε)  (g'  f  g  ε'))  ((η'  g  f  g')  (η  g'))"
            proof -
              have "(η'  g)  (g  ε') = (η'  g  trg f)  (src f  g  ε')"
                using A.antipar A'.antipar hcomp_arr_obj hcomp_obj_arr [of "src f" "g  ε'"]
                      hseqI'
                by (metis A'.counit_simps(1) A'.counit_simps(5) A.ide_right ideD(1)
                    obj_trg trg_hcomp)
              also have "... = η'  g  ε'"
                using A.antipar A'.antipar interchange [of η' "src f" "g  trg f" "g  ε'"]
                      whisker_left comp_arr_dom comp_cod_arr
                by simp
              also have "... = ((g'  f)  g  ε')  (η'  g  (f  g'))"
                using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar
                      A'.unit_in_hom A'.counit_in_hom interchange whisker_left
                      comp_arr_dom comp_cod_arr
                by (metis A'.counit_simps(1-2,5) A'.unit_simps(1,3) hseqI' ide_char)
              also have "... = (g'  f  g  ε')  (η'  g  f  g')"
                using hcomp_assoc by simp
              finally show ?thesis
                using comp_assoc by simp
            qed
            also have "... = (g'  ε')  ((g'  (ε  f)  g')  (g'  (f  η)  g'))  (η'  g')"
            proof -
              have "(g'  ε)  (g'  f  g  ε') = (g'  ε')  (g'  ε  f  g')"
              proof -
                have "(g'  ε)  (g'  f  g  ε') = g'  ε  ε'"
                proof -
                  have "ε  (f  g  ε') = ε  ε'"
                    using A.ide_left A.ide_right A.antipar A'.antipar hcomp_arr_obj comp_arr_dom
                      comp_cod_arr interchange obj_src trg_src
                    by (metis A'.counit_simps(1,3) A.counit_simps(1-2,4) hcomp_assoc)
                  thus ?thesis
                    using A.antipar A'.antipar whisker_left [of g' ε "f  g  ε'"]
                    by (simp add: hcomp_assoc)
                qed
                also have "... = (g'  ε')  (g'  ε  f  g')"
                proof -
                  have "ε  ε' = ε'  (ε  f  g')"
                    using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar
                          hcomp_obj_arr hcomp_arr_obj comp_arr_dom comp_cod_arr interchange
                          obj_src trg_src
                    by (metis A'.counit_simps(1-2,5) A.counit_simps(1,3-4) arr_cod
                        not_arr_null seq_if_composable)
                  thus ?thesis
                    using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar
                          whisker_left
                    by (metis A'.counit_simps(1,5) A.counit_simps(1,4) hseqI')
                qed
                finally show ?thesis by simp
              qed
              moreover have "(η'  g  f  g')  (η  g') = (g'  f  η  g')  (η'  g')"
              proof -
                have "(η'  g  f  g')  (η  g') = η'  η  g'"
                proof -
                  have "(η'  g  f)  η = η'  η"
                    using A.ide_left A.ide_right A.antipar A'.antipar A'.unit_in_hom hcomp_arr_obj
                          interchange comp_arr_dom comp_cod_arr
                    by (metis A'.unit_simps(1-2,4) A.unit_simps(1,3,5) hcomp_obj_arr obj_trg)
                  thus ?thesis
                    using A.antipar A'.antipar whisker_right [of g' "η'  g  f" η]
                    by (simp add: hcomp_assoc)
                qed
                also have "... = (g'  f  η  g')  (η'  g')"
                proof -
                  have "η'  η = (g'  f  η)  η'"
                    using A.ide_left A.ide_right A.antipar A'.antipar A'.unit_in_hom hcomp_arr_obj
                          comp_arr_dom comp_cod_arr hcomp_assoc interchange
                    by (metis A'.unit_simps(1,3-4) A.unit_simps(1-2) obj_src)
                  thus ?thesis
                    using A.ide_left A.ide_right A.antipar A'.antipar A'.unit_in_hom hcomp_arr_obj
                          whisker_right [of g' "g'  f  η" η']
                    by (metis A'.ide_right A'.unit_simps(1,4) A.unit_simps(1,5)
                        hseqI' hcomp_assoc)
                qed
                finally show ?thesis by simp
              qed
              ultimately show ?thesis
                using comp_assoc hcomp_assoc by simp
            qed
            also have "... = (g'  ε')  ((g'  f)  g')  (η'  g')"
            proof -
              have "(g'  (ε  f)  g')  (g'  (f  η)  g') = g'  f  g'"
              proof -
                have "(g'  (ε  f)  g')  (g'  (f  η)  g') =
                      g'  ((ε  f)  g')  ((f  η)  g')"
                  using A.ide_left A.ide_right A.antipar A'.antipar A'.unit_in_hom
                        A'.counit_in_hom whisker_left [of g' "(ε  f)  g'" "(f  η)  g'"]
                  by (metis A'.ide_right A.triangle_left hseqI' ideD(1) whisker_right)
                also have "... = g'  (ε  f)  (f  η)  g'"
                  using A.antipar A'.antipar whisker_right [of g' "ε  f" "f  η"]
                  by (simp add: A.triangle_left)
                also have "... = g'  f  g'"
                  using A.triangle_left by simp
                finally show ?thesis by simp
              qed
              thus ?thesis
                using hcomp_assoc by simp
            qed
            also have "... = (g'  ε')  (η'  g')"
              using A.antipar A'.antipar A'.unit_in_hom A'.counit_in_hom comp_cod_arr
              by (metis A'.ide_right A'.triangle_in_hom(2) A.ide_left arrI assoc_is_natural_2
                  ide_char seqE strict_assoc)
            also have "... = g'"
              using A'.triangle_right by simp
            finally have "   = g'" by simp
            thus ?thesis by simp
          qed
          show "ide (  )"
          proof -
            have 1: "ide (trg f)  trg (trg f) = trg f"
              by simp
            have "   = (g  ε')  ((η  g')  (g'  ε))  (η'  g)"
              using A.antipar A'.antipar A'.trnlη_eq [of "trg f" g ε]
                    A.trnlη_eq [of "trg f" g' ε'] comp_assoc A.counit_in_hom A'.counit_in_hom
              by simp
            also have "... = ((g  ε')  (g  f  g'  ε))  ((η  g'  f  g)  (η'  g))"
            proof -
              have "(η  g')  (g'  ε) = (η  g'  trg f)  (src f  g'  ε)"
                using A.antipar A'.antipar hcomp_arr_obj hcomp_obj_arr hseqI'
                by (metis A'.ide_right A.unit_simps(1,4) hcomp_assoc hcomp_obj_arr
                    ideD(1) obj_src)
              also have "... = η  g'  ε"
                using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar A.unit_in_hom
                      A.counit_in_hom interchange
                by (metis "1" A.counit_simps(5) A.unit_simps(4) hseqI' ide_def ide_in_hom(2)
                    not_arr_null seqI' src.preserves_ide)
              also have "... = ((g  f)  g'  ε)  (η  g'  (f  g))"
                using A'.ide_right A'.antipar interchange ide_char comp_arr_dom comp_cod_arr hseqI'
                by (metis A.counit_simps(1-2,5) A.unit_simps(1,3))
              also have "... = (g  f  g'  ε)  (η  g'  f  g)"
                using hcomp_assoc by simp
              finally show ?thesis
                using comp_assoc by simp
            qed
            also have "... = (g  ε)  ((g  (ε'  f)  g)  (g  (f  η')  g))  (η  g)"
            proof -
              have "(g  ε')  (g  f  g'  ε) = (g  ε)  (g  ε'  f  g)"
              proof -
                have "(g  ε')  (g  f  g'  ε) = g  ε'  ε"
                proof -
                  have "ε'  (f  g'  ε) = ε'  ε"
                    using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar hcomp_arr_obj
                          comp_arr_dom comp_cod_arr interchange obj_src trg_src hcomp_assoc
                    by (metis A.counit_simps(1,3) A'.counit_simps(1-2,4))
                  thus ?thesis
                    using A.antipar A'.antipar whisker_left [of g ε' "f  g'  ε"]
                    by (simp add: hcomp_assoc)
                qed
                also have "... = (g  ε)  (g  ε'  f  g)"
                proof -
                  have "ε'  ε = ε  (ε'  f  g)"
                    using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar hcomp_obj_arr
                          hcomp_arr_obj comp_arr_dom comp_cod_arr interchange obj_src trg_src
                    by (metis A.counit_simps(1-2,5) A'.counit_simps(1,3-4)
                        arr_cod not_arr_null seq_if_composable)
                  thus ?thesis
                    using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar
                          whisker_left
                    by (metis A.counit_simps(1,5) A'.counit_simps(1,4) hseqI')
                qed
                finally show ?thesis by simp
              qed
              moreover have "(η  g'  f  g)  (η'  g) = (g  f  η'  g)  (η  g)"
              proof -
                have "(η  g'  f  g)  (η'  g) = η  η'  g"
                proof -
                  have "(η  g'  f)  η' = η  η'"
                    using A.antipar A'.antipar A.unit_in_hom hcomp_arr_obj
                          comp_arr_dom comp_cod_arr hcomp_obj_arr interchange
                    by (metis A'.unit_simps(1,3,5) A.unit_simps(1-2,4) obj_trg)
                  thus ?thesis
                    using A.antipar A'.antipar whisker_right [of g "η  g'  f" η']
                    by (simp add: hcomp_assoc)
                qed
                also have "... = ((g  f)  η'  g)  (η  src f  g)"
                  using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar A.unit_in_hom
                        A'.unit_in_hom comp_arr_dom comp_cod_arr interchange
                  by (metis A'.unit_simps(1-2,4) A.unit_simps(1,3) hseqI' ide_char)
                also have "... = (g  f  η'  g)  (η  g)"
                  using A.antipar A'.antipar hcomp_assoc
                  by (simp add: hcomp_obj_arr)
                finally show ?thesis by simp
              qed
              ultimately show ?thesis
                using comp_assoc hcomp_assoc by simp
            qed
            also have "... = (g  ε)  ((g  f)  g)  (η  g)"
            proof -
              have "(g  (ε'  f)  g)  (g  (f  η')  g) = g  f  g"
              proof -
                have "(g  (ε'  f)  g)  (g  (f  η')  g) =
                      g  ((ε'  f)  g)  ((f  η')  g)"
                  using A.ide_left A.ide_right A'.ide_right A.antipar A'.antipar A.unit_in_hom
                        A.counit_in_hom whisker_left
                  by (metis A'.triangle_left hseqI' ideD(1) whisker_right)
                also have "... = g  (ε'  f)  (f  η')  g"
                  using A.antipar A'.antipar whisker_right [of g "ε'  f" "f  η'"]
                  by (simp add: A'.triangle_left)
                also have "... = g  f  g"
                  using A'.triangle_left by simp
                finally show ?thesis by simp
              qed
              thus ?thesis
                using hcomp_assoc by simp
            qed
            also have "... = (g  ε)  (η  g)"
              using A.antipar A'.antipar A.unit_in_hom A.counit_in_hom comp_cod_arr
              by (metis A.ide_left A.ide_right A.triangle_in_hom(2) arrI assoc_is_natural_2
                  ide_char seqE strict_assoc)
            also have "... = g"
              using A.triangle_right by simp
            finally have "   = g" by simp
            moreover have "ide g"
              by simp
            ultimately show ?thesis by simp
          qed
        qed
      qed
      ultimately show ?thesis
        using isomorphic_def by auto
    qed

  end

  text ‹
    We now use strictification to extend to arbitrary bicategories.
  ›

  context 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 UP: fully_faithful_functor V S.vcomp S.UP
      using S.UP_is_fully_faithful_functor by auto

    lemma left_adjoint_determines_right_up_to_iso:
    assumes "adjoint_pair f g" and "adjoint_pair f g'"
    shows "g  g'"
    proof -
      have 0: "ide g  ide g'"
        using assms adjoint_pair_def adjunction_in_bicategory_def
              adjunction_data_in_bicategory_def adjunction_data_in_bicategory_axioms_def
        by metis
      have 1: "S.adjoint_pair (S.UP f) (S.UP g)  S.adjoint_pair (S.UP f) (S.UP g')"
        using assms UP.preserves_adjoint_pair by simp
      obtain ν where ν: "«ν : S.UP g S S.UP g'»  S.iso ν"
        using 1 S.left_adjoint_determines_right_up_to_iso S.isomorphic_def by blast
      obtain μ where μ: "«μ : g  g'»  S.UP μ = ν"
        using 0 ν UP.is_full [of g' g ν] by auto
      have "«μ : g  g'»  iso μ"
        using μ ν UP.reflects_iso by auto
      thus ?thesis
        using isomorphic_def by auto
    qed

    lemma right_adjoint_determines_left_up_to_iso:
    assumes "adjoint_pair f g" and "adjoint_pair f' g"
    shows "f  f'"
    proof -
      obtain η ε where A: "adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
        using assms adjoint_pair_def by auto
      interpret A: adjunction_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using A by auto
      obtain η' ε' where A': "adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g η' ε'"
        using assms adjoint_pair_def by auto
      interpret A': adjunction_in_bicategory V H 𝖺 𝗂 src trg f' g η' ε'
        using A' by auto
      interpret Cop: op_bicategory V H 𝖺 𝗂 src trg ..
      interpret Aop: adjunction_in_bicategory V Cop.H Cop.𝖺 𝗂 Cop.src Cop.trg g f η ε
        using A.antipar A.triangle_left A.triangle_right Cop.assoc_ide_simp
              Cop.lunit_ide_simp Cop.runit_ide_simp
        by (unfold_locales, auto)
      interpret Aop': adjunction_in_bicategory V Cop.H Cop.𝖺 𝗂 Cop.src Cop.trg g f' η' ε'
        using A'.antipar A'.triangle_left A'.triangle_right Cop.assoc_ide_simp
              Cop.lunit_ide_simp Cop.runit_ide_simp
        by (unfold_locales, auto)
      show ?thesis
        using Aop.adjunction_in_bicategory_axioms Aop'.adjunction_in_bicategory_axioms
              Cop.left_adjoint_determines_right_up_to_iso Cop.adjoint_pair_def
        by blast
    qed

  end

  context chosen_right_adjoints
  begin

    lemma isomorphic_to_left_adjoint_implies_isomorphic_right_adjoint:
    assumes "is_left_adjoint f" and "f  h"
    shows "f*  h*"
    proof -
      have 1: "adjoint_pair f f*"
        using assms left_adjoint_extends_to_adjoint_pair by blast
      moreover have "adjoint_pair h f*"
        using assms 1 adjoint_pair_preserved_by_iso isomorphic_symmetric isomorphic_reflexive
        by (meson isomorphic_def right_adjoint_simps(1))
      thus ?thesis
        using left_adjoint_determines_right_up_to_iso left_adjoint_extends_to_adjoint_pair
        by blast
    qed

  end

  context bicategory
  begin

    lemma equivalence_is_adjoint:
    assumes "equivalence_map f"
    shows equivalence_is_left_adjoint: "is_left_adjoint f"
    and equivalence_is_right_adjoint: "is_right_adjoint f"
    proof -
      obtain g η ε where fg: "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
        using assms equivalence_map_extends_to_adjoint_equivalence by blast
      interpret fg: adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using fg by simp
      interpret gf: adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg g f inv ε inv η
        using fg.dual_adjoint_equivalence by simp
      show "is_left_adjoint f"
        using fg.adjunction_in_bicategory_axioms adjoint_pair_def by auto
      show "is_right_adjoint f"
        using gf.adjunction_in_bicategory_axioms adjoint_pair_def by auto
    qed

    lemma right_adjoint_to_equivalence_is_equivalence:
    assumes "equivalence_map f" and "adjoint_pair f g"
    shows "equivalence_map g"
    proof -
      obtain η ε where fg: "adjunction_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε"
        using assms adjoint_pair_def by auto
      interpret fg: adjunction_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g η ε
        using fg by simp
      obtain g' φ ψ where fg': "equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g' φ ψ"
        using assms equivalence_map_def by auto
      interpret fg': equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g' φ ψ
        using fg' by auto
      obtain ψ' where ψ': "adjoint_equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g' φ ψ'"
        using assms equivalence_refines_to_adjoint_equivalence [of f g' φ]
              fg'.antipar fg'.unit_in_hom fg'.unit_is_iso
        by auto
      interpret ψ': adjoint_equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g' φ ψ'
        using ψ' by simp
      have 1: "g  g'"
        using fg.adjunction_in_bicategory_axioms ψ'.adjunction_in_bicategory_axioms
              left_adjoint_determines_right_up_to_iso adjoint_pair_def
        by blast
      obtain γ where γ: "«γ : g'  g»  iso γ"
        using 1 isomorphic_def isomorphic_symmetric by metis
      have "equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg f g ((γ  f)  φ) (ψ'  (f  inv γ))"
        using γ equivalence_preserved_by_iso_right ψ'.equivalence_in_bicategory_axioms by simp
      hence "quasi_inverses f g"
        using quasi_inverses_def by blast
      thus ?thesis
        using equivalence_mapI quasi_inverses_symmetric by blast
    qed

    lemma left_adjoint_to_equivalence_is_equivalence:
    assumes "equivalence_map f" and "adjoint_pair g f"
    shows "equivalence_map g"
    proof -
      obtain η ε where gf: "adjunction_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g f η ε"
        using assms adjoint_pair_def by auto
      interpret gf: adjunction_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g f η ε
        using gf by simp
      obtain g' where 1: "quasi_inverses g' f"
        using assms equivalence_mapE quasi_inverses_symmetric by blast
      obtain φ ψ where g'f: "equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g' f φ ψ"
        using assms 1 quasi_inverses_def by auto
      interpret g'f: equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g' f φ ψ
        using g'f by auto
      obtain ψ' where ψ': "adjoint_equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g' f φ ψ'"
        using assms 1 equivalence_refines_to_adjoint_equivalence [of g' f φ]
              g'f.antipar g'f.unit_in_hom g'f.unit_is_iso quasi_inverses_def
              equivalence_map_def
        by auto
      interpret ψ': adjoint_equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g' f φ ψ'
        using ψ' by simp
      have 1: "g  g'"
        using gf.adjunction_in_bicategory_axioms ψ'.adjunction_in_bicategory_axioms
              right_adjoint_determines_left_up_to_iso adjoint_pair_def
        by blast
      obtain γ where γ: "«γ : g'  g»  iso γ"
        using 1 isomorphic_def isomorphic_symmetric by metis
      have "equivalence_in_bicategory (⋅) (⋆) 𝖺 𝗂 src trg g f ((f  γ)  φ) (ψ'  (inv γ  f))"
        using γ equivalence_preserved_by_iso_left ψ'.equivalence_in_bicategory_axioms by simp
      hence "quasi_inverses g f"
        using quasi_inverses_def by auto
      thus ?thesis
        using quasi_inverses_symmetric quasi_inverses_def equivalence_map_def by blast
    qed

    lemma quasi_inverses_are_adjoint_pair:
    assumes "quasi_inverses f g"
    shows "adjoint_pair f g"
    proof -
      obtain η ε where ηε: "equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε"
        using assms quasi_inverses_def by auto
      interpret ηε: equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε
        using ηε by auto
      obtain ε' where ηε': "adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε'"
        using ηε equivalence_map_def ηε.antipar ηε.unit_in_hom ηε.unit_is_iso
              ηε.ide_right equivalence_refines_to_adjoint_equivalence [of f g η]
        by force
      interpret ηε': adjoint_equivalence_in_bicategory V H 𝖺 𝗂 src trg f g η ε'
        using ηε' by auto
      show ?thesis
        using ηε' adjoint_pair_def ηε'.adjunction_in_bicategory_axioms by auto
    qed

    lemma quasi_inverses_isomorphic_right:
    assumes "quasi_inverses f g"
    shows "quasi_inverses f g'  g  g'"
    proof
      show "g  g'  quasi_inverses f g'"
        using assms quasi_inverses_def isomorphic_def equivalence_preserved_by_iso_right
        by metis
      assume g': "quasi_inverses f g'"
      show "g  g'"
        using assms g' quasi_inverses_are_adjoint_pair left_adjoint_determines_right_up_to_iso
        by blast
    qed

    lemma quasi_inverses_isomorphic_left:
    assumes "quasi_inverses f g"
    shows "quasi_inverses f' g  f  f'"
    proof
      show "f  f'  quasi_inverses f' g"
        using assms quasi_inverses_def isomorphic_def equivalence_preserved_by_iso_left
        by metis
      assume f': "quasi_inverses f' g"
      show "f  f'"
        using assms f' quasi_inverses_are_adjoint_pair right_adjoint_determines_left_up_to_iso
        by blast
    qed      

  end

end