Session Bicategory

Theory IsomorphismClass

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

section "Isomorphism Classes"

text ‹
  The following is a small theory that facilitates working with isomorphism classes of objects
  in a category.
›

theory IsomorphismClass
imports Category3.EpiMonoIso Category3.NaturalTransformation
begin

  context category
  begin

    notation isomorphic (infix "≅" 50)

    definition iso_class ("⟦_⟧")
    where "iso_class f ≡ {f'. f ≅ f'}"

    definition is_iso_class
    where "is_iso_class F ≡ ∃f. f ∈ F ∧ F = iso_class f"

    definition iso_class_rep
    where "iso_class_rep F ≡ SOME f. f ∈ F"

    lemmas isomorphic_transitive [trans]
    lemmas naturally_isomorphic_transitive [trans]

    lemma inv_in_homI [intro]:
    assumes "iso f" and "«f : a → b»"
    shows "«inv f : b → a»"
      using assms inv_is_inverse seqE inverse_arrowsE
      by (metis ide_compE in_homE in_homI)

    lemma iso_class_is_nonempty:
    assumes "is_iso_class F"
    shows "F ≠ {}"
      using assms is_iso_class_def iso_class_def by auto

    lemma iso_class_memb_is_ide:
    assumes "is_iso_class F" and "f ∈ F"
    shows "ide f"
      using assms is_iso_class_def iso_class_def isomorphic_def by auto

    lemma ide_in_iso_class:
    assumes "ide f"
    shows "f ∈ ⟦f⟧"
      using assms iso_class_def is_iso_class_def isomorphic_reflexive by simp

    lemma rep_in_iso_class:
    assumes "is_iso_class F"
    shows "iso_class_rep F ∈ F"
      using assms is_iso_class_def iso_class_rep_def someI_ex [of "λf. f ∈ F"]
            ide_in_iso_class
      by metis

    lemma is_iso_classI:
    assumes "ide f"
    shows "is_iso_class ⟦f⟧"
      using assms iso_class_def is_iso_class_def isomorphic_reflexive by blast

    lemma rep_iso_class:
    assumes "ide f"
    shows "iso_class_rep ⟦f⟧ ≅ f"
      using assms is_iso_classI rep_in_iso_class iso_class_def isomorphic_symmetric
      by blast

    lemma iso_class_elems_isomorphic:
    assumes "is_iso_class F" and "f ∈ F" and "f' ∈ F"
    shows "f ≅ f'"
      using assms iso_class_def
      by (metis is_iso_class_def isomorphic_symmetric isomorphic_transitive mem_Collect_eq)

    lemma iso_class_eqI [intro]:
    assumes "f ≅ g"
    shows "⟦f⟧ = ⟦g⟧"
    proof -
      have f: "ide f"
        using assms isomorphic_def by auto
      have g: "ide g"
        using assms isomorphic_def by auto
      have "f ∈ ⟦g⟧"
        using assms iso_class_def isomorphic_symmetric by simp
      moreover have "g ∈ ⟦g⟧"
        using assms g iso_class_def isomorphic_reflexive isomorphic_def by simp
      ultimately have "⋀h. (h ∈ ⟦f⟧) = (h ∈ ⟦g⟧)"
        using assms g iso_class_def [of f] iso_class_def [of g]
              isomorphic_reflexive isomorphic_symmetric isomorphic_transitive
        by blast
      thus ?thesis by auto
    qed

    lemma iso_class_eq:
    assumes "is_iso_class F" and "is_iso_class G" and "F ∩ G ≠ {}"
    shows "F = G"
    proof -
      obtain h where h: "h ∈ F ∧ h ∈ G"
        using assms by auto
      show ?thesis
        using assms h
        by (metis is_iso_class_def iso_class_elems_isomorphic iso_class_eqI)
    qed

    lemma iso_class_rep [simp]:
    assumes "is_iso_class F"
    shows "⟦iso_class_rep F⟧ = F"
    proof (intro iso_class_eq)
      show "is_iso_class ⟦iso_class_rep F⟧"
        using assms is_iso_classI iso_class_memb_is_ide rep_in_iso_class by blast
      show "is_iso_class F"
        using assms by simp
      show "⟦iso_class_rep F⟧ ∩ F ≠ {}"
        using assms rep_in_iso_class
        by (meson disjoint_iff_not_equal ide_in_iso_class iso_class_memb_is_ide)
    qed

  end

end

Theory Prebicategory

theory Prebicategory
imports EquivalenceOfCategories Subcategory IsomorphismClass
(*  Title:       PreBicategory
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2019
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

  text ‹
    The objective of this section is to construct a formalization of bicategories that is
    compatible with our previous formulation of categories \cite{Category3-AFP}
    and that permits us to carry over unchanged as much of the work done on categories as possible.
    For these reasons, we conceive of a bicategory in what might be regarded as a somewhat
    unusual fashion.  Rather than a traditional development, which would typically define
    a bicategory to be essentially ``a `category' whose homs themselves have the structure
    of categories,'' here we regard a bicategory as ``a (vertical) category that has been
    equipped with a suitable (horizontal) weak composition.''  Stated another way, we think
    of a bicategory as a generalization of a monoidal category in which the tensor product is
    a partial operation, rather than a total one.  Our definition of bicategory can thus
    be summarized as follows: a bicategory is a (vertical) category that has been equipped
    with idempotent endofunctors ‹src› and ‹trg› that assign to each arrow its ``source''
    and ``target'' subject to certain commutativity constraints,
    a partial binary operation ‹⋆› of horizontal composition that is suitably functorial on
    the ``hom-categories'' determined by the assignment of sources and targets,
    ``associativity'' isomorphisms ‹«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ (g ⋆ h)»› for each horizontally
    composable triple of vertical identities ‹f›, ‹g›, ‹h›, subject to the usual naturality
    and coherence conditions, and for each ``object'' ‹a› (defined to be an arrow that is
    its own source and target) a ``unit isomorphism'' ‹«𝗂[a] : a ⋆ a ⇒ a»›.
    As is the case for monoidal categories, the unit isomorphisms and associator isomorphisms
    together enable a canonical definition of left and right ``unit'' isomorphisms
    ‹«𝗅[f] : a ⋆ f ⇒ f»› and ‹«𝗋[f] : f ⋆ a ⇒ f»› when ‹f› is a vertical identity
    horizontally composable on the left or right by ‹a›, and it can be shown that these are
    the components of natural transformations.

    The definition of bicategory just sketched shares with a more traditional version the
    requirement that assignments of source and target are given as basic data, and these
    assignments determine horizontal composability in the sense that arrows ‹μ› and ‹ν›
    are composable if the chosen source of ‹μ› coincides with the chosen target of ‹ν›.
    Thus it appears, at least on its face, that composability of arrows depends on an assignment
    of sources and targets.  We are interested in establishing whether this is essential or
    whether bicategories can be formalized in a completely ``object-free'' fashion.

    It turns out that we can obtain such an object-free formalization through a rather direct
    generalization of the approach we used in the formalization of categories.
    Specifically, we define a \emph{weak composition} to be a partial binary operation ‹⋆›
    on the arrow type of a ``vertical'' category ‹V›, such that the domain of definition of this
    operation is itself a category (of ``horizontally composable pairs of arrows''),
    the operation is functorial, and it is subject to certain matching conditions which include
    those satisfied by a category.
    From the axioms for a weak composition we can prove the existence of ``hom-categories'',
    which are subcategories of ‹V› consisting of arrows horizontally composable on the
    left or right by a specified vertical identity.
    A \emph{weak unit} is defined to be a vertical identity ‹a› such that ‹a ⋆ a ≅ a›
    and is such that the mappings ‹a ⋆ ‐› and ‹‐ ⋆ a› are fully faithful endofunctors
    of the subcategories of ‹V› consisting of the arrows for which they are defined.
    We define the \emph{sources} of an arrow ‹μ› to be the weak units that are horizontally
    composable with ‹μ› on the right, and the \emph{targets} of ‹μ› to be the weak units
    that are horizontally composable with ‹μ› on the left.
    An \emph{associative weak composition} is defined to be a weak composition that is equipped
    with ``associator'' isomorphisms ‹«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ (g ⋆ h)»› for horizontally
    composable vertical identities ‹f›, ‹g›, ‹h›, subject to the usual naturality and coherence
    conditions.
    A \emph{prebicategory} is defined to be an associative weak composition for which every
    arrow has a source and a target.  We show that the sets of sources and targets of each
    arrow in a prebicategory is an isomorphism class of weak units, and that horizontal
    composability of arrows ‹μ› and ‹ν› is characterized by the set of sources of ‹μ› being
    equal to the set of targets of ‹ν›.

    We show that prebicategories are essentially ``bicategories without objects''.
    Given a prebicategory, we may choose an arbitrary representative of each
    isomorphism class of weak units and declare these to be ``objects''
    (this is analogous to choosing a particular unit object in a monoidal category).
    For each object we may choose a particular \emph{unit isomorphism} ‹«𝗂[a] : a ⋆ a ⇒ a»›.
    This choice, together with the associator isomorphisms, enables a canonical definition
    of left and right unit isomorphisms ‹«𝗅[f] : a ⋆ f ⇒ f»› and ‹«𝗋[f] : f ⋆ a ⇒ f»›
    when ‹f› is a vertical identity horizontally composable on the left or right by ‹a›,
    and it can be shown that these are the components of natural isomorphisms.
    We may then define ``the source'' of an arrow to be the chosen representative of the
    set of its sources and ``the target'' to be the chosen representative of the set of its
    targets.  We show that the resulting structure is a bicategory, in which horizontal
    composability as given by the weak composition coincides with the ``syntactic'' version
    determined by the chosen sources and targets.
    Conversely, a bicategory determines a prebicategory, essentially by forgetting
    the sources, targets and unit isomorphisms.
    These results make it clear that the assignment of sources and targets to arrows in
    a bicategory is basically a convenience and that horizontal composability of arrows
    is not dependent on a particular choice.
›

theory Prebicategory
imports Category3.EquivalenceOfCategories Category3.Subcategory IsomorphismClass
begin

  section "Weak Composition"

  text ‹
    In this section we define a locale ‹weak_composition›, which formalizes a functorial
    operation of ``horizontal'' composition defined on an underlying ``vertical'' category.
    The definition is expressed without the presumption of the existence of any sort
    of ``objects'' that determine horizontal composability.  Rather, just as we did
    in showing that the @{locale partial_magma} locale supported the definition of ``identity
    arrow'' as a kind of unit for vertical composition which ultimately served as a basis
    for the definition of ``domain'' and ``codomain'' of an arrow, here we show that the
    ‹weak_composition› locale supports a definition of \emph{weak unit} for horizontal
    composition which can ultimately be used to define the \emph{sources} and \emph{targets}
    of an arrow with respect to horizontal composition.
    In particular, the definition of weak composition involves axioms that relate horizontal
    and vertical composability.  As a consequence of these axioms, for any fixed arrow ‹μ›,
    the sets of arrows horizontally composable on the left and on the right with ‹μ›
    form subcategories with respect to vertical composition.  We define the
    sources of ‹μ› to be the weak units that are composable with ‹μ› on the right,
    and the targets of ‹μ› to be the weak units that are composable with ‹μ›
    on the left.  Weak units are then characterized as arrows that are members
    of the set of their own sources (or, equivalently, of their own targets).
  ›

  subsection "Definition"

  locale weak_composition =
    category V +
    VxV: product_category V V +
    VoV: subcategory VxV.comp ‹λμν. fst μν ⋆ snd μν ≠ null› +
    "functor" VoV.comp V ‹λμν. fst μν ⋆ snd μν›
  for V :: "'a comp"         (infixr "⋅" 55)
  and H :: "'a comp"         (infixr "⋆" 53) +
  assumes left_connected: "seq ν ν' ⟹ ν ⋆ μ ≠ null ⟷ ν' ⋆ μ ≠ null"
  and right_connected: "seq μ μ' ⟹ ν ⋆ μ ≠ null ⟷ ν ⋆ μ' ≠ null"
  and match_1: "⟦ ν ⋆ μ ≠ null; (ν ⋆ μ) ⋆ τ ≠ null ⟧ ⟹ μ ⋆ τ ≠ null"
  and match_2: "⟦ ν ⋆ (μ ⋆ τ) ≠ null; μ ⋆ τ ≠ null ⟧ ⟹ ν ⋆ μ ≠ null"
  and match_3: "⟦ μ ⋆ τ ≠ null; ν ⋆ μ ≠ null ⟧ ⟹ (ν ⋆ μ) ⋆ τ ≠ null"
  and match_4: "⟦ μ ⋆ τ ≠ null; ν ⋆ μ ≠ null ⟧ ⟹ ν ⋆ (μ ⋆ τ) ≠ null"
  begin

    text ‹
      We think of the arrows of the vertical category as ``2-cells'' and the vertical identities
      as ``1-cells''.  In the formal development, the predicate @{term arr} (``arrow'')
      will have its normal meaning with respect to the vertical composition, hence @{term "arr μ"}
      will mean, essentially, ``‹μ› is a 2-cell''.  This is somewhat unfortunate, as it is
      traditional when discussing bicategories to use the term ``arrow'' to refer to the 1-cells.
      However, we are trying to carry over all the formalism that we have already developed for
      categories and apply it to bicategories with as little change and redundancy as possible.
      It becomes too confusing to try to repurpose the name @{term arr} to mean @{term ide} and
      to introduce a replacement for the name @{term arr}, so we will simply tolerate the
      situation.  In informal text, we will prefer the terms ``2-cell'' and ``1-cell'' over
      (vertical) ``arrow'' and ``identity'' when there is a chance for confusion.

      We do, however, make the following adjustments in notation for @{term in_hom} so that
      it is distinguished from the notion @{term in_hhom} (``in horizontal hom'') to be
      introduced subsequently.
    ›

    no_notation in_hom      ("«_ : _ → _»")
    notation in_hom         ("«_ : _ ⇒ _»")

    lemma is_partial_magma:
    shows "partial_magma H"
    proof
      show "∃!n. ∀f. n ⋆ f = n ∧ f ⋆ n = n"
      proof
        show 1: "∀f. null ⋆ f = null ∧ f ⋆ null = null"
          using is_extensional VoV.inclusion VoV.arr_char by force
        show "⋀n. ∀f. n ⋆ f = n ∧ f ⋆ n = n ⟹ n = null"
          using 1 VoV.arr_char is_extensional not_arr_null by metis
      qed
    qed

    interpretation H: partial_magma H
      using is_partial_magma by auto

    text ‹
      Either ‹match_1› or ‹match_2› seems essential for the next result, which states
      that the nulls for the horizontal and vertical compositions coincide.
    ›

    lemma null_agreement [simp]:
    shows "H.null = null"
      by (metis VoV.inclusion VxV.not_arr_null match_1 H.comp_null(1))

    lemma composable_implies_arr:
    assumes "ν ⋆ μ ≠ null"
    shows "arr μ" and "arr ν"
      using assms is_extensional VoV.arr_char VoV.inclusion by auto

    lemma hcomp_null [simp]:
    shows "null ⋆ μ = null" and "μ ⋆ null = null"
      using H.comp_null by auto

    lemma hcomp_simpsWC [simp]:
    assumes "ν ⋆ μ ≠ null"
    shows "arr (ν ⋆ μ)" and "dom (ν ⋆ μ) = dom ν ⋆ dom μ" and "cod (ν ⋆ μ) = cod ν ⋆ cod μ"
      using assms preserves_arr preserves_dom preserves_cod VoV.arr_char VoV.inclusion
      by force+

    lemma ide_hcompWC [simp]:
    assumes "ide f" and "ide g" and "g ⋆ f ≠ null"
    shows "ide (g ⋆ f)"
      using assms preserves_ide VoV.ide_char by force

    lemma hcomp_in_homWC [intro]:
    assumes "ν ⋆ μ ≠ null"
    shows "«ν ⋆ μ : dom ν ⋆ dom μ ⇒ cod ν ⋆ cod μ»"
      using assms by auto

    text ‹
      Horizontal composability of arrows is determined by horizontal composability of
      their domains and codomains (defined with respect to vertical composition).
    ›

    lemma hom_connected:
    shows "ν ⋆ μ ≠ null ⟷ dom ν ⋆ μ ≠ null"
    and "ν ⋆ μ ≠ null ⟷ ν ⋆ dom μ ≠ null"
    and "ν ⋆ μ ≠ null ⟷ cod ν ⋆ μ ≠ null"
    and "ν ⋆ μ ≠ null ⟷ ν ⋆ cod μ ≠ null"
    proof -
      show "ν ⋆ μ ≠ null ⟷ dom ν ⋆ μ ≠ null"
        using left_connected [of ν "dom ν" μ] composable_implies_arr arr_dom_iff_arr by force
      show "ν ⋆ μ ≠ null ⟷ cod ν ⋆ μ ≠ null"
        using left_connected [of  "cod ν" ν μ] composable_implies_arr arr_cod_iff_arr by force
      show "ν ⋆ μ ≠ null ⟷ ν ⋆ dom μ ≠ null"
        using right_connected [of μ "dom μ" ν] composable_implies_arr arr_dom_iff_arr by force
      show "ν ⋆ μ ≠ null ⟷ ν ⋆ cod μ ≠ null"
        using right_connected [of "cod μ" μ ν] composable_implies_arr arr_cod_iff_arr by force
    qed

    lemma isomorphic_implies_equicomposable:
    assumes "f ≅ g"
    shows "τ ⋆ f ≠ null ⟷ τ ⋆ g ≠ null"
    and "f ⋆ σ ≠ null ⟷ g ⋆ σ ≠ null"
      using assms isomorphic_def hom_connected by auto

    lemma interchange:
    assumes "seq ν μ" and "seq τ σ"
    shows "(ν ⋅ μ) ⋆ (τ ⋅ σ) = (ν ⋆ τ) ⋅ (μ ⋆ σ)"
    proof -
      have "μ ⋆ σ = null ⟹ ?thesis"
        by (metis assms comp_null(2) dom_comp hom_connected(1-2))
      moreover have "μ ⋆ σ ≠ null ⟹ ?thesis"
      proof -
        assume μσ: "μ ⋆ σ ≠ null"
        have 1: "VoV.arr (μ, σ)"
          using μσ VoV.arr_char by auto
        have ντ: "(ν, τ) ∈ VoV.hom (VoV.cod (μ, σ)) (VoV.cod (ν, τ))"
        proof -
          have "VoV.arr (ν, τ)"
            using assms 1 hom_connected VoV.arr_char
            by (elim seqE, auto, metis)
          thus ?thesis
            using assms μσ VoV.dom_char VoV.cod_char by fastforce
        qed
        show ?thesis
        proof -
          have "VoV.seq (ν, τ) (μ, σ)"
            using assms 1 μσ ντ VoV.seqI by blast
          thus ?thesis
            using assms 1 μσ ντ VoV.comp_char preserves_comp [of "(ν, τ)" "(μ, σ)"] VoV.seqI
            by fastforce
        qed
      qed
      ultimately show ?thesis by blast
    qed

    lemma paste_1:
    shows "ν ⋆ μ = (cod ν ⋆ μ) ⋅ (ν ⋆ dom μ)"
      using interchange composable_implies_arr comp_arr_dom comp_cod_arr
            hom_connected(2-3)
      by (metis comp_null(2))

    lemma paste_2:
    shows "ν ⋆ μ = (ν ⋆ cod μ) ⋅ (dom ν ⋆ μ)"
      using interchange composable_implies_arr comp_arr_dom comp_cod_arr
            hom_connected(1,4)
      by (metis comp_null(2))

    lemma whisker_left:
    assumes "seq ν μ" and "ide f"
    shows "f ⋆ (ν ⋅ μ) = (f ⋆ ν) ⋅ (f ⋆ μ)"
      using assms interchange [of f f ν μ] hom_connected by auto

    lemma whisker_right:
    assumes "seq ν μ" and "ide f"
    shows "(ν ⋅ μ) ⋆ f = (ν ⋆ f) ⋅ (μ ⋆ f)"
      using assms interchange [of ν μ f f] hom_connected by auto

    subsection "Hom-Subcategories"

    definition left
    where "left τ ≡ λμ. τ ⋆ μ ≠ null"

    definition right
    where "right σ ≡ λμ. μ ⋆ σ ≠ null"

    lemma right_iff_left:
    shows "right σ τ ⟷ left τ σ"
      using right_def left_def by simp

    lemma left_respects_isomorphic:
    assumes "f ≅ g"
    shows "left f = left g"
      using assms isomorphic_implies_equicomposable left_def by auto

    lemma right_respects_isomorphic:
    assumes "f ≅ g"
    shows "right f = right g"
      using assms isomorphic_implies_equicomposable right_def by auto

    lemma left_iff_left_inv:
    assumes "iso μ"
    shows "left τ μ ⟷ left τ (inv μ)"
      using assms left_def inv_in_hom hom_connected(2) hom_connected(4) [of τ "inv μ"]
      by auto
        
    lemma right_iff_right_inv:
    assumes "iso μ"
    shows "right σ μ ⟷ right σ (inv μ)"
      using assms right_def inv_in_hom hom_connected(1) hom_connected(3) [of "inv μ" σ]
      by auto

    lemma left_hom_is_subcategory:
    assumes "arr μ"
    shows "subcategory V (left μ)"
    proof (unfold left_def, unfold_locales)
      show "⋀f. μ ⋆ f ≠ null ⟹ arr f" using composable_implies_arr by simp
      show "⋀f. μ ⋆ f ≠ null ⟹ μ ⋆ dom f ≠ null" using hom_connected(2) by simp
      show "⋀f. μ ⋆ f ≠ null ⟹ μ ⋆ cod f ≠ null" using hom_connected(4) by auto
      show "⋀f g. ⟦ μ ⋆ f ≠ null; μ ⋆ g ≠ null; cod f = dom g ⟧ ⟹ μ ⋆ (g ⋅ f) ≠ null"
      proof -
        fix f g
        assume f: "μ ⋆ f ≠ null" and g: "μ ⋆ g ≠ null" and fg: "cod f = dom g"
        show "μ ⋆ (g ⋅ f) ≠ null"
          using f g fg composable_implies_arr hom_connected(2) [of μ "g ⋅ f"] hom_connected(2)
          by simp
      qed
    qed

    lemma right_hom_is_subcategory:
    assumes "arr μ"
    shows "subcategory V (right μ)"
    proof (unfold right_def, unfold_locales)
      show "⋀f. f ⋆ μ ≠ null ⟹ arr f" using composable_implies_arr by simp
      show "⋀f. f ⋆ μ ≠ null ⟹ dom f ⋆ μ ≠ null" using hom_connected(1) by auto
      show "⋀f. f ⋆ μ ≠ null ⟹ cod f ⋆ μ ≠ null" using hom_connected(3) by auto
      show "⋀f g. ⟦ f ⋆ μ ≠ null; g ⋆ μ ≠ null; cod f = dom g ⟧ ⟹ (g ⋅ f) ⋆ μ ≠ null"
      proof -
        fix f g
        assume f: "f ⋆ μ ≠ null" and g: "g ⋆ μ ≠ null" and fg: "cod f = dom g"
        show "(g ⋅ f) ⋆ μ ≠ null"
          using f g fg composable_implies_arr hom_connected(1) [of "g ⋅ f" μ] hom_connected(1)
          by simp
      qed
    qed

    abbreviation Left
    where "Left a ≡ subcategory.comp V (left a)"

    abbreviation Right
    where "Right a ≡ subcategory.comp V (right a)"

    text ‹
      We define operations of composition on the left or right with a fixed 1-cell,
      and show that such operations are functorial in case that 1-cell is
      horizontally self-composable.
    ›

    definition HL
    where "HL g ≡ λμ. g ⋆ μ"

    definition HR
    where "HR f ≡ λμ. μ ⋆ f"

    (* TODO: Why do the following fail when I use @{thm ...} *)
    text ‹
      Note that ‹match_3› and ‹match_4› are required for the next results.
    ›

    lemma endofunctor_HL:
    assumes "ide g" and "g ⋆ g ≠ null"
    shows "endofunctor (Left g) (HL g)"
    proof -
      interpret L: subcategory V ‹left g› using assms left_hom_is_subcategory by simp
      have *: "⋀μ. L.arr μ ⟹ HL g μ = g ⋆ μ"
        using assms HL_def by simp
      have preserves_arr: "⋀μ. L.arr μ ⟹ L.arr (HL g μ)"
        using assms * L.arr_char left_def match_4 by force
      show "endofunctor L.comp (HL g)"
      proof
        show "⋀μ. ¬ L.arr μ ⟹ HL g μ = L.null"
          using assms L.arr_char L.null_char left_def HL_def by fastforce
        show "⋀μ. L.arr μ ⟹ L.arr (HL g μ)" by fact
        fix μ
        assume "L.arr μ"
        hence μ: "L.arr μ ∧ arr μ ∧ g ⋆ μ ≠ null"
          using assms L.arr_char composable_implies_arr left_def by metis
        show "L.dom (HL g μ) = HL g (L.dom μ)"
          using assms μ * L.arr_char L.dom_char preserves_arr hom_connected(2) left_def
          by simp
        show "L.cod (HL g μ) = HL g (L.cod μ)"
          using assms μ * L.arr_char L.cod_char preserves_arr hom_connected(4) left_def
          by simp
        next
        fix μ ν
        assume μν: "L.seq ν μ"
        have μ: "L.arr μ"
          using μν by (elim L.seqE, auto)
        have ν: "L.arr ν ∧ arr ν ∧ in_hom ν (L.cod μ) (L.cod ν) ∧ left g ν ∧ g ⋆ ν ≠ null"
        proof -
          have 1: "L.in_hom ν (L.cod μ) (L.cod ν)"
            using μν by (elim L.seqE, auto)
          hence "arr ν ∧ left g ν"
            using L.hom_char by blast
          thus ?thesis
            using assms 1 left_def by fastforce
        qed
        show "HL g (L.comp ν μ) = L.comp (HL g ν) (HL g μ)"
        proof -
          have "HL g (L.comp ν μ) = g ⋆ (ν ⋅ μ)"
            using μ ν HL_def L.comp_def L.arr_char by fastforce
          also have "... = (g ⋆ ν) ⋅ (g ⋆ μ)"
            using assms μ ν L.inclusion whisker_left L.arr_char by fastforce
          also have "... = L.comp (HL g ν) (HL g μ)"
            using assms μν μ ν * preserves_arr L.arr_char L.dom_char L.cod_char L.comp_char
                  L.inclusion HL_def left_def
            by auto
          finally show ?thesis by blast
        qed
      qed
    qed

    lemma endofunctor_HR:
    assumes "ide f" and "f ⋆ f ≠ null"
    shows "endofunctor (Right f) (HR f)"
    proof -
      interpret R: subcategory V ‹right f› using assms right_hom_is_subcategory by simp
      have *: "⋀μ. R.arr μ ⟹ HR f μ = μ ⋆ f"
        using assms HR_def by simp
      have preserves_arr: "⋀μ. R.arr μ ⟹ R.arr (HR f μ)"
        using assms * R.arr_char right_def match_3 by force
      show "endofunctor R.comp (HR f)"
      proof
        show "⋀μ. ¬ R.arr μ ⟹ HR f μ = R.null"
          using assms R.arr_char R.null_char right_def HR_def by fastforce
        show "⋀μ. R.arr μ ⟹ R.arr (HR f μ)" by fact
        fix μ
        assume "R.arr μ"
        hence μ: "R.arr μ ∧ arr μ ∧ μ ⋆ f ≠ null"
          using assms R.arr_char composable_implies_arr right_def by simp
        show "R.dom (HR f μ) = HR f (R.dom μ)"
          using assms μ * R.arr_char R.dom_char preserves_arr hom_connected(1) right_def
          by simp
        show "R.cod (HR f μ) = HR f (R.cod μ)"
          using assms μ * R.arr_char R.cod_char preserves_arr hom_connected(3) right_def
          by simp
        next
        fix μ ν
        assume μν: "R.seq ν μ"
        have μ: "R.arr μ"
          using μν by (elim R.seqE, auto)
        have ν: "R.arr ν ∧ arr ν ∧ in_hom ν (R.cod μ) (R.cod ν) ∧ right f ν ∧ ν ⋆ f ≠ null"
        proof -
          have 1: "R.in_hom ν (R.cod μ) (R.cod ν)"
            using μν by (elim R.seqE, auto)
          hence "arr ν ∧ right f ν"
            using R.hom_char by blast
          thus ?thesis
            using assms 1 right_def by fastforce
        qed
        show "HR f (R.comp ν μ) = R.comp (HR f ν) (HR f μ)"
        proof -
          have "HR f (R.comp ν μ) = (ν ⋅ μ) ⋆ f"
            using μ ν HR_def R.comp_def R.arr_char by fastforce
          also have "... = (ν ⋆ f) ⋅ (μ ⋆ f)"
            using assms μ ν R.inclusion whisker_right R.arr_char by fastforce
          also have "... = R.comp (HR f ν) (HR f μ)"
            using assms μν μ ν * preserves_arr R.arr_char R.dom_char R.cod_char R.comp_char
                  R.inclusion HR_def right_def
            by auto
          finally show ?thesis by blast
        qed
      qed
    qed

  end

  locale left_hom =
    weak_composition V H +
    S: subcategory V ‹left ω›
  for V :: "'a comp"                  (infixr "⋅" 55)
  and H :: "'a comp"                  (infixr "⋆" 53)
  and ω :: 'a +
  assumes arr_ω: "arr ω"
  begin

    no_notation in_hom      ("«_ : _ → _»")
    notation in_hom         ("«_ : _ ⇒ _»")
    notation S.comp         (infixr "⋅S" 55)
    notation S.in_hom       ("«_ : _ ⇒S _»")

    lemma right_hcomp_closed [simp]:
    assumes "«μ : x ⇒S y»" and "«ν : c ⇒ d»" and "μ ⋆ ν ≠ null"
    shows "«μ ⋆ ν : x ⋆ c ⇒S y ⋆ d»"
    proof
      show 1: "S.arr (μ ⋆ ν)"
        using assms arr_ω S.arr_char left_def match_4
        by (elim S.in_homE, meson)
      show "S.dom (μ ⋆ ν) = x ⋆ c"
        using assms 1 by force
      show "S.cod (μ ⋆ ν) = y ⋆ d"
        using assms 1 by force
    qed

    lemma interchange:
    assumes "S.seq ν μ" and "S.seq τ σ" and "μ ⋆ σ ≠ null"
    shows "(ν ⋅S μ) ⋆ (τ ⋅S σ) = (ν ⋆ τ) ⋅S (μ ⋆ σ)"
    proof -
      have 1: "ν ⋆ τ ≠ null"
        using assms hom_connected(1) [of ν σ] hom_connected(2) [of ν τ] hom_connected(3-4)
        by force
      have "(ν ⋅S μ) ⋆ (τ ⋅S σ) = (ν ⋅ μ) ⋆ (τ ⋅ σ)"
        using assms S.comp_char S.seq_char by metis
      also have "... = (ν ⋆ τ) ⋅ (μ ⋆ σ)"
        using assms interchange S.seq_char S.arr_char by simp
      also have "... = (ν ⋆ τ) ⋅S (μ ⋆ σ)"
      proof -
        have "S.arr (ν ⋆ τ)"
        proof -
          have "«τ : dom τ ⇒ cod τ»"
            using assms S.in_hom_char by blast
          thus ?thesis
            using assms 1 right_hcomp_closed by blast
        qed
        moreover have "S.arr (μ ⋆ σ)"
        proof -
          have "«σ : dom σ ⇒ cod σ»"
            using assms S.in_hom_char by blast
          thus ?thesis
            using assms right_hcomp_closed [of μ "dom μ" "cod μ" σ "dom σ" "cod σ"] by fastforce
        qed
        moreover have "seq (ν ⋆ τ) (μ ⋆ σ)"
          using assms 1 S.in_hom_char
          by (metis (full_types) S.seq_char hcomp_simpsWC(1-3) seqE seqI)
        ultimately show ?thesis
          using S.comp_char by auto
      qed
      finally show ?thesis by blast
    qed

    lemma inv_char:
    assumes "S.arr φ" and "iso φ"
    shows "S.inverse_arrows φ (inv φ)"
    and "S.inv φ = inv φ"
    proof -
      have 1: "S.arr (inv φ)"
      proof -
        have "S.arr φ" using assms by auto
        hence "ω ⋆ φ ≠ null"
          using S.arr_char left_def by simp
        hence "ω ⋆ cod φ ≠ null"
          using hom_connected(4) by blast
        hence "ω ⋆ dom (inv φ) ≠ null"
          using assms S.iso_char by simp
        hence "ω ⋆ inv φ ≠ null"
          using hom_connected by blast
        thus "S.arr (inv φ)"
          using S.arr_char left_def by force
      qed
      show "S.inv φ = inv φ"
        using assms 1 S.inv_char S.iso_char by blast
      thus "S.inverse_arrows φ (inv φ)"
        using assms 1 S.iso_char S.inv_is_inverse by metis
    qed

    lemma iso_char:
    assumes "S.arr φ"
    shows "S.iso φ ⟷ iso φ"
      using assms S.iso_char inv_char by auto

  end

  locale right_hom =
    weak_composition V H +
    S: subcategory V ‹right ω›
  for V :: "'a comp"        (infixr "⋅" 55)
  and H :: "'a comp"        (infixr "⋆" 53)
  and ω :: 'a +
  assumes arr_ω: "arr ω"
  begin

    no_notation in_hom      ("«_ : _ → _»")
    notation in_hom         ("«_ : _ ⇒ _»")
    notation S.comp         (infixr "⋅S" 55)
    notation S.in_hom       ("«_ : _ ⇒S _»")

    lemma left_hcomp_closed [simp]:
    assumes "«μ : x ⇒S y»" and "«ν : c ⇒ d»" and "ν ⋆ μ ≠ null"
    shows "«ν ⋆ μ : c ⋆ x ⇒S d ⋆ y»"
    proof
      show 1: "S.arr (ν ⋆ μ)"
        using assms arr_ω S.arr_char right_def match_3
        by (elim S.in_homE, meson)
      show "S.dom (ν ⋆ μ) = c ⋆ x"
        using assms 1 by force
      show "S.cod (ν ⋆ μ) = d ⋆ y"
        using assms 1 by force
    qed

    lemma interchange:
    assumes "S.seq ν μ" and "S.seq τ σ" and "μ ⋆ σ ≠ null"
    shows "(ν ⋅S μ) ⋆ (τ ⋅S σ) = (ν ⋆ τ) ⋅S (μ ⋆ σ)"
    proof -
      have 1: "ν ⋆ τ ≠ null"
        using assms hom_connected(1) [of ν σ] hom_connected(2) [of ν τ] hom_connected(3-4)
        by fastforce
      have "(ν ⋅S μ) ⋆ (τ ⋅S σ) = (ν ⋅ μ) ⋆ (τ ⋅ σ)"
        using assms S.comp_char S.seq_char by metis
      also have "... = (ν ⋆ τ) ⋅ (μ ⋆ σ)"
        using assms interchange S.seq_char S.arr_char by simp
      also have "... = (ν ⋆ τ) ⋅S (μ ⋆ σ)"
      proof -
        have "S.arr (ν ⋆ τ)"
        proof -
          have "«ν : dom ν ⇒ cod ν»"
            using assms S.in_hom_char by blast
          thus ?thesis
            using assms 1 left_hcomp_closed by blast
        qed
        moreover have "S.arr (μ ⋆ σ)"
        proof -
          have "«μ : dom μ ⇒ cod μ»"
            using assms S.in_hom_char by blast
          thus ?thesis
            using assms left_hcomp_closed [of σ "dom σ" "cod σ" μ "dom μ" "cod μ"]
            by fastforce
        qed
        moreover have "seq (ν ⋆ τ) (μ ⋆ σ)"
          using assms 1 S.in_hom_char
          by (metis (full_types) S.seq_char hcomp_simpsWC(1-3) seqE seqI)
        ultimately show ?thesis
          using S.comp_char by auto
      qed
      finally show ?thesis by blast
    qed

    lemma inv_char:
    assumes "S.arr φ" and "iso φ"
    shows "S.inverse_arrows φ (inv φ)"
    and "S.inv φ = inv φ"
    proof -
      have 1: "S.arr (inv φ)"
      proof -
        have "S.arr φ" using assms by auto
        hence "φ ⋆ ω ≠ null"
          using S.arr_char right_def by simp
        hence "cod φ ⋆ ω ≠ null"
          using hom_connected(3) by blast
        hence "dom (inv φ) ⋆ ω ≠ null"
          using assms S.iso_char by simp
        hence "inv φ ⋆ ω ≠ null"
          using hom_connected(1) by blast
        thus ?thesis
          using S.arr_char right_def by force
      qed
      show "S.inv φ = inv φ"
        using assms 1 S.inv_char S.iso_char by blast
      thus "S.inverse_arrows φ (inv φ)"
        using assms 1 S.iso_char S.inv_is_inverse by metis
    qed

    lemma iso_char:
    assumes "S.arr φ"
    shows "S.iso φ ⟷ iso φ"
      using assms S.iso_char inv_char by auto

  end

  subsection "Weak Units"

  text ‹
    We now define a \emph{weak unit} to be an arrow ‹a› such that:
    \begin{enumerate}
    \item  ‹a ⋆ a› is isomorphic to ‹a›
           (and hence ‹a› is a horizontally self-composable 1-cell).
    \item  Horizontal composition on the left with ‹a› is a fully faithful endofunctor of the
           subcategory of arrows that are composable on the left with ‹a›.
    \item  Horizontal composition on the right with ‹a› is fully faithful endofunctor of the
           subcategory of arrows that are composable on the right with ‹a›.
    \end{enumerate}
  ›

  context weak_composition
  begin

    definition weak_unit :: "'a ⇒ bool"
    where "weak_unit a ≡ a ⋆ a ≅ a ∧
                         fully_faithful_functor (Left a) (Left a) (HL a) ∧
                         fully_faithful_functor (Right a) (Right a) (HR a)"

    lemma weak_unit_self_composable [simp]:
    assumes "weak_unit a"
    shows "ide a" and "ide (a ⋆ a)" and "a ⋆ a ≠ null"
    proof -
      obtain φ where φ: "«φ : a ⋆ a ⇒ a» ∧ iso φ"
        using assms weak_unit_def isomorphic_def by blast
      have 1: "arr φ" using φ by blast
      show "ide a" using φ ide_cod by blast
      thus "ide (a ⋆ a)" using φ ide_dom by force
      thus "a ⋆ a ≠ null" using not_arr_null ideD(1) by metis
    qed

    lemma weak_unit_self_right:
    assumes "weak_unit a"
    shows "right a a"
      using assms weak_unit_self_composable right_def by simp

    lemma weak_unit_self_left:
    assumes "weak_unit a"
    shows "left a a"
      using assms weak_unit_self_composable left_def by simp

    lemma weak_unit_in_vhom:
    assumes "weak_unit a"
    shows "«a : a ⇒ a»"
      using assms weak_unit_self_composable left_def by auto

    text ‹
      If ‹a› is a weak unit, then there exists a ``unit isomorphism'' ‹«ι : a ⋆ a ⇒ a»›.
      It need not be unique, but we may choose one arbitrarily.
    ›

    definition some_unit
    where "some_unit a ≡ SOME ι. iso ι ∧ «ι : a ⋆ a ⇒ a»"

    lemma iso_some_unit:
    assumes "weak_unit a"
    shows "iso (some_unit a)"
    and "«some_unit a : a ⋆ a ⇒ a»"
    proof -
      let ?P = "λι. iso ι ∧ «ι : a ⋆ a ⇒ a»"
      have "∃ι. ?P ι"
        using assms weak_unit_def by auto
      hence 1: "?P (some_unit a)"
        using someI_ex [of ?P] some_unit_def by simp
      show "iso (some_unit a)" using 1 by blast
      show "«some_unit a : a ⋆ a ⇒ a»" using 1 by blast
    qed

    text ‹
      The \emph{sources} of an arbitrary arrow ‹μ› are the weak units that are composable with ‹μ›
      on the right.  Similarly, the \emph{targets} of ‹μ› are the weak units that are composable
      with ‹μ› on the left.
    ›

    definition sources
    where "sources μ ≡ {a. weak_unit a ∧ μ ⋆ a ≠ null}"

    lemma sourcesI [intro]:
    assumes "weak_unit a" and "μ ⋆ a ≠ null"
    shows "a ∈ sources μ"
      using assms sources_def by blast

    lemma sourcesD [dest]:
    assumes "a ∈ sources μ"
    shows "ide a" and "weak_unit a" and "μ ⋆ a ≠ null"
      using assms sources_def by auto

    definition targets
    where "targets μ ≡ {b. weak_unit b ∧ b ⋆ μ ≠ null}"

    lemma targetsI [intro]:
    assumes "weak_unit b" and "b ⋆ μ ≠ null"
    shows "b ∈ targets μ"
      using assms targets_def by blast

    lemma targetsD [dest]:
    assumes "b ∈ targets μ"
    shows "ide b" and "weak_unit b" and "b ⋆ μ ≠ null"
      using assms targets_def by auto

    lemma sources_dom [simp]:
    assumes "arr μ"
    shows "sources (dom μ) = sources μ"
      using assms hom_connected(1) by blast

    lemma sources_cod [simp]:
    assumes "arr μ"
    shows "sources (cod μ) = sources μ"
      using assms hom_connected(3) by blast

    lemma targets_dom [simp]:
    assumes "arr μ"
    shows "targets (dom μ) = targets μ"
      using assms hom_connected(2) by blast

    lemma targets_cod [simp]:
    assumes "arr μ"
    shows "targets (cod μ) = targets μ"
      using assms hom_connected(4) by blast

    lemma weak_unit_iff_self_source:
    shows "weak_unit a ⟷ a ∈ sources a"
      using weak_unit_self_composable by auto

    lemma weak_unit_iff_self_target:
    shows "weak_unit b ⟷ b ∈ targets b"
      using weak_unit_self_composable by auto

    abbreviation (input) in_hhomWC  ("«_ : _ →WC _»")
    where "in_hhomWC μ f g ≡ arr μ ∧ f ∈ sources μ ∧ g ∈ targets μ"

    lemma sources_hcomp:
    assumes "ν ⋆ μ ≠ null"
    shows "sources (ν ⋆ μ) = sources μ"
      using assms match_1 match_3 null_agreement by blast

    lemma targets_hcomp:
    assumes "ν ⋆ μ ≠ null"
    shows "targets (ν ⋆ μ) = targets ν"
      using assms match_2 match_4 null_agreement by blast

    lemma HR_preserved_along_iso:
    assumes "weak_unit a" and "a ≅ a'"
    shows "endofunctor (Right a) (HR a')"
    proof -
      have a: "ide a ∧ weak_unit a" using assms isomorphic_def by auto
      have a': "ide a'" using assms isomorphic_def by auto
      (* TODO: The following interpretation re-introduces unwanted notation for "in_hom" *)
      interpret R: subcategory V ‹right a› using a right_hom_is_subcategory by simp
      have *: "⋀μ. R.arr μ ⟹ HR a' μ = μ ⋆ a'"
        using assms HR_def by simp
      have preserves_arr: "⋀μ. R.arr μ ⟹ R.arr (HR a' μ)"
        using assms a' * R.arr_char right_def weak_unit_def weak_unit_self_composable
              isomorphic_implies_equicomposable R.ide_char match_3 hcomp_simpsWC(1)
              null_agreement
        by metis
      show "endofunctor R.comp (HR a')"
      proof
        show "⋀μ. ¬ R.arr μ ⟹ HR a' μ = R.null"
          using assms R.arr_char R.null_char right_def HR_def null_agreement
                right_respects_isomorphic
          by metis
        fix μ
        assume "R.arr μ"
        hence μ: "R.arr μ ∧ arr μ ∧ right a μ ∧ right a' μ ∧ μ ⋆ a ≠ null ∧ μ ⋆ a' ≠ null"
          using assms R.arr_char right_respects_isomorphic composable_implies_arr null_agreement
                right_def
          by metis
        show "R.arr (HR a' μ)" using μ preserves_arr by blast
        show "R.dom (HR a' μ) = HR a' (R.dom μ)"
          using a' μ * R.arr_char R.dom_char preserves_arr hom_connected(1) right_def
          by simp
        show "R.cod (HR a' μ) = HR a' (R.cod μ)"
          using a' μ * R.arr_char R.cod_char preserves_arr hom_connected(3) right_def
          by simp
        next
        fix μ ν
        assume μν: "R.seq ν μ"
        have "R.arr μ"
          using μν by (elim R.seqE, auto)
        hence μ: "R.arr μ ∧ arr μ ∧ right a μ ∧ right a' μ ∧ μ ⋆ a ≠ null ∧ μ ⋆ a' ≠ null"
          using assms R.arr_char right_respects_isomorphic composable_implies_arr null_agreement
                right_def
          by metis
        have "ν ∈ R.hom (R.cod μ) (R.cod ν)"
          using μν by (elim R.seqE, auto)
        hence "«ν : R.cod μ ⇒ R.cod ν» ∧ arr ν ∧ ν ∈ Collect (right a)"
          using R.hom_char by blast
        hence ν: "«ν : R.cod μ → R.cod ν» ∧ arr ν ∧
                  right a ν ∧ H ν a ≠ null ∧ right a' ν ∧ H ν a' ≠ null"
          using assms right_def right_respects_isomorphic isomorphic_implies_equicomposable
          by simp
        show "HR a' (R.comp ν μ) = R.comp (HR a' ν) (HR a' μ)"
        proof -
          have 1: "R.arr (HR a' ν)"
            using ν preserves_arr by blast
          have 2: "seq (ν ⋆ a') (μ ⋆ a')"
            using a' μ ν R.arr_char R.inclusion R.dom_char R.cod_char
                   isomorphic_implies_equicomposable
            by auto
          show ?thesis
          proof -
            have "HR a' (R.comp ν μ) = (ν ⋅ μ) ⋆ a'"
              using μ ν HR_def R.comp_def by fastforce
            also have "... = (ν ⋆ a') ⋅ (μ ⋆ a')"
            proof -
              have "seq ν μ"
                using μ ν μν by (elim R.seqE, auto)
              thus ?thesis
                using a' ν whisker_right right_def by blast
            qed
            also have "... = R.comp (HR a' ν) (HR a' μ)"
              using assms μ 1 2 preserves_arr R.comp_char R.inclusion HR_def by auto
            finally show ?thesis by blast
          qed
        qed
      qed
    qed

    lemma HL_preserved_along_iso:
    assumes "weak_unit a" and "a ≅ a'"
    shows "endofunctor (Left a) (HL a')"
    proof -
      have a: "ide a ∧ weak_unit a" using assms isomorphic_def by auto
      have a': "ide a'" using assms isomorphic_def by auto
      (* TODO: The following interpretation re-introduces unwanted notation for "in_hom" *)
      interpret L: subcategory V ‹left a› using a left_hom_is_subcategory by simp
      have *: "⋀μ. L.arr μ ⟹ HL a' μ = a' ⋆ μ"
        using assms HL_def by simp
      have preserves_arr: "⋀μ. L.arr μ ⟹ L.arr (HL a' μ)"
        using assms a' * L.arr_char left_def weak_unit_def weak_unit_self_composable
              isomorphic_implies_equicomposable L.ide_char match_4 hcomp_simpsWC(1)
              null_agreement
        by metis
      show "endofunctor L.comp (HL a')"
      proof
        show "⋀μ. ¬ L.arr μ ⟹ HL a' μ = L.null"
          using assms L.arr_char L.null_char left_def HL_def null_agreement
                left_respects_isomorphic
          by metis
        fix μ
        assume "L.arr μ"
        hence μ: "L.arr μ ∧ arr μ ∧ left a μ ∧ left a' μ ∧ a ⋆ μ ≠ null ∧ a' ⋆ μ ≠ null"
          using assms L.arr_char left_respects_isomorphic composable_implies_arr null_agreement
                left_def
          by metis
        show "L.arr (HL a' μ)" using μ preserves_arr by blast
        show "L.dom (HL a' μ) = HL a' (L.dom μ)"
          using a' μ * L.arr_char L.dom_char preserves_arr hom_connected(2) left_def
          by simp
        show "L.cod (HL a' μ) = HL a' (L.cod μ)"
          using a' μ * L.arr_char L.cod_char preserves_arr hom_connected(4) left_def
          by simp
        next
        fix μ ν
        assume μν: "L.seq ν μ"
        have "L.arr μ"
          using μν by (elim L.seqE, auto)
        hence μ: "L.arr μ ∧ arr μ ∧ left a μ ∧ left a' μ ∧ a ⋆ μ ≠ null ∧ a' ⋆ μ ≠ null"
          using assms L.arr_char left_respects_isomorphic composable_implies_arr null_agreement
                left_def
          by metis
        have "L.in_hom ν (L.cod μ) (L.cod ν)"
          using μν by (elim L.seqE, auto)
        hence "«ν : L.cod μ ⇒ L.cod ν» ∧ arr ν ∧ ν ∈ Collect (left a)"
          using L.hom_char by blast
        hence ν: "«ν : L.cod μ ⇒ L.cod ν» ∧ arr ν ∧
                  left a ν ∧ a ⋆ ν ≠ null ∧ left a' ν ∧ a' ⋆ ν ≠ null"
          using assms left_def left_respects_isomorphic isomorphic_implies_equicomposable
          by simp
        show "HL a' (L.comp ν μ) = L.comp (HL a' ν) (HL a' μ)"
        proof -
          have 1: "L.arr (HL a' ν)"
            using ν preserves_arr by blast
          have 2: "seq (a' ⋆ ν) (a' ⋆ μ)"
            using a' μ ν L.arr_char L.inclusion L.dom_char L.cod_char
                  isomorphic_implies_equicomposable
            by auto
          have "HL a' (L.comp ν μ) = a' ⋆ (ν ⋅ μ)"
            using μ ν HL_def L.comp_def by fastforce
          also have "... = (a' ⋆ ν) ⋅ (a' ⋆ μ)"
          proof -
            have "seq ν μ"
              using μ ν μν by (elim L.seqE, auto)
            thus ?thesis
              using a' ν whisker_left right_def by blast
          qed
          also have "... = L.comp (HL a' ν) (HL a' μ)"
            using assms μ 1 2 preserves_arr L.comp_char L.inclusion HL_def by auto
          finally show ?thesis by blast
        qed
      qed
    qed

  end

  subsection "Regularity"

  text ‹
    We call a weak composition \emph{regular} if ‹f ⋆ a ≅ f› whenever ‹a› is a source of
    1-cell ‹f›, and ‹b ⋆ f ≅ f› whenever ‹b› is a target of ‹f›.  A consequence of regularity
    is that horizontal composability of 2-cells is fully determined by their sets of
    sources and targets.
  ›

  locale regular_weak_composition =
    weak_composition +
  assumes comp_ide_source: "⟦ a ∈ sources f; ide f ⟧ ⟹ f ⋆ a ≅ f"
  and comp_target_ide: "⟦ b ∈ targets f; ide f ⟧ ⟹ b ⋆ f ≅ f"
  begin

    lemma sources_determine_composability:
    assumes "a ∈ sources τ"
    shows "τ ⋆ μ ≠ null ⟷ a ⋆ μ ≠ null"
    proof -
      have *: "⋀τ. ide τ ∧ a ∈ sources τ ⟹ τ ⋆ μ ≠ null ⟷ a ⋆ μ ≠ null"
      proof -
        fix τ
        assume τ: "ide τ ∧ a ∈ sources τ"
        show "τ ⋆ μ ≠ null ⟷ a ⋆ μ ≠ null"
        proof
          assume μ: "τ ⋆ μ ≠ null"
          show "a ⋆ μ ≠ null"
            using assms μ τ comp_ide_source isomorphic_implies_equicomposable match_1
            by blast
          next
          assume μ: "a ⋆ μ ≠ null"
          show "τ ⋆ μ ≠ null"
            using assms μ τ comp_ide_source isomorphic_implies_equicomposable match_3
            by blast
        qed
      qed
      show ?thesis
      proof -
        have "arr τ" using assms composable_implies_arr by auto
        thus ?thesis
          using assms * [of "dom τ"] hom_connected(1) by auto
      qed
    qed

    lemma targets_determine_composability:
    assumes "b ∈ targets μ"
    shows "τ ⋆ μ ≠ null ⟷ τ ⋆ b ≠ null"
    proof -
      have *: "⋀μ. ide μ ∧ b ∈ targets μ ⟹ τ ⋆ μ ≠ null ⟷ τ ⋆ b ≠ null"
      proof -
        fix μ
        assume μ: "ide μ ∧ b ∈ targets μ"
        show "τ ⋆ μ ≠ null ⟷ τ ⋆ b ≠ null"
        proof
          assume τ: "τ ⋆ μ ≠ null"
          show "τ ⋆ b ≠ null"
            using assms μ τ comp_target_ide isomorphic_implies_equicomposable match_2
            by blast
          next
          assume τ: "τ ⋆ b ≠ null"
          show "τ ⋆ μ ≠ null"
            using assms μ τ  comp_target_ide isomorphic_implies_equicomposable match_4
            by blast
        qed
      qed
      show ?thesis
      proof -
        have "arr μ" using assms composable_implies_arr by auto
        thus ?thesis
          using assms * [of "dom μ"] hom_connected(2) by auto
      qed
    qed

    lemma composable_if_connected:
    assumes "sources ν ∩ targets μ ≠ {}"
    shows "ν ⋆ μ ≠ null"
      using assms targets_determine_composability by blast

    lemma connected_if_composable:
    assumes "ν ⋆ μ ≠ null"
    shows "sources ν = targets μ"
      using assms sources_determine_composability targets_determine_composability by blast

    lemma iso_hcompRWC:
    assumes "iso μ" and "iso ν" and "sources ν ∩ targets μ ≠ {}"
    shows "iso (ν ⋆ μ)"
    and "inverse_arrows (ν ⋆ μ) (inv ν ⋆ inv μ)"
    proof -
      have μ: "arr μ ∧ «μ : dom μ ⇒ cod μ» ∧
               iso μ ∧ «inv μ : cod μ ⇒ dom μ»"
        using assms inv_in_hom arr_iff_in_hom iso_is_arr by auto
      have ν: "arr ν ∧ «ν : dom ν ⇒ cod ν» ∧
               iso ν ∧ «inv ν : cod ν ⇒ dom ν»"
        using assms inv_in_hom by blast
      have 1: "sources (inv ν) ∩ targets (inv μ) ≠ {}"
      proof -
        have "sources (inv ν) ∩ targets (inv μ) = sources ν ∩ targets μ"
        proof -
          have "sources (inv ν) ∩ targets (inv μ)
                  = sources (cod (inv ν)) ∩ targets (cod (inv μ))"
            using assms μ ν sources_cod targets_cod arr_inv by presburger
          also have "... = sources (dom ν) ∩ targets (dom μ)"
            using μ ν by simp
          also have "... = sources ν ∩ targets μ"
            using μ ν sources_dom targets_dom by simp
          finally show ?thesis by blast
        qed
        thus ?thesis using assms by simp
      qed
      show "inverse_arrows (ν ⋆ μ) (inv ν ⋆ inv μ)"
      proof
        have "(inv ν ⋆ inv μ) ⋅ (ν ⋆ μ) = dom ν ⋆ dom μ"
          using assms μ ν inv_in_hom inv_is_inverse comp_inv_arr
                interchange [of "inv ν" ν "inv μ" μ] composable_if_connected
          by simp
        moreover have "ide (dom ν ⋆ dom μ)"
          using assms μ ν ide_hcompWC composable_if_connected sources_dom targets_dom
          by auto
        ultimately show "ide ((inv ν ⋆ inv μ) ⋅ (ν ⋆ μ))"
          by presburger
        have "(ν ⋆ μ) ⋅ (inv ν ⋆ inv μ) = cod ν ⋆ cod μ"
          using assms 1 μ ν inv_in_hom inv_is_inverse comp_arr_inv
                interchange [of ν "inv ν" μ "inv μ"] composable_if_connected
          by simp
        moreover have "ide (cod ν ⋆ cod μ)"
          using assms μ ν ide_hcompWC composable_if_connected sources_cod targets_cod
          by auto
        ultimately show "ide ((ν ⋆ μ) ⋅ (inv ν ⋆ inv μ))"
          by presburger
      qed
      thus "iso (ν ⋆ μ)" by auto
    qed

    lemma inv_hcompRWC:
    assumes "iso μ" and "iso ν" and "sources ν ∩ targets μ ≠ {}"
    shows "inv (ν ⋆ μ) = inv ν ⋆ inv μ"
      using assms iso_hcompRWC(2) [of μ ν] inverse_arrow_unique [of "H ν μ"] inv_is_inverse
      by auto

  end

  subsection "Associativity"

  text ‹
    An \emph{associative weak composition} consists of a weak composition that has been
    equipped with an \emph{associator} isomorphism: ‹«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»›
    for each composable triple ‹(f, g, h)› of 1-cells, subject to naturality and
    coherence conditions.
  ›

  locale associative_weak_composition =
    weak_composition +
  fixes 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a"    ("𝖺[_, _, _]")
  assumes assoc_in_vhomAWC:
           "⟦ ide f; ide g; ide h; f ⋆ g ≠ null; g ⋆ h ≠ null ⟧ ⟹
              «𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»"
  and assoc_naturalityAWC:
           "⟦ τ ⋆ μ ≠ null; μ ⋆ ν ≠ null ⟧ ⟹
              𝖺[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) = (τ ⋆ μ ⋆ ν) ⋅ 𝖺[dom τ, dom μ, dom ν]"
  and iso_assocAWC: "⟦ ide f; ide g; ide h; f ⋆ g ≠ null; g ⋆ h ≠ null ⟧ ⟹ iso 𝖺[f, g, h]"
  and pentagonAWC:
           "⟦ ide f; ide g; ide h; ide k; sources f ∩ targets g ≠ {};
              sources g ∩ targets h ≠ {}; sources h ∩ targets k ≠ {} ⟧ ⟹
              (f ⋆ 𝖺[g, h, k]) ⋅ 𝖺[f, g ⋆ h, k] ⋅ (𝖺[f, g, h] ⋆ k) = 𝖺[f, g, h ⋆ k] ⋅ 𝖺[f ⋆ g, h, k]"
  begin

    lemma assoc_in_homAWC:
    assumes "ide f" and "ide g" and "ide h"
    and "f ⋆ g ≠ null" and "g ⋆ h ≠ null"
    shows "sources 𝖺[f, g, h] = sources h" and "targets 𝖺[f, g, h] = targets f"
    and "«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»"
    proof -
      show 1: "«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»"
        using assms assoc_in_vhomAWC by simp
      show "sources 𝖺[f, g, h] = sources h"
        using assms 1 sources_dom [of "𝖺[f, g, h]"] sources_hcomp match_3
        by (elim in_homE, auto)
      show "targets 𝖺[f, g, h] = targets f"
        using assms 1 targets_cod [of "𝖺[f, g, h]"] targets_hcomp match_4
        by (elim in_homE, auto)
    qed

    lemma assoc_simpsAWC [simp]:
    assumes "ide f" and "ide g" and "ide h"
    and "f ⋆ g ≠ null" and "g ⋆ h ≠ null"
    shows "arr 𝖺[f, g, h]"
    and "dom 𝖺[f, g, h] = (f ⋆ g) ⋆ h"
    and "cod 𝖺[f, g, h] = f ⋆ g ⋆ h"
    proof -
      have 1: "«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»"
        using assms assoc_in_homAWC by auto
      show "arr 𝖺[f, g, h]" using 1 by auto
      show "dom 𝖺[f, g, h] = (f ⋆ g) ⋆ h" using 1 by auto
      show "cod 𝖺[f, g, h] = f ⋆ g ⋆ h" using 1 by auto
    qed

    lemma assoc'_in_homAWC:
    assumes "ide f" and "ide g" and "ide h"
    and "f ⋆ g ≠ null" and "g ⋆ h ≠ null"
    shows "sources (inv 𝖺[f, g, h]) = sources h" and "targets (inv 𝖺[f, g, h]) = targets f"
    and "«inv 𝖺[f, g, h] :  f ⋆ g ⋆ h ⇒ (f ⋆ g) ⋆ h»"
    proof -
      show 1: "«inv 𝖺[f, g, h] :  f ⋆ g ⋆ h ⇒ (f ⋆ g) ⋆ h»"
        using assms assoc_in_homAWC iso_assocAWC inv_in_hom by auto
      show "sources (inv 𝖺[f, g, h]) = sources h"
        using assms 1 sources_hcomp [of "f ⋆ g" h] sources_cod match_3 null_agreement
        by (elim in_homE, metis)
      show "targets (inv 𝖺[f, g, h]) = targets f"
        using assms 1 targets_hcomp [of f "g ⋆ h"] targets_dom match_4 null_agreement
        by (elim in_homE, metis)
    qed

    lemma assoc'_simpsAWC [simp]:
    assumes "ide f" and "ide g" and "ide h"
    and "f ⋆ g ≠ null" and "g ⋆ h ≠ null"
    shows "arr (inv 𝖺[f, g, h])"
    and "dom (inv 𝖺[f, g, h]) = f ⋆ g ⋆ h"
    and "cod (inv 𝖺[f, g, h]) = (f ⋆ g) ⋆ h"
    proof -
      have 1: "«inv 𝖺[f, g, h] : f ⋆ g ⋆ h ⇒ (f ⋆ g) ⋆ h»"
        using assms assoc'_in_homAWC by auto
      show "arr (inv 𝖺[f, g, h])" using 1 by auto
      show "dom (inv 𝖺[f, g, h]) = f ⋆ g ⋆ h" using 1 by auto
      show "cod (inv 𝖺[f, g, h]) = (f ⋆ g) ⋆ h" using 1 by auto
    qed

    lemma assoc'_naturalityAWC:
    assumes "τ ⋆ μ ≠ null" and "μ ⋆ ν ≠ null"
    shows "inv 𝖺[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν) = ((τ ⋆ μ) ⋆ ν) ⋅ inv 𝖺[dom τ, dom μ, dom ν]"
    proof -
      have τμν: "arr τ ∧ arr μ ∧ arr ν"
        using assms composable_implies_arr by simp
      have 0: "dom τ ⋆ dom μ ≠ null ∧ dom μ ⋆ dom ν ≠ null ∧
               cod τ ⋆ cod μ ≠ null ∧ cod μ ⋆ cod ν ≠ null"
        using assms τμν hom_connected by simp
      have 1: "«τ ⋆ μ ⋆ ν : dom τ ⋆ dom μ ⋆ dom ν ⇒ cod τ ⋆ cod μ ⋆ cod ν»"
        using assms match_4 by auto
      have 2: "«(τ ⋆ μ) ⋆ ν : (dom τ ⋆ dom μ) ⋆ dom ν ⇒ (cod τ ⋆ cod μ) ⋆ cod ν»"
        using assms match_3 by auto
      have "(inv 𝖺[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν)) ⋅ 𝖺[dom τ, dom μ, dom ν] = (τ ⋆ μ) ⋆ ν"
      proof -
        have "(τ ⋆ μ) ⋆ ν = (inv 𝖺[cod τ, cod μ, cod ν] ⋅ 𝖺[cod τ, cod μ, cod ν]) ⋅ ((τ ⋆ μ) ⋆ ν)"
          using 0 2 τμν assoc_in_homAWC iso_assocAWC comp_inv_arr inv_is_inverse comp_cod_arr
          by auto
        also have "... = inv 𝖺[cod τ, cod μ, cod ν] ⋅ 𝖺[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν)"
          using comp_assoc by auto
        also have "... = inv 𝖺[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν) ⋅ 𝖺[dom τ, dom μ, dom ν]"
          using assms τμν 0 2 assoc_naturalityAWC by presburger
        also have "... = (inv 𝖺[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν)) ⋅ 𝖺[dom τ, dom μ, dom ν]"
          using comp_assoc by auto
        finally show ?thesis by argo
      qed
      thus ?thesis
        using 0 1 2 τμν iso_assocAWC assoc'_in_homAWC inv_in_hom invert_side_of_triangle(2)
        by auto
      qed

  end

  subsection "Unitors"

  text ‹
    For an associative weak composition with a chosen unit isomorphism ‹ι : a ⋆ a ⇒ a›,
    where ‹a› is a weak unit, horizontal composition on the right by ‹a› is a fully faithful
    endofunctor ‹R› of the subcategory of arrows composable on the right with ‹a›, and is
    consequently an endo-equivalence of that subcategory.  This equivalence, together with the
    associator isomorphisms and unit isomorphism ‹ι›, canonically associate, with each
    identity arrow ‹f› composable on the right with ‹a›, a \emph{right unit} isomorphism
    ‹«𝗋[f] : f ⋆ a ⇒ f»›.  These isomorphisms are the components of a natural isomorphism
    from ‹R› to the identity functor.
  ›

  locale right_hom_with_unit =
    associative_weak_composition V H 𝖺 +
    right_hom V H a
  for V :: "'a comp"                  (infixr "⋅" 55)
  and H :: "'a comp"                  (infixr "⋆" 53)
  and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a"      ("𝖺[_, _, _]")
  and ι :: 'a
  and a :: 'a +
  assumes weak_unit_a: "weak_unit a"
  and ι_in_hom: "«ι : a ⋆ a ⇒ a»"
  and iso_ι: "iso ι"
  begin

    abbreviation R
    where "R ≡ HR a"

    interpretation R: endofunctor S.comp R
      using weak_unit_a weak_unit_self_composable endofunctor_HR by simp
    interpretation R: fully_faithful_functor S.comp S.comp R
      using weak_unit_a weak_unit_def by simp

    lemma fully_faithful_functor_R:
    shows "fully_faithful_functor S.comp S.comp R"
      ..

    definition runit  ("𝗋[_]")
    where "runit f ≡ THE μ. «μ : R f ⇒S f» ∧ R μ = (f ⋆ ι) ⋅S 𝖺[f, a, a]"

    lemma iso_unit:
    shows "S.iso ι" and "«ι : a ⋆ a ⇒S a»"
    proof -
      show "«ι : a ⋆ a ⇒S a»"
      proof -
        have a: "weak_unit a ∧ S.ide a"
          using weak_unit_a S.ide_char S.arr_char right_def weak_unit_self_composable
          by metis
        moreover have "S.arr (a ⋆ a)"
          using a S.ideD(1) R.preserves_arr HR_def by auto
        ultimately show ?thesis
          using a S.in_hom_char S.arr_char right_def ι_in_hom
          by (metis S.ideD(1) hom_connected(3) in_homE)
      qed
      thus "S.iso ι"
        using iso_ι iso_char by blast
    qed

    lemma characteristic_iso:
    assumes "S.ide f"
    shows "«𝖺[f, a, a] : (f ⋆ a) ⋆ a ⇒S f ⋆ a ⋆ a»"
    and "«f ⋆ ι : f ⋆ a ⋆ a ⇒S f ⋆ a»"
    and "«(f ⋆ ι) ⋅S 𝖺[f, a, a] : R (R f) ⇒S R f»"
    and "S.iso ((f ⋆ ι) ⋅S 𝖺[f, a, a])"
    proof -
      have f: "S.ide f ∧ ide f"
        using assms S.ide_char by simp
      have a: "weak_unit a ∧ ide a ∧ S.ide a"
        using weak_unit_a S.ide_char weak_unit_def S.arr_char right_def
              weak_unit_self_composable
        by metis
      have fa: "f ⋆ a ≠ null ∧ (f ⋆ a) ⋆ a ≠ null ∧ ((f ⋆ a) ⋆ a) ⋆ a ≠ null"
      proof -
        have "S.arr (f ⋆ a) ∧ S.arr ((f ⋆ a) ⋆ a) ∧ S.arr (((f ⋆ a) ⋆ a) ⋆ a)"
          using assms S.ideD(1) R.preserves_arr HR_def by auto
        thus ?thesis
          using S.not_arr_null by fastforce
      qed
      have aa: "a ⋆ a ≠ null"
        using a S.ideD(1) R.preserves_arr HR_def S.not_arr_null by auto
      have ia_a: "ι ⋆ a ≠ null"
        using weak_unit_a hom_connected(3) weak_unit_self_composable ι_in_hom by blast
      have f_ia: "f ⋆ ι ≠ null"
        using assms S.ide_char right_def S.arr_char hom_connected(4) ι_in_hom by auto
      show assoc_in_hom: "«𝖺[f, a, a] : (f ⋆ a) ⋆ a ⇒S f ⋆ a ⋆ a»"
        using a f fa hom_connected(1) [of "𝖺[f, a, a]" a] S.arr_char right_def
              match_3 match_4 S.in_hom_char
        by auto
      show 1: "«f ⋆ ι : f ⋆ a ⋆ a ⇒S f ⋆ a»"
        using a f fa iso_unit
        by (simp add: f_ia ide_in_hom)
      moreover have "S.iso (f ⋆ ι)"
        using a f fa f_ia 1 VoV.arr_char VxV.inv_simp
              inv_in_hom hom_connected(2) [of f "inv ι"] VoV.arr_char VoV.iso_char
              preserves_iso iso_char iso_ι
        by auto
      ultimately have unit_part: "«f ⋆ ι : f ⋆ a ⋆ a ⇒S f ⋆ a» ∧ S.iso (f ⋆ ι)"
        by blast
      show "S.iso ((f ⋆ ι) ⋅S 𝖺[f, a, a])"
        using assms a f fa aa hom_connected(1) [of "𝖺[f, a, a]" a] right_def
              iso_assocAWC iso_char S.arr_char unit_part assoc_in_hom isos_compose
        using S.isos_compose S.seqI' by auto
      show "«(f ⋆ ι) ⋅S 𝖺[f, a, a] : R (R f) ⇒S R f»"
        unfolding HR_def using unit_part assoc_in_hom by blast
    qed

    lemma runit_char:
    assumes "S.ide f"
    shows "«𝗋[f] : R f ⇒S f»" and "R 𝗋[f] = (f ⋆ ι) ⋅S 𝖺[f, a, a]"
    and "∃!μ. «μ : R f ⇒S f» ∧ R μ = (f ⋆ ι) ⋅S 𝖺[f, a, a]"
    proof -
      let ?P = "λμ. «μ : R f ⇒S f» ∧ R μ = (f ⋆ ι) ⋅S 𝖺[f, a, a]"
      show "∃!μ. ?P μ"
      proof -
        have "∃μ. ?P μ"
        proof -
          have 1: "S.ide f"
            using assms S.ide_char S.arr_char by simp
          moreover have "S.ide (R f)"
            using 1 R.preserves_ide by simp
          ultimately show ?thesis
            using assms characteristic_iso(3) R.is_full by blast
        qed
        moreover have "∀μ μ'. ?P μ ∧ ?P μ' ⟶ μ = μ'"
        proof
          fix μ
          show "∀μ'. ?P μ ∧ ?P μ' ⟶ μ = μ'"
            using R.is_faithful [of μ] by fastforce
        qed
        ultimately show ?thesis by blast
      qed
      hence "?P (THE μ. ?P μ)"
        using theI' [of ?P] by fastforce
      hence 1: "?P 𝗋[f]"
        unfolding runit_def by blast
      show "«𝗋[f] : R f ⇒S f»" using 1 by fast
      show "R 𝗋[f] = (f ⋆ ι) ⋅S 𝖺[f, a, a]" using 1 by fast
    qed

    lemma iso_runit:
    assumes "S.ide f"
    shows "S.iso 𝗋[f]"
      using assms characteristic_iso(4) runit_char R.reflects_iso by metis

    lemma runit_eqI:
    assumes "«f : a ⇒S b»" and "«μ : R f ⇒S f»"
    and "R μ = ((f ⋆ ι) ⋅S 𝖺[f, a, a])"
    shows "μ = 𝗋[f]"
    proof -
      have "S.ide f" using assms(2) S.ide_cod by auto
      thus ?thesis using assms runit_char [of f] by auto
    qed

    lemma runit_naturality:
    assumes "S.arr μ"
    shows "𝗋[S.cod μ] ⋅S R μ = μ ⋅S 𝗋[S.dom μ]"
    proof -
      have 1: "«𝗋[S.cod μ] ⋅S R μ : R (S.dom μ) ⇒S S.cod μ»"
        using assms runit_char(1) S.ide_cod by blast
      have 2: "S.par (𝗋[S.cod μ] ⋅S R μ) (μ ⋅S 𝗋[S.dom μ])"
      proof -
        have "«μ ⋅S 𝗋[S.dom μ] : R (S.dom μ) ⇒S S.cod μ»"
          using assms S.ide_dom runit_char(1) by blast
        thus ?thesis using 1 by (elim S.in_homE, auto)
      qed
      moreover have "R (𝗋[S.cod μ] ⋅S R μ) = R (μ ⋅S 𝗋[S.dom μ])"
      proof -
        have 3: "«μ ⋆ a ⋆ a : S.dom μ ⋆ a ⋆ a ⇒S S.cod μ ⋆ a ⋆ a»"
          using assms weak_unit_a R.preserves_hom HR_def S.arr_iff_in_hom S.arr_char
          by (metis match_4 weak_unit_in_vhom weak_unit_self_right S.in_hom_char
              left_hcomp_closed S.not_arr_null S.null_char)
        have 4: "R (𝗋[S.cod μ] ⋅S R μ) = R 𝗋[S.cod μ] ⋅S R (R μ)"
          using assms 1 R.preserves_comp_2 by blast
        also have 5: "... = ((S.cod μ ⋆ ι) ⋅S 𝖺[S.cod μ, a, a]) ⋅S ((μ ⋆ a) ⋆ a)"
          using assms R.preserves_arr runit_char S.ide_cod HR_def by auto
        also have 6: "... = (S.cod μ ⋆ ι) ⋅S 𝖺[S.cod μ, a, a] ⋅S ((μ ⋆ a) ⋆ a)"
          using assms S.comp_assoc by simp
        also have "... = (S.cod μ ⋆ ι) ⋅S (μ ⋆ a ⋆ a) ⋅S 𝖺[S.dom μ, a, a]"
        proof -
          have "(μ ⋆ a ⋆ a) ⋅S 𝖺[S.dom μ, a, a] = 𝖺[S.cod μ, a, a] ⋅S ((μ ⋆ a) ⋆ a)"
          proof -
            have "(μ ⋆ a ⋆ a) ⋅S 𝖺[S.dom μ, a, a] = (μ ⋆ a ⋆ a) ⋅ 𝖺[S.dom μ, a, a]"
              using assms 3 S.ide_dom characteristic_iso(1) S.in_hom_char
                    S.comp_char [of "μ ⋆ a ⋆ a" "𝖺[S.dom μ, a, a]"]
              by fastforce
            also have "... = 𝖺[S.cod μ, a, a] ⋅ ((μ ⋆ a) ⋆ a)"
            proof -
              have "μ ⋆ a ≠ null"
                using assms S.arr_char right_def by simp
              thus ?thesis
                using assms weak_unit_a assoc_naturalityAWC [of μ a a] by fastforce
            qed
            also have "... = 𝖺[S.cod μ, a, a] ⋅S ((μ ⋆ a) ⋆ a)"
              using S.in_hom_char S.comp_char
              by (metis 2 4 5 6 R.preserves_arr S.seq_char)
            finally show ?thesis by blast
          qed
         thus ?thesis by argo
        qed
        also have "... = ((S.cod μ ⋆ ι) ⋅S (μ ⋆ a ⋆ a)) ⋅S 𝖺[S.dom μ, a, a]"
          using S.comp_assoc by auto
        also have "... = ((μ ⋆ a) ⋅S (S.dom μ ⋆ ι)) ⋅S 𝖺[S.dom μ, a, a]"
        proof -
          have "μ ⋆ a ⋆ a ≠ null"
            using 3 S.not_arr_null by (elim S.in_homE, auto)
          moreover have "S.dom μ ⋆ ι ≠ null"
            using assms S.not_arr_null
            by (metis S.dom_char ι_in_hom calculation hom_connected(1-2) in_homE)
          ultimately have "(S.cod μ ⋆ ι) ⋅S (μ ⋆ a ⋆ a) = (μ ⋆ a) ⋅S (S.dom μ ⋆ ι)"
            using assms weak_unit_a iso_unit S.comp_arr_dom S.comp_cod_arr
                  interchange [of "S.cod μ" μ ι "a ⋆ a"] interchange [of μ "S.dom μ" a ι]
            by auto
          thus ?thesis by argo
        qed
        also have "... = (μ ⋆ a) ⋅S (S.dom μ ⋆ ι) ⋅S 𝖺[S.dom μ, a, a]"
          using S.comp_assoc by auto
        also have "... = R μ ⋅S R 𝗋[S.dom μ]"
          using assms runit_char(2) S.ide_dom HR_def by auto
        also have "... = R (μ ⋅S 𝗋[S.dom μ])"
          using assms S.arr_iff_in_hom [of μ] runit_char(1) S.ide_dom by fastforce
        finally show ?thesis by blast
      qed
      ultimately show "𝗋[S.cod μ] ⋅S (R μ) = μ ⋅S 𝗋[S.dom μ]"
        using R.is_faithful by blast
    qed

    abbreviation 𝔯
    where "𝔯 μ ≡ if S.arr μ then μ ⋅S 𝗋[S.dom μ] else null"

    interpretation 𝔯: natural_transformation S.comp S.comp R S.map 𝔯
    proof -
      interpret 𝔯: transformation_by_components S.comp S.comp R S.map runit
        using runit_char(1) runit_naturality by (unfold_locales, simp_all)
      have "𝔯.map = 𝔯"
        using 𝔯.is_extensional 𝔯.map_def 𝔯.naturality 𝔯.map_simp_ide S.ide_dom S.ide_cod
              S.map_def
        by auto
      thus "natural_transformation S.comp S.comp R S.map 𝔯"
        using 𝔯.natural_transformation_axioms by auto
    qed

    lemma natural_transformation_𝔯:
    shows "natural_transformation S.comp S.comp R S.map 𝔯" ..

    interpretation 𝔯: natural_isomorphism S.comp S.comp R S.map 𝔯
      using S.ide_is_iso iso_runit runit_char(1) S.isos_compose
      by (unfold_locales, force)

    lemma natural_isomorphism_𝔯:
    shows "natural_isomorphism S.comp S.comp R S.map 𝔯" ..

    interpretation R: equivalence_functor S.comp S.comp R
      using natural_isomorphism_𝔯 R.isomorphic_to_identity_is_equivalence by blast

    lemma equivalence_functor_R:
    shows "equivalence_functor S.comp S.comp R"
      ..

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

  end

  text ‹
    Symmetric results hold for the subcategory of all arrows composable on the left with
    a specified weak unit ‹b›.  This yields the \emph{left unitors}.
  ›

  locale left_hom_with_unit =
    associative_weak_composition V H 𝖺 +
    left_hom V H b
  for V :: "'a comp"                  (infixr "⋅" 55)
  and H :: "'a comp"                  (infixr "⋆" 53)
  and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a"      ("𝖺[_, _, _]")
  and ι :: 'a
  and b :: 'a +
  assumes weak_unit_b: "weak_unit b"
  and ι_in_hom: "«ι : b ⋆ b ⇒ b»"
  and iso_ι: "iso ι"
  begin

    abbreviation L
    where "L ≡ HL b"

    interpretation L: endofunctor S.comp L
      using weak_unit_b weak_unit_self_composable endofunctor_HL by simp
    interpretation L: fully_faithful_functor S.comp S.comp L
      using weak_unit_b weak_unit_def by simp

    lemma fully_faithful_functor_L:
    shows "fully_faithful_functor S.comp S.comp L"
      ..

    definition lunit  ("𝗅[_]")
    where "lunit f ≡ THE μ. «μ : L f ⇒S f» ∧ L μ = (ι ⋆ f) ⋅S (inv 𝖺[b, b, f])"

    lemma iso_unit:
    shows "S.iso ι" and "«ι : b ⋆ b ⇒S b»"
    proof -
      show "«ι : b ⋆ b ⇒S b»"
      proof -
        have b: "weak_unit b ∧ S.ide b"
          using weak_unit_b S.ide_char S.arr_char left_def weak_unit_self_composable
          by metis
        moreover have "S.arr (b ⋆ b)"
          using b S.ideD(1) L.preserves_arr HL_def by auto
        ultimately show ?thesis
          using b S.in_hom_char S.arr_char left_def ι_in_hom
          by (metis S.ideD(1) hom_connected(4) in_homE)
      qed
      thus "S.iso ι"
        using iso_ι iso_char by blast
    qed

    lemma characteristic_iso:
    assumes "S.ide f"
    shows "«inv 𝖺[b, b, f] :  b ⋆ b ⋆ f ⇒S (b ⋆ b) ⋆ f»"
    and "«ι ⋆ f : (b ⋆ b) ⋆ f ⇒S b ⋆ f»"
    and "«(ι ⋆ f) ⋅S inv 𝖺[b, b, f] : L (L f) ⇒S L f»"
    and "S.iso ((ι ⋆ f) ⋅S inv 𝖺[b, b, f])"
    proof -
      have f: "S.ide f ∧ ide f"
        using assms S.ide_char by simp
      have b: "weak_unit b ∧ ide b ∧ S.ide b"
        using weak_unit_b S.ide_char weak_unit_def S.arr_char left_def
              weak_unit_self_composable
        by metis
      have bf: "b ⋆ f ≠ null ∧ b ⋆ b ⋆ b ⋆ f ≠ null"
      proof -
        have "S.arr (b ⋆ f) ∧ S.arr (b ⋆ b ⋆ f) ∧ S.arr (b ⋆ b ⋆ b ⋆ f)"
          using assms S.ideD(1) L.preserves_arr HL_def by auto
        thus ?thesis
          using S.not_arr_null by fastforce
      qed
      have bb: "b ⋆ b ≠ null"
      proof -
        have "S.arr (b ⋆ b)"
          using b S.ideD(1) L.preserves_arr HL_def by auto
        thus ?thesis
          using S.not_arr_null by fastforce
      qed
      have b_ib: "b ⋆ ι ≠ null"
        using weak_unit_b hom_connected(4) weak_unit_self_composable ι_in_hom by blast
      have ib_f: "ι ⋆ f ≠ null"
        using assms S.ide_char left_def S.arr_char hom_connected(3) ι_in_hom
        by auto
      show assoc_in_hom: "«inv 𝖺[b, b, f] : b ⋆ b ⋆ f ⇒S (b ⋆ b) ⋆ f»"
        using b f bf bb hom_connected(2) [of b "inv 𝖺[b, b, f]"] left_def
        by (metis S.arrI S.cod_closed S.in_hom_char assoc'_in_homAWC(3) assoc'_simpsAWC(2-3))
      show 1: "«ι ⋆ f : (b ⋆ b) ⋆ f ⇒S b ⋆ f»"
        using b f bf by (simp add: ib_f ide_in_hom iso_unit(2))
      moreover have "S.iso (ι ⋆ f)"
        using b f bf ib_f 1 VoV.arr_char VxV.inv_simp
              inv_in_hom hom_connected(1) [of "inv ι" f] VoV.arr_char VoV.iso_char
              preserves_iso iso_char iso_ι
        by auto
      ultimately have unit_part: "«ι ⋆ f : (b ⋆ b) ⋆ f ⇒S b ⋆ f» ∧ S.iso (ι ⋆ f)"
        by blast
      show "S.iso ((ι ⋆ f) ⋅S inv 𝖺[b, b, f])"
      proof -
        have "S.iso (inv 𝖺[b, b, f])"
          using assms b f bf bb hom_connected(2) [of b "inv 𝖺[b, b, f]"] left_def
               iso_assocAWC iso_inv_iso iso_char S.arr_char left_def
          by simp 
        thus ?thesis       
          using unit_part assoc_in_hom isos_compose by blast
      qed
      show "«(ι ⋆ f) ⋅S inv 𝖺[b, b, f] : L (L f) ⇒S L f»"
        unfolding HL_def using unit_part assoc_in_hom by blast
    qed

    lemma lunit_char:
    assumes "S.ide f"
    shows "«𝗅[f] : L f ⇒S f»" and "L 𝗅[f] = (ι ⋆ f) ⋅S inv 𝖺[b, b, f]"
    and "∃!μ. «μ : L f ⇒S f» ∧ L μ = (ι ⋆ f) ⋅S inv 𝖺[b, b, f]"
    proof -
      let ?P = "λμ. «μ : L f ⇒S f» ∧ L μ = (ι ⋆ f) ⋅S inv 𝖺[b, b, f]"
      show "∃!μ. ?P μ"
      proof -
        have "∃μ. ?P μ"
        proof -
          have 1: "S.ide f"
            using assms S.ide_char S.arr_char by simp
          moreover have "S.ide (L f)"
            using 1 L.preserves_ide by simp
          ultimately show ?thesis
            using assms characteristic_iso(3) L.is_full by blast
        qed
        moreover have "∀μ μ'. ?P μ ∧ ?P μ' ⟶ μ = μ'"
        proof
          fix μ
          show "∀μ'. ?P μ ∧ ?P μ' ⟶ μ = μ'"
              using L.is_faithful [of μ] by fastforce
        qed
        ultimately show ?thesis by blast
      qed
      hence "?P (THE μ. ?P μ)"
        using theI' [of ?P] by fastforce
      hence 1: "?P 𝗅[f]"
        unfolding lunit_def by blast
      show "«𝗅[f] : L f ⇒S f»" using 1 by fast
      show "L 𝗅[f] = (ι ⋆ f) ⋅S inv 𝖺[b, b, f]" using 1 by fast
    qed

    lemma iso_lunit:
    assumes "S.ide f"
    shows "S.iso 𝗅[f]"
      using assms characteristic_iso(4) lunit_char L.reflects_iso by metis

    lemma lunit_eqI:
    assumes "«f : a ⇒S b»" and "«μ : L f ⇒S f»"
    and "L μ = ((ι ⋆ f) ⋅S inv 𝖺[b, b, f])"
    shows "μ = 𝗅[f]"
    proof -
      have "S.ide f" using assms(2) S.ide_cod by auto
      thus ?thesis using assms lunit_char [of f] by auto
    qed

    lemma lunit_naturality:
    assumes "S.arr μ"
    shows "𝗅[S.cod μ] ⋅S L μ = μ ⋅S 𝗅[S.dom μ]"
    proof -
      have 1: "«𝗅[S.cod μ] ⋅S L μ : L (S.dom μ) ⇒S S.cod μ»"
        using assms lunit_char(1) [of "S.cod μ"] S.ide_cod by blast
      have "S.par (𝗅[S.cod μ] ⋅S L μ) (μ ⋅S 𝗅[S.dom μ])"
      proof -
        have "«μ ⋅S 𝗅[S.dom μ] : L (S.dom μ) ⇒S S.cod μ»"
          using assms S.ide_dom lunit_char(1) by blast
        thus ?thesis using 1 by (elim S.in_homE, auto)
      qed
      moreover have "L (𝗅[S.cod μ] ⋅S L μ) = L (μ ⋅S 𝗅[S.dom μ])"
      proof -
        have 2: "«b ⋆ b ⋆ μ : b ⋆ b ⋆ S.dom μ ⇒S b ⋆ b ⋆ S.cod μ»"
          using assms weak_unit_b L.preserves_hom HL_def S.arr_iff_in_hom [of μ] S.arr_char
          by simp
        have 3: "«(b ⋆ b) ⋆ μ : (b ⋆ b) ⋆ S.dom μ ⇒S (b ⋆ b) ⋆ S.cod μ»"
          using assms weak_unit_b L.preserves_hom HL_def S.arr_iff_in_hom S.arr_char
          by (metis match_3 weak_unit_in_vhom weak_unit_self_left S.in_hom_char
              S.not_arr_null S.null_char right_hcomp_closed)

        have "L (𝗅[S.cod μ] ⋅S L μ) = L 𝗅[S.cod μ] ⋅S L (L μ)"
          using assms 1 L.preserves_comp_2 by blast
        also have "... = ((ι ⋆ S.cod μ) ⋅S inv 𝖺[b, b, S.cod μ]) ⋅S (b ⋆ b ⋆ μ)"
          using assms L.preserves_arr lunit_char S.ide_cod HL_def by auto
        also have "... = (ι ⋆ S.cod μ) ⋅S inv 𝖺[b, b, S.cod μ] ⋅S (b ⋆ b ⋆ μ)"
          using S.comp_assoc by auto
        also have "... = (ι ⋆ S.cod μ) ⋅S ((b ⋆ b) ⋆ μ) ⋅S inv 𝖺[b, b, S.dom μ]"
        proof -
          have "inv 𝖺[b, b, S.cod μ] ⋅S (b ⋆ b ⋆ μ) = ((b ⋆ b) ⋆ μ) ⋅S inv 𝖺[b, b, S.dom μ]"
          proof -
            have "((b ⋆ b) ⋆ μ) ⋅S inv 𝖺[b, b, S.dom μ] = ((b ⋆ b) ⋆ μ) ⋅ inv 𝖺[b, b, S.dom μ]"
              using assms 3 S.in_hom_char S.comp_char [of "(b ⋆ b) ⋆ μ" "inv 𝖺[b, b, S.dom μ]"]
              by (metis S.ide_dom characteristic_iso(1) ext)
            also have "... = inv 𝖺[b, b, S.cod μ] ⋅ (b ⋆ b ⋆ μ)"
            proof -
              have "b ⋆ μ ≠ null"
                using assms S.arr_char left_def by simp
              thus ?thesis
                using assms weak_unit_b assoc'_naturalityAWC [of b b μ] by fastforce
            qed
            also have "... = inv 𝖺[b, b, S.cod μ] ⋅S (b ⋆ b ⋆ μ)"
              using assms 2 S.in_hom_char S.comp_char
              by (metis S.comp_simp S.ide_cod S.seqI' characteristic_iso(1))
            finally show ?thesis by argo
          qed
         thus ?thesis by argo
        qed
        also have "... = ((ι ⋆ S.cod μ) ⋅S ((b ⋆ b) ⋆ μ)) ⋅S inv 𝖺[b, b, S.dom μ]"
          using S.comp_assoc by auto
        also have "... = ((b ⋆ μ) ⋅S (ι ⋆ S.dom μ)) ⋅S inv 𝖺[b, b, S.dom μ]"
        proof -
          have "(b ⋆ b) ⋆ μ ≠ null"
            using 3 S.not_arr_null by (elim S.in_homE, auto)
          moreover have "ι ⋆ S.dom μ ≠ null"
            using assms S.not_arr_null
            by (metis S.dom_char ι_in_hom calculation hom_connected(1-2) in_homE)
          ultimately have "(ι ⋆ S.cod μ) ⋅S ((b ⋆ b) ⋆ μ) = (b ⋆ μ) ⋅S (ι ⋆ S.dom μ)"
            using assms weak_unit_b iso_unit S.comp_arr_dom S.comp_cod_arr
                  interchange [of ι "b ⋆ b" "S.cod μ" μ ] interchange [of b ι μ "S.dom μ"]
            by auto
          thus ?thesis by argo
        qed
        also have "... = (b ⋆ μ) ⋅S (ι ⋆ S.dom μ) ⋅S inv 𝖺[b, b, S.dom μ]"
          using S.comp_assoc by auto
        also have "... = L μ ⋅S L 𝗅[S.dom μ]"
          using assms lunit_char(2) S.ide_dom HL_def by auto
        also have "... = L (μ ⋅S 𝗅[S.dom μ])"
          using assms S.arr_iff_in_hom [of μ] lunit_char(1) S.ide_dom S.seqI
          by fastforce
        finally show ?thesis by blast
      qed
      ultimately show "𝗅[S.cod μ] ⋅S L μ = μ ⋅S 𝗅[S.dom μ]"
        using L.is_faithful by blast
    qed

    abbreviation 𝔩
    where "𝔩 μ ≡ if S.arr μ then μ ⋅S 𝗅[S.dom μ] else null"

    interpretation 𝔩: natural_transformation S.comp S.comp L S.map 𝔩
    proof -
      interpret 𝔩: transformation_by_components S.comp S.comp L S.map lunit
        using lunit_char(1) lunit_naturality by (unfold_locales, simp_all)
      have "𝔩.map = 𝔩"
        using 𝔩.is_extensional 𝔩.map_def 𝔩.naturality 𝔩.map_simp_ide S.ide_dom S.ide_cod
              S.map_def
        by auto
      thus "natural_transformation S.comp S.comp L S.map 𝔩"
        using 𝔩.natural_transformation_axioms by auto
    qed

    lemma natural_transformation_𝔩:
    shows "natural_transformation S.comp S.comp L S.map 𝔩" ..

    interpretation 𝔩: natural_isomorphism S.comp S.comp L S.map 𝔩
      using S.ide_is_iso iso_lunit lunit_char(1) S.isos_compose
      by (unfold_locales, force)

    lemma natural_isomorphism_𝔩:
    shows "natural_isomorphism S.comp S.comp L S.map 𝔩" ..

    interpretation L: equivalence_functor S.comp S.comp L
      using natural_isomorphism_𝔩 L.isomorphic_to_identity_is_equivalence by blast

    lemma equivalence_functor_L:
    shows "equivalence_functor S.comp S.comp L"
      ..

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

  end

  subsection "Prebicategories"

  text ‹
    A \emph{prebicategory} is an associative weak composition satisfying the additional assumption
    that every arrow has a source and a target.
  ›

  locale prebicategory =
    associative_weak_composition +
  assumes arr_has_source: "arr μ ⟹ sources μ ≠ {}"
  and arr_has_target: "arr μ ⟹ targets μ ≠ {}"
  begin

    lemma arr_iff_has_src:
    shows "arr μ ⟷ sources μ ≠ {}"
      using arr_has_source composable_implies_arr by auto

    lemma arr_iff_has_trg:
    shows "arr μ ⟷ targets μ ≠ {}"
      using arr_has_target composable_implies_arr by auto

  end

  text ‹
    The horizontal composition of a prebicategory is regular.
  ›

  sublocale prebicategory  regular_weak_composition V H
  proof
    show "⋀a f. a ∈ sources f ⟹ ide f ⟹ f ⋆ a ≅ f"
    proof -
      fix a f
      assume a: "a ∈ sources f" and f: "ide f"
      interpret Right_a: subcategory V ‹right a›
        using a right_hom_is_subcategory weak_unit_self_composable by force
      interpret Right_a: right_hom_with_unit V H 𝖺 ‹some_unit a› a
        using a iso_some_unit by (unfold_locales, auto)
      show "f ⋆ a ≅ f"
      proof -
        have "Right_a.ide f"
          using a f Right_a.ide_char Right_a.arr_char right_def by auto
        hence "Right_a.iso (Right_a.runit f) ∧ (Right_a.runit f) ∈ Right_a.hom (f ⋆ a) f"
          using Right_a.iso_runit Right_a.runit_char(1) HR_def by simp
        hence "iso (Right_a.runit f) ∧ (Right_a.runit f) ∈ hom (f ⋆ a) f"
          using Right_a.iso_char Right_a.hom_char by auto
        thus ?thesis using f isomorphic_def by auto
      qed
    qed
    show "⋀b f. b ∈ targets f ⟹ ide f ⟹ b ⋆ f ≅ f"
    proof -
      fix b f
      assume b: "b ∈ targets f" and f: "ide f"
      interpret Left_b: subcategory V ‹left b›
        using b left_hom_is_subcategory weak_unit_self_composable by force
      interpret Left_b: left_hom_with_unit V H 𝖺 ‹some_unit b› b
        using b iso_some_unit by (unfold_locales, auto)
      show "b ⋆ f ≅ f"
      proof -
        have "Left_b.ide f"
          using b f Left_b.ide_char Left_b.arr_char left_def by auto
        hence "Left_b.iso (Left_b.lunit f) ∧ (Left_b.lunit f) ∈ Left_b.hom (b ⋆ f) f"
          using b f Left_b.iso_lunit Left_b.lunit_char(1) HL_def by simp
        hence "iso (Left_b.lunit f) ∧ (Left_b.lunit f) ∈ hom (b ⋆ f) f"
          using Left_b.iso_char Left_b.hom_char by auto
        thus ?thesis using isomorphic_def by auto
      qed
    qed
  qed

  text ‹
    The regularity allows us to show that, in a prebicategory, all sources of
    a given arrow are isomorphic, and similarly for targets.
  ›

  context prebicategory
  begin

    lemma sources_are_isomorphic:
    assumes "a ∈ sources μ" and "a' ∈ sources μ"
    shows "a ≅ a'"
    proof -
      have μ: "arr μ" using assms composable_implies_arr by auto
      have 0: "⋀f. ⟦ ide f; a ∈ sources f; a' ∈ sources f ⟧ ⟹ a ≅ a'"
      proof -
        fix f
        assume f: "ide f" and a: "a ∈ sources f" and a': "a' ∈ sources f"
        have 1: "a ⋆ a' ≠ null"
          using a a' f μ assms(1) sources_determine_composability sourcesD(2-3) by meson
        have 2: "a ∈ targets a' ∧ a' ∈ sources a"
          using assms 1 by blast
        show "a ≅ a'"
          using a a' 1 2 comp_ide_source comp_target_ide [of a a']
                weak_unit_self_composable(1) [of a] weak_unit_self_composable(1) [of a']
                isomorphic_transitive isomorphic_symmetric
          by blast
      qed
      have "ide (dom μ) ∧ a ∈ sources (dom μ) ∧ a' ∈ sources (dom μ)"
        using assms μ sources_dom by auto
      thus ?thesis using 0 by auto
    qed
      
    lemma targets_are_isomorphic:
    assumes "b ∈ targets μ" and "b' ∈ targets μ"
    shows "b ≅ b'"
    proof -
      have μ: "arr μ" using assms composable_implies_arr by auto
      have 0: "⋀f. ⟦ ide f; b ∈ targets f; b' ∈ targets f ⟧ ⟹ b ≅ b'"
      proof -
        fix f
        assume f: "ide f" and b: "b ∈ targets f" and b': "b' ∈ targets f"
        have 1: "b ⋆ b' ≠ null"
          using b b' f μ assms(1) targets_determine_composability targetsD(2-3) by meson
        have 2: "b ∈ targets b' ∧ b' ∈ sources b"
          using assms 1 by blast
        show "b ≅ b'"
          using b b' 1 2 comp_ide_source comp_target_ide [of b b']
                weak_unit_self_composable(1) [of b] weak_unit_self_composable(1) [of b']
                isomorphic_transitive isomorphic_symmetric
          by blast
      qed
      have "ide (dom μ) ∧ b ∈ targets (dom μ) ∧ b' ∈ targets (dom μ)"
        using assms μ targets_dom [of μ] by auto
      thus ?thesis using 0 by auto
    qed

    text ‹
      In fact, we now show that the sets of sources and targets of a 2-cell are
      isomorphism-closed, and hence are isomorphism classes.
      We first show that the notion ``weak unit'' is preserved under isomorphism.
    ›

    interpretation H: partial_magma H
      using is_partial_magma by auto

    lemma isomorphism_respects_weak_units:
    assumes "weak_unit a" and "a ≅ a'"
    shows "weak_unit a'"
    proof -
      obtain φ where φ: "iso φ ∧ «φ : a ⇒ a'»"
        using assms by auto
      interpret Left_a: subcategory V ‹left a›
        using assms left_hom_is_subcategory by fastforce
      interpret Left_a: left_hom_with_unit V H 𝖺 ‹some_unit a› a
        using assms iso_some_unit
        apply unfold_locales by auto
      interpret Right_a: subcategory V "right a"
        using assms right_hom_is_subcategory by fastforce
      interpret Right_a: right_hom_with_unit V H 𝖺 ‹some_unit a› a
        using assms iso_some_unit
        apply unfold_locales by auto
      have a': "ide a' ∧ a ⋆ a' ≠ null ∧ a' ⋆ a ≠ null ∧ a' ⋆ a' ≠ null ∧
                φ ⋆ a' ≠ null ∧ Left_a.ide a'"
        using assms φ weak_unit_self_composable hom_connected
              Left_a.ide_char Left_a.arr_char left_def
        apply auto
            apply (meson weak_unit_self_composable(3) isomorphic_implies_equicomposable)
           apply (meson weak_unit_self_composable(3) isomorphic_implies_equicomposable)
          apply (meson weak_unit_self_composable(3) isomorphic_implies_equicomposable)
         apply (metis weak_unit_self_composable(3) in_homE)
        by (meson weak_unit_self_composable(3) isomorphic_implies_equicomposable)
      have iso: "a' ⋆ a' ≅ a'"
      proof -
        have 1: "Right a' = Right a"
          using assms right_respects_isomorphic by simp
        interpret Right_a': subcategory V ‹right a'›
          using assms right_hom_is_subcategory by fastforce
        (* TODO: The previous interpretation brings in unwanted notation for in_hom. *)
        interpret Ra': endofunctor ‹Right a'› ‹HR a'›
          using assms a' endofunctor_HR by auto
        let  = "Left_a.lunit a' ⋅ inv (φ ⋆ a')"
        have "iso ?ψ ∧ «?ψ : a' ⋆ a' ⇒ a'»"
        proof -
          have "iso (Left_a.lunit a') ∧ «Left_a.lunit a' : a ⋆ a' ⇒ a'»"
            using a' Left_a.lunit_char(1) Left_a.iso_lunit Left_a.iso_char
                  Left_a.in_hom_char HL_def
            by auto
          moreover have "iso (φ ⋆ a') ∧ «φ ⋆ a' : a ⋆ a' ⇒ a' ⋆ a'»"
          proof -
            have 1: "Right_a'.iso φ ∧ φ ∈ Right_a'.hom (Right_a'.dom φ) (Right_a'.cod φ)"
              using a' φ Right_a'.iso_char Right_a'.arr_char right_def right_iff_right_inv
                    Right_a'.arr_iff_in_hom [of φ]
              by simp
            have "Right_a'.iso (HR a' φ) ∧
                  Right_a'.in_hom (HR a' φ) (HR a' (Right_a'.dom φ)) (HR a' (Right_a'.cod φ))"
              using φ 1 Ra'.preserves_iso Ra'.preserves_hom Right_a'.iso_char
                    Ra'.preserves_dom Ra'.preserves_cod Right_a'.arr_iff_in_hom [of "HR a' φ"]
              by simp
            thus ?thesis
              using φ 1 Right_a'.in_hom_char Right_a'.iso_char HR_def by auto
          qed
          ultimately show ?thesis
            using isos_compose iso_inv_iso inv_in_hom by blast
        qed
        thus ?thesis using isomorphic_def by auto
      qed
      text ‹
        We show that horizontal composition on the left and right by @{term a'}
        is naturally isomorphic to the identity functor.  This follows from the fact
        that if @{term a} is isomorphic to @{term a'}, then horizontal composition with @{term a}
        is naturally isomorphic to horizontal composition with @{term a'}, hence the latter is
        naturally isomorphic to the identity if the former is.
        This is conceptually simple, but there are tedious composability details to handle.
      ›  
      have 1: "Left a' = Left a ∧ Right a' = Right a"
        using assms left_respects_isomorphic right_respects_isomorphic by simp
      interpret L: fully_faithful_functor ‹Left a› ‹Left a› ‹HL a›
        using assms weak_unit_def by simp
      interpret L': endofunctor ‹Left a› ‹HL a'›
        using a' 1 endofunctor_HL [of a'] by auto
      interpret Φ: natural_isomorphism ‹Left a› ‹Left a› ‹HL a› ‹HL a'› ‹HL φ›
      proof
        fix μ
        show "¬ Left_a.arr μ ⟹ HL φ μ = Left_a.null"
          using left_def φ HL_def hom_connected(1) Left_a.null_char null_agreement
                Left_a.arr_char
          by auto
        assume "Left_a.arr μ"
        hence μ: "Left_a.arr μ ∧ arr μ ∧ a ⋆ μ ≠ null"
          using Left_a.arr_char left_def composable_implies_arr by simp
        have 2: "φ ⋆ μ ≠ null"
          using assms φ μ Left_a.arr_char left_def hom_connected by auto
        show "Left_a.dom (HL φ μ) = HL a (Left_a.dom μ)"
          using assms 2 φ μ Left_a.arr_char left_def hom_connected(2) [of a φ]
                weak_unit_self_composable match_4 Left_a.dom_char HL_def by auto
        show "Left_a.cod (HL φ μ) = HL a' (Left_a.cod μ)"
          using assms 2 φ μ Left_a.arr_char left_def hom_connected(2) [of a φ]
                weak_unit_self_composable match_4 Left_a.cod_char HL_def
          by auto
        show "Left_a.comp (HL a' μ) (HL φ (Left_a.dom μ)) = HL φ μ"
        proof -
          have "Left_a.comp (HL a' μ) (HL φ (Left_a.dom μ)) =
                Left_a.comp (a' ⋆ μ) (φ ⋆ dom μ)"
            using assms 1 2 φ μ Left_a.dom_char left_def HL_def by simp
          also have "... = (a' ⋆ μ) ⋅ (φ ⋆ dom μ)"
          proof -
            have "Left_a.seq (a' ⋆ μ) (φ ⋆ dom μ)"
            proof (intro Left_a.seqI)
              show 3: "Left_a.arr (φ ⋆ dom μ)"
                using assms 2 φ μ Left_a.arr_char left_def
                by (metis HL_def L'.preserves_arr hcomp_simpsWC(1) in_homE right_connected
                    paste_1)
              show 4: "Left_a.arr (a' ⋆ μ)"
                using μ HL_def L'.preserves_arr by auto
              show "Left_a.dom (a' ⋆ μ) = Left_a.cod (φ ⋆ dom μ)"
                using a' φ μ 2 3 4 Left_a.dom_char Left_a.cod_char
                by (metis Left_a.seqE Left_a.seq_char hcomp_simpsWC(1) in_homE paste_1)
            qed
            thus ?thesis using Left_a.comp_char Left_a.arr_char left_def by auto
          qed
          also have "... = a' ⋅ φ ⋆ μ ⋅ dom μ"
            using a' φ μ interchange hom_connected by auto
          also have "... = φ ⋆ μ"
            using φ μ comp_arr_dom comp_cod_arr by auto
          finally show ?thesis using HL_def by simp
        qed
        show "Left_a.comp (HL φ (Left_a.cod μ)) (Left_a.L μ) = HL φ μ"
        proof -
          have "Left_a.comp (HL φ (Left_a.cod μ)) (Left_a.L μ) = Left_a.comp (φ ⋆ cod μ) (a ⋆ μ)"
            using assms 1 2 φ μ Left_a.cod_char left_def HL_def by simp
          also have "... = (φ ⋆ cod μ) ⋅ (a ⋆ μ)"
          proof -
            have "Left_a.seq (φ ⋆ cod μ) (a ⋆ μ)"
            proof (intro Left_a.seqI)
              show 3: "Left_a.arr (φ ⋆ cod μ)"
                using φ μ 2 Left_a.arr_char left_def
                by (metis (no_types, lifting) HL_def L.preserves_arr hcomp_simpsWC(1)
                    in_homE right_connected paste_2)
              show 4: "Left_a.arr (a ⋆ μ)"
                using assms μ Left_a.arr_char left_def
                using HL_def L.preserves_arr by auto
              show "Left_a.dom (φ ⋆ cod μ) = Left_a.cod (a ⋆ μ)"
                using assms φ μ 2 3 4 Left_a.dom_char Left_a.cod_char
                by (metis Left_a.seqE Left_a.seq_char hcomp_simpsWC(1) in_homE paste_2)
            qed
            thus ?thesis using Left_a.comp_char Left_a.arr_char left_def by auto
          qed
          also have "... = φ ⋅ a ⋆ cod μ ⋅ μ"
            using φ μ interchange hom_connected by auto
          also have "... = φ ⋆ μ"
            using φ μ comp_arr_dom comp_cod_arr by auto
          finally show ?thesis using HL_def by simp
        qed
        next
        fix μ
        assume μ: "Left_a.ide μ"
        have 1: "φ ⋆ μ ≠ null"
          using assms φ μ Left_a.ide_char Left_a.arr_char left_def hom_connected by auto
        show "Left_a.iso (HL φ μ)"
        proof -
          have "iso (φ ⋆ μ)"
          proof -
            have "a ∈ sources φ ∩ targets μ"
              using assms φ μ 1 hom_connected weak_unit_self_composable
                    Left_a.ide_char Left_a.arr_char left_def connected_if_composable
              by auto
            thus ?thesis
              using φ μ Left_a.ide_char ide_is_iso iso_hcompRWC(1) by blast
          qed
          moreover have "left a (φ ⋆ μ)"
            using assms 1 φ weak_unit_self_composable hom_connected(2) [of a φ]
                  left_def match_4 null_agreement
            by auto
          ultimately show ?thesis
            using Left_a.iso_char Left_a.arr_char left_iff_left_inv Left_a.inv_char HL_def
            by simp
        qed
      qed
      interpret L': equivalence_functor ‹Left a'› ‹Left a'› ‹HL a'›
      proof -
        have "naturally_isomorphic (Left a) (Left a) (HL a) Left_a.map"
          using assms Left_a.natural_isomorphism_𝔩 naturally_isomorphic_def by blast
        moreover have "naturally_isomorphic (Left a) (Left a) (HL a) (HL a')"
          using naturally_isomorphic_def Φ.natural_isomorphism_axioms by blast
        ultimately have "naturally_isomorphic (Left a) (Left a) (HL a')
                                              (identity_functor.map (Left a))"
          using naturally_isomorphic_symmetric naturally_isomorphic_transitive by fast
        hence "naturally_isomorphic (Left a') (Left a') (HL a') (identity_functor.map (Left a'))"
          using 1 by auto
        thus "equivalence_functor (Left a') (Left a') (HL a')"
          using 1 L'.isomorphic_to_identity_is_equivalence naturally_isomorphic_def by fastforce
      qed

      text ‹
        Now we do the same for ‹R'›.
      ›
      interpret R: fully_faithful_functor ‹Right a› ‹Right a› ‹HR a›
        using assms weak_unit_def by simp
      interpret R': endofunctor ‹Right a› ‹HR a'›
        using a' 1 endofunctor_HR [of a'] by auto
      interpret Ψ: natural_isomorphism ‹Right a› ‹Right a› ‹HR a› ‹HR a'› ‹HR φ›
      proof
        fix μ
        show "¬ Right_a.arr μ ⟹ HR φ μ = Right_a.null"
          using right_def φ HR_def hom_connected Right_a.null_char Right_a.arr_char
          by auto
        assume "Right_a.arr μ"
        hence μ: "Right_a.arr μ ∧ arr μ ∧ μ ⋆ a ≠ null"
          using Right_a.arr_char right_def composable_implies_arr by simp
        have 2: "μ ⋆ φ ≠ null"
          using assms φ μ Right_a.arr_char right_def hom_connected by auto
        show "Right_a.dom (HR φ μ) = HR a (Right_a.dom μ)"
          using assms 2 φ μ Right_a.arr_char right_def hom_connected(1) [of φ a]
                weak_unit_self_composable match_3 Right_a.dom_char HR_def
          by auto
        show "Right_a.cod (HR φ μ) = HR a' (Right_a.cod μ)"
          using assms 2 a' φ μ Right_a.arr_char right_def hom_connected(3) [of φ a]
                weak_unit_self_composable match_3 Right_a.cod_char HR_def
          by auto
        show "Right_a.comp (HR a' μ) (HR φ (Right_a.dom μ)) = HR φ μ"
        proof -
          have "Right_a.comp (HR a' μ) (HR φ (Right_a.dom μ)) =
                Right_a.comp (μ ⋆ a') (dom μ ⋆ φ)"
            using assms 1 2 φ μ Right_a.dom_char right_def HR_def by simp
          also have "... = (μ ⋆ a') ⋅ (dom μ ⋆ φ)"
          proof -
            have "Right_a.seq (μ ⋆ a') (dom μ ⋆ φ)"
            proof (intro Right_a.seqI)
              show 3: "Right_a.arr (dom μ ⋆ φ)"
                using assms 2 φ μ Right_a.arr_char right_def
                by (metis HR_def R'.preserves_arr hcomp_simpsWC(1) in_homE left_connected
                          paste_2)
              show 4: "Right_a.arr (μ ⋆ a')"
                using μ HR_def R'.preserves_arr by auto
              show "Right_a.dom (μ ⋆ a') = Right_a.cod (dom μ ⋆ φ)"
                using a' φ μ 2 3 4 Right_a.dom_char Right_a.cod_char
                by (metis Right_a.seqE Right_a.seq_char hcomp_simpsWC(1) in_homE paste_2)
            qed
            thus ?thesis using Right_a.comp_char Right_a.arr_char right_def by auto
          qed
          also have "... = μ ⋅ dom μ ⋆ a' ⋅ φ"
            using a' φ μ interchange hom_connected by auto
          also have "... = μ ⋆ φ"
            using φ μ comp_arr_dom comp_cod_arr by auto
          finally show ?thesis using HR_def by simp
        qed
        show "Right_a.comp (HR φ (Right_a.cod μ)) (Right_a.R μ) = HR φ μ"
        proof -
          have "Right_a.comp (HR φ (Right_a.cod μ)) (Right_a.R μ)
                  = Right_a.comp (cod μ ⋆ φ) (μ ⋆ a)"
            using assms 1 2 φ μ Right_a.cod_char right_def HR_def by simp
          also have "... = (cod μ ⋆ φ) ⋅ (μ ⋆ a)"
          proof -
            have "Right_a.seq (cod μ ⋆ φ) (μ ⋆ a)"
            proof (intro Right_a.seqI)
              show 3: "Right_a.arr (cod μ ⋆ φ)"
                using φ μ 2 Right_a.arr_char right_def
                by (metis (no_types, lifting) HR_def R.preserves_arr hcomp_simpsWC(1)
                    in_homE left_connected paste_1)
              show 4: "Right_a.arr (μ ⋆ a)"
                using assms μ Right_a.arr_char right_def
                using HR_def R.preserves_arr by auto
              show "Right_a.dom (cod μ ⋆ φ) = Right_a.cod (μ ⋆ a)"
                using assms φ μ 2 3 4 Right_a.dom_char Right_a.cod_char
                by (metis Right_a.seqE Right_a.seq_char hcomp_simpsWC(1) in_homE paste_1)
            qed
            thus ?thesis using Right_a.comp_char Right_a.arr_char right_def by auto
          qed
          also have "... = cod μ ⋅ μ ⋆ φ ⋅ a"
            using φ μ interchange hom_connected by auto
          also have "... = μ ⋆ φ"
            using φ μ comp_arr_dom comp_cod_arr by auto
          finally show ?thesis using HR_def by simp
        qed
        next
        fix μ
        assume μ: "Right_a.ide μ"
        have 1: "μ ⋆ φ ≠ null"
          using assms φ μ Right_a.ide_char Right_a.arr_char right_def hom_connected by auto
        show "Right_a.iso (HR φ μ)"
        proof -
          have "iso (μ ⋆ φ)"
          proof -
            have "a ∈ targets φ ∩ sources μ"
              using assms φ μ 1 hom_connected weak_unit_self_composable
                    Right_a.ide_char Right_a.arr_char right_def connected_if_composable
              by (metis (full_types) IntI targetsI)
            thus ?thesis
              using φ μ Right_a.ide_char ide_is_iso iso_hcompRWC(1) by blast
          qed
          moreover have "right a (μ ⋆ φ)"
            using assms 1 φ weak_unit_self_composable hom_connected(1) [of φ a]
                  right_def match_3 null_agreement
            by auto
          ultimately show ?thesis
            using Right_a.iso_char Right_a.arr_char right_iff_right_inv
                  Right_a.inv_char HR_def
            by simp
        qed
      qed
      interpret R': equivalence_functor ‹Right a'› ‹Right a'› ‹HR a'›
      proof -
        have "naturally_isomorphic (Right a) (Right a) (HR a) Right_a.map"
          using assms Right_a.natural_isomorphism_𝔯 naturally_isomorphic_def by blast
        moreover have "naturally_isomorphic (Right a) (Right a) (HR a) (HR a')"
          using naturally_isomorphic_def Ψ.natural_isomorphism_axioms by blast
        ultimately have "naturally_isomorphic (Right a) (Right a) (HR a') Right_a.map"
          using naturally_isomorphic_symmetric naturally_isomorphic_transitive by fast
        hence "naturally_isomorphic (Right a') (Right a') (HR a') 
                 (identity_functor.map (Right a'))"
          using 1 by auto
        thus "equivalence_functor (Right a') (Right a') (HR a')"
          using 1 R'.isomorphic_to_identity_is_equivalence naturally_isomorphic_def
          by fastforce
      qed

      show "weak_unit a'"
        using weak_unit_def iso L'.fully_faithful_functor_axioms R'.fully_faithful_functor_axioms
        by blast
    qed

    lemma sources_iso_closed:
    assumes "a ∈ sources μ" and "a ≅ a'"
    shows "a' ∈ sources μ"
      using assms isomorphism_respects_weak_units isomorphic_implies_equicomposable
      by blast

    lemma targets_iso_closed:
    assumes "a ∈ targets μ" and "a ≅ a'"
    shows "a' ∈ targets μ"
      using assms isomorphism_respects_weak_units isomorphic_implies_equicomposable
      by blast

    lemma sources_eqI:
    assumes "sources μ ∩ sources ν ≠ {}"
    shows "sources μ = sources ν"
      using assms sources_iso_closed sources_are_isomorphic by blast

    lemma targets_eqI:
    assumes "targets μ ∩ targets ν ≠ {}"
    shows "targets μ = targets ν"
      using assms targets_iso_closed targets_are_isomorphic by blast

    text ‹
      The sets of sources and targets of a weak unit are isomorphism classes.
    ›

    lemma sources_char:
    assumes "weak_unit a"
    shows "sources a = {x. x ≅ a}"
      using assms sources_iso_closed weak_unit_iff_self_source sources_are_isomorphic
            isomorphic_symmetric
      by blast

    lemma targets_char:
    assumes "weak_unit a"
    shows "targets a = {x. x ≅ a}"
      using assms targets_iso_closed weak_unit_iff_self_target targets_are_isomorphic
            isomorphic_symmetric
      by blast

  end

  section "Horizontal Homs"

  text ‹
    Here we define a locale that axiomatizes a (vertical) category ‹V› that has been
    punctuated into ``horizontal homs'' by the choice of idempotent endofunctors ‹src› and ‹trg›
    that assign a specific ``source'' and ``target'' 1-cell to each of its arrows.
    The functors ‹src› and ‹trg› are also subject to further conditions that constrain how
    they commute with each other.
  ›

  locale horizontal_homs =
    category V +
    src: endofunctor V src +
    trg: endofunctor V trg
  for V :: "'a comp"      (infixr "⋅" 55)
  and src :: "'a ⇒ 'a"
  and trg :: "'a ⇒ 'a" +
  assumes ide_src [simp]: "arr μ ⟹ ide (src μ)"
  and ide_trg [simp]: "arr μ ⟹ ide (trg μ)"
  and src_src [simp]: "arr μ ⟹ src (src μ) = src μ"
  and trg_trg [simp]: "arr μ ⟹ trg (trg μ) = trg μ"
  and trg_src [simp]: "arr μ ⟹ trg (src μ) = src μ"
  and src_trg [simp]: "arr μ ⟹ src (trg μ) = trg μ"
  begin

    no_notation in_hom        ("«_ : _ → _»")
    notation in_hom           ("«_ : _ ⇒ _»")

    text ‹
      We define an \emph{object} to be an arrow that is its own source
      (or equivalently, its own target).
    ›

    definition obj
    where "obj a ≡ arr a ∧ src a = a"

    lemma obj_def':
    shows "obj a ⟷ arr a ∧ trg a = a"
      using trg_src src_trg obj_def by metis

    lemma objE [elim]:
    assumes "obj a" and "⟦ ide a; src a = a; trg a = a ⟧ ⟹ T"
    shows T
    proof -
      have "ide a" using assms obj_def ide_src by metis
      moreover have "src a = a" using assms obj_def by simp
      moreover have "trg a = a" using assms obj_def' by simp
      ultimately show ?thesis using assms by simp
    qed

    (* TODO: Can't add "arr a" or "ide a" due to looping. *)
    lemma obj_simps (* [simp] *):
    assumes "obj a"
    shows "src a = a" and "trg a = a"
      using assms by auto

    lemma obj_src [intro, simp]:
    assumes "arr μ"
    shows "obj (src μ)"
      using assms obj_def by auto

    lemma obj_trg [intro, simp]:
    assumes "arr μ"
    shows "obj (trg μ)"
      using assms obj_def by auto

    definition in_hhom  ("«_ : _ → _»")
    where "in_hhom μ a b ≡ arr μ ∧ src μ = a ∧ trg μ = b"

    abbreviation hhom
    where "hhom a b ≡ {μ. «μ : a → b»}"

    abbreviation (input) hseqHH
    where "hseqHH ≡ λμ ν. arr μ ∧ arr ν ∧ src μ = trg ν"

    lemma in_hhomI [intro, simp]:
    assumes "arr μ" and "src μ = a" and "trg μ = b"
    shows "«μ : a → b»"
      using assms in_hhom_def by auto

    lemma in_hhomE [elim]:
    assumes "«μ : a → b»"
    and "⟦ arr μ; obj a; obj b; src μ = a; trg μ = b ⟧ ⟹ T"
    shows "T"
      using assms in_hhom_def by auto

    (*
     * TODO: I tried removing the second assertion here, thinking that it should already
     * be covered by the category locale, but in fact it breaks some proofs in
     * SpanBicategory that ought to be trivial.  So it seems that the presence of
     * this introduction rule adds something, and I should consider whether this rule
     * should be added to the category locale.
     *)
    lemma ide_in_hom [intro]:
    assumes "ide f"
    shows "«f : src f → trg f»" and "«f : f ⇒ f»"
      using assms by auto

    lemma src_dom [simp]:
    assumes "arr μ"
    shows "src (dom μ) = src μ"
      using assms src.preserves_dom [of μ] by simp

    lemma src_cod [simp]:
    assumes "arr μ"
    shows "src (cod μ) = src μ"
      using assms src.preserves_cod [of μ] by simp

    lemma trg_dom [simp]:
    assumes "arr μ"
    shows "trg (dom μ) = trg μ"
      using assms trg.preserves_dom [of μ] by simp

    lemma trg_cod [simp]:
    assumes "arr μ"
    shows "trg (cod μ) = trg μ"
      using assms trg.preserves_cod [of μ] by simp

    (*
     * TODO: In theory, the following simps should already be available from the fact
     * that src and trg are endofunctors.  But they seem not to get used.
     *)
    lemma dom_src [simp]:
    assumes "arr μ"
    shows "dom (src μ) = src μ"
      using assms by simp

    lemma cod_src [simp]:
    assumes "arr μ"
    shows "cod (src μ) = src μ"
      using assms by simp

    lemma dom_trg [simp]:
    assumes "arr μ"
    shows "dom (trg μ) = trg μ"
      using assms by simp

    lemma cod_trg [simp]:
    assumes "arr μ"
    shows "cod (trg μ) = trg μ"
      using assms by simp

    lemma vcomp_in_hhom [intro, simp]:
    assumes "seq ν μ" and "src ν = a" and "trg ν = b"
    shows "«ν ⋅ μ : a → b»"
      using assms src_cod [of "ν ⋅ μ"] trg_cod [of "ν ⋅ μ"] by auto

    lemma src_vcomp [simp]:
    assumes "seq ν μ"
    shows "src (ν ⋅ μ) = src ν"
      using assms src_cod [of "ν ⋅ μ"] by auto

    lemma trg_vcomp [simp]:
    assumes "seq ν μ"
    shows "trg (ν ⋅ μ) = trg ν"
      using assms trg_cod [of "ν ⋅ μ"] by auto

    lemma vseq_implies_hpar:
    assumes "seq ν μ"
    shows "src ν = src μ" and "trg ν = trg μ"
      using assms src_dom [of "ν ⋅ μ"] trg_dom [of "ν ⋅ μ"] src_cod [of "ν ⋅ μ"]
            trg_cod [of "ν ⋅ μ"]
      by auto

    lemma vconn_implies_hpar:
    assumes "«μ : f ⇒ g»"
    shows "src μ = src f" and "trg μ = trg f" and "src g = src f" and "trg g = trg f"
      using assms by auto

    lemma src_inv [simp]:
    assumes "iso μ"
    shows "src (inv μ) = src μ"
      using assms inv_in_hom iso_is_arr src_dom src_cod iso_inv_iso dom_inv by metis

    lemma trg_inv [simp]:
    assumes "iso μ"
    shows "trg (inv μ) = trg μ"
      using assms inv_in_hom iso_is_arr trg_dom trg_cod iso_inv_iso cod_inv by metis

    lemma inv_in_hhom [intro, simp]:
    assumes "iso μ" and "src μ = a" and "trg μ = b"
    shows "«inv μ : a → b»"
      using assms iso_is_arr by simp

    lemma hhom_is_subcategory:
    shows "subcategory V (λμ. «μ : a → b»)"
      using src_dom trg_dom src_cod trg_cod by (unfold_locales, auto)

    lemma isomorphic_objects_are_equal:
    assumes "obj a" and "obj b" and "a ≅ b"
    shows "a = b"
      using assms isomorphic_def
      by (metis arr_inv dom_inv in_homE objE src_dom src_inv)


    text ‹
      Having the functors ‹src› and ‹trg› allows us to form categories VV and VVV
      of formally horizontally composable pairs and triples of arrows.
    ›

    interpretation VxV: product_category V V ..
    interpretation VV: subcategory VxV.comp ‹λμν. hseqHH (fst μν) (snd μν)›
      by (unfold_locales, auto)

    lemma subcategory_VV:
    shows "subcategory VxV.comp (λμν. hseqHH (fst μν) (snd μν))"
      ..

    interpretation VxVxV: product_category V VxV.comp ..
    interpretation VVV: subcategory VxVxV.comp
                            ‹λτμν. arr (fst τμν) ∧ VV.arr (snd τμν) ∧
                                   src (fst τμν) = trg (fst (snd τμν))›
      using VV.arr_char
      by (unfold_locales, auto)

    lemma subcategory_VVV:
    shows "subcategory VxVxV.comp
             (λτμν. arr (fst τμν) ∧ VV.arr (snd τμν) ∧
                    src (fst τμν) = trg (fst (snd τμν)))"
      ..

  end

  subsection "Prebicategories with Homs"

  text ‹
    A \emph{weak composition with homs} consists of a weak composition that is
    equipped with horizontal homs in such a way that the chosen source and
    target of each 2-cell ‹μ› in fact lie in the set of sources and targets,
    respectively, of ‹μ›, such that horizontal composition respects the
    chosen sources and targets, and such that if 2-cells ‹μ› and ‹ν› are
    horizontally composable, then the chosen target of ‹μ› coincides with
    the chosen source of ‹ν›.
  ›

  locale weak_composition_with_homs =
    weak_composition +
    horizontal_homs +
  assumes src_in_sources: "arr μ ⟹ src μ ∈ sources μ"
  and trg_in_targets: "arr μ ⟹ trg μ ∈ targets μ"
  and src_hcomp': "ν ⋆ μ ≠ null ⟹ src (ν ⋆ μ) = src μ"
  and trg_hcomp': "ν ⋆ μ ≠ null ⟹ trg (ν ⋆ μ) = trg ν"
  and seq_if_composable: "ν ⋆ μ ≠ null ⟹ src ν = trg μ"

  locale prebicategory_with_homs =
    prebicategory +
    weak_composition_with_homs
  begin

    lemma composable_charPBH:
    shows "ν ⋆ μ ≠ null ⟷ arr μ ∧ arr ν ∧ src ν = trg μ"
    proof
      show "arr μ ∧ arr ν ∧ src ν = trg μ ⟹ ν ⋆ μ ≠ null"
        using trg_in_targets src_in_sources composable_if_connected
        by (metis sourcesD(3) targets_determine_composability)
      show "ν ⋆ μ ≠ null ⟹ arr μ ∧ arr ν ∧ src ν = trg μ"
        using seq_if_composable composable_implies_arr by auto
    qed

    lemma hcomp_in_homPBH:
    assumes "«μ : a →WC b»" and "«ν : b →WC c»"
    shows "«ν ⋆ μ : a →WC c»"
    and "«ν ⋆ μ : dom ν ⋆ dom μ ⇒ cod ν ⋆ cod μ»"
    proof -
      show "«ν ⋆ μ : a →WC c»"
        using assms sources_determine_composability sources_hcomp targets_hcomp by auto
      thus "«ν ⋆ μ : dom ν ⋆ dom μ ⇒ cod ν ⋆ cod μ»"
        using assms by auto
    qed

    text ‹
      In a prebicategory with homs, if ‹a› is an object (i.e. ‹src a = a› and ‹trg a = a›),
      then ‹a› is a weak unit.  The converse need not hold: there can be weak units that the
      ‹src› and ‹trg› mappings send to other 1-cells in the same isomorphism class.
    ›

    lemma obj_is_weak_unit:
    assumes "obj a"
    shows "weak_unit a"
    proof -
      have "a ∈ sources a"
        using assms objE src_in_sources ideD(1) by metis
      thus ?thesis by auto
    qed

  end

  subsection "Choosing Homs"

  text ‹
    Every prebicategory extends to a prebicategory with homs, by choosing an arbitrary
    representative of each isomorphism class of weak units to serve as an object.
    ``The source'' of a 2-cell is defined to be the chosen representative of the set of
     all its sources (which is an isomorphism class), and similarly for ``the target''.
  ›

  context prebicategory
  begin

    definition rep
    where "rep f ≡ SOME f'. f' ∈ { f'. f ≅ f' }"

    definition some_src
    where "some_src μ ≡ if arr μ then rep (SOME a. a ∈ sources μ) else null"

    definition some_trg
    where "some_trg μ ≡ if arr μ then rep (SOME b. b ∈ targets μ) else null"

    lemma isomorphic_ide_rep:
    assumes "ide f"
    shows "f ≅ rep f"
    proof -
      have "∃f'. f' ∈ { f'. f ≅ f' }"
        using assms isomorphic_reflexive by blast
      thus ?thesis using rep_def someI_ex by simp
    qed

    lemma rep_rep:
    assumes "ide f"
    shows "rep (rep f) = rep f"
    proof -
      have "rep f ∈ { f'. f ≅ f' }"
        using assms isomorphic_ide_rep by simp
      have "{ f'. f ≅ f' } = { f'. rep f ≅ f' }"
      proof -
        have "⋀f'. f ≅ f' ⟷ rep f ≅ f'"
        proof
          fix f'
          assume f': "f ≅ f'"
          show "rep f ≅ f'"
          proof -
            obtain φ where φ: "φ ∈ hom f f' ∧ iso φ"
              using f' by auto
            obtain ψ where ψ: "ψ ∈ hom f (rep f) ∧ iso ψ"
              using assms isomorphic_ide_rep by blast
            have "inv ψ ∈ hom (rep f) f ∧ iso (inv ψ)"
              using ψ iso_inv_iso inv_in_hom by simp
            hence "iso (V φ (inv ψ)) ∧ V φ (inv ψ) ∈ hom (rep f) f'"
              using φ isos_compose by auto
            thus ?thesis using isomorphic_def by auto
          qed
          next
          fix f'
          assume f': "rep f ≅ f'"
          show "f ≅ f'"
            using assms f' isomorphic_ide_rep isos_compose isomorphic_def by blast
        qed
        thus ?thesis by auto
      qed
      hence "rep (rep f) = (SOME f'. f' ∈ { f'. f ≅ f' })"
        using assms rep_def by fastforce
      also have "... = rep f"
        using assms rep_def by simp
      finally show ?thesis by simp
    qed

    lemma some_src_in_sources:
    assumes "arr μ"
    shows "some_src μ ∈ sources μ"
    proof -
      have 1: "(SOME a. a ∈ sources μ) ∈ sources μ"
        using assms arr_iff_has_src someI_ex [of "λa. a ∈ sources μ"] by blast
      moreover have "ide (SOME a. a ∈ sources μ)"
        using 1 weak_unit_self_composable by auto
      ultimately show ?thesis
        using assms 1 some_src_def
              sources_iso_closed [of "SOME a. a ∈ sources μ" μ]
              isomorphic_ide_rep [of "SOME a. a ∈ sources μ"]
        by metis
    qed

    lemma some_trg_in_targets:
    assumes "arr μ"
    shows "some_trg μ ∈ targets μ"
    proof -
      have 1: "(SOME a. a ∈ targets μ) ∈ targets μ"
        using assms arr_iff_has_trg someI_ex [of "λa. a ∈ targets μ"] by blast
      moreover have "ide (SOME a. a ∈ targets μ)"
        using 1 weak_unit_self_composable by auto
      ultimately show ?thesis
        using assms 1 some_trg_def
              targets_iso_closed [of "SOME a. a ∈ targets μ" μ]
              isomorphic_ide_rep [of "SOME a. a ∈ targets μ"]
        by presburger
    qed

    lemma some_src_dom:
    assumes "arr μ"
    shows "some_src (dom μ) = some_src μ"
      using assms some_src_def sources_dom by simp

    lemma some_src_cod:
    assumes "arr μ"
    shows "some_src (cod μ) = some_src μ"
      using assms some_src_def sources_cod by simp

    lemma some_trg_dom:
    assumes "arr μ"
    shows "some_trg (dom μ) = some_trg μ"
      using assms some_trg_def targets_dom by simp

    lemma some_trg_cod:
    assumes "arr μ"
    shows "some_trg (cod μ) = some_trg μ"
      using assms some_trg_def targets_cod by simp

    lemma ide_some_src:
    assumes "arr μ"
    shows "ide (some_src μ)"
      using assms some_src_in_sources weak_unit_self_composable by blast

    lemma ide_some_trg:
    assumes "arr μ"
    shows "ide (some_trg μ)"
      using assms some_trg_in_targets weak_unit_self_composable by blast

    lemma some_src_composable:
    assumes "arr τ"
    shows "τ ⋆ μ ≠ null ⟷ some_src τ ⋆ μ ≠ null"
      using assms some_src_in_sources sources_determine_composability by blast

    lemma some_trg_composable:
    assumes "arr σ"
    shows "μ ⋆ σ ≠ null ⟷ μ ⋆ some_trg σ ≠ null"
      using assms some_trg_in_targets targets_determine_composability by blast

    lemma sources_some_src:
    assumes "arr μ"
    shows "sources (some_src μ) = sources μ"
      using assms sources_determine_composability some_src_in_sources by blast

    lemma targets_some_trg:
    assumes "arr μ"
    shows "targets (some_trg μ) = targets μ"
      using assms targets_determine_composability some_trg_in_targets by blast

    lemma src_some_src:
    assumes "arr μ"
    shows "some_src (some_src μ) = some_src μ"
      using assms some_src_def ide_some_src sources_some_src by force

    lemma trg_some_trg:
    assumes "arr μ"
    shows "some_trg (some_trg μ) = some_trg μ"
      using assms some_trg_def ide_some_trg targets_some_trg by force

    lemma sources_char':
    assumes "arr μ"
    shows "a ∈ sources μ ⟷ some_src μ ≅ a"
      using assms some_src_in_sources sources_iso_closed sources_are_isomorphic by meson

    lemma targets_char':
    assumes "arr μ"
    shows "a ∈ targets μ ⟷ some_trg μ ≅ a"
      using assms some_trg_in_targets targets_iso_closed targets_are_isomorphic by blast

    text ‹
      An arbitrary choice of sources and targets in a prebicategory results in a notion of
      formal composability that coincides with the actual horizontal composability
      of the prebicategory.
    ›

    lemma composable_charPB:
    shows "τ ⋆ σ ≠ null ⟷ arr σ ∧ arr τ ∧ some_src τ = some_trg σ"
    proof
        assume στ: "τ ⋆ σ ≠ null"
        show "arr σ ∧ arr τ ∧ some_src τ = some_trg σ"
          using στ composable_implies_arr connected_if_composable some_src_def some_trg_def
          by force
        next
        assume στ: "arr σ ∧ arr τ ∧ some_src τ = some_trg σ"
        show "τ ⋆ σ ≠ null"
          using στ some_src_in_sources some_trg_composable by force
    qed

    text ‹
      A 1-cell is its own source if and only if it is its own target.
    ›

    lemma self_src_iff_self_trg:
    assumes "ide a"
    shows "a = some_src a ⟷ a = some_trg a"
    proof
      assume a: "a = some_src a"
      have "weak_unit a ∧ a ⋆ a ≠ null"
        using assms a some_src_in_sources [of a] by force
      thus "a = some_trg a" using a composable_charPB by simp
      next
      assume a: "a = some_trg a"
      have "weak_unit a ∧ a ⋆ a ≠ null"
        using assms a some_trg_in_targets [of a] by force
      thus "a = some_src a" using a composable_charPB by simp
    qed

    lemma some_trg_some_src:
    assumes "arr μ"
    shows "some_trg (some_src μ) = some_src μ"
      using assms ide_some_src some_src_def some_trg_def some_src_in_sources sources_char
            targets_char sources_some_src
      by force

    lemma src_some_trg:
    assumes "arr μ"
    shows "some_src (some_trg μ) = some_trg μ"
      using assms ide_some_trg some_src_def some_trg_def some_trg_in_targets sources_char
            targets_char targets_some_trg
      by force

    lemma some_src_eqI:
    assumes "a ∈ sources μ" and "some_src a = a"
    shows "some_src μ = a"
    proof -
      have 1: "arr μ ∧ arr a" using assms composable_implies_arr by auto
      have "some_src μ = rep (SOME x. x ∈ sources μ)"
        using assms 1 some_src_def by simp
      also have "... = rep (SOME x. some_src μ ≅ x)"
        using assms 1 sources_char' by simp
      also have "... = rep (SOME x. some_src a ≅ x)"
        using assms 1 some_src_in_sources sources_are_isomorphic
              isomorphic_symmetric isomorphic_transitive
        by metis
      also have "... = rep (SOME x. x ∈ sources a)"
        using assms 1 sources_char' by auto
      also have "... = some_src a"
        using assms 1 some_src_def by simp
      also have "... = a"
        using assms by auto
      finally show ?thesis by simp
    qed

    lemma some_trg_eqI:
    assumes "b ∈ targets μ" and "some_trg b = b"
    shows "some_trg μ = b"
    proof -
      have 1: "arr μ ∧ arr b" using assms composable_implies_arr by auto
      have "some_trg μ = rep (SOME x. x ∈ targets μ)"
        using assms 1 some_trg_def by simp
      also have "... = rep (SOME x. some_trg μ ≅ x)"
        using assms 1 targets_char' by simp
      also have "... = rep (SOME x. some_trg b ≅ x)"
        using assms 1 some_trg_in_targets targets_are_isomorphic
              isomorphic_symmetric isomorphic_transitive
        by metis
      also have "... = rep (SOME x. x ∈ targets b)"
        using assms 1 targets_char' by auto
      also have "... = some_trg b"
        using assms 1 some_trg_def by simp
      also have "... = b"
        using assms by auto
      finally show ?thesis by simp
    qed

    lemma some_src_comp:
    assumes "τ ⋆ σ ≠ null"
    shows "some_src (τ ⋆ σ) = some_src σ"
    proof (intro some_src_eqI [of "some_src σ" "τ ⋆ σ"])
      show "some_src (some_src σ) = some_src σ"
        using assms src_some_src composable_implies_arr by simp
      show "some_src σ ∈ sources (H τ σ)"
        using assms some_src_in_sources composable_charPB match_3 [of σ "some_src σ"]
        by (simp add: sources_hcomp)
    qed

    lemma some_trg_comp:
    assumes "τ ⋆ σ ≠ null"
    shows "some_trg (τ ⋆ σ) = some_trg τ"
    proof (intro some_trg_eqI [of "some_trg τ" "τ ⋆ σ"])
      show "some_trg (some_trg τ) = some_trg τ"
        using assms trg_some_trg composable_implies_arr by simp
      show "some_trg τ ∈ targets (H τ σ)"
        using assms some_trg_in_targets composable_charPB match_4 [of τ σ "some_trg τ"]
        by (simp add: targets_hcomp)
    qed

    text ‹
      The mappings that take an arrow to its chosen source or target are endofunctors
      of the vertical category, which commute with each other in the manner required
      for horizontal homs.
    ›

    interpretation S: endofunctor V some_src
      apply unfold_locales
           using some_src_def apply simp
          using ide_some_src apply simp
        using some_src_dom ide_some_src apply simp
       using some_src_cod ide_some_src apply simp
    proof -
      fix ν μ
      assume μν: "seq ν μ"
      show "some_src (ν ⋅ μ) = some_src ν ⋅ some_src μ"
        using μν some_src_dom [of "ν ⋅ μ"] some_src_dom some_src_cod [of "ν ⋅ μ"]
              some_src_cod ide_some_src
        by auto
    qed

    interpretation T: endofunctor V some_trg
      apply unfold_locales
          using some_trg_def apply simp
         using ide_some_trg apply simp
        using some_trg_dom ide_some_trg apply simp
       using some_trg_cod ide_some_trg apply simp
    proof -
      fix ν μ
      assume μν: "seq ν μ"
      show "some_trg (ν ⋅ μ) = some_trg ν ⋅ some_trg μ"
        using μν some_trg_dom [of "ν ⋅ μ"] some_trg_dom some_trg_cod [of "ν ⋅ μ"]
              some_trg_cod ide_some_trg
        by auto
    qed

    interpretation weak_composition_with_homs V H some_src some_trg
      apply unfold_locales
      using some_src_in_sources some_trg_in_targets
            src_some_src trg_some_trg src_some_trg some_trg_some_src
            some_src_comp some_trg_comp composable_charPB ide_some_src ide_some_trg
      by simp_all

    proposition extends_to_weak_composition_with_homs:
    shows "weak_composition_with_homs V H some_src some_trg"
      ..

    proposition extends_to_prebicategory_with_homs:
    shows "prebicategory_with_homs V H 𝖺 some_src some_trg"
      ..

  end

  subsection "Choosing Units"

  text ‹
    A \emph{prebicategory with units} is a prebicategory equipped with a choice,
    for each weak unit ‹a›, of a ``unit isomorphism'' ‹«𝗂[a] : a ⋆ a ⇒ a»›.
  ›

  locale prebicategory_with_units =
    prebicategory V H 𝖺 +
    weak_composition V H
  for V :: "'a comp"                  (infixr "⋅" 55)
  and H :: "'a comp"                  (infixr "⋆" 53)
  and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a"      ("𝖺[_, _, _]")
  and 𝗂 :: "'a ⇒ 'a"                  ("𝗂[_]") +
  assumes unit_in_vhomPBU: "weak_unit a ⟹ «𝗂[a] : a ⋆ a ⇒ a»"
  and iso_unitPBU: "weak_unit a ⟹ iso 𝗂[a]"
  begin

    lemma unit_in_homPBU:
    assumes "weak_unit a"
    shows "«𝗂[a] : a →WC a»" and "«𝗂[a] : a ⋆ a ⇒ a»"
    proof -
      show 1: "«𝗂[a] : a ⋆ a ⇒ a»"
        using assms unit_in_vhomPBU by auto
      show "«𝗂[a] : a →WC a»"
        using assms 1 weak_unit_iff_self_source weak_unit_iff_self_target
              sources_cod [of "𝗂[a]"] targets_cod [of "𝗂[a]"]
        by (elim in_homE, auto)
    qed

    lemma unit_simps [simp]:
    assumes "weak_unit a"
    shows "arr 𝗂[a]" and "dom 𝗂[a] = a ⋆ a" and "cod 𝗂[a] = a"
      using assms unit_in_vhomPBU by auto

  end

  text ‹
    Every prebicategory extends to a prebicategory with units, simply by choosing the
    unit isomorphisms arbitrarily.
  ›

  context prebicategory
  begin

    proposition extends_to_prebicategory_with_units:
    shows "prebicategory_with_units V H 𝖺 some_unit"
      using iso_some_unit by (unfold_locales, auto)

  end

  subsection "Horizontal Composition"

  text ‹
    The following locale axiomatizes a (vertical) category ‹V› with horizontal homs,
    which in addition has been equipped with a functorial operation ‹H› of
    horizontal composition from ‹VV› to ‹V›, assumed to preserve source and target.
  ›

  locale horizontal_composition =
    horizontal_homs V src trg +
    VxV: product_category V V +
    VV: subcategory VxV.comp ‹λμν. hseqHH (fst μν) (snd μν)› +
    H: "functor" VV.comp V ‹λμν. H (fst μν) (snd μν)›
  for V :: "'a comp"          (infixr "⋅" 55)
  and H :: "'a ⇒ 'a ⇒ 'a"   (infixr "⋆" 53)
  and src :: "'a ⇒ 'a"
  and trg :: "'a ⇒ 'a" +
  assumes src_hcomp: "arr (μ ⋆ ν) ⟹ src (μ ⋆ ν) = src ν"
  and trg_hcomp: "arr (μ ⋆ ν) ⟹ trg (μ ⋆ ν) = trg μ"
  begin
    (* TODO: Why does this get re-introduced? *)
    no_notation in_hom        ("«_ : _ → _»")

    text ‹
      ‹H› is a partial magma, which shares its null with ‹V›.
    ›

    lemma is_partial_magma:
    shows "partial_magma H" and "partial_magma.null H = null"
    proof -
      have 1: "∀f. null ⋆ f = null ∧ f ⋆ null = null"
        using H.is_extensional VV.arr_char not_arr_null by auto
      interpret H: partial_magma H
      proof
        show "∃!n. ∀f. n ⋆ f = n ∧ f ⋆ n = n"
        proof
          show "∀f. null ⋆ f = null ∧ f ⋆ null = null" by fact
          show "⋀n. ∀f. n ⋆ f = n ∧ f ⋆ n = n ⟹ n = null"
            using 1 VV.arr_char H.is_extensional not_arr_null by metis
        qed
      qed
      show "partial_magma H" ..
      show "H.null = null"
        using 1 H.null_def the1_equality [of "λn. ∀f. n ⋆ f = n ∧ f ⋆ n = n"]
        by metis
    qed

    text ‹
      \textbf{Note:} The following is ``almost'' ‹H.seq›, but for that we would need
      ‹H.arr = V.arr›.
      This would be unreasonable to expect, in general, as the definition of ‹H.arr› is based
      on ``strict'' units rather than weak units.
      Later we will show that we do have ‹H.arr = V.arr› if the vertical category is discrete.
    ›

    abbreviation hseq
    where "hseq ν μ ≡ arr (ν ⋆ μ)"

    lemma hseq_char:
    shows "hseq ν μ ⟷ arr μ ∧ arr ν ∧ src ν = trg μ"
    proof -
      have "hseq ν μ ⟷ VV.arr (ν, μ)"
        using H.is_extensional H.preserves_arr by force
      also have "... ⟷ arr μ ∧ arr ν ∧ src ν = trg μ"
        using VV.arr_char by force
      finally show ?thesis by blast
    qed

    lemma hseq_char':
    shows "hseq ν μ ⟷ ν ⋆ μ ≠ null"
      using VV.arr_char H.preserves_arr H.is_extensional hseq_char [of ν μ] by auto

    lemma hseqI' [simp]:
    assumes "arr μ" and "arr ν" and "src ν = trg μ"
    shows "hseq ν μ"
      using assms hseq_char by simp

    lemma hseqI [intro]:
    assumes "«μ : a → b»" and "«ν : b → c»"
    shows "hseq ν μ"
      using assms hseq_char by auto

    lemma hseqE [elim]:
    assumes "hseq ν μ"
    and "arr μ ⟹ arr ν ⟹ src ν = trg μ ⟹ T"
    shows "T"
      using assms hseq_char by simp

    lemma hcomp_simps [simp]:
    assumes "hseq ν μ"
    shows "src (ν ⋆ μ) = src μ" and "trg (ν ⋆ μ) = trg ν"
    and "dom (ν ⋆ μ) = dom ν ⋆ dom μ" and "cod (ν ⋆ μ) = cod ν ⋆ cod μ"
      using assms VV.arr_char src_hcomp apply blast
      using assms VV.arr_char trg_hcomp apply blast
      using assms VV.arr_char H.preserves_dom apply force
      using assms VV.arr_char H.preserves_cod by force

    lemma ide_hcomp [intro, simp]:
    assumes "ide ν" and "ide μ" and "src ν = trg μ"
    shows "ide (ν ⋆ μ)"
      using assms VV.ide_char VV.arr_char H.preserves_ide [of "(ν, μ)"] by auto

    lemma hcomp_in_hhom [intro]:
    assumes "«μ : a → b»" and "«ν : b → c»"
    shows "«ν ⋆ μ : a → c»"
      using assms hseq_char by fastforce

    lemma hcomp_in_hhom' (* [simp] *):
    assumes "arr μ" and "arr ν" and "src μ = a" and "trg ν = c" and "src ν = trg μ"
    shows "«ν ⋆ μ : a → c»"
      using assms hseq_char by fastforce

    lemma hcomp_in_hhomE [elim]:
    assumes "«ν ⋆ μ : a → c»"
    and "⟦ arr μ; arr ν; src ν = trg μ; src μ = a; trg ν = c ⟧ ⟹ T"
    shows T
      using assms in_hhom_def by fastforce

    lemma hcomp_in_vhom [intro]:
    assumes "«μ : f ⇒ g»" and "«ν : h ⇒ k»" and "src h = trg f"
    shows "«ν ⋆ μ : h ⋆ f ⇒ k ⋆ g»"
      using assms by fastforce

    lemma hcomp_in_vhom' [simp]:
    assumes "hseq ν μ"
    and "dom μ = f" and "dom ν = h" and "cod μ = g" and "cod ν = k"
    assumes "«μ : f ⇒ g»" and "«ν : h ⇒ k»" and "src h = trg f"
    shows "«ν ⋆ μ : h ⋆ f ⇒ k ⋆ g»"
      using assms by fastforce

    lemma hcomp_in_vhomE [elim]:
    assumes "«ν ⋆ μ : f ⇒ g»"
    and "⟦ arr μ; arr ν; src ν = trg μ; src μ = src f; src μ = src g;
           trg ν = trg f; trg ν = trg g ⟧ ⟹ T"
    shows T
      using assms in_hom_def
      by (metis in_homE hseqE src_cod src_dom src_hcomp trg_cod trg_dom trg_hcomp)

    text ‹
      A horizontal composition yields a weak composition by simply forgetting
      the ‹src› and ‹trg› functors.
    ›

    lemma match_1:
    assumes "ν ⋆ μ ≠ null" and "(ν ⋆ μ) ⋆ τ ≠ null"
    shows "μ ⋆ τ ≠ null"
      using assms H.is_extensional not_arr_null VV.arr_char hseq_char hseq_char' by auto

    lemma match_2:
    assumes "ν ⋆ (μ ⋆ τ) ≠ null" and "μ ⋆ τ ≠ null"
    shows "ν ⋆ μ ≠ null"
      using assms H.is_extensional not_arr_null VV.arr_char hseq_char hseq_char' by auto

    lemma match_3:
    assumes "μ ⋆ τ ≠ null" and "ν ⋆ μ ≠ null"
    shows "(ν ⋆ μ) ⋆ τ ≠ null"
      using assms H.is_extensional not_arr_null VV.arr_char hseq_char hseq_char' by auto

    lemma match_4:
    assumes "μ ⋆ τ ≠ null" and "ν ⋆ μ ≠ null"
    shows "ν ⋆ (μ ⋆ τ) ≠ null"
      using assms H.is_extensional not_arr_null VV.arr_char hseq_char hseq_char' by auto

    lemma left_connected:
    assumes "seq ν ν'"
    shows "ν ⋆ μ ≠ null ⟷ ν' ⋆ μ ≠ null"
      using assms H.is_extensional not_arr_null VV.arr_char hseq_char'
      by (metis hseq_char seqE vseq_implies_hpar(1))

    lemma right_connected:
    assumes "seq μ μ'"
    shows "H ν μ ≠ null ⟷ H ν μ' ≠ null"
      using assms H.is_extensional not_arr_null VV.arr_char hseq_char'
      by (metis hseq_char seqE vseq_implies_hpar(2))

    proposition is_weak_composition:
    shows "weak_composition V H"
    proof -
      have 1: "(λμν. fst μν ⋆ snd μν ≠ null)
                 = (λμν. arr (fst μν) ∧ arr (snd μν) ∧ src (fst μν) = trg (snd μν))"
        using hseq_char' by auto
      interpret VoV: subcategory VxV.comp ‹λμν. fst μν ⋆ snd μν ≠ null›
        using 1 VV.subcategory_axioms by simp
      interpret H: "functor" VoV.comp V ‹λμν. fst μν ⋆ snd μν›
        using H.functor_axioms 1 by simp
      show ?thesis
        using match_1 match_2 match_3 match_4 left_connected right_connected
        by (unfold_locales, metis)
    qed

    interpretation weak_composition V H
      using is_weak_composition by auto

     text ‹
      It can be shown that ‹arr ((ν ⋅ μ) ⋆ (τ ⋅ σ)) ⟹ (ν ⋅ μ) ⋆ (τ ⋅ σ) = (ν ⋆ τ) ⋅ (μ ⋆ σ)›.
      However, we do not have ‹arr ((ν ⋆ τ) ⋅ (μ ⋆ σ)) ⟹ (ν ⋅ μ) ⋆ (τ ⋅ σ) = (ν ⋆ τ) ⋅ (μ ⋆ σ)›,
      because it does not follow from ‹arr ((ν ⋆ τ) ⋅ (μ ⋆ σ))› that ‹dom ν = cod μ›
      and ‹dom τ = cod σ›, only that ‹dom ν ⋆ dom τ = cod μ ⋆ cod σ›.
      So we don't get interchange unconditionally.
    ›

    lemma interchange:
    assumes "seq ν μ" and "seq τ σ"
    shows "(ν ⋅ μ) ⋆ (τ ⋅ σ) = (ν ⋆ τ) ⋅ (μ ⋆ σ)"
      using assms interchange by simp

    lemma whisker_right:
    assumes "ide f" and "seq ν μ"
    shows "(ν ⋅ μ) ⋆ f = (ν ⋆ f) ⋅ (μ ⋆ f)"
      using assms whisker_right by simp

    lemma whisker_left:
    assumes "ide f" and "seq ν μ"
    shows "f ⋆ (ν ⋅ μ) = (f ⋆ ν) ⋅ (f ⋆ μ)"
      using assms whisker_left by simp

    lemma inverse_arrows_hcomp:
    assumes "iso μ" and "iso ν" and "src ν = trg μ"
    shows "inverse_arrows (ν ⋆ μ) (inv ν ⋆ inv μ)"
    proof -
      show "inverse_arrows (ν ⋆ μ) (inv ν ⋆ inv μ)"
      proof
        show "ide ((inv ν ⋆ inv μ) ⋅ (ν ⋆ μ))"
        proof -
          have "(inv ν ⋆ inv μ) ⋅ (ν ⋆ μ) = dom ν ⋆ dom μ"
            using assms interchange iso_is_arr comp_inv_arr'
            by (metis arr_dom)
          thus ?thesis
            using assms iso_is_arr by simp
        qed
        show "ide ((ν ⋆ μ) ⋅ (inv ν ⋆ inv μ))"
        proof -
          have "(ν ⋆ μ) ⋅ (inv ν ⋆ inv μ) = cod ν ⋆ cod μ"
            using assms interchange iso_is_arr comp_arr_inv'
            by (metis arr_cod)
          thus ?thesis
            using assms iso_is_arr by simp
        qed
      qed
    qed

    lemma iso_hcomp [intro, simp]:
    assumes "iso μ" and "iso ν" and "src ν = trg μ"
    shows "iso (ν ⋆ μ)"
      using assms inverse_arrows_hcomp by auto

    lemma isomorphic_implies_ide:
    assumes "f ≅ g"
    shows "ide f" and "ide g"
      using assms isomorphic_def by auto

    lemma hcomp_ide_isomorphic:
    assumes "ide f" and "g ≅ h" and "src f = trg g"
    shows "f ⋆ g ≅ f ⋆ h"
    proof -
      obtain μ where μ: "iso μ ∧ «μ : g ⇒ h»"
        using assms isomorphic_def by auto
      have "iso (f ⋆ μ) ∧ «f ⋆ μ : f ⋆ g ⇒ f ⋆ h»"
        using assms μ iso_hcomp by auto
      thus ?thesis
        using isomorphic_def by auto
    qed

    lemma hcomp_isomorphic_ide:
    assumes "f ≅ g" and "ide h" and "src f = trg h"
    shows "f ⋆ h ≅ g ⋆ h"
    proof -
      obtain μ where μ: "iso μ ∧ «μ : f ⇒ g»"
        using assms isomorphic_def by auto
      have "iso (μ ⋆ h) ∧ «μ ⋆ h : f ⋆ h ⇒ g ⋆ h»"
        using assms μ iso_hcomp by auto
      thus ?thesis
        using isomorphic_def by auto
    qed

    lemma isomorphic_implies_hpar:
    assumes "f ≅ f'"
    shows "ide f" and "ide f'" and "src f = src f'" and "trg f = trg f'"
      using assms isomorphic_def by auto

    lemma inv_hcomp [simp]:
    assumes "iso ν" and "iso μ" and "src ν = trg μ"
    shows "inv (ν ⋆ μ) = inv ν ⋆ inv μ"
      using assms inverse_arrow_unique [of "ν ⋆ μ"] inv_is_inverse inverse_arrows_hcomp
      by auto

    interpretation VxVxV: product_category V VxV.comp ..
    interpretation VVV: subcategory VxVxV.comp
                          ‹λτμν. arr (fst τμν) ∧ VV.arr (snd τμν) ∧
                                 src (fst τμν) = trg (fst (snd τμν))›
      using subcategory_VVV by auto

    text ‹
      The following define the two ways of using horizontal composition to compose three arrows.
    ›

    definition HoHV
    where "HoHV μ ≡ if VVV.arr μ then (fst μ ⋆ fst (snd μ)) ⋆ snd (snd μ) else null"

    definition HoVH
    where "HoVH μ ≡ if VVV.arr μ then fst μ ⋆ fst (snd μ) ⋆ snd (snd μ) else null"

    lemma functor_HoHV:
    shows "functor VVV.comp V HoHV"
      apply unfold_locales
      using VVV.arr_char VV.arr_char VVV.dom_char VVV.cod_char VVV.comp_char HoHV_def
          apply auto[4]
    proof -
      fix f g
      assume fg: "VVV.seq g f"
      show "HoHV (VVV.comp g f) = HoHV g ⋅ HoHV f"
      proof -
        have "VxVxV.comp g f =
              (fst g ⋅ fst f, fst (snd g) ⋅ fst (snd f), snd (snd g) ⋅ snd (snd f))"
          using fg VVV.seq_char VVV.arr_char VV.arr_char VxVxV.comp_char VxV.comp_char
          by (metis (no_types, lifting) VxV.seqE VxVxV.seqE)
        hence "HoHV (VVV.comp g f) =
              (fst g ⋅ fst f ⋆ fst (snd g) ⋅ fst (snd f)) ⋆ snd (snd g) ⋅ snd (snd f)"
          using HoHV_def VVV.comp_simp fg by auto
        also have "... = ((fst g ⋆ fst (snd g)) ⋆ snd (snd g)) ⋅
                           ((fst f ⋆ fst (snd f)) ⋆ snd (snd f))"
          using fg VVV.seq_char VVV.arr_char VV.arr_char interchange
          by (metis (no_types, lifting) VxV.seqE VxVxV.seqE hseqI' src_vcomp trg_vcomp)
        also have "... = HoHV g ⋅ HoHV f"
          using HoHV_def fg by auto
        finally show ?thesis by simp
      qed
    qed

    lemma functor_HoVH:
    shows "functor VVV.comp V HoVH"
      apply unfold_locales
      using VVV.arr_char VV.arr_char VVV.dom_char VVV.cod_char VVV.comp_char
            HoHV_def HoVH_def
          apply auto[4]
    proof -
      fix f g
      assume fg: "VVV.seq g f"
      show "HoVH (VVV.comp g f) = HoVH g ⋅ HoVH f"
      proof -
        have "VxVxV.comp g f =
              (fst g ⋅ fst f, fst (snd g) ⋅ fst (snd f), snd (snd g) ⋅ snd (snd f))"
          using fg VVV.seq_char VVV.arr_char VV.arr_char VxVxV.comp_char VxV.comp_char
          by (metis (no_types, lifting) VxV.seqE VxVxV.seqE)
        hence "HoVH (VVV.comp g f) =
              fst g ⋅ fst f ⋆ fst (snd g) ⋅ fst (snd f) ⋆ snd (snd g) ⋅ snd (snd f)"
          using HoVH_def VVV.comp_simp fg by auto
        also have "... = (fst g ⋆ fst (snd g) ⋆ snd (snd g)) ⋅
                           (fst f ⋆ fst (snd f) ⋆ snd (snd f))"
          using fg VVV.seq_char VVV.arr_char VV.arr_char interchange
          by (metis (no_types, lifting) VxV.seqE VxVxV.seqE hseqI' src_vcomp trg_vcomp)
        also have "... = HoVH g ⋅ HoVH f"
          using fg VVV.seq_char VVV.arr_char HoVH_def VVV.comp_char VV.arr_char
          by (metis (no_types, lifting))
        finally show ?thesis by simp
      qed
    qed

    text ‹
      The following define horizontal composition of an arrow on the left by its target
      and on the right by its source.
    ›

    abbreviation L
    where "L ≡ λμ. if arr μ then trg μ ⋆ μ else null"

    abbreviation R
    where "R ≡ λμ. if arr μ then μ ⋆ src μ else null"

    lemma endofunctor_L:
    shows "endofunctor V L"
      using vseq_implies_hpar(2) whisker_left
      by (unfold_locales, auto)

    lemma endofunctor_R:
    shows "endofunctor V R"
      using vseq_implies_hpar(1) whisker_right
      by (unfold_locales, auto)

  end

end

Theory Bicategory

theory Bicategory
imports Prebicategory DiscreteCategory MonoidalCategory
(*  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 +
    VxVxV: product_category V VxV.comp +
    VVV: subcategory VxVxV.comp ‹λτμν. arr (fst τμν) ∧ VV.arr (snd τμν) ∧
                                       src (fst τμν) = trg (fst (snd τμν))› +
    HoHV: "functor" VVV.comp V HoHV +
    HoVH: "functor" VVV.comp V HoVH +
    α: natural_isomorphism VVV.comp V HoHV HoVH
         ‹λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ))› +
    L: fully_faithful_functor V V L +
    R: fully_faithful_functor V V R
  for V :: "'a comp"                 (infixr "⋅" 55)
  and H :: "'a ⇒ 'a ⇒ 'a"          (infixr "⋆" 53)
  and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a"     ("𝖺[_, _, _]")
  and 𝗂 :: "'a ⇒ 'a"                 ("𝗂[_]")
  and src :: "'a ⇒ 'a"
  and trg :: "'a ⇒ 'a" +
  assumes unit_in_vhom: "obj a ⟹ «𝗂[a] : a ⋆ a ⇒ a»"
  and iso_unit: "obj a ⟹ iso 𝗂[a]"
  and pentagon: "⟦ ide f; ide g; ide h; ide k; src f = trg g; src g = trg h; src h = trg k ⟧ ⟹
                   (f ⋆ 𝖺 g h k) ⋅ 𝖺 f (g ⋆ h) k ⋅ (𝖺 f g h ⋆ k) = 𝖺 f g (h ⋆ k) ⋅ 𝖺 (f ⋆ g) h k"
  begin
    (*
     * TODO: the mapping 𝗂 is not currently assumed to be extensional.
     * It might be best in the long run if it were.
     *)

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

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

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

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

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

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

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

    lemma iso_assoc [intro, simp]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "iso 𝖺[f, g, h]"
      using assms α.components_are_iso [of "(f, g, h)"] VVV.ide_char VVV.arr_char VV.arr_char
      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 VxV: product_category V V ..
    interpretation VV: subcategory VxV.comp
                          ‹λμν. V.arr (fst μν) ∧ V.arr (snd μν) ∧ dom (fst μν) = cod (snd μν)›
      using H.subcategory_VV by auto
    interpretation VxVxV: product_category V VxV.comp ..
    interpretation VVV: subcategory VxVxV.comp ‹λτμν. V.arr (fst τμν) ∧
                          VV.arr (snd τμν) ∧ dom (fst τμν) = cod (fst (snd τμν))›
      using H.subcategory_VVV by auto

    interpretation H: "functor" VV.comp V ‹λμν. fst μν ⋅ snd μν›
      apply (unfold_locales)
      using VV.arr_char V.null_char ext
          apply force
      using VV.arr_char V.null_char VV.dom_char VV.cod_char
         apply auto[3]
    proof -
      show "⋀g f. VV.seq g f ⟹
                   fst (VV.comp g f) ⋅ snd (VV.comp g f) = V (fst g ⋅ snd g) (fst f ⋅ snd f)"
      proof -
        have 0: "⋀f. VV.arr f ⟹ V.arr (fst f ⋅ snd f)"
          using VV.arr_char 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. VxV.seq g f ⟹ VxV.ide f ∧ g = f"
          using 1 VxV.seq_char by (metis VxV.dom_eqI VxV.ide_Ide)
        fix f g
        assume fg: "VV.seq g f"
        have 3: "VV.ide f ∧ f = g"
          using fg 2 VV.seq_char VV.ide_char by blast
        show "fst (VV.comp g f) ⋅ snd (VV.comp g f) = V (fst g ⋅ snd g) (fst f ⋅ snd f)"
          using fg 0 1 3 VV.comp_char VV.arr_char VV.ide_char V.arr_char V.comp_char
                VV.comp_arr_ide
          by (metis (no_types, lifting))
      qed
    qed

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

    interpretation H.HoHV: "functor" VVV.comp V H.HoHV
      using H.functor_HoHV by blast
    interpretation H.HoVH: "functor" VVV.comp V H.HoVH
      using H.functor_HoVH by blast

    abbreviation 𝖺
    where "𝖺 f g h ≡ f ⋅ g ⋅ h"

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

    interpretation endofunctor V H.L
        using H.endofunctor_L by auto
    interpretation endofunctor V H.R
      using H.endofunctor_R by auto

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

    abbreviation 𝗂
    where "𝗂 ≡ λx. x"

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

  end

  subsection "Monoidal Categories induce Bicategories"

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

  context monoidal_category
  begin

    interpretation I: constant_functor C C 
      using ι_in_hom by unfold_locales auto
    interpretation HH: horizontal_homs C I.map I.map
      by unfold_locales auto
    interpretation CC': subcategory CC.comp ‹λμν. arr (fst μν) ∧ arr (snd μν) ∧
                                                  I.map (fst μν) = I.map (snd μν)›
      using HH.subcategory_VV by auto
    interpretation CCC': subcategory CCC.comp ‹λτμν. arr (fst τμν) ∧ CC'.arr (snd τμν) ∧
                                                     I.map (fst τμν) = I.map (fst (snd τμν))›
      using HH.subcategory_VVV by simp

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

    lemma CCC'_eq_CCC:
    shows "CCC.comp = CCC'.comp"
    proof -
      have "⋀g f. CCC.comp g f = CCC'.comp g f"
      proof -
        fix f g
        show "CCC.comp g f = CCC'.comp g f"
        proof -
          have "CCC.seq g f ⟹ CCC.comp g f = CCC'.comp g f"
            using CCC'.comp_char CCC'.arr_char CCC.seq_char CC'.arr_char
            by (elim CCC.seqE CC.seqE seqE, simp)
          moreover have "¬ CCC.seq g f ⟹ CCC.comp g f = CCC'.comp g f"
            using CCC'.seq_char CCC'.ext CCC'.null_char CCC.ext
            by (metis (no_types, lifting))
          ultimately show ?thesis by blast
        qed
      qed
      thus ?thesis by blast
    qed

    interpretation H: "functor" CC'.comp C ‹λμν. fst μν ⊗ snd μν›
      using CC'_eq_CC 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_CCC by presburger

    interpretation HoHV: "functor" CCC'.comp C H.HoHV
      using T.functor_ToTC HoHV_eq_ToTC CCC'_eq_CCC by argo

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

    interpretation HoVH: "functor" CCC'.comp C H.HoVH
      using T.functor_ToCT HoVH_eq_ToCT CCC'_eq_CCC by argo

    interpretation α: natural_isomorphism CCC'.comp C H.HoHV H.HoVH α
      using α.natural_isomorphism_axioms CCC'_eq_CCC HoHV_eq_ToTC HoVH_eq_ToCT
      by simp

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

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

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

    lemma obj_char:
    shows "HH.obj a ⟷ a = ℐ"
      using HH.obj_def ι_in_hom by fastforce

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

  end

  subsection "Prebicategories Extend to Bicategories"

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

  context prebicategory_with_homs
  begin

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

    lemma induces_horizontal_composition:
    shows "horizontal_composition V H src trg"
    proof -
      interpret VxV: product_category V V ..
      interpret VV: subcategory VxV.comp ‹λμν. arr (fst μν) ∧ arr (snd μν) ∧
                                               src (fst μν) = trg (snd μν)›
        using subcategory_VV by argo
      interpret VxVxV: product_category V VxV.comp ..
      interpret VVV: subcategory VxVxV.comp
                          ‹λτμν. arr (fst τμν) ∧ VV.arr (snd τμν) ∧
                                 src (fst τμν) = trg (fst (snd τμν))›
        using subcategory_VVV by blast
      interpret H: "functor" VV.comp V ‹λμν. fst μν ⋆ snd μν›
      proof -
        have "VV.comp = VoV.comp"
          using composable_charPBH by meson
        thus "functor VV.comp V (λμν. fst μν ⋆ snd μν)"
          using functor_axioms by argo
      qed
      show "horizontal_composition V H src trg"
        using src_hcomp' trg_hcomp' composable_charPBH not_arr_null
        by (unfold_locales; metis)
    qed

  end

  sublocale prebicategory_with_homs  horizontal_composition V H src trg
    using induces_horizontal_composition by auto

  locale prebicategory_with_homs_and_units =
    prebicategory_with_units +
    prebicategory_with_homs
  begin

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

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

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

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

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

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

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

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

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

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

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

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

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

    lemma lunit_naturality:
    assumes "arr μ"
    shows "μ ⋅ 𝗅[dom μ] = 𝗅[cod μ] ⋅ (trg μ ⋆ μ)"
    proof -
      let ?a = "src μ" and ?b = "trg μ"
      interpret Left: subcategory V ‹left ?b›
        using assms obj_trg left_hom_is_subcategory weak_unit_self_composable by force
      interpret Left: left_hom_with_unit V H 𝖺 ‹𝗂[?b]› ?b
        using assms obj_is_weak_unit iso_unitPBU by (unfold_locales, auto)
      interpret Left.L: endofunctor ‹Left ?b› Left.L
        using assms endofunctor_HL [of ?b] weak_unit_self_composable obj_trg obj_is_weak_unit
        by blast
      have 1: "Left.in_hom μ (dom μ) (cod μ)"
        using assms Left.hom_char Left.arr_char left_def composable_charPBH obj_trg by auto
      have 2: "Left.in_hom 𝗅[Left.dom μ] (?b ⋆ dom μ) (dom μ)"
        unfolding lunit_def
        using assms 1 Left.in_hom_char trg_dom Left.lunit_char(1) HL_def
              Left.arr_char Left.dom_char Left.ide_dom
        by force
      have 3: "Left.in_hom 𝗅[Left.cod μ] (?b ⋆ cod μ) (cod μ)"
        unfolding lunit_def
        using assms 1 Left.in_hom_char trg_cod Left.lunit_char(1) HL_def
              Left.cod_char Left.ide_cod
        by force
      have 4: "Left.in_hom (Left.L μ) (?b ⋆ dom μ) (?b ⋆ cod μ)"
        using 1 Left.L.preserves_hom [of μ "dom μ" "cod μ"] HL_def by auto
      show ?thesis
      proof -
        have "μ ⋅ 𝗅[dom μ] = Left.comp μ 𝗅[Left.dom μ]"
          using 1 2 Left.comp_simp by fastforce
        also have "... = Left.comp μ (Left.lunit (Left.dom μ))"
          using assms 1 lunit_def by auto
        also have "... = Left.comp (Left.lunit (Left.cod μ)) (Left.L μ)"
          using 1 Left.lunit_naturality by auto
        also have "... = Left.comp (lunit (Left.cod μ)) (Left.L μ)"
          using assms 1 lunit_def by auto
        also have "... = 𝗅[cod μ] ⋅ Left.L μ"
          using 1 3 4 Left.comp_char Left.cod_char Left.in_hom_char by auto
        also have "... = 𝗅[cod μ] ⋅ (trg μ ⋆ μ)"
          using 1 by (simp add: HL_def)
        finally show ?thesis by simp
      qed
    qed

    lemma runit_naturality:
    assumes "arr μ"
    shows "μ ⋅ 𝗋[dom μ] = 𝗋[cod μ] ⋅ (μ ⋆ src μ)"
    proof -
      let ?a = "src μ" and ?b = "trg μ"
      interpret Right: subcategory V ‹right ?a›
        using assms right_hom_is_subcategory weak_unit_self_composable by force
      interpret Right: right_hom_with_unit V H 𝖺 ‹𝗂[?a]› ?a
        using assms obj_is_weak_unit iso_unitPBU by (unfold_locales, auto)
      interpret Right.R: endofunctor ‹Right ?a› Right.R
        using assms endofunctor_HR [of ?a] weak_unit_self_composable obj_src obj_is_weak_unit
        by blast
      have 1: "Right.in_hom μ (dom μ) (cod μ)"
        using assms Right.hom_char Right.arr_char right_def composable_charPBH by auto
      have 2: "Right.in_hom 𝗋[Right.dom μ] (dom μ ⋆ ?a) (dom μ)"
        unfolding runit_def
        using 1 Right.in_hom_char trg_dom Right.runit_char(1) [of "Right.dom μ"] HR_def
              Right.arr_char Right.dom_char Right.ide_dom assms
        by force
      have 3: "𝗋[Right.cod μ] ∈ Right.hom (cod μ ⋆ ?a) (cod μ)"
        unfolding runit_def
        using 1 Right.in_hom_char trg_cod Right.runit_char(1) [of "Right.cod μ"] HR_def
              Right.cod_char Right.ide_cod assms
        by force
      have 4: "Right.R μ ∈ Right.hom (dom μ ⋆ ?a) (cod μ ⋆ ?a)"
        using 1 Right.R.preserves_hom [of μ "dom μ" "cod μ"] HR_def by auto
      show ?thesis
      proof -
        have "μ ⋅ 𝗋[dom μ] = Right.comp μ 𝗋[Right.dom μ]"
          by (metis 1 2 Right.comp_char Right.in_homE Right.seqI' Right.seq_char)
        also have "... = Right.comp μ (Right.runit (Right.dom μ))"
          using assms 1 src_dom trg_dom Right.hom_char runit_def by auto
        also have "... = Right.comp (Right.runit (Right.cod μ)) (Right.R μ)"
          using 1 Right.runit_naturality by auto
        also have "... = Right.comp (runit (Right.cod μ)) (Right.R μ)"
          using assms 1 runit_def by auto
        also have "... = 𝗋[cod μ] ⋅ Right.R μ"
          using 1 3 4 Right.comp_char Right.cod_char Right.in_hom_char by auto
        also have "... = 𝗋[cod μ] ⋅ (μ ⋆ ?a)"
          using 1 by (simp add: HR_def)
        finally show ?thesis by simp
      qed
    qed

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

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

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

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

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

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

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

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

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

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

    interpretation VxVxV: product_category V VxV.comp ..
    interpretation VVV: subcategory VxVxV.comp
                            ‹λτμν. arr (fst τμν) ∧ VV.arr (snd τμν) ∧
                                   src (fst τμν) = trg (fst (snd τμν))›
      using subcategory_VVV by blast
    interpretation HoHV: "functor" VVV.comp V HoHV
      using functor_HoHV by blast
    interpretation HoVH: "functor" VVV.comp V HoVH
      using functor_HoVH by blast

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

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

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

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

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

  end

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

  context prebicategory
  begin

    interpretation prebicategory_with_homs V H 𝖺 some_src some_trg
      using extends_to_prebicategory_with_homs by auto

    interpretation prebicategory_with_units V H 𝖺 some_unit
      using extends_to_prebicategory_with_units by auto

    interpretation prebicategory_with_homs_and_units V H 𝖺 some_unit some_src some_trg ..

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

  end

  section "Bicategories as Prebicategories"

  subsection "Bicategories are Prebicategories"

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

  context bicategory
  begin

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    lemma unit_in_hom [intro, simp]:
    assumes "obj a"
    shows "«𝗂[a] : a → a»" and "«𝗂[a] : a ⋆ a ⇒ a»"
    proof -
      show "«𝗂[a] : a ⋆ a ⇒ a»"
        using assms unit_in_vhom by simp
      thus "«𝗂[a] : a → a»"
        using assms src_cod trg_cod by fastforce
    qed

    interpretation weak_composition V H
      using is_weak_composition by auto

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

    lemma obj_self_composable:
    assumes "obj a"
    shows "a ⋆ a ≠ null"
    and "isomorphic (a ⋆ a) a"
    proof -
      show 1: "isomorphic (a ⋆ a) a"
        using assms unit_in_hom iso_unit isomorphic_def by blast
      obtain φ where φ: "iso φ ∧ «φ : a ⋆ a ⇒ a»"
        using 1 isomorphic_def by blast
      have "ide (a ⋆ a)" using 1 φ ide_dom [of φ] by fastforce
      thus "a ⋆ a ≠ null" using ideD(1) not_arr_null by metis
    qed

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

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

      interpret La: endofunctor ‹Left a› ‹HL a›
        using assms obj_self_composable endofunctor_HL [of a] by force
      interpret La: fully_faithful_functor ‹Left a› ‹Left a› ‹HL a›
      proof
        show "⋀f f'. Left_a.par f f' ⟹ HL a f = HL a f' ⟹ f = f'"
        proof -
          fix μ μ'
          assume par: "Left_a.par μ μ'"
          assume eq: "HL a μ = HL a μ'"
          have 1: "par μ μ'"
            using par Left_a.arr_char Left_a.dom_char Left_a.cod_char left_def
                  composable_implies_arr null_agreement
            by metis
          moreover have "L μ = L μ'"
            using par eq HL_def Left_a.arr_char left_def preserves_arr
                  assms 1 seq_if_composable [of a μ] not_arr_null seq_if_composable [of a μ']
            by auto
          ultimately show "μ = μ'"
            using L.is_faithful by blast
        qed
        show "⋀f g μ. ⟦ Left_a.ide f; Left_a.ide g; Left_a.in_hom μ (HL a f) (HL a g) ⟧ ⟹
                        ∃ν. Left_a.in_hom ν f g ∧ HL a ν = μ"
        proof -
          fix f g μ
          assume f: "Left_a.ide f" and g: "Left_a.ide g"
          and μ: "Left_a.in_hom μ (HL a f) (HL a g)"
          have 1: "a = trg f ∧ a = trg g"
            using assms f g Left_a.ide_char Left_a.arr_char left_def seq_if_composable [of a f]
                  seq_if_composable [of a g]
            by auto
          show "∃ν. Left_a.in_hom ν f g ∧ HL a ν = μ"
          proof -
            have 2: "∃ν. «ν : f ⇒ g» ∧ L ν = μ"
              using f g μ 1 Left_a.ide_char HL_def L.preserves_reflects_arr Left_a.arr_char
                    Left_a.in_hom_char 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 left_def hseq_char' by fastforce
            moreover have "HL a ν = μ"
              using ν 1 trg_dom HL_def by auto
            ultimately show ?thesis
              using ν by force
          qed
        qed
      qed
      interpret Ra: endofunctor ‹Right a› ‹HR a›
        using assms obj_self_composable endofunctor_HR [of a] by force
      interpret Ra: fully_faithful_functor ‹Right a› ‹Right a› ‹HR a›
      proof
        show "⋀f f'. Right_a.par f f' ⟹ HR a f = HR a f' ⟹ f = f'"
        proof -
          fix μ μ'
          assume par: "Right_a.par μ μ'"
          assume eq: "HR a μ = HR a μ'"
          have 1: "par μ μ'"
            using par Right_a.arr_char Right_a.dom_char Right_a.cod_char right_def
                  composable_implies_arr null_agreement
            by metis
          moreover have "R μ = R μ'"
            using par eq HR_def Right_a.arr_char right_def preserves_arr
                  assms 1 seq_if_composable [of μ a] not_arr_null seq_if_composable [of μ' a]
            by auto
          ultimately show "μ = μ'"
            using R.is_faithful by blast
        qed
        show "⋀f g μ. ⟦ Right_a.ide f; Right_a.ide g; Right_a.in_hom μ (HR a f) (HR a g) ⟧ ⟹
                        ∃ν. Right_a.in_hom ν f g ∧ HR a ν = μ"
        proof -
          fix f g μ
          assume f: "Right_a.ide f" and g: "Right_a.ide g"
          and μ: "Right_a.in_hom μ (HR a f) (HR a g)"
          have 1: "a = src f ∧ a = src g"
            using assms f g Right_a.ide_char Right_a.arr_char right_def seq_if_composable
            by auto
          show "∃ν. Right_a.in_hom ν f g ∧ HR a ν = μ"
          proof -
            have 2: "∃ν. «ν : f ⇒ g» ∧ R ν = μ"
              using f g μ 1 Right_a.ide_char HR_def R.preserves_reflects_arr Right_a.arr_char
                    Right_a.in_hom_char 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 right_def hseq_char' by fastforce
            moreover have "HR a ν = μ"
              using ν 1 src_dom HR_def by auto
            ultimately show ?thesis
              using ν by force
          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 by unfold_locales auto
      interpret La: fully_faithful_functor ‹Left a› ‹Left a› ‹HL a›
        using assms weak_unit_def by fast
      obtain φ where φ: "iso φ ∧ «φ : a ⋆ f ⇒ a ⋆ g»"
        using assms by blast
      have 1: "Left_a.iso φ ∧ Left_a.in_hom φ (a ⋆ f) (a ⋆ g)"
      proof
        have "a ⋆ φ ≠ null"
        proof -
          have "a ⋆ dom φ ≠ null"
            using assms φ weak_unit_self_composable
            by (metis arr_dom_iff_arr hseq_char' in_homE match_4)
          thus ?thesis
            using hom_connected by simp
        qed
        thus "Left_a.in_hom φ (a ⋆ f) (a ⋆ g)"
          using φ Left_a.hom_char left_def by auto
        thus "Left_a.iso φ"
          using φ Left_a.iso_char by auto
      qed
      hence 2: "Left_a.ide (a ⋆ f) ∧ Left_a.ide (a ⋆ g)"
        using Left_a.ide_dom [of φ] Left_a.ide_cod [of φ] by auto
      hence 3: "Left_a.ide f ∧ Left_a.ide g"
        by (metis Left_a.ideI Left_a.ide_def Left_a.null_char assms(2) assms(3) left_def)
      obtain ψ where ψ: "ψ ∈ Left_a.hom f g ∧ a ⋆ ψ = φ"
        using assms 1 2 3 La.is_full [of g f φ] HL_def by auto
      have "Left_a.iso ψ"
        using ψ 1 HL_def La.reflects_iso by auto
      hence "iso ψ ∧ «ψ : f ⇒ g»"
        using ψ Left_a.iso_char Left_a.in_hom_char 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 by unfold_locales auto
      interpret R: fully_faithful_functor ‹Right a› ‹Right a› ‹HR a›
        using assms weak_unit_def by fast
      obtain φ where φ: "iso φ ∧ in_hom φ (f ⋆ a) (g ⋆ a)"
        using assms by blast
      have 1: "Right_a.iso φ ∧ φ ∈ Right_a.hom (f ⋆ a) (g ⋆ a)"
      proof
        have "φ ⋆ a ≠ null"
        proof -
          have "dom φ ⋆ a ≠ null"
            using assms φ weak_unit_self_composable
            by (metis arr_dom_iff_arr hseq_char' in_homE match_3)
          thus ?thesis
            using hom_connected by simp
        qed
        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 φ]