# Theory IsomorphismClass

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

section "Isomorphism Classes"

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

theory IsomorphismClass
imports Category3.EpiMonoIso Category3.NaturalTransformation
begin

context category
begin

notation isomorphic (infix "≅" 50)

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

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

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

lemmas isomorphic_transitive [trans]
lemmas naturally_isomorphic_transitive [trans]

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

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

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

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

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

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

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

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

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

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

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

end

end


# Theory Prebicategory

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

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

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

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

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

theory Prebicategory
imports Category3.EquivalenceOfCategories Category3.Subcategory IsomorphismClass
begin

section "Weak Composition"

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

subsection "Definition"

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

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

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

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

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

interpretation H: partial_magma H
using is_partial_magma by auto

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

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

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

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

lemma hcomp_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
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 σ"]
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 τ"]
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
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
proof -
fix f g
assume fg: "VVV.seq g f"
show "HoVH (VVV.comp g f) = HoVH g ⋅ HoVH f"
proof -
have "VxVxV.comp g f =
(fst g ⋅ fst f, fst (snd g) ⋅ fst (snd f), snd (snd g) ⋅ snd (snd f))"
using fg VVV.seq_char VVV.arr_char VV.arr_char VxVxV.comp_char VxV.comp_char
by (metis (no_types, lifting) VxV.seqE VxVxV.seqE)
hence "HoVH (VVV.comp g f) =
fst g ⋅ fst f ⋆ fst (snd g) ⋅ fst (snd f) ⋆ snd (snd g) ⋅ snd (snd f)"
using HoVH_def VVV.comp_simp fg by auto
also have "... = (fst g ⋆ fst (snd g) ⋆ snd (snd g)) ⋅
(fst f ⋆ fst (snd f) ⋆ snd (snd f))"
using fg VVV.seq_char VVV.arr_char VV.arr_char interchange
by (metis (no_types, lifting) VxV.seqE VxVxV.seqE hseqI' src_vcomp trg_vcomp)
also have "... = HoVH g ⋅ HoVH f"
using fg VVV.seq_char VVV.arr_char HoVH_def VVV.comp_char VV.arr_char
by (metis (no_types, lifting))
finally show ?thesis by simp
qed
qed

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

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

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

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

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

end

end


# Theory Bicategory

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

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

section "Bicategories"

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

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

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

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

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

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

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

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

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

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

end

subsection "Categories Induce Bicategories"

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

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

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

abbreviation V
where "V ≡ V.comp"

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

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

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

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

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

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

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

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

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

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

abbreviation 𝗂
where "𝗂 ≡ λx. x"

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

end

subsection "Monoidal Categories induce Bicategories"

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

context monoidal_category
begin

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

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

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

interpretation H: "functor" CC'.comp C ‹λμν. fst μν ⊗ snd μν›
using CC'_eq_CC T.functor_axioms by simp
interpretation H: horizontal_composition C tensor I.map I.map
by (unfold_locales, simp_all)

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

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

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

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

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

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

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

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

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

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

end

subsection "Prebicategories Extend to Bicategories"

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

context prebicategory_with_homs
begin

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

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

end

sublocale prebicategory_with_homs ⊆ horizontal_composition V H src trg
using induces_horizontal_composition by auto

locale prebicategory_with_homs_and_units =
prebicategory_with_units +
prebicategory_with_homs
begin

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma α_ide_simp [simp]:
assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
shows "α f g h = 𝖺[f, g, h]"
proof -
have "α f g h = (f ⋆ g ⋆ h) ⋅ 𝖺[dom f, dom g, dom h]"
using assms α_def VVV.arr_char [of "(f, g, h)"] by auto
also have "... = (f ⋆ g ⋆ h) ⋅ 𝖺[f, g, h]"
using assms by simp
also have "... = 𝖺[f, g, h]"
using assms α_def assoc_in_hom⇩A⇩W⇩C hcomp_in_hom⇩P⇩B⇩H VVV.arr_char VoV.arr_char
comp_cod_arr composable_char⇩P⇩B⇩H
by auto
finally show ?thesis by simp
qed

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

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

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

end

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

context prebicategory
begin

interpretation prebicategory_with_homs V H 𝖺 some_src some_trg
using extends_to_prebicategory_with_homs by auto

interpretation prebicategory_with_units V H 𝖺 some_unit
using extends_to_prebicategory_with_units by auto

interpretation prebicategory_with_homs_and_units V H 𝖺 some_unit some_src some_trg ..

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

end

section "Bicategories as Prebicategories"

subsection "Bicategories are Prebicategories"

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

context bicategory
begin

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

interpretation weak_composition V H
using is_weak_composition by auto

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

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

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

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

interpret La: endofunctor ‹Left a› ‹H⇩L a›
using assms obj_self_composable endofunctor_H⇩L [of a] by force
interpret La: fully_faithful_functor ‹Left a› ‹Left a› ‹H⇩L a›
proof
show "⋀f f'. Left_a.par f f' ⟹ H⇩L a f = H⇩L a f' ⟹ f = f'"
proof -
fix μ μ'
assume par: "Left_a.par μ μ'"
assume eq: "H⇩L a μ = H⇩L a μ'"
have 1: "par μ μ'"
using par Left_a.arr_char Left_a.dom_char Left_a.cod_char left_def
composable_implies_arr null_agreement
by metis
moreover have "L μ = L μ'"
using par eq H⇩L_def Left_a.arr_char left_def preserves_arr
assms 1 seq_if_composable [of a μ] not_arr_null seq_if_composable [of a μ']
by auto
ultimately show "μ = μ'"
using L.is_faithful by blast
qed
show "⋀f g μ. ⟦ Left_a.ide f; Left_a.ide g; Left_a.in_hom μ (H⇩L a f) (H⇩L a g) ⟧ ⟹
∃ν. Left_a.in_hom ν f g ∧ H⇩L a ν = μ"
proof -
fix f g μ
assume f: "Left_a.ide f" and g: "Left_a.ide g"
and μ: "Left_a.in_hom μ (H⇩L a f) (H⇩L a g)"
have 1: "a = trg f ∧ a = trg g"
using assms f g Left_a.ide_char Left_a.arr_char left_def seq_if_composable [of a f]
seq_if_composable [of a g]
by auto
show "∃ν. Left_a.in_hom ν f g ∧ H⇩L a ν = μ"
proof -
have 2: "∃ν. «ν : f ⇒ g» ∧ L ν = μ"
using f g μ 1 Left_a.ide_char H⇩L_def L.preserves_reflects_arr Left_a.arr_char
Left_a.in_hom_char L.is_full
by force
obtain ν where ν: "«ν : f ⇒ g» ∧ L ν = μ"
using 2 by blast
have "Left_a.arr ν"
using ν 1 trg_dom Left_a.arr_char left_def hseq_char' by fastforce
moreover have "H⇩L a ν = μ"
using ν 1 trg_dom H⇩L_def by auto
ultimately show ?thesis
using ν by force
qed
qed
qed
interpret Ra: endofunctor ‹Right a› ‹H⇩R a›
using assms obj_self_composable endofunctor_H⇩R [of a] by force
interpret Ra: fully_faithful_functor ‹Right a› ‹Right a› ‹H⇩R a›
proof
show "⋀f f'. Right_a.par f f' ⟹ H⇩R a f = H⇩R a f' ⟹ f = f'"
proof -
fix μ μ'
assume par: "Right_a.par μ μ'"
assume eq: "H⇩R a μ = H⇩R a μ'"
have 1: "par μ μ'"
using par Right_a.arr_char Right_a.dom_char Right_a.cod_char right_def
composable_implies_arr null_agreement
by metis
moreover have "R μ = R μ'"
using par eq H⇩R_def Right_a.arr_char right_def preserves_arr
assms 1 seq_if_composable [of μ a] not_arr_null seq_if_composable [of μ' a]
by auto
ultimately show "μ = μ'"
using R.is_faithful by blast
qed
show "⋀f g μ. ⟦ Right_a.ide f; Right_a.ide g; Right_a.in_hom μ (H⇩R a f) (H⇩R a g) ⟧ ⟹
∃ν. Right_a.in_hom ν f g ∧ H⇩R a ν = μ"
proof -
fix f g μ
assume f: "Right_a.ide f" and g: "Right_a.ide g"
and μ: "Right_a.in_hom μ (H⇩R a f) (H⇩R a g)"
have 1: "a = src f ∧ a = src g"
using assms f g Right_a.ide_char Right_a.arr_char right_def seq_if_composable
by auto
show "∃ν. Right_a.in_hom ν f g ∧ H⇩R a ν = μ"
proof -
have 2: "∃ν. «ν : f ⇒ g» ∧ R ν = μ"
using f g μ 1 Right_a.ide_char H⇩R_def R.preserves_reflects_arr Right_a.arr_char
Right_a.in_hom_char R.is_full
by force
obtain ν where ν: "«ν : f ⇒ g» ∧ R ν = μ"
using 2 by blast
have "Right_a.arr ν"
using ν 1 src_dom Right_a.arr_char right_def hseq_char' by fastforce
moreover have "H⇩R a ν = μ"
using ν 1 src_dom H⇩R_def by auto
ultimately show ?thesis
using ν by force
qed
qed
qed
have "isomorphic (a ⋆ a) a ∧ a ⋆ a ≠ null"
using assms obj_self_composable unit_in_hom iso_unit isomorphic_def by blast
thus ?thesis
using La.fully_faithful_functor_axioms Ra.fully_faithful_functor_axioms weak_unit_def
by blast
qed

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

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

lemma weak_unit_cancel_left:
assumes "weak_unit a" and "ide f" and "ide g"
and "a ⋆ f ≅ a ⋆ g"
shows "f ≅ g"
proof -
have 0: "ide a"
using assms weak_unit_def by force
interpret Left_a: subcategory V ‹left a›
using 0 left_hom_is_subcategory by simp
interpret Left_a: left_hom V H a
using assms by unfold_locales auto
interpret La: fully_faithful_functor ‹Left a› ‹Left a› ‹H⇩L a›
using assms weak_unit_def by fast
obtain φ where φ: "iso φ ∧ «φ : a ⋆ f ⇒ a ⋆ g»"
using assms by blast
have 1: "Left_a.iso φ ∧ Left_a.in_hom φ (a ⋆ f) (a ⋆ g)"
proof
have "a ⋆ φ ≠ null"
proof -
have "a ⋆ dom φ ≠ null"
using assms φ weak_unit_self_composable
by (metis arr_dom_iff_arr hseq_char' in_homE match_4)
thus ?thesis
using hom_connected by simp
qed
thus "Left_a.in_hom φ (a ⋆ f) (a ⋆ g)"
using φ Left_a.hom_char left_def by auto
thus "Left_a.iso φ"
using φ Left_a.iso_char by auto
qed
hence 2: "Left_a.ide (a ⋆ f) ∧ Left_a.ide (a ⋆ g)"
using Left_a.ide_dom [of φ] Left_a.ide_cod [of φ] by auto
hence 3: "Left_a.ide f ∧ Left_a.ide g"
by (metis Left_a.ideI Left_a.ide_def Left_a.null_char assms(2) assms(3) left_def)
obtain ψ where ψ: "ψ ∈ Left_a.hom f g ∧ a ⋆ ψ = φ"
using assms 1 2 3 La.is_full [of g f φ] H⇩L_def by auto
have "Left_a.iso ψ"
using ψ 1 H⇩L_def La.reflects_iso by auto
hence "iso ψ ∧ «ψ : f ⇒ g»"
using ψ Left_a.iso_char Left_a.in_hom_char by auto
thus ?thesis by auto
qed

lemma weak_unit_cancel_right:
assumes "weak_unit a" and "ide f" and "ide g"
and "f ⋆ a ≅ g ⋆ a"
shows "f ≅ g"
proof -
have 0: "ide a"
using assms weak_unit_def by force
interpret Right_a: subcategory V ‹right a›
using 0 right_hom_is_subcategory by simp
interpret Right_a: right_hom V H a
using assms by unfold_locales auto
interpret R: fully_faithful_functor ‹Right a› ‹Right a› ‹H⇩R a›
using assms weak_unit_def by fast
obtain φ where φ: "iso φ ∧ in_hom φ (f ⋆ a) (g ⋆ a)"
using assms by blast
have 1: "Right_a.iso φ ∧ φ ∈ Right_a.hom (f ⋆ a) (g ⋆ a)"
proof
have "φ ⋆ a ≠ null"
proof -
have "dom φ ⋆ a ≠ null"
using assms φ weak_unit_self_composable
by (metis arr_dom_iff_arr hseq_char' in_homE match_3)
thus ?thesis
using hom_connected by simp
qed
thus "φ ∈ Right_a.hom (f ⋆ a) (g ⋆ a)"
using φ Right_a.hom_char right_def by simp
thus "Right_a.iso φ"
using φ Right_a.iso_char by auto
qed
hence 2: "Right_a.ide (f ⋆ a) ∧ Right_a.ide (g ⋆ a)"
using Right_a.ide_dom [of φ] Right_a.ide_cod [of φ] `