Quelle  Bicategory.thy

(*  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
         ‹λμντ. a (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 ==> 'a"     (‹a[_, _, _]›)
  and i :: "'a ==> 'a"                 (‹i[_]›)
  and src :: "'a ==> 'a"
  and trg :: "'a ==> 'a" +
  assumes unit_in_vhom: "obj a ==> «i[a] : a ⋆ a ==> a¬"
  and iso_unit: "obj a ==> iso i[a]"
  and pentagon: "[ ide f; ide g; ide h; ide k; src f = trg g; src g = trg h; src h = trg k ] ==>
                   (f ⋆ a[g, h, k]) ⋅ a[f, g ⋆ h, k] ⋅ (a[f, g, h] ⋆ k) = a[f, g, h ⋆ k] ⋅ a[f ⋆ g, h, k]"
  begin
    (*
     * TODO: the mapping \<i> is not currently assumed to be extensional.
     * It might be best in the long run if it were.
     *)

    definition α
    where "α μντ ≡ a (fst μντ) (fst (snd μντ)) (snd (snd μντ))"

    lemma assoc_in_hom':
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "in_hhom a[μ, ν, τ] (src τ) (trg μ)"
    and "«a[μ, ν, τ] : (dom μ ⋆ dom ν) ⋆ dom τ ==> cod μ ⋆ cod ν ⋆ cod τ¬"
    proof -
      show "«a[μ, ν, τ] : (dom μ ⋆ dom ν) ⋆ dom τ ==> cod μ ⋆ cod ν ⋆ cod τ¬"
      proof -
        have 1: "VVV.in_hom (μ, ν, τ) (dom μ, dom ν, dom τ) (cod μ, cod ν, cod τ)"
          using assms VVV.in_hom_char_SbC VVV.arr_char_SbC VV.arr_char_SbC by auto
        have "«a[μ, ν, τ] : 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_char_SbC)
        moreover have "HoVH (cod μ, cod ν, cod τ) = cod μ ⋆ cod ν ⋆ cod τ"
          using 1 HoVH_def by (simp add: VVV.in_hom_char_SbC)
        ultimately show ?thesis by simp
      qed
      thus "in_hhom a[μ, ν, τ] (src τ) (trg μ)"
        using assms src_cod trg_cod vconn_implies_hpar(1) vconn_implies_hpar(2) by auto
    qed

    lemma assoc_naturality1:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "a[μ, ν, τ] = (μ ⋆ ν ⋆ τ) ⋅ a[dom μ, dom ν, dom τ]"
      using assms α.naturality1 [of "(μ, ν, τ)"] VVV.arr_char_SbC VV.arr_char_SbC VVV.dom_char_SbC
            HoVH_def src_dom trg_dom
      by simp

    lemma assoc_naturality2:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "a[μ, ν, τ] = a[cod μ, cod ν, cod τ] ⋅ ((μ ⋆ ν) ⋆ τ)"
      using assms α.naturality2 [of "(μ, ν, τ)"] VVV.arr_char_SbC VV.arr_char_SbC VVV.cod_char_SbC
            HoHV_def src_dom trg_dom
      by simp

    lemma assoc_naturality:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "a[cod μ, cod ν, cod τ] ⋅ ((μ ⋆ ν) ⋆ τ) = (μ ⋆ ν ⋆ τ) ⋅ a[dom μ, dom ν, dom τ]"
      using assms α.naturality VVV.arr_char_SbC VV.arr_char_SbC HoVH_def HoHV_def
            VVV.dom_char_SbC VVV.cod_char_SbC
      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 a[f, g, h] (src h) (trg f)"
    and "«a[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 a[f, g, h]"
    and "src a[f, g, h] = src h" and "trg a[f, g, h] = trg f"
    and "dom a[f, g, h] = (dom f ⋆ dom g) ⋆ dom h"
    and "cod a[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 a[f, g, h]"
      using assms α.components_are_iso [of "(f, g, h)"] VVV.ide_char_SbC VVV.arr_char_SbC VV.arr_char_SbC
      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_char_SbC V.null_char ext
          apply force
      using H.VV.arr_char_SbC V.null_char H.VV.dom_char_SbC H.VV.cod_char_SbC
         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_char_SbC 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_char_SbC H.VV.ide_char_SbC 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_char_SbC 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 a
    where "a f g h ≡ f ⋅ g ⋅ h"

    interpretation α: natural_isomorphism H.VVV.comp V H.HoHV H.HoVH
                        ‹λμντ. a (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_char_SbC H.VV.arr_char_SbC H.VVV.dom_char_SbC
            H.VV.dom_char_SbC H.VVV.cod_char_SbC H.VV.cod_char_SbC 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 i
    where "i ≡ λx. x"

    proposition induces_bicategory:
    shows "bicategory V C a i 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-‹I› functors
 as src and trg and ‹ι› as the unit isomorphism from ‹I ⊗ I› to ‹I›.
 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 I
      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_char_SbC 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_char_SbC 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.seqE_PC CC_eq_VV I.map_simp
                I.preserves_reflects_arr VV.seq_char_SbC VVV.arrI_SbC VVV.comp_simp VVV.seq_char_SbC
                trg_vcomp vseq_implies_hpar(1))
          moreover have "¬ CCC.seq g f ==> CCC.comp g f = VVV.comp g f"
            using VVV.seq_char_SbC 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.extensionality CC_eq_VV CC.arr_char by force

    lemma L'_eq_L:
    shows "H.L = L"
      using H.extensionality 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 = I"
      using obj_def [of a] unit_in_hom by fastforce

    proposition induces_bicategory:
    shows "bicategory C tensor (λμ ν τ. α (μ, ν, τ)) (λ_. ι) I.map I.map"
      using unit_in_hom unit_is_iso pentagon α.extensionality
            α.naturality1 α.naturality2 CCC.arrE CCC_eq_VVV
      by unfold_locales auto

  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 ‹l› and ‹r› 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_char_PBH 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_char_PBH 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  (‹l[_]›)
    where "lunit f ≡ left_hom_with_unit.lunit V H a i[trg f] (trg f) f"

    definition runit  (‹r[_]›)
    where "runit f ≡ right_hom_with_unit.runit V H a i[src f] (src f) f"

    lemma lunit_in_hom:
    assumes "ide f"
    shows "«l[f] : src f →_WC trg f¬" and "«l[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 a ‹i[trg f]› ‹trg f›
        using assms obj_is_weak_unit iso_unit_PBU by (unfold_locales, auto)
      have 0: "Left.ide f"
        using assms Left.ide_char_SbC Left.arr_char_SbC left_def composable_char_PBH by auto
      show 1: "«l[f] : trg f ⋆ f ==> f¬"
        unfolding lunit_def
        using assms 0 Left.lunit_char(1) Left.hom_char H_{L_def} by auto
      show "«l[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 "«r[f] : src f →_WC trg f¬" and "«r[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 a ‹i[src f]› ‹src f›
        using assms obj_is_weak_unit iso_unit_PBU by (unfold_locales, auto)
      have 0: "Right.ide f"
        using assms Right.ide_char_SbC Right.arr_char_SbC right_def composable_char_PBH by auto
      show 1: "«r[f] : f ⋆ src f ==> f¬"
        unfolding runit_def
        using assms 0 Right.runit_char(1) Right.hom_char H_{R_def} by auto
      show "«r[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 "«l[f] : src f →_WC trg f¬" and "«l[f] : trg f ⋆ f ==> f¬"
    and "trg f ⋆ l[f] = (i[trg f] ⋆ f) ⋅ inv a[trg f, trg f, f]"
    and "∃!μ. «μ : trg f ⋆ f ==> f¬ ∧ trg f ⋆ μ = (i[trg f] ⋆ f) ⋅ inv a[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 a ‹i[?b]› ?b
        using assms obj_is_weak_unit iso_unit_PBU by (unfold_locales, auto)
      have 0: "Left.ide f"
        using assms Left.ide_char_SbC Left.arr_char_SbC left_def composable_char_PBH by auto
      show "«l[f] : src f →_WC trg f¬"
        using assms lunit_in_hom by simp
      show A: "«l[f] : trg f ⋆ f ==> f¬"
        using assms lunit_in_hom by simp
      show B: "?b ⋆ l[f] = (i[?b] ⋆ f) ⋅ inv a[?b, ?b, f]"
        unfolding lunit_def using 0 Left.lunit_char(2) H_{L_def}
        by (metis Left.comp_simp Left.characteristic_iso(1-2) Left.seqI')
      show "∃!μ. «μ : trg f ⋆ f ==> f¬ ∧ trg f ⋆ μ = (i[?b] ⋆ f) ⋅ inv a[?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 H_{L_def} by simp
          show "Left.hom (Left.L f) f ⊆ hom (?b ⋆ f) f"
            using assms Left.hom_char [of "?b ⋆ f" f] H_{L_def} by simp
          show "hom (?b ⋆ f) f ⊆ Left.hom (Left.L f) f"
            using assms 1 ide_in_hom composable_char_PBH 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 μ = (i[?b] ⋆ f) ⋅ (inv a[?b, ?b, f])"
        let ?R = "λμ. ?b ⋆ μ = (i[?b] ⋆ f) ⋅ (inv a[?b, ?b, f])"
        have 2: "?P = ?P'"
          using 0 1 H_{L_def} Left.hom_char by blast
        moreover have "∀μ. ?P μ ⟶ (?Q μ ⟷ ?R μ)"
          using 2 Left.lunit_eqI H_{L_def} by presburger
        moreover have "(∃!μ. ?P μ ∧ ?Q μ)"
          using 0 2 A B Left.lunit_char(3) Left.ide_char Left.arr_char_SbC
          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 "«r[f] : src f →_WC trg f¬" and "«r[f] : f ⋆ src f ==> f¬"
    and "r[f] ⋆ src f = (f ⋆ i[src f]) ⋅ a[f, src f, src f]"
    and "∃!μ. «μ : f ⋆ src f ==> f¬ ∧ μ ⋆ src f = (f ⋆ i[src f]) ⋅ a[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 ‹i[?a]› ?a
        using assms obj_is_weak_unit iso_unit_PBU by (unfold_locales, auto)
      have 0: "Right.ide f"
        using assms Right.ide_char_SbC Right.arr_char_SbC right_def composable_char_PBH by auto
      show "«r[f] : src f →_WC trg f¬"
        using assms runit_in_hom by simp
      show A: "«r[f] : f ⋆ src f ==> f¬"
        using assms runit_in_hom by simp
      show B: "r[f] ⋆ ?a = (f ⋆ i[?a]) ⋅ a[f, ?a, ?a]"
        unfolding runit_def using 0 Right.runit_char(2) H_{R_def}
        using Right.comp_simp Right.characteristic_iso(4) Right.iso_is_arr by auto
      show "∃!μ. «μ : f ⋆ src f ==> f¬ ∧ μ ⋆ ?a = (f ⋆ i[?a]) ⋅ 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 H_{R_def} by simp
          show "Right.hom (Right.R f) f ⊆ hom (f ⋆ ?a) f"
            using assms Right.hom_char [of "f ⋆ ?a" f] H_{R_def} by simp
          show "hom (f ⋆ ?a) f ⊆ Right.hom (Right.R f) f"
            using assms 1 ide_in_hom composable_char_PBH 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 ⋆ i[?a]) ⋅ a[f, ?a, ?a]"
        let ?R = "λμ. μ ⋆ ?a = (f ⋆ i[?a]) ⋅ a[f, ?a, ?a]"
        have 2: "?P = ?P'"
          using 0 1 H_{R_def} Right.hom_char by blast
        moreover have "∀μ. ?P μ ⟶ (?Q μ ⟷ ?R μ)"
          using 2 Right.runit_eqI H_{R_def} by presburger
        moreover have "(∃!μ. ?P μ ∧ ?Q μ)"
          using 0 2 A B Right.runit_char(3) Right.ide_char Right.arr_char_SbC
          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 ⋆ μ = (i[trg f] ⋆ f) ⋅ (inv a[trg f, trg f, f])"
    shows "μ = l[f]"
      using assms lunit_char(2-4) by blast

    lemma runit_eqI:
    assumes "ide f" and "«μ : f ⋆ src f ==> f¬"
    and "μ ⋆ src f = (f ⋆ i[src f]) ⋅ a[f, src f, src f]"
    shows "μ = r[f]"
      using assms runit_char(2-4) by blast

    lemma iso_lunit:
    assumes "ide f"
    shows "iso l[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 a ‹i[?b]› ?b
        using assms obj_is_weak_unit iso_unit_PBU by (unfold_locales, auto)
      show ?thesis
      proof -
        have 0: "Left.ide f"
          using assms Left.ide_char_SbC Left.arr_char_SbC left_def composable_char_PBH 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 r[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 ‹i[?a]› ?a
        using assms obj_is_weak_unit iso_unit_PBU by (unfold_locales, auto)
      show ?thesis
      proof -
        have 0: "Right.ide f"
          using assms Right.ide_char_SbC Right.arr_char_SbC right_def composable_char_PBH by auto
        thus ?thesis
          unfolding runit_def using Right.iso_runit Right.iso_char by blast
      qed
    qed

    lemma lunit_naturality:
    assumes "arr μ"
    shows "μ ⋅ l[dom μ] = l[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 a ‹i[?b]› ?b
        using assms obj_is_weak_unit iso_unit_PBU by (unfold_locales, auto)
      interpret Left.L: endofunctor ‹Left ?b› Left.L
        using assms endofunctor_H_L [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_char_SbC left_def composable_char_PBH obj_trg by auto
      have 2: "Left.in_hom l[Left.dom μ] (?b ⋆ dom μ) (dom μ)"
        unfolding lunit_def
        using assms 1 Left.in_hom_char_SbC trg_dom Left.lunit_char(1) H_{L_def}
              Left.arr_char_SbC Left.dom_char_SbC Left.ide_dom
        by force
      have 3: "Left.in_hom l[Left.cod μ] (?b ⋆ cod μ) (cod μ)"
        unfolding lunit_def
        using assms 1 Left.in_hom_char_SbC trg_cod Left.lunit_char(1) H_{L_def}
              Left.cod_char_SbC 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 μ"] H_{L_def} by auto
      show ?thesis
        by (metis "1" "2" H_{L_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 "μ ⋅ r[dom μ] = r[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 ‹i[?a]› ?a
        using assms obj_is_weak_unit iso_unit_PBU by (unfold_locales, auto)
      interpret Right.R: endofunctor ‹Right ?a› Right.R
        using assms endofunctor_H_R [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_char_SbC right_def composable_char_PBH by auto
      have 2: "Right.in_hom r[Right.dom μ] (dom μ ⋆ ?a) (dom μ)"
        unfolding runit_def
        using 1 Right.in_hom_char_SbC trg_dom Right.runit_char(1) [of "Right.dom μ"] H_{R_def}
              Right.arr_char_SbC Right.dom_char_SbC Right.ide_dom assms
        by force
      have 3: "r[Right.cod μ] ∈ Right.hom (cod μ ⋆ ?a) (cod μ)"
        unfolding runit_def
        using 1 Right.in_hom_char_SbC trg_cod Right.runit_char(1) [of "Right.cod μ"] H_{R_def}
              Right.cod_char_SbC 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 μ"] H_{R_def} by auto
      show ?thesis
        by (metis "1" "2" H_{R_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 l: transformation_by_components V V L map lunit
      using lunit_in_hom lunit_naturality by unfold_locales auto
    interpretation l: natural_isomorphism V V L map l.map
      using iso_lunit by unfold_locales auto

    lemma natural_isomorphism_l:
    shows "natural_isomorphism V V L map l.map"
      ..

    interpretation L: equivalence_functor V V L
      using L.isomorphic_to_identity_is_equivalence l.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[L f] = L l[f]"
    proof -
      have "seq l[f] (L l[f])"
        using assms lunit_char(2) L.preserves_hom by fastforce
      moreover have "seq l[f] l[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 "l[f]"] iso_lunit
              iso_is_section section_is_mono mono_cancel [of "l[f]" "L l[f]" "l[L f]"]
        by auto
    qed

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

    lemma natural_isomorphism_r:
    shows "natural_isomorphism V V R map r.map"
      ..

    interpretation R: equivalence_functor V V R
      using R.isomorphic_to_identity_is_equivalence r.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[R f] = R r[f]"
    proof -
      have "seq r[f] (R r[f])"
        using assms runit_char(2) R.preserves_hom by fastforce
      moreover have "seq r[f] r[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 "r[f]"] iso_runit
              iso_is_section section_is_mono mono_cancel [of "r[f]" "R r[f]" "r[R f]"]
        by auto
    qed

    definition α
    where "α μ ν τ ≡ if VVV.arr (μ, ν, τ) then
                        (μ ⋆ ν ⋆ τ) ⋅ a[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 = a[f, g, h]"
    proof -
      have "α f g h = (f ⋆ g ⋆ h) ⋅ a[dom f, dom g, dom h]"
        using assms α_def VVV.arr_char_SbC [of "(f, g, h)"] by auto
      also have "... = (f ⋆ g ⋆ h) ⋅ a[f, g, h]"
        using assms by simp
      also have "... = a[f, g, h]"
        using assms α_def assoc_in_hom_AWC hcomp_in_hom_PBH VVV.arr_char_SbC VoV.arr_char_SbC
              comp_cod_arr composable_char_PBH
        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. a[fst f, fst (snd f), snd (snd f)]›
      proof
        show 1: "∧x. VVV.ide x ==> «a[fst x, fst (snd x), snd (snd x)] : HoHV x ==> HoVH x¬"
        proof -
          fix x
          assume x: "VVV.ide x"
          show "«a[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_char_SbC VVV.arr_char_SbC VV.arr_char_SbC composable_char_PBH by simp
            hence "a[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_hom_AWC by simp
            thus ?thesis
              unfolding HoHV_def HoVH_def
              using x VVV.ideD(1) by simp
          qed
        qed
        show "∧f. VVV.arr f ==>
                   a[fst (VVV.cod f), fst (snd (VVV.cod f)), snd (snd (VVV.cod f))] ⋅ HoHV f =
                   HoVH f ⋅ a[fst (VVV.dom f), fst (snd (VVV.dom f)), snd (snd (VVV.dom f))]"
          unfolding HoHV_def HoVH_def
          using assoc_naturality_AWC VVV.arr_char_SbC VV.arr_char_SbC VVV.dom_char_SbC VVV.cod_char_SbC
                composable_char_PBH
          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_char_SbC [of f] VV.arr_char_SbC composable_char_PBH by auto
          thus ?thesis
            using f α.map_simp_ide iso_assoc_AWC VVV.ide_char_SbC VVV.arr_char_SbC 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 μντ)) ⋅
                  a[dom (fst μντ), dom (fst (snd μντ)), dom (snd (snd μντ))]"
            using μντ α_def by simp
          also have "... = a[cod (fst μντ), cod (fst (snd μντ)), cod (snd (snd μντ))] ⋅
                             ((fst μντ ⋆ fst (snd μντ)) ⋆ snd (snd μντ))"
            using μντ HoHV_def HoVH_def VVV.arr_char_SbC VV.arr_char_SbC assoc_naturality_AWC
                  composable_char_PBH
            by simp
          also have "... =
                     a[fst (VVV.cod μντ), fst (snd (VVV.cod μντ)), snd (snd (VVV.cod μντ))] ⋅
                       ((fst μντ ⋆ fst (snd μντ)) ⋆ snd (snd μντ))"
            using μντ VVV.arr_char_SbC VVV.cod_char_SbC VV.arr_char_SbC by simp
          also have "... = α.map μντ"
            using μντ α.map_def HoHV_def composable_char_PBH 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 α i 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 α i src trg"
      proof
        show "∧a. obj a ==> «i[a] : a ⋆ a ==> a¬"
          using obj_is_weak_unit unit_in_vhom_PBU by blast
        show "∧a. obj a ==> iso i[a]"
          using obj_is_weak_unit iso_unit_PBU 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 = a[f, g, h] ∧ α g h k = a[g, h, k]"
            using f g h k fg gh hk α_ide_simp by simp
          moreover have "α f (g ⋆ h) k = a[f, g ⋆ h, k] ∧ α f g (h ⋆ k) = a[f, g, h ⋆ k] ∧
                         α (f ⋆ g) h k = a[f ⋆ g, h, k]"
            using f g h k fg gh hk α_ide_simp preserves_ide hcomp_in_hom_PBH(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 pentagon_AWC [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 a some_src some_trg
      using extends_to_prebicategory_with_homs by auto

    interpretation prebicategory_with_units V H a some_unit
      using extends_to_prebicategory_with_units by auto

    interpretation prebicategory_with_homs_and_units V H a 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
                         ‹λμντ. a (fst μντ) (fst (snd μντ)) (snd (snd μντ))› ..

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

    definition a'  (‹a^-1[_, _, _]›)
    where "a^-1[μ, ν, τ] ≡ α'.map (μ, ν, τ)"

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

    lemma assoc'_naturality1:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "a^-1[μ, ν, τ] = ((μ ⋆ ν) ⋆ τ) ⋅ a^-1[dom μ, dom ν, dom τ]"
      using assms α'.naturality1 [of "(μ, ν, τ)"] VVV.arr_char_SbC VV.arr_char_SbC
            VVV.dom_char_SbC HoHV_def src_dom trg_dom a'_def
      by simp

    lemma assoc'_naturality2:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "a^-1[μ, ν, τ] = a^-1[cod μ, cod ν, cod τ] ⋅ (μ ⋆ ν ⋆ τ)"
      using assms α'.naturality2 [of "(μ, ν, τ)"] VVV.arr_char_SbC VV.arr_char_SbC
            VVV.cod_char_SbC HoVH_def src_dom trg_dom a'_def
      by simp

    lemma assoc'_naturality:
    assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
    shows "a^-1[cod μ, cod ν, cod τ] ⋅ (μ ⋆ ν ⋆ τ) = ((μ ⋆ ν) ⋆ τ) ⋅ a^-1[dom μ, dom ν, dom τ]"
      using assms assoc'_naturality1 assoc'_naturality2 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 a^-1[f, g, h] (src h) (trg f)"
    and "«a^-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 a^-1[f, g, h]"
    and "src a^-1[f, g, h] = src h" and "trg a^-1[f, g, h] = trg f"
    and "dom a^-1[f, g, h] = dom f ⋆ dom g ⋆ dom h"
    and "cod a^-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 "a^-1[f, g, h] = inv a[f, g, h]"
      using assms VVV.ide_char_SbC VVV.arr_char_SbC VV.ide_char_SbC VV.arr_char_SbC α'.map_ide_simp
            a'_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 a[f, g, h] a^-1[f, g, h]"
      using assms VVV.ide_char_SbC VVV.arr_char_SbC VV.ide_char_SbC VV.arr_char_SbC α'.map_ide_simp
            α'.inverts_components a'_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 a^-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 "a[f, g, h] ⋅ a^-1[f, g, h] = f ⋆ g ⋆ h"
    and "a^-1[f, g, h] ⋅ a[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 "«i[a] : a → a¬" and "«i[a] : a ⋆ a ==> a¬"
    proof -
      show "«i[a] : a ⋆ a ==> a¬"
        using assms unit_in_vhom by simp
      thus "«i[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.extensionality [of "(ν, μ)"] VV.arr_char_SbC 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 ‹H_L 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› ‹H_L a›
        using assms obj_self_composable endofunctor_H_L [of a] by force
      interpret La: fully_faithful_functor ‹Left a› ‹Left a› ‹H_L a›
      proof
        show "∧f f'. Left_a.par f f' ==> H_L a f = H_L a f' ==> f = f'"
        proof -
          fix μ μ'
          assume par: "Left_a.par μ μ'"
          assume eq: "H_L a μ = H_L a μ'"
          have 1: "par μ μ'"
            using par Left_a.arr_char_SbC Left_a.dom_char_SbC Left_a.cod_char_SbC left_def
                  composable_implies_arr null_agreement
            by metis
          moreover have "L μ = L μ'"
            using par eq H_{L_def} Left_a.arr_char_SbC 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 μ (H_L a f) (H_L a g) ] ==>
                        ∃ν. Left_a.in_hom ν f g ∧ H_L a ν = μ"
        proof -
          fix f g μ
          assume f: "Left_a.ide f" and g: "Left_a.ide g"
          and μ: "Left_a.in_hom μ (H_L a f) (H_L a g)"
          have 1: "a = trg f ∧ a = trg g"
            using assms f g Left_a.ide_char Left_a.arr_char_SbC left_def seq_if_composable [of a f]
                  seq_if_composable [of a g]
            by auto
          show "∃ν. Left_a.in_hom ν f g ∧ H_L a ν = μ"
          proof -
            have 2: "∃ν. «ν : f ==> g¬ ∧ L ν = μ"
              using f g μ 1 Left_a.ide_char_SbC H_{L_def} L.preserves_reflects_arr Left_a.arr_char_SbC
                    Left_a.in_hom_char_SbC 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_char_SbC left_def hseq_char' by fastforce
            moreover have "H_L a ν = μ"
              using ν 1 trg_dom H_{L_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› ‹H_R a›
        using assms obj_self_composable endofunctor_H_R [of a] by force
      interpret Ra: fully_faithful_functor ‹Right a› ‹Right a› ‹H_R a›
      proof
        show "∧f f'. Right_a.par f f' ==> H_R a f = H_R a f' ==> f = f'"
        proof -
          fix μ μ'
          assume par: "Right_a.par μ μ'"
          assume eq: "H_R a μ = H_R a μ'"
          have 1: "par μ μ'"
            using par Right_a.arr_char_SbC Right_a.dom_char_SbC Right_a.cod_char_SbC right_def
                  composable_implies_arr null_agreement
            by metis
          moreover have "R μ = R μ'"
            using par eq H_{R_def} Right_a.arr_char_SbC 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 μ (H_R a f) (H_R a g) ] ==>
                        ∃ν. Right_a.in_hom ν f g ∧ H_R a ν = μ"
        proof -
          fix f g μ
          assume f: "Right_a.ide f" and g: "Right_a.ide g"
          and μ: "Right_a.in_hom μ (H_R a f) (H_R a g)"
          have 1: "a = src f ∧ a = src g"
            using assms f g Right_a.ide_char Right_a.arr_char_SbC right_def seq_if_composable
            by auto
          show "∃ν. Right_a.in_hom ν f g ∧ H_R a ν = μ"
          proof -
            have 2: "∃ν. «ν : f ==> g¬ ∧ R ν = μ"
              using f g μ 1 Right_a.ide_char_SbC H_{R_def} R.preserves_reflects_arr Right_a.arr_char_SbC
                    Right_a.in_hom_char_SbC 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_char_SbC right_def hseq_char' by fastforce
            moreover have "H_R a ν = μ"
              using ν 1 src_dom H_{R_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› ‹H_L 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 H_{L_def} La.extensionality La.preserves_arr Left_a.dom_closed
            Left_a.in_hom_char_SbC 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.ideI_SbC 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 φ] H_{L_def} by auto
      have "Left_a.iso ψ"
        using ψ 1 H_{L_def} La.reflects_iso by auto
      hence "iso ψ ∧ «ψ : f ==> g¬"
        using ψ Left_a.iso_char Left_a.in_hom_char_SbC 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› ‹H_R 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_char_SbC Right_a.arr_char_SbC 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 φ] H_{R_def} by auto
      have "Right_a.iso ψ"
        using ψ 1 H_{R_def} R.reflects_iso by auto
      hence "iso ψ ∧ «ψ : f ==> g¬"
        using ψ Right_a.iso_char Right_a.in_hom_char_SbC 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 a^-1[a, a, src a] ∧
                           «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 a[trg b, b, b] ∧
                           «a[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 a"
    proof -
      have 1: "∧ν μ. ν ⋆ μ ≠ null ==> src ν = trg μ"
        using H.extensionality VV.arr_char_SbC by force
      show "associative_weak_composition V H a"
      proof
        show "∧f g h. ide f ==> ide g ==> ide h ==> f ⋆ g ≠ null ==> g ⋆ h ≠ null ==>
                      «a[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 a[f, g, h]"
          using 1 iso_assoc by presburger
        show "∧τ μ ν. τ ⋆ μ ≠ null ==> μ ⋆ ν ≠ null ==>
                      a[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) = (τ ⋆ μ ⋆ ν) ⋅ a[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 ⋆ a[g, h, k]) ⋅ a[f, g ⋆ h, k] ⋅ (a[f, g, h] ⋆ k) =
                        a[f, g, h ⋆ k] ⋅ a[f ⋆ g, h, k]"
           using 1 connected_iff_seq pentagon ideD(1) by auto
      qed
    qed

    interpretation associative_weak_composition V H a
      using is_associative_weak_composition by auto

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

    interpretation prebicategory V H a
      using is_prebicategory by auto

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

    interpretation prebicategory_with_homs V H a 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_simps_WC(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 a 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_simps_WC(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_char_SbC
        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_char_SbC
        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 a[h, g, f] ∧ «a[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 a
      using is_prebicategory by auto

    definition i'
    where "i' a ≡ SOME φ. iso φ ∧ φ ∈ hom (a ⋆ a) a ∧ (obj a ⟶ φ = i[a])"

    lemma i'_extends_i:
    assumes "weak_unit a"
    shows "iso (i' a)" and "«i' a : a ⋆ a ==> a¬" and "obj a ==> i' a = i[a]"
    proof -
      let ?P = "λa φ. iso φ ∧ «φ : a ⋆ a ==> a¬ ∧ (obj a ⟶ φ = i[a])"
      have "∃φ. ?P a φ"
        by (metis assms iso_some_unit(1) iso_some_unit(2) iso_unit unit_in_vhom)
      hence 1: "?P a (i' a)"
        using i'_def someI_ex [of "?P a"] by simp
      show "iso (i' a)" using 1 by simp
      show "«i' a : a ⋆ a ==> a¬" using 1 by simp
      show "obj a ==> i' a = i[a]" using 1 by simp
    qed

    proposition extends_to_prebicategory_with_units:
    shows "prebicategory_with_units V H a i'"
      using i'_extends_i by unfold_locales auto

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

    proposition extends_to_prebicategory_with_homs_and_units:
    shows "prebicategory_with_homs_and_units V H a i' src trg"
      ..

    definition lunit                 (‹l[_]›)
    where "l[a] ≡ PB.lunit a"

    definition runit                 (‹r[_]›)
    where "r[a] ≡ PB.runit a"

    abbreviation lunit'              (‹l^-1[_]›)
    where "l^-1[a] ≡ inv l[a]"

    abbreviation runit'              (‹r^-1[_]›)
    where "r^-1[a] ≡ inv r[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 ‹i'›,
 rather than the given ‹i›. We want ``native versions'' for the present context.
 ›

    lemma lunit_char:
    assumes "ide f"
    shows "«l[f] : L f ==> f¬" and "L l[f] = (i[trg f] ⋆ f) ⋅ a^-1[trg f, trg f, f]"
    and "∃!μ. «μ : L f ==> f¬ ∧ L μ = (i[trg f] ⋆ f) ⋅ a^-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 "«l[f] : L f ==> f¬"
        unfolding lunit_def
        using assms PB.lunit_char by simp
      show "L l[f] = (i[trg f] ⋆ f) ⋅ a^-1[trg f, trg f, f]"
        unfolding lunit_def
        using assms 1 PB.lunit_char obj_is_weak_unit i'_extends_i by simp
      let ?P = "λμ. «μ : L f ==> f¬ ∧ L μ = (i[trg f] ⋆ f) ⋅ a^-1[trg f, trg f, f]"
      have "?P = (λμ. «μ : trg f ⋆ f ==> f¬ ∧
                      trg f ⋆ μ = (i' (trg f) ⋆ f) ⋅ inv a[trg f, trg f, f])"
      proof -
        have "∧μ. «μ : L f ==> f¬ ⟷ «μ : trg f ⋆ f ==> f¬"
          using assms by simp
        moreover have "∧μ. «μ : L f ==> f¬ ==>
                            L μ = (i[trg f] ⋆ f) ⋅ a^-1[trg f, trg f, f] ⟷
                            trg f ⋆ μ = (i' (trg f) ⋆ f) ⋅ inv a[trg f, trg f, f]"
          using calculation obj_is_weak_unit i'_extends_i by auto
        ultimately show ?thesis by blast
      qed
      thus "∃!μ. «μ : L f ==> f¬ ∧ L μ = (i[trg f] ⋆ f) ⋅ a^-1[trg f, trg f, f]"
        using assms PB.lunit_char by simp
    qed

    lemma lunit_in_hom [intro]:
    assumes "ide f"
    shows "«l[f] : src f → trg f¬" and "«l[f] : trg f ⋆ f ==> f¬"
    proof -
      show "«l[f] : trg f ⋆ f ==> f¬"
        using assms lunit_char by auto
      thus "«l[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 "«l[f] : b ⋆ f ==> f¬"
      using assms by auto

    lemma lunit_simps [simp]:
    assumes "ide f"
    shows "arr l[f]" and "src l[f] = src f" and "trg l[f] = trg f"
    and "dom l[f] = trg f ⋆ f" and "cod l[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 "«r[f] : R f ==> f¬" and "R r[f] = (f ⋆ i[src f]) ⋅ a[f, src f, src f]"
    and "∃!μ. «μ : R f ==> f¬ ∧ R μ = (f ⋆ i[src f]) ⋅ a[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 "«r[f] : R f ==> f¬"
        unfolding runit_def
        using assms PB.runit_char by simp
      show "R r[f] = (f ⋆ i[src f]) ⋅ a[f, src f, src f]"
        unfolding runit_def
        using assms 1 PB.runit_char obj_is_weak_unit i'_extends_i by simp
      let ?P = "λμ. «μ : R f ==> f¬ ∧ R μ = (f ⋆ i[src f]) ⋅ a[f, src f, src f]"
      have "?P = (λμ. «μ : f ⋆ src f ==> f¬ ∧
                      μ ⋆ src f = (f ⋆ i' (src f)) ⋅ a[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 ⋆ i[src f]) ⋅ a[f, src f, src f] ⟷
                            μ ⋆ src f = (f ⋆ i' (src f)) ⋅ a[f, src f, src f]"
          using calculation obj_is_weak_unit i'_extends_i by auto
        ultimately show ?thesis by blast
      qed
      thus "∃!μ. «μ : R f ==> f¬ ∧ R μ = (f ⋆ i[src f]) ⋅ a[f, src f, src f]"
        using assms PB.runit_char by simp
    qed

    lemma runit_in_hom [intro]:
    assumes "ide f"
    shows "«r[f] : src f → trg f¬" and "«r[f] : f ⋆ src f ==> f¬"
    proof -
      show "«r[f] : f ⋆ src f ==> f¬"
        using assms runit_char by auto
      thus "«r[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 "«r[f] : f ⋆ a ==> f¬"
      using assms by auto

    lemma runit_simps [simp]:
    assumes "ide f"
    shows "arr r[f]" and "src r[f] = src f" and "trg r[f] = trg f"
    and "dom r[f] = f ⋆ src f" and "cod r[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 ⋆ μ = (i[trg f] ⋆ f) ⋅ a^-1[trg f, trg f, f]"
    shows "μ = l[f]"
      unfolding lunit_def
      using assms PB.lunit_eqI i'_extends_i trg.preserves_ide obj_is_weak_unit by simp

    lemma runit_eqI:
    assumes "ide f" and "«μ : f ⋆ src f ==> f¬"
    and "μ ⋆ src f = (f ⋆ i[src f]) ⋅ a[f, src f, src f]"
    shows "μ = r[f]"
      unfolding runit_def
      using assms PB.runit_eqI i'_extends_i src.preserves_ide obj_is_weak_unit by simp

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

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

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

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

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

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

    lemma lunit'_in_hom [intro]:
    assumes "ide f"
    shows "«l^-1[f] : src f → trg f¬" and "«l^-1[f] : f ==> trg f ⋆ f¬"
    proof -
      show "«l^-1[f] : f ==> trg f ⋆ f¬"
        using assms lunit_char iso_lunit by simp
      thus "«l^-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 "«l^-1[f] : f ==> b ⋆ f¬"
      using assms by auto

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

    lemma runit'_in_hom [intro]:
    assumes "ide f"
    shows "«r^-1[f] : src f → trg f¬" and "«r^-1[f] : f ==> f ⋆ src f¬"
    proof -
      show "«r^-1[f] : f ==> f ⋆ src f¬"
        using assms runit_char iso_runit by simp
      thus "«r^-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 "«r^-1[f] : f ==> f ⋆ a¬"
      using assms by auto

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

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

    lemma natural_isomorphism_l:
    shows "natural_isomorphism V V L map l.map"
      ..

    abbreviation l
    where "l ≡ l.map"

    lemma l_ide_simp:
    assumes "ide f"
    shows "l f = l[f]"
      using assms by simp

    interpretation L: equivalence_functor V V L
      using L.isomorphic_to_identity_is_equivalence l.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[L f] = L l[f]"
      unfolding lunit_def
      using assms PB.lunit_commutes_with_L by blast

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

    lemma natural_isomorphism_r:
    shows "natural_isomorphism V V R map r.map"
      ..

    abbreviation r
    where "r ≡ r.map"

    lemma r_ide_simp:
    assumes "ide f"
    shows "r f = r[f]"
      using assms by simp

    interpretation R: equivalence_functor V V R
      using R.isomorphic_to_identity_is_equivalence r.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[R f] = R r[f]"
      unfolding runit_def
      using assms PB.runit_commutes_with_R by blast

    lemma lunit'_naturality:
    assumes "arr μ"
    shows "(trg μ ⋆ μ) ⋅ l^-1[dom μ] = l^-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 μ) ⋅ r^-1[dom μ] = r^-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 i[a]" and "src i[a] = a" and "trg i[a] = a"
    and "dom i[a] = a ⋆ a" and "cod i[a] = a"
      using assms unit_in_hom by blast+

    lemma triangle:
    assumes "ide f" and "ide g" and "src g = trg f"
    shows "(g ⋆ l[f]) ⋅ a[g, src g, f] = r[g] ⋆ f"
    proof -
      let ?b = "src g"
      have *: "(g ⋆ l[?b ⋆ f]) ⋅ a[g, ?b, ?b ⋆ f] = r[g] ⋆ ?b ⋆ f"
      proof -
        have 1: "((g ⋆ l[?b ⋆ f]) ⋅ a[g, ?b, ?b ⋆ f]) ⋅ a[g ⋆ ?b, ?b, f]
                    = (r[g] ⋆ ?b ⋆ f) ⋅ a[g ⋆ ?b, ?b, f]"
        proof -
          have "((g ⋆ l[?b ⋆ f]) ⋅ a[g, ?b, ?b ⋆ f]) ⋅ a[g ⋆ ?b, ?b, f]
                  = (g ⋆ l[?b ⋆ f]) ⋅ a[g, ?b, ?b ⋆ f] ⋅ a[g ⋆ ?b, ?b, f]"
            using HoVH_def HoHV_def comp_assoc by auto
          also have
              "... = (g ⋆ l[?b ⋆ f]) ⋅ (g ⋆ a[?b, ?b, f]) ⋅ a[g, ?b ⋆ ?b, f] ⋅ (a[g, ?b, ?b] ⋆ f)"
            using assms pentagon by force
          also have
              "... = ((g ⋆ l[?b ⋆ f]) ⋅ (g ⋆ a[?b, ?b, f])) ⋅ a[g, ?b ⋆ ?b, f] ⋅ (a[g, ?b, ?b] ⋆ f)"
            using assms assoc_in_hom HoVH_def HoHV_def comp_assoc by auto
          also have
              "... = ((g ⋆ ?b ⋆ l[f]) ⋅ (g ⋆ a[?b, ?b, f])) ⋅ a[g, ?b ⋆ ?b, f] ⋅ (a[g, ?b, ?b] ⋆ f)"
            using assms lunit_commutes_with_L lunit_in_hom by force
          also have "... = ((g ⋆ (i[?b] ⋆ f) ⋅ a^-1[?b, ?b, f]) ⋅ (g ⋆ a[?b, ?b, f]))
                             ⋅ a[g, ?b ⋆ ?b, f] ⋅ (a[g, ?b, ?b] ⋆ f)"
            using assms lunit_char(2) by force
          also have "... = (g ⋆ ((i[?b] ⋆ f) ⋅ a^-1[?b, ?b, f]) ⋅ a[?b, ?b, f])
                             ⋅ a[g, ?b ⋆ ?b, f] ⋅ (a[g, ?b, ?b] ⋆ f)"
            using assms interchange [of g g "(i[?b] ⋆ f) ⋅ a^-1[?b, ?b, f]" "a[?b, ?b, f]"]
            by auto
          also have "... = ((g ⋆ i[?b] ⋆ f) ⋅ a[g, ?b ⋆ ?b, f]) ⋅ (a[g, ?b, ?b] ⋆ f)"
            using assms comp_arr_dom comp_assoc_assoc' comp_assoc by auto
          also have "... = (a[g, ?b, f] ⋅ ((g ⋆ i[?b]) ⋆ f)) ⋅ (a[g, ?b, ?b] ⋆ f)"
            using assms assoc_naturality [of g "i[?b]" f] by simp
          also have "... = a[g, ?b, f] ⋅ ((g ⋆ i[?b]) ⋅ a[g, ?b, ?b] ⋆ f)"
            using assms interchange [of "g ⋆ i[?b]" "a[g, ?b, ?b]" f f] comp_assoc by simp
          also have "... = a[g, ?b, f] ⋅ ((r[g] ⋆ ?b) ⋆ f)"
            using assms runit_char(2) by force
          also have "... = (r[g] ⋆ ?b ⋆ f) ⋅ a[g ⋆ ?b, ?b, f]"
            using assms assoc_naturality [of "r[g]" ?b f] by auto
          finally show ?thesis by blast
        qed
        show "(g ⋆ l[?b ⋆ f]) ⋅ a[g, ?b, ?b ⋆ f] = r[g] ⋆ ?b ⋆ f"
        proof -
          have "epi a[g ⋆ ?b, ?b, f]"
            using assms preserves_ide iso_assoc iso_is_retraction retraction_is_epi by force
          thus ?thesis
            using assms 1 epi_cancel by auto
        qed
      qed
      have "(g ⋆ l[f]) ⋅ a[g, ?b, f] = ((g ⋆ l[f]) ⋅ (g ⋆ l[?b ⋆ f]) ⋅ (g ⋆ ?b ⋆ l^-1[f])) ⋅
                                     (g ⋆ ?b ⋆ l[f]) ⋅ a[g, ?b, ?b ⋆ f] ⋅ ((g ⋆ ?b) ⋆ l^-1[f])"
      proof -
        have "a[g, ?b, f] = (g ⋆ ?b ⋆ l[f]) ⋅ a[g, ?b, ?b ⋆ f] ⋅ ((g ⋆ ?b) ⋆ l^-1[f])"
        proof -
          have "a[g, ?b, f] = (g ⋆ ?b ⋆ f) ⋅ a[g, ?b, f]"
            using assms comp_cod_arr by simp
          have "a[g, ?b, f] = ((g ⋆ ?b ⋆ l[f]) ⋅ (g ⋆ ?b ⋆ l^-1[f])) ⋅ a[g, ?b, f]"
            using assms comp_cod_arr comp_arr_inv' whisker_left [of g]
                  whisker_left [of ?b "l[f]" "l^-1[f]"]
            by simp
          also have "... = (g ⋆ ?b ⋆ l[f]) ⋅ a[g, ?b, ?b ⋆ f] ⋅ ((g ⋆ ?b) ⋆ l^-1[f])"
            using assms iso_lunit assoc_naturality [of g ?b "l^-1[f]"] comp_assoc by force
          finally show ?thesis by blast
        qed
        moreover have "g ⋆ l[f] = (g ⋆ l[f]) ⋅ (g ⋆ l[?b ⋆ f]) ⋅ (g ⋆ ?b ⋆ l^-1[f])"
        proof -
          have "(g ⋆ l[?b ⋆ f]) ⋅ (g ⋆ ?b ⋆ l^-1[f]) = g ⋆ ?b ⋆ f"
          proof -
            have "(g ⋆ l[?b ⋆ f]) ⋅ (g ⋆ ?b ⋆ l^-1[f]) = (g ⋆ ?b ⋆ l[f]) ⋅ (g ⋆ ?b ⋆ l^-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 "l[f]" "l^-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 ⋆ l[f]) ⋅ (g ⋆ l[?b ⋆ f]) ⋅ ((g ⋆ ?b ⋆ l^-1[f]) ⋅ (g ⋆ ?b ⋆ l[f])) ⋅
                       a[g, ?b, ?b ⋆ f] ⋅ ((g ⋆ ?b) ⋆ l^-1[f])"
        using comp_assoc by simp
      also have "... = (g ⋆ l[f]) ⋅ (g ⋆ l[?b ⋆ f]) ⋅ ((g ⋆ ?b ⋆ (?b ⋆ f)) ⋅
                       a[g, ?b, ?b ⋆ f]) ⋅ ((g ⋆ ?b) ⋆ l^-1[f])"
        using assms iso_lunit comp_inv_arr' interchange [of g g "?b ⋆ l^-1[f]" "?b ⋆ l[f]"]
              interchange [of ?b ?b "l^-1[f]" "l[f]"] comp_assoc
        by auto
      also have "... = (g ⋆ l[f]) ⋅ ((g ⋆ l[?b ⋆ f]) ⋅ a[g, ?b, ?b ⋆ f]) ⋅ ((g ⋆ ?b) ⋆ l^-1[f])"
        using assms comp_cod_arr comp_assoc by auto
      also have "... = r[g] ⋆ f"
      proof -
        have "r[g] ⋆ f = (g ⋆ l[f]) ⋅ (r[g] ⋆ ?b ⋆ f) ⋅ ((g ⋆ ?b) ⋆ l^-1[f])"
        proof -
          have "(g ⋆ l[f]) ⋅ (r[g] ⋆ ?b ⋆ f) ⋅ ((g ⋆ ?b) ⋆ l^-1[f])
                  = (g ⋆ l[f]) ⋅ (r[g] ⋅ (g ⋆ ?b) ⋆ (?b ⋆ f) ⋅ l^-1[f])"
            using assms iso_lunit interchange [of "r[g]" "g ⋆ ?b" "?b ⋆ f" "l^-1[f]"]
            by force
          also have "... = (g ⋆ l[f]) ⋅ (r[g] ⋆ l^-1[f])"
            using assms comp_arr_dom comp_cod_arr by simp
          also have "... = r[g] ⋆ l[f] ⋅ l^-1[f]"
            using assms interchange [of g "r[g]" "l[f]" "l^-1[f]"] comp_cod_arr
            by simp
          also have "... = r[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 ⋆ l[g ⋆ h]) ⋅ (f ⋆ a[trg g, g, h]) = f ⋆ l[g] ⋆ h"
    proof -
      have "((f ⋆ l[g ⋆ h]) ⋅ (f ⋆ a[trg g, g, h])) ⋅ a[f, trg g ⋆ g, h] ⋅ (a[f, trg g, g] ⋆ h) =
            (f ⋆ (l[g] ⋆ h)) ⋅ a[f, trg g ⋆ g, h] ⋅ (a[f, trg g, g] ⋆ h)"
      proof -
        have "((f ⋆ l[g ⋆ h]) ⋅ (f ⋆ a[trg g, g, h])) ⋅ (a[f, trg g ⋆ g, h] ⋅ (a[f, trg g, g] ⋆ h)) =
              ((f ⋆ l[g ⋆ h]) ⋅ a[f, trg g, g ⋆ h]) ⋅ a[f ⋆ trg g, g, h]"
          using assms pentagon comp_assoc by simp
        also have "... = (r[f] ⋆ (g ⋆ h)) ⋅ a[f ⋆ trg g, g, h]"
          using assms triangle [of "g ⋆ h" f] by auto
        also have "... = a[f, g, h] ⋅ ((r[f] ⋆ g) ⋆ h)"
          using assms assoc_naturality [of "r[f]" g h] by simp
        also have "... = (a[f, g, h] ⋅ ((f ⋆ l[g]) ⋆ h)) ⋅ (a[f, trg g, g] ⋆ h)"
          using assms triangle interchange [of "f ⋆ l[g]" "a[f, trg g, g]" h h] comp_assoc
          by auto
        also have "... = (f ⋆ (l[g] ⋆ h)) ⋅ (a[f, trg g ⋆ g, h] ⋅ (a[f, trg g, g] ⋆ h))"
          using assms assoc_naturality [of f "l[g]" h] comp_assoc by simp
        finally show ?thesis by blast
      qed
      moreover have "iso (a[f, trg g ⋆ g, h] ⋅ (a[f, trg g, g] ⋆ h))"
        using assms iso_assoc isos_compose by simp
      ultimately show ?thesis
        using assms iso_is_retraction retraction_is_epi
              epi_cancel
                [of "a[f, trg g ⋆ g, h] ⋅ (a[f, trg g, g] ⋆ h)"
                    "(f ⋆ l[g ⋆ h]) ⋅ (f ⋆ a[trg g, g, h])" "f ⋆ l[g] ⋆ h"]
         by auto
    qed

    lemma lunit_hcomp:
    assumes "ide f" and "ide g" and "src f = trg g"
    shows "l[f ⋆ g] ⋅ a[trg f, f, g] = l[f] ⋆ g"
    and "a^-1[trg f, f, g] ⋅ l^-1[f ⋆ g] = l^-1[f] ⋆ g"
    and "l[f ⋆ g] = (l[f] ⋆ g) ⋅ a^-1[trg f, f, g]"
    and "l^-1[f ⋆ g] = a[trg f, f, g] ⋅ (l^-1[f] ⋆ g)"
    proof -
      show 1: "l[f ⋆ g] ⋅ a[trg f, f, g] = l[f] ⋆ g"
      proof -
        have "L (l[f ⋆ g] ⋅ a[trg f, f, g]) = L (l[f] ⋆ g)"
          using assms interchange [of "trg f" "trg f" "l[f ⋆ g]" "a[trg f, f, g]"] lunit_hcomp_gen
          by fastforce
        thus ?thesis
          using assms L.is_faithful [of "l[f ⋆ g] ⋅ a[trg f, f, g]" "l[f] ⋆ g"] by force
      qed
      show "a^-1[trg f, f, g] ⋅ l^-1[f ⋆ g] = l^-1[f] ⋆ g"
      proof -
        have "a^-1[trg f, f, g] ⋅ l^-1[f ⋆ g] = inv (l[f ⋆ g] ⋅ a[trg f, f, g])"
          using assms by (simp add: inv_comp)
        also have "... = inv (l[f] ⋆ g)"
          using 1 by simp
        also have "... = l^-1[f] ⋆ g"
          using assms by simp
        finally show ?thesis by simp
      qed
      show 2: "l[f ⋆ g] = (l[f] ⋆ g) ⋅ a^-1[trg f, f, g]"
        using assms 1 invert_side_of_triangle(2) by auto
      show "l^-1[f ⋆ g] = a[trg f, f, g] ⋅ (l^-1[f] ⋆ g)"
      proof -
        have "l^-1[f ⋆ g] = inv ((l[f] ⋆ g) ⋅ a^-1[trg f, f, g])"
          using 2 by simp
        also have "... = a[trg f, f, g] ⋅ inv (l[f] ⋆ g)"
          using assms inv_comp by simp
        also have "... = a[trg f, f, g] ⋅ (l^-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 "r[f ⋆ g] ⋆ h = ((f ⋆ r[g]) ⋆ h) ⋅ (a[f, g, src g] ⋆ h)"
    proof -
      have "r[f ⋆ g] ⋆ h = ((f ⋆ g) ⋆ l[h]) ⋅ a[f ⋆ g, src g, h]"
        using assms triangle by simp
      also have "... = (a^-1[f, g, h] ⋅ (f ⋆ g ⋆ l[h]) ⋅ a[f, g, src g ⋆ h]) ⋅ a[f ⋆ g, src g, h]"
        using assms assoc_naturality [of f g "l[h]"] invert_side_of_triangle(1)
        by simp
      also have "... = a^-1[f, g, h] ⋅ (f ⋆ g ⋆ l[h]) ⋅ a[f, g, src g ⋆ h] ⋅ a[f ⋆ g, src g, h]"
        using comp_assoc by simp
      also have "... = (a^-1[f, g, h] ⋅ (f ⋆ (r[g] ⋆ h))) ⋅ (f ⋆ a^-1[g, src g, h]) ⋅
                       a[f, g, src g ⋆ h] ⋅ a[f ⋆ g, src g, h]"
        using assms interchange [of f f] triangle comp_assoc
              invert_side_of_triangle(2) [of "r[g] ⋆ h" "g ⋆ l[h]" "a[g, src g, h]"]
        by simp
      also have "... = ((f ⋆ r[g]) ⋆ h) ⋅ a^-1[f, g ⋆ src g, h] ⋅ (f ⋆ a^-1[g, src g, h]) ⋅
                       a[f, g, src g ⋆ h] ⋅ a[f ⋆ g, src g, h]"
        using assms assoc'_naturality [of f "r[g]" h] comp_assoc by simp
      also have "... = ((f ⋆ r[g]) ⋆ h) ⋅ (a[f, g, src g] ⋆ h)"
        using assms pentagon [of f g "src g" h] iso_assoc inv_hcomp
              invert_side_of_triangle(1)
                [of "a[f, g, src g ⋆ h] ⋅ a[f ⋆ g, src g, h]" "f ⋆ a[g, src g, h]"
                    "a[f, g ⋆ src g, h] ⋅ (a[f, g, src g] ⋆ h)"]
              invert_side_of_triangle(1)
                [of "(f ⋆ a^-1[g, src g, h]) ⋅ a[f, g, src g ⋆ h] ⋅ a[f ⋆ g, src g, h]"
                    "a[f, g ⋆ src g, h]" "a[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 "r[f ⋆ g] = (f ⋆ r[g]) ⋅ a[f, g, src g]"
    and "r^-1[f ⋆ g] = a^-1[f, g, src g] ⋅ (f ⋆ r^-1[g])"
    and "r[f ⋆ g] ⋅ a^-1[f, g, src g] = f ⋆ r[g]"
    and "a[f, g, src g] ⋅ r^-1[f ⋆ g] = f ⋆ r^-1[g]"
    proof -
      show 1: "r[f ⋆ g] = (f ⋆ r[g]) ⋅ a[f, g, src g]"
        using assms interchange [of "f ⋆ r[g]" "a[f, g, src g]" "src g" "src g"]
              runit_hcomp_gen [of f g "src g"]
              R.is_faithful [of "(f ⋆ r[g]) ⋅ (a[f, g, src g])" "r[f ⋆ g]"]
        by simp
      show "r^-1[f ⋆ g] = a^-1[f, g, src g] ⋅ (f ⋆ r^-1[g])"
        using assms 1 inv_comp inv_hcomp by auto
      show 2: "r[f ⋆ g] ⋅ a^-1[f, g, src g] = f ⋆ r[g]"
        using assms 1 comp_arr_dom comp_cod_arr comp_assoc hseqI' comp_assoc_assoc' by auto
      show "a[f, g, src g] ⋅ r^-1[f ⋆ g] = f ⋆ r^-1[g]"
      proof -
        have "a[f, g, src g] ⋅ r^-1[f ⋆ g] = inv (r[f ⋆ g] ⋅ a^-1[f, g, src g])"
          using assms inv_comp by simp
        also have "... = inv (f ⋆ r[g])"
          using 2 by simp
        also have "... = f ⋆ r^-1[g]"
          using assms inv_hcomp [of f "r[g]"] by simp
        finally show ?thesis by simp
      qed
    qed

    lemma unitor_coincidence:
    assumes "obj a"
    shows "l[a] = i[a]" and "r[a] = i[a]"
    proof -
      have "R l[a] = R i[a] ∧ R r[a] = R i[a]"
      proof -
        have "R l[a] = (a ⋆ l[a]) ⋅ a[a, a, a]"
          using assms lunit_hcomp [of a a] lunit_commutes_with_L [of a] by auto
        moreover have "(a ⋆ l[a]) ⋅ a[a, a, a] = R r[a]"
          using assms triangle [of a a] by auto
        moreover have "(a ⋆ l[a]) ⋅ a[a, a, a] = R i[a]"
        proof -
          have "(a ⋆ l[a]) ⋅ a[a, a, a] = ((i[a] ⋆ a) ⋅ a^-1[a, a, a]) ⋅ a[a, a, a]"
            using assms lunit_char(2) by force
          also have "... = R i[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 l[a] i[a] ∧ par r[a] i[a]"
        using assms by auto
      ultimately have 1: "l[a] = i[a] ∧ r[a] = i[a]"
        using R.is_faithful by blast
      show "l[a] = i[a]" using 1 by auto
      show "r[a] = i[a]" using 1 by auto
    qed

    lemma unit_triangle:
    assumes "obj a"
    shows "i[a] ⋆ a = (a ⋆ i[a]) ⋅ a[a, a, a]"
    and "(i[a] ⋆ a) ⋅ a^-1[a, a, a] = a ⋆ i[a]"
    proof -
      show 1: "i[a] ⋆ a = (a ⋆ i[a]) ⋅ a[a, a, a]"
        using assms triangle [of a a] unitor_coincidence by auto
      show "(i[a] ⋆ a) ⋅ a^-1[a, a, a] = a ⋆ i[a]"
        using assms 1 invert_side_of_triangle(2) [of "i[a] ⋆ a" "a ⋆ i[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 = r^-1[cod μ] ⋅ μ ⋅ r[dom μ]"
    and "r[cod μ] ⋅ (μ ⋆ a) ⋅ r^-1[dom μ] = μ"
    proof -
      show "μ ⋆ a = r^-1[cod μ] ⋅ μ ⋅ r[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 "r[cod μ] ⋅ (μ ⋆ a) ⋅ r^-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 ⋆ μ = l^-1[cod μ] ⋅ μ ⋅ l[dom μ]"
    and "l[cod μ] ⋅ (b ⋆ μ) ⋅ l^-1[dom μ] = μ"
    proof -
      show "b ⋆ μ = l^-1[cod μ] ⋅ μ ⋅ l[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 "l[cod μ] ⋅ (b ⋆ μ) ⋅ l^-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 "(τ ⋆ μ) ⋆ ν = a^-1[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν) ⋅ a[dom τ, dom μ, dom ν]"
    and "τ ⋆ μ ⋆ ν = a[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) ⋅ a^-1[dom τ, dom μ, dom ν]"
    proof -
      show "(τ ⋆ μ) ⋆ ν = a^-1[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν) ⋅ a[dom τ, dom μ, dom ν]"
      proof -
        have "(τ ⋆ μ) ⋆ ν = (a^-1[cod τ, cod μ, cod ν] ⋅ a[cod τ, cod μ, cod ν]) ⋅ ((τ ⋆ μ) ⋆ ν)"
          using assms comp_assoc_assoc'(2) comp_cod_arr by simp
        also have "... = a^-1[cod τ, cod μ, cod ν] ⋅ a[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν)"
          using comp_assoc by simp
        also have "... = a^-1[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν) ⋅ a[dom τ, dom μ, dom ν]"
          using assms assoc_naturality by simp
        finally show ?thesis by simp
      qed
      show "τ ⋆ μ ⋆ ν = a[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) ⋅ a^-1[dom τ, dom μ, dom ν]"
      proof -
        have "τ ⋆ μ ⋆ ν = (τ ⋆ μ ⋆ ν) ⋅ a[dom τ, dom μ, dom ν] ⋅ a^-1[dom τ, dom μ, dom ν]"
          using assms comp_assoc_assoc'(1) comp_arr_dom by simp
        also have "... = ((τ ⋆ μ ⋆ ν) ⋅ a[dom τ, dom μ, dom ν]) ⋅ a^-1[dom τ, dom μ, dom ν]"
          using comp_assoc by simp
        also have "... = (a[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν)) ⋅ a^-1[dom τ, dom μ, dom ν]"
          using assms assoc_naturality by simp
        also have "... = a[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) ⋅ a^-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 ⋆ l[g]) = (r[f] ⋆ g) ⋅ a^-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 "((a^-1[f, g, h] ⋆ k) ⋅ a^-1[f, g ⋆ h, k]) ⋅ (f ⋆ a^-1[g, h, k])
              = a^-1[f ⋆ g, h, k] ⋅ a^-1[f, g, h ⋆ k]"
    proof -
      have "((a^-1[f, g, h] ⋆ k) ⋅ a^-1[f, g ⋆ h, k]) ⋅ (f ⋆ a^-1[g, h, k])
              = inv ((f ⋆ a[g, h, k]) ⋅ (a[f, g ⋆ h, k] ⋅ (a[f, g, h] ⋆ k)))"
      proof -
        have "inv ((f ⋆ a[g, h, k]) ⋅ (a[f, g ⋆ h, k] ⋅ (a[f, g, h] ⋆ k))) =
              inv (a[f, g ⋆ h, k] ⋅ (a[f, g, h] ⋆ k)) ⋅ inv (f ⋆ a[g, h, k])"
          using assms inv_comp [of "a[f, g ⋆ h, k] ⋅ (a[f, g, h] ⋆ k)" "f ⋆ a[g, h, k]"]
          by force
        also have "... = (inv (a[f, g, h] ⋆ k) ⋅ inv a[f, g ⋆ h, k]) ⋅ inv (f ⋆ a[g, h, k])"
          using assms iso_assoc inv_comp by simp
        also have "... = ((a^-1[f, g, h] ⋆ k) ⋅ a^-1[f, g ⋆ h, k]) ⋅ (f ⋆ a^-1[g, h, k])"
          using assms inv_hcomp by simp
        finally show ?thesis by simp
      qed
      also have "... = inv (a[f, g, h ⋆ k] ⋅ a[f ⋆ g, h, k])"
        using assms pentagon by simp
      also have "... = a^-1[f ⋆ g, h, k] ⋅ a^-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
          ‹λμντ. a (fst μντ) (fst (snd μντ)) (snd (snd μντ))› +
    α': inverse_transformation VVV.comp V HoHV HoVH
          ‹λμντ. a (fst μντ) (fst (snd μντ)) (snd (snd μντ))› +
    l: natural_isomorphism V V L map l +
    l': inverse_transformation V V L map l +
    r: natural_isomorphism V V R map r +
    r': inverse_transformation V V R map r

  sublocale bicategory ⊆ extended_bicategory V H a i 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
                    ‹λμντ. a (fst μντ) (fst (snd μντ)) (snd (snd μντ))› ..
    interpret l: natural_isomorphism V V L map l using natural_isomorphism_l by auto
    interpret l': inverse_transformation V V L map l ..
    interpret r: natural_isomorphism V V R map r using natural_isomorphism_r by auto
    interpret r': inverse_transformation V V R map r ..
    interpret extended_bicategory V H a i src trg ..
    show "extended_bicategory V H a i src trg" ..
  qed

end