Theory Bicategory

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

theory Bicategory
imports Prebicategory Category3.Subcategory Category3.DiscreteCategory
        MonoidalCategory.MonoidalCategory
begin

  section "Bicategories"

  text ‹
    A \emph{bicategory} is a (vertical) category that has been equipped with
    a horizontal composition, an associativity natural isomorphism,
    and for each object a ``unit isomorphism'', such that horizontal
    composition on the left by target and on the right by source are
    fully faithful endofunctors of the vertical category, and such that
    the usual pentagon coherence condition holds for the associativity.
  ›

  locale bicategory =
    horizontal_composition V H src trg +
    α: natural_isomorphism VVV.comp V HoHV HoVH
         λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ)) +
    L: fully_faithful_functor V V L +
    R: fully_faithful_functor V V R
  for V :: "'a comp"                 (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" +
  assumes unit_in_vhom: "obj a  «𝗂[a] : a  a  a»"
  and iso_unit: "obj a  iso 𝗂[a]"
  and pentagon: " ide f; ide g; ide h; ide k; src f = trg g; src g = trg h; src h = trg k  
                   (f  𝖺[g, h, k])  𝖺[f, g  h, k]  (𝖺[f, g, h]  k) = 𝖺[f, g, h  k]  𝖺[f  g, h, k]"
  begin
    (*
     * TODO: the mapping 𝗂 is not currently assumed to be extensional.
     * It might be best in the long run if it were.
     *)

    definition α
    where "α μντ  𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ))"

    lemma assoc_in_hom':
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "in_hhom 𝖺[μ, ν, τ] (src τ) (trg μ)"
    and "«𝖺[μ, ν, τ] : (dom μ  dom ν)  dom τ  cod μ  cod ν  cod τ»"
    proof -
      show "«𝖺[μ, ν, τ] : (dom μ  dom ν)  dom τ  cod μ  cod ν  cod τ»"
      proof -
        have 1: "VVV.in_hom (μ, ν, τ) (dom μ, dom ν, dom τ) (cod μ, cod ν, cod τ)"
          using assms VVV.in_hom_charSbC VVV.arr_charSbC VV.arr_charSbC by auto
        have "«𝖺[μ, ν, τ] : HoHV (dom μ, dom ν, dom τ)  HoVH (cod μ, cod ν, cod τ)»"
          using 1 α.preserves_hom by auto
        moreover have "HoHV (dom μ, dom ν, dom τ) = (dom μ  dom ν)  dom τ"
          using 1 HoHV_def by (simp add: VVV.in_hom_charSbC)
        moreover have "HoVH (cod μ, cod ν, cod τ) = cod μ  cod ν  cod τ"
          using 1 HoVH_def by (simp add: VVV.in_hom_charSbC)
        ultimately show ?thesis by simp
      qed
      thus "in_hhom 𝖺[μ, ν, τ] (src τ) (trg μ)"
        using assms src_cod trg_cod vconn_implies_hpar(1) vconn_implies_hpar(2) by auto
    qed

    lemma assoc_is_natural_1:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "𝖺[μ, ν, τ] = (μ  ν  τ)  𝖺[dom μ, dom ν, dom τ]"
      using assms α.is_natural_1 [of "(μ, ν, τ)"] VVV.arr_charSbC VV.arr_charSbC VVV.dom_charSbC
            HoVH_def src_dom trg_dom
      by simp

    lemma assoc_is_natural_2:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "𝖺[μ, ν, τ] = 𝖺[cod μ, cod ν, cod τ]  ((μ  ν)  τ)"
      using assms α.is_natural_2 [of "(μ, ν, τ)"] VVV.arr_charSbC VV.arr_charSbC VVV.cod_charSbC
            HoHV_def src_dom trg_dom
      by simp

    lemma assoc_naturality:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "𝖺[cod μ, cod ν, cod τ]  ((μ  ν)  τ) = (μ  ν  τ)  𝖺[dom μ, dom ν, dom τ]"
      using assms α.naturality VVV.arr_charSbC VV.arr_charSbC HoVH_def HoHV_def
            VVV.dom_charSbC VVV.cod_charSbC
      by auto

    lemma assoc_in_hom [intro]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "in_hhom 𝖺[f, g, h] (src h) (trg f)"
    and "«𝖺[f, g, h] : (dom f  dom g)  dom h  cod f  cod g  cod h»"
      using assms assoc_in_hom' apply auto[1]
      using assms assoc_in_hom' ideD(1) by metis

    lemma assoc_simps [simp]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "arr 𝖺[f, g, h]"
    and "src 𝖺[f, g, h] = src h" and "trg 𝖺[f, g, h] = trg f"
    and "dom 𝖺[f, g, h] = (dom f  dom g)  dom h"
    and "cod 𝖺[f, g, h] = cod f  cod g  cod h"
      using assms assoc_in_hom apply auto
      using assoc_in_hom(1) by auto

    lemma iso_assoc [intro, simp]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "iso 𝖺[f, g, h]"
      using assms α.components_are_iso [of "(f, g, h)"] VVV.ide_charSbC VVV.arr_charSbC VV.arr_charSbC
      by simp

  end

  subsection "Categories Induce Bicategories"

  text ‹
    In this section we show that a category becomes a bicategory if we take the vertical
    composition to be discrete, we take the composition of the category as the
    horizontal composition, and we take the vertical domain and codomain as src› and trg›.
  ›

  (*
   * It is helpful to make a few local definitions here, but I don't want them to
   * clutter the category locale.  Using a context and private definitions does not
   * work as expected.  So we have to define a new locale just for the present purpose.
   *)
  locale category_as_bicategory = category
  begin

    interpretation V: discrete_category Collect arr null
      using not_arr_null by (unfold_locales, blast)

    abbreviation V
    where "V  V.comp"

    interpretation src: "functor" V V dom
      using V.null_char
      by (unfold_locales, simp add: has_domain_iff_arr dom_def, auto)
    interpretation trg: "functor" V V cod
      using V.null_char
      by (unfold_locales, simp add: has_codomain_iff_arr cod_def, auto)

    interpretation H: horizontal_homs V dom cod
      by (unfold_locales, auto)

    interpretation H: "functor" H.VV.comp V λμν. fst μν  snd μν
      apply (unfold_locales)
      using H.VV.arr_charSbC V.null_char ext
          apply force
      using H.VV.arr_charSbC V.null_char H.VV.dom_charSbC H.VV.cod_charSbC
         apply auto[3]
    proof -
      show "g f. H.VV.seq g f 
                   fst (H.VV.comp g f)  snd (H.VV.comp g f) = V (fst g  snd g) (fst f  snd f)"
      proof -
        have 0: "f. H.VV.arr f  V.arr (fst f  snd f)"
          using H.VV.arr_charSbC by auto
        have 1: "f g. V.seq g f  V.ide f  g = f"
          using V.arr_char V.dom_char V.cod_char V.not_arr_null by force
        have 2: "f g. H.VxV.seq g f  H.VxV.ide f  g = f"
          using 1 H.VxV.seq_char by (metis H.VxV.dom_eqI H.VxV.ide_Ide)
        fix f g
        assume fg: "H.VV.seq g f"
        have 3: "H.VV.ide f  f = g"
          using fg 2 H.VV.seq_charSbC H.VV.ide_charSbC by blast
        show "fst (H.VV.comp g f)  snd (H.VV.comp g f) = V (fst g  snd g) (fst f  snd f)"
          using fg 0 1 3 H.VV.comp_char H.VV.arr_charSbC H.VV.ide_char V.arr_char V.comp_char
                H.VV.comp_arr_ide
          by (metis (no_types, lifting))
      qed
    qed

    interpretation H: horizontal_composition V C dom cod
      by (unfold_locales, auto)

    abbreviation 𝖺
    where "𝖺 f g h  f  g  h"

    interpretation α: natural_isomorphism H.VVV.comp V H.HoHV H.HoVH
                        λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ))
      apply unfold_locales
      using V.null_char ext
           apply fastforce
      using H.HoHV_def H.HoVH_def H.VVV.arr_charSbC H.VV.arr_charSbC H.VVV.dom_charSbC
            H.VV.dom_charSbC H.VVV.cod_charSbC H.VV.cod_charSbC H.VVV.ide_char comp_assoc
      by auto

    interpretation fully_faithful_functor V V H.R
      using comp_arr_dom by (unfold_locales, auto)
    interpretation fully_faithful_functor V V H.L
      using comp_cod_arr by (unfold_locales, auto)

    abbreviation 𝗂
    where "𝗂  λx. x"

    proposition induces_bicategory:
    shows "bicategory V C 𝖺 𝗂 dom cod"
      apply (unfold_locales, auto simp add: comp_assoc)
      using comp_arr_dom by fastforce

  end

  subsection "Monoidal Categories induce Bicategories"

  text ‹
    In this section we show that our definition of bicategory directly generalizes our
    definition of monoidal category:
    a monoidal category becomes a bicategory when equipped with the constant-ℐ› functors
    as src and trg and ι› as the unit isomorphism from ℐ ⊗ ℐ› to ℐ›.
    There is a slight mismatch because the bicategory locale assumes that the associator
    is given in curried form, whereas for monoidal categories it is given in tupled form.
    Ultimately, the monoidal category locale should be revised to also use curried form,
    which ends up being more convenient in most situations.
  ›

  context monoidal_category
  begin

    interpretation I: constant_functor C C 
      using unit_in_hom by unfold_locales auto
    interpretation horizontal_homs C I.map I.map
      by unfold_locales auto

    lemma CC_eq_VV:
    shows "CC.comp = VV.comp"
    proof -
      have "g f. CC.comp g f = VV.comp g f"
      proof -
        fix f g
        show "CC.comp g f = VV.comp g f"
        proof -
          have "CC.seq g f  CC.comp g f = VV.comp g f"
            using VV.comp_char VV.arr_charSbC CC.seq_char
            by (elim CC.seqE seqE, simp)
          moreover have "¬ CC.seq g f  CC.comp g f = VV.comp g f"
            using VV.seq_charSbC VV.ext VV.null_char CC.ext
            by (metis (no_types, lifting))
          ultimately show ?thesis by blast
        qed
      qed
      thus ?thesis by blast
    qed

    lemma CCC_eq_VVV:
    shows "CCC.comp = VVV.comp"
    proof -
      have "g f. CCC.comp g f = VVV.comp g f"
      proof -
        fix f g
        show "CCC.comp g f = VVV.comp g f"
        proof -
          have "CCC.seq g f  CCC.comp g f = VVV.comp g f"
            by (metis (no_types, lifting) CC.arrE CCC.seqEPC CC_eq_VV I.map_simp
                I.preserves_reflects_arr VV.seq_charSbC VVV.arrISbC VVV.comp_simp VVV.seq_charSbC
                trg_vcomp vseq_implies_hpar(1))
          moreover have "¬ CCC.seq g f  CCC.comp g f = VVV.comp g f"
            using VVV.seq_charSbC VVV.ext VVV.null_char CCC.ext
            by (metis (no_types, lifting))
          ultimately show ?thesis by blast
        qed
      qed
      thus ?thesis by blast
    qed

    interpretation H: "functor" VV.comp C λμν. fst μν  snd μν
      using CC_eq_VV T.functor_axioms by simp
    interpretation H: horizontal_composition C tensor I.map I.map
      by (unfold_locales, simp_all)

    lemma HoHV_eq_ToTC:
    shows "H.HoHV = T.ToTC"
      using H.HoHV_def T.ToTC_def CCC_eq_VVV by presburger

    lemma HoVH_eq_ToCT:
    shows "H.HoVH = T.ToCT"
      using H.HoVH_def T.ToCT_def CCC_eq_VVV by presburger

    interpretation α: natural_isomorphism VVV.comp C H.HoHV H.HoVH α
      using α.natural_isomorphism_axioms CCC_eq_VVV HoHV_eq_ToTC HoVH_eq_ToCT
      by simp

    lemma R'_eq_R:
    shows "H.R = R"
      using H.is_extensional CC_eq_VV CC.arr_char by force

    lemma L'_eq_L:
    shows "H.L = L"
      using H.is_extensional CC_eq_VV CC.arr_char by force

    interpretation R': fully_faithful_functor C C H.R
      using R'_eq_R R.fully_faithful_functor_axioms by auto
    interpretation L': fully_faithful_functor C C H.L
      using L'_eq_L L.fully_faithful_functor_axioms by auto

    lemma obj_char:
    shows "obj a  a = "
      using obj_def [of a] unit_in_hom by fastforce

    proposition induces_bicategory:
    shows "bicategory C tensor (λμ ν τ. α (μ, ν, τ)) (λ_. ι) I.map I.map"
      using obj_char unit_in_hom unit_is_iso pentagon α.is_extensional α.is_natural_1 α.is_natural_2
      by unfold_locales simp_all

  end

  subsection "Prebicategories Extend to Bicategories"

  text ‹
    In this section, we show that a prebicategory with homs and units extends to a bicategory.
    The main work is to show that the endofunctors L› and R› are fully faithful.
    We take the left and right unitor isomorphisms, which were obtained via local
    constructions in the left and right hom-subcategories defined by a specified
    weak unit, and show that in the presence of the chosen sources and targets they
    are the components of a global natural isomorphisms 𝔩› and 𝔯› from the endofunctors
    L› and R› to the identity functor.  A consequence is that functors L› and R› are
    endo-equivalences, hence fully faithful.
  ›

  context prebicategory_with_homs
  begin

    text ‹
      Once it is equipped with a particular choice of source and target for each arrow,
      a prebicategory determines a horizontal composition.
    ›

    lemma induces_horizontal_composition:
    shows "horizontal_composition V H src trg"
    proof -
      interpret H: "functor" VV.comp V λμν. fst μν  snd μν
      proof -
        have "VV.comp = VoV.comp"
          using composable_charPBH by meson
        thus "functor VV.comp V (λμν. fst μν  snd μν)"
          using functor_axioms by argo
      qed
      show "horizontal_composition V H src trg"
        using src_hcomp' trg_hcomp' composable_charPBH not_arr_null
        by (unfold_locales; metis)
    qed

  end

  sublocale prebicategory_with_homs  horizontal_composition V H src trg
    using induces_horizontal_composition by auto

  locale prebicategory_with_homs_and_units =
    prebicategory_with_units +
    prebicategory_with_homs
  begin

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

    text ‹
      The next definitions extend the left and right unitors that were defined locally with
      respect to a particular weak unit, to globally defined versions using the chosen
      source and target for each arrow.
    ›

    definition lunit  ("𝗅[_]")
    where "lunit f  left_hom_with_unit.lunit V H 𝖺 𝗂[trg f] (trg f) f"

    definition runit  ("𝗋[_]")
    where "runit f  right_hom_with_unit.runit V H 𝖺 𝗂[src f] (src f) f"

    lemma lunit_in_hom:
    assumes "ide f"
    shows "«𝗅[f] : src f WC trg f»" and "«𝗅[f] : trg f  f  f»"
    proof -
      interpret Left: subcategory V left (trg f)
        using assms left_hom_is_subcategory by simp
      interpret Left: left_hom_with_unit V H 𝖺 𝗂[trg f] trg f
        using assms obj_is_weak_unit iso_unitPBU by (unfold_locales, auto)
      have 0: "Left.ide f"
        using assms Left.ide_charSbC Left.arr_charSbC left_def composable_charPBH by auto
      show 1: "«𝗅[f] : trg f  f  f»"
        unfolding lunit_def
        using assms 0 Left.lunit_char(1) Left.hom_char HL_def by auto
      show "«𝗅[f] : src f WC trg f»"
        using 1 src_cod trg_cod src_in_sources trg_in_targets
        by (metis arrI vconn_implies_hpar)
    qed

    lemma runit_in_hom:
    assumes "ide f"
    shows "«𝗋[f] : src f WC trg f»" and "«𝗋[f] : f  src f  f»"
    proof -
      interpret Right: subcategory V right (src f)
        using assms right_hom_is_subcategory weak_unit_self_composable by force
      interpret Right: right_hom_with_unit V H 𝖺 𝗂[src f] src f
        using assms obj_is_weak_unit iso_unitPBU by (unfold_locales, auto)
      have 0: "Right.ide f"
        using assms Right.ide_charSbC Right.arr_charSbC right_def composable_charPBH by auto
      show 1: "«𝗋[f] : f  src f  f»"
        unfolding runit_def
        using assms 0 Right.runit_char(1) Right.hom_char HR_def by auto
      show "«𝗋[f] : src f WC trg f»"
        using 1 src_cod trg_cod src_in_sources trg_in_targets
        by (metis arrI vconn_implies_hpar)
    qed

    text ‹
      The characterization of the locally defined unitors yields a corresponding characterization
      of the globally defined versions, by plugging in the chosen source or target for each
      arrow for the unspecified weak unit in the the local versions.
    ›

    lemma lunit_char:
    assumes "ide f"
    shows "«𝗅[f] : src f WC trg f»" and "«𝗅[f] : trg f  f  f»"
    and "trg f  𝗅[f] = (𝗂[trg f]  f)  inv 𝖺[trg f, trg f, f]"
    and "∃!μ. «μ : trg f  f  f»  trg f  μ = (𝗂[trg f]  f)  inv 𝖺[trg f, trg f, f]"
    proof -
      let ?a = "src f" and ?b = "trg f"
      interpret Left: subcategory V left ?b
        using assms left_hom_is_subcategory weak_unit_self_composable by force
      interpret Left: left_hom_with_unit V H 𝖺 𝗂[?b] ?b
        using assms obj_is_weak_unit iso_unitPBU by (unfold_locales, auto)
      have 0: "Left.ide f"
        using assms Left.ide_charSbC Left.arr_charSbC left_def composable_charPBH by auto
      show "«𝗅[f] : src f WC trg f»"
        using assms lunit_in_hom by simp
      show A: "«𝗅[f] : trg f  f  f»"
        using assms lunit_in_hom by simp
      show B: "?b  𝗅[f] = (𝗂[?b]  f)  inv 𝖺[?b, ?b, f]"
        unfolding lunit_def using 0 Left.lunit_char(2) HL_def
        by (metis Left.comp_simp Left.characteristic_iso(1-2) Left.seqI')
      show "∃!μ. «μ : trg f  f  f»  trg f  μ = (𝗂[?b]  f)  inv 𝖺[?b, ?b, f]"
      proof -
        have 1: "hom (trg f  f) f = Left.hom (Left.L f) f"
        proof
          have 1: "Left.L f = ?b  f"
          using 0 HL_def by simp
          show "Left.hom (Left.L f) f  hom (?b  f) f"
            using assms Left.hom_char [of "?b  f" f] HL_def by simp
          show "hom (?b  f) f  Left.hom (Left.L f) f"
            using assms 1 ide_in_hom composable_charPBH hom_connected left_def
                  Left.hom_char
            by auto
        qed
        let ?P = "λμ. Left.in_hom μ (Left.L f) f"
        let ?P' = "λμ. «μ : ?b  f  f»"
        let ?Q = "λμ. Left.L μ = (𝗂[?b]  f)  (inv 𝖺[?b, ?b, f])"
        let ?R = "λμ. ?b  μ = (𝗂[?b]  f)  (inv 𝖺[?b, ?b, f])"
        have 2: "?P = ?P'"
          using 0 1 HL_def Left.hom_char by blast
        moreover have "μ. ?P μ  (?Q μ  ?R μ)"
          using 2 Left.lunit_eqI HL_def by presburger
        moreover have "(∃!μ. ?P μ  ?Q μ)"
          using 0 2 A B Left.lunit_char(3) Left.ide_char Left.arr_charSbC
          by (metis (no_types, lifting) Left.lunit_char(2) calculation(2) lunit_def)
        ultimately show ?thesis by metis
      qed
    qed

    lemma runit_char:
    assumes "ide f"
    shows "«𝗋[f] : src f WC trg f»" and "«𝗋[f] : f  src f  f»"
    and "𝗋[f]  src f = (f  𝗂[src f])  𝖺[f, src f, src f]"
    and "∃!μ. «μ : f  src f  f»  μ  src f = (f  𝗂[src f])  𝖺[f, src f, src f]"
    proof -
      let ?a = "src f" and ?b = "trg f"
      interpret Right: subcategory V right ?a
        using assms right_hom_is_subcategory weak_unit_self_composable by force
      interpret Right: right_hom_with_unit V H 𝖺 𝗂[?a] ?a
        using assms obj_is_weak_unit iso_unitPBU by (unfold_locales, auto)
      have 0: "Right.ide f"
        using assms Right.ide_charSbC Right.arr_charSbC right_def composable_charPBH by auto
      show "«𝗋[f] : src f WC trg f»"
        using assms runit_in_hom by simp
      show A: "«𝗋[f] : f  src f  f»"
        using assms runit_in_hom by simp
      show B: "𝗋[f]  ?a = (f  𝗂[?a])  𝖺[f, ?a, ?a]"
        unfolding runit_def using 0 Right.runit_char(2) HR_def
        using Right.comp_simp Right.characteristic_iso(4) Right.iso_is_arr by auto
      show "∃!μ. «μ : f  src f  f»  μ  ?a = (f  𝗂[?a])  𝖺[f, ?a, ?a]"
      proof -
        have 1: "hom (f  ?a) f = Right.hom (Right.R f) f"
        proof
          have 1: "Right.R f = f  ?a"
          using 0 HR_def by simp
          show "Right.hom (Right.R f) f  hom (f  ?a) f"
            using assms Right.hom_char [of "f  ?a" f] HR_def by simp
          show "hom (f  ?a) f  Right.hom (Right.R f) f"
            using assms 1 ide_in_hom composable_charPBH hom_connected right_def
                  Right.hom_char
            by auto
        qed
        let ?P = "λμ. Right.in_hom μ (Right.R f) f"
        let ?P' = "λμ. «μ : f  ?a  f»"
        let ?Q = "λμ. Right.R μ = (f  𝗂[?a])  𝖺[f, ?a, ?a]"
        let ?R = "λμ. μ  ?a = (f  𝗂[?a])  𝖺[f, ?a, ?a]"
        have 2: "?P = ?P'"
          using 0 1 HR_def Right.hom_char by blast
        moreover have "μ. ?P μ  (?Q μ  ?R μ)"
          using 2 Right.runit_eqI HR_def by presburger
        moreover have "(∃!μ. ?P μ  ?Q μ)"
          using 0 2 A B Right.runit_char(3) Right.ide_char Right.arr_charSbC
          by (metis (no_types, lifting) Right.runit_char(2) calculation(2) runit_def)
        ultimately show ?thesis by metis
      qed
    qed

    lemma lunit_eqI:
    assumes "ide f" and "«μ : trg f  f  f»"
    and "trg f  μ = (𝗂[trg f]  f)  (inv 𝖺[trg f, trg f, f])"
    shows "μ = 𝗅[f]"
      using assms lunit_char(2-4) by blast

    lemma runit_eqI:
    assumes "ide f" and "«μ : f  src f  f»"
    and "μ  src f = (f  𝗂[src f])  𝖺[f, src f, src f]"
    shows "μ = 𝗋[f]"
      using assms runit_char(2-4) by blast

    lemma iso_lunit:
    assumes "ide f"
    shows "iso 𝗅[f]"
    proof -
      let ?b = "trg f"
      interpret Left: subcategory V left ?b
        using assms left_hom_is_subcategory weak_unit_self_composable by force
      interpret Left: left_hom_with_unit V H 𝖺 𝗂[?b] ?b
        using assms obj_is_weak_unit iso_unitPBU by (unfold_locales, auto)
      show ?thesis
      proof -
        have 0: "Left.ide f"
          using assms Left.ide_charSbC Left.arr_charSbC left_def composable_charPBH by auto
        thus ?thesis
          unfolding lunit_def using Left.iso_lunit Left.iso_char by blast
      qed
    qed

    lemma iso_runit:
    assumes "ide f"
    shows "iso 𝗋[f]"
    proof -
      let ?a = "src f"
      interpret Right: subcategory V right ?a
        using assms right_hom_is_subcategory weak_unit_self_composable by force
      interpret Right: right_hom_with_unit V H 𝖺 𝗂[?a] ?a
        using assms obj_is_weak_unit iso_unitPBU by (unfold_locales, auto)
      show ?thesis
      proof -
        have 0: "Right.ide f"
          using assms Right.ide_charSbC Right.arr_charSbC right_def composable_charPBH by auto
        thus ?thesis
          unfolding runit_def using Right.iso_runit Right.iso_char by blast
      qed
    qed

    lemma lunit_naturality:
    assumes "arr μ"
    shows "μ  𝗅[dom μ] = 𝗅[cod μ]  (trg μ  μ)"
    proof -
      let ?a = "src μ" and ?b = "trg μ"
      interpret Left: subcategory V left ?b
        using assms obj_trg left_hom_is_subcategory weak_unit_self_composable by force
      interpret Left: left_hom_with_unit V H 𝖺 𝗂[?b] ?b
        using assms obj_is_weak_unit iso_unitPBU by (unfold_locales, auto)
      interpret Left.L: endofunctor Left ?b Left.L
        using assms endofunctor_HL [of ?b] weak_unit_self_composable obj_trg obj_is_weak_unit
        by blast
      have 1: "Left.in_hom μ (dom μ) (cod μ)"
        using assms Left.hom_char Left.arr_charSbC left_def composable_charPBH obj_trg by auto
      have 2: "Left.in_hom 𝗅[Left.dom μ] (?b  dom μ) (dom μ)"
        unfolding lunit_def
        using assms 1 Left.in_hom_charSbC trg_dom Left.lunit_char(1) HL_def
              Left.arr_charSbC Left.dom_charSbC Left.ide_dom
        by force
      have 3: "Left.in_hom 𝗅[Left.cod μ] (?b  cod μ) (cod μ)"
        unfolding lunit_def
        using assms 1 Left.in_hom_charSbC trg_cod Left.lunit_char(1) HL_def
              Left.cod_charSbC Left.ide_cod
        by force
      have 4: "Left.in_hom (Left.L μ) (?b  dom μ) (?b  cod μ)"
        using 1 Left.L.preserves_hom [of μ "dom μ" "cod μ"] HL_def by auto
      show ?thesis
        by (metis "1" "2" HL_def Left.comp_simp Left.in_homE Left.lunit_naturality
            Left.seqI' lunit_def trg_cod trg_dom)
    qed

    lemma runit_naturality:
    assumes "arr μ"
    shows "μ  𝗋[dom μ] = 𝗋[cod μ]  (μ  src μ)"
    proof -
      let ?a = "src μ" and ?b = "trg μ"
      interpret Right: subcategory V right ?a
        using assms right_hom_is_subcategory weak_unit_self_composable by force
      interpret Right: right_hom_with_unit V H 𝖺 𝗂[?a] ?a
        using assms obj_is_weak_unit iso_unitPBU by (unfold_locales, auto)
      interpret Right.R: endofunctor Right ?a Right.R
        using assms endofunctor_HR [of ?a] weak_unit_self_composable obj_src obj_is_weak_unit
        by blast
      have 1: "Right.in_hom μ (dom μ) (cod μ)"
        using assms Right.hom_char Right.arr_charSbC right_def composable_charPBH by auto
      have 2: "Right.in_hom 𝗋[Right.dom μ] (dom μ  ?a) (dom μ)"
        unfolding runit_def
        using 1 Right.in_hom_charSbC trg_dom Right.runit_char(1) [of "Right.dom μ"] HR_def
              Right.arr_charSbC Right.dom_charSbC Right.ide_dom assms
        by force
      have 3: "𝗋[Right.cod μ]  Right.hom (cod μ  ?a) (cod μ)"
        unfolding runit_def
        using 1 Right.in_hom_charSbC trg_cod Right.runit_char(1) [of "Right.cod μ"] HR_def
              Right.cod_charSbC Right.ide_cod assms
        by force
      have 4: "Right.R μ  Right.hom (dom μ  ?a) (cod μ  ?a)"
        using 1 Right.R.preserves_hom [of μ "dom μ" "cod μ"] HR_def by auto
      show ?thesis
        by (metis "1" "2" HR_def Right.comp_simp Right.in_homE Right.runit_naturality
            Right.seqI' runit_def src_cod src_dom)
    qed

    interpretation L: endofunctor V L
      using endofunctor_L by auto
    interpretation 𝔩: transformation_by_components V V L map lunit
      using lunit_in_hom lunit_naturality by unfold_locales auto
    interpretation 𝔩: natural_isomorphism V V L map 𝔩.map
      using iso_lunit by unfold_locales auto

    lemma natural_isomorphism_𝔩:
    shows "natural_isomorphism V V L map 𝔩.map"
      ..

    interpretation L: equivalence_functor V V L
      using L.isomorphic_to_identity_is_equivalence 𝔩.natural_isomorphism_axioms by simp

    lemma equivalence_functor_L:
    shows "equivalence_functor V V L"
      ..

    lemma lunit_commutes_with_L:
    assumes "ide f"
    shows "𝗅[L f] = L 𝗅[f]"
    proof -
      have "seq 𝗅[f] (L 𝗅[f])"
        using assms lunit_char(2) L.preserves_hom by fastforce
      moreover have "seq 𝗅[f] 𝗅[L f]"
        using assms lunit_char(2) lunit_char(2) [of "L f"] L.preserves_ide by auto
      ultimately show ?thesis
        using assms lunit_char(2) [of f] lunit_naturality [of "𝗅[f]"] iso_lunit
              iso_is_section section_is_mono monoE [of "𝗅[f]" "L 𝗅[f]" "𝗅[L f]"]
        by auto
    qed

    interpretation R: endofunctor V R
      using endofunctor_R by auto
    interpretation 𝔯: transformation_by_components V V R map runit
      using runit_in_hom runit_naturality by unfold_locales auto
    interpretation 𝔯: natural_isomorphism V V R map 𝔯.map
      using iso_runit by unfold_locales auto

    lemma natural_isomorphism_𝔯:
    shows "natural_isomorphism V V R map 𝔯.map"
      ..

    interpretation R: equivalence_functor V V R
      using R.isomorphic_to_identity_is_equivalence 𝔯.natural_isomorphism_axioms by simp

    lemma equivalence_functor_R:
    shows "equivalence_functor V V R"
      ..

    lemma runit_commutes_with_R:
    assumes "ide f"
    shows "𝗋[R f] = R 𝗋[f]"
    proof -
      have "seq 𝗋[f] (R 𝗋[f])"
        using assms runit_char(2) R.preserves_hom by fastforce
      moreover have "seq 𝗋[f] 𝗋[R f]"
        using assms runit_char(2) runit_char(2) [of "R f"] R.preserves_ide by auto
      ultimately show ?thesis
        using assms runit_char(2) [of f] runit_naturality [of "𝗋[f]"] iso_runit
              iso_is_section section_is_mono monoE [of "𝗋[f]" "R 𝗋[f]" "𝗋[R f]"]
        by auto
    qed

    definition α
    where "α μ ν τ  if VVV.arr (μ, ν, τ) then
                        (μ  ν  τ)  𝖺[dom μ, dom ν, dom τ]
                      else null"

    lemma α_ide_simp [simp]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "α f g h = 𝖺[f, g, h]"
    proof -
      have "α f g h = (f  g  h)  𝖺[dom f, dom g, dom h]"
        using assms α_def VVV.arr_charSbC [of "(f, g, h)"] by auto
      also have "... = (f  g  h)  𝖺[f, g, h]"
        using assms by simp
      also have "... = 𝖺[f, g, h]"
        using assms α_def assoc_in_homAWC hcomp_in_homPBH VVV.arr_charSbC VoV.arr_charSbC
              comp_cod_arr composable_charPBH
        by auto
      finally show ?thesis by simp
    qed

    (* TODO: Figure out how this got reinstated. *)
    no_notation in_hom      ("«_ : _  _»")

    lemma natural_isomorphism_α:
    shows "natural_isomorphism VVV.comp V HoHV HoVH
             (λμντ. α (fst μντ) (fst (snd μντ)) (snd (snd μντ)))"
    proof -
      interpret α: transformation_by_components VVV.comp V HoHV HoVH
                     λf. 𝖺[fst f, fst (snd f), snd (snd f)]
      proof
        show 1: "x. VVV.ide x  «𝖺[fst x, fst (snd x), snd (snd x)] : HoHV x  HoVH x»"
        proof -
          fix x
          assume x: "VVV.ide x"
          show "«𝖺[fst x, fst (snd x), snd (snd x)] : HoHV x  HoVH x»"
          proof -
            have "ide (fst x)  ide (fst (snd x))  ide (snd (snd x)) 
                  fst x  fst (snd x)  null  fst (snd x)  snd (snd x)  null"
              using x VVV.ide_charSbC VVV.arr_charSbC VV.arr_charSbC composable_charPBH by simp
            hence "𝖺[fst x, fst (snd x), snd (snd x)]
                      hom ((fst x  fst (snd x))  snd (snd x))
                             (fst x  fst (snd x)  snd (snd x))"
              using x assoc_in_homAWC by simp
            thus ?thesis
              unfolding HoHV_def HoVH_def
              using x VVV.ideD(1) by simp
          qed
        qed
        show "f. VVV.arr f 
                   𝖺[fst (VVV.cod f), fst (snd (VVV.cod f)), snd (snd (VVV.cod f))]  HoHV f =
                   HoVH f  𝖺[fst (VVV.dom f), fst (snd (VVV.dom f)), snd (snd (VVV.dom f))]"
          unfolding HoHV_def HoVH_def
          using assoc_naturalityAWC VVV.arr_charSbC VV.arr_charSbC VVV.dom_charSbC VVV.cod_charSbC
                composable_charPBH
          by simp
      qed
      interpret α: natural_isomorphism VVV.comp V HoHV HoVH α.map
      proof
        fix f
        assume f: "VVV.ide f"
        show "iso (α.map f)"
        proof -
          have "fst f  fst (snd f)  null  fst (snd f)  snd (snd f)  null"
            using f VVV.ideD(1) VVV.arr_charSbC [of f] VV.arr_charSbC composable_charPBH by auto
          thus ?thesis
            using f α.map_simp_ide iso_assocAWC VVV.ide_charSbC VVV.arr_charSbC by simp
        qed
      qed
      have "(λμντ. α (fst μντ) (fst (snd μντ)) (snd (snd μντ))) = α.map"
      proof
        fix μντ
        have "¬ VVV.arr μντ  α (fst μντ) (fst (snd μντ)) (snd (snd μντ)) = α.map μντ"
          using α_def α.map_def by simp
        moreover have "VVV.arr μντ 
                         α (fst μντ) (fst (snd μντ)) (snd (snd μντ)) = α.map μντ"
        proof -
          assume μντ: "VVV.arr μντ"
          have "α (fst μντ) (fst (snd μντ)) (snd (snd μντ)) =
                (fst μντ  fst (snd μντ)  snd (snd μντ)) 
                  𝖺[dom (fst μντ), dom (fst (snd μντ)), dom (snd (snd μντ))]"
            using μντ α_def by simp
          also have "... = 𝖺[cod (fst μντ), cod (fst (snd μντ)), cod (snd (snd μντ))] 
                             ((fst μντ  fst (snd μντ))  snd (snd μντ))"
            using μντ HoHV_def HoVH_def VVV.arr_charSbC VV.arr_charSbC assoc_naturalityAWC
                  composable_charPBH
            by simp
          also have "... =
                     𝖺[fst (VVV.cod μντ), fst (snd (VVV.cod μντ)), snd (snd (VVV.cod μντ))] 
                       ((fst μντ  fst (snd μντ))  snd (snd μντ))"
            using μντ VVV.arr_charSbC VVV.cod_charSbC VV.arr_charSbC by simp
          also have "... = α.map μντ"
            using μντ α.map_def HoHV_def composable_charPBH by auto
          finally show ?thesis by blast
        qed
        ultimately show "α (fst μντ) (fst (snd μντ)) (snd (snd μντ)) = α.map μντ" by blast
      qed
      thus ?thesis using α.natural_isomorphism_axioms by simp
    qed

    proposition induces_bicategory:
    shows "bicategory V H α 𝗂 src trg"
    proof -
      interpret VxVxV: product_category V VxV.comp ..
      interpret VoVoV: subcategory VxVxV.comp
                       λτμν. arr (fst τμν)  VV.arr (snd τμν) 
                              src (fst τμν) = trg (fst (snd τμν))
        using subcategory_VVV by blast
      interpret HoHV: "functor" VVV.comp V HoHV
        using functor_HoHV by blast
      interpret HoVH: "functor" VVV.comp V HoVH
        using functor_HoVH by blast
      interpret α: natural_isomorphism VVV.comp V HoHV HoVH
                     λμντ. α (fst μντ) (fst (snd μντ)) (snd (snd μντ))
        using natural_isomorphism_α by blast
      interpret L: equivalence_functor V V L
        using equivalence_functor_L by blast
      interpret R: equivalence_functor V V R
        using equivalence_functor_R by blast
      show "bicategory V H α 𝗂 src trg"
      proof
        show "a. obj a  «𝗂[a] : a  a  a»"
          using obj_is_weak_unit unit_in_vhomPBU by blast
        show "a. obj a  iso 𝗂[a]"
          using obj_is_weak_unit iso_unitPBU by blast
        show "f g h k.  ide f; ide g; ide h; ide k;
                          src f = trg g; src g = trg h; src h = trg k  
                          (f  α g h k)  α f (g  h) k  (α f g h  k) =
                          α f g (h  k)  α (f  g) h k"
        proof -
          fix f g h k
          assume f: "ide f" and g: "ide g" and h: "ide h" and k: "ide k"
          and fg: "src f = trg g" and gh: "src g = trg h" and hk: "src h = trg k"
          have "sources f  targets g  {}"
            using f g fg src_in_sources [of f] trg_in_targets ideD(1) by auto
          moreover have "sources g  targets h  {}"
            using g h gh src_in_sources [of g] trg_in_targets ideD(1) by auto
          moreover have "sources h  targets k  {}"
            using h k hk src_in_sources [of h] trg_in_targets ideD(1) by auto
          moreover have "α f g h = 𝖺[f, g, h]  α g h k = 𝖺[g, h, k]"
            using f g h k fg gh hk α_ide_simp by simp
          moreover have "α f (g  h) k = 𝖺[f, g  h, k]  α f g (h  k) = 𝖺[f, g, h  k] 
                         α (f  g) h k = 𝖺[f  g, h, k]"
            using f g h k fg gh hk α_ide_simp preserves_ide hcomp_in_homPBH(1) by simp
          ultimately show "(f  α g h k)  α f (g  h) k  (α f g h  k) =
                           α f g (h  k)  α (f  g) h k"
            using f g h k fg gh hk pentagonAWC [of f g h k] α_ide_simp by presburger
        qed
      qed
    qed

  end

  text ‹
    The following is the main result of this development:
    Every prebicategory extends to a bicategory, by making an arbitrary choice of
    representatives of each isomorphism class of weak units and using that to
    define the source and target mappings, and then choosing an arbitrary isomorphism
    in hom (a ⋆ a) a› for each weak unit a›.
  ›

  context prebicategory
  begin

    interpretation prebicategory_with_homs V H 𝖺 some_src some_trg
      using extends_to_prebicategory_with_homs by auto

    interpretation prebicategory_with_units V H 𝖺 some_unit
      using extends_to_prebicategory_with_units by auto

    interpretation prebicategory_with_homs_and_units V H 𝖺 some_unit some_src some_trg ..

    theorem extends_to_bicategory:
    shows "bicategory V H α some_unit some_src some_trg"
      using induces_bicategory by simp

  end

  section "Bicategories as Prebicategories"

  subsection "Bicategories are Prebicategories"

  text ‹
    In this section we show that a bicategory determines a prebicategory with homs,
    whose weak units are exactly those arrows that are isomorphic to their chosen source,
    or equivalently, to their chosen target.
    Moreover, the notion of horizontal composability, which in a bicategory is determined
    by the coincidence of chosen sources and targets, agrees with the version defined
    for the induced weak composition in terms of nonempty intersections of source and
    target sets, which is not dependent on any arbitrary choices.
  ›

  context bicategory
  begin

    (* TODO: Why does this get re-introduced? *)
    no_notation in_hom        ("«_ : _  _»")

    interpretation α': inverse_transformation VVV.comp V HoHV HoVH
                         λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ)) ..

    abbreviation α'
    where "α'  α'.map"

    definition 𝖺'  ("𝖺-1[_, _, _]")
    where "𝖺-1[μ, ν, τ]  α'.map (μ, ν, τ)"

    lemma assoc'_in_hom':
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "in_hhom 𝖺-1[μ, ν, τ] (src τ) (trg μ)"
    and "«𝖺-1[μ, ν, τ] : dom μ  dom ν  dom τ  (cod μ  cod ν)  cod τ»"
    proof -
      show "«𝖺-1[μ, ν, τ] : dom μ  dom ν  dom τ  (cod μ  cod ν)  cod τ»"
      proof -
        have 1: "VVV.in_hom (μ, ν, τ) (dom μ, dom ν, dom τ) (cod μ, cod ν, cod τ)"
          using assms VVV.in_hom_charSbC VVV.arr_charSbC VV.arr_charSbC by auto
        have "«𝖺-1[μ, ν, τ] : HoVH (dom μ, dom ν, dom τ)  HoHV (cod μ, cod ν, cod τ)»"
          using 1 𝖺'_def α'.preserves_hom by auto
        moreover have "HoVH (dom μ, dom ν, dom τ) = dom μ  dom ν  dom τ"
          using 1 HoVH_def by (simp add: VVV.in_hom_charSbC)
        moreover have "HoHV (cod μ, cod ν, cod τ) = (cod μ  cod ν)  cod τ"
          using 1 HoHV_def by (simp add: VVV.in_hom_charSbC)
        ultimately show ?thesis by simp
      qed
      thus "in_hhom 𝖺-1[μ, ν, τ] (src τ) (trg μ)"
        using assms vconn_implies_hpar(1) vconn_implies_hpar(2) by auto
    qed

    lemma assoc'_is_natural_1:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "𝖺-1[μ, ν, τ] = ((μ  ν)  τ)  𝖺-1[dom μ, dom ν, dom τ]"
      using assms α'.is_natural_1 [of "(μ, ν, τ)"] VVV.arr_charSbC VV.arr_charSbC
            VVV.dom_charSbC HoHV_def src_dom trg_dom 𝖺'_def
      by simp

    lemma assoc'_is_natural_2:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "𝖺-1[μ, ν, τ] = 𝖺-1[cod μ, cod ν, cod τ]  (μ  ν  τ)"
      using assms α'.is_natural_2 [of "(μ, ν, τ)"] VVV.arr_charSbC VV.arr_charSbC
            VVV.cod_charSbC HoVH_def src_dom trg_dom 𝖺'_def
      by simp

    lemma assoc'_naturality:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "𝖺-1[cod μ, cod ν, cod τ]  (μ  ν  τ) = ((μ  ν)  τ)  𝖺-1[dom μ, dom ν, dom τ]"
      using assms assoc'_is_natural_1 assoc'_is_natural_2 by metis

    lemma assoc'_in_hom [intro]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "in_hhom 𝖺-1[f, g, h] (src h) (trg f)"
    and "«𝖺-1[f, g, h] : dom f  dom g  dom h  (cod f  cod g)  cod h»"
      using assms assoc'_in_hom'(1-2) ideD(1) by meson+

    lemma assoc'_simps [simp]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "arr 𝖺-1[f, g, h]"
    and "src 𝖺-1[f, g, h] = src h" and "trg 𝖺-1[f, g, h] = trg f"
    and "dom 𝖺-1[f, g, h] = dom f  dom g  dom h"
    and "cod 𝖺-1[f, g, h] = (cod f  cod g)  cod h"
      using assms assoc'_in_hom by blast+

    lemma assoc'_eq_inv_assoc [simp]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "𝖺-1[f, g, h] = inv 𝖺[f, g, h]"
      using assms VVV.ide_charSbC VVV.arr_charSbC VV.ide_charSbC VV.arr_charSbC α'.map_ide_simp
            𝖺'_def
      by auto

    lemma inverse_assoc_assoc' [intro]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "inverse_arrows 𝖺[f, g, h] 𝖺-1[f, g, h]"
      using assms VVV.ide_charSbC VVV.arr_charSbC VV.ide_charSbC VV.arr_charSbC α'.map_ide_simp
            α'.inverts_components 𝖺'_def
      by auto

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

    lemma comp_assoc_assoc' [simp]:
    assumes "ide f" and "ide g" and "ide h"
    and "src f = trg g" and "src g = trg h"
    shows "𝖺[f, g, h]  𝖺-1[f, g, h] = f  g  h"
    and "𝖺-1[f, g, h]  𝖺[f, g, h] = (f  g)  h"
      using assms comp_arr_inv' comp_inv_arr' by auto

    lemma unit_in_hom [intro, simp]:
    assumes "obj a"
    shows "«𝗂[a] : a  a»" and "«𝗂[a] : a  a  a»"
    proof -
      show "«𝗂[a] : a  a  a»"
        using assms unit_in_vhom by simp
      thus "«𝗂[a] : a  a»"
        using assms
        by (metis arrI in_hhom_def obj_simps(2-3) vconn_implies_hpar(1-4))
    qed

    interpretation weak_composition V H
      using is_weak_composition by auto

    lemma seq_if_composable:
    assumes "ν  μ  null"
    shows "src ν = trg μ"
      using assms H.is_extensional [of "(ν, μ)"] VV.arr_charSbC by auto

    lemma obj_self_composable:
    assumes "obj a"
    shows "a  a  null"
    and "isomorphic (a  a) a"
       apply (metis arr_dom_iff_arr assms in_homE not_arr_null unit_in_vhom)
      by (meson assms iso_unit isomorphic_def unit_in_vhom)

    lemma obj_is_weak_unit:
    assumes "obj a"
    shows "weak_unit a"
    proof -
      interpret Left_a: subcategory V left a
        using assms left_hom_is_subcategory by force
      interpret Right_a: subcategory V right a
        using assms right_hom_is_subcategory by force

      text ‹
        We know that HL a› is fully faithful as a global endofunctor,
        but the definition of weak unit involves its restriction to a
        subcategory.  So we have to verify that the restriction
        is also a fully faithful functor.
      ›

      interpret La: endofunctor Left a HL a
        using assms obj_self_composable endofunctor_HL [of a] by force
      interpret La: fully_faithful_functor Left a Left a HL a
      proof
        show "f f'. Left_a.par f f'  HL a f = HL a f'  f = f'"
        proof -
          fix μ μ'
          assume par: "Left_a.par μ μ'"
          assume eq: "HL a μ = HL a μ'"
          have 1: "par μ μ'"
            using par Left_a.arr_charSbC Left_a.dom_charSbC Left_a.cod_charSbC left_def
                  composable_implies_arr null_agreement
            by metis
          moreover have "L μ = L μ'"
            using par eq HL_def Left_a.arr_charSbC left_def preserves_arr
                  assms 1 seq_if_composable [of a μ] not_arr_null seq_if_composable [of a μ']
            by auto
          ultimately show "μ = μ'"
            using L.is_faithful by blast
        qed
        show "f g μ.  Left_a.ide f; Left_a.ide g; Left_a.in_hom μ (HL a f) (HL a g)  
                        ν. Left_a.in_hom ν f g  HL a ν = μ"
        proof -
          fix f g μ
          assume f: "Left_a.ide f" and g: "Left_a.ide g"
          and μ: "Left_a.in_hom μ (HL a f) (HL a g)"
          have 1: "a = trg f  a = trg g"
            using assms f g Left_a.ide_char Left_a.arr_charSbC left_def seq_if_composable [of a f]
                  seq_if_composable [of a g]
            by auto
          show "ν. Left_a.in_hom ν f g  HL a ν = μ"
          proof -
            have 2: "ν. «ν : f  g»  L ν = μ"
              using f g μ 1 Left_a.ide_charSbC HL_def L.preserves_reflects_arr Left_a.arr_charSbC
                    Left_a.in_hom_charSbC L.is_full
              by force
            obtain ν where ν: "«ν : f  g»  L ν = μ"
              using 2 by blast
            have "Left_a.arr ν"
              using ν 1 trg_dom Left_a.arr_charSbC left_def hseq_char' by fastforce
            moreover have "HL a ν = μ"
              using ν 1 trg_dom HL_def by auto
            ultimately show ?thesis
              using ν Left_a.dom_simp Left_a.cod_simp by blast
          qed
        qed
      qed
      interpret Ra: endofunctor Right a HR a
        using assms obj_self_composable endofunctor_HR [of a] by force
      interpret Ra: fully_faithful_functor Right a Right a HR a
      proof
        show "f f'. Right_a.par f f'  HR a f = HR a f'  f = f'"
        proof -
          fix μ μ'
          assume par: "Right_a.par μ μ'"
          assume eq: "HR a μ = HR a μ'"
          have 1: "par μ μ'"
            using par Right_a.arr_charSbC Right_a.dom_charSbC Right_a.cod_charSbC right_def
                  composable_implies_arr null_agreement
            by metis
          moreover have "R μ = R μ'"
            using par eq HR_def Right_a.arr_charSbC right_def preserves_arr
                  assms 1 seq_if_composable [of μ a] not_arr_null seq_if_composable [of μ' a]
            by auto
          ultimately show "μ = μ'"
            using R.is_faithful by blast
        qed
        show "f g μ.  Right_a.ide f; Right_a.ide g; Right_a.in_hom μ (HR a f) (HR a g)  
                        ν. Right_a.in_hom ν f g  HR a ν = μ"
        proof -
          fix f g μ
          assume f: "Right_a.ide f" and g: "Right_a.ide g"
          and μ: "Right_a.in_hom μ (HR a f) (HR a g)"
          have 1: "a = src f  a = src g"
            using assms f g Right_a.ide_char Right_a.arr_charSbC right_def seq_if_composable
            by auto
          show "ν. Right_a.in_hom ν f g  HR a ν = μ"
          proof -
            have 2: "ν. «ν : f  g»  R ν = μ"
              using f g μ 1 Right_a.ide_charSbC HR_def R.preserves_reflects_arr Right_a.arr_charSbC
                    Right_a.in_hom_charSbC R.is_full
              by force
            obtain ν where ν: "«ν : f  g»  R ν = μ"
              using 2 by blast
            have "Right_a.arr ν"
              using ν 1 src_dom Right_a.arr_charSbC right_def hseq_char' by fastforce
            moreover have "HR a ν = μ"
              using ν 1 src_dom HR_def by auto
            ultimately show ?thesis
              using ν Right_a.dom_simp Right_a.cod_simp by blast
          qed
        qed
      qed
      have "isomorphic (a  a) a  a  a  null"
        using assms obj_self_composable unit_in_hom iso_unit isomorphic_def by blast
      thus ?thesis
        using La.fully_faithful_functor_axioms Ra.fully_faithful_functor_axioms weak_unit_def
        by blast
    qed

    lemma src_in_sources:
    assumes "arr μ"
    shows "src μ  sources μ"
      using assms obj_is_weak_unit R.preserves_arr hseq_char' by auto

    lemma trg_in_targets:
    assumes "arr μ"
    shows "trg μ  targets μ"
      using assms obj_is_weak_unit L.preserves_arr hseq_char' by auto

    lemma weak_unit_cancel_left:
    assumes "weak_unit a" and "ide f" and "ide g"
    and "a  f  a  g"
    shows "f  g"
    proof -
      have 0: "ide a"
        using assms weak_unit_def by force
      interpret Left_a: subcategory V left a
        using 0 left_hom_is_subcategory by simp
      interpret Left_a: left_hom V H a
        using assms weak_unit_self_composable by unfold_locales auto
      interpret La: fully_faithful_functor Left a Left a HL a
        using assms weak_unit_def by fast
      obtain φ where φ: "iso φ  «φ : a  f  a  g»"
        using assms by blast
      have 1: "Left_a.iso φ  Left_a.in_hom φ (a  f) (a  g)"
        by (metis HL_def La.is_extensional La.preserves_arr Left_a.dom_closed
            Left_a.in_hom_charSbC Left_a.iso_char Left_a.not_arr_null Left_a.null_char φ assms(4)
            hom_connected(4) hseq_char' ide_char' in_homE isomorphic_implies_ide(2) left_def)
      hence 2: "Left_a.ide (a  f)  Left_a.ide (a  g)"
        using Left_a.ide_dom [of φ] Left_a.ide_cod [of φ] Left_a.dom_simp Left_a.cod_simp
        by auto
      hence 3: "Left_a.ide f  Left_a.ide g"
        by (metis Left_a.ideISbC Left_a.ide_def Left_a.null_char assms(2) assms(3) left_def)
      obtain ψ where ψ: "ψ  Left_a.hom f g  a  ψ = φ"
        using assms 1 2 3 La.is_full [of g f φ] HL_def by auto
      have "Left_a.iso ψ"
        using ψ 1 HL_def La.reflects_iso by auto
      hence "iso ψ  «ψ : f  g»"
        using ψ Left_a.iso_char Left_a.in_hom_charSbC by auto
      thus ?thesis by auto
    qed

    lemma weak_unit_cancel_right:
    assumes "weak_unit a" and "ide f" and "ide g"
    and "f  a  g  a"
    shows "f  g"
    proof -
      have 0: "ide a"
        using assms weak_unit_def by force
      interpret Right_a: subcategory V right a
        using 0 right_hom_is_subcategory by simp
      interpret Right_a: right_hom V H a
        using assms weak_unit_self_composable by unfold_locales auto
      interpret R: fully_faithful_functor Right a Right a HR a
        using assms weak_unit_def by fast
      obtain φ where φ: "iso φ  in_hom φ (f  a) (g  a)"
        using assms by blast
      have 1: "Right_a.iso φ  φ  Right_a.hom (f  a) (g  a)"
      proof
        have "φ  a  null"
          by (metis φ assms(1,4) hom_connected(3) ideD(1) in_homE isomorphic_implies_ide(2)
              match_3 not_arr_null weak_unit_self_composable(3))
        thus "φ  Right_a.hom (f  a) (g  a)"
          using φ Right_a.hom_char right_def by simp
        thus "Right_a.iso φ"
          using φ Right_a.iso_char by auto
      qed
      hence 2: "Right_a.ide (f  a)  Right_a.ide (g  a)"
        using Right_a.ide_dom [of φ] Right_a.ide_cod [of φ] Right_a.dom_simp Right_a.cod_simp
        by auto
      hence 3: "Right_a.ide f  Right_a.ide g"
        using assms Right_a.ide_charSbC Right_a.arr_charSbC right_def Right_a.ide_def Right_a.null_char
        by metis
      obtain ψ where ψ: "ψ  Right_a.hom f g  ψ  a = φ"
        using assms 1 2 3 R.is_full [of g f φ] HR_def by auto
      have "Right_a.iso ψ"
        using ψ 1 HR_def R.reflects_iso by auto
      hence "iso ψ  «ψ : f  g»"
        using ψ Right_a.iso_char Right_a.in_hom_charSbC by auto
      thus ?thesis by auto
    qed

    text ‹
      All sources of an arrow ({\em i.e.}~weak units composable on the right with that arrow)
      are isomorphic to the chosen source, and similarly for targets.  That these statements
      hold was somewhat surprising to me.
    ›

    lemma source_iso_src:
    assumes "arr μ" and "a  sources μ"
    shows "a  src μ"
    proof -
      have 0: "ide a"
        using assms weak_unit_def by force
      have 1: "src a = trg a"
        using assms ide_dom sources_def weak_unit_iff_self_target seq_if_composable
              weak_unit_self_composable
        by simp
      obtain φ where φ: "iso φ  «φ : a  a  a»"
        using assms weak_unit_def by blast
      have "a  src a  src a  src a"
      proof -
        have "src a  src a  src a"
          using 0 obj_is_weak_unit weak_unit_def isomorphic_symmetric by auto
        moreover have "a  src a  src a"
        proof -
          have "a  a  src a  a  src a"
          proof -
            have "iso (φ  src a)  «φ  src a : (a  a)  src a  a  src a»"
              using 0 1 φ ide_in_hom(2) by auto
            moreover have "iso 𝖺-1[a, a, src a] 
                           «𝖺-1[a, a, src a] :  a  a  src a  (a  a)  src a»"
              using 0 1 iso_assoc' by force
            ultimately show ?thesis
              using isos_compose isomorphic_def by auto
          qed
          thus ?thesis
            using assms 0 weak_unit_cancel_left by auto
        qed
        ultimately show ?thesis
          using isomorphic_transitive by meson
      qed
      hence "a  src a"
        using 0 weak_unit_cancel_right [of "src a" a "src a"] obj_is_weak_unit by auto
      thus ?thesis using assms seq_if_composable 1 by auto
    qed

    lemma target_iso_trg:
    assumes "arr μ" and "b  targets μ"
    shows "b  trg μ"
    proof -
      have 0: "ide b"
        using assms weak_unit_def by force
      have 1: "trg μ = src b"
        using assms seq_if_composable by auto
      obtain φ where φ: "iso φ  «φ : b  b  b»"
        using assms weak_unit_def by blast
      have "trg b  b  trg b  trg b"
      proof -
        have "trg b  trg b  trg b"
          using 0 obj_is_weak_unit weak_unit_def isomorphic_symmetric by auto
        moreover have "trg b  b  trg b"
        proof -
          have "(trg b  b)  b  trg b  b"
          proof -
            have "iso (trg b  φ)  «trg b  φ : trg b  b  b  trg b  b»"
              using assms 0 1 φ ide_in_hom(2) targetsD(1) weak_unit_self_composable
              apply (intro conjI hcomp_in_vhom) by auto
            moreover have "iso 𝖺[trg b, b, b] 
                           «𝖺[trg b, b, b] : (trg b  b)  b  trg b  b  b»"
              using assms(2) 0 1 seq_if_composable targetsD(1-2) weak_unit_self_composable
              by auto
            ultimately show ?thesis
              using isos_compose isomorphic_def by auto
          qed
          thus ?thesis
            using assms 0 weak_unit_cancel_right by auto
        qed
        ultimately show ?thesis
          using isomorphic_transitive by meson
      qed
      hence "b  trg b"
        using 0 weak_unit_cancel_left [of "trg b" b "trg b"] obj_is_weak_unit by simp
      thus ?thesis
        using assms 0 1 seq_if_composable weak_unit_iff_self_source targetsD(1-2) source_iso_src
        by simp
    qed

    lemma is_weak_composition_with_homs:
    shows "weak_composition_with_homs V H src trg"
      using src_in_sources trg_in_targets seq_if_composable composable_implies_arr
      by (unfold_locales, simp_all)

    interpretation weak_composition_with_homs V H src trg
      using is_weak_composition_with_homs by auto

    text ‹
      In a bicategory, the notion of composability defined in terms of
      the chosen sources and targets coincides with the version defined
      for a weak composition, which does not involve particular choices.
    ›

    lemma connected_iff_seq:
    assumes "arr μ" and "arr ν"
    shows "sources ν  targets μ  {}  src ν = trg μ"
    proof
      show "src ν = trg μ  sources ν  targets μ  {}"
        using assms src_in_sources [of ν] trg_in_targets [of μ] by auto
      show "sources ν  targets μ  {}  src ν = trg μ"
      proof -
        assume 1: "sources ν  targets μ  {}"
        obtain a where a: "a  sources ν  targets μ"
          using assms 1 by blast
        have μ: "arr μ"
          using a composable_implies_arr by auto
        have ν: "arr ν"
          using a composable_implies_arr by auto
        have 2: "a'. a'  sources ν  src a' = src a  trg a' = trg a"
          by (metis IntE a seq_if_composable sourcesD(2-3) weak_unit_self_composable(3))
        have "src ν = src (src ν)" using ν by simp
        also have "... = src (trg μ)"
          using ν 2 [of "src ν"] src_in_sources a weak_unit_self_composable seq_if_composable
          by auto
        also have "... = trg (trg μ)" using μ by simp
        also have "... = trg μ" using μ by simp
        finally show "src ν = trg μ" by blast
      qed
    qed

    lemma is_associative_weak_composition:
    shows "associative_weak_composition V H 𝖺"
    proof -
      have 1: "ν μ. ν  μ  null  src ν = trg μ"
        using H.is_extensional VV.arr_charSbC by force
      show "associative_weak_composition V H 𝖺"
      proof
        show "f g h. ide f  ide g  ide h  f  g  null  g  h  null 
                      «𝖺[f, g, h] : (f  g)  h  f  g  h»"
          using 1 by auto
        show "f g h. ide f  ide g  ide h  f  g  null  g  h  null 
                      iso 𝖺[f, g, h]"
          using 1 iso_assoc by presburger
        show "τ μ ν. τ  μ  null  μ  ν  null 
                      𝖺[cod τ, cod μ, cod ν]  ((τ  μ)  ν) = (τ  μ  ν)  𝖺[dom τ, dom μ, dom ν]"
           using 1 assoc_naturality hseq_char hseq_char' by metis
        show "f g h k. ide f  ide g  ide h  ide k 
                         sources f  targets g  {} 
                         sources g  targets h  {} 
                         sources h  targets k  {} 
                        (f  𝖺[g, h, k])  𝖺[f, g  h, k]  (𝖺[f, g, h]  k) =
                        𝖺[f, g, h  k]  𝖺[f  g, h, k]"
           using 1 connected_iff_seq pentagon ideD(1) by auto
      qed
    qed

    interpretation associative_weak_composition V H 𝖺
      using is_associative_weak_composition by auto

    theorem is_prebicategory:
    shows "prebicategory V H 𝖺"
      using src_in_sources trg_in_targets by (unfold_locales, auto)

    interpretation prebicategory V H 𝖺
      using is_prebicategory by auto

    corollary is_prebicategory_with_homs:
    shows "prebicategory_with_homs V H 𝖺 src trg"
      ..

    interpretation prebicategory_with_homs V H 𝖺 src trg
      using is_prebicategory_with_homs by auto

    text ‹
      In a bicategory, an arrow is a weak unit if and only if it is
      isomorphic to its chosen source (or to its chosen target).
    ›

    lemma weak_unit_char:
    shows "weak_unit a  a  src a"
    and "weak_unit a  a  trg a"
    proof -
      show "weak_unit a  a  src a"
        using isomorphism_respects_weak_units isomorphic_symmetric
        by (meson ideD(1) isomorphic_implies_ide(2) obj_is_weak_unit obj_src source_iso_src
            weak_unit_iff_self_source weak_unit_self_composable(1))
      show "weak_unit a  a  trg a"
        using isomorphism_respects_weak_units isomorphic_symmetric
        by (metis weak_unit a = isomorphic a (src a) ideD(1) isomorphic_implies_hpar(3)
            isomorphic_implies_ide(1) src_trg target_iso_trg weak_unit_iff_self_target)
    qed
        
    interpretation H: partial_composition H
      using is_partial_composition by auto

    text ‹
      Every arrow with respect to horizontal composition is also an arrow with respect
      to vertical composition.  The converse is not necessarily true.
    ›

    lemma harr_is_varr:
    assumes "H.arr μ"
    shows "arr μ"
      using H.arr_def H.codomains_def H.domains_def assms composable_implies_arr(1)
            composable_implies_arr(2)
      by auto

    text ‹
      An identity for horizontal composition is also an identity for vertical composition.
    ›

    lemma horizontal_identity_is_ide:
    assumes "H.ide μ"
    shows "ide μ"
    proof -
      have μ: "arr μ"
        using assms H.ide_def composable_implies_arr(2) by auto
      hence 1: "μ  dom μ  null"
        using assms hom_connected H.ide_def by auto
      have "μ  dom μ = dom μ"
        using assms 1 H.ide_def by simp
      moreover have "μ  dom μ = μ"
        using assms 1 H.ide_def [of μ] null_agreement
        by (metis μ cod_cod cod_dom hcomp_simpsWC(3) ideD(2) ide_char' paste_1)
      ultimately have "dom μ = μ"
        by simp
      thus ?thesis
        using μ by (metis ide_dom)
    qed

    text ‹
      Every identity for horizontal composition is a weak unit.
    ›

    lemma horizontal_identity_is_weak_unit:
    assumes "H.ide μ"
    shows "weak_unit μ"
      using assms weak_unit_char
      by (metis H.ide_def comp_target_ide horizontal_identity_is_ide ideD(1)
          isomorphism_respects_weak_units null_agreement targetsD(2-3) trg_in_targets)

  end

  subsection "Vertically Discrete Bicategories are Categories"

  text ‹
    In this section we show that if a bicategory is discrete with respect to vertical
    composition, then it is a category with respect to horizontal composition.
    To obtain this result, we need to establish that the set of arrows for the horizontal
    composition coincides with the set of arrows for the vertical composition.
    This is not true for a general bicategory, and even with the assumption that the
    vertical category is discrete it is not immediately obvious from the definitions.
    The issue is that the notion ``arrow'' for the horizontal composition is defined
    in terms of the existence of ``domains'' and ``codomains'' with respect to that
    composition, whereas the axioms for a bicategory only relate the notion ``arrow''
    for the vertical category to the existence of sources and targets with respect
    to the horizontal composition.
    So we have to establish that, under the assumption of vertical discreteness,
    sources coincide with domains and targets coincide with codomains.
    We also need the fact that horizontal identities are weak units, which previously
    required some effort to show.
  ›

  locale vertically_discrete_bicategory =
    bicategory +
  assumes vertically_discrete: "ide = arr"
  begin

    interpretation prebicategory_with_homs V H 𝖺 src trg
      using is_prebicategory_with_homs by auto

    interpretation H: partial_composition H
      using is_partial_composition(1) by auto

    lemma weak_unit_is_horizontal_identity:
    assumes "weak_unit a"
    shows "H.ide a"
    proof -
      have "a  a  H.null"
        using assms weak_unit_self_composable by simp
      moreover have "f. f  a  H.null  f  a = f"
      proof -
        fix f
        assume "f  a  H.null"
        hence "f  a  f"
          using assms comp_ide_source composable_implies_arr(2) sourcesI vertically_discrete
          by auto
        thus "f  a = f"
          using vertically_discrete isomorphic_def by auto
      qed
      moreover have "f. a  f  H.null  a  f = f"
      proof -
        fix f
        assume "a  f  H.null"
        hence "a  f  f"
          using assms comp_target_ide composable_implies_arr(1) targetsI vertically_discrete
          by auto
        thus "a  f = f"
          using vertically_discrete isomorphic_def by auto
      qed
      ultimately show "H.ide a"
        using H.ide_def by simp
    qed

    lemma sources_eq_domains:
    shows "sources μ = H.domains μ"
      using weak_unit_is_horizontal_identity H.domains_def sources_def
            horizontal_identity_is_weak_unit
      by auto

    lemma targets_eq_codomains:
    shows "targets μ = H.codomains μ"
      using weak_unit_is_horizontal_identity H.codomains_def targets_def
            horizontal_identity_is_weak_unit
      by auto

    lemma arr_agreement:
    shows "arr = H.arr"
      using arr_def H.arr_def arr_iff_has_src arr_iff_has_trg
            sources_eq_domains targets_eq_codomains
      by auto

    interpretation H: category H
    proof
      show "g f. g  f  H.null  H.seq g f"
        using arr_agreement hcomp_simpsWC(1) by auto
      show "f. (H.domains f  {}) = (H.codomains f  {})"
        using sources_eq_domains targets_eq_codomains arr_iff_has_src arr_iff_has_trg
        by simp
      fix f g h
      show "H.seq h g  H.seq (h  g) f  H.seq g f"
        using null_agreement arr_agreement H.not_arr_null preserves_arr VoV.arr_charSbC
        by (metis hseq_char' match_1)
      show "H.seq h (g  f)  H.seq g f  H.seq h g"
        using null_agreement arr_agreement H.not_arr_null preserves_arr VoV.arr_charSbC
        by (metis hseq_char' match_2)
      show "H.seq g f  H.seq h g  H.seq (h  g) f"
        using arr_agreement match_3 hseq_char(1) by auto
      show "H.seq g f  H.seq h g  (h  g)  f = h  g  f"
      proof -
        assume hg: "H.seq h g"
        assume gf: "H.seq g f"
        have "iso 𝖺[h, g, f]  «𝖺[h, g, f] : (h  g)  f  h  g  f»"
          using hg gf vertically_discrete arr_agreement hseq_char assoc_in_hom iso_assoc
          by auto
        thus ?thesis
          using arr_agreement vertically_discrete by auto
      qed
    qed

    proposition is_category:
    shows "category H"
      ..

  end

  subsection "Obtaining the Unitors"

  text ‹
    We now want to exploit the construction of unitors in a prebicategory with units,
    to obtain left and right unitors in a bicategory.  However, a bicategory is not
    \emph{a priori} a prebicategory with units, because a bicategory only assigns unit
    isomorphisms to each \emph{object}, not to each weak unit.  In order to apply the results
    about prebicategories with units to a bicategory, we first need to extend the bicategory to
    a prebicategory with units, by extending the mapping ι›, which provides a unit isomorphism
    for each object, to a mapping that assigns a unit isomorphism to all weak units.
    This extension can be made in an arbitrary way, as the values chosen for
    non-objects ultimately do not affect the components of the unitors at objects.
  ›

  context bicategory
  begin

    interpretation prebicategory V H 𝖺
      using is_prebicategory by auto

    definition 𝗂'
    where "𝗂' a  SOME φ. iso φ  φ  hom (a  a) a  (obj a  φ = 𝗂[a])"

    lemma 𝗂'_extends_𝗂:
    assumes "weak_unit a"
    shows "iso (𝗂' a)" and "«𝗂' a : a  a  a»" and "obj a  𝗂' a = 𝗂[a]"
    proof -
      let ?P = "λa φ. iso φ  «φ : a  a  a»  (obj a  φ = 𝗂[a])"
      have "φ. ?P a φ"
        by (metis assms iso_some_unit(1) iso_some_unit(2) iso_unit unit_in_vhom)
      hence 1: "?P a (𝗂' a)"
        using 𝗂'_def someI_ex [of "?P a"] by simp
      show "iso (𝗂' a)" using 1 by simp
      show "«𝗂' a : a  a  a»" using 1 by simp
      show "obj a  𝗂' a = 𝗂[a]" using 1 by simp
    qed

    proposition extends_to_prebicategory_with_units:
    shows "prebicategory_with_units V H 𝖺 𝗂'"
      using 𝗂'_extends_𝗂 by unfold_locales auto

    interpretation PB: prebicategory_with_units V H 𝖺 𝗂'
      using extends_to_prebicategory_with_units by auto
    interpretation PB: prebicategory_with_homs V H 𝖺 src trg
      using is_prebicategory_with_homs by auto
    interpretation PB: prebicategory_with_homs_and_units V H 𝖺 𝗂' src trg ..

    proposition extends_to_prebicategory_with_homs_and_units:
    shows "prebicategory_with_homs_and_units V H 𝖺 𝗂' src trg"
      ..

    definition lunit                 ("𝗅[_]")
    where "𝗅[a]  PB.lunit a"

    definition runit                 ("𝗋[_]")
    where "𝗋[a]  PB.runit a"

    abbreviation lunit'              ("𝗅-1[_]")
    where "𝗅-1[a]  inv 𝗅[a]"

    abbreviation runit'              ("𝗋-1[_]")
    where "𝗋-1[a]  inv 𝗋[a]"

    text ‹
      \sloppypar
      The characterizations of the left and right unitors that we obtain from locale
      @{locale prebicategory_with_homs_and_units} mention the arbitarily chosen extension 𝗂'›,
      rather than the given 𝗂›.  We want ``native versions'' for the present context.
    ›

    lemma lunit_char:
    assumes "ide f"
    shows "«𝗅[f] : L f  f»" and "L 𝗅[f] = (𝗂[trg f]  f)  𝖺-1[trg f, trg f, f]"
    and "∃!μ. «μ : L f  f»  L μ = (𝗂[trg f]  f)  𝖺-1[trg f, trg f, f]"
    proof -
      have 1: "trg (PB.lunit f) = trg f"
        using assms PB.lunit_char [of f] vconn_implies_hpar(2) vconn_implies_hpar(4)
        by metis
      show "«𝗅[f] : L f  f»"
        unfolding lunit_def
        using assms PB.lunit_char by simp
      show "L 𝗅[f] = (𝗂[trg f]  f)  𝖺-1[trg f, trg f, f]"
        unfolding lunit_def
        using assms 1 PB.lunit_char obj_is_weak_unit 𝗂'_extends_𝗂 by simp
      let ?P = "λμ. «μ : L f  f»  L μ = (𝗂[trg f]  f)  𝖺-1[trg f, trg f, f]"
      have "?P = (λμ. «μ : trg f  f  f» 
                      trg f  μ = (𝗂' (trg f)  f)  inv 𝖺[trg f, trg f, f])"
      proof -
        have "μ. «μ : L f  f»  «μ : trg f  f  f»"
          using assms by simp
        moreover have "μ. «μ : L f  f» 
                            L μ = (𝗂[trg f]  f)  𝖺-1[trg f, trg f, f] 
                            trg f  μ = (𝗂' (trg f)  f)  inv 𝖺[trg f, trg f, f]"
          using calculation obj_is_weak_unit 𝗂'_extends_𝗂 by auto
        ultimately show ?thesis by blast
      qed
      thus "∃!μ. «μ : L f  f»  L μ = (𝗂[trg f]  f)  𝖺-1[trg f, trg f, f]"
        using assms PB.lunit_char by simp
    qed

    lemma lunit_in_hom [intro]:
    assumes "ide f"
    shows "«𝗅[f] : src f  trg f»" and "«𝗅[f] : trg f  f  f»"
    proof -
      show "«𝗅[f] : trg f  f  f»"
        using assms lunit_char by auto
      thus "«𝗅[f] : src f  trg f»"
        by (metis arrI in_hhomI vconn_implies_hpar(1-4))
    qed

    lemma lunit_in_vhom [simp]:
    assumes "ide f" and "trg f = b"
    shows "«𝗅[f] : b  f  f»"
      using assms by auto

    lemma lunit_simps [simp]:
    assumes "ide f"
    shows "arr 𝗅[f]" and "src 𝗅[f] = src f" and "trg 𝗅[f] = trg f"
    and "dom 𝗅[f] = trg f  f" and "cod 𝗅[f] = f"
      using assms lunit_in_hom
          apply auto
      using assms lunit_in_hom
       apply blast
      using assms lunit_in_hom
      by blast

    lemma runit_char:
    assumes "ide f"
    shows "«𝗋[f] : R f  f»" and "R 𝗋[f] = (f  𝗂[src f])  𝖺[f, src f, src f]"
    and "∃!μ. «μ : R f  f»  R μ = (f  𝗂[src f])  𝖺[f, src f, src f]"
    proof -
      have 1: "src (PB.runit f) = src f"
        using assms PB.runit_char [of f] vconn_implies_hpar(1) vconn_implies_hpar(3)
        by metis
      show "«𝗋[f] : R f  f»"
        unfolding runit_def
        using assms PB.runit_char by simp
      show "R 𝗋[f] = (f  𝗂[src f])  𝖺[f, src f, src f]"
        unfolding runit_def
        using assms 1 PB.runit_char obj_is_weak_unit 𝗂'_extends_𝗂 by simp
      let ?P = "λμ. «μ : R f  f»  R μ = (f  𝗂[src f])  𝖺[f, src f, src f]"
      have "?P = (λμ. «μ : f  src f  f» 
                      μ  src f = (f  𝗂' (src f))   𝖺[f, src f, src f])"
      proof -
        have "μ. «μ : R f  f»  «μ : f  src f  f»"
          using assms by simp
        moreover have "μ. «μ : R f  f» 
                            R μ = (f  𝗂[src f])  𝖺[f, src f, src f] 
                            μ  src f = (f  𝗂' (src f))   𝖺[f, src f, src f]"
          using calculation obj_is_weak_unit 𝗂'_extends_𝗂 by auto
        ultimately show ?thesis by blast
      qed
      thus "∃!μ. «μ : R f  f»  R μ = (f  𝗂[src f])  𝖺[f, src f, src f]"
        using assms PB.runit_char by simp
    qed

    lemma runit_in_hom [intro]:
    assumes "ide f"
    shows "«𝗋[f] : src f  trg f»" and "«𝗋[f] : f  src f  f»"
    proof -
      show "«𝗋[f] : f  src f  f»"
        using assms runit_char by auto
      thus "«𝗋[f] : src f  trg f»"
        by (metis arrI in_hhom_def vconn_implies_hpar(1-4))
    qed

    lemma runit_in_vhom [simp]:
    assumes "ide f" and "src f = a"
    shows "«𝗋[f] : f  a  f»"
      using assms by auto

    lemma runit_simps [simp]:
    assumes "ide f"
    shows "arr 𝗋[f]" and "src 𝗋[f] = src f" and "trg 𝗋[f] = trg f"
    and "dom 𝗋[f] = f  src f" and "cod 𝗋[f] = f"
      using assms runit_in_hom
          apply auto
      using assms runit_in_hom
       apply blast
      using assms runit_in_hom
      by blast

    lemma lunit_eqI:
    assumes "ide f" and "«μ : trg f  f  f»"
    and "trg f  μ = (𝗂[trg f]  f)  𝖺-1[trg f, trg f, f]"
    shows "μ = 𝗅[f]"
      unfolding lunit_def
      using assms PB.lunit_eqI 𝗂'_extends_𝗂 trg.preserves_ide obj_is_weak_unit by simp

    lemma runit_eqI:
    assumes "ide f" and "«μ : f  src f  f»"
    and "μ  src f = (f  𝗂[src f])  𝖺[f, src f, src f]"
    shows "μ = 𝗋[f]"
      unfolding runit_def
      using assms PB.runit_eqI 𝗂'_extends_𝗂 src.preserves_ide obj_is_weak_unit by simp

    lemma lunit_naturality:
    assumes "arr μ"
    shows "μ  𝗅[dom μ] = 𝗅[cod μ]  (trg μ  μ)"
      unfolding lunit_def
      using assms PB.lunit_naturality by auto

    lemma runit_naturality:
    assumes "arr μ"
    shows "μ  𝗋[dom μ] = 𝗋[cod μ]  (μ  src μ)"
      unfolding runit_def
      using assms PB.runit_naturality by auto

    lemma iso_lunit [simp]:
    assumes "ide f"
    shows "iso 𝗅[f]"
      unfolding lunit_def
      using assms PB.iso_lunit by blast

    lemma iso_runit [simp]:
    assumes "ide f"
    shows "iso 𝗋[f]"
      unfolding runit_def
      using assms PB.iso_runit by blast

    lemma iso_lunit' [simp]:
    assumes "ide f"
    shows "iso 𝗅-1[f]"
      using assms iso_lunit by blast

    lemma iso_runit' [simp]:
    assumes "ide f"
    shows "iso 𝗋-1[f]"
      using assms iso_runit by blast

    lemma lunit'_in_hom [intro]:
    assumes "ide f"
    shows "«𝗅-1[f] : src f  trg f»" and "«𝗅-1[f] : f  trg f  f»"
    proof -
      show "«𝗅-1[f] : f  trg f  f»"
        using assms lunit_char iso_lunit by simp
      thus "«𝗅-1[f] : src f  trg f»"
        using assms src_dom trg_dom by simp
    qed

    lemma lunit'_in_vhom [simp]:
    assumes "ide f" and "trg f = b"
    shows "«𝗅-1[f] : f  b  f»"
      using assms by auto

    lemma lunit'_simps [simp]:
    assumes "ide f"
    shows "arr 𝗅-1[f]" and "src 𝗅-1[f] = src f" and "trg 𝗅-1[f] = trg f"
    and "dom 𝗅-1[f] = f" and "cod 𝗅-1[f] = trg f  f"
      using assms lunit'_in_hom by auto

    lemma runit'_in_hom [intro]:
    assumes "ide f"
    shows "«𝗋-1[f] : src f  trg f»" and "«𝗋-1[f] : f  f  src f»"
    proof -
      show "«𝗋-1[f] : f  f  src f»"
        using assms runit_char iso_runit by simp
      thus "«𝗋-1[f] : src f  trg f»"
        using src_dom trg_dom
        by (simp add: assms)
    qed

    lemma runit'_in_vhom [simp]:
    assumes "ide f" and "src f = a"
    shows "«𝗋-1[f] : f  f  a»"
      using assms by auto

    lemma runit'_simps [simp]:
    assumes "ide f"
    shows "arr 𝗋-1[f]" and "src 𝗋-1[f] = src f" and "trg 𝗋-1[f] = trg f"
    and "dom 𝗋-1[f] = f" and "cod 𝗋-1[f] = f  src f"
      using assms runit'_in_hom by auto

    interpretation L: endofunctor V L ..
    interpretation 𝔩: transformation_by_components V V L map lunit
      using lunit_in_hom lunit_naturality by unfold_locales auto
    interpretation 𝔩: natural_isomorphism V V L map 𝔩.map
      using iso_lunit by (unfold_locales, auto)

    lemma natural_isomorphism_𝔩:
    shows "natural_isomorphism V V L map 𝔩.map"
      ..

    abbreviation 𝔩
    where "𝔩  𝔩.map"

    lemma 𝔩_ide_simp:
    assumes "ide f"
    shows "𝔩 f = 𝗅[f]"
      using assms by simp

    interpretation L: equivalence_functor V V L
      using L.isomorphic_to_identity_is_equivalence 𝔩.natural_isomorphism_axioms by simp

    lemma equivalence_functor_L:
    shows "equivalence_functor V V L"
      ..

    lemma lunit_commutes_with_L:
    assumes "ide f"
    shows "𝗅[L f] = L 𝗅[f]"
      unfolding lunit_def
      using assms PB.lunit_commutes_with_L by blast

    interpretation R: endofunctor V R ..
    interpretation 𝔯: transformation_by_components V V R map runit
      using runit_in_hom runit_naturality by unfold_locales auto
    interpretation 𝔯: natural_isomorphism V V R map 𝔯.map
      using iso_runit by (unfold_locales, auto)

    lemma natural_isomorphism_𝔯:
    shows "natural_isomorphism V V R map 𝔯.map"
      ..

    abbreviation 𝔯
    where "𝔯  𝔯.map"

    lemma 𝔯_ide_simp:
    assumes "ide f"
    shows "𝔯 f = 𝗋[f]"
      using assms by simp

    interpretation R: equivalence_functor V V R
      using R.isomorphic_to_identity_is_equivalence 𝔯.natural_isomorphism_axioms by simp

    lemma equivalence_functor_R:
    shows "equivalence_functor V V R"
      ..

    lemma runit_commutes_with_R:
    assumes "ide f"
    shows "𝗋[R f] = R 𝗋[f]"
      unfolding runit_def
      using assms PB.runit_commutes_with_R by blast

    lemma lunit'_naturality:
    assumes "arr μ"
    shows "(trg μ  μ)  𝗅-1[dom μ] = 𝗅-1[cod μ]  μ"
      using assms iso_lunit lunit_naturality invert_opposite_sides_of_square L.preserves_arr
            L.preserves_cod arr_cod ide_cod ide_dom lunit_simps(1) lunit_simps(4) seqI
      by presburger

    lemma runit'_naturality:
    assumes "arr μ"
    shows "(μ  src μ)  𝗋-1[dom μ] = 𝗋-1[cod μ]  μ"
      using assms iso_runit runit_naturality invert_opposite_sides_of_square R.preserves_arr
            R.preserves_cod arr_cod ide_cod ide_dom runit_simps(1) runit_simps(4) seqI
      by presburger

    lemma isomorphic_unit_right:
    assumes "ide f"
    shows "f  src f  f"
      using assms runit'_in_hom iso_runit' isomorphic_def isomorphic_symmetric by blast

    lemma isomorphic_unit_left:
    assumes "ide f"
    shows "trg f  f  f"
      using assms lunit'_in_hom iso_lunit' isomorphic_def isomorphic_symmetric by blast

  end

  subsection "Further Properties of Bicategories"

  text ‹
    Here we derive further properties of bicategories, now that we
    have the unitors at our disposal.  This section generalizes the corresponding
    development in theory @{theory MonoidalCategory.MonoidalCategory},
    which has some diagrams to illustrate the longer calculations.
    The present section also includes some additional facts that are now nontrivial
    due to the partiality of horizontal composition.
  ›

  context bicategory
  begin

    lemma unit_simps [simp]:
    assumes "obj a"
    shows "arr 𝗂[a]" and "src 𝗂[a] = a" and "trg 𝗂[a] = a"
    and "dom 𝗂[a] = a  a" and "cod 𝗂[a] = a"
      using assms unit_in_hom by blast+

    lemma triangle:
    assumes "ide f" and "ide g" and "src g = trg f"
    shows "(g  𝗅[f])  𝖺[g, src g, f] = 𝗋[g]  f"
    proof -
      let ?b = "src g"
      have *: "(g  𝗅[?b  f])  𝖺[g, ?b, ?b  f] = 𝗋[g]  ?b  f"
      proof -
        have 1: "((g  𝗅[?b  f])  𝖺[g, ?b, ?b  f])  𝖺[g  ?b, ?b, f]
                    = (𝗋[g]  ?b  f)  𝖺[g  ?b, ?b, f]"
        proof -
          have "((g  𝗅[?b  f])  𝖺[g, ?b, ?b  f])  𝖺[g  ?b, ?b, f]
                  = (g  𝗅[?b  f])  𝖺[g, ?b, ?b  f]  𝖺[g  ?b, ?b, f]"
            using HoVH_def HoHV_def comp_assoc by auto
          also have
              "... = (g  𝗅[?b  f])  (g  𝖺[?b, ?b, f])  𝖺[g, ?b  ?b, f]  (𝖺[g, ?b, ?b]  f)"
            using assms pentagon by force
          also have
              "... = ((g  𝗅[?b  f])  (g  𝖺[?b, ?b, f]))  𝖺[g, ?b  ?b, f]  (𝖺[g, ?b, ?b]  f)"
            using assms assoc_in_hom HoVH_def HoHV_def comp_assoc by auto
          also have
              "... = ((g  ?b  𝗅[f])  (g  𝖺[?b, ?b, f]))  𝖺[g, ?b  ?b, f]  (𝖺[g, ?b, ?b]  f)"
            using assms lunit_commutes_with_L lunit_in_hom by force
          also have "... = ((g  (𝗂[?b]  f)  𝖺-1[?b, ?b, f])  (g  𝖺[?b, ?b, f]))
                              𝖺[g, ?b  ?b, f]  (𝖺[g, ?b, ?b]  f)"
            using assms lunit_char(2) by force
          also have "... = (g  ((𝗂[?b]  f)  𝖺-1[?b, ?b, f])  𝖺[?b, ?b, f])
                              𝖺[g, ?b  ?b, f]  (𝖺[g, ?b, ?b]  f)"
            using assms interchange [of g g "(𝗂[?b]  f)  𝖺-1[?b, ?b, f]" "𝖺[?b, ?b, f]"]
            by auto
          also have "... = ((g  𝗂[?b]  f)  𝖺[g, ?b  ?b, f])  (𝖺[g, ?b, ?b]  f)"
            using assms comp_arr_dom comp_assoc_assoc' comp_assoc by auto
          also have "... = (𝖺[g, ?b, f]  ((g  𝗂[?b])  f))  (𝖺[g, ?b, ?b]  f)"
            using assms assoc_naturality [of g "𝗂[?b]" f] by simp
          also have "... = 𝖺[g, ?b, f]  ((g  𝗂[?b])  𝖺[g, ?b, ?b]  f)"
            using assms interchange [of "g  𝗂[?b]" "𝖺[g, ?b, ?b]" f f] comp_assoc by simp
          also have "... = 𝖺[g, ?b, f]  ((𝗋[g]  ?b)  f)"
            using assms runit_char(2) by force
          also have "... = (𝗋[g]  ?b  f)  𝖺[g  ?b, ?b, f]"
            using assms assoc_naturality [of "𝗋[g]" ?b f] by auto
          finally show ?thesis by blast
        qed
        show "(g  𝗅[?b  f])  𝖺[g, ?b, ?b  f] = 𝗋[g]  ?b  f"
        proof -
          have "epi 𝖺[g  ?b, ?b, f]"
            using assms preserves_ide iso_assoc iso_is_retraction retraction_is_epi by force
          thus ?thesis
            using assms 1 by auto
        qed
      qed
      have "(g  𝗅[f])  𝖺[g, ?b, f] = ((g  𝗅[f])  (g  𝗅[?b  f])  (g  ?b  𝗅-1[f])) 
                                     (g  ?b  𝗅[f])  𝖺[g, ?b, ?b  f]  ((g  ?b)  𝗅-1[f])"
      proof -
        have "𝖺[g, ?b, f] = (g  ?b  𝗅[f])  𝖺[g, ?b, ?b  f]  ((g  ?b)  𝗅-1[f])"
        proof -
          have "𝖺[g, ?b, f] = (g  ?b  f)  𝖺[g, ?b, f]"
            using assms comp_cod_arr by simp
          have "𝖺[g, ?b, f] = ((g  ?b  𝗅[f])  (g  ?b  𝗅-1[f]))  𝖺[g, ?b, f]"
            using assms comp_cod_arr comp_arr_inv' whisker_left [of g]
                  whisker_left [of ?b "𝗅[f]" "𝗅-1[f]"]
            by simp
          also have "... = (g  ?b  𝗅[f])  𝖺[g, ?b, ?b  f]  ((g  ?b)  𝗅-1[f])"
            using assms iso_lunit assoc_naturality [of g ?b "𝗅-1[f]"] comp_assoc by force
          finally show ?thesis by blast
        qed
        moreover have "g  𝗅[f] = (g  𝗅[f])  (g  𝗅[?b  f])  (g  ?b  𝗅-1[f])"
        proof -
          have "(g  𝗅[?b  f])  (g  ?b  𝗅-1[f]) = g  ?b  f"
          proof -
            have "(g  𝗅[?b  f])  (g  ?b  𝗅-1[f]) = (g  ?b  𝗅[f])  (g  ?b  𝗅-1[f])"
              using assms lunit_in_hom lunit_commutes_with_L by simp
            also have "... = g  ?b  f"
              using assms comp_arr_inv' whisker_left [of g] whisker_left [of ?b "𝗅[f]" "𝗅-1[f]"]
              by simp
            finally show ?thesis by blast
          qed
          thus ?thesis
            using assms comp_arr_dom by auto
        qed
        ultimately show ?thesis by simp
      qed
      also have "... = (g  𝗅[f])  (g  𝗅[?b  f])  ((g  ?b  𝗅-1[f])  (g  ?b  𝗅[f])) 
                       𝖺[g, ?b, ?b  f]  ((g  ?b)  𝗅-1[f])"
        using comp_assoc by simp
      also have "... = (g  𝗅[f])  (g  𝗅[?b  f])  ((g  ?b  (?b  f)) 
                       𝖺[g, ?b, ?b  f])  ((g  ?b)  𝗅-1[f])"
        using assms iso_lunit comp_inv_arr' interchange [of g g "?b  𝗅-1[f]" "?b  𝗅[f]"]
              interchange [of ?b ?b "𝗅-1[f]" "𝗅[f]"] comp_assoc
        by auto
      also have "... = (g  𝗅[f])  ((g  𝗅[?b  f])  𝖺[g, ?b, ?b  f])  ((g  ?b)  𝗅-1[f])"
        using assms comp_cod_arr comp_assoc by auto
      also have "... = 𝗋[g]  f"
      proof -
        have "𝗋[g]  f = (g  𝗅[f])  (𝗋[g]  ?b  f)  ((g  ?b)  𝗅-1[f])"
        proof -
          have "(g  𝗅[f])  (𝗋[g]  ?b  f)  ((g  ?b)  𝗅-1[f])
                  = (g  𝗅[f])  (𝗋[g]  (g  ?b)  (?b  f)  𝗅-1[f])"
            using assms iso_lunit interchange [of "𝗋[g]" "g  ?b" "?b  f" "𝗅-1[f]"]
            by force
          also have "... = (g  𝗅[f])  (𝗋[g]  𝗅-1[f])"
            using assms comp_arr_dom comp_cod_arr by simp
          also have "... = 𝗋[g]  𝗅[f]  𝗅-1[f]"
            using assms interchange [of g "𝗋[g]" "𝗅[f]" "𝗅-1[f]"] comp_cod_arr
            by simp
          also have "... = 𝗋[g]  f"
            using assms iso_lunit comp_arr_inv' by simp
          finally show ?thesis by argo
        qed
        thus ?thesis using assms * by argo
      qed
      finally show ?thesis by blast
    qed

    lemma lunit_hcomp_gen:
    assumes "ide f" and "ide g" and "ide h"
    and "src f = trg g" and "src g = trg h"
    shows "(f  𝗅[g  h])  (f  𝖺[trg g, g, h]) = f  𝗅[g]  h"
    proof -
      have "((f  𝗅[g  h])  (f  𝖺[trg g, g, h]))  𝖺[f, trg g  g, h]  (𝖺[f, trg g, g]  h) =
            (f  (𝗅[g]  h))  𝖺[f, trg g  g, h]  (𝖺[f, trg g, g]  h)"
      proof -
        have "((f  𝗅[g  h])  (f  𝖺[trg g, g, h]))  (𝖺[f, trg g  g, h]  (𝖺[f, trg g, g]  h)) =
              ((f  𝗅[g  h])  𝖺[f, trg g, g  h])  𝖺[f  trg g, g, h]"
          using assms pentagon comp_assoc by simp
        also have "... = (𝗋[f]  (g  h))  𝖺[f  trg g, g, h]"
          using assms triangle [of "g  h" f] by auto
        also have "... = 𝖺[f, g, h]  ((𝗋[f]  g)  h)"
          using assms assoc_naturality [of "𝗋[f]" g h] by simp
        also have "... = (𝖺[f, g, h]  ((f  𝗅[g])  h))  (𝖺[f, trg g, g]  h)"
          using assms triangle interchange [of "f  𝗅[g]" "𝖺[f, trg g, g]" h h] comp_assoc
          by auto
        also have "... = (f  (𝗅[g]  h))  (𝖺[f, trg g  g, h]  (𝖺[f, trg g, g]  h))"
          using assms assoc_naturality [of f "𝗅[g]" h] comp_assoc by simp
        finally show ?thesis by blast
      qed
      moreover have "iso (𝖺[f, trg g  g, h]  (𝖺[f, trg g, g]  h))"
        using assms iso_assoc isos_compose by simp
      ultimately show ?thesis
        using assms iso_is_retraction retraction_is_epi
              epiE [of "𝖺[f, trg g  g, h]  (𝖺[f, trg g, g]  h)"
                         "(f  𝗅[g  h])  (f  𝖺[trg g, g, h])" "f  𝗅[g]  h"]
         by auto
    qed

    lemma lunit_hcomp:
    assumes "ide f" and "ide g" and "src f = trg g"
    shows "𝗅[f  g]  𝖺[trg f, f, g] = 𝗅[f]  g"
    and "𝖺-1[trg f, f, g]  𝗅-1[f  g] = 𝗅-1[f]  g"
    and "𝗅[f  g] = (𝗅[f]  g)  𝖺-1[trg f, f, g]"
    and "𝗅-1[f  g] = 𝖺[trg f, f, g]  (𝗅-1[f]  g)"
    proof -
      show 1: "𝗅[f  g]  𝖺[trg f, f, g] = 𝗅[f]  g"
      proof -
        have "L (𝗅[f  g]  𝖺[trg f, f, g]) = L (𝗅[f]  g)"
          using assms interchange [of "trg f" "trg f" "𝗅[f  g]" "𝖺[trg f, f, g]"] lunit_hcomp_gen
          by fastforce
        thus ?thesis
          using assms L.is_faithful [of "𝗅[f  g]  𝖺[trg f, f, g]" "𝗅[f]  g"] by force
      qed
      show "𝖺-1[trg f, f, g]  𝗅-1[f  g] = 𝗅-1[f]  g"
      proof -
        have "𝖺-1[trg f, f, g]  𝗅-1[f  g] = inv (𝗅[f  g]  𝖺[trg f, f, g])"
          using assms by (simp add: inv_comp)
        also have "... = inv (𝗅[f]  g)"
          using 1 by simp
        also have "... = 𝗅-1[f]  g"
          using assms by simp
        finally show ?thesis by simp
      qed
      show 2: "𝗅[f  g] = (𝗅[f]  g)  𝖺-1[trg f, f, g]"
        using assms 1 invert_side_of_triangle(2) by auto
      show "𝗅-1[f  g] = 𝖺[trg f, f, g]  (𝗅-1[f]  g)"
      proof -
        have "𝗅-1[f  g] = inv ((𝗅[f]  g)  𝖺-1[trg f, f, g])"
          using 2 by simp
        also have "... = 𝖺[trg f, f, g]  inv (𝗅[f]  g)"
          using assms inv_comp by simp
        also have "... = 𝖺[trg f, f, g]  (𝗅-1[f]  g)"
          using assms by simp
        finally show ?thesis by simp
      qed
    qed

    lemma runit_hcomp_gen:
    assumes "ide f" and "ide g" and "ide h"
    and "src f = trg g" and "src g = trg h"
    shows "𝗋[f  g]  h = ((f  𝗋[g])  h)  (𝖺[f, g, src g]  h)"
    proof -
      have "𝗋[f  g]  h = ((f  g)  𝗅[h])  𝖺[f  g, src g, h]"
        using assms triangle by simp
      also have "... = (𝖺-1[f, g, h]  (f  g  𝗅[h])  𝖺[f, g, src g  h])  𝖺[f  g, src g, h]"
        using assms assoc_naturality [of f g "𝗅[h]"] invert_side_of_triangle(1)
        by simp
      also have "... = 𝖺-1[f, g, h]  (f  g  𝗅[h])  𝖺[f, g, src g  h]  𝖺[f  g, src g, h]"
        using comp_assoc by simp
      also have "... = (𝖺-1[f, g, h]  (f  (𝗋[g]  h)))  (f  𝖺-1[g, src g, h]) 
                       𝖺[f, g, src g  h]  𝖺[f  g, src g, h]"
        using assms interchange [of f f] triangle comp_assoc
              invert_side_of_triangle(2) [of "𝗋[g]  h" "g  𝗅[h]" "𝖺[g, src g, h]"]
        by simp
      also have "... = ((f  𝗋[g])  h)  𝖺-1[f, g  src g, h]  (f  𝖺-1[g, src g, h]) 
                       𝖺[f, g, src g  h]  𝖺[f  g, src g, h]"
        using assms assoc'_naturality [of f "𝗋[g]" h] comp_assoc by simp
      also have "... = ((f  𝗋[g])  h)  (𝖺[f, g, src g]  h)"
        using assms pentagon [of f g "src g" h] iso_assoc inv_hcomp
              invert_side_of_triangle(1)
                [of "𝖺[f, g, src g  h]  𝖺[f  g, src g, h]" "f  𝖺[g, src g, h]"
                    "𝖺[f, g  src g, h]  (𝖺[f, g, src g]  h)"]
              invert_side_of_triangle(1)
                [of "(f  𝖺-1[g, src g, h])  𝖺[f, g, src g  h]  𝖺[f  g, src g, h]"
                    "𝖺[f, g  src g, h]" "𝖺[f, g, src g]  h"]
        by auto
      finally show ?thesis by blast
    qed

    lemma runit_hcomp:
    assumes "ide f" and "ide g" and "src f = trg g"
    shows "𝗋[f  g] = (f  𝗋[g])  𝖺[f, g, src g]"
    and "𝗋-1[f  g] = 𝖺-1[f, g, src g]  (f  𝗋-1[g])"
    and "𝗋[f  g]  𝖺-1[f, g, src g] = f  𝗋[g]"
    and "𝖺[f, g, src g]  𝗋-1[f  g] = f  𝗋-1[g]"
    proof -
      show 1: "𝗋[f  g] = (f  𝗋[g])  𝖺[f, g, src g]"
        using assms interchange [of "f  𝗋[g]" "𝖺[f, g, src g]" "src g" "src g"]
              runit_hcomp_gen [of f g "src g"]
              R.is_faithful [of "(f  𝗋[g])  (𝖺[f, g, src g])" "𝗋[f  g]"]
        by simp
      show "𝗋-1[f  g] = 𝖺-1[f, g, src g]  (f  𝗋-1[g])"
        using assms 1 inv_comp inv_hcomp by auto
      show 2: "𝗋[f  g]  𝖺-1[f, g, src g] = f  𝗋[g]"
        using assms 1 comp_arr_dom comp_cod_arr comp_assoc hseqI' comp_assoc_assoc' by auto
      show "𝖺[f, g, src g]  𝗋-1[f  g] = f  𝗋-1[g]"
      proof -
        have "𝖺[f, g, src g]  𝗋-1[f  g] = inv (𝗋[f  g]  𝖺-1[f, g, src g])"
          using assms inv_comp by simp
        also have "... = inv (f  𝗋[g])"
          using 2 by simp
        also have "... = f  𝗋-1[g]"
          using assms inv_hcomp [of f "𝗋[g]"] by simp
        finally show ?thesis by simp
      qed
    qed

    lemma unitor_coincidence:
    assumes "obj a"
    shows "𝗅[a] = 𝗂[a]" and "𝗋[a] = 𝗂[a]"
    proof -
      have "R 𝗅[a] = R 𝗂[a]  R 𝗋[a] = R 𝗂[a]"
      proof -
        have "R 𝗅[a] = (a  𝗅[a])  𝖺[a, a, a]"
          using assms lunit_hcomp [of a a] lunit_commutes_with_L [of a] by auto
        moreover have "(a  𝗅[a])  𝖺[a, a, a] = R 𝗋[a]"
          using assms triangle [of a a] by auto
        moreover have "(a  𝗅[a])  𝖺[a, a, a] = R 𝗂[a]"
        proof -
          have "(a  𝗅[a])  𝖺[a, a, a] = ((𝗂[a]  a)  𝖺-1[a, a, a])  𝖺[a, a, a]"
            using assms lunit_char(2) by force
          also have "... = R 𝗂[a]"
            using assms comp_arr_dom comp_assoc comp_assoc_assoc'
            apply (elim objE)
            by (simp add: assms)
          finally show ?thesis by blast
        qed
        ultimately show ?thesis by argo
      qed
      moreover have "par 𝗅[a] 𝗂[a]  par 𝗋[a] 𝗂[a]"
        using assms by auto
      ultimately have 1: "𝗅[a] = 𝗂[a]  𝗋[a] = 𝗂[a]"
        using R.is_faithful by blast
      show "𝗅[a] = 𝗂[a]" using 1 by auto
      show "𝗋[a] = 𝗂[a]" using 1 by auto
    qed

    lemma unit_triangle:
    assumes "obj a"
    shows "𝗂[a]  a = (a  𝗂[a])  𝖺[a, a, a]"
    and "(𝗂[a]  a)  𝖺-1[a, a, a] = a  𝗂[a]"
    proof -
      show 1: "𝗂[a]  a = (a  𝗂[a])  𝖺[a, a, a]"
        using assms triangle [of a a] unitor_coincidence by auto
      show "(𝗂[a]  a)  𝖺-1[a, a, a] = a  𝗂[a]"
        using assms 1 invert_side_of_triangle(2) [of "𝗂[a]  a" "a  𝗂[a]" "𝖺[a, a, a]"]
              assoc'_eq_inv_assoc
        by (metis hseqI' iso_assoc objE obj_def' unit_simps(1) unit_simps(2))
    qed

    lemma hcomp_assoc_isomorphic:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "(f  g)  h  f  g  h"
      using assms assoc_in_hom [of f g h] iso_assoc isomorphic_def by auto

    lemma hcomp_arr_obj:
    assumes "arr μ" and "obj a" and "src μ = a"
    shows "μ  a = 𝗋-1[cod μ]  μ  𝗋[dom μ]"
    and "𝗋[cod μ]  (μ  a)  𝗋-1[dom μ] = μ"
    proof -
      show "μ  a = 𝗋-1[cod μ]  μ  𝗋[dom μ]"
        using assms iso_runit runit_naturality comp_cod_arr
        by (metis ide_cod ide_dom invert_side_of_triangle(1) runit_simps(1) runit_simps(5) seqI)
      show "𝗋[cod μ]  (μ  a)  𝗋-1[dom μ] = μ"
        using assms iso_runit runit_naturality [of μ] comp_cod_arr
        by (metis ide_dom invert_side_of_triangle(2) comp_assoc runit_simps(1)
            runit_simps(5) seqI)
    qed

    lemma hcomp_obj_arr:
    assumes "arr μ" and "obj b" and "b = trg μ"
    shows "b  μ = 𝗅-1[cod μ]  μ  𝗅[dom μ]"
    and "𝗅[cod μ]  (b  μ)  𝗅-1[dom μ] = μ"
    proof -
      show "b  μ = 𝗅-1[cod μ]  μ  𝗅[dom μ]"
        using assms iso_lunit lunit_naturality comp_cod_arr
        by (metis ide_cod ide_dom invert_side_of_triangle(1) lunit_simps(1) lunit_simps(5) seqI)
      show "𝗅[cod μ]  (b  μ)  𝗅-1[dom μ] = μ"
        using assms iso_lunit lunit_naturality [of μ] comp_cod_arr
        by (metis ide_dom invert_side_of_triangle(2) comp_assoc lunit_simps(1)
            lunit_simps(5) seqI)
    qed

    lemma hcomp_reassoc:
    assumes "arr τ" and "arr μ" and "arr ν"
    and "src τ = trg μ" and "src μ = trg ν"
    shows "(τ  μ)  ν = 𝖺-1[cod τ, cod μ, cod ν]  (τ  μ  ν)  𝖺[dom τ, dom μ, dom ν]"
    and "τ  μ  ν = 𝖺[cod τ, cod μ, cod ν]  ((τ  μ)  ν)  𝖺-1[dom τ, dom μ, dom ν]"
    proof -
      show "(τ  μ)  ν = 𝖺-1[cod τ, cod μ, cod ν]  (τ  μ  ν)  𝖺[dom τ, dom μ, dom ν]"
      proof -
        have "(τ  μ)  ν = (𝖺-1[cod τ, cod μ, cod ν]  𝖺[cod τ, cod μ, cod ν])  ((τ  μ)  ν)"
          using assms comp_assoc_assoc'(2) comp_cod_arr by simp
        also have "... = 𝖺-1[cod τ, cod μ, cod ν]  𝖺[cod τ, cod μ, cod ν]  ((τ  μ)  ν)"
          using comp_assoc by simp
        also have "... = 𝖺-1[cod τ, cod μ, cod ν]  (τ  μ  ν)  𝖺[dom τ, dom μ, dom ν]"
          using assms assoc_naturality by simp
        finally show ?thesis by simp
      qed
      show "τ  μ  ν = 𝖺[cod τ, cod μ, cod ν]  ((τ  μ)  ν)  𝖺-1[dom τ, dom μ, dom ν]"
      proof -
        have "τ  μ  ν = (τ  μ  ν)  𝖺[dom τ, dom μ, dom ν]  𝖺-1[dom τ, dom μ, dom ν]"
          using assms comp_assoc_assoc'(1) comp_arr_dom by simp
        also have "... = ((τ  μ  ν)  𝖺[dom τ, dom μ, dom ν])  𝖺-1[dom τ, dom μ, dom ν]"
          using comp_assoc by simp
        also have "... = (𝖺[cod τ, cod μ, cod ν]  ((τ  μ)  ν))  𝖺-1[dom τ, dom μ, dom ν]"
          using assms assoc_naturality by simp
        also have "... = 𝖺[cod τ, cod μ, cod ν]  ((τ  μ)  ν)  𝖺-1[dom τ, dom μ, dom ν]"
          using comp_assoc by simp
        finally show ?thesis by simp
      qed
    qed

    lemma triangle':
    assumes "ide f" and "ide g" and "src f = trg g"
    shows "(f  𝗅[g]) = (𝗋[f]  g)  𝖺-1[f, src f, g]"
      using assms(1-3) invert_side_of_triangle(2) triangle by force

    lemma pentagon':
    assumes "ide f" and "ide g" and "ide h" and "ide k"
    and "src f = trg g" and "src g = trg h" and "src h = trg k"
    shows "((𝖺-1[f, g, h]  k)  𝖺-1[f, g  h, k])  (f  𝖺-1[g, h, k])
              = 𝖺-1[f  g, h, k]  𝖺-1[f, g, h  k]"
    proof -
      have "((𝖺-1[f, g, h]  k)  𝖺-1[f, g  h, k])  (f  𝖺-1[g, h, k])
              = inv ((f  𝖺[g, h, k])  (𝖺[f, g  h, k]  (𝖺[f, g, h]  k)))"
      proof -
        have "inv ((f  𝖺[g, h, k])  (𝖺[f, g  h, k]  (𝖺[f, g, h]  k))) =
              inv (𝖺[f, g  h, k]  (𝖺[f, g, h]  k))  inv (f  𝖺[g, h, k])"
          using assms inv_comp [of "𝖺[f, g  h, k]  (𝖺[f, g, h]  k)" "f  𝖺[g, h, k]"]
          by force
        also have "... = (inv (𝖺[f, g, h]  k)  inv 𝖺[f, g  h, k])  inv (f  𝖺[g, h, k])"
          using assms iso_assoc inv_comp by simp
        also have "... = ((𝖺-1[f, g, h]  k)  𝖺-1[f, g  h, k])  (f  𝖺-1[g, h, k])"
          using assms inv_hcomp by simp
        finally show ?thesis by simp
      qed
      also have "... = inv (𝖺[f, g, h  k]  𝖺[f  g, h, k])"
        using assms pentagon by simp
      also have "... = 𝖺-1[f  g, h, k]  𝖺-1[f, g, h  k]"
        using assms inv_comp by simp
      finally show ?thesis by auto
    qed

  end

  text ‹
    The following convenience locale extends @{locale bicategory} by pre-interpreting
    the various functors and natural transformations.
  ›

  locale extended_bicategory =
    bicategory +
    L: equivalence_functor V V L +
    R: equivalence_functor V V R +
    α: natural_isomorphism VVV.comp V HoHV HoVH
          λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ)) +
    α': inverse_transformation VVV.comp V HoHV HoVH
          λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ)) +
    𝔩: natural_isomorphism V V L map 𝔩 +
    𝔩': inverse_transformation V V L map 𝔩 +
    𝔯: natural_isomorphism V V R map 𝔯 +
    𝔯': inverse_transformation V V R map 𝔯

  sublocale bicategory  extended_bicategory V H 𝖺 𝗂 src trg
  proof -
    interpret L: equivalence_functor V V L using equivalence_functor_L by auto
    interpret R: equivalence_functor V V R using equivalence_functor_R by auto
    interpret α': inverse_transformation VVV.comp V HoHV HoVH
                    λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ)) ..
    interpret 𝔩: natural_isomorphism V V L map 𝔩 using natural_isomorphism_𝔩 by auto
    interpret 𝔩': inverse_transformation V V L map 𝔩 ..
    interpret 𝔯: natural_isomorphism V V R map 𝔯 using natural_isomorphism_𝔯 by auto
    interpret 𝔯': inverse_transformation V V R map 𝔯 ..
    interpret extended_bicategory V H 𝖺 𝗂 src trg ..
    show "extended_bicategory V H 𝖺 𝗂 src trg" ..
  qed

end