Theory Bicategory
theory Bicategory
imports Prebicategory Category3.Subcategory Category3.DiscreteCategory
MonoidalCategory.MonoidalCategory
begin
section "Bicategories"
text ‹
A \emph{bicategory} is a (vertical) category that has been equipped with
a horizontal composition, an associativity natural isomorphism,
and for each object a ``unit isomorphism'', such that horizontal
composition on the left by target and on the right by source are
fully faithful endofunctors of the vertical category, and such that
the usual pentagon coherence condition holds for the associativity.
›
locale bicategory =
horizontal_composition V H src trg +
α: natural_isomorphism VVV.comp V HoHV HoVH
‹λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ))› +
L: fully_faithful_functor V V L +
R: fully_faithful_functor V V R
for V :: "'a comp" (infixr ‹⋅› 55)
and H :: "'a ⇒ 'a ⇒ 'a" (infixr ‹⋆› 53)
and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹𝖺[_, _, _]›)
and 𝗂 :: "'a ⇒ 'a" (‹𝗂[_]›)
and src :: "'a ⇒ 'a"
and trg :: "'a ⇒ 'a" +
assumes unit_in_vhom: "obj a ⟹ «𝗂[a] : a ⋆ a ⇒ a»"
and iso_unit: "obj a ⟹ iso 𝗂[a]"
and pentagon: "⟦ ide f; ide g; ide h; ide k; src f = trg g; src g = trg h; src h = trg k ⟧ ⟹
(f ⋆ 𝖺[g, h, k]) ⋅ 𝖺[f, g ⋆ h, k] ⋅ (𝖺[f, g, h] ⋆ k) = 𝖺[f, g, h ⋆ k] ⋅ 𝖺[f ⋆ g, h, k]"
begin
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⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C)
moreover have "HoVH (cod μ, cod ν, cod τ) = cod μ ⋆ cod ν ⋆ cod τ"
using 1 HoVH_def by (simp add: VVV.in_hom_char⇩S⇩b⇩C)
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_naturality1:
assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
shows "𝖺[μ, ν, τ] = (μ ⋆ ν ⋆ τ) ⋅ 𝖺[dom μ, dom ν, dom τ]"
using assms α.naturality1 [of "(μ, ν, τ)"] VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C VVV.dom_char⇩S⇩b⇩C
HoVH_def src_dom trg_dom
by simp
lemma assoc_naturality2:
assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
shows "𝖺[μ, ν, τ] = 𝖺[cod μ, cod ν, cod τ] ⋅ ((μ ⋆ ν) ⋆ τ)"
using assms α.naturality2 [of "(μ, ν, τ)"] VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C VVV.cod_char⇩S⇩b⇩C
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⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C HoVH_def HoHV_def
VVV.dom_char⇩S⇩b⇩C VVV.cod_char⇩S⇩b⇩C
by auto
lemma assoc_in_hom [intro]:
assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
shows "in_hhom 𝖺[f, g, h] (src h) (trg f)"
and "«𝖺[f, g, h] : (dom f ⋆ dom g) ⋆ dom h ⇒ cod f ⋆ cod g ⋆ cod h»"
using assms assoc_in_hom' apply auto[1]
using assms assoc_in_hom' ideD(1) by metis
lemma assoc_simps [simp]:
assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
shows "arr 𝖺[f, g, h]"
and "src 𝖺[f, g, h] = src h" and "trg 𝖺[f, g, h] = trg f"
and "dom 𝖺[f, g, h] = (dom f ⋆ dom g) ⋆ dom h"
and "cod 𝖺[f, g, h] = cod f ⋆ cod g ⋆ cod h"
using assms assoc_in_hom apply auto
using assoc_in_hom(1) by auto
lemma iso_assoc [intro, simp]:
assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
shows "iso 𝖺[f, g, h]"
using assms α.components_are_iso [of "(f, g, h)"] VVV.ide_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
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›.
›
locale category_as_bicategory = category
begin
interpretation V: discrete_category ‹Collect arr› null
using not_arr_null by (unfold_locales, blast)
abbreviation V
where "V ≡ V.comp"
interpretation src: "functor" V V dom
using V.null_char
by (unfold_locales, simp add: has_domain_iff_arr dom_def, auto)
interpretation trg: "functor" V V cod
using V.null_char
by (unfold_locales, simp add: has_codomain_iff_arr cod_def, auto)
interpretation H: horizontal_homs V dom cod
by (unfold_locales, auto)
interpretation H: "functor" H.VV.comp V ‹λμν. fst μν ⋅ snd μν›
apply (unfold_locales)
using H.VV.arr_char⇩S⇩b⇩C V.null_char ext
apply force
using H.VV.arr_char⇩S⇩b⇩C V.null_char H.VV.dom_char⇩S⇩b⇩C H.VV.cod_char⇩S⇩b⇩C
apply auto[3]
proof -
show "⋀g f. H.VV.seq g f ⟹
fst (H.VV.comp g f) ⋅ snd (H.VV.comp g f) = V (fst g ⋅ snd g) (fst f ⋅ snd f)"
proof -
have 0: "⋀f. H.VV.arr f ⟹ V.arr (fst f ⋅ snd f)"
using H.VV.arr_char⇩S⇩b⇩C by auto
have 1: "⋀f g. V.seq g f ⟹ V.ide f ∧ g = f"
using V.arr_char V.dom_char V.cod_char V.not_arr_null by force
have 2: "⋀f g. H.VxV.seq g f ⟹ H.VxV.ide f ∧ g = f"
using 1 H.VxV.seq_char by (metis H.VxV.dom_eqI H.VxV.ide_Ide)
fix f g
assume fg: "H.VV.seq g f"
have 3: "H.VV.ide f ∧ f = g"
using fg 2 H.VV.seq_char⇩S⇩b⇩C H.VV.ide_char⇩S⇩b⇩C by blast
show "fst (H.VV.comp g f) ⋅ snd (H.VV.comp g f) = V (fst g ⋅ snd g) (fst f ⋅ snd f)"
using fg 0 1 3 H.VV.comp_char H.VV.arr_char⇩S⇩b⇩C H.VV.ide_char V.arr_char V.comp_char
H.VV.comp_arr_ide
by (metis (no_types, lifting))
qed
qed
interpretation H: horizontal_composition V C dom cod
by (unfold_locales, auto)
abbreviation 𝖺
where "𝖺 f g h ≡ f ⋅ g ⋅ h"
interpretation α: natural_isomorphism H.VVV.comp V H.HoHV H.HoVH
‹λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ))›
apply unfold_locales
using V.null_char ext
apply fastforce
using H.HoHV_def H.HoVH_def H.VVV.arr_char⇩S⇩b⇩C H.VV.arr_char⇩S⇩b⇩C H.VVV.dom_char⇩S⇩b⇩C
H.VV.dom_char⇩S⇩b⇩C H.VVV.cod_char⇩S⇩b⇩C H.VV.cod_char⇩S⇩b⇩C H.VVV.ide_char comp_assoc
by auto
interpretation fully_faithful_functor V V H.R
using comp_arr_dom by (unfold_locales, auto)
interpretation fully_faithful_functor V V H.L
using comp_cod_arr by (unfold_locales, auto)
abbreviation 𝗂
where "𝗂 ≡ λx. x"
proposition induces_bicategory:
shows "bicategory V C 𝖺 𝗂 dom cod"
apply (unfold_locales, auto simp add: comp_assoc)
using comp_arr_dom by fastforce
end
subsection "Monoidal Categories induce Bicategories"
text ‹
In this section we show that our definition of bicategory directly generalizes our
definition of monoidal category:
a monoidal category becomes a bicategory when equipped with the constant-‹ℐ› functors
as src and trg and ‹ι› as the unit isomorphism from ‹ℐ ⊗ ℐ› to ‹ℐ›.
There is a slight mismatch because the bicategory locale assumes that the associator
is given in curried form, whereas for monoidal categories it is given in tupled form.
Ultimately, the monoidal category locale should be revised to also use curried form,
which ends up being more convenient in most situations.
›
context monoidal_category
begin
interpretation I: constant_functor C C ℐ
using unit_in_hom by unfold_locales auto
interpretation horizontal_homs C I.map I.map
by unfold_locales auto
lemma CC_eq_VV:
shows "CC.comp = VV.comp"
proof -
have "⋀g f. CC.comp g f = VV.comp g f"
proof -
fix f g
show "CC.comp g f = VV.comp g f"
proof -
have "CC.seq g f ⟹ CC.comp g f = VV.comp g f"
using VV.comp_char VV.arr_char⇩S⇩b⇩C CC.seq_char
by (elim CC.seqE seqE, simp)
moreover have "¬ CC.seq g f ⟹ CC.comp g f = VV.comp g f"
using VV.seq_char⇩S⇩b⇩C VV.ext VV.null_char CC.ext
by (metis (no_types, lifting))
ultimately show ?thesis by blast
qed
qed
thus ?thesis by blast
qed
lemma CCC_eq_VVV:
shows "CCC.comp = VVV.comp"
proof -
have "⋀g f. CCC.comp g f = VVV.comp g f"
proof -
fix f g
show "CCC.comp g f = VVV.comp g f"
proof -
have "CCC.seq g f ⟹ CCC.comp g f = VVV.comp g f"
by (metis (no_types, lifting) CC.arrE CCC.seqE⇩P⇩C CC_eq_VV I.map_simp
I.preserves_reflects_arr VV.seq_char⇩S⇩b⇩C VVV.arrI⇩S⇩b⇩C VVV.comp_simp VVV.seq_char⇩S⇩b⇩C
trg_vcomp vseq_implies_hpar(1))
moreover have "¬ CCC.seq g f ⟹ CCC.comp g f = VVV.comp g f"
using VVV.seq_char⇩S⇩b⇩C VVV.ext VVV.null_char CCC.ext
by (metis (no_types, lifting))
ultimately show ?thesis by blast
qed
qed
thus ?thesis by blast
qed
interpretation H: "functor" VV.comp C ‹λμν. fst μν ⊗ snd μν›
using CC_eq_VV T.functor_axioms by simp
interpretation H: horizontal_composition C tensor I.map I.map
by (unfold_locales, simp_all)
lemma HoHV_eq_ToTC:
shows "H.HoHV = T.ToTC"
using H.HoHV_def T.ToTC_def CCC_eq_VVV by presburger
lemma HoVH_eq_ToCT:
shows "H.HoVH = T.ToCT"
using H.HoVH_def T.ToCT_def CCC_eq_VVV by presburger
interpretation α: natural_isomorphism VVV.comp C H.HoHV H.HoVH α
using α.natural_isomorphism_axioms CCC_eq_VVV HoHV_eq_ToTC HoVH_eq_ToCT
by simp
lemma R'_eq_R:
shows "H.R = R"
using H.extensionality CC_eq_VV CC.arr_char by force
lemma L'_eq_L:
shows "H.L = L"
using H.extensionality CC_eq_VV CC.arr_char by force
interpretation R': fully_faithful_functor C C H.R
using R'_eq_R R.fully_faithful_functor_axioms by auto
interpretation L': fully_faithful_functor C C H.L
using L'_eq_L L.fully_faithful_functor_axioms by auto
lemma obj_char:
shows "obj a ⟷ a = ℐ"
using obj_def [of a] unit_in_hom by fastforce
proposition induces_bicategory:
shows "bicategory C tensor (λμ ν τ. α (μ, ν, τ)) (λ_. ι) I.map I.map"
using unit_in_hom unit_is_iso pentagon α.extensionality
α.naturality1 α.naturality2 CCC.arrE CCC_eq_VVV
by unfold_locales auto
end
subsection "Prebicategories Extend to Bicategories"
text ‹
In this section, we show that a prebicategory with homs and units extends to a bicategory.
The main work is to show that the endofunctors ‹L› and ‹R› are fully faithful.
We take the left and right unitor isomorphisms, which were obtained via local
constructions in the left and right hom-subcategories defined by a specified
weak unit, and show that in the presence of the chosen sources and targets they
are the components of a global natural isomorphisms ‹𝔩› and ‹𝔯› from the endofunctors
‹L› and ‹R› to the identity functor. A consequence is that functors ‹L› and ‹R› are
endo-equivalences, hence fully faithful.
›
context prebicategory_with_homs
begin
text ‹
Once it is equipped with a particular choice of source and target for each arrow,
a prebicategory determines a horizontal composition.
›
lemma induces_horizontal_composition:
shows "horizontal_composition V H src trg"
proof -
interpret H: "functor" VV.comp V ‹λμν. fst μν ⋆ snd μν›
proof -
have "VV.comp = VoV.comp"
using composable_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⇩S⇩b⇩C Left.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C Right.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C Left.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C
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⇩S⇩b⇩C Right.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C
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⇩S⇩b⇩C Left.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C Right.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C 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⇩S⇩b⇩C trg_dom Left.lunit_char(1) H⇩L_def
Left.arr_char⇩S⇩b⇩C Left.dom_char⇩S⇩b⇩C 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⇩S⇩b⇩C trg_cod Left.lunit_char(1) H⇩L_def
Left.cod_char⇩S⇩b⇩C Left.ide_cod
by force
have 4: "Left.in_hom (Left.L μ) (?b ⋆ dom μ) (?b ⋆ cod μ)"
using 1 Left.L.preserves_hom [of μ "dom μ" "cod μ"] H⇩L_def by auto
show ?thesis
by (metis "1" "2" H⇩L_def Left.comp_simp Left.in_homE Left.lunit_naturality
Left.seqI' lunit_def trg_cod trg_dom)
qed
lemma runit_naturality:
assumes "arr μ"
shows "μ ⋅ 𝗋[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⇩S⇩b⇩C 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⇩S⇩b⇩C trg_dom Right.runit_char(1) [of "Right.dom μ"] H⇩R_def
Right.arr_char⇩S⇩b⇩C Right.dom_char⇩S⇩b⇩C Right.ide_dom assms
by force
have 3: "𝗋[Right.cod μ] ∈ Right.hom (cod μ ⋆ ?a) (cod μ)"
unfolding runit_def
using 1 Right.in_hom_char⇩S⇩b⇩C trg_cod Right.runit_char(1) [of "Right.cod μ"] H⇩R_def
Right.cod_char⇩S⇩b⇩C Right.ide_cod assms
by force
have 4: "Right.R μ ∈ Right.hom (dom μ ⋆ ?a) (cod μ ⋆ ?a)"
using 1 Right.R.preserves_hom [of μ "dom μ" "cod μ"] H⇩R_def by auto
show ?thesis
by (metis "1" "2" H⇩R_def Right.comp_simp Right.in_homE Right.runit_naturality
Right.seqI' runit_def src_cod src_dom)
qed
interpretation L: endofunctor V L
using endofunctor_L by auto
interpretation 𝔩: 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 mono_cancel [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 mono_cancel [of "𝗋[f]" "R 𝗋[f]" "𝗋[R f]"]
by auto
qed
definition α
where "α μ ν τ ≡ if VVV.arr (μ, ν, τ) then
(μ ⋆ ν ⋆ τ) ⋅ 𝖺[dom μ, dom ν, dom τ]
else null"
lemma α_ide_simp [simp]:
assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
shows "α f g h = 𝖺[f, g, h]"
proof -
have "α f g h = (f ⋆ g ⋆ h) ⋅ 𝖺[dom f, dom g, dom h]"
using assms α_def VVV.arr_char⇩S⇩b⇩C [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⇩S⇩b⇩C VoV.arr_char⇩S⇩b⇩C
comp_cod_arr composable_char⇩P⇩B⇩H
by auto
finally show ?thesis by simp
qed
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⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C VVV.dom_char⇩S⇩b⇩C VVV.cod_char⇩S⇩b⇩C
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⇩S⇩b⇩C [of f] VV.arr_char⇩S⇩b⇩C composable_char⇩P⇩B⇩H by auto
thus ?thesis
using f α.map_simp_ide iso_assoc⇩A⇩W⇩C VVV.ide_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C VVV.cod_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C 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
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⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C)
moreover have "HoHV (cod μ, cod ν, cod τ) = (cod μ ⋆ cod ν) ⋆ cod τ"
using 1 HoHV_def by (simp add: VVV.in_hom_char⇩S⇩b⇩C)
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'_naturality1:
assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
shows "𝖺⇧-⇧1[μ, ν, τ] = ((μ ⋆ ν) ⋆ τ) ⋅ 𝖺⇧-⇧1[dom μ, dom ν, dom τ]"
using assms α'.naturality1 [of "(μ, ν, τ)"] VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
VVV.dom_char⇩S⇩b⇩C HoHV_def src_dom trg_dom 𝖺'_def
by simp
lemma assoc'_naturality2:
assumes "arr μ" and "arr ν" and "arr τ" and "src μ = trg ν" and "src ν = trg τ"
shows "𝖺⇧-⇧1[μ, ν, τ] = 𝖺⇧-⇧1[cod μ, cod ν, cod τ] ⋅ (μ ⋆ ν ⋆ τ)"
using assms α'.naturality2 [of "(μ, ν, τ)"] VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
VVV.cod_char⇩S⇩b⇩C 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'_naturality1 assoc'_naturality2 by metis
lemma assoc'_in_hom [intro]:
assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
shows "in_hhom 𝖺⇧-⇧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⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.ide_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C α'.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⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.ide_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C α'.map_ide_simp
α'.inverts_components 𝖺'_def
by auto
lemma iso_assoc' [intro, simp]:
assumes "ide f" and "ide g" and "ide h"
and "src f = trg g" and "src g = trg h"
shows "iso 𝖺⇧-⇧1[f, g, h]"
using assms by simp
lemma comp_assoc_assoc' [simp]:
assumes "ide f" and "ide g" and "ide h"
and "src f = trg g" and "src g = trg h"
shows "𝖺[f, g, h] ⋅ 𝖺⇧-⇧1[f, g, h] = f ⋆ g ⋆ h"
and "𝖺⇧-⇧1[f, g, h] ⋅ 𝖺[f, g, h] = (f ⋆ g) ⋆ h"
using assms comp_arr_inv' comp_inv_arr' by auto
lemma unit_in_hom [intro, simp]:
assumes "obj a"
shows "«𝗂[a] : a → a»" and "«𝗂[a] : a ⋆ a ⇒ a»"
proof -
show "«𝗂[a] : a ⋆ a ⇒ a»"
using assms unit_in_vhom by simp
thus "«𝗂[a] : a → a»"
using assms
by (metis arrI in_hhom_def obj_simps(2-3) vconn_implies_hpar(1-4))
qed
interpretation weak_composition V H
using is_weak_composition by auto
lemma seq_if_composable:
assumes "ν ⋆ μ ≠ null"
shows "src ν = trg μ"
using assms H.extensionality [of "(ν, μ)"] VV.arr_char⇩S⇩b⇩C by auto
lemma obj_self_composable:
assumes "obj a"
shows "a ⋆ a ≠ null"
and "isomorphic (a ⋆ a) a"
apply (metis arr_dom_iff_arr assms in_homE not_arr_null unit_in_vhom)
by (meson assms iso_unit isomorphic_def unit_in_vhom)
lemma obj_is_weak_unit:
assumes "obj a"
shows "weak_unit a"
proof -
interpret Left_a: subcategory V ‹left a›
using assms left_hom_is_subcategory by force
interpret Right_a: subcategory V ‹right a›
using assms right_hom_is_subcategory by force
text ‹
We know that ‹H⇩L a› is fully faithful as a global endofunctor,
but the definition of weak unit involves its restriction to a
subcategory. So we have to verify that the restriction
is also a fully faithful functor.
›
interpret La: endofunctor ‹Left a› ‹H⇩L a›
using assms obj_self_composable endofunctor_H⇩L [of a] by force
interpret La: fully_faithful_functor ‹Left a› ‹Left a› ‹H⇩L a›
proof
show "⋀f f'. Left_a.par f f' ⟹ H⇩L a f = H⇩L a f' ⟹ f = f'"
proof -
fix μ μ'
assume par: "Left_a.par μ μ'"
assume eq: "H⇩L a μ = H⇩L a μ'"
have 1: "par μ μ'"
using par Left_a.arr_char⇩S⇩b⇩C Left_a.dom_char⇩S⇩b⇩C Left_a.cod_char⇩S⇩b⇩C left_def
composable_implies_arr null_agreement
by metis
moreover have "L μ = L μ'"
using par eq H⇩L_def Left_a.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C 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⇩S⇩b⇩C H⇩L_def L.preserves_reflects_arr Left_a.arr_char⇩S⇩b⇩C
Left_a.in_hom_char⇩S⇩b⇩C 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⇩S⇩b⇩C left_def hseq_char' by fastforce
moreover have "H⇩L a ν = μ"
using ν 1 trg_dom H⇩L_def by auto
ultimately show ?thesis
using ν Left_a.dom_simp Left_a.cod_simp by blast
qed
qed
qed
interpret Ra: endofunctor ‹Right a› ‹H⇩R a›
using assms obj_self_composable endofunctor_H⇩R [of a] by force
interpret Ra: fully_faithful_functor ‹Right a› ‹Right a› ‹H⇩R a›
proof
show "⋀f f'. Right_a.par f f' ⟹ H⇩R a f = H⇩R a f' ⟹ f = f'"
proof -
fix μ μ'
assume par: "Right_a.par μ μ'"
assume eq: "H⇩R a μ = H⇩R a μ'"
have 1: "par μ μ'"
using par Right_a.arr_char⇩S⇩b⇩C Right_a.dom_char⇩S⇩b⇩C Right_a.cod_char⇩S⇩b⇩C right_def
composable_implies_arr null_agreement
by metis
moreover have "R μ = R μ'"
using par eq H⇩R_def Right_a.arr_char⇩S⇩b⇩C 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⇩S⇩b⇩C 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⇩S⇩b⇩C H⇩R_def R.preserves_reflects_arr Right_a.arr_char⇩S⇩b⇩C
Right_a.in_hom_char⇩S⇩b⇩C 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⇩S⇩b⇩C right_def hseq_char' by fastforce
moreover have "H⇩R a ν = μ"
using ν 1 src_dom H⇩R_def by auto
ultimately show ?thesis
using ν Right_a.dom_simp Right_a.cod_simp by blast
qed
qed
qed
have "isomorphic (a ⋆ a) a ∧ a ⋆ a ≠ null"
using assms obj_self_composable unit_in_hom iso_unit isomorphic_def by blast
thus ?thesis
using La.fully_faithful_functor_axioms Ra.fully_faithful_functor_axioms weak_unit_def
by blast
qed
lemma src_in_sources:
assumes "arr μ"
shows "src μ ∈ sources μ"
using assms obj_is_weak_unit R.preserves_arr hseq_char' by auto
lemma trg_in_targets:
assumes "arr μ"
shows "trg μ ∈ targets μ"
using assms obj_is_weak_unit L.preserves_arr hseq_char' by auto
lemma weak_unit_cancel_left:
assumes "weak_unit a" and "ide f" and "ide g"
and "a ⋆ f ≅ a ⋆ g"
shows "f ≅ g"
proof -
have 0: "ide a"
using assms weak_unit_def by force
interpret Left_a: subcategory V ‹left a›
using 0 left_hom_is_subcategory by simp
interpret Left_a: left_hom V H a
using assms weak_unit_self_composable by unfold_locales auto
interpret La: fully_faithful_functor ‹Left a› ‹Left a› ‹H⇩L a›
using assms weak_unit_def by fast
obtain φ where φ: "iso φ ∧ «φ : a ⋆ f ⇒ a ⋆ g»"
using assms by blast
have 1: "Left_a.iso φ ∧ Left_a.in_hom φ (a ⋆ f) (a ⋆ g)"
by (metis H⇩L_def La.extensionality La.preserves_arr Left_a.dom_closed
Left_a.in_hom_char⇩S⇩b⇩C Left_a.iso_char Left_a.not_arr_null Left_a.null_char φ assms(4)
hom_connected(4) hseq_char' ide_char' in_homE isomorphic_implies_ide(2) left_def)
hence 2: "Left_a.ide (a ⋆ f) ∧ Left_a.ide (a ⋆ g)"
using Left_a.ide_dom [of φ] Left_a.ide_cod [of φ] Left_a.dom_simp Left_a.cod_simp
by auto
hence 3: "Left_a.ide f ∧ Left_a.ide g"
by (metis Left_a.ideI⇩S⇩b⇩C 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⇩S⇩b⇩C by auto
thus ?thesis by auto
qed
lemma weak_unit_cancel_right:
assumes "weak_unit a" and "ide f" and "ide g"
and "f ⋆ a ≅ g ⋆ a"
shows "f ≅ g"
proof -
have 0: "ide a"
using assms weak_unit_def by force
interpret Right_a: subcategory V ‹right a›
using 0 right_hom_is_subcategory by simp
interpret Right_a: right_hom V H a
using assms weak_unit_self_composable by unfold_locales auto
interpret R: fully_faithful_functor ‹Right a› ‹Right a› ‹H⇩R a›
using assms weak_unit_def by fast
obtain φ where φ: "iso φ ∧ in_hom φ (f ⋆ a) (g ⋆ a)"
using assms by blast
have 1: "Right_a.iso φ ∧ φ ∈ Right_a.hom (f ⋆ a) (g ⋆ a)"
proof
have "φ ⋆ a ≠ null"
by (metis φ assms(1,4) hom_connected(3) ideD(1) in_homE isomorphic_implies_ide(2)
match_3 not_arr_null weak_unit_self_composable(3))
thus "φ ∈ Right_a.hom (f ⋆ a) (g ⋆ a)"
using φ Right_a.hom_char right_def by simp
thus "Right_a.iso φ"
using φ Right_a.iso_char by auto
qed
hence 2: "Right_a.ide (f ⋆ a) ∧ Right_a.ide (g ⋆ a)"
using Right_a.ide_dom [of φ] Right_a.ide_cod [of φ] Right_a.dom_simp Right_a.cod_simp
by auto
hence 3: "Right_a.ide f ∧ Right_a.ide g"
using assms Right_a.ide_char⇩S⇩b⇩C Right_a.arr_char⇩S⇩b⇩C right_def Right_a.ide_def Right_a.null_char
by metis
obtain ψ where ψ: "ψ ∈ Right_a.hom f g ∧ ψ ⋆ a = φ"
using assms 1 2 3 R.is_full [of g f φ] H⇩R_def by auto
have "Right_a.iso ψ"
using ψ 1 H⇩R_def R.reflects_iso by auto
hence "iso ψ ∧ «ψ : f ⇒ g»"
using ψ Right_a.iso_char Right_a.in_hom_char⇩S⇩b⇩C by auto
thus ?thesis by auto
qed
text ‹
All sources of an arrow ({\em i.e.}~weak units composable on the right with that arrow)
are isomorphic to the chosen source, and similarly for targets. That these statements
hold was somewhat surprising to me.
›
lemma source_iso_src:
assumes "arr μ" and "a ∈ sources μ"
shows "a ≅ src μ"
proof -
have 0: "ide a"
using assms weak_unit_def by force
have 1: "src a = trg a"
using assms ide_dom sources_def weak_unit_iff_self_target seq_if_composable
weak_unit_self_composable
by simp
obtain φ where φ: "iso φ ∧ «φ : a ⋆ a ⇒ a»"
using assms weak_unit_def by blast
have "a ⋆ src a ≅ src a ⋆ src a"
proof -
have "src a ≅ src a ⋆ src a"
using 0 obj_is_weak_unit weak_unit_def isomorphic_symmetric by auto
moreover have "a ⋆ src a ≅ src a"
proof -
have "a ⋆ a ⋆ src a ≅ a ⋆ src a"
proof -
have "iso (φ ⋆ src a) ∧ «φ ⋆ src a : (a ⋆ a) ⋆ src a ⇒ a ⋆ src a»"
using 0 1 φ ide_in_hom(2) by auto
moreover have "iso 𝖺⇧-⇧1[a, a, src a] ∧
«𝖺⇧-⇧1[a, a, src a] : a ⋆ a ⋆ src a ⇒ (a ⋆ a) ⋆ src a»"
using 0 1 iso_assoc' by force
ultimately show ?thesis
using isos_compose isomorphic_def by auto
qed
thus ?thesis
using assms 0 weak_unit_cancel_left by auto
qed
ultimately show ?thesis
using isomorphic_transitive by meson
qed
hence "a ≅ src a"
using 0 weak_unit_cancel_right [of "src a" a "src a"] obj_is_weak_unit by auto
thus ?thesis using assms seq_if_composable 1 by auto
qed
lemma target_iso_trg:
assumes "arr μ" and "b ∈ targets μ"
shows "b ≅ trg μ"
proof -
have 0: "ide b"
using assms weak_unit_def by force
have 1: "trg μ = src b"
using assms seq_if_composable by auto
obtain φ where φ: "iso φ ∧ «φ : b ⋆ b ⇒ b»"
using assms weak_unit_def by blast
have "trg b ⋆ b ≅ trg b ⋆ trg b"
proof -
have "trg b ≅ trg b ⋆ trg b"
using 0 obj_is_weak_unit weak_unit_def isomorphic_symmetric by auto
moreover have "trg b ⋆ b ≅ trg b"
proof -
have "(trg b ⋆ b) ⋆ b ≅ trg b ⋆ b"
proof -
have "iso (trg b ⋆ φ) ∧ «trg b ⋆ φ : trg b ⋆ b ⋆ b ⇒ trg b ⋆ b»"
using assms 0 1 φ ide_in_hom(2) targetsD(1) weak_unit_self_composable
apply (intro conjI hcomp_in_vhom) by auto
moreover have "iso 𝖺[trg b, b, b] ∧
«𝖺[trg b, b, b] : (trg b ⋆ b) ⋆ b ⇒ trg b ⋆ b ⋆ b»"
using assms(2) 0 1 seq_if_composable targetsD(1-2) weak_unit_self_composable
by auto
ultimately show ?thesis
using isos_compose isomorphic_def by auto
qed
thus ?thesis
using assms 0 weak_unit_cancel_right by auto
qed
ultimately show ?thesis
using isomorphic_transitive by meson
qed
hence "b ≅ trg b"
using 0 weak_unit_cancel_left [of "trg b" b "trg b"] obj_is_weak_unit by simp
thus ?thesis
using assms 0 1 seq_if_composable weak_unit_iff_self_source targetsD(1-2) source_iso_src
by simp
qed
lemma is_weak_composition_with_homs:
shows "weak_composition_with_homs V H src trg"
using src_in_sources trg_in_targets seq_if_composable composable_implies_arr
by (unfold_locales, simp_all)
interpretation weak_composition_with_homs V H src trg
using is_weak_composition_with_homs by auto
text ‹
In a bicategory, the notion of composability defined in terms of
the chosen sources and targets coincides with the version defined
for a weak composition, which does not involve particular choices.
›
lemma connected_iff_seq:
assumes "arr μ" and "arr ν"
shows "sources ν ∩ targets μ ≠ {} ⟷ src ν = trg μ"
proof
show "src ν = trg μ ⟹ sources ν ∩ targets μ ≠ {}"
using assms src_in_sources [of ν] trg_in_targets [of μ] by auto
show "sources ν ∩ targets μ ≠ {} ⟹ src ν = trg μ"
proof -
assume 1: "sources ν ∩ targets μ ≠ {}"
obtain a where a: "a ∈ sources ν ∩ targets μ"
using assms 1 by blast
have μ: "arr μ"
using a composable_implies_arr by auto
have ν: "arr ν"
using a composable_implies_arr by auto
have 2: "⋀a'. a' ∈ sources ν ⟹ src a' = src a ∧ trg a' = trg a"
by (metis IntE a seq_if_composable sourcesD(2-3) weak_unit_self_composable(3))
have "src ν = src (src ν)" using ν by simp
also have "... = src (trg μ)"
using ν 2 [of "src ν"] src_in_sources a weak_unit_self_composable seq_if_composable
by auto
also have "... = trg (trg μ)" using μ by simp
also have "... = trg μ" using μ by simp
finally show "src ν = trg μ" by blast
qed
qed
lemma is_associative_weak_composition:
shows "associative_weak_composition V H 𝖺"
proof -
have 1: "⋀ν μ. ν ⋆ μ ≠ null ⟹ src ν = trg μ"
using H.extensionality VV.arr_char⇩S⇩b⇩C by force
show "associative_weak_composition V H 𝖺"
proof
show "⋀f g h. ide f ⟹ ide g ⟹ ide h ⟹ f ⋆ g ≠ null ⟹ g ⋆ h ≠ null ⟹
«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»"
using 1 by auto
show "⋀f g h. ide f ⟹ ide g ⟹ ide h ⟹ f ⋆ g ≠ null ⟹ g ⋆ h ≠ null ⟹
iso 𝖺[f, g, h]"
using 1 iso_assoc by presburger
show "⋀τ μ ν. τ ⋆ μ ≠ null ⟹ μ ⋆ ν ≠ null ⟹
𝖺[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) = (τ ⋆ μ ⋆ ν) ⋅ 𝖺[dom τ, dom μ, dom ν]"
using 1 assoc_naturality hseq_char hseq_char' by metis
show "⋀f g h k. ide f ⟹ ide g ⟹ ide h ⟹ ide k ⟹
sources f ∩ targets g ≠ {} ⟹
sources g ∩ targets h ≠ {} ⟹
sources h ∩ targets k ≠ {} ⟹
(f ⋆ 𝖺[g, h, k]) ⋅ 𝖺[f, g ⋆ h, k] ⋅ (𝖺[f, g, h] ⋆ k) =
𝖺[f, g, h ⋆ k] ⋅ 𝖺[f ⋆ g, h, k]"
using 1 connected_iff_seq pentagon ideD(1) by auto
qed
qed
interpretation associative_weak_composition V H 𝖺
using is_associative_weak_composition by auto
theorem is_prebicategory:
shows "prebicategory V H 𝖺"
using src_in_sources trg_in_targets by (unfold_locales, auto)
interpretation prebicategory V H 𝖺
using is_prebicategory by auto
corollary is_prebicategory_with_homs:
shows "prebicategory_with_homs V H 𝖺 src trg"
..
interpretation prebicategory_with_homs V H 𝖺 src trg
using is_prebicategory_with_homs by auto
text ‹
In a bicategory, an arrow is a weak unit if and only if it is
isomorphic to its chosen source (or to its chosen target).
›
lemma weak_unit_char:
shows "weak_unit a ⟷ a ≅ src a"
and "weak_unit a ⟷ a ≅ trg a"
proof -
show "weak_unit a ⟷ a ≅ src a"
using isomorphism_respects_weak_units isomorphic_symmetric
by (meson ideD(1) isomorphic_implies_ide(2) obj_is_weak_unit obj_src source_iso_src
weak_unit_iff_self_source weak_unit_self_composable(1))
show "weak_unit a ⟷ a ≅ trg a"
using isomorphism_respects_weak_units isomorphic_symmetric
by (metis ‹weak_unit a = isomorphic a (src a)› ideD(1) isomorphic_implies_hpar(3)
isomorphic_implies_ide(1) src_trg target_iso_trg weak_unit_iff_self_target)
qed
interpretation H: partial_composition H
using is_partial_composition by auto
text ‹
Every arrow with respect to horizontal composition is also an arrow with respect
to vertical composition. The converse is not necessarily true.
›
lemma harr_is_varr:
assumes "H.arr μ"
shows "arr μ"
using H.arr_def H.codomains_def H.domains_def assms composable_implies_arr(1)
composable_implies_arr(2)
by auto
text ‹
An identity for horizontal composition is also an identity for vertical composition.
›
lemma horizontal_identity_is_ide:
assumes "H.ide μ"
shows "ide μ"
proof -
have μ: "arr μ"
using assms H.ide_def composable_implies_arr(2) by auto
hence 1: "μ ⋆ dom μ ≠ null"
using assms hom_connected H.ide_def by auto
have "μ ⋆ dom μ = dom μ"
using assms 1 H.ide_def by simp
moreover have "μ ⋆ dom μ = μ"
using assms 1 H.ide_def [of μ] null_agreement
by (metis μ cod_cod cod_dom hcomp_simps⇩W⇩C(3) ideD(2) ide_char' paste_1)
ultimately have "dom μ = μ"
by simp
thus ?thesis
using μ by (metis ide_dom)
qed
text ‹
Every identity for horizontal composition is a weak unit.
›
lemma horizontal_identity_is_weak_unit:
assumes "H.ide μ"
shows "weak_unit μ"
using assms weak_unit_char
by (metis H.ide_def comp_target_ide horizontal_identity_is_ide ideD(1)
isomorphism_respects_weak_units null_agreement targetsD(2-3) trg_in_targets)
end
subsection "Vertically Discrete Bicategories are Categories"
text ‹
In this section we show that if a bicategory is discrete with respect to vertical
composition, then it is a category with respect to horizontal composition.
To obtain this result, we need to establish that the set of arrows for the horizontal
composition coincides with the set of arrows for the vertical composition.
This is not true for a general bicategory, and even with the assumption that the
vertical category is discrete it is not immediately obvious from the definitions.
The issue is that the notion ``arrow'' for the horizontal composition is defined
in terms of the existence of ``domains'' and ``codomains'' with respect to that
composition, whereas the axioms for a bicategory only relate the notion ``arrow''
for the vertical category to the existence of sources and targets with respect
to the horizontal composition.
So we have to establish that, under the assumption of vertical discreteness,
sources coincide with domains and targets coincide with codomains.
We also need the fact that horizontal identities are weak units, which previously
required some effort to show.
›
locale vertically_discrete_bicategory =
bicategory +
assumes vertically_discrete: "ide = arr"
begin
interpretation prebicategory_with_homs V H 𝖺 src trg
using is_prebicategory_with_homs by auto
interpretation H: partial_composition H
using is_partial_composition(1) by auto
lemma weak_unit_is_horizontal_identity:
assumes "weak_unit a"
shows "H.ide a"
proof -
have "a ⋆ a ≠ H.null"
using assms weak_unit_self_composable by simp
moreover have "⋀f. f ⋆ a ≠ H.null ⟹ f ⋆ a = f"
proof -
fix f
assume "f ⋆ a ≠ H.null"
hence "f ⋆ a ≅ f"
using assms comp_ide_source composable_implies_arr(2) sourcesI vertically_discrete
by auto
thus "f ⋆ a = f"
using vertically_discrete isomorphic_def by auto
qed
moreover have "⋀f. a ⋆ f ≠ H.null ⟹ a ⋆ f = f"
proof -
fix f
assume "a ⋆ f ≠ H.null"
hence "a ⋆ f ≅ f"
using assms comp_target_ide composable_implies_arr(1) targetsI vertically_discrete
by auto
thus "a ⋆ f = f"
using vertically_discrete isomorphic_def by auto
qed
ultimately show "H.ide a"
using H.ide_def by simp
qed
lemma sources_eq_domains:
shows "sources μ = H.domains μ"
using weak_unit_is_horizontal_identity H.domains_def sources_def
horizontal_identity_is_weak_unit
by auto
lemma targets_eq_codomains:
shows "targets μ = H.codomains μ"
using weak_unit_is_horizontal_identity H.codomains_def targets_def
horizontal_identity_is_weak_unit
by auto
lemma arr_agreement:
shows "arr = H.arr"
using arr_def H.arr_def arr_iff_has_src arr_iff_has_trg
sources_eq_domains targets_eq_codomains
by auto
interpretation H: category H
proof
show "⋀g f. g ⋆ f ≠ H.null ⟹ H.seq g f"
using arr_agreement hcomp_simps⇩W⇩C(1) by auto
show "⋀f. (H.domains f ≠ {}) = (H.codomains f ≠ {})"
using sources_eq_domains targets_eq_codomains arr_iff_has_src arr_iff_has_trg
by simp
fix f g h
show "H.seq h g ⟹ H.seq (h ⋆ g) f ⟹ H.seq g f"
using null_agreement arr_agreement H.not_arr_null preserves_arr VoV.arr_char⇩S⇩b⇩C
by (metis hseq_char' match_1)
show "H.seq h (g ⋆ f) ⟹ H.seq g f ⟹ H.seq h g"
using null_agreement arr_agreement H.not_arr_null preserves_arr VoV.arr_char⇩S⇩b⇩C
by (metis hseq_char' match_2)
show "H.seq g f ⟹ H.seq h g ⟹ H.seq (h ⋆ g) f"
using arr_agreement match_3 hseq_char(1) by auto
show "H.seq g f ⟹ H.seq h g ⟹ (h ⋆ g) ⋆ f = h ⋆ g ⋆ f"
proof -
assume hg: "H.seq h g"
assume gf: "H.seq g f"
have "iso 𝖺[h, g, f] ∧ «𝖺[h, g, f] : (h ⋆ g) ⋆ f ⇒ h ⋆ g ⋆ f»"
using hg gf vertically_discrete arr_agreement hseq_char assoc_in_hom iso_assoc
by auto
thus ?thesis
using arr_agreement vertically_discrete by auto
qed
qed
proposition is_category:
shows "category H"
..
end
subsection "Obtaining the Unitors"
text ‹
We now want to exploit the construction of unitors in a prebicategory with units,
to obtain left and right unitors in a bicategory. However, a bicategory is not
\emph{a priori} a prebicategory with units, because a bicategory only assigns unit
isomorphisms to each \emph{object}, not to each weak unit. In order to apply the results
about prebicategories with units to a bicategory, we first need to extend the bicategory to
a prebicategory with units, by extending the mapping ‹ι›, which provides a unit isomorphism
for each object, to a mapping that assigns a unit isomorphism to all weak units.
This extension can be made in an arbitrary way, as the values chosen for
non-objects ultimately do not affect the components of the unitors at objects.
›
context bicategory
begin
interpretation prebicategory V H 𝖺
using is_prebicategory by auto
definition 𝗂'
where "𝗂' a ≡ SOME φ. iso φ ∧ φ ∈ hom (a ⋆ a) a ∧ (obj a ⟶ φ = 𝗂[a])"
lemma 𝗂'_extends_𝗂:
assumes "weak_unit a"
shows "iso (𝗂' a)" and "«𝗂' a : a ⋆ a ⇒ a»" and "obj a ⟹ 𝗂' a = 𝗂[a]"
proof -
let ?P = "λa φ. iso φ ∧ «φ : a ⋆ a ⇒ a» ∧ (obj a ⟶ φ = 𝗂[a])"
have "∃φ. ?P a φ"
by (metis assms iso_some_unit(1) iso_some_unit(2) iso_unit unit_in_vhom)
hence 1: "?P a (𝗂' a)"
using 𝗂'_def someI_ex [of "?P a"] by simp
show "iso (𝗂' a)" using 1 by simp
show "«𝗂' a : a ⋆ a ⇒ a»" using 1 by simp
show "obj a ⟹ 𝗂' a = 𝗂[a]" using 1 by simp
qed
proposition extends_to_prebicategory_with_units:
shows "prebicategory_with_units V H 𝖺 𝗂'"
using 𝗂'_extends_𝗂 by unfold_locales auto
interpretation PB: prebicategory_with_units V H 𝖺 𝗂'
using extends_to_prebicategory_with_units by auto
interpretation PB: prebicategory_with_homs V H 𝖺 src trg
using is_prebicategory_with_homs by auto
interpretation PB: prebicategory_with_homs_and_units V H 𝖺 𝗂' src trg ..
proposition extends_to_prebicategory_with_homs_and_units:
shows "prebicategory_with_homs_and_units V H 𝖺 𝗂' src trg"
..
definition lunit (‹𝗅[_]›)
where "𝗅[a] ≡ PB.lunit a"
definition runit (‹𝗋[_]›)
where "𝗋[a] ≡ PB.runit a"
abbreviation lunit' (‹𝗅⇧-⇧1[_]›)
where "𝗅⇧-⇧1[a] ≡ inv 𝗅[a]"
abbreviation runit' (‹𝗋⇧-⇧1[_]›)
where "𝗋⇧-⇧1[a] ≡ inv 𝗋[a]"
text ‹
\sloppypar
The characterizations of the left and right unitors that we obtain from locale
@{locale prebicategory_with_homs_and_units} mention the arbitarily chosen extension ‹𝗂'›,
rather than the given ‹𝗂›. We want ``native versions'' for the present context.
›
lemma lunit_char:
assumes "ide f"
shows "«𝗅[f] : L f ⇒ f»" and "L 𝗅[f] = (𝗂[trg f] ⋆ f) ⋅ 𝖺⇧-⇧1[trg f, trg f, f]"
and "∃!μ. «μ : L f ⇒ f» ∧ L μ = (𝗂[trg f] ⋆ f) ⋅ 𝖺⇧-⇧1[trg f, trg f, f]"
proof -
have 1: "trg (PB.lunit f) = trg f"
using assms PB.lunit_char [of f] vconn_implies_hpar(2) vconn_implies_hpar(4)
by metis
show "«𝗅[f] : L f ⇒ f»"
unfolding lunit_def
using assms PB.lunit_char by simp
show "L 𝗅[f] = (𝗂[trg f] ⋆ f) ⋅ 𝖺⇧-⇧1[trg f, trg f, f]"
unfolding lunit_def
using assms 1 PB.lunit_char obj_is_weak_unit 𝗂'_extends_𝗂 by simp
let ?P = "λμ. «μ : L f ⇒ f» ∧ L μ = (𝗂[trg f] ⋆ f) ⋅ 𝖺⇧-⇧1[trg f, trg f, f]"
have "?P = (λμ. «μ : trg f ⋆ f ⇒ f» ∧
trg f ⋆ μ = (𝗂' (trg f) ⋆ f) ⋅ inv 𝖺[trg f, trg f, f])"
proof -
have "⋀μ. «μ : L f ⇒ f» ⟷ «μ : trg f ⋆ f ⇒ f»"
using assms by simp
moreover have "⋀μ. «μ : L f ⇒ f» ⟹
L μ = (𝗂[trg f] ⋆ f) ⋅ 𝖺⇧-⇧1[trg f, trg f, f] ⟷
trg f ⋆ μ = (𝗂' (trg f) ⋆ f) ⋅ inv 𝖺[trg f, trg f, f]"
using calculation obj_is_weak_unit 𝗂'_extends_𝗂 by auto
ultimately show ?thesis by blast
qed
thus "∃!μ. «μ : L f ⇒ f» ∧ L μ = (𝗂[trg f] ⋆ f) ⋅ 𝖺⇧-⇧1[trg f, trg f, f]"
using assms PB.lunit_char by simp
qed
lemma lunit_in_hom [intro]:
assumes "ide f"
shows "«𝗅[f] : src f → trg f»" and "«𝗅[f] : trg f ⋆ f ⇒ f»"
proof -
show "«𝗅[f] : trg f ⋆ f ⇒ f»"
using assms lunit_char by auto
thus "«𝗅[f] : src f → trg f»"
by (metis arrI in_hhomI vconn_implies_hpar(1-4))
qed
lemma lunit_in_vhom [simp]:
assumes "ide f" and "trg f = b"
shows "«𝗅[f] : b ⋆ f ⇒ f»"
using assms by auto
lemma lunit_simps [simp]:
assumes "ide f"
shows "arr 𝗅[f]" and "src 𝗅[f] = src f" and "trg 𝗅[f] = trg f"
and "dom 𝗅[f] = trg f ⋆ f" and "cod 𝗅[f] = f"
using assms lunit_in_hom
apply auto
using assms lunit_in_hom
apply blast
using assms lunit_in_hom
by blast
lemma runit_char:
assumes "ide f"
shows "«𝗋[f] : R f ⇒ f»" and "R 𝗋[f] = (f ⋆ 𝗂[src f]) ⋅ 𝖺[f, src f, src f]"
and "∃!μ. «μ : R f ⇒ f» ∧ R μ = (f ⋆ 𝗂[src f]) ⋅ 𝖺[f, src f, src f]"
proof -
have 1: "src (PB.runit f) = src f"
using assms PB.runit_char [of f] vconn_implies_hpar(1) vconn_implies_hpar(3)
by metis
show "«𝗋[f] : R f ⇒ f»"
unfolding runit_def
using assms PB.runit_char by simp
show "R 𝗋[f] = (f ⋆ 𝗂[src f]) ⋅ 𝖺[f, src f, src f]"
unfolding runit_def
using assms 1 PB.runit_char obj_is_weak_unit 𝗂'_extends_𝗂 by simp
let ?P = "λμ. «μ : R f ⇒ f» ∧ R μ = (f ⋆ 𝗂[src f]) ⋅ 𝖺[f, src f, src f]"
have "?P = (λμ. «μ : f ⋆ src f ⇒ f» ∧
μ ⋆ src f = (f ⋆ 𝗂' (src f)) ⋅ 𝖺[f, src f, src f])"
proof -
have "⋀μ. «μ : R f ⇒ f» ⟷ «μ : f ⋆ src f ⇒ f»"
using assms by simp
moreover have "⋀μ. «μ : R f ⇒ f» ⟹
R μ = (f ⋆ 𝗂[src f]) ⋅ 𝖺[f, src f, src f] ⟷
μ ⋆ src f = (f ⋆ 𝗂' (src f)) ⋅ 𝖺[f, src f, src f]"
using calculation obj_is_weak_unit 𝗂'_extends_𝗂 by auto
ultimately show ?thesis by blast
qed
thus "∃!μ. «μ : R f ⇒ f» ∧ R μ = (f ⋆ 𝗂[src f]) ⋅ 𝖺[f, src f, src f]"
using assms PB.runit_char by simp
qed
lemma runit_in_hom [intro]:
assumes "ide f"
shows "«𝗋[f] : src f → trg f»" and "«𝗋[f] : f ⋆ src f ⇒ f»"
proof -
show "«𝗋[f] : f ⋆ src f ⇒ f»"
using assms runit_char by auto
thus "«𝗋[f] : src f → trg f»"
by (metis arrI in_hhom_def vconn_implies_hpar(1-4))
qed
lemma runit_in_vhom [simp]:
assumes "ide f" and "src f = a"
shows "«𝗋[f] : f ⋆ a ⇒ f»"
using assms by auto
lemma runit_simps [simp]:
assumes "ide f"
shows "arr 𝗋[f]" and "src 𝗋[f] = src f" and "trg 𝗋[f] = trg f"
and "dom 𝗋[f] = f ⋆ src f" and "cod 𝗋[f] = f"
using assms runit_in_hom
apply auto
using assms runit_in_hom
apply blast
using assms runit_in_hom
by blast
lemma lunit_eqI:
assumes "ide f" and "«μ : trg f ⋆ f ⇒ f»"
and "trg f ⋆ μ = (𝗂[trg f] ⋆ f) ⋅ 𝖺⇧-⇧1[trg f, trg f, f]"
shows "μ = 𝗅[f]"
unfolding lunit_def
using assms PB.lunit_eqI 𝗂'_extends_𝗂 trg.preserves_ide obj_is_weak_unit by simp
lemma runit_eqI:
assumes "ide f" and "«μ : f ⋆ src f ⇒ f»"
and "μ ⋆ src f = (f ⋆ 𝗂[src f]) ⋅ 𝖺[f, src f, src f]"
shows "μ = 𝗋[f]"
unfolding runit_def
using assms PB.runit_eqI 𝗂'_extends_𝗂 src.preserves_ide obj_is_weak_unit by simp
lemma lunit_naturality:
assumes "arr μ"
shows "μ ⋅ 𝗅[dom μ] = 𝗅[cod μ] ⋅ (trg μ ⋆ μ)"
unfolding lunit_def
using assms PB.lunit_naturality by auto
lemma runit_naturality:
assumes "arr μ"
shows "μ ⋅ 𝗋[dom μ] = 𝗋[cod μ] ⋅ (μ ⋆ src μ)"
unfolding runit_def
using assms PB.runit_naturality by auto
lemma iso_lunit [simp]:
assumes "ide f"
shows "iso 𝗅[f]"
unfolding lunit_def
using assms PB.iso_lunit by blast
lemma iso_runit [simp]:
assumes "ide f"
shows "iso 𝗋[f]"
unfolding runit_def
using assms PB.iso_runit by blast
lemma iso_lunit' [simp]:
assumes "ide f"
shows "iso 𝗅⇧-⇧1[f]"
using assms iso_lunit by blast
lemma iso_runit' [simp]:
assumes "ide f"
shows "iso 𝗋⇧-⇧1[f]"
using assms iso_runit by blast
lemma lunit'_in_hom [intro]:
assumes "ide f"
shows "«𝗅⇧-⇧1[f] : src f → trg f»" and "«𝗅⇧-⇧1[f] : f ⇒ trg f ⋆ f»"
proof -
show "«𝗅⇧-⇧1[f] : f ⇒ trg f ⋆ f»"
using assms lunit_char iso_lunit by simp
thus "«𝗅⇧-⇧1[f] : src f → trg f»"
using assms src_dom trg_dom by simp
qed
lemma lunit'_in_vhom [simp]:
assumes "ide f" and "trg f = b"
shows "«𝗅⇧-⇧1[f] : f ⇒ b ⋆ f»"
using assms by auto
lemma lunit'_simps [simp]:
assumes "ide f"
shows "arr 𝗅⇧-⇧1[f]" and "src 𝗅⇧-⇧1[f] = src f" and "trg 𝗅⇧-⇧1[f] = trg f"
and "dom 𝗅⇧-⇧1[f] = f" and "cod 𝗅⇧-⇧1[f] = trg f ⋆ f"
using assms lunit'_in_hom by auto
lemma runit'_in_hom [intro]:
assumes "ide f"
shows "«𝗋⇧-⇧1[f] : src f → trg f»" and "«𝗋⇧-⇧1[f] : f ⇒ f ⋆ src f»"
proof -
show "«𝗋⇧-⇧1[f] : f ⇒ f ⋆ src f»"
using assms runit_char iso_runit by simp
thus "«𝗋⇧-⇧1[f] : src f → trg f»"
using src_dom trg_dom
by (simp add: assms)
qed
lemma runit'_in_vhom [simp]:
assumes "ide f" and "src f = a"
shows "«𝗋⇧-⇧1[f] : f ⇒ f ⋆ a»"
using assms by auto
lemma runit'_simps [simp]:
assumes "ide f"
shows "arr 𝗋⇧-⇧1[f]" and "src 𝗋⇧-⇧1[f] = src f" and "trg 𝗋⇧-⇧1[f] = trg f"
and "dom 𝗋⇧-⇧1[f] = f" and "cod 𝗋⇧-⇧1[f] = f ⋆ src f"
using assms runit'_in_hom by auto
interpretation L: endofunctor V L ..
interpretation 𝔩: transformation_by_components V V L map lunit
using lunit_in_hom lunit_naturality by unfold_locales auto
interpretation 𝔩: natural_isomorphism V V L map 𝔩.map
using iso_lunit by (unfold_locales, auto)
lemma natural_isomorphism_𝔩:
shows "natural_isomorphism V V L map 𝔩.map"
..
abbreviation 𝔩
where "𝔩 ≡ 𝔩.map"
lemma 𝔩_ide_simp:
assumes "ide f"
shows "𝔩 f = 𝗅[f]"
using assms by simp
interpretation L: equivalence_functor V V L
using L.isomorphic_to_identity_is_equivalence 𝔩.natural_isomorphism_axioms by simp
lemma equivalence_functor_L:
shows "equivalence_functor V V L"
..
lemma lunit_commutes_with_L:
assumes "ide f"
shows "𝗅[L f] = L 𝗅[f]"
unfolding lunit_def
using assms PB.lunit_commutes_with_L by blast
interpretation R: endofunctor V R ..
interpretation 𝔯: transformation_by_components V V R map runit
using runit_in_hom runit_naturality by unfold_locales auto
interpretation 𝔯: natural_isomorphism V V R map 𝔯.map
using iso_runit by (unfold_locales, auto)
lemma natural_isomorphism_𝔯:
shows "natural_isomorphism V V R map 𝔯.map"
..
abbreviation 𝔯
where "𝔯 ≡ 𝔯.map"
lemma 𝔯_ide_simp:
assumes "ide f"
shows "𝔯 f = 𝗋[f]"
using assms by simp
interpretation R: equivalence_functor V V R
using R.isomorphic_to_identity_is_equivalence 𝔯.natural_isomorphism_axioms by simp
lemma equivalence_functor_R:
shows "equivalence_functor V V R"
..
lemma runit_commutes_with_R:
assumes "ide f"
shows "𝗋[R f] = R 𝗋[f]"
unfolding runit_def
using assms PB.runit_commutes_with_R by blast
lemma lunit'_naturality:
assumes "arr μ"
shows "(trg μ ⋆ μ) ⋅ 𝗅⇧-⇧1[dom μ] = 𝗅⇧-⇧1[cod μ] ⋅ μ"
using assms iso_lunit lunit_naturality invert_opposite_sides_of_square L.preserves_arr
L.preserves_cod arr_cod ide_cod ide_dom lunit_simps(1) lunit_simps(4) seqI
by presburger
lemma runit'_naturality:
assumes "arr μ"
shows "(μ ⋆ src μ) ⋅ 𝗋⇧-⇧1[dom μ] = 𝗋⇧-⇧1[cod μ] ⋅ μ"
using assms iso_runit runit_naturality invert_opposite_sides_of_square R.preserves_arr
R.preserves_cod arr_cod ide_cod ide_dom runit_simps(1) runit_simps(4) seqI
by presburger
lemma isomorphic_unit_right:
assumes "ide f"
shows "f ⋆ src f ≅ f"
using assms runit'_in_hom iso_runit' isomorphic_def isomorphic_symmetric by blast
lemma isomorphic_unit_left:
assumes "ide f"
shows "trg f ⋆ f ≅ f"
using assms lunit'_in_hom iso_lunit' isomorphic_def isomorphic_symmetric by blast
end
subsection "Further Properties of Bicategories"
text ‹
Here we derive further properties of bicategories, now that we
have the unitors at our disposal. This section generalizes the corresponding
development in theory @{theory MonoidalCategory.MonoidalCategory},
which has some diagrams to illustrate the longer calculations.
The present section also includes some additional facts that are now nontrivial
due to the partiality of horizontal composition.
›
context bicategory
begin
lemma unit_simps [simp]:
assumes "obj a"
shows "arr 𝗂[a]" and "src 𝗂[a] = a" and "trg 𝗂[a] = a"
and "dom 𝗂[a] = a ⋆ a" and "cod 𝗂[a] = a"
using assms unit_in_hom by blast+
lemma triangle:
assumes "ide f" and "ide g" and "src g = trg f"
shows "(g ⋆ 𝗅[f]) ⋅ 𝖺[g, src g, f] = 𝗋[g] ⋆ f"
proof -
let ?b = "src g"
have *: "(g ⋆ 𝗅[?b ⋆ f]) ⋅ 𝖺[g, ?b, ?b ⋆ f] = 𝗋[g] ⋆ ?b ⋆ f"
proof -
have 1: "((g ⋆ 𝗅[?b ⋆ f]) ⋅ 𝖺[g, ?b, ?b ⋆ f]) ⋅ 𝖺[g ⋆ ?b, ?b, f]
= (𝗋[g] ⋆ ?b ⋆ f) ⋅ 𝖺[g ⋆ ?b, ?b, f]"
proof -
have "((g ⋆ 𝗅[?b ⋆ f]) ⋅ 𝖺[g, ?b, ?b ⋆ f]) ⋅ 𝖺[g ⋆ ?b, ?b, f]
= (g ⋆ 𝗅[?b ⋆ f]) ⋅ 𝖺[g, ?b, ?b ⋆ f] ⋅ 𝖺[g ⋆ ?b, ?b, f]"
using HoVH_def HoHV_def comp_assoc by auto
also have
"... = (g ⋆ 𝗅[?b ⋆ f]) ⋅ (g ⋆ 𝖺[?b, ?b, f]) ⋅ 𝖺[g, ?b ⋆ ?b, f] ⋅ (𝖺[g, ?b, ?b] ⋆ f)"
using assms pentagon by force
also have
"... = ((g ⋆ 𝗅[?b ⋆ f]) ⋅ (g ⋆ 𝖺[?b, ?b, f])) ⋅ 𝖺[g, ?b ⋆ ?b, f] ⋅ (𝖺[g, ?b, ?b] ⋆ f)"
using assms assoc_in_hom HoVH_def HoHV_def comp_assoc by auto
also have
"... = ((g ⋆ ?b ⋆ 𝗅[f]) ⋅ (g ⋆ 𝖺[?b, ?b, f])) ⋅ 𝖺[g, ?b ⋆ ?b, f] ⋅ (𝖺[g, ?b, ?b] ⋆ f)"
using assms lunit_commutes_with_L lunit_in_hom by force
also have "... = ((g ⋆ (𝗂[?b] ⋆ f) ⋅ 𝖺⇧-⇧1[?b, ?b, f]) ⋅ (g ⋆ 𝖺[?b, ?b, f]))
⋅ 𝖺[g, ?b ⋆ ?b, f] ⋅ (𝖺[g, ?b, ?b] ⋆ f)"
using assms lunit_char(2) by force
also have "... = (g ⋆ ((𝗂[?b] ⋆ f) ⋅ 𝖺⇧-⇧1[?b, ?b, f]) ⋅ 𝖺[?b, ?b, f])
⋅ 𝖺[g, ?b ⋆ ?b, f] ⋅ (𝖺[g, ?b, ?b] ⋆ f)"
using assms interchange [of g g "(𝗂[?b] ⋆ f) ⋅ 𝖺⇧-⇧1[?b, ?b, f]" "𝖺[?b, ?b, f]"]
by auto
also have "... = ((g ⋆ 𝗂[?b] ⋆ f) ⋅ 𝖺[g, ?b ⋆ ?b, f]) ⋅ (𝖺[g, ?b, ?b] ⋆ f)"
using assms comp_arr_dom comp_assoc_assoc' comp_assoc by auto
also have "... = (𝖺[g, ?b, f] ⋅ ((g ⋆ 𝗂[?b]) ⋆ f)) ⋅ (𝖺[g, ?b, ?b] ⋆ f)"
using assms assoc_naturality [of g "𝗂[?b]" f] by simp
also have "... = 𝖺[g, ?b, f] ⋅ ((g ⋆ 𝗂[?b]) ⋅ 𝖺[g, ?b, ?b] ⋆ f)"
using assms interchange [of "g ⋆ 𝗂[?b]" "𝖺[g, ?b, ?b]" f f] comp_assoc by simp
also have "... = 𝖺[g, ?b, f] ⋅ ((𝗋[g] ⋆ ?b) ⋆ f)"
using assms runit_char(2) by force
also have "... = (𝗋[g] ⋆ ?b ⋆ f) ⋅ 𝖺[g ⋆ ?b, ?b, f]"
using assms assoc_naturality [of "𝗋[g]" ?b f] by auto
finally show ?thesis by blast
qed
show "(g ⋆ 𝗅[?b ⋆ f]) ⋅ 𝖺[g, ?b, ?b ⋆ f] = 𝗋[g] ⋆ ?b ⋆ f"
proof -
have "epi 𝖺[g ⋆ ?b, ?b, f]"
using assms preserves_ide iso_assoc iso_is_retraction retraction_is_epi by force
thus ?thesis
using assms 1 epi_cancel by auto
qed
qed
have "(g ⋆ 𝗅[f]) ⋅ 𝖺[g, ?b, f] = ((g ⋆ 𝗅[f]) ⋅ (g ⋆ 𝗅[?b ⋆ f]) ⋅ (g ⋆ ?b ⋆ 𝗅⇧-⇧1[f])) ⋅
(g ⋆ ?b ⋆ 𝗅[f]) ⋅ 𝖺[g, ?b, ?b ⋆ f] ⋅ ((g ⋆ ?b) ⋆ 𝗅⇧-⇧1[f])"
proof -
have "𝖺[g, ?b, f] = (g ⋆ ?b ⋆ 𝗅[f]) ⋅ 𝖺[g, ?b, ?b ⋆ f] ⋅ ((g ⋆ ?b) ⋆ 𝗅⇧-⇧1[f])"
proof -
have "𝖺[g, ?b, f] = (g ⋆ ?b ⋆ f) ⋅ 𝖺[g, ?b, f]"
using assms comp_cod_arr by simp
have "𝖺[g, ?b, f] = ((g ⋆ ?b ⋆ 𝗅[f]) ⋅ (g ⋆ ?b ⋆ 𝗅⇧-⇧1[f])) ⋅ 𝖺[g, ?b, f]"
using assms comp_cod_arr comp_arr_inv' whisker_left [of g]
whisker_left [of ?b "𝗅[f]" "𝗅⇧-⇧1[f]"]
by simp
also have "... = (g ⋆ ?b ⋆ 𝗅[f]) ⋅ 𝖺[g, ?b, ?b ⋆ f] ⋅ ((g ⋆ ?b) ⋆ 𝗅⇧-⇧1[f])"
using assms iso_lunit assoc_naturality [of g ?b "𝗅⇧-⇧1[f]"] comp_assoc by force
finally show ?thesis by blast
qed
moreover have "g ⋆ 𝗅[f] = (g ⋆ 𝗅[f]) ⋅ (g ⋆ 𝗅[?b ⋆ f]) ⋅ (g ⋆ ?b ⋆ 𝗅⇧-⇧1[f])"
proof -
have "(g ⋆ 𝗅[?b ⋆ f]) ⋅ (g ⋆ ?b ⋆ 𝗅⇧-⇧1[f]) = g ⋆ ?b ⋆ f"
proof -
have "(g ⋆ 𝗅[?b ⋆ f]) ⋅ (g ⋆ ?b ⋆ 𝗅⇧-⇧1[f]) = (g ⋆ ?b ⋆ 𝗅[f]) ⋅ (g ⋆ ?b ⋆ 𝗅⇧-⇧1[f])"
using assms lunit_in_hom lunit_commutes_with_L by simp
also have "... = g ⋆ ?b ⋆ f"
using assms comp_arr_inv' whisker_left [of g] whisker_left [of ?b "𝗅[f]" "𝗅⇧-⇧1[f]"]
by simp
finally show ?thesis by blast
qed
thus ?thesis
using assms comp_arr_dom by auto
qed
ultimately show ?thesis by simp
qed
also have "... = (g ⋆ 𝗅[f]) ⋅ (g ⋆ 𝗅[?b ⋆ f]) ⋅ ((g ⋆ ?b ⋆ 𝗅⇧-⇧1[f]) ⋅ (g ⋆ ?b ⋆ 𝗅[f])) ⋅
𝖺[g, ?b, ?b ⋆ f] ⋅ ((g ⋆ ?b) ⋆ 𝗅⇧-⇧1[f])"
using comp_assoc by simp
also have "... = (g ⋆ 𝗅[f]) ⋅ (g ⋆ 𝗅[?b ⋆ f]) ⋅ ((g ⋆ ?b ⋆ (?b ⋆ f)) ⋅
𝖺[g, ?b, ?b ⋆ f]) ⋅ ((g ⋆ ?b) ⋆ 𝗅⇧-⇧1[f])"
using assms iso_lunit comp_inv_arr' interchange [of g g "?b ⋆ 𝗅⇧-⇧1[f]" "?b ⋆ 𝗅[f]"]
interchange [of ?b ?b "𝗅⇧-⇧1[f]" "𝗅[f]"] comp_assoc
by auto
also have "... = (g ⋆ 𝗅[f]) ⋅ ((g ⋆ 𝗅[?b ⋆ f]) ⋅ 𝖺[g, ?b, ?b ⋆ f]) ⋅ ((g ⋆ ?b) ⋆ 𝗅⇧-⇧1[f])"
using assms comp_cod_arr comp_assoc by auto
also have "... = 𝗋[g] ⋆ f"
proof -
have "𝗋[g] ⋆ f = (g ⋆ 𝗅[f]) ⋅ (𝗋[g] ⋆ ?b ⋆ f) ⋅ ((g ⋆ ?b) ⋆ 𝗅⇧-⇧1[f])"
proof -
have "(g ⋆ 𝗅[f]) ⋅ (𝗋[g] ⋆ ?b ⋆ f) ⋅ ((g ⋆ ?b) ⋆ 𝗅⇧-⇧1[f])
= (g ⋆ 𝗅[f]) ⋅ (𝗋[g] ⋅ (g ⋆ ?b) ⋆ (?b ⋆ f) ⋅ 𝗅⇧-⇧1[f])"
using assms iso_lunit interchange [of "𝗋[g]" "g ⋆ ?b" "?b ⋆ f" "𝗅⇧-⇧1[f]"]
by force
also have "... = (g ⋆ 𝗅[f]) ⋅ (𝗋[g] ⋆ 𝗅⇧-⇧1[f])"
using assms comp_arr_dom comp_cod_arr by simp
also have "... = 𝗋[g] ⋆ 𝗅[f] ⋅ 𝗅⇧-⇧1[f]"
using assms interchange [of g "𝗋[g]" "𝗅[f]" "𝗅⇧-⇧1[f]"] comp_cod_arr
by simp
also have "... = 𝗋[g] ⋆ f"
using assms iso_lunit comp_arr_inv' by simp
finally show ?thesis by argo
qed
thus ?thesis using assms * by argo
qed
finally show ?thesis by blast
qed
lemma lunit_hcomp_gen:
assumes "ide f" and "ide g" and "ide h"
and "src f = trg g" and "src g = trg h"
shows "(f ⋆ 𝗅[g ⋆ h]) ⋅ (f ⋆ 𝖺[trg g, g, h]) = f ⋆ 𝗅[g] ⋆ h"
proof -
have "((f ⋆ 𝗅[g ⋆ h]) ⋅ (f ⋆ 𝖺[trg g, g, h])) ⋅ 𝖺[f, trg g ⋆ g, h] ⋅ (𝖺[f, trg g, g] ⋆ h) =
(f ⋆ (𝗅[g] ⋆ h)) ⋅ 𝖺[f, trg g ⋆ g, h] ⋅ (𝖺[f, trg g, g] ⋆ h)"
proof -
have "((f ⋆ 𝗅[g ⋆ h]) ⋅ (f ⋆ 𝖺[trg g, g, h])) ⋅ (𝖺[f, trg g ⋆ g, h] ⋅ (𝖺[f, trg g, g] ⋆ h)) =
((f ⋆ 𝗅[g ⋆ h]) ⋅ 𝖺[f, trg g, g ⋆ h]) ⋅ 𝖺[f ⋆ trg g, g, h]"
using assms pentagon comp_assoc by simp
also have "... = (𝗋[f] ⋆ (g ⋆ h)) ⋅ 𝖺[f ⋆ trg g, g, h]"
using assms triangle [of "g ⋆ h" f] by auto
also have "... = 𝖺[f, g, h] ⋅ ((𝗋[f] ⋆ g) ⋆ h)"
using assms assoc_naturality [of "𝗋[f]" g h] by simp
also have "... = (𝖺[f, g, h] ⋅ ((f ⋆ 𝗅[g]) ⋆ h)) ⋅ (𝖺[f, trg g, g] ⋆ h)"
using assms triangle interchange [of "f ⋆ 𝗅[g]" "𝖺[f, trg g, g]" h h] comp_assoc
by auto
also have "... = (f ⋆ (𝗅[g] ⋆ h)) ⋅ (𝖺[f, trg g ⋆ g, h] ⋅ (𝖺[f, trg g, g] ⋆ h))"
using assms assoc_naturality [of f "𝗅[g]" h] comp_assoc by simp
finally show ?thesis by blast
qed
moreover have "iso (𝖺[f, trg g ⋆ g, h] ⋅ (𝖺[f, trg g, g] ⋆ h))"
using assms iso_assoc isos_compose by simp
ultimately show ?thesis
using assms iso_is_retraction retraction_is_epi
epi_cancel
[of "𝖺[f, trg g ⋆ g, h] ⋅ (𝖺[f, trg g, g] ⋆ h)"
"(f ⋆ 𝗅[g ⋆ h]) ⋅ (f ⋆ 𝖺[trg g, g, h])" "f ⋆ 𝗅[g] ⋆ h"]
by auto
qed
lemma lunit_hcomp:
assumes "ide f" and "ide g" and "src f = trg g"
shows "𝗅[f ⋆ g] ⋅ 𝖺[trg f, f, g] = 𝗅[f] ⋆ g"
and "𝖺⇧-⇧1[trg f, f, g] ⋅ 𝗅⇧-⇧1[f ⋆ g] = 𝗅⇧-⇧1[f] ⋆ g"
and "𝗅[f ⋆ g] = (𝗅[f] ⋆ g) ⋅ 𝖺⇧-⇧1[trg f, f, g]"
and "𝗅⇧-⇧1[f ⋆ g] = 𝖺[trg f, f, g] ⋅ (𝗅⇧-⇧1[f] ⋆ g)"
proof -
show 1: "𝗅[f ⋆ g] ⋅ 𝖺[trg f, f, g] = 𝗅[f] ⋆ g"
proof -
have "L (𝗅[f ⋆ g] ⋅ 𝖺[trg f, f, g]) = L (𝗅[f] ⋆ g)"
using assms interchange [of "trg f" "trg f" "𝗅[f ⋆ g]" "𝖺[trg f, f, g]"] lunit_hcomp_gen
by fastforce
thus ?thesis
using assms L.is_faithful [of "𝗅[f ⋆ g] ⋅ 𝖺[trg f, f, g]" "𝗅[f] ⋆ g"] by force
qed
show "𝖺⇧-⇧1[trg f, f, g] ⋅ 𝗅⇧-⇧1[f ⋆ g] = 𝗅⇧-⇧1[f] ⋆ g"
proof -
have "𝖺⇧-⇧1[trg f, f, g] ⋅ 𝗅⇧-⇧1[f ⋆ g] = inv (𝗅[f ⋆ g] ⋅ 𝖺[trg f, f, g])"
using assms by (simp add: inv_comp)
also have "... = inv (𝗅[f] ⋆ g)"
using 1 by simp
also have "... = 𝗅⇧-⇧1[f] ⋆ g"
using assms by simp
finally show ?thesis by simp
qed
show 2: "𝗅[f ⋆ g] = (𝗅[f] ⋆ g) ⋅ 𝖺⇧-⇧1[trg f, f, g]"
using assms 1 invert_side_of_triangle(2) by auto
show "𝗅⇧-⇧1[f ⋆ g] = 𝖺[trg f, f, g] ⋅ (𝗅⇧-⇧1[f] ⋆ g)"
proof -
have "𝗅⇧-⇧1[f ⋆ g] = inv ((𝗅[f] ⋆ g) ⋅ 𝖺⇧-⇧1[trg f, f, g])"
using 2 by simp
also have "... = 𝖺[trg f, f, g] ⋅ inv (𝗅[f] ⋆ g)"
using assms inv_comp by simp
also have "... = 𝖺[trg f, f, g] ⋅ (𝗅⇧-⇧1[f] ⋆ g)"
using assms by simp
finally show ?thesis by simp
qed
qed
lemma runit_hcomp_gen:
assumes "ide f" and "ide g" and "ide h"
and "src f = trg g" and "src g = trg h"
shows "𝗋[f ⋆ g] ⋆ h = ((f ⋆ 𝗋[g]) ⋆ h) ⋅ (𝖺[f, g, src g] ⋆ h)"
proof -
have "𝗋[f ⋆ g] ⋆ h = ((f ⋆ g) ⋆ 𝗅[h]) ⋅ 𝖺[f ⋆ g, src g, h]"
using assms triangle by simp
also have "... = (𝖺⇧-⇧1[f, g, h] ⋅ (f ⋆ g ⋆ 𝗅[h]) ⋅ 𝖺[f, g, src g ⋆ h]) ⋅ 𝖺[f ⋆ g, src g, h]"
using assms assoc_naturality [of f g "𝗅[h]"] invert_side_of_triangle(1)
by simp
also have "... = 𝖺⇧-⇧1[f, g, h] ⋅ (f ⋆ g ⋆ 𝗅[h]) ⋅ 𝖺[f, g, src g ⋆ h] ⋅ 𝖺[f ⋆ g, src g, h]"
using comp_assoc by simp
also have "... = (𝖺⇧-⇧1[f, g, h] ⋅ (f ⋆ (𝗋[g] ⋆ h))) ⋅ (f ⋆ 𝖺⇧-⇧1[g, src g, h]) ⋅
𝖺[f, g, src g ⋆ h] ⋅ 𝖺[f ⋆ g, src g, h]"
using assms interchange [of f f] triangle comp_assoc
invert_side_of_triangle(2) [of "𝗋[g] ⋆ h" "g ⋆ 𝗅[h]" "𝖺[g, src g, h]"]
by simp
also have "... = ((f ⋆ 𝗋[g]) ⋆ h) ⋅ 𝖺⇧-⇧1[f, g ⋆ src g, h] ⋅ (f ⋆ 𝖺⇧-⇧1[g, src g, h]) ⋅
𝖺[f, g, src g ⋆ h] ⋅ 𝖺[f ⋆ g, src g, h]"
using assms assoc'_naturality [of f "𝗋[g]" h] comp_assoc by simp
also have "... = ((f ⋆ 𝗋[g]) ⋆ h) ⋅ (𝖺[f, g, src g] ⋆ h)"
using assms pentagon [of f g "src g" h] iso_assoc inv_hcomp
invert_side_of_triangle(1)
[of "𝖺[f, g, src g ⋆ h] ⋅ 𝖺[f ⋆ g, src g, h]" "f ⋆ 𝖺[g, src g, h]"
"𝖺[f, g ⋆ src g, h] ⋅ (𝖺[f, g, src g] ⋆ h)"]
invert_side_of_triangle(1)
[of "(f ⋆ 𝖺⇧-⇧1[g, src g, h]) ⋅ 𝖺[f, g, src g ⋆ h] ⋅ 𝖺[f ⋆ g, src g, h]"
"𝖺[f, g ⋆ src g, h]" "𝖺[f, g, src g] ⋆ h"]
by auto
finally show ?thesis by blast
qed
lemma runit_hcomp:
assumes "ide f" and "ide g" and "src f = trg g"
shows "𝗋[f ⋆ g] = (f ⋆ 𝗋[g]) ⋅ 𝖺[f, g, src g]"
and "𝗋⇧-⇧1[f ⋆ g] = 𝖺⇧-⇧1[f, g, src g] ⋅ (f ⋆ 𝗋⇧-⇧1[g])"
and "𝗋[f ⋆ g] ⋅ 𝖺⇧-⇧1[f, g, src g] = f ⋆ 𝗋[g]"
and "𝖺[f, g, src g] ⋅ 𝗋⇧-⇧1[f ⋆ g] = f ⋆ 𝗋⇧-⇧1[g]"
proof -
show 1: "𝗋[f ⋆ g] = (f ⋆ 𝗋[g]) ⋅ 𝖺[f, g, src g]"
using assms interchange [of "f ⋆ 𝗋[g]" "𝖺[f, g, src g]" "src g" "src g"]
runit_hcomp_gen [of f g "src g"]
R.is_faithful [of "(f ⋆ 𝗋[g]) ⋅ (𝖺[f, g, src g])" "𝗋[f ⋆ g]"]
by simp
show "𝗋⇧-⇧1[f ⋆ g] = 𝖺⇧-⇧1[f, g, src g] ⋅ (f ⋆ 𝗋⇧-⇧1[g])"
using assms 1 inv_comp inv_hcomp by auto
show 2: "𝗋[f ⋆ g] ⋅ 𝖺⇧-⇧1[f, g, src g] = f ⋆ 𝗋[g]"
using assms 1 comp_arr_dom comp_cod_arr comp_assoc hseqI' comp_assoc_assoc' by auto
show "𝖺[f, g, src g] ⋅ 𝗋⇧-⇧1[f ⋆ g] = f ⋆ 𝗋⇧-⇧1[g]"
proof -
have "𝖺[f, g, src g] ⋅ 𝗋⇧-⇧1[f ⋆ g] = inv (𝗋[f ⋆ g] ⋅ 𝖺⇧-⇧1[f, g, src g])"
using assms inv_comp by simp
also have "... = inv (f ⋆ 𝗋[g])"
using 2 by simp
also have "... = f ⋆ 𝗋⇧-⇧1[g]"
using assms inv_hcomp [of f "𝗋[g]"] by simp
finally show ?thesis by simp
qed
qed
lemma unitor_coincidence:
assumes "obj a"
shows "𝗅[a] = 𝗂[a]" and "𝗋[a] = 𝗂[a]"
proof -
have "R 𝗅[a] = R 𝗂[a] ∧ R 𝗋[a] = R 𝗂[a]"
proof -
have "R 𝗅[a] = (a ⋆ 𝗅[a]) ⋅ 𝖺[a, a, a]"
using assms lunit_hcomp [of a a] lunit_commutes_with_L [of a] by auto
moreover have "(a ⋆ 𝗅[a]) ⋅ 𝖺[a, a, a] = R 𝗋[a]"
using assms triangle [of a a] by auto
moreover have "(a ⋆ 𝗅[a]) ⋅ 𝖺[a, a, a] = R 𝗂[a]"
proof -
have "(a ⋆ 𝗅[a]) ⋅ 𝖺[a, a, a] = ((𝗂[a] ⋆ a) ⋅ 𝖺⇧-⇧1[a, a, a]) ⋅ 𝖺[a, a, a]"
using assms lunit_char(2) by force
also have "... = R 𝗂[a]"
using assms comp_arr_dom comp_assoc comp_assoc_assoc'
apply (elim objE)
by (simp add: assms)
finally show ?thesis by blast
qed
ultimately show ?thesis by argo
qed
moreover have "par 𝗅[a] 𝗂[a] ∧ par 𝗋[a] 𝗂[a]"
using assms by auto
ultimately have 1: "𝗅[a] = 𝗂[a] ∧ 𝗋[a] = 𝗂[a]"
using R.is_faithful by blast
show "𝗅[a] = 𝗂[a]" using 1 by auto
show "𝗋[a] = 𝗂[a]" using 1 by auto
qed
lemma unit_triangle:
assumes "obj a"
shows "𝗂[a] ⋆ a = (a ⋆ 𝗂[a]) ⋅ 𝖺[a, a, a]"
and "(𝗂[a] ⋆ a) ⋅ 𝖺⇧-⇧1[a, a, a] = a ⋆ 𝗂[a]"
proof -
show 1: "𝗂[a] ⋆ a = (a ⋆ 𝗂[a]) ⋅ 𝖺[a, a, a]"
using assms triangle [of a a] unitor_coincidence by auto
show "(𝗂[a] ⋆ a) ⋅ 𝖺⇧-⇧1[a, a, a] = a ⋆ 𝗂[a]"
using assms 1 invert_side_of_triangle(2) [of "𝗂[a] ⋆ a" "a ⋆ 𝗂[a]" "𝖺[a, a, a]"]
assoc'_eq_inv_assoc
by (metis hseqI' iso_assoc objE obj_def' unit_simps(1) unit_simps(2))
qed
lemma hcomp_assoc_isomorphic:
assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
shows "(f ⋆ g) ⋆ h ≅ f ⋆ g ⋆ h"
using assms assoc_in_hom [of f g h] iso_assoc isomorphic_def by auto
lemma hcomp_arr_obj:
assumes "arr μ" and "obj a" and "src μ = a"
shows "μ ⋆ a = 𝗋⇧-⇧1[cod μ] ⋅ μ ⋅ 𝗋[dom μ]"
and "𝗋[cod μ] ⋅ (μ ⋆ a) ⋅ 𝗋⇧-⇧1[dom μ] = μ"
proof -
show "μ ⋆ a = 𝗋⇧-⇧1[cod μ] ⋅ μ ⋅ 𝗋[dom μ]"
using assms iso_runit runit_naturality comp_cod_arr
by (metis ide_cod ide_dom invert_side_of_triangle(1) runit_simps(1) runit_simps(5) seqI)
show "𝗋[cod μ] ⋅ (μ ⋆ a) ⋅ 𝗋⇧-⇧1[dom μ] = μ"
using assms iso_runit runit_naturality [of μ] comp_cod_arr
by (metis ide_dom invert_side_of_triangle(2) comp_assoc runit_simps(1)
runit_simps(5) seqI)
qed
lemma hcomp_obj_arr:
assumes "arr μ" and "obj b" and "b = trg μ"
shows "b ⋆ μ = 𝗅⇧-⇧1[cod μ] ⋅ μ ⋅ 𝗅[dom μ]"
and "𝗅[cod μ] ⋅ (b ⋆ μ) ⋅ 𝗅⇧-⇧1[dom μ] = μ"
proof -
show "b ⋆ μ = 𝗅⇧-⇧1[cod μ] ⋅ μ ⋅ 𝗅[dom μ]"
using assms iso_lunit lunit_naturality comp_cod_arr
by (metis ide_cod ide_dom invert_side_of_triangle(1) lunit_simps(1) lunit_simps(5) seqI)
show "𝗅[cod μ] ⋅ (b ⋆ μ) ⋅ 𝗅⇧-⇧1[dom μ] = μ"
using assms iso_lunit lunit_naturality [of μ] comp_cod_arr
by (metis ide_dom invert_side_of_triangle(2) comp_assoc lunit_simps(1)
lunit_simps(5) seqI)
qed
lemma hcomp_reassoc:
assumes "arr τ" and "arr μ" and "arr ν"
and "src τ = trg μ" and "src μ = trg ν"
shows "(τ ⋆ μ) ⋆ ν = 𝖺⇧-⇧1[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν) ⋅ 𝖺[dom τ, dom μ, dom ν]"
and "τ ⋆ μ ⋆ ν = 𝖺[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) ⋅ 𝖺⇧-⇧1[dom τ, dom μ, dom ν]"
proof -
show "(τ ⋆ μ) ⋆ ν = 𝖺⇧-⇧1[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν) ⋅ 𝖺[dom τ, dom μ, dom ν]"
proof -
have "(τ ⋆ μ) ⋆ ν = (𝖺⇧-⇧1[cod τ, cod μ, cod ν] ⋅ 𝖺[cod τ, cod μ, cod ν]) ⋅ ((τ ⋆ μ) ⋆ ν)"
using assms comp_assoc_assoc'(2) comp_cod_arr by simp
also have "... = 𝖺⇧-⇧1[cod τ, cod μ, cod ν] ⋅ 𝖺[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν)"
using comp_assoc by simp
also have "... = 𝖺⇧-⇧1[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν) ⋅ 𝖺[dom τ, dom μ, dom ν]"
using assms assoc_naturality by simp
finally show ?thesis by simp
qed
show "τ ⋆ μ ⋆ ν = 𝖺[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) ⋅ 𝖺⇧-⇧1[dom τ, dom μ, dom ν]"
proof -
have "τ ⋆ μ ⋆ ν = (τ ⋆ μ ⋆ ν) ⋅ 𝖺[dom τ, dom μ, dom ν] ⋅ 𝖺⇧-⇧1[dom τ, dom μ, dom ν]"
using assms comp_assoc_assoc'(1) comp_arr_dom by simp
also have "... = ((τ ⋆ μ ⋆ ν) ⋅ 𝖺[dom τ, dom μ, dom ν]) ⋅ 𝖺⇧-⇧1[dom τ, dom μ, dom ν]"
using comp_assoc by simp
also have "... = (𝖺[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν)) ⋅ 𝖺⇧-⇧1[dom τ, dom μ, dom ν]"
using assms assoc_naturality by simp
also have "... = 𝖺[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) ⋅ 𝖺⇧-⇧1[dom τ, dom μ, dom ν]"
using comp_assoc by simp
finally show ?thesis by simp
qed
qed
lemma triangle':
assumes "ide f" and "ide g" and "src f = trg g"
shows "(f ⋆ 𝗅[g]) = (𝗋[f] ⋆ g) ⋅ 𝖺⇧-⇧1[f, src f, g]"
using assms(1-3) invert_side_of_triangle(2) triangle by force
lemma pentagon':
assumes "ide f" and "ide g" and "ide h" and "ide k"
and "src f = trg g" and "src g = trg h" and "src h = trg k"
shows "((𝖺⇧-⇧1[f, g, h] ⋆ k) ⋅ 𝖺⇧-⇧1[f, g ⋆ h, k]) ⋅ (f ⋆ 𝖺⇧-⇧1[g, h, k])
= 𝖺⇧-⇧1[f ⋆ g, h, k] ⋅ 𝖺⇧-⇧1[f, g, h ⋆ k]"
proof -
have "((𝖺⇧-⇧1[f, g, h] ⋆ k) ⋅ 𝖺⇧-⇧1[f, g ⋆ h, k]) ⋅ (f ⋆ 𝖺⇧-⇧1[g, h, k])
= inv ((f ⋆ 𝖺[g, h, k]) ⋅ (𝖺[f, g ⋆ h, k] ⋅ (𝖺[f, g, h] ⋆ k)))"
proof -
have "inv ((f ⋆ 𝖺[g, h, k]) ⋅ (𝖺[f, g ⋆ h, k] ⋅ (𝖺[f, g, h] ⋆ k))) =
inv (𝖺[f, g ⋆ h, k] ⋅ (𝖺[f, g, h] ⋆ k)) ⋅ inv (f ⋆ 𝖺[g, h, k])"
using assms inv_comp [of "𝖺[f, g ⋆ h, k] ⋅ (𝖺[f, g, h] ⋆ k)" "f ⋆ 𝖺[g, h, k]"]
by force
also have "... = (inv (𝖺[f, g, h] ⋆ k) ⋅ inv 𝖺[f, g ⋆ h, k]) ⋅ inv (f ⋆ 𝖺[g, h, k])"
using assms iso_assoc inv_comp by simp
also have "... = ((𝖺⇧-⇧1[f, g, h] ⋆ k) ⋅ 𝖺⇧-⇧1[f, g ⋆ h, k]) ⋅ (f ⋆ 𝖺⇧-⇧1[g, h, k])"
using assms inv_hcomp by simp
finally show ?thesis by simp
qed
also have "... = inv (𝖺[f, g, h ⋆ k] ⋅ 𝖺[f ⋆ g, h, k])"
using assms pentagon by simp
also have "... = 𝖺⇧-⇧1[f ⋆ g, h, k] ⋅ 𝖺⇧-⇧1[f, g, h ⋆ k]"
using assms inv_comp by simp
finally show ?thesis by auto
qed
end
text ‹
The following convenience locale extends @{locale bicategory} by pre-interpreting
the various functors and natural transformations.
›
locale extended_bicategory =
bicategory +
L: equivalence_functor V V L +
R: equivalence_functor V V R +
α: natural_isomorphism VVV.comp V HoHV HoVH
‹λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ))› +
α': inverse_transformation VVV.comp V HoHV HoVH
‹λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ))› +
𝔩: natural_isomorphism V V L map 𝔩 +
𝔩': inverse_transformation V V L map 𝔩 +
𝔯: natural_isomorphism V V R map 𝔯 +
𝔯': inverse_transformation V V R map 𝔯
sublocale bicategory ⊆ extended_bicategory V H 𝖺 𝗂 src trg
proof -
interpret L: equivalence_functor V V L using equivalence_functor_L by auto
interpret R: equivalence_functor V V R using equivalence_functor_R by auto
interpret α': inverse_transformation VVV.comp V HoHV HoVH
‹λμντ. 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ))› ..
interpret 𝔩: natural_isomorphism V V L map 𝔩 using natural_isomorphism_𝔩 by auto
interpret 𝔩': inverse_transformation V V L map 𝔩 ..
interpret 𝔯: natural_isomorphism V V R map 𝔯 using natural_isomorphism_𝔯 by auto
interpret 𝔯': inverse_transformation V V R map 𝔯 ..
interpret extended_bicategory V H 𝖺 𝗂 src trg ..
show "extended_bicategory V H 𝖺 𝗂 src trg" ..
qed
end