(*  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

(*  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_simps⇩W⇩C [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_hcomp⇩W⇩C [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_hom⇩W⇩C [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 H⇩L
    where "H⇩L g ≡ λμ. g ⋆ μ"

    definition H⇩R
    where "H⇩R 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_H⇩L:
    assumes "ide g" and "g ⋆ g ≠ null"
    shows "endofunctor (Left g) (H⇩L g)"
    proof -
      interpret L: subcategory V ‹left g› using assms left_hom_is_subcategory by simp
      have *: "⋀μ. L.arr μ ⟹ H⇩L g μ = g ⋆ μ"
        using assms H⇩L_def by simp
      have preserves_arr: "⋀μ. L.arr μ ⟹ L.arr (H⇩L g μ)"
        using assms * L.arr_char left_def match_4 by force
      show "endofunctor L.comp (H⇩L g)"
      proof
        show "⋀μ. ¬ L.arr μ ⟹ H⇩L g μ = L.null"
          using assms L.arr_char L.null_char left_def H⇩L_def by fastforce
        show "⋀μ. L.arr μ ⟹ L.arr (H⇩L 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 (H⇩L g μ) = H⇩L g (L.dom μ)"
          using assms μ * L.arr_char L.dom_char preserves_arr hom_connected(2) left_def
          by simp
        show "L.cod (H⇩L g μ) = H⇩L 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 "H⇩L g (L.comp ν μ) = L.comp (H⇩L g ν) (H⇩L g μ)"
        proof -
          have "H⇩L g (L.comp ν μ) = g ⋆ (ν ⋅ μ)"
            using μ ν H⇩L_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 (H⇩L g ν) (H⇩L g μ)"
            using assms μν μ ν * preserves_arr L.arr_char L.dom_char L.cod_char L.comp_char
                  L.inclusion H⇩L_def left_def
            by auto
          finally show ?thesis by blast
        qed
      qed
    qed

    lemma endofunctor_H⇩R:
    assumes "ide f" and "f ⋆ f ≠ null"
    shows "endofunctor (Right f) (H⇩R f)"
    proof -
      interpret R: subcategory V ‹right f› using assms right_hom_is_subcategory by simp
      have *: "⋀μ. R.arr μ ⟹ H⇩R f μ = μ ⋆ f"
        using assms H⇩R_def by simp
      have preserves_arr: "⋀μ. R.arr μ ⟹ R.arr (H⇩R f μ)"
        using assms * R.arr_char right_def match_3 by force
      show "endofunctor R.comp (H⇩R f)"
      proof
        show "⋀μ. ¬ R.arr μ ⟹ H⇩R f μ = R.null"
          using assms R.arr_char R.null_char right_def H⇩R_def by fastforce
        show "⋀μ. R.arr μ ⟹ R.arr (H⇩R 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 (H⇩R f μ) = H⇩R f (R.dom μ)"
          using assms μ * R.arr_char R.dom_char preserves_arr hom_connected(1) right_def
          by simp
        show "R.cod (H⇩R f μ) = H⇩R 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 "H⇩R f (R.comp ν μ) = R.comp (H⇩R f ν) (H⇩R f μ)"
        proof -
          have "H⇩R f (R.comp ν μ) = (ν ⋅ μ) ⋆ f"
            using μ ν H⇩R_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 (H⇩R f ν) (H⇩R f μ)"
            using assms μν μ ν * preserves_arr R.arr_char R.dom_char R.cod_char R.comp_char
                  R.inclusion H⇩R_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_simps⇩W⇩C(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_simps⇩W⇩C(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) (H⇩L a) ∧
                         fully_faithful_functor (Right a) (Right a) (H⇩R 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_hhom⇩W⇩C  ("«_ : _ →⇩W⇩C _»")
    where "in_hhom⇩W⇩C μ 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 H⇩R_preserved_along_iso:
    assumes "weak_unit a" and "a ≅ a'"
    shows "endofunctor (Right a) (H⇩R 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 μ ⟹ H⇩R a' μ = μ ⋆ a'"
        using assms H⇩R_def by simp
      have preserves_arr: "⋀μ. R.arr μ ⟹ R.arr (H⇩R 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_simps⇩W⇩C(1)
              null_agreement
        by metis
      show "endofunctor R.comp (H⇩R a')"
      proof
        show "⋀μ. ¬ R.arr μ ⟹ H⇩R a' μ = R.null"
          using assms R.arr_char R.null_char right_def H⇩R_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 (H⇩R a' μ)" using μ preserves_arr by blast
        show "R.dom (H⇩R a' μ) = H⇩R a' (R.dom μ)"
          using a' μ * R.arr_char R.dom_char preserves_arr hom_connected(1) right_def
          by simp
        show "R.cod (H⇩R a' μ) = H⇩R 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 "H⇩R a' (R.comp ν μ) = R.comp (H⇩R a' ν) (H⇩R a' μ)"
        proof -
          have 1: "R.arr (H⇩R 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 "H⇩R a' (R.comp ν μ) = (ν ⋅ μ) ⋆ a'"
              using μ ν H⇩R_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 (H⇩R a' ν) (H⇩R a' μ)"
              using assms μ 1 2 preserves_arr R.comp_char R.inclusion H⇩R_def by auto
            finally show ?thesis by blast
          qed
        qed
      qed
    qed

    lemma H⇩L_preserved_along_iso:
    assumes "weak_unit a" and "a ≅ a'"
    shows "endofunctor (Left a) (H⇩L 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 μ ⟹ H⇩L a' μ = a' ⋆ μ"
        using assms H⇩L_def by simp
      have preserves_arr: "⋀μ. L.arr μ ⟹ L.arr (H⇩L 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_simps⇩W⇩C(1)
              null_agreement
        by metis
      show "endofunctor L.comp (H⇩L a')"
      proof
        show "⋀μ. ¬ L.arr μ ⟹ H⇩L a' μ = L.null"
          using assms L.arr_char L.null_char left_def H⇩L_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 (H⇩L a' μ)" using μ preserves_arr by blast
        show "L.dom (H⇩L a' μ) = H⇩L a' (L.dom μ)"
          using a' μ * L.arr_char L.dom_char preserves_arr hom_connected(2) left_def
          by simp
        show "L.cod (H⇩L a' μ) = H⇩L 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 "H⇩L a' (L.comp ν μ) = L.comp (H⇩L a' ν) (H⇩L a' μ)"
        proof -
          have 1: "L.arr (H⇩L 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 "H⇩L a' (L.comp ν μ) = a' ⋆ (ν ⋅ μ)"
            using μ ν H⇩L_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 (H⇩L a' ν) (H⇩L a' μ)"
            using assms μ 1 2 preserves_arr L.comp_char L.inclusion H⇩L_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_hcomp⇩R⇩W⇩C:
    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_hcomp⇩W⇩C 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_hcomp⇩W⇩C composable_if_connected sources_cod targets_cod
          by auto
        ultimately show "ide ((ν ⋆ μ) ⋅ (inv ν ⋆ inv μ))"
          by presburger
      qed
      thus "iso (ν ⋆ μ)" by auto
    qed

    lemma inv_hcomp⇩R⇩W⇩C:
    assumes "iso μ" and "iso ν" and "sources ν ∩ targets μ ≠ {}"
    shows "inv (ν ⋆ μ) = inv ν ⋆ inv μ"
      using assms iso_hcomp⇩R⇩W⇩C(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_vhom⇩A⇩W⇩C:
           "⟦ ide f; ide g; ide h; f ⋆ g ≠ null; g ⋆ h ≠ null ⟧ ⟹
              «𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»"
  and assoc_naturality⇩A⇩W⇩C:
           "⟦ τ ⋆ μ ≠ null; μ ⋆ ν ≠ null ⟧ ⟹
              𝖺[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) = (τ ⋆ μ ⋆ ν) ⋅ 𝖺[dom τ, dom μ, dom ν]"
  and iso_assoc⇩A⇩W⇩C: "⟦ ide f; ide g; ide h; f ⋆ g ≠ null; g ⋆ h ≠ null ⟧ ⟹ iso 𝖺[f, g, h]"
  and pentagon⇩A⇩W⇩C:
           "⟦ 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_hom⇩A⇩W⇩C:
    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_vhom⇩A⇩W⇩C 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_simps⇩A⇩W⇩C [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_hom⇩A⇩W⇩C 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_hom⇩A⇩W⇩C:
    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_hom⇩A⇩W⇩C iso_assoc⇩A⇩W⇩C 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'_simps⇩A⇩W⇩C [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_hom⇩A⇩W⇩C 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'_naturality⇩A⇩W⇩C:
    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_hom⇩A⇩W⇩C iso_assoc⇩A⇩W⇩C 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_naturality⇩A⇩W⇩C 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_assoc⇩A⇩W⇩C assoc'_in_hom⇩A⇩W⇩C 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 ≡ H⇩R a"

    interpretation R: endofunctor S.comp R
      using weak_unit_a weak_unit_self_composable endofunctor_H⇩R 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 H⇩R_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 H⇩R_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 H⇩R_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_assoc⇩A⇩W⇩C 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 H⇩R_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 H⇩R_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 H⇩R_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_naturality⇩A⇩W⇩C [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 H⇩R_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 ≡ H⇩L b"

    interpretation L: endofunctor S.comp L
      using weak_unit_b weak_unit_self_composable endofunctor_H⇩L 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 H⇩L_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 H⇩L_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 H⇩L_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_hom⇩A⇩W⇩C(3) assoc'_simps⇩A⇩W⇩C(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_assoc⇩A⇩W⇩C 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 H⇩L_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 H⇩L_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 H⇩L_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 H⇩L_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'_naturality⇩A⇩W⇩C [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 H⇩L_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) H⇩R_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) H⇩L_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'› ‹H⇩R a'›
          using assms a' endofunctor_H⇩R 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 H⇩L_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 (H⇩R a' φ) ∧
                  Right_a'.in_hom (H⇩R a' φ) (H⇩R a' (Right_a'.dom φ)) (H⇩R 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 "H⇩R a' φ"]
              by simp
            thus ?thesis
              using φ 1 Right_a'.in_hom_char Right_a'.iso_char H⇩R_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› ‹H⇩L a›
        using assms weak_unit_def by simp
      interpret L': endofunctor ‹Left a› ‹H⇩L a'›
        using a' 1 endofunctor_H⇩L [of a'] by auto
      interpret Φ: natural_isomorphism ‹Left a› ‹Left a› ‹H⇩L a› ‹H⇩L a'› ‹H⇩L φ›
      proof
        fix μ
        show "¬ Left_a.arr μ ⟹ H⇩L φ μ = Left_a.null"
          using left_def φ H⇩L_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 (H⇩L φ μ) = H⇩L 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 H⇩L_def by auto
        show "Left_a.cod (H⇩L φ μ) = H⇩L 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 H⇩L_def
          by auto
        show "Left_a.comp (H⇩L a' μ) (H⇩L φ (Left_a.dom μ)) = H⇩L φ μ"
        proof -
          have "Left_a.comp (H⇩L a' μ) (H⇩L φ (Left_a.dom μ)) =
                Left_a.comp (a' ⋆ μ) (φ ⋆ dom μ)"
            using assms 1 2 φ μ Left_a.dom_char left_def H⇩L_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 H⇩L_def L'.preserves_arr hcomp_simps⇩W⇩C(1) in_homE right_connected
                    paste_1)
              show 4: "Left_a.arr (a' ⋆ μ)"
                using μ H⇩L_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_simps⇩W⇩C(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 H⇩L_def by simp
        qed
        show "Left_a.comp (H⇩L φ (Left_a.cod μ)) (Left_a.L μ) = H⇩L φ μ"
        proof -
          have "Left_a.comp (H⇩L φ (Left_a.cod μ)) (Left_a.L μ) = Left_a.comp (φ ⋆ cod μ) (a ⋆ μ)"
            using assms 1 2 φ μ Left_a.cod_char left_def H⇩L_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) H⇩L_def L.preserves_arr hcomp_simps⇩W⇩C(1)
                    in_homE right_connected paste_2)
              show 4: "Left_a.arr (a ⋆ μ)"
                using assms μ Left_a.arr_char left_def
                using H⇩L_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_simps⇩W⇩C(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 H⇩L_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 (H⇩L φ μ)"
        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_hcomp⇩R⇩W⇩C(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 H⇩L_def
            by simp
        qed
      qed
      interpret L': equivalence_functor ‹Left a'› ‹Left a'› ‹H⇩L a'›
      proof -
        have "naturally_isomorphic (Left a) (Left a) (H⇩L a) Left_a.map"
          using assms Left_a.natural_isomorphism_𝔩 naturally_isomorphic_def by blast
        moreover have "naturally_isomorphic (Left a) (Left a) (H⇩L a) (H⇩L a')"
          using naturally_isomorphic_def Φ.natural_isomorphism_axioms by blast
        ultimately have "naturally_isomorphic (Left a) (Left a) (H⇩L a')
                                              (identity_functor.map (Left a))"
          using naturally_isomorphic_symmetric naturally_isomorphic_transitive by fast
        hence "naturally_isomorphic (Left a') (Left a') (H⇩L a') (identity_functor.map (Left a'))"
          using 1 by auto
        thus "equivalence_functor (Left a') (Left a') (H⇩L 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› ‹H⇩R a›
        using assms weak_unit_def by simp
      interpret R': endofunctor ‹Right a› ‹H⇩R a'›
        using a' 1 endofunctor_H⇩R [of a'] by auto
      interpret Ψ: natural_isomorphism ‹Right a› ‹Right a› ‹H⇩R a› ‹H⇩R a'› ‹H⇩R φ›
      proof
        fix μ
        show "¬ Right_a.arr μ ⟹ H⇩R φ μ = Right_a.null"
          using right_def φ H⇩R_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 (H⇩R φ μ) = H⇩R 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 H⇩R_def
          by auto
        show "Right_a.cod (H⇩R φ μ) = H⇩R 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 H⇩R_def
          by auto
        show "Right_a.comp (H⇩R a' μ) (H⇩R φ (Right_a.dom μ)) = H⇩R φ μ"
        proof -
          have "Right_a.comp (H⇩R a' μ) (H⇩R φ (Right_a.dom μ)) =
                Right_a.comp (μ ⋆ a') (dom μ ⋆ φ)"
            using assms 1 2 φ μ Right_a.dom_char right_def H⇩R_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 H⇩R_def R'.preserves_arr hcomp_simps⇩W⇩C(1) in_homE left_connected
                          paste_2)
              show 4: "Right_a.arr (μ ⋆ a')"
                using μ H⇩R_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_simps⇩W⇩C(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 H⇩R_def by simp
        qed
        show "Right_a.comp (H⇩R φ (Right_a.cod μ)) (Right_a.R μ) = H⇩R φ μ"
        proof -
          have "Right_a.comp (H⇩R φ (Right_a.cod μ)) (Right_a.R μ)
                  = Right_a.comp (cod μ ⋆ φ) (μ ⋆ a)"
            using assms 1 2 φ μ Right_a.cod_char right_def H⇩R_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) H⇩R_def R.preserves_arr hcomp_simps⇩W⇩C(1)
                    in_homE left_connected paste_1)
              show 4: "Right_a.arr (μ ⋆ a)"
                using assms μ Right_a.arr_char right_def
                using H⇩R_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_simps⇩W⇩C(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 H⇩R_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 (H⇩R φ μ)"
        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_hcomp⇩R⇩W⇩C(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 H⇩R_def
            by simp
        qed
      qed
      interpret R': equivalence_functor ‹Right a'› ‹Right a'› ‹H⇩R a'›
      proof -
        have "naturally_isomorphic (Right a) (Right a) (H⇩R a) Right_a.map"
          using assms Right_a.natural_isomorphism_𝔯 naturally_isomorphic_def by blast
        moreover have "naturally_isomorphic (Right a) (Right a) (H⇩R a) (H⇩R a')"
          using naturally_isomorphic_def Ψ.natural_isomorphism_axioms by blast
        ultimately have "naturally_isomorphic (Right a) (Right a) (H⇩R a') Right_a.map"
          using naturally_isomorphic_symmetric naturally_isomorphic_transitive by fast
        hence "naturally_isomorphic (Right a') (Right a') (H⇩R a') 
                 (identity_functor.map (Right a'))"
          using 1 by auto
        thus "equivalence_functor (Right a') (Right a') (H⇩R 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) hseq⇩H⇩H
    where "hseq⇩H⇩H ≡ λμ ν. 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 ‹λμν. hseq⇩H⇩H (fst μν) (snd μν)›
      by (unfold_locales, auto)

    lemma subcategory_VV:
    shows "subcategory VxV.comp (λμν. hseq⇩H⇩H (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_char⇩P⇩B⇩H:
    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_hom⇩P⇩B⇩H:
    assumes "«μ : a →⇩W⇩C b»" and "«ν : b →⇩W⇩C c»"
    shows "«ν ⋆ μ : a →⇩W⇩C c»"
    and "«ν ⋆ μ : dom ν ⋆ dom μ ⇒ cod ν ⋆ cod μ»"
    proof -
      show "«ν ⋆ μ : a →⇩W⇩C 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_char⇩P⇩B:
    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_char⇩P⇩B 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_char⇩P⇩B 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_char⇩P⇩B 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_char⇩P⇩B 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_char⇩P⇩B 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_vhom⇩P⇩B⇩U: "weak_unit a ⟹ «𝗂[a] : a ⋆ a ⇒ a»"
  and iso_unit⇩P⇩B⇩U: "weak_unit a ⟹ iso 𝗂[a]"
  begin

    lemma unit_in_hom⇩P⇩B⇩U:
    assumes "weak_unit a"
    shows "«𝗂[a] : a →⇩W⇩C a»" and "«𝗂[a] : a ⋆ a ⇒ a»"
    proof -
      show 1: "«𝗂[a] : a ⋆ a ⇒ a»"
        using assms unit_in_vhom⇩P⇩B⇩U by auto
      show "«𝗂[a] : a →⇩W⇩C 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_vhom⇩P⇩B⇩U 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 ‹λμν. hseq⇩H⇩H (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