Theory Pseudofunctor
section "Pseudofunctors"
theory Pseudofunctor
imports MonoidalCategory.MonoidalFunctor Bicategory Subbicategory InternalEquivalence Coherence
begin
text ‹
The traditional definition of a pseudofunctor ‹F : C → D› between bicategories ‹C› and ‹D›
is in terms of two maps: an ``object map'' ‹F⇩o› that takes objects of ‹C› to objects of ‹D›
and an ``arrow map'' ‹F⇩a› that assigns to each pair of objects ‹a› and ‹b› of ‹C›
a functor ‹F⇩a a b› from the hom-category ‹hom⇩C a b› to the hom-category ‹hom⇩D (F⇩o a) (F⇩o b)›.
In addition, there is assigned to each object ‹a› of ‹C› an invertible 2-cell
‹«Ψ a : F⇩o a ⇒⇩D (F⇩a a a) a»›, and to each pair ‹(f, g)› of composable 1-cells of C there
is assigned an invertible 2-cell ‹«Φ (f, g) : F g ⋆ F f ⇒ F (g ⋆ f)»›, all subject to
naturality and coherence conditions.
In keeping with the ``object-free'' style in which we have been working, we do not wish
to adopt a definition of pseudofunctor that distinguishes between objects and other
arrows. Instead, we would like to understand a pseudofunctor as an ordinary functor between
(vertical) categories that weakly preserves horizontal composition in a suitable sense.
So, we take as a starting point that a pseudofunctor ‹F : C → D› is a functor from
‹C› to ‹D›, when these are regarded as ordinary categories with respect to vertical
composition. Next, ‹F› should preserve source and target, but only ``weakly''
(up to isomorphism, rather than ``on the nose'').
Weak preservation of horizontal composition is expressed by specifying, for each horizontally
composable pair of vertical identities ‹(f, g)› of ‹C›, a ``compositor''
‹«Φ (f, g) : F g ⋆ F f ⇒ F (g ⋆ f)»› in ‹D›, such that the ‹Φ (f, g)› are the components
of a natural isomorphism.
Associators must also be weakly preserved by F; this is expressed by a coherence
condition that relates an associator ‹𝖺⇩C[f, g, h]› in ‹C›, its image ‹F 𝖺⇩C[f, g, h]›,
the associator ‹𝖺⇩D[F f, F g, F h]› in ‹D› and compositors involving ‹f›, ‹g›, and ‹h›.
As regards the weak preservation of unitors, just as for monoidal functors,
which are in fact pseudofunctors between one-object bicategories, it is only necessary
to assume that ‹F 𝗂⇩C[a]› and ‹𝗂⇩D[F a]› are isomorphic in ‹D› for each object ‹a› of ‹C›,
for there is then a canonical way to obtain, for each ‹a›, an isomorphism
‹«Ψ a : src (F a) → F a»› that satisfies the usual coherence conditions relating the
unitors and the associators. Note that the map ‹a ↦ src (F a)› amounts to the traditional
``object map'' ‹F⇩o›, so that this becomes a derived notion, rather than a primitive one.
›
subsection "Weak Arrows of Homs"
text ‹
We begin with a locale that defines a functor between ``horizontal homs'' that preserves
source and target up to isomorphism.
›
locale weak_arrow_of_homs =
C: horizontal_homs C src⇩C trg⇩C +
D: horizontal_homs D src⇩D trg⇩D +
"functor" C D F
for C :: "'c comp" (infixr "⋅⇩C" 55)
and src⇩C :: "'c ⇒ 'c"
and trg⇩C :: "'c ⇒ 'c"
and D :: "'d comp" (infixr "⋅⇩D" 55)
and src⇩D :: "'d ⇒ 'd"
and trg⇩D :: "'d ⇒ 'd"
and F :: "'c ⇒ 'd" +
assumes weakly_preserves_src: "⋀μ. C.arr μ ⟹ D.isomorphic (F (src⇩C μ)) (src⇩D (F μ))"
and weakly_preserves_trg: "⋀μ. C.arr μ ⟹ D.isomorphic (F (trg⇩C μ)) (trg⇩D (F μ))"
begin
lemma isomorphic_src:
assumes "C.obj a"
shows "D.isomorphic (src⇩D (F a)) (F a)"
using assms weakly_preserves_src [of a] D.isomorphic_symmetric by auto
lemma isomorphic_trg:
assumes "C.obj a"
shows "D.isomorphic (trg⇩D (F a)) (F a)"
using assms weakly_preserves_trg [of a] D.isomorphic_symmetric by auto
abbreviation (input) hseq⇩C
where "hseq⇩C μ ν ≡ C.arr μ ∧ C.arr ν ∧ src⇩C μ = trg⇩C ν"
abbreviation (input) hseq⇩D
where "hseq⇩D μ ν ≡ D.arr μ ∧ D.arr ν ∧ src⇩D μ = trg⇩D ν"
lemma preserves_hseq:
assumes "hseq⇩C μ ν"
shows "hseq⇩D (F μ) (F ν)"
by (metis D.isomorphic_def D.src_src D.src_trg D.vconn_implies_hpar(3)
assms preserves_reflects_arr weakly_preserves_src weakly_preserves_trg)
text ‹
Though ‹F› does not preserve objects ``on the nose'', we can recover from it the
usual ``object map'', which does.
It is slightly confusing at first to get used to the idea that applying the
object map of a weak arrow of homs to an object does not give the same thing
as applying the underlying functor, but rather only something isomorphic to it.
The following defines the object map associated with ‹F›.
›
definition map⇩0
where "map⇩0 a ≡ src⇩D (F a)"
lemma map⇩0_simps [simp]:
assumes "C.obj a"
shows "D.obj (map⇩0 a)"
and "src⇩D (map⇩0 a) = map⇩0 a" and "trg⇩D (map⇩0 a) = map⇩0 a"
and "D.dom (map⇩0 a) = map⇩0 a" and "D.cod (map⇩0 a) = map⇩0 a"
using assms map⇩0_def by auto
lemma preserves_src [simp]:
assumes "C.arr μ"
shows "src⇩D (F μ) = map⇩0 (src⇩C μ)"
using assms
by (metis C.src.preserves_arr C.src_src C.trg_src map⇩0_def preserves_hseq)
lemma preserves_trg [simp]:
assumes "C.arr μ"
shows "trg⇩D (F μ) = map⇩0 (trg⇩C μ)"
using assms map⇩0_def preserves_hseq C.src_trg C.trg.preserves_arr by presburger
lemma preserves_hhom [intro]:
assumes "C.arr μ"
shows "D.in_hhom (F μ) (map⇩0 (src⇩C μ)) (map⇩0 (trg⇩C μ))"
using assms by simp
text ‹
We define here the lifting of ‹F› to a functor ‹FF: CC → DD›.
We need this to define the domains and codomains of the compositors.
›
definition FF
where "FF ≡ λμν. if C.VV.arr μν then (F (fst μν), F (snd μν)) else D.VV.null"
sublocale FF: "functor" C.VV.comp D.VV.comp FF
proof -
have 1: "⋀μν. C.VV.arr μν ⟹ D.VV.arr (FF μν)"
unfolding FF_def using C.VV.arr_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C preserves_hseq by simp
show "functor C.VV.comp D.VV.comp FF"
proof
fix μν
show "¬ C.VV.arr μν ⟹ FF μν = D.VV.null"
using FF_def by simp
show "C.VV.arr μν ⟹ D.VV.arr (FF μν)"
using 1 by simp
assume μν: "C.VV.arr μν"
show "D.VV.dom (FF μν) = FF (C.VV.dom μν)"
using μν 1 FF_def C.VV.arr_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C C.VV.dom_simp D.VV.dom_simp
by simp
show "D.VV.cod (FF μν) = FF (C.VV.cod μν)"
using μν 1 FF_def C.VV.arr_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C C.VV.cod_simp D.VV.cod_simp
by simp
next
fix μν τπ
assume 2: "C.VV.seq μν τπ"
show "FF (C.VV.comp μν τπ) = D.VV.comp (FF μν) (FF τπ)"
proof -
have "FF (C.VV.comp μν τπ) = (F (fst μν) ⋅⇩D F (fst τπ), F (snd μν) ⋅⇩D F (snd τπ))"
using 1 2 FF_def C.VV.comp_char C.VxV.comp_char C.VV.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting) C.VV.seq_char⇩S⇩b⇩C C.VxV.seqE⇩P⇩C fst_conv
as_nat_trans.preserves_comp_2 snd_conv)
also have "... = D.VV.comp (FF μν) (FF τπ)"
using 1 2 FF_def D.VV.comp_char D.VxV.comp_char C.VV.arr_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C
C.VV.seq_char⇩S⇩b⇩C C.VxV.seqE⇩P⇩C preserves_seq
by simp meson
finally show ?thesis by simp
qed
qed
qed
lemma functor_FF:
shows "functor C.VV.comp D.VV.comp FF"
..
end
subsection "Definition of Pseudofunctors"
text ‹
I don't much like the term "pseudofunctor", which is suggestive of something that
is ``not really'' a functor. In the development here we can see that a pseudofunctor
is really a \emph{bona fide} functor with respect to vertical composition,
which happens to have in addition a weak preservation property with respect to
horizontal composition.
This weak preservation of horizontal composition is captured by extra structure,
the ``compositors'', which are the components of a natural transformation.
So ``pseudofunctor'' is really a misnomer; it's an actual functor that has been equipped
with additional structure relating to horizontal composition. I would use the term
``bifunctor'' for such a thing, but it seems to not be generally accepted and also tends
to conflict with the usage of that term to refer to an ordinary functor of two
arguments; which I have called a ``binary functor''. Sadly, there seem to be no other
plausible choices of terminology, other than simply ``functor''
(recommended on n-Lab @{url ‹https://ncatlab.org/nlab/show/pseudofunctor›}),
but that is not workable here because we need a name that does not clash with that
used for an ordinary functor between categories.
›
locale pseudofunctor =
C: bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C +
D: bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D +
weak_arrow_of_homs V⇩C src⇩C trg⇩C V⇩D src⇩D trg⇩D F +
FoH⇩C: composite_functor C.VV.comp V⇩C V⇩D ‹λμν. H⇩C (fst μν) (snd μν)› F +
H⇩DoFF: composite_functor C.VV.comp D.VV.comp V⇩D
FF ‹λμν. H⇩D (fst μν) (snd μν)› +
Φ: natural_isomorphism C.VV.comp V⇩D H⇩DoFF.map FoH⇩C.map Φ
for V⇩C :: "'c comp" (infixr "⋅⇩C" 55)
and H⇩C :: "'c comp" (infixr "⋆⇩C" 53)
and 𝖺⇩C :: "'c ⇒ 'c ⇒ 'c ⇒ 'c" ("𝖺⇩C[_, _, _]")
and 𝗂⇩C :: "'c ⇒ 'c" ("𝗂⇩C[_]")
and src⇩C :: "'c ⇒ 'c"
and trg⇩C :: "'c ⇒ 'c"
and V⇩D :: "'d comp" (infixr "⋅⇩D" 55)
and H⇩D :: "'d comp" (infixr "⋆⇩D" 53)
and 𝖺⇩D :: "'d ⇒ 'd ⇒ 'd ⇒ 'd" ("𝖺⇩D[_, _, _]")
and 𝗂⇩D :: "'d ⇒ 'd" ("𝗂⇩D[_]")
and src⇩D :: "'d ⇒ 'd"
and trg⇩D :: "'d ⇒ 'd"
and F :: "'c ⇒ 'd"
and Φ :: "'c * 'c ⇒ 'd" +
assumes assoc_coherence:
"⟦ C.ide f; C.ide g; C.ide h; src⇩C f = trg⇩C g; src⇩C g = trg⇩C h ⟧ ⟹
F 𝖺⇩C[f, g, h] ⋅⇩D Φ (f ⋆⇩C g, h) ⋅⇩D (Φ (f, g) ⋆⇩D F h) =
Φ (f, g ⋆⇩C h) ⋅⇩D (F f ⋆⇩D Φ (g, h)) ⋅⇩D 𝖺⇩D[F f, F g, F h]"
begin
no_notation C.in_hom ("«_ : _ →⇩C _»")
no_notation D.in_hom ("«_ : _ →⇩D _»")
notation C.in_hhom ("«_ : _ →⇩C _»")
notation C.in_hom ("«_ : _ ⇒⇩C _»")
notation D.in_hhom ("«_ : _ →⇩D _»")
notation D.in_hom ("«_ : _ ⇒⇩D _»")
notation C.lunit ("𝗅⇩C[_]")
notation C.runit ("𝗋⇩C[_]")
notation C.lunit' ("𝗅⇩C⇧-⇧1[_]")
notation C.runit' ("𝗋⇩C⇧-⇧1[_]")
notation C.𝖺' ("𝖺⇩C⇧-⇧1[_, _, _]")
notation D.lunit ("𝗅⇩D[_]")
notation D.runit ("𝗋⇩D[_]")
notation D.lunit' ("𝗅⇩D⇧-⇧1[_]")
notation D.runit' ("𝗋⇩D⇧-⇧1[_]")
notation D.𝖺' ("𝖺⇩D⇧-⇧1[_, _, _]")
lemma weakly_preserves_objects:
assumes "C.obj a"
shows "D.isomorphic (map⇩0 a) (F a)"
using assms weakly_preserves_src [of a] D.isomorphic_symmetric by auto
lemma cmp_in_hom [intro]:
assumes "C.ide a" and "C.ide b" and "src⇩C a = trg⇩C b"
shows "«Φ (a, b) : map⇩0 (src⇩C b) →⇩D map⇩0 (trg⇩C a)»"
and "«Φ (a, b) : F a ⋆⇩D F b ⇒⇩D F (a ⋆⇩C b)»"
proof -
show "«Φ (a, b) : F a ⋆⇩D F b ⇒⇩D F (a ⋆⇩C b)»"
using assms C.VV.arr_char⇩S⇩b⇩C C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C FF_def by auto
thus "«Φ (a, b) : map⇩0 (src⇩C b) →⇩D map⇩0 (trg⇩C a)»"
using assms D.vconn_implies_hpar by auto
qed
lemma cmp_simps [simp]:
assumes "C.ide f" and "C.ide g" and "src⇩C f = trg⇩C g"
shows "D.arr (Φ (f, g))"
and "src⇩D (Φ (f, g)) = src⇩D (F g)" and "trg⇩D (Φ (f, g)) = trg⇩D (F f)"
and "D.dom (Φ (f, g)) = F f ⋆⇩D F g" and "D.cod (Φ (f, g)) = F (f ⋆⇩C g)"
using assms cmp_in_hom by simp_all blast+
lemma cmp_in_hom':
assumes "C.arr μ" and "C.arr ν" and "src⇩C μ = trg⇩C ν"
shows "«Φ (μ, ν) : map⇩0 (src⇩C ν) →⇩D map⇩0 (trg⇩C μ)»"
and "«Φ (μ, ν) : F (C.dom μ) ⋆⇩D F (C.dom ν) ⇒⇩D F (C.cod μ ⋆⇩C C.cod ν)»"
proof -
show "«Φ (μ, ν) : F (C.dom μ) ⋆⇩D F (C.dom ν) ⇒⇩D F (C.cod μ ⋆⇩C C.cod ν)»"
using assms C.VV.arr_char⇩S⇩b⇩C C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C FF_def by auto
thus "«Φ (μ, ν) : map⇩0 (src⇩C ν) →⇩D map⇩0 (trg⇩C μ)»"
using assms D.vconn_implies_hpar by auto
qed
lemma cmp_simps':
assumes "C.arr μ" and "C.arr ν" and "src⇩C μ = trg⇩C ν"
shows "D.arr (Φ (μ, ν))"
and "src⇩D (Φ (μ, ν)) = map⇩0 (src⇩C ν)" and "trg⇩D (Φ (μ, ν)) = map⇩0 (trg⇩C μ)"
and "D.dom (Φ (μ, ν)) = F (C.dom μ) ⋆⇩D F (C.dom ν)"
and "D.cod (Φ (μ, ν)) = F (C.cod μ ⋆⇩C C.cod ν)"
using assms cmp_in_hom' by blast+
lemma cmp_components_are_iso [simp]:
assumes "C.ide f" and "C.ide g" and "src⇩C f = trg⇩C g"
shows "D.iso (Φ (f, g))"
using assms C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C by simp
lemma weakly_preserves_hcomp:
assumes "C.ide f" and "C.ide g" and "src⇩C f = trg⇩C g"
shows "D.isomorphic (F f ⋆⇩D F g) (F (f ⋆⇩C g))"
using assms D.isomorphic_def by auto
end
context pseudofunctor
begin
text ‹
The following defines the image of the unit isomorphism ‹𝗂⇩C[a]› under ‹F›.
We will use ‹(F a, 𝗂[a])› as an ``alternate unit'', to substitute for
‹(src⇩D (F a), 𝗂⇩D[src⇩D (F a)])›.
›
abbreviation (input) 𝗂 ("𝗂[_]")
where "𝗂[a] ≡ F 𝗂⇩C[a] ⋅⇩D Φ (a, a)"
lemma 𝗂_in_hom [intro]:
assumes "C.obj a"
shows "«F 𝗂⇩C[a] ⋅⇩D Φ (a, a) : map⇩0 a →⇩D map⇩0 a»"
and "«𝗂[a] : F a ⋆⇩D F a ⇒⇩D F a»"
proof (unfold map⇩0_def)
show "«F 𝗂⇩C[a] ⋅⇩D Φ (a, a) : F a ⋆⇩D F a ⇒⇩D F a»"
using assms preserves_hom cmp_in_hom
by (intro D.comp_in_homI, auto)
show "«F 𝗂⇩C[a] ⋅⇩D Φ (a, a) : src⇩D (F a) →⇩D src⇩D (F a)»"
using assms C.VV.arr_char⇩S⇩b⇩C C.VV.dom_simp C.VV.cod_simp
by (intro D.vcomp_in_hhom D.seqI, auto)
qed
lemma 𝗂_simps [simp]:
assumes "C.obj a"
shows "D.arr (𝗂 a)"
and "src⇩D 𝗂[a] = map⇩0 a" and "trg⇩D 𝗂[a] = map⇩0 a"
and "D.dom 𝗂[a] = F a ⋆⇩D F a" and "D.cod 𝗂[a] = F a"
using assms 𝗂_in_hom by auto
lemma iso_𝗂:
assumes "C.obj a"
shows "D.iso 𝗂[a]"
using assms C.iso_unit C.obj_self_composable(1) C.seq_if_composable
by (meson C.objE D.isos_compose 𝗂_simps(1) cmp_components_are_iso preserves_iso)
text ‹
If ‹a› is an object of ‹C› and we have an isomorphism ‹«Φ (a, a) : F a ⋆⇩D F a ⇒⇩D F (a ⋆⇩C a)»›,
then there is a canonical way to define a compatible isomorphism ‹«Ψ a : map⇩0 a ⇒⇩D F a»›.
Specifically, we take ‹Ψ a› to be the unique isomorphism ‹«ψ : map⇩0 a ⇒⇩D F a»› such that
‹ψ ⋅⇩D 𝗂⇩D[map⇩0 a] = 𝗂[a] ⋅⇩D (ψ ⋆⇩D ψ)›.
›
definition unit
where "unit a ≡ THE ψ. «ψ : map⇩0 a ⇒⇩D F a» ∧ D.iso ψ ∧
ψ ⋅⇩D 𝗂⇩D[map⇩0 a] = 𝗂[a] ⋅⇩D (ψ ⋆⇩D ψ)"
lemma unit_char:
assumes "C.obj a"
shows "«unit a : map⇩0 a ⇒⇩D F a»" and "D.iso (unit a)"
and "unit a ⋅⇩D 𝗂⇩D[map⇩0 a] = 𝗂[a] ⋅⇩D (unit a ⋆⇩D unit a)"
and "∃!ψ. «ψ : map⇩0 a ⇒⇩D F a» ∧ D.iso ψ ∧ ψ ⋅⇩D 𝗂⇩D[map⇩0 a] = 𝗂[a] ⋅⇩D (ψ ⋆⇩D ψ)"
proof -
let ?P = "λψ. «ψ : map⇩0 a ⇒⇩D F a» ∧ D.iso ψ ∧ ψ ⋅⇩D 𝗂⇩D[map⇩0 a] = 𝗂[a] ⋅⇩D (ψ ⋆⇩D ψ)"
show "∃!ψ. ?P ψ"
proof -
have "D.obj (map⇩0 a)"
using assms by simp
moreover have "D.isomorphic (map⇩0 a) (F a)"
unfolding map⇩0_def
using assms isomorphic_src by simp
ultimately show ?thesis
using assms D.unit_unique_upto_unique_iso Φ.preserves_hom 𝗂_in_hom iso_𝗂 by simp
qed
hence 1: "?P (unit a)"
using assms unit_def the1I2 [of ?P ?P] by simp
show "«unit a : map⇩0 a ⇒⇩D F a»" using 1 by simp
show "D.iso (unit a)" using 1 by simp
show "unit a ⋅⇩D 𝗂⇩D[map⇩0 a] = 𝗂[a] ⋅⇩D (unit a ⋆⇩D unit a)"
using 1 by simp
qed
lemma unit_simps [simp]:
assumes "C.obj a"
shows "D.arr (unit a)"
and "src⇩D (unit a) = map⇩0 a" and "trg⇩D (unit a) = map⇩0 a"
and "D.dom (unit a) = map⇩0 a" and "D.cod (unit a) = F a"
using assms unit_char(1)
apply auto
apply (metis D.vconn_implies_hpar(1) map⇩0_simps(2))
by (metis D.vconn_implies_hpar(2) map⇩0_simps(3))
lemma unit_in_hom [intro]:
assumes "C.obj a"
shows "«unit a : map⇩0 a →⇩D map⇩0 a»"
and "«unit a : map⇩0 a ⇒⇩D F a»"
using assms by auto
lemma unit_eqI:
assumes "C.obj a" and "«μ: map⇩0 a ⇒⇩D F a»" and "D.iso μ"
and "μ ⋅⇩D 𝗂⇩D[map⇩0 a] = 𝗂 a ⋅⇩D (μ ⋆⇩D μ)"
shows "μ = unit a"
using assms unit_def unit_char
the1_equality [of "λμ. «μ : map⇩0 a ⇒⇩D F a» ∧ D.iso μ ∧
μ ⋅⇩D 𝗂⇩D[map⇩0 a] = 𝗂[a] ⋅⇩D (μ ⋆⇩D μ)" μ]
by simp
text ‹
The following defines the unique isomorphism satisfying the characteristic conditions
for the left unitor ‹𝗅⇩D[trg⇩D (F f)]›, but using the ``alternate unit'' ‹𝗂[trg⇩C f]›
instead of ‹𝗂⇩D[trg⇩D (F f)]›, which is used to define ‹𝗅⇩D[trg⇩D (F f)]›.
›
definition lF
where "lF f ≡ THE μ. «μ : F (trg⇩C f) ⋆⇩D F f ⇒⇩D F f» ∧
F (trg⇩C f) ⋆⇩D μ =(𝗂[trg⇩C f] ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F (trg⇩C f), F (trg⇩C f), F f]"
lemma lF_char:
assumes "C.ide f"
shows "«lF f : F (trg⇩C f) ⋆⇩D F f ⇒⇩D F f»"
and "F (trg⇩C f) ⋆⇩D lF f = (𝗂[trg⇩C f] ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F (trg⇩C f), F (trg⇩C f), F f]"
and "∃!μ. «μ : F (trg⇩C f) ⋆⇩D F f ⇒⇩D F f» ∧
F (trg⇩C f) ⋆⇩D μ = (𝗂[trg⇩C f] ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F (trg⇩C f), F (trg⇩C f), F f]"
proof -
let ?P = "λμ. «μ : F (trg⇩C f) ⋆⇩D F f ⇒⇩D F f» ∧
F (trg⇩C f) ⋆⇩D μ = (𝗂[trg⇩C f] ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F (trg⇩C f), F (trg⇩C f), F f]"
show "∃!μ. ?P μ"
proof -
interpret Df: prebicategory ‹(⋅⇩D)› ‹(⋆⇩D)› 𝖺⇩D
using D.is_prebicategory by simp
interpret S: subcategory ‹(⋅⇩D)› ‹Df.left (F (trg⇩C f))›
using assms Df.left_hom_is_subcategory by simp
interpret Df: left_hom ‹(⋅⇩D)› ‹(⋆⇩D)› ‹F (trg⇩C f)›
using assms D.weak_unit_char
by unfold_locales simp
interpret Df: left_hom_with_unit ‹(⋅⇩D)› ‹(⋆⇩D)› 𝖺⇩D ‹𝗂[trg⇩C f]› ‹F (trg⇩C f)›
using assms 𝗂_in_hom iso_𝗂 D.weak_unit_char(1) assms weakly_preserves_trg
by unfold_locales auto
have "∃!μ. «μ : Df.L (F f) ⇒⇩S F f» ∧
Df.L μ = (𝗂[trg⇩C f] ⋆⇩D F f) ⋅⇩S 𝖺⇩D⇧-⇧1[F (trg⇩C f), F (trg⇩C f), F f]"
proof -
have "Df.left (F (trg⇩C f)) (F f)"
using assms weakly_preserves_src D.isomorphic_def D.hseq_char D.hseq_char'
Df.left_def
by fastforce
thus ?thesis
using assms Df.lunit_char(3) S.ide_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C by simp
qed
moreover have "Df.L (F f) = F (trg⇩C f) ⋆⇩D F f"
using assms by (simp add: Df.H⇩L_def)
moreover have "⋀μ. Df.L μ = F (trg⇩C f) ⋆⇩D μ"
using Df.H⇩L_def by simp
moreover have "(𝗂[trg⇩C f] ⋆⇩D F f) ⋅⇩S 𝖺⇩D⇧-⇧1[F (trg⇩C f), F (trg⇩C f), F f] =
(𝗂[trg⇩C f] ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F (trg⇩C f), F (trg⇩C f), F f]"
by (metis (no_types, lifting) D.arrI D.ext D.hseqI' D.hseq_char' D.seqE
D.seq_if_composable D.vconn_implies_hpar(1) D.vconn_implies_hpar(2-3)
D.vconn_implies_hpar(4) Df.ι_in_hom Df.arr_ω S.comp_char S.in_hom_char⇩S⇩b⇩C
calculation(1,3))
moreover have "⋀μ. «μ : F (trg⇩C f) ⋆⇩D F f ⇒⇩D F f» ⟷
«μ : F (trg⇩C f) ⋆⇩D F f ⇒⇩S F f»"
using assms S.in_hom_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C
by (metis D.in_homE Df.hom_connected(2) Df.left_def calculation(1-2))
ultimately show ?thesis by simp
qed
hence 1: "?P (lF f)"
using lF_def the1I2 [of ?P ?P] by simp
show "«lF f : F (trg⇩C f) ⋆⇩D F f ⇒⇩D F f»"
using 1 by simp
show "F (trg⇩C f) ⋆⇩D lF f = (𝗂[trg⇩C f] ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F (trg⇩C f), F (trg⇩C f), F f]"
using 1 by simp
qed
lemma lF_simps [simp]:
assumes "C.ide f"
shows "D.arr (lF f)"
and "src⇩D (lF f) = map⇩0 (src⇩C f)" and "trg⇩D (lF f) = map⇩0 (trg⇩C f)"
and "D.dom (lF f) = F (trg⇩C f) ⋆⇩D F f" and "D.cod (lF f) = F f"
using assms lF_char(1)
apply auto[5]
unfolding map⇩0_def
using assms
apply (metis C.ideD(1) D.vconn_implies_hpar(1,3) map⇩0_def preserves_src)
by (metis C.ideD(1) C.src_trg C.trg.preserves_arr D.in_homE D.trg_cod
preserves_src preserves_trg)
text ‹
\sloppypar
The next two lemmas generalize the eponymous results from
@{theory MonoidalCategory.MonoidalFunctor}. See the proofs of those results for diagrams.
›
lemma lunit_coherence1:
assumes "C.ide f"
shows "𝗅⇩D[F f] ⋅⇩D D.inv (unit (trg⇩C f) ⋆⇩D F f) = lF f"
proof -
let ?b = "trg⇩C f"
have 1: "trg⇩D (F f) = map⇩0 ?b"
using assms by simp
have "lF f ⋅⇩D (unit ?b ⋆⇩D F f) = 𝗅⇩D[F f]"
proof -
have "D.par (lF f ⋅⇩D (unit ?b ⋆⇩D F f)) 𝗅⇩D[F f]"
using assms 1 D.lunit_in_hom unit_char(1-2) lF_char(1) D.ideD(1) by auto
moreover have "map⇩0 ?b ⋆⇩D (lF f ⋅⇩D (unit ?b ⋆⇩D F f)) = map⇩0 ?b ⋆⇩D 𝗅⇩D[F f]"
proof -
have "map⇩0 ?b ⋆⇩D (lF f ⋅⇩D (unit ?b ⋆⇩D F f)) =
(map⇩0 ?b ⋆⇩D lF f) ⋅⇩D (map⇩0 ?b ⋆⇩D unit ?b ⋆⇩D F f)"
using assms D.objE [of "map⇩0 (trg⇩C f)"]
D.whisker_left [of "map⇩0 ?b" "lF f" "unit ?b ⋆⇩D F f"]
by auto
also have "... = (map⇩0 ?b ⋆⇩D lF f) ⋅⇩D
(D.inv (unit ?b) ⋆⇩D F ?b ⋆⇩D F f) ⋅⇩D (unit ?b ⋆⇩D unit ?b ⋆⇩D F f)"
proof -
have "(D.inv (unit ?b) ⋆⇩D F ?b ⋆⇩D F f) ⋅⇩D (unit ?b ⋆⇩D unit ?b ⋆⇩D F f) =
D.inv (unit ?b) ⋅⇩D unit ?b ⋆⇩D F ?b ⋅⇩D unit ?b ⋆⇩D F f ⋅⇩D F f"
using assms unit_char(1-2)
D.interchange [of "F ?b" "unit ?b" "F f" "F f"]
D.interchange [of "D.inv (unit ?b)" "unit ?b" "F ?b ⋆⇩D F f" "unit ?b ⋆⇩D F f"]
by simp
also have "... = map⇩0 ?b ⋆⇩D unit ?b ⋆⇩D F f"
using assms unit_char(1-2) [of ?b] D.comp_arr_dom D.comp_cod_arr D.comp_inv_arr
by (simp add: D.inv_is_inverse)
finally show ?thesis by simp
qed
also have "... =
(D.inv (unit ?b) ⋆⇩D F f) ⋅⇩D (F ?b ⋆⇩D lF f) ⋅⇩D (unit ?b ⋆⇩D unit ?b ⋆⇩D F f)"
proof -
have "(map⇩0 ?b ⋆⇩D lF f) ⋅⇩D (D.inv (unit ?b) ⋆⇩D F ?b ⋆⇩D F f) =
(D.inv (unit ?b) ⋆⇩D F f) ⋅⇩D (F ?b ⋆⇩D lF f)"
proof -
have "(map⇩0 ?b ⋆⇩D lF f) ⋅⇩D (D.inv (unit ?b) ⋆⇩D F ?b ⋆⇩D F f) =
D.inv (unit ?b) ⋆⇩D lF f"
using assms unit_char(1-2) lF_char(1) D.comp_arr_dom D.comp_cod_arr
D.interchange [of "map⇩0 ?b" "D.inv (unit ?b)" "lF f" "F ?b ⋆⇩D F f"]
by simp
also have "... = D.inv (unit ?b) ⋅⇩D F ?b ⋆⇩D F f ⋅⇩D lF f"
using assms unit_char(1-2) lF_char(1) D.comp_arr_dom D.comp_cod_arr
D.inv_in_hom
by auto
also have "... = (D.inv (unit ?b) ⋆⇩D F f) ⋅⇩D (F ?b ⋆⇩D lF f)"
using assms unit_char(1-2) lF_char(1) D.inv_in_hom
D.interchange [of "D.inv (unit ?b)" "F ?b" "F f" "lF f"]
by simp
finally show ?thesis by simp
qed
thus ?thesis
using assms unit_char(1-2) D.inv_in_hom D.comp_assoc by metis
qed
also have "... = (D.inv (unit ?b) ⋆⇩D F f) ⋅⇩D (𝗂 ?b ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F ?b, F ?b, F f] ⋅⇩D
(unit ?b ⋆⇩D unit ?b ⋆⇩D F f)"
using assms unit_char(1-2) lF_char(2) D.comp_assoc by auto
also have "... = ((D.inv (unit ?b) ⋆⇩D F f) ⋅⇩D (𝗂 ?b ⋆⇩D F f) ⋅⇩D
((unit ?b ⋆⇩D unit ?b) ⋆⇩D F f)) ⋅⇩D 𝖺⇩D⇧-⇧1[map⇩0 ?b, map⇩0 ?b, F f]"
using assms unit_char(1-2) D.assoc'_naturality [of "unit ?b" "unit ?b" "F f"] D.comp_assoc
by (simp add: ‹trg⇩D (F f) = map⇩0 (trg⇩C f)›)
also have "... = (𝗂⇩D[map⇩0 ?b] ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[map⇩0 ?b, map⇩0 ?b, F f]"
proof -
have "((D.inv (unit ?b) ⋆⇩D F f) ⋅⇩D (𝗂 ?b ⋆⇩D F f) ⋅⇩D ((unit ?b ⋆⇩D unit ?b) ⋆⇩D F f)) =
𝗂⇩D[map⇩0 ?b] ⋆⇩D F f"
proof -
have "((D.inv (unit ?b) ⋆⇩D F f) ⋅⇩D (𝗂 ?b ⋆⇩D F f) ⋅⇩D ((unit ?b ⋆⇩D unit ?b) ⋆⇩D F f)) =
D.inv (unit ?b) ⋅⇩D unit ?b ⋅⇩D 𝗂⇩D[map⇩0 ?b] ⋆⇩D F f"
using assms 1 D.unit_in_hom D.whisker_right [of "F f"] unit_char(2-3)
D.invert_side_of_triangle(1)
by (metis C.ideD(1) C.obj_trg D.seqI' map⇩0_simps(1) unit_in_hom(2) preserves_ide)
also have "... = 𝗂⇩D[map⇩0 ?b] ⋆⇩D F f"
proof -
have "(D.inv (unit (trg⇩C f)) ⋅⇩D unit (trg⇩C f)) ⋅⇩D 𝗂⇩D[map⇩0 ?b] = 𝗂⇩D[map⇩0 ?b]"
by (simp add: D.comp_cod_arr D.comp_inv_arr D.inv_is_inverse unit_char(2)
assms)
thus ?thesis
by (simp add: D.comp_assoc)
qed
finally show ?thesis by blast
qed
thus ?thesis by simp
qed
also have "... = map⇩0 ?b ⋆⇩D 𝗅⇩D[F f]"
using assms D.lunit_char [of "F f"] ‹trg⇩D (F f) = map⇩0 ?b› by simp
finally show ?thesis by blast
qed
ultimately show ?thesis
using assms D.L.is_faithful
by (metis D.trg_cod D.trg_vcomp D.vseq_implies_hpar(2) lF_simps(3))
qed
thus ?thesis
using assms 1 unit_char(1-2) C.ideD(1) C.obj_trg D.inverse_arrows_hcomp(1)
D.invert_side_of_triangle(2) D.lunit_simps(1) unit_simps(2) preserves_ide
D.iso_hcomp as_nat_iso.components_are_iso
by metis
qed
lemma lunit_coherence2:
assumes "C.ide f"
shows "lF f = F 𝗅⇩C[f] ⋅⇩D Φ (trg⇩C f, f)"
proof -
let ?b = "trg⇩C f"
have "D.par (F 𝗅⇩C[f] ⋅⇩D Φ (?b, f)) (lF f)"
using assms cmp_simps'(1) cmp_simps(4-5) by force
moreover have "F ?b ⋆⇩D F 𝗅⇩C[f] ⋅⇩D Φ (?b, f) = F ?b ⋆⇩D lF f"
proof -
have "F ?b ⋆⇩D F 𝗅⇩C[f] ⋅⇩D Φ (?b, f) = (F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D (F ?b ⋆⇩D Φ (?b, f))"
using assms cmp_in_hom D.whisker_left [of "F ?b" "F 𝗅⇩C[f]" "Φ (?b, f)"]
by (simp add: calculation)
also have "... = F ?b ⋆⇩D lF f"
proof -
have "(F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D (F ?b ⋆⇩D Φ (?b, f))
= (F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D F 𝖺⇩C[?b, ?b, f] ⋅⇩D
Φ (?b ⋆⇩C ?b, f) ⋅⇩D (Φ (?b, ?b) ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F ?b, F ?b, F f]"
proof -
have 1: "D.seq (F 𝖺⇩C[trg⇩C f, trg⇩C f, f])
(Φ (trg⇩C f ⋆⇩C trg⇩C f, f) ⋅⇩D (Φ (trg⇩C f, trg⇩C f) ⋆⇩D F f))"
using assms by fastforce
hence 2: "D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D F 𝖺⇩C[?b, ?b, f] ⋅⇩D Φ (?b ⋆⇩C ?b, f) ⋅⇩D
(Φ (?b, ?b) ⋆⇩D F f)
= (F ?b ⋆⇩D Φ (?b, f)) ⋅⇩D 𝖺⇩D[F ?b, F ?b, F f]"
using assms cmp_in_hom assoc_coherence cmp_components_are_iso
D.invert_side_of_triangle(1)
[of "F 𝖺⇩C[?b, ?b, f] ⋅⇩D Φ (?b ⋆⇩C ?b, f) ⋅⇩D (Φ (?b, ?b) ⋆⇩D F f)"
"Φ (?b, ?b ⋆⇩C f)"
"(F ?b ⋆⇩D Φ (?b, f)) ⋅⇩D 𝖺⇩D[F ?b, F ?b, F f]"]
C.ideD(1) C.ide_hcomp C.trg_hcomp C.trg_trg C.src_trg C.trg.preserves_ide
by metis
hence "F ?b ⋆⇩D Φ (?b, f)
= (D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D F 𝖺⇩C[?b, ?b, f] ⋅⇩D Φ (?b ⋆⇩C ?b, f) ⋅⇩D
(Φ (?b, ?b) ⋆⇩D F f)) ⋅⇩D 𝖺⇩D⇧-⇧1[F ?b, F ?b, F f]"
proof -
have "D.seq (D.inv (Φ (trg⇩C f, trg⇩C f ⋆⇩C f)))
(F 𝖺⇩C[trg⇩C f, trg⇩C f, f] ⋅⇩D Φ (trg⇩C f ⋆⇩C trg⇩C f, f) ⋅⇩D
(Φ (trg⇩C f, trg⇩C f) ⋆⇩D F f))"
using assms 1 D.hseq_char by auto
moreover have "(F (trg⇩C f) ⋆⇩D Φ (trg⇩C f, f)) ⋅⇩D 𝖺⇩D[F (trg⇩C f), F (trg⇩C f), F f] =
D.inv (Φ (trg⇩C f, trg⇩C f ⋆⇩C f)) ⋅⇩D
F 𝖺⇩C[trg⇩C f, trg⇩C f, f] ⋅⇩D Φ (trg⇩C f ⋆⇩C trg⇩C f, f) ⋅⇩D
(Φ (trg⇩C f, trg⇩C f) ⋆⇩D F f)"
using assms 2 by simp
ultimately show ?thesis
using assms
D.invert_side_of_triangle(2)
[of "D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D F 𝖺⇩C[?b, ?b, f] ⋅⇩D Φ (?b ⋆⇩C ?b, f) ⋅⇩D
(Φ (?b, ?b) ⋆⇩D F f)"
"F ?b ⋆⇩D Φ (?b, f)" "𝖺⇩D[F ?b, F ?b, F f]"]
by fastforce
qed
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D
(D.inv (F (?b ⋆⇩C 𝗅⇩C[f])) ⋅⇩D F (𝗂⇩C[?b] ⋆⇩C f)) ⋅⇩D
Φ (?b ⋆⇩C ?b, f) ⋅⇩D (Φ (?b, ?b) ⋆⇩D F f) ⋅⇩D
𝖺⇩D⇧-⇧1[F ?b, F ?b, F f]"
proof -
have 1: "F (?b ⋆⇩C 𝗅⇩C[f]) = F (𝗂⇩C[?b] ⋆⇩C f) ⋅⇩D D.inv (F 𝖺⇩C[?b, ?b, f])"
using assms C.lunit_char(1-2) C.unit_in_hom preserves_inv by auto
have "F 𝖺⇩C[?b, ?b, f] = D.inv (F (?b ⋆⇩C 𝗅⇩C[f])) ⋅⇩D F (𝗂⇩C[?b] ⋆⇩C f)"
proof -
have "F 𝖺⇩C[?b, ?b, f] ⋅⇩D D.inv (F (𝗂⇩C[?b] ⋆⇩C f)) =
D.inv (F (𝗂⇩C[?b] ⋆⇩C f) ⋅⇩D D.inv (F 𝖺⇩C[?b, ?b, f]))"
using assms by (simp add: C.iso_unit D.inv_comp)
thus ?thesis
using assms 1 D.invert_side_of_triangle D.iso_inv_iso
by (metis C.iso_hcomp C.ideD(1) C.ide_is_iso C.iso_lunit C.iso_unit
C.lunit_simps(3) C.obj_trg C.src_trg C.trg.as_nat_iso.components_are_iso
C.unit_simps(2) D.arr_inv D.inv_inv preserves_iso)
qed
thus ?thesis by argo
qed
also have "... = (F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D
D.inv (F (?b ⋆⇩C 𝗅⇩C[f])) ⋅⇩D (F (𝗂⇩C[?b] ⋆⇩C f) ⋅⇩D Φ (?b ⋆⇩C ?b, f)) ⋅⇩D
(Φ (?b, ?b) ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F ?b, F ?b, F f]"
using D.comp_assoc by auto
also have "... = (F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D
D.inv (F (?b ⋆⇩C 𝗅⇩C[f])) ⋅⇩D (Φ (?b, f) ⋅⇩D (F 𝗂⇩C[?b] ⋆⇩D F f)) ⋅⇩D
(Φ (?b, ?b) ⋆⇩D F f) ⋅⇩D 𝖺⇩D⇧-⇧1[F ?b, F ?b, F f]"
using assms Φ.naturality [of "(𝗂⇩C[?b], f)"] FF_def C.VV.arr_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C
C.VV.dom_char⇩S⇩b⇩C
by simp
also have "... = (F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D
D.inv (F (?b ⋆⇩C 𝗅⇩C[f])) ⋅⇩D Φ (?b, f) ⋅⇩D
((F 𝗂⇩C[?b] ⋆⇩D F f)) ⋅⇩D (Φ (?b, ?b) ⋆⇩D F f) ⋅⇩D
𝖺⇩D⇧-⇧1[F ?b, F ?b, F f]"
using D.comp_assoc by auto
also have "... = (F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D
D.inv (F (?b ⋆⇩C 𝗅⇩C[f])) ⋅⇩D Φ (?b, f) ⋅⇩D (𝗂 ?b ⋆⇩D F f) ⋅⇩D
𝖺⇩D⇧-⇧1[F ?b, F ?b, F f]"
using assms by (simp add: D.comp_assoc D.whisker_right)
also have "... = (F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D
(D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D D.inv (F (?b ⋆⇩C 𝗅⇩C[f])) ⋅⇩D Φ (?b, f)) ⋅⇩D
(F ?b ⋆⇩D lF f)"
using D.comp_assoc assms lF_char(2) by presburger
also have "... = (F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D D.inv (F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D (F ?b ⋆⇩D lF f)"
proof -
have "D.inv (F ?b ⋆⇩D F 𝗅⇩C[f]) =
D.inv (((F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D D.inv (Φ (?b, ?b ⋆⇩C f))) ⋅⇩D Φ (?b, ?b ⋆⇩C f))"
using assms D.comp_inv_arr D.comp_inv_arr' cmp_simps(4)
D.comp_arr_dom D.comp_assoc
by simp
also have "... = D.inv (D.inv (Φ (?b, f)) ⋅⇩D F (?b ⋆⇩C 𝗅⇩C[f]) ⋅⇩D Φ (?b, ?b ⋆⇩C f))"
proof -
have 1: "Φ (?b, f) ⋅⇩D (F ?b ⋆⇩D F 𝗅⇩C[f]) = F (?b ⋆⇩C 𝗅⇩C[f]) ⋅⇩D Φ (?b, ?b ⋆⇩C f)"
using assms Φ.naturality [of "(?b, 𝗅⇩C[f])"] FF_def C.VV.arr_char⇩S⇩b⇩C
C.VV.cod_char⇩S⇩b⇩C D.VV.null_char C.VV.dom_simp
by simp
have "(F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D D.inv (Φ (?b, ?b ⋆⇩C f)) =
D.inv (Φ (?b, f)) ⋅⇩D F (?b ⋆⇩C 𝗅⇩C[f])"
proof -
have "D.seq (Φ (?b, f)) (F ?b ⋆⇩D F 𝗅⇩C[f])"
using assms cmp_in_hom(2) [of ?b f] by auto
moreover have "D.iso (Φ (?b, f)) ∧ D.iso (Φ (?b, ?b ⋆⇩C f))"
using assms by simp
ultimately show ?thesis
using 1 D.invert_opposite_sides_of_square by simp
qed
thus ?thesis
using D.comp_assoc by auto
qed
also have "... = D.inv (F (?b ⋆⇩C 𝗅⇩C[f]) ⋅⇩D Φ (?b, ?b ⋆⇩C f)) ⋅⇩D Φ (?b, f)"
proof -
have "D.iso (F (?b ⋆⇩C 𝗅⇩C[f]) ⋅⇩D Φ (?b, ?b ⋆⇩C f))"
using assms D.isos_compose C.VV.arr_char⇩S⇩b⇩C C.iso_lunit C.VV.dom_simp
C.VV.cod_simp
by simp
moreover have "D.iso (D.inv (Φ (?b, f)))"
using assms by simp
moreover have "D.seq (D.inv (Φ (?b, f))) (F (?b ⋆⇩C 𝗅⇩C[f]) ⋅⇩D Φ (?b, ?b ⋆⇩C f))"
using assms C.VV.arr_char⇩S⇩b⇩C C.VV.dom_simp C.VV.cod_simp by simp
ultimately show ?thesis
using assms D.inv_comp by simp
qed
also have "... = D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D D.inv (F (?b ⋆⇩C 𝗅⇩C[f])) ⋅⇩D Φ (?b, f)"
using D.comp_assoc D.inv_comp assms cmp_simps'(1) cmp_simps(5) by force
finally have "D.inv (F ?b ⋆⇩D F 𝗅⇩C[f])
= D.inv (Φ (?b, ?b ⋆⇩C f)) ⋅⇩D D.inv (F (?b ⋆⇩C 𝗅⇩C[f])) ⋅⇩D Φ (?b, f)"
by blast
thus ?thesis by argo
qed
also have "... = ((F ?b ⋆⇩D F 𝗅⇩C[f]) ⋅⇩D D.inv (F ?b ⋆⇩D F 𝗅⇩C[f])) ⋅⇩D (F ?b ⋆⇩D lF f)"
using D.comp_assoc by simp
also have "... = F ?b ⋆⇩D lF f"
using assms D.comp_arr_inv' [of "F ?b ⋆⇩D F 𝗅⇩C[f]"] D.comp_cod_arr by simp
finally show ?thesis by simp
qed
ultimately show ?thesis by simp
qed
ultimately show ?thesis
using assms D.L.is_faithful
by (metis D.in_homI lF_char(2-3) lF_simps(4-5))
qed
lemma lunit_coherence:
assumes "C.ide f"
shows "𝗅⇩D[F f] = F 𝗅⇩C[f] ⋅⇩D Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f)"
proof -
have "𝗅⇩D[F f] = (F 𝗅⇩C[f] ⋅⇩D Φ (trg⇩C f, f)) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f)"
by (metis C.ideD(1) C.obj_trg D.inv_inv D.invert_side_of_triangle(2)
D.iso_hcomp D.iso_inv_iso as_nat_iso.components_are_iso assms lF_simps(1)
lunit_coherence1 lunit_coherence2 preserves_trg unit_char(2) unit_simps(2))
thus ?thesis
using assms D.comp_assoc by simp
qed
text ‹
We postpone proving the dual version of this result until after we have developed
the notion of the ``op bicategory'' in the next section.
›
end
subsection "Pseudofunctors and Opposite Bicategories"
text ‹
There are three duals to a bicategory:
\begin{enumerate}
\item ``op'': sources and targets are exchanged;
\item ``co'': domains and codomains are exchanged;
\item ``co-op'': both sources and targets and domains and codomains are exchanged.
\end{enumerate}
Here we consider the "op" case.
›
locale op_bicategory =
B: bicategory V H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B
for V :: "'a comp" (infixr "⋅" 55)
and H⇩B :: "'a comp" (infixr "⋆⇩B" 53)
and 𝖺⇩B :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("𝖺⇩B[_, _, _]")
and 𝗂⇩B :: "'a ⇒ 'a" ("𝗂⇩B[_]")
and src⇩B :: "'a ⇒ 'a"
and trg⇩B :: "'a ⇒ 'a"
begin
abbreviation H (infixr "⋆" 53)
where "H f g ≡ H⇩B g f"
abbreviation 𝗂 ("𝗂[_]")
where "𝗂 ≡ 𝗂⇩B"
abbreviation src
where "src ≡ trg⇩B"
abbreviation trg
where "trg ≡ src⇩B"
interpretation horizontal_homs V src trg
by (unfold_locales, auto)
interpretation H: "functor" VV.comp V ‹λμν. fst μν ⋆ snd μν›
using VV.arr_char⇩S⇩b⇩C VV.dom_simp VV.cod_simp
apply unfold_locales
apply (metis (no_types, lifting) B.hseqE B.hseq_char')
apply auto[3]
using VV.comp_char VV.seq_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C B.VxV.comp_char B.interchange
by (metis (no_types, lifting) B.VxV.seqE⇩P⇩C fst_conv snd_conv)
interpretation horizontal_composition V H src trg
by (unfold_locales, auto)
abbreviation UP
where "UP μντ ≡ if B.VVV.arr μντ then
(snd (snd μντ), fst (snd μντ), fst μντ)
else VVV.null"
abbreviation DN
where "DN μντ ≡ if VVV.arr μντ then
(snd (snd μντ), fst (snd μντ), fst μντ)
else B.VVV.null"
lemma VVV_arr_char:
shows "VVV.arr μντ ⟷ B.VVV.arr (DN μντ)"
using VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C B.VVV.not_arr_null
by auto
lemma VVV_ide_char:
shows "VVV.ide μντ ⟷ B.VVV.ide (DN μντ)"
proof -
have "VVV.ide μντ ⟷ VVV.arr μντ ∧ B.VxVxV.ide μντ"
using VVV.ide_char⇩S⇩b⇩C by simp
also have "... ⟷ B.VVV.arr (DN μντ) ∧ B.VxVxV.ide (DN μντ)"
using VVV_arr_char B.VxVxV.ide_char⇩P⇩C by auto
also have "... ⟷ B.VVV.ide (DN μντ)"
using B.VVV.ide_char⇩S⇩b⇩C [of "DN μντ"] by blast
finally show ?thesis by fast
qed
lemma VVV_dom_char:
shows "VVV.dom μντ = UP (B.VVV.dom (DN μντ))"
proof (cases "VVV.arr μντ")
show "¬ VVV.arr μντ ⟹ VVV.dom μντ = UP (B.VVV.dom (DN μντ))"
using VVV.dom_def VVV.has_domain_iff_arr VVV_arr_char B.VVV.dom_null
by auto
show "VVV.arr μντ ⟹ VVV.dom μντ = UP (B.VVV.dom (DN μντ))"
proof -
assume μντ: "VVV.arr μντ"
have "VVV.dom μντ =
(B.dom (fst μντ), B.dom (fst (snd μντ)), B.dom (snd (snd μντ)))"
using μντ VVV.dom_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C
by simp
also have "... = UP (B.dom (snd (snd μντ)), B.dom (fst (snd μντ)), B.dom (fst μντ))"
by (metis (no_types, lifting) B.VV.arrI⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.arr_dom VV.arrE VVV.arrE
μντ fst_conv snd_conv src_dom trg_dom)
also have "... = UP (B.VVV.dom (DN μντ))"
using μντ B.VVV.dom_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
by simp
finally show ?thesis by blast
qed
qed
lemma VVV_cod_char:
shows "VVV.cod μντ = UP (B.VVV.cod (DN μντ))"
proof (cases "VVV.arr μντ")
show "¬ VVV.arr μντ ⟹ VVV.cod μντ = UP (B.VVV.cod (DN μντ))"
using VVV.cod_def VVV.has_codomain_iff_arr VVV_arr_char B.VVV.cod_null
by auto
show "VVV.arr μντ ⟹ VVV.cod μντ = UP (B.VVV.cod (DN μντ))"
proof -
assume μντ: "VVV.arr μντ"
have "VVV.cod μντ = (B.cod (fst μντ), B.cod (fst (snd μντ)), B.cod (snd (snd μντ)))"
using μντ VVV.cod_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C
by simp
also have "... = UP (B.cod (snd (snd μντ)), B.cod (fst (snd μντ)), B.cod (fst μντ))"
by (metis (no_types, lifting) B.VV.arrI⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.arr_cod VV.arrE VVV.arrE
μντ fst_conv snd_conv src_cod trg_cod)
also have "... = UP (B.VVV.cod (DN μντ))"
using μντ B.VVV.cod_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
by simp
finally show ?thesis by blast
qed
qed
lemma HoHV_char:
shows "HoHV μντ = B.HoVH (DN μντ)"
using HoHV_def B.HoVH_def VVV_arr_char by simp
lemma HoVH_char:
shows "HoVH μντ = B.HoHV (DN μντ)"
using HoVH_def B.HoHV_def VVV_arr_char by simp
definition 𝖺 ("𝖺[_, _, _]")
where "𝖺[μ, ν, τ] ≡ B.α' (DN (μ, ν, τ))"
interpretation natural_isomorphism VVV.comp ‹(⋅)› HoHV HoVH
‹λμντ. 𝖺[fst μντ, fst (snd μντ), snd (snd μντ)]›
proof
fix μντ
show "¬ VVV.arr μντ ⟹ 𝖺[fst μντ, fst (snd μντ), snd (snd μντ)] = B.null"
using VVV.arr_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C 𝖺_def B.α'.is_extensional by auto
assume μντ: "VVV.arr μντ"
show "B.dom 𝖺[fst μντ, fst (snd μντ), snd (snd μντ)] = HoHV (VVV.dom μντ)"
using μντ 𝖺_def HoHV_def B.α'.preserves_dom VVV.arr_char⇩S⇩b⇩C VVV.dom_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
B.HoVH_def B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C B.VVV.dom_char⇩S⇩b⇩C
by auto
show "B.cod 𝖺[fst μντ, fst (snd μντ), snd (snd μντ)] = HoVH (VVV.cod μντ)"
using μντ 𝖺_def HoVH_def B.α'.preserves_cod VVV.arr_char⇩S⇩b⇩C VVV.cod_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
B.HoHV_def B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C B.VVV.cod_char⇩S⇩b⇩C
by auto
show "HoVH μντ ⋅
𝖺[fst (VVV.dom μντ), fst (snd (VVV.dom μντ)), snd (snd (VVV.dom μντ))] =
𝖺[fst μντ, fst (snd μντ), snd (snd μντ)]"
proof -
have "HoVH μντ ⋅
𝖺[fst (VVV.dom μντ), fst (snd (VVV.dom μντ)), snd (snd (VVV.dom μντ))] =
HoVH μντ ⋅ B.α' (B.VVV.dom (snd (snd μντ), fst (snd μντ), fst μντ))"
unfolding 𝖺_def
using μντ VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C VVV.dom_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VVV.dom_char⇩S⇩b⇩C
by auto
also have "... = B.α' (snd (snd μντ), fst (snd μντ), fst μντ)"
using B.α'.is_natural_1 VVV_arr_char μντ HoVH_char by presburger
also have "... = 𝖺[fst μντ, fst (snd μντ), snd (snd μντ)]"
using μντ 𝖺_def by simp
finally show ?thesis by blast
qed
show "𝖺[fst (VVV.cod μντ), fst (snd (VVV.cod μντ)), snd (snd (VVV.cod μντ))] ⋅
HoHV μντ =
𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ))"
proof -
have "𝖺[fst (VVV.cod μντ), fst (snd (VVV.cod μντ)), snd (snd (VVV.cod μντ))] ⋅
HoHV μντ =
B.α' (B.VVV.cod (snd (snd μντ), fst (snd μντ), fst μντ)) ⋅ HoHV μντ"
unfolding 𝖺_def
using μντ VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C VVV.cod_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VVV.cod_char⇩S⇩b⇩C
by auto
also have "... = B.α' (snd (snd μντ), fst (snd μντ), fst μντ)"
using B.α'.is_natural_2 VVV_arr_char μντ HoHV_char by presburger
also have "... = 𝖺[fst μντ, fst (snd μντ), snd (snd μντ)]"
using μντ 𝖺_def by simp
finally show ?thesis by blast
qed
next
fix μντ
assume μντ: "VVV.ide μντ"
show "B.iso 𝖺[fst μντ, fst (snd μντ), snd (snd μντ)]"
proof -
have "B.VVV.ide (DN μντ)"
using μντ VVV_ide_char by blast
thus ?thesis
using μντ 𝖺_def B.α'.components_are_iso by force
qed
qed
sublocale bicategory V H 𝖺 𝗂 src trg
proof
show "⋀a. obj a ⟹ «𝗂 a : H a a →⇩B a»"
using obj_def objE B.obj_def B.objE B.unit_in_hom by meson
show "⋀a. obj a ⟹ B.iso (𝗂 a)"
using obj_def objE B.obj_def B.objE B.iso_unit by meson
show "⋀f g h k. ⟦ B.ide f; B.ide g; B.ide h; B.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]"
unfolding 𝖺_def
using B.𝖺'_def B.comp_assoc B.pentagon' VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C by simp
qed
proposition is_bicategory:
shows "bicategory V H 𝖺 𝗂 src trg"
..
lemma assoc_ide_simp:
assumes "B.ide f" and "B.ide g" and "B.ide h"
and "src f = trg g" and "src g = trg h"
shows "𝖺[f, g, h] = B.𝖺' h g f"
using assms 𝖺_def B.𝖺'_def by fastforce
lemma lunit_ide_simp:
assumes "B.ide f"
shows "lunit f = B.runit f"
proof (intro B.runit_eqI)
show "B.ide f" by fact
show "«lunit f : H (trg f) f →⇩B f»"
using assms by simp
show "trg f ⋆ lunit f = (𝗂[trg f] ⋆ f) ⋅ 𝖺⇩B[f, trg f, trg f]"
proof -
have "trg f ⋆ lunit f = (𝗂[trg f] ⋆ f) ⋅ 𝖺' (trg f) (trg f) f"
using assms lunit_char(1-2) [of f] by simp
moreover have "𝖺' (trg f) (trg f) f = 𝖺⇩B[f, trg f, trg f]"
proof (unfold 𝖺'_def)
have 1: "VVV.ide (trg f, trg f, f)"
using assms VVV.ide_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C by simp
have "α' (trg f, trg f, f) = B.inv 𝖺[trg f, trg f, f]"
using 1 B.α'.inverts_components by simp
also have "... = B.inv (B.α' (f, trg f, trg f))"
unfolding 𝖺_def using 1 by simp
also have "... = 𝖺⇩B[f, trg f, trg f]"
using 1 B.VVV.ide_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C VVV.ide_char⇩S⇩b⇩C
VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C B.α'.inverts_components B.α_def
by force
finally show "α' (trg f, trg f, f) = 𝖺⇩B[f, trg f, trg f]"
by blast
qed
ultimately show ?thesis by simp
qed
qed
lemma runit_ide_simp:
assumes "B.ide f"
shows "runit f = B.lunit f"
using assms runit_char(1-2) [of f] B.𝖺'_def assoc_ide_simp
by (intro B.lunit_eqI) auto
end
context pseudofunctor
begin
interpretation C': op_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C ..
interpretation D': op_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ..
notation C'.H (infixr "⋆⇩C⇧o⇧p" 53)
notation D'.H (infixr "⋆⇩D⇧o⇧p" 53)
interpretation F': weak_arrow_of_homs V⇩C C'.src C'.trg V⇩D D'.src D'.trg F
apply unfold_locales
using weakly_preserves_src weakly_preserves_trg by simp_all
interpretation H⇩D'oFF: composite_functor C'.VV.comp D'.VV.comp V⇩D F'.FF
‹λμν. fst μν ⋆⇩D⇧o⇧p snd μν› ..
interpretation FoH⇩C': composite_functor C'.VV.comp V⇩C V⇩D
‹λμν. fst μν ⋆⇩C⇧o⇧p snd μν› F
..
interpretation Φ': natural_isomorphism C'.VV.comp V⇩D H⇩D'oFF.map FoH⇩C'.map
‹λf. Φ (snd f, fst f)›
using C.VV.arr_char⇩S⇩b⇩C C'.VV.arr_char⇩S⇩b⇩C C'.VV.ide_char⇩S⇩b⇩C C.VV.ide_char⇩S⇩b⇩C FF_def F'.FF_def
Φ.is_extensional Φ.is_natural_1 Φ.is_natural_2
C.VV.dom_simp C.VV.cod_simp C'.VV.dom_simp C'.VV.cod_simp
by unfold_locales auto
interpretation F': pseudofunctor V⇩C C'.H C'.𝖺 𝗂⇩C C'.src C'.trg
V⇩D D'.H D'.𝖺 𝗂⇩D D'.src D'.trg
F ‹λf. Φ (snd f, fst f)›
proof
fix f g h
assume f: "C.ide f" and g: "C.ide g" and h: "C.ide h"
and fg: "C'.src f = C'.trg g" and gh: "C'.src g = C'.trg h"
show "F (C'.𝖺 f g h) ⋅⇩D Φ (snd (f ⋆⇩C⇧o⇧p g, h), fst (f ⋆⇩C⇧o⇧p g, h)) ⋅⇩D
(Φ (snd (f, g), fst (f, g)) ⋆⇩D⇧o⇧p F h) =
Φ (snd (f, g ⋆⇩C⇧o⇧p h), fst (f, g ⋆⇩C⇧o⇧p h)) ⋅⇩D (F f ⋆⇩D⇧o⇧p Φ (snd (g, h), fst (g, h))) ⋅⇩D
D'.𝖺 (F f) (F g) (F h)"
using f g h fg gh C.VV.in_hom_char⇩S⇩b⇩C FF_def C.VV.arr_char⇩S⇩b⇩C C.VV.dom_simp C.VV.cod_simp
C'.assoc_ide_simp D'.assoc_ide_simp preserves_inv assoc_coherence
D.invert_opposite_sides_of_square
[of "F (𝖺⇩C h g f)" "Φ (g ⋆⇩C⇧o⇧p h, f) ⋅⇩D (F f ⋆⇩D⇧o⇧p Φ (h, g))"
"Φ (h, f ⋆⇩C⇧o⇧p g) ⋅⇩D (Φ (g, f) ⋆⇩D⇧o⇧p F h)" "𝖺⇩D (F h) (F g) (F f)"]
D.comp_assoc
by auto
qed
lemma induces_pseudofunctor_between_opposites:
shows "pseudofunctor (⋅⇩C) (⋆⇩C⇧o⇧p) C'.𝖺 𝗂⇩C C'.src C'.trg
(⋅⇩D) (⋆⇩D⇧o⇧p) D'.𝖺 𝗂⇩D D'.src D'.trg
F (λf. Φ (snd f, fst f))"
..
text ‹
It is now easy to dualize the coherence condition for ‹F› with respect to
left unitors to obtain the corresponding condition for right unitors.
›
lemma runit_coherence:
assumes "C.ide f"
shows "𝗋⇩D[F f] = F 𝗋⇩C[f] ⋅⇩D Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f))"
proof -
have "C'.lunit f = 𝗋⇩C[f]"
using assms C'.lunit_ide_simp by simp
moreover have "D'.lunit (F f) = 𝗋⇩D[F f]"
using assms D'.lunit_ide_simp by simp
moreover have "F'.unit (src⇩C f) = unit (src⇩C f)"
using assms F'.unit_char F'.preserves_trg
by (intro unit_eqI) auto
moreover have "D'.lunit (F f) =
F (C'.lunit f) ⋅⇩D Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D F'.unit (src⇩C f))"
using assms F'.lunit_coherence by simp
ultimately show ?thesis by simp
qed
end
subsection "Preservation Properties"
text ‹
The objective of this section is to establish explicit formulas for the result
of applying a pseudofunctor to expressions of various forms.
›
context pseudofunctor
begin
lemma preserves_lunit:
assumes "C.ide f"
shows "F 𝗅⇩C[f] = 𝗅⇩D[F f] ⋅⇩D (D.inv (unit (trg⇩C f)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (trg⇩C f, f))"
and "F 𝗅⇩C⇧-⇧1[f] = Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f) ⋅⇩D 𝗅⇩D⇧-⇧1[F f]"
proof -
show 1: "F 𝗅⇩C[f] = 𝗅⇩D[F f] ⋅⇩D (D.inv (unit (trg⇩C f)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (trg⇩C f, f))"
proof -
have "𝗅⇩D[F f] ⋅⇩D D.inv (Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f)) = F 𝗅⇩C[f]"
proof -
have "D.arr 𝗅⇩D[F f]"
using assms by simp
moreover have "𝗅⇩D[F f] = F 𝗅⇩C[f] ⋅⇩D Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f)"
using assms lunit_coherence by simp
moreover have "D.iso (Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f))"
using assms unit_char cmp_components_are_iso
by (intro D.isos_compose D.seqI) auto
ultimately show ?thesis
using assms D.invert_side_of_triangle(2) by metis
qed
moreover have "D.inv (Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f)) =
(D.inv (unit (trg⇩C f)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (trg⇩C f, f))"
using assms C.VV.arr_char⇩S⇩b⇩C unit_char FF_def D.inv_comp C.VV.dom_simp by simp
ultimately show ?thesis by simp
qed
show "F 𝗅⇩C⇧-⇧1[f] = Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f) ⋅⇩D 𝗅⇩D⇧-⇧1[F f]"
proof -
have "F 𝗅⇩C⇧-⇧1[f] =
D.inv (𝗅⇩D[F f] ⋅⇩D (D.inv (unit (trg⇩C f)) ⋆⇩D F f) ⋅⇩D D.inv (Φ (trg⇩C f, f)))"
using assms 1 preserves_inv by simp
also have "... = Φ (trg⇩C f, f) ⋅⇩D (unit (trg⇩C f) ⋆⇩D F f) ⋅⇩D 𝗅⇩D⇧-⇧1[F f]"
using assms unit_char D.comp_assoc D.isos_compose
by (auto simp add: D.inv_comp)
finally show ?thesis by simp
qed
qed
lemma preserves_runit:
assumes "C.ide f"
shows "F 𝗋⇩C[f] = 𝗋⇩D[F f] ⋅⇩D (F f ⋆⇩D D.inv (unit (src⇩C f))) ⋅⇩D D.inv (Φ (f, src⇩C f))"
and "F 𝗋⇩C⇧-⇧1[f] = Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f)) ⋅⇩D 𝗋⇩D⇧-⇧1[F f]"
proof -
show 1: "F 𝗋⇩C[f] = 𝗋⇩D[F f] ⋅⇩D (F f ⋆⇩D D.inv (unit (src⇩C f))) ⋅⇩D D.inv (Φ (f, src⇩C f))"
proof -
have "F 𝗋⇩C[f] = 𝗋⇩D[F f] ⋅⇩D D.inv (Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f)))"
proof -
have "𝗋⇩D[F f] = F 𝗋⇩C[f] ⋅⇩D Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f))"
using assms runit_coherence by simp
moreover have "D.iso (Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f)))"
using assms unit_char D.iso_hcomp FF_def
apply (intro D.isos_compose D.seqI) by auto
moreover have "D.arr 𝗋⇩D[F f]"
using assms by simp
ultimately show ?thesis
using assms D.invert_side_of_triangle(2) by metis
qed
moreover have "D.inv (Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f))) =
(F f ⋆⇩D D.inv (unit (src⇩C f))) ⋅⇩D D.inv (Φ (f, src⇩C f))"
using assms C.VV.arr_char⇩S⇩b⇩C unit_char D.iso_hcomp FF_def D.inv_comp C.VV.dom_simp
by simp
ultimately show ?thesis by simp
qed
show "F 𝗋⇩C⇧-⇧1[f] = Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f)) ⋅⇩D 𝗋⇩D⇧-⇧1[F f]"
proof -
have "F 𝗋⇩C⇧-⇧1[f] =
D.inv (𝗋⇩D[F f] ⋅⇩D (F f ⋆⇩D D.inv (unit (src⇩C f))) ⋅⇩D D.inv (Φ (f, src⇩C f)))"
using assms 1 preserves_inv C.iso_runit by simp
also have "... = Φ (f, src⇩C f) ⋅⇩D (F f ⋆⇩D unit (src⇩C f)) ⋅⇩D 𝗋⇩D⇧-⇧1[F f]"
using assms unit_char D.comp_assoc D.isos_compose
by (auto simp add: D.inv_comp)
finally show ?thesis by simp
qed
qed
lemma preserves_assoc:
assumes "C.ide f" and "C.ide g" and "C.ide h"
and "src⇩C f = trg⇩C g" and "src⇩C g = trg⇩C h"
shows "F 𝖺⇩C[f, g, h] = Φ (f, g ⋆⇩C h) ⋅⇩D (F f ⋆⇩D Φ (g, h)) ⋅⇩D 𝖺⇩D[F f, F g, F h] ⋅⇩D
(D.inv (Φ (f, g)) ⋆⇩D F h) ⋅⇩D D.inv (Φ (f ⋆⇩C g, h))"
and "F 𝖺⇩C⇧-⇧1[f, g, h] = Φ (f ⋆⇩C g, h) ⋅⇩D (Φ (f, g) ⋆⇩D F h) ⋅⇩D 𝖺⇩D⇧-⇧1[F f, F g, F h] ⋅⇩D
(F f ⋆⇩D D.inv (Φ (g, h))) ⋅⇩D D.inv (Φ (f, g ⋆⇩C h))"
proof -
show 1: "F 𝖺⇩C[f, g, h] =
Φ (f, g ⋆⇩C h) ⋅⇩D (F f ⋆⇩D Φ (g, h)) ⋅⇩D 𝖺⇩D[F f, F g, F h] ⋅⇩D
(D.inv (Φ (f, g)) ⋆⇩D F h) ⋅⇩D D.inv (Φ (f ⋆⇩C g, h))"
proof -
have "F 𝖺⇩C[f, g, h] ⋅⇩D Φ (f ⋆⇩C g, h) ⋅⇩D (Φ (f, g) ⋆⇩D F h) =
Φ (f, g ⋆⇩C h) ⋅⇩D (F f ⋆⇩D Φ (g, h)) ⋅⇩D 𝖺⇩D[F f, F g, F h]"
using assms assoc_coherence [of f g h] by simp
moreover have "D.seq (Φ (f, g ⋆⇩C h)) ((F f ⋆⇩D Φ (g, h)) ⋅⇩D 𝖺⇩D[F f, F g, F h])"
using assms C.VV.arr_char⇩S⇩b⇩C FF_def C.VV.dom_simp C.VV.cod_simp by auto
moreover have 2: "D.iso (Φ (f ⋆⇩C g, h) ⋅⇩D (Φ (f, g) ⋆⇩D F h))"
using assms C.VV.arr_char⇩S⇩b⇩C FF_def C.VV.dom_simp C.VV.cod_simp by auto
moreover have "D.inv (Φ (f ⋆⇩C g, h) ⋅⇩D (Φ (f, g) ⋆⇩D F h)) =
(D.inv (Φ (f, g)) ⋆⇩D F h) ⋅⇩D D.inv (Φ (f ⋆⇩C g, h))"
using assms 2 C.VV.arr_char⇩S⇩b⇩C FF_def D.inv_comp C.VV.dom_simp C.VV.cod_simp
by simp
ultimately show ?thesis
using D.invert_side_of_triangle(2)
[of "Φ (f, g ⋆⇩C h) ⋅⇩D (F f ⋆⇩D Φ (g, h)) ⋅⇩D 𝖺⇩D[F f, F g, F h]"
"F 𝖺⇩C[f, g, h]" "Φ (f ⋆⇩C g, h) ⋅⇩D (Φ (f, g) ⋆⇩D F h)"]
D.comp_assoc
by simp
qed
show "F 𝖺⇩C⇧-⇧1[f, g, h] =
Φ (f ⋆⇩C g, h) ⋅⇩D (Φ (f, g) ⋆⇩D F h) ⋅⇩D 𝖺⇩D⇧-⇧1[F f, F g, F h] ⋅⇩D
(F f ⋆⇩D D.inv (Φ (g, h))) ⋅⇩D D.inv (Φ (f, g ⋆⇩C h))"
proof -
have "F 𝖺⇩C⇧-⇧1[f, g, h] =
D.inv (Φ (f, g ⋆⇩C h) ⋅⇩D (F f ⋆⇩D Φ (g, h)) ⋅⇩D 𝖺⇩D[F f, F g, F h] ⋅⇩D
(D.inv (Φ (f, g)) ⋆⇩D F h) ⋅⇩D D.inv (Φ (f ⋆⇩C g, h)))"
using assms 1 preserves_inv by simp
also have "... = Φ (f ⋆⇩C g, h) ⋅⇩D (Φ (f, g) ⋆⇩D F h) ⋅⇩D 𝖺⇩D⇧-⇧1[F f, F g, F h] ⋅⇩D
(F f ⋆⇩D D.inv (Φ (g, h))) ⋅⇩D D.inv (Φ (f, g ⋆⇩C h))"
proof -
have "«Φ (f, g ⋆⇩C h) : F f ⋆⇩D F (g ⋆⇩C h) ⇒⇩D F (f ⋆⇩C g ⋆⇩C h)» ∧ D.iso (Φ (f, g ⋆⇩C h))"
using assms by auto
moreover have "«F f ⋆⇩D Φ (g, h) : F f ⋆⇩D F g ⋆⇩D F h ⇒⇩D F f ⋆⇩D F (g ⋆⇩C h)» ∧
D.iso (F f ⋆⇩D Φ (g, h))"
using assms
by (intro conjI D.hcomp_in_vhom, auto)
ultimately show ?thesis
using assms D.isos_compose D.comp_assoc D.inv_comp
by (elim conjE D.in_homE) auto
qed
finally show ?thesis by simp
qed
qed
lemma preserves_hcomp:
assumes "C.hseq μ ν"
shows "F (μ ⋆⇩C ν) =
Φ (C.cod μ, C.cod ν) ⋅⇩D (F μ ⋆⇩D F ν) ⋅⇩D D.inv (Φ (C.dom μ, C.dom ν))"
proof -
have "F (μ ⋆⇩C ν) ⋅⇩D Φ (C.dom μ, C.dom ν) = Φ (C.cod μ, C.cod ν) ⋅⇩D (F μ ⋆⇩D F ν)"
using assms Φ.naturality C.VV.arr_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C FF_def C.VV.dom_simp
by auto
thus ?thesis
by (metis (no_types) assms C.hcomp_simps(3) C.hseqE C.ide_dom C.src_dom C.trg_dom
D.comp_arr_inv' D.comp_assoc cmp_components_are_iso cmp_simps(5)
as_nat_trans.is_natural_1)
qed
lemma preserves_adjunction_data:
assumes "adjunction_data_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε"
shows "adjunction_data_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D
(F f) (F g) (D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f))
(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g))"
proof
interpret adjunction_data_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε
using assms by auto
show "D.ide (F f)"
using preserves_ide by simp
show "D.ide (F g)"
using preserves_ide by simp
show "«D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f) : src⇩D (F f) ⇒⇩D F g ⋆⇩D F f»"
using antipar C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C cmp_in_hom(2) unit_in_hom FF_def by auto
show "«D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g) : F f ⋆⇩D F g ⇒⇩D src⇩D (F g)»"
using antipar C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C FF_def cmp_in_hom(2) unit_in_hom(2)
unit_char(2)
by auto
qed
lemma preserves_equivalence:
assumes "equivalence_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε"
shows "equivalence_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D
(F f) (F g) (D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f))
(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g))"
proof -
interpret equivalence_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε
using assms by auto
show "equivalence_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D
(F f) (F g) (D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f))
(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g))"
using antipar unit_is_iso preserves_iso unit_char(2) C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C
FF_def D.isos_compose
by (unfold_locales) auto
qed
lemma preserves_equivalence_maps:
assumes "C.equivalence_map f"
shows "D.equivalence_map (F f)"
proof -
obtain g η ε where E: "equivalence_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε"
using assms C.equivalence_map_def by auto
interpret E: equivalence_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε
using E by auto
show ?thesis
using E preserves_equivalence C.equivalence_map_def D.equivalence_map_def map⇩0_simps
by blast
qed
lemma preserves_equivalent_objects:
assumes "C.equivalent_objects a b"
shows "D.equivalent_objects (map⇩0 a) (map⇩0 b)"
using assms D.equivalent_objects_def preserves_equivalence_maps
unfolding C.equivalent_objects_def by fast
lemma preserves_isomorphic:
assumes "C.isomorphic f g"
shows "D.isomorphic (F f) (F g)"
using assms C.isomorphic_def D.isomorphic_def preserves_iso by auto
lemma preserves_quasi_inverses:
assumes "C.quasi_inverses f g"
shows "D.quasi_inverses (F f) (F g)"
using assms C.quasi_inverses_def D.quasi_inverses_def preserves_equivalence by blast
lemma preserves_quasi_inverse:
assumes "C.equivalence_map f"
shows "D.isomorphic (F (C.some_quasi_inverse f)) (D.some_quasi_inverse (F f))"
using assms preserves_quasi_inverses C.quasi_inverses_some_quasi_inverse
D.quasi_inverse_unique D.quasi_inverses_some_quasi_inverse
preserves_equivalence_maps
by blast
end
subsection "Identity Pseudofunctors"
locale identity_pseudofunctor =
B: bicategory V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B
for V⇩B :: "'b comp" (infixr "⋅⇩B" 55)
and H⇩B :: "'b comp" (infixr "⋆⇩B" 53)
and 𝖺⇩B :: "'b ⇒ 'b ⇒ 'b ⇒ 'b" ("𝖺⇩B[_, _, _]")
and 𝗂⇩B :: "'b ⇒ 'b" ("𝗂⇩B[_]")
and src⇩B :: "'b ⇒ 'b"
and trg⇩B :: "'b ⇒ 'b"
begin
text‹
The underlying vertical functor is just the identity functor on the vertical category,
which is already available as ‹B.map›.
›
abbreviation map
where "map ≡ B.map"
interpretation I: weak_arrow_of_homs V⇩B src⇩B trg⇩B V⇩B src⇩B trg⇩B map
using B.isomorphic_reflexive by unfold_locales auto
interpretation II: "functor" B.VV.comp B.VV.comp I.FF
using I.functor_FF by simp
interpretation H⇩BoII: composite_functor B.VV.comp B.VV.comp V⇩B I.FF
‹λμν. fst μν ⋆⇩B snd μν›
..
interpretation IoH⇩B: composite_functor B.VV.comp V⇩B V⇩B ‹λμν. fst μν ⋆⇩B snd μν› map
..
text‹
The horizontal composition provides the compositor.
›
abbreviation cmp
where "cmp ≡ λμν. fst μν ⋆⇩B snd μν"
interpretation cmp: natural_transformation B.VV.comp V⇩B H⇩BoII.map IoH⇩B.map cmp
using B.VV.arr_char⇩S⇩b⇩C B.VV.dom_simp B.VV.cod_simp B.H.as_nat_trans.is_natural_1
B.H.as_nat_trans.is_natural_2 I.FF_def
apply unfold_locales
apply auto
by (meson B.hseqE B.hseq_char')+
interpretation cmp: natural_isomorphism B.VV.comp V⇩B H⇩BoII.map IoH⇩B.map cmp
by unfold_locales simp
sublocale pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B map cmp
apply unfold_locales
by (metis B.assoc_is_natural_2 B.assoc_naturality B.assoc_simps(1) B.comp_ide_self
B.hcomp_simps(1) B.ide_char B.ide_hcomp B.map_simp fst_conv snd_conv)
lemma is_pseudofunctor:
shows "pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B map cmp"
..
lemma unit_char':
assumes "B.obj a"
shows "unit a = a"
proof -
have "src⇩B a = a ∧ B.ide a"
using assms by auto
hence "a = unit a"
using assms B.comp_arr_dom B.comp_cod_arr I.map⇩0_def map_def
B.ide_in_hom(2) B.objE [of a] B.ide_is_iso [of a]
by (intro unit_eqI) auto
thus ?thesis by simp
qed
end
lemma (in identity_pseudofunctor) map⇩0_simp [simp]:
assumes "B.obj a"
shows "map⇩0 a = a"
using assms map⇩0_def by auto
subsection "Embedding Pseudofunctors"
text ‹
In this section, we construct the embedding pseudofunctor of a sub-bicategory
into the ambient bicategory.
›
locale embedding_pseudofunctor =
B: bicategory V H 𝖺⇩B 𝗂 src⇩B trg⇩B +
S: subbicategory
begin
no_notation B.in_hom ("«_ : _ →⇩B _»")
notation B.in_hhom ("«_ : _ →⇩B _»")
definition map
where "map μ = (if S.arr μ then μ else B.null)"
lemma map_in_hom [intro]:
assumes "S.arr μ"
shows "«map μ : src⇩B (map (S.src μ)) →⇩B src⇩B (map (S.trg μ))»"
and "«map μ : map (S.dom μ) ⇒⇩B map (S.cod μ)»"
proof -
show 1: "«map μ : map (S.dom μ) ⇒⇩B map (S.cod μ)»"
using assms map_def S.in_hom_char⇩S⇩b⇩C by fastforce
show "«map μ : src⇩B (map (S.src μ)) →⇩B src⇩B (map (S.trg μ))»"
using assms 1 map_def S.arr_char⇩S⇩b⇩C S.src_def S.trg_def S.obj_char S.obj_src S.obj_trg
by auto
qed
lemma map_simps [simp]:
assumes "S.arr μ"
shows "B.arr (map μ)"
and "src⇩B (map μ) = src⇩B (map (S.src μ))" and "trg⇩B (map μ) = src⇩B (map (S.trg μ))"
and "B.dom (map μ) = map (S.dom μ)" and "B.cod (map μ) = map (S.cod μ)"
using assms map_in_hom by blast+
interpretation "functor" S.comp V map
apply unfold_locales
apply auto
using map_def S.comp_char S.seq_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C
apply auto[1]
using map_def S.comp_simp by auto
interpretation weak_arrow_of_homs S.comp S.src S.trg V src⇩B trg⇩B map
using S.arr_char⇩S⇩b⇩C map_def S.src_def S.trg_def S.src_closed S.trg_closed B.isomorphic_reflexive
preserves_ide S.ide_src S.ide_trg
apply unfold_locales
by presburger+
interpretation HoFF: composite_functor S.VV.comp B.VV.comp V FF
‹λμν. fst μν ⋆⇩B snd μν›
..
interpretation FoH: composite_functor S.VV.comp S.comp V ‹λμν. fst μν ⋆ snd μν› map
..
no_notation B.in_hom ("«_ : _ →⇩B _»")
definition cmp
where "cmp μν = (if S.VV.arr μν then fst μν ⋆⇩B snd μν else B.null)"
lemma cmp_in_hom [intro]:
assumes "S.VV.arr μν"
shows "«cmp μν : src⇩B (snd μν) →⇩B trg⇩B (fst μν)»"
and "«cmp μν : map (S.dom (fst μν)) ⋆⇩B map (S.dom (snd μν))
⇒⇩B map (S.cod (fst μν) ⋆ S.cod (snd μν))»"
proof -
show "«cmp μν : map (S.dom (fst μν)) ⋆⇩B map (S.dom (snd μν))
⇒⇩B map (S.cod (fst μν) ⋆ S.cod (snd μν))»"
proof
show 1: "B.arr (cmp μν)"
unfolding cmp_def
using assms S.arr_char⇩S⇩b⇩C S.VV.arr_char⇩S⇩b⇩C S.inclusion S.src_def S.trg_def by auto
show "B.dom (cmp μν) = map (S.dom (fst μν)) ⋆⇩B map (S.dom (snd μν))"
unfolding cmp_def map_def
using assms 1 cmp_def S.dom_simp S.cod_simp S.VV.arr_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C S.hcomp_def
S.inclusion S.dom_closed
by auto
show "B.cod (cmp μν) = map (S.cod (fst μν) ⋆ S.cod (snd μν))"
unfolding cmp_def map_def
using assms 1 S.H.preserves_arr S.cod_simp S.hcomp_eqI S.hcomp_simps(4) S.hseq_char'
by auto
qed
thus "«cmp μν : src⇩B (snd μν) →⇩B trg⇩B (fst μν)»"
using cmp_def by auto
qed
lemma cmp_simps [simp]:
assumes "S.VV.arr μν"
shows "B.arr (cmp μν)"
and "src⇩B (cmp μν) = S.src (snd μν)" and "trg⇩B (cmp μν) = S.trg (fst μν)"
and "B.dom (cmp μν) = map (S.dom (fst μν)) ⋆⇩B map (S.dom (snd μν))"
and "B.cod (cmp μν) = map (S.cod (fst μν) ⋆ S.cod (snd μν))"
using assms cmp_in_hom S.src_def S.trg_def S.VV.arr_char⇩S⇩b⇩C
by simp_all blast+
lemma iso_cmp:
assumes "S.VV.ide μν"
shows "B.iso (cmp μν)"
using assms S.VV.ide_char⇩S⇩b⇩C S.VV.arr_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C cmp_def S.ide_char⇩S⇩b⇩C S.src_def S.trg_def
by auto
interpretation Φ⇩E: natural_isomorphism S.VV.comp V HoFF.map FoH.map cmp
proof
show "⋀μν. ¬ S.VV.arr μν ⟹ cmp μν = B.null"
using cmp_def by simp
fix μν
assume μν: "S.VV.arr μν"
have 1: "S.arr (fst μν) ∧ S.arr (snd μν) ∧ S.src (fst μν) = S.trg (snd μν)"
using μν S.VV.arr_char⇩S⇩b⇩C by simp
show "B.dom (cmp μν) = HoFF.map (S.VV.dom μν)"
using μν FF_def S.VV.arr_char⇩S⇩b⇩C S.VV.dom_char⇩S⇩b⇩C S.arr_dom S.src_def S.trg_def
S.dom_char⇩S⇩b⇩C S.src.preserves_dom S.trg.preserves_dom
apply simp
by (metis (no_types, lifting))
show "B.cod (cmp μν) = FoH.map (S.VV.cod μν)"
using μν 1 map_def S.hseq_char S.hcomp_def S.cod_char⇩S⇩b⇩C S.arr_cod S.VV.cod_simp
by simp
show "cmp (S.VV.cod μν) ⋅⇩B HoFF.map μν = cmp μν"
using μν 1 cmp_def S.VV.arr_char⇩S⇩b⇩C S.VV.cod_char⇩S⇩b⇩C FF_def S.arr_cod S.cod_simp
S.src_def S.trg_def map_def
apply simp
by (metis (no_types, lifting) B.comp_cod_arr B.hcomp_simps(4) cmp_simps(1) μν)
show "FoH.map μν ⋅⇩B cmp (S.VV.dom μν) = cmp μν"
unfolding cmp_def map_def
using μν S.VV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C S.VV.dom_char⇩S⇩b⇩C S.VV.cod_char⇩S⇩b⇩C B.comp_arr_dom
S.hcomp_def
apply simp
by (metis (no_types, lifting) B.hcomp_simps(3) cmp_def cmp_simps(1) S.arr_char⇩S⇩b⇩C
S.dom_char⇩S⇩b⇩C S.hcomp_closed S.src_def S.trg_def)
next
show "⋀fg. S.VV.ide fg ⟹ B.iso (cmp fg)"
using iso_cmp by simp
qed
sublocale pseudofunctor S.comp S.hcomp S.𝖺 𝗂 S.src S.trg V H 𝖺⇩B 𝗂 src⇩B trg⇩B map cmp
proof
fix f g h
assume f: "S.ide f" and g: "S.ide g" and h: "S.ide h"
and fg: "S.src f = S.trg g" and gh: "S.src g = S.trg h"
have 1: "B.ide f ∧ B.ide g ∧ B.ide h ∧ src⇩B f = trg⇩B g ∧ src⇩B g = trg⇩B h"
using f g h fg gh S.ide_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C S.src_def S.trg_def by simp
show "map (S.𝖺 f g h) ⋅⇩B cmp (f ⋆ g, h) ⋅⇩B cmp (f, g) ⋆⇩B map h =
cmp (f, g ⋆ h) ⋅⇩B (map f ⋆⇩B cmp (g, h)) ⋅⇩B 𝖺⇩B[map f, map g, map h]"
proof -
have "map (S.𝖺 f g h) ⋅⇩B cmp (f ⋆ g, h) ⋅⇩B cmp (f, g) ⋆⇩B map h =
𝖺⇩B[f, g, h] ⋅⇩B ((f ⋆⇩B g) ⋆⇩B h) ⋅⇩B ((f ⋆⇩B g) ⋆⇩B h)"
unfolding map_def cmp_def
using 1 f g h fg gh S.VVV.arr_char⇩S⇩b⇩C S.VV.arr_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C
B.comp_arr_dom S.arr_char⇩S⇩b⇩C S.comp_char S.hcomp_closed S.hcomp_def
S.ideD(1) S.src_def
by (simp add: S.assoc_closed)
also have "... = cmp (f, g ⋆ h) ⋅⇩B (map f ⋆⇩B cmp (g, h)) ⋅⇩B 𝖺⇩B[map f, map g, map h]"
unfolding cmp_def map_def
using 1 f g h fg gh S.VV.arr_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C
B.comp_arr_dom B.comp_cod_arr S.hcomp_def S.comp_char
S.arr_char⇩S⇩b⇩C S.assoc_closed S.hcomp_closed S.ideD(1) S.trg_def
by auto
finally show ?thesis by blast
qed
qed
lemma is_pseudofunctor:
shows "pseudofunctor S.comp S.hcomp S.𝖺 𝗂 S.src S.trg V H 𝖺⇩B 𝗂 src⇩B trg⇩B map cmp"
..
lemma map⇩0_simp [simp]:
assumes "S.obj a"
shows "map⇩0 a = a"
using assms map⇩0_def map_def S.obj_char by auto
lemma unit_char':
assumes "S.obj a"
shows "unit a = a"
proof -
have a: "S.arr a"
using assms by auto
have 1: "B.ide a"
using assms S.obj_char by auto
have 2: "src⇩B a = a"
using assms S.obj_char by auto
have "a = unit a"
proof (intro unit_eqI)
show "S.obj a" by fact
show "«a : map⇩0 a ⇒⇩B map a»"
using assms a 2 map⇩0_def map_def S.src_def S.dom_char⇩S⇩b⇩C S.cod_char⇩S⇩b⇩C S.obj_char
by auto
show "B.iso a"
using assms 1 by simp
show "a ⋅⇩B 𝗂[map⇩0 a] = (map 𝗂[a] ⋅⇩B cmp (a, a)) ⋅⇩B (a ⋆⇩B a)"
proof -
have "a ⋅⇩B 𝗂[a] = 𝗂[a] ⋅⇩B cmp (a, a) ⋅⇩B (a ⋆⇩B a)"
proof -
have "a ⋅⇩B 𝗂[a] = 𝗂[a]"
using assms 1 2 S.comp_cod_arr S.unitor_coincidence S.lunit_in_hom
S.obj_char S.comp_simp
by auto
moreover have "(a ⋆⇩B a) ⋅⇩B (a ⋆⇩B a) = a ⋆⇩B a"
using assms S.obj_char S.comp_ide_self by auto
moreover have "B.dom 𝗂[a] = a ⋆⇩B a"
using assms S.obj_char by simp
moreover have "𝗂[a] ⋅⇩B (a ⋆⇩B a) = 𝗂[a]"
using assms S.obj_char B.comp_arr_dom by simp
ultimately show ?thesis
using assms cmp_def S.VV.arr_char⇩S⇩b⇩C by auto
qed
thus ?thesis
using assms a 2 map⇩0_def map_def S.src_def B.comp_assoc by simp
qed
qed
thus ?thesis by simp
qed
end
subsection "Composition of Pseudofunctors"
text ‹
In this section, we show how pseudofunctors may be composed. The main work is to
establish the coherence condition for associativity.
›
locale composite_pseudofunctor =
B: bicategory V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B +
C: bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C +
D: bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D +
F: pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C F Φ⇩F +
G: pseudofunctor V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D G Φ⇩G
for V⇩B :: "'b comp" (infixr "⋅⇩B" 55)
and H⇩B :: "'b comp" (infixr "⋆⇩B" 53)
and 𝖺⇩B :: "'b ⇒ 'b ⇒ 'b ⇒ 'b" ("𝖺⇩B[_, _, _]")
and 𝗂⇩B :: "'b ⇒ 'b" ("𝗂⇩B[_]")
and src⇩B :: "'b ⇒ 'b"
and trg⇩B :: "'b ⇒ 'b"
and V⇩C :: "'c comp" (infixr "⋅⇩C" 55)
and H⇩C :: "'c comp" (infixr "⋆⇩C" 53)
and 𝖺⇩C :: "'c ⇒ 'c ⇒ 'c ⇒ 'c" ("𝖺⇩C[_, _, _]")
and 𝗂⇩C :: "'c ⇒ 'c" ("𝗂⇩C[_]")
and src⇩C :: "'c ⇒ 'c"
and trg⇩C :: "'c ⇒ 'c"
and V⇩D :: "'d comp" (infixr "⋅⇩D" 55)
and H⇩D :: "'d comp" (infixr "⋆⇩D" 53)
and 𝖺⇩D :: "'d ⇒ 'd ⇒ 'd ⇒ 'd" ("𝖺⇩D[_, _, _]")
and 𝗂⇩D :: "'d ⇒ 'd" ("𝗂⇩D[_]")
and src⇩D :: "'d ⇒ 'd"
and trg⇩D :: "'d ⇒ 'd"
and F :: "'b ⇒ 'c"
and Φ⇩F :: "'b * 'b ⇒ 'c"
and G :: "'c ⇒ 'd"
and Φ⇩G :: "'c * 'c ⇒ 'd"
begin
sublocale composite_functor V⇩B V⇩C V⇩D F G ..
sublocale weak_arrow_of_homs V⇩B src⇩B trg⇩B V⇩D src⇩D trg⇩D ‹G o F›
proof
show "⋀μ. B.arr μ ⟹ D.isomorphic ((G o F) (src⇩B μ)) (src⇩D ((G o F) μ))"
proof -
fix μ
assume μ: "B.arr μ"
show "D.isomorphic ((G o F) (src⇩B μ)) (src⇩D ((G o F) μ))"
proof -
have "(G o F) (src⇩B μ) = G (F (src⇩B μ))"
using μ by simp
also have "D.isomorphic ... (G (src⇩C (F μ)))"
using μ F.weakly_preserves_src G.preserves_iso
by (meson C.isomorphicE D.isomorphic_def G.preserves_hom)
also have "D.isomorphic ... (src⇩D (G (F μ)))"
using μ G.weakly_preserves_src by blast
also have "... = src⇩D ((G o F) μ)"
by simp
finally show ?thesis by blast
qed
qed
show "⋀μ. B.arr μ ⟹ D.isomorphic ((G o F) (trg⇩B μ)) (trg⇩D ((G o F) μ))"
proof -
fix μ
assume μ: "B.arr μ"
show "D.isomorphic ((G o F) (trg⇩B μ)) (trg⇩D ((G o F) μ))"
proof -
have "(G o F) (trg⇩B μ) = G (F (trg⇩B μ))"
using μ by simp
also have "D.isomorphic ... (G (trg⇩C (F μ)))"
using μ F.weakly_preserves_trg G.preserves_iso
by (meson C.isomorphicE D.isomorphic_def G.preserves_hom)
also have "D.isomorphic ... (trg⇩D (G (F μ)))"
using μ G.weakly_preserves_trg by blast
also have "... = trg⇩D ((G o F) μ)"
by simp
finally show ?thesis by blast
qed
qed
qed
interpretation H⇩DoGF_GF: composite_functor B.VV.comp D.VV.comp V⇩D FF
‹λμν. fst μν ⋆⇩D snd μν›
..
interpretation GFoH⇩B: composite_functor B.VV.comp V⇩B V⇩D ‹λμν. fst μν ⋆⇩B snd μν›
‹G o F›
..
definition cmp
where "cmp μν = (if B.VV.arr μν then
G (F (H⇩B (fst μν) (snd μν))) ⋅⇩D G (Φ⇩F (B.VV.dom μν)) ⋅⇩D
Φ⇩G (F (B.dom (fst μν)), F (B.dom (snd μν)))
else D.null)"
lemma cmp_in_hom [intro]:
assumes "B.VV.arr μν"
shows "«cmp μν : H⇩DoGF_GF.map (B.VV.dom μν) ⇒⇩D GFoH⇩B.map (B.VV.cod μν)»"
proof -
have "cmp μν = G (F (H⇩B (fst μν) (snd μν))) ⋅⇩D G (Φ⇩F (B.VV.dom μν)) ⋅⇩D
Φ⇩G (F (B.dom (fst μν)), F (B.dom (snd μν)))"
using assms cmp_def by simp
moreover have "« ... : H⇩DoGF_GF.map (B.VV.dom μν) ⇒⇩D GFoH⇩B.map (B.VV.cod μν)»"
proof (intro D.comp_in_homI)
show "«Φ⇩G (F (B.dom (fst μν)), F (B.dom (snd μν))) :
H⇩DoGF_GF.map (B.VV.dom μν)
⇒⇩D G (F (B.dom (fst μν)) ⋆⇩C F (B.dom (snd μν)))»"
using assms F.FF_def FF_def B.VV.arr_char⇩S⇩b⇩C B.VV.dom_simp by auto
show "«G (Φ⇩F (B.VV.dom μν)) :
G (F (B.dom (fst μν)) ⋆⇩C F (B.dom (snd μν)))
⇒⇩D GFoH⇩B.map (B.VV.dom μν)»"
using assms B.VV.arr_char⇩S⇩b⇩C F.FF_def B.VV.dom_simp B.VV.cod_simp by auto
show "«G (F (fst μν ⋆⇩B snd μν)) :
GFoH⇩B.map (B.VV.dom μν) ⇒⇩D GFoH⇩B.map (B.VV.cod μν)»"
proof -
have "B.VV.in_hom μν (B.VV.dom μν) (B.VV.cod μν)"
using assms by auto
thus ?thesis by auto
qed
qed
ultimately show ?thesis by argo
qed
lemma cmp_simps [simp]:
assumes "B.VV.arr μν"
shows "D.arr (cmp μν)"
and "D.dom (cmp μν) = H⇩DoGF_GF.map (B.VV.dom μν)"
and "D.cod (cmp μν) = GFoH⇩B.map (B.VV.cod μν)"
using assms cmp_in_hom by blast+
interpretation Φ: natural_transformation
B.VV.comp V⇩D H⇩DoGF_GF.map GFoH⇩B.map cmp
proof
show "⋀μν. ¬ B.VV.arr μν ⟹ cmp μν = D.null"
unfolding cmp_def by simp
fix μν
assume μν: "B.VV.arr μν"
show "D.dom (cmp μν) = H⇩DoGF_GF.map (B.VV.dom μν)"
using μν cmp_in_hom by blast
show "D.cod (cmp μν) = GFoH⇩B.map (B.VV.cod μν)"
using μν cmp_in_hom by blast
show "GFoH⇩B.map μν ⋅⇩D cmp (B.VV.dom μν) = cmp μν"
unfolding cmp_def
using μν B.VV.ide_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C D.comp_ide_arr B.VV.dom_char⇩S⇩b⇩C D.comp_assoc
as_nat_trans.is_natural_1
apply simp
by (metis (no_types, lifting) B.H.preserves_arr B.hcomp_simps(3))
show "cmp (B.VV.cod μν) ⋅⇩D H⇩DoGF_GF.map μν = cmp μν"
proof -
have "cmp (B.VV.cod μν) ⋅⇩D H⇩DoGF_GF.map μν =
(G (F (B.cod (fst μν) ⋆⇩B B.cod (snd μν))) ⋅⇩D
G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))) ⋅⇩D
Φ⇩G (F (B.cod (fst μν)), F (B.cod (snd μν)))) ⋅⇩D
(fst (FF μν) ⋆⇩D snd (FF μν))"
unfolding cmp_def
using μν B.VV.arr_char⇩S⇩b⇩C B.VV.dom_simp B.VV.cod_simp by simp
also have "... = (G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))) ⋅⇩D
Φ⇩G (F (B.cod (fst μν)), F (B.cod (snd μν)))) ⋅⇩D
(fst (FF μν) ⋆⇩D snd (FF μν))"
proof -
have "D.ide (G (F (B.cod (fst μν) ⋆⇩B B.cod (snd μν))))"
using μν B.VV.arr_char⇩S⇩b⇩C by simp
moreover have "D.seq (G (F (B.cod (fst μν) ⋆⇩B B.cod (snd μν))))
(G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))) ⋅⇩D
Φ⇩G (F (B.cod (fst μν)), F (B.cod (snd μν))))"
using μν B.VV.arr_char⇩S⇩b⇩C B.VV.dom_char⇩S⇩b⇩C B.VV.cod_char⇩S⇩b⇩C F.FF_def
apply (intro D.seqI)
apply auto
proof -
show "G (F (B.cod (fst μν) ⋆⇩B B.cod (snd μν))) =
D.cod (G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))) ⋅⇩D
Φ⇩G (F (B.cod (fst μν)), F (B.cod (snd μν))))"
proof -
have "D.seq (G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))))
(Φ⇩G (F (B.cod (fst μν)), F (B.cod (snd μν))))"
using μν B.VV.arr_char⇩S⇩b⇩C F.FF_def B.VV.arr_char⇩S⇩b⇩C B.VV.dom_char⇩S⇩b⇩C B.VV.cod_char⇩S⇩b⇩C
by (intro D.seqI) auto
thus ?thesis
using μν B.VV.arr_char⇩S⇩b⇩C B.VV.cod_simp by simp
qed
qed
ultimately show ?thesis
using μν D.comp_ide_arr [of "G (F (B.cod (fst μν) ⋆⇩B B.cod (snd μν)))"
"G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))) ⋅⇩D
Φ⇩G (F (B.cod (fst μν)), F (B.cod (snd μν)))"]
by simp
qed
also have "... = G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))) ⋅⇩D
(Φ⇩G (F (B.cod (fst μν)), F (B.cod (snd μν))) ⋅⇩D
(fst (FF μν) ⋆⇩D snd (FF μν)))"
using D.comp_assoc by simp
also have "... = G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))) ⋅⇩D
Φ⇩G (C.VV.cod (F.FF μν)) ⋅⇩D G.H⇩DoFF.map (F.FF μν)"
using μν B.VV.arr_char⇩S⇩b⇩C F.FF_def G.FF_def FF_def C.VV.cod_simp by auto
also have "... = G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))) ⋅⇩D
G.FoH⇩C.map (F.FF μν) ⋅⇩D Φ⇩G (C.VV.dom (F.FF μν))"
using μν B.VV.arr_char⇩S⇩b⇩C G.Φ.naturality C.VV.dom_simp C.VV.cod_simp by simp
also have "... = (G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))) ⋅⇩D
G.FoH⇩C.map (F.FF μν)) ⋅⇩D Φ⇩G (C.VV.dom (F.FF μν))"
using D.comp_assoc by simp
also have "... = (G (Φ⇩F (B.VV.cod μν) ⋅⇩C F.H⇩DoFF.map μν)) ⋅⇩D
Φ⇩G (C.VV.dom (F.FF μν))"
proof -
have "(B.cod (fst μν), B.cod (snd μν)) = B.VV.cod μν"
using μν B.VV.arr_char⇩S⇩b⇩C B.VV.cod_simp by simp
moreover have "G.FoH⇩C.map (F.FF μν) = G (F.H⇩DoFF.map μν)"
using μν F.FF_def by simp
moreover have "G (Φ⇩F (B.cod (fst μν), B.cod (snd μν))) ⋅⇩D G (F.H⇩DoFF.map μν) =
G (Φ⇩F (B.VV.cod μν) ⋅⇩C F.H⇩DoFF.map μν)"
using μν B.VV.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting) F.Φ.is_natural_2 F.Φ.preserves_reflects_arr
G.preserves_comp calculation(1))
ultimately show ?thesis by argo
qed
also have "... = G (F.FoH⇩C.map μν ⋅⇩C Φ⇩F (B.VV.dom μν)) ⋅⇩D
Φ⇩G (C.VV.dom (F.FF μν))"
using μν F.Φ.naturality [of μν] F.FF_def by simp
also have "... = G (F.FoH⇩C.map μν) ⋅⇩D G (Φ⇩F (B.VV.dom μν)) ⋅⇩D
Φ⇩G (C.VV.dom (F.FF μν))"
proof -
have "G (F.FoH⇩C.map μν ⋅⇩C Φ⇩F (B.VV.dom μν)) =
G (F.FoH⇩C.map μν) ⋅⇩D G (Φ⇩F (B.VV.dom μν))"
using μν
by (metis (mono_tags, lifting) F.Φ.is_natural_1 F.Φ.preserves_reflects_arr
G.preserves_comp)
thus ?thesis
using μν D.comp_assoc by simp
qed
also have "... = cmp μν"
using μν B.VV.arr_char⇩S⇩b⇩C cmp_def F.FF_def F.FF.preserves_dom B.VV.dom_simp
by auto
finally show ?thesis by simp
qed
qed
interpretation Φ: natural_isomorphism B.VV.comp V⇩D H⇩DoGF_GF.map GFoH⇩B.map cmp
proof
show "⋀hk. B.VV.ide hk ⟹ D.iso (cmp hk)"
proof -
fix hk
assume hk: "B.VV.ide hk"
have "D.iso (G (F (fst hk ⋆⇩B snd hk)) ⋅⇩D G (Φ⇩F (B.VV.dom hk)) ⋅⇩D
Φ⇩G (F (B.dom (fst hk)), F (B.dom (snd hk))))"
proof (intro D.isos_compose)
show "D.iso (Φ⇩G (F (B.dom (fst hk)), F (B.dom (snd hk))))"
using hk G.Φ.components_are_iso [of "(F (B.dom (fst hk)), F (B.dom (snd hk)))"]
C.VV.ide_char B.VV.arr_char⇩S⇩b⇩C B.VV.dom_char⇩S⇩b⇩C
by (metis (no_types, lifting) B.VV.ideD(1) B.VV.ideD(2) B.VxV.dom_char
F.FF_def F.FF.as_nat_iso.components_are_iso G.Φ.preserves_iso fst_conv snd_conv)
show "D.iso (G (Φ⇩F (B.VV.dom hk)))"
using hk F.Φ.components_are_iso B.VV.arr_char⇩S⇩b⇩C B.VV.dom_char⇩S⇩b⇩C B.VV.ideD(2)
by auto
show "D.seq (G (Φ⇩F (B.VV.dom hk))) (Φ⇩G (F (B.dom (fst hk)), F (B.dom (snd hk))))"
using hk B.VV.arr_char⇩S⇩b⇩C B.VV.ide_char⇩S⇩b⇩C B.VV.dom_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C F.FF_def
C.VV.dom_simp C.VV.cod_simp
by auto
show "D.iso (G (F (fst hk ⋆⇩B snd hk)))"
using hk F.Φ.components_are_iso B.VV.arr_char⇩S⇩b⇩C by simp
show "D.seq (G (F (fst hk ⋆⇩B snd hk)))
(G (Φ⇩F (B.VV.dom hk)) ⋅⇩D Φ⇩G (F (B.dom (fst hk)), F (B.dom (snd hk))))"
using hk B.VV.arr_char⇩S⇩b⇩C B.VV.dom_char⇩S⇩b⇩C
by (metis (no_types, lifting) B.VV.ideD(1) cmp_def cmp_simps(1))
qed
thus "D.iso (cmp hk)"
unfolding cmp_def using hk by simp
qed
qed
sublocale pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ‹G o F› cmp
proof
fix f g h
assume f: "B.ide f" and g: "B.ide g" and h: "B.ide h"
assume fg: "src⇩B f = trg⇩B g" and gh: "src⇩B g = trg⇩B h"
show "map 𝖺⇩B[f, g, h] ⋅⇩D cmp (f ⋆⇩B g, h) ⋅⇩D (cmp (f, g) ⋆⇩D map h) =
cmp (f, g ⋆⇩B h) ⋅⇩D (map f ⋆⇩D cmp (g, h)) ⋅⇩D 𝖺⇩D[map f, map g, map h]"
proof -
have "map 𝖺⇩B[f, g, h] ⋅⇩D cmp (f ⋆⇩B g, h) ⋅⇩D (cmp (f, g) ⋆⇩D map h) =
G (F 𝖺⇩B[f, g, h]) ⋅⇩D
(G (F ((f ⋆⇩B g) ⋆⇩B h)) ⋅⇩D G (Φ⇩F (f ⋆⇩B g, h)) ⋅⇩D Φ⇩G (F (f ⋆⇩B g), F h)) ⋅⇩D
(G (F (f ⋆⇩B g)) ⋅⇩D G (Φ⇩F (f, g)) ⋅⇩D Φ⇩G (F f, F g) ⋆⇩D G (F h))"
unfolding cmp_def
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C B.VV.dom_simp by simp
also have "... = G (F 𝖺⇩B[f, g, h]) ⋅⇩D
(G (Φ⇩F (f ⋆⇩B g, h)) ⋅⇩D Φ⇩G (F (f ⋆⇩B g), F h)) ⋅⇩D
(G (F (f ⋆⇩B g)) ⋅⇩D G (Φ⇩F (f, g)) ⋅⇩D Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using f g h fg gh D.comp_ide_arr D.comp_assoc
by (metis B.ideD(1) B.ide_hcomp B.src_hcomp F.cmp_simps(1) F.cmp_simps(5)
G.as_nat_trans.is_natural_2)
also have "... = G (F 𝖺⇩B[f, g, h]) ⋅⇩D
(G (Φ⇩F (f ⋆⇩B g, h)) ⋅⇩D Φ⇩G (F (f ⋆⇩B g), F h)) ⋅⇩D
(G (Φ⇩F (f, g)) ⋅⇩D Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using f g fg
by (metis (no_types) D.comp_assoc F.cmp_simps(1) F.cmp_simps(5)
G.as_nat_trans.is_natural_2)
also have "... = (G (F 𝖺⇩B[f, g, h]) ⋅⇩D G (Φ⇩F (f ⋆⇩B g, h))) ⋅⇩D
Φ⇩G (F (f ⋆⇩B g), F h) ⋅⇩D (G (Φ⇩F (f, g)) ⋅⇩D Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using D.comp_assoc by simp
also have "... = G (F 𝖺⇩B[f, g, h] ⋅⇩C Φ⇩F (f ⋆⇩B g, h)) ⋅⇩D
Φ⇩G (F (f ⋆⇩B g), F h) ⋅⇩D (G (Φ⇩F (f, g)) ⋅⇩D Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C B.VV.cod_simp by simp
also have "... = G (F 𝖺⇩B[f, g, h] ⋅⇩C Φ⇩F (f ⋆⇩B g, h)) ⋅⇩D
Φ⇩G (F (f ⋆⇩B g), F h) ⋅⇩D (G (Φ⇩F (f, g)) ⋆⇩D G (F h)) ⋅⇩D
(Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C F.FF_def D.whisker_right
B.VV.dom_simp C.VV.cod_simp
by auto
also have "... = G (F 𝖺⇩B[f, g, h] ⋅⇩C Φ⇩F (f ⋆⇩B g, h)) ⋅⇩D
(Φ⇩G (F (f ⋆⇩B g), F h) ⋅⇩D (G (Φ⇩F (f, g)) ⋆⇩D G (F h))) ⋅⇩D
(Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using D.comp_assoc by simp
also have "... = G (F 𝖺⇩B[f, g, h] ⋅⇩C Φ⇩F (f ⋆⇩B g, h)) ⋅⇩D
(G (Φ⇩F (f, g) ⋆⇩C F h) ⋅⇩D Φ⇩G (F f ⋆⇩C F g, F h)) ⋅⇩D
(Φ⇩G (F f, F g) ⋆⇩D G (F h))"
proof -
have "Φ⇩G (F (f ⋆⇩B g), F h) = Φ⇩G (C.VV.cod (Φ⇩F (f, g), F h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C B.VV.cod_simp C.VV.cod_simp
by simp
moreover have "G (Φ⇩F (f, g)) ⋆⇩D G (F h) = G.H⇩DoFF.map (Φ⇩F (f, g), F h)"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C G.FF_def by simp
moreover have "G.FoH⇩C.map (Φ⇩F (f, g), F h) = G (Φ⇩F (f, g) ⋆⇩C F h)"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C by simp
moreover have "Φ⇩G (C.VV.dom (Φ⇩F (f, g), F h)) = Φ⇩G (F f ⋆⇩C F g, F h)"
using f g h fg gh C.VV.arr_char⇩S⇩b⇩C F.cmp_in_hom [of f g] C.VV.dom_simp by auto
ultimately show ?thesis
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C G.Φ.naturality
by (metis (mono_tags, lifting) C.VV.arr_cod_iff_arr C.VV.arr_dom_iff_arr
G.FoH⇩C.is_extensional G.H⇩DoFF.is_extensional G.Φ.is_extensional)
qed
also have "... = (G (F 𝖺⇩B[f, g, h] ⋅⇩C Φ⇩F (f ⋆⇩B g, h)) ⋅⇩D (G (Φ⇩F (f, g) ⋆⇩C F h))) ⋅⇩D
Φ⇩G (F f ⋆⇩C F g, F h) ⋅⇩D (Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using D.comp_assoc by simp
also have "... = G ((F 𝖺⇩B[f, g, h] ⋅⇩C Φ⇩F (f ⋆⇩B g, h)) ⋅⇩C (Φ⇩F (f, g) ⋆⇩C F h)) ⋅⇩D
Φ⇩G (F f ⋆⇩C F g, F h) ⋅⇩D (Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C F.FF_def B.VV.dom_simp B.VV.cod_simp by auto
also have "... = G (F 𝖺⇩B[f, g, h] ⋅⇩C Φ⇩F (f ⋆⇩B g, h) ⋅⇩C (Φ⇩F (f, g) ⋆⇩C F h)) ⋅⇩D
Φ⇩G (F f ⋆⇩C F g, F h) ⋅⇩D (Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using C.comp_assoc by simp
also have "... = G (Φ⇩F (f, g ⋆⇩B h) ⋅⇩C (F f ⋆⇩C Φ⇩F (g, h)) ⋅⇩C 𝖺⇩C[F f, F g, F h]) ⋅⇩D
Φ⇩G (F f ⋆⇩C F g, F h) ⋅⇩D (Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using f g h fg gh F.assoc_coherence [of f g h] by simp
also have "... = G ((Φ⇩F (f, g ⋆⇩B h) ⋅⇩C (F f ⋆⇩C Φ⇩F (g, h))) ⋅⇩C 𝖺⇩C[F f, F g, F h]) ⋅⇩D
Φ⇩G (F f ⋆⇩C F g, F h) ⋅⇩D (Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using C.comp_assoc by simp
also have "... = (G (Φ⇩F (f, g ⋆⇩B h) ⋅⇩C (F f ⋆⇩C Φ⇩F (g, h))) ⋅⇩D G 𝖺⇩C[F f, F g, F h]) ⋅⇩D
Φ⇩G (F f ⋆⇩C F g, F h) ⋅⇩D (Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C F.FF_def B.VV.dom_simp B.VV.cod_simp by auto
also have "... = G (Φ⇩F (f, g ⋆⇩B h) ⋅⇩C (F f ⋆⇩C Φ⇩F (g, h))) ⋅⇩D
G 𝖺⇩C[F f, F g, F h] ⋅⇩D Φ⇩G (F f ⋆⇩C F g, F h) ⋅⇩D
(Φ⇩G (F f, F g) ⋆⇩D G (F h))"
using D.comp_assoc by simp
also have "... = G (Φ⇩F (f, g ⋆⇩B h) ⋅⇩C (F f ⋆⇩C Φ⇩F (g, h))) ⋅⇩D
Φ⇩G (F f, F g ⋆⇩C F h) ⋅⇩D (G (F f) ⋆⇩D Φ⇩G (F g, F h)) ⋅⇩D
𝖺⇩D[G (F f), G (F g), G (F h)]"
using f g h fg gh G.assoc_coherence [of "F f" "F g" "F h"] by simp
also have "... = (G (Φ⇩F (f, g ⋆⇩B h) ⋅⇩C (F f ⋆⇩C Φ⇩F (g, h))) ⋅⇩D
Φ⇩G (F f, F g ⋆⇩C F h) ⋅⇩D (G (F f) ⋆⇩D Φ⇩G (F g, F h))) ⋅⇩D
𝖺⇩D[G (F f), G (F g), G (F h)]"
using D.comp_assoc by simp
also have "... = (cmp (f, g ⋆⇩B h) ⋅⇩D (G (F f) ⋆⇩D cmp (g, h))) ⋅⇩D
𝖺⇩D[G (F f), G (F g), G (F h)]"
proof -
have "G (Φ⇩F (f, g ⋆⇩B h) ⋅⇩C (F f ⋆⇩C Φ⇩F (g, h))) ⋅⇩D
Φ⇩G (F f, F g ⋆⇩C F h) ⋅⇩D (G (F f) ⋆⇩D Φ⇩G (F g, F h)) =
cmp (f, g ⋆⇩B h) ⋅⇩D (G (F f) ⋆⇩D cmp (g, h))"
proof -
have "cmp (f, g ⋆⇩B h) ⋅⇩D (G (F f) ⋆⇩D cmp (g, h)) =
(G (F (f ⋆⇩B g ⋆⇩B h)) ⋅⇩D G (Φ⇩F (f, g ⋆⇩B h)) ⋅⇩D Φ⇩G (F f, F (g ⋆⇩B h))) ⋅⇩D
(G (F f) ⋆⇩D G (F (g ⋆⇩B h)) ⋅⇩D G (Φ⇩F (g, h)) ⋅⇩D Φ⇩G (F g, F h))"
unfolding cmp_def
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C B.VV.dom_simp B.VV.cod_simp by simp
also have "... = (G (Φ⇩F (f, g ⋆⇩B h)) ⋅⇩D Φ⇩G (F f, F (g ⋆⇩B h))) ⋅⇩D
(G (F f) ⋆⇩D G (F (g ⋆⇩B h)) ⋅⇩D G (Φ⇩F (g, h)) ⋅⇩D Φ⇩G (F g, F h))"
proof -
have "G (F (f ⋆⇩B g ⋆⇩B h)) ⋅⇩D G (Φ⇩F (f, g ⋆⇩B h)) = G (Φ⇩F (f, g ⋆⇩B h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C D.comp_ide_arr B.VV.dom_simp B.VV.cod_simp
by simp
thus ?thesis
using D.comp_assoc by metis
qed
also have "... = G (Φ⇩F (f, g ⋆⇩B h)) ⋅⇩D Φ⇩G (F f, F (g ⋆⇩B h)) ⋅⇩D
(G (F f) ⋆⇩D G (F (g ⋆⇩B h)) ⋅⇩D G (Φ⇩F (g, h)) ⋅⇩D Φ⇩G (F g, F h))"
using D.comp_assoc by simp
also have "... = G (Φ⇩F (f, g ⋆⇩B h)) ⋅⇩D Φ⇩G (F f, F (g ⋆⇩B h)) ⋅⇩D
(G (F f) ⋆⇩D G (Φ⇩F (g, h)) ⋅⇩D Φ⇩G (F g, F h))"
proof -
have "G (F (g ⋆⇩B h)) ⋅⇩D G (Φ⇩F (g, h)) = G (Φ⇩F (g, h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C D.comp_ide_arr B.VV.dom_simp B.VV.cod_simp
by simp
thus ?thesis
using D.comp_assoc by metis
qed
also have "... = G (Φ⇩F (f, g ⋆⇩B h)) ⋅⇩D Φ⇩G (F f, F (g ⋆⇩B h)) ⋅⇩D
(G (F f) ⋆⇩D G (Φ⇩F (g, h))) ⋅⇩D (G (F f) ⋆⇩D Φ⇩G (F g, F h))"
using f g h fg gh
D.whisker_left [of "G (F f)" "G (Φ⇩F (g, h))" "Φ⇩G (F g, F h)"]
by fastforce
also have "... = G (Φ⇩F (f, g ⋆⇩B h)) ⋅⇩D
(Φ⇩G (F f, F (g ⋆⇩B h)) ⋅⇩D (G (F f) ⋆⇩D G (Φ⇩F (g, h)))) ⋅⇩D
(G (F f) ⋆⇩D Φ⇩G (F g, F h))"
using D.comp_assoc by simp
also have "... = G (Φ⇩F (f, g ⋆⇩B h)) ⋅⇩D
(G (F f ⋆⇩C Φ⇩F (g, h)) ⋅⇩D Φ⇩G (F f, F g ⋆⇩C F h)) ⋅⇩D
(G (F f) ⋆⇩D Φ⇩G (F g, F h))"
proof -
have "Φ⇩G (C.VV.cod (F f, Φ⇩F (g, h))) = Φ⇩G (F f, F (g ⋆⇩B h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C B.VV.dom_simp B.VV.cod_simp
by auto
moreover have "G.H⇩DoFF.map (F f, Φ⇩F (g, h)) = G (F f) ⋆⇩D G (Φ⇩F (g, h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C G.FF_def by auto
moreover have "G.FoH⇩C.map (F f, Φ⇩F (g, h)) = G (F f ⋆⇩C Φ⇩F (g, h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C by simp
moreover have "C.VV.dom (F f, Φ⇩F (g, h)) = (F f, F g ⋆⇩C F h)"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C C.VV.dom_char⇩S⇩b⇩C
F.cmp_in_hom [of g h]
by auto
ultimately show ?thesis
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C
G.Φ.naturality [of "(F f, Φ⇩F (g, h))"]
by simp
qed
also have "... = (G (Φ⇩F (f, g ⋆⇩B h)) ⋅⇩D (G (F f ⋆⇩C Φ⇩F (g, h)))) ⋅⇩D
Φ⇩G (F f, F g ⋆⇩C F h) ⋅⇩D (G (F f) ⋆⇩D Φ⇩G (F g, F h))"
using D.comp_assoc by simp
also have "... = G (Φ⇩F (f, g ⋆⇩B h) ⋅⇩C (F f ⋆⇩C Φ⇩F (g, h))) ⋅⇩D
Φ⇩G (F f, F g ⋆⇩C F h) ⋅⇩D (G (F f) ⋆⇩D Φ⇩G (F g, F h))"
using f g h fg gh B.VV.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting) B.assoc_simps(1) C.comp_assoc C.seqE
F.preserves_assoc(1) F.preserves_reflects_arr G.preserves_comp)
finally show ?thesis by simp
qed
thus ?thesis by simp
qed
also have "... = cmp (f, g ⋆⇩B h) ⋅⇩D (G (F f) ⋆⇩D cmp (g, h)) ⋅⇩D
𝖺⇩D[G (F f), G (F g), G (F h)]"
using D.comp_assoc by simp
finally show ?thesis by simp
qed
qed
lemma is_pseudofunctor:
shows "pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D (G o F) cmp"
..
lemma map⇩0_simp [simp]:
assumes "B.obj a"
shows "map⇩0 a = G.map⇩0 (F.map⇩0 a)"
using assms map⇩0_def by auto
lemma unit_char':
assumes "B.obj a"
shows "unit a = G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a)"
proof -
have "G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a) = unit a"
proof (intro unit_eqI [of a "G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a)"])
show "B.obj a" by fact
show "«G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a) : map⇩0 a ⇒⇩D map a»"
using assms by auto
show "D.iso (G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a))"
by (simp add: D.isos_compose F.unit_char(2) G.unit_char(2) assms)
show "(G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a)) ⋅⇩D 𝗂⇩D[map⇩0 a] =
(map 𝗂⇩B[a] ⋅⇩D cmp (a, a)) ⋅⇩D
(G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a) ⋆⇩D G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a))"
proof -
have 1: "cmp (a, a) = G (Φ⇩F (a, a)) ⋅⇩D Φ⇩G (F a, F a)"
proof -
have "cmp (a, a) = (G (F (a ⋆⇩B a)) ⋅⇩D G (Φ⇩F (a, a))) ⋅⇩D Φ⇩G (F a, F a)"
using assms cmp_def B.VV.ide_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C B.VV.dom_char⇩S⇩b⇩C B.VV.cod_char⇩S⇩b⇩C
B.VxV.dom_char B.objE D.comp_assoc B.obj_simps
by simp
also have "... = G (Φ⇩F (a, a)) ⋅⇩D Φ⇩G (F a, F a)"
using assms D.comp_cod_arr B.VV.arr_char⇩S⇩b⇩C B.VV.ide_char⇩S⇩b⇩C by auto
finally show ?thesis by blast
qed
have "(map 𝗂⇩B[a] ⋅⇩D cmp (a, a)) ⋅⇩D
(G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a) ⋆⇩D G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a)) =
map 𝗂⇩B[a] ⋅⇩D G (Φ⇩F (a, a)) ⋅⇩D
(Φ⇩G (F a, F a) ⋅⇩D (G (F.unit a) ⋆⇩D G (F.unit a))) ⋅⇩D
(G.unit (F.map⇩0 a) ⋆⇩D G.unit (F.map⇩0 a))"
using assms 1 D.comp_assoc D.interchange by simp
also have "... = (map 𝗂⇩B[a] ⋅⇩D G (Φ⇩F (a, a)) ⋅⇩D G (F.unit a ⋆⇩C F.unit a)) ⋅⇩D
Φ⇩G (F.map⇩0 a, F.map⇩0 a) ⋅⇩D
(G.unit (F.map⇩0 a) ⋆⇩D G.unit (F.map⇩0 a))"
using assms G.Φ.naturality [of "(F.unit a, F.unit a)"]
C.VV.arr_char⇩S⇩b⇩C C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C G.FF_def D.comp_assoc
by simp
also have "... = (G (F 𝗂⇩B[a] ⋅⇩C Φ⇩F (a, a) ⋅⇩C (F.unit a ⋆⇩C F.unit a))) ⋅⇩D
Φ⇩G (F.map⇩0 a, F.map⇩0 a) ⋅⇩D
(G.unit (F.map⇩0 a) ⋆⇩D G.unit (F.map⇩0 a))"
proof -
have "C.arr (F 𝗂⇩B[a] ⋅⇩C Φ⇩F (a, a) ⋅⇩C (F.unit a ⋆⇩C F.unit a))"
using assms B.VV.ide_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C F.cmp_in_hom(2)
by (intro C.seqI' C.comp_in_homI) auto
hence "map 𝗂⇩B[a] ⋅⇩D G (Φ⇩F (a, a)) ⋅⇩D G (F.unit a ⋆⇩C F.unit a) =
G (F 𝗂⇩B[a] ⋅⇩C Φ⇩F (a, a) ⋅⇩C (F.unit a ⋆⇩C F.unit a))"
by auto
thus ?thesis by argo
qed
also have "... = G (F.unit a ⋅⇩C 𝗂⇩C[F.map⇩0 a]) ⋅⇩D
Φ⇩G (F.map⇩0 a, F.map⇩0 a) ⋅⇩D
(G.unit (F.map⇩0 a) ⋆⇩D G.unit (F.map⇩0 a))"
using assms F.unit_char C.comp_assoc by simp
also have "... = G (F.unit a) ⋅⇩D (G 𝗂⇩C[F.map⇩0 a] ⋅⇩D
Φ⇩G (F.map⇩0 a, F.map⇩0 a)) ⋅⇩D
(G.unit (F.map⇩0 a) ⋆⇩D G.unit (F.map⇩0 a))"
using assms D.comp_assoc by simp
also have "... = (G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a)) ⋅⇩D 𝗂⇩D[G.map⇩0 (F.map⇩0 a)]"
using assms G.unit_char D.comp_assoc by simp
also have "... = (G (F.unit a) ⋅⇩D G.unit (F.map⇩0 a)) ⋅⇩D 𝗂⇩D[map⇩0 a]"
using assms map⇩0_def by auto
finally show ?thesis by simp
qed
qed
thus ?thesis by simp
qed
end
subsection "Restriction of Pseudofunctors"
text ‹
In this section, we construct the restriction and corestriction of a pseudofunctor to
a subbicategory of its domain and codomain, respectively.
›
locale restricted_pseudofunctor =
C: bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C +
D: bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D +
F: pseudofunctor V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ +
C': subbicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C Arr
for V⇩C :: "'c comp" (infixr "⋅⇩C" 55)
and H⇩C :: "'c comp" (infixr "⋆⇩C" 53)
and 𝖺⇩C :: "'c ⇒ 'c ⇒ 'c ⇒ 'c" ("𝖺⇩C[_, _, _]")
and 𝗂⇩C :: "'c ⇒ 'c" ("𝗂⇩C[_]")
and src⇩C :: "'c ⇒ 'c"
and trg⇩C :: "'c ⇒ 'c"
and V⇩D :: "'d comp" (infixr "⋅⇩D" 55)
and H⇩D :: "'d comp" (infixr "⋆⇩D" 53)
and 𝖺⇩D :: "'d ⇒ 'd ⇒ 'd ⇒ 'd" ("𝖺⇩D[_, _, _]")
and 𝗂⇩D :: "'d ⇒ 'd" ("𝗂⇩D[_]")
and src⇩D :: "'d ⇒ 'd"
and trg⇩D :: "'d ⇒ 'd"
and F :: "'c ⇒ 'd"
and Φ :: "'c * 'c ⇒ 'd"
and Arr :: "'c ⇒ bool"
begin
abbreviation map
where "map ≡ λμ. if C'.arr μ then F μ else D.null"
abbreviation cmp
where "cmp ≡ λμν. if C'.VV.arr μν then Φ μν else D.null"
interpretation "functor" C'.comp V⇩D map
using C'.inclusion C'.arr_char⇩S⇩b⇩C C'.dom_char⇩S⇩b⇩C C'.cod_char⇩S⇩b⇩C C'.seq_char⇩S⇩b⇩C C'.comp_char
C'.arr_dom C'.arr_cod
apply (unfold_locales)
apply auto
by presburger
interpretation weak_arrow_of_homs C'.comp C'.src C'.trg V⇩D src⇩D trg⇩D map
using C'.arrE C'.ide_src C'.ide_trg C'.inclusion C'.src_def C'.trg_def
F.weakly_preserves_src F.weakly_preserves_trg
by unfold_locales auto
interpretation H⇩D⇩'oFF: composite_functor C'.VV.comp D.VV.comp V⇩D FF
‹λμν. fst μν ⋆⇩D snd μν›
..
interpretation FoH⇩C⇩': composite_functor C'.VV.comp C'.comp V⇩D
‹λμν. C'.hcomp (fst μν) (snd μν)› map
..
interpretation Φ: natural_transformation C'.VV.comp V⇩D H⇩D⇩'oFF.map FoH⇩C⇩'.map cmp
using C'.arr_char⇩S⇩b⇩C C'.dom_char⇩S⇩b⇩C C'.cod_char⇩S⇩b⇩C C'.VV.arr_char⇩S⇩b⇩C C'.VV.dom_char⇩S⇩b⇩C C'.VV.cod_char⇩S⇩b⇩C
FF_def C'.inclusion C'.dom_closed C'.cod_closed C'.src_def C'.trg_def
C'.hcomp_def C'.hcomp_closed F.Φ.is_natural_1 F.Φ.is_natural_2
C.VV.arr_char⇩S⇩b⇩C C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C F.FF_def
by unfold_locales auto
interpretation Φ: natural_isomorphism C'.VV.comp V⇩D H⇩D⇩'oFF.map FoH⇩C⇩'.map cmp
using C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C C'.VV.ide_char⇩S⇩b⇩C C'.VV.arr_char⇩S⇩b⇩C C'.arr_char⇩S⇩b⇩C
C'.src_def C'.trg_def C'.ide_char⇩S⇩b⇩C F.Φ.components_are_iso
by unfold_locales auto
sublocale pseudofunctor C'.comp C'.hcomp C'.𝖺 𝗂⇩C C'.src C'.trg V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D
map cmp
using F.assoc_coherence C'.VVV.arr_char⇩S⇩b⇩C C'.VV.arr_char⇩S⇩b⇩C C'.arr_char⇩S⇩b⇩C C'.hcomp_def
C'.src_def C'.trg_def C'.assoc_closed C'.hcomp_closed C'.ide_char⇩S⇩b⇩C
by unfold_locales auto
lemma is_pseudofunctor:
shows "pseudofunctor C'.comp C'.hcomp C'.𝖺 𝗂⇩C C'.src C'.trg V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D map cmp"
..
lemma map⇩0_simp [simp]:
assumes "C'.obj a"
shows "map⇩0 a = F.map⇩0 a"
using assms map⇩0_def C'.obj_char by auto
lemma unit_char':
assumes "C'.obj a"
shows "F.unit a = unit a"
using assms map⇩0_simp C'.obj_char F.unit_in_hom(2) [of a] F.unit_char(2-3) 𝗂_simps(1)
apply (intro unit_eqI)
apply auto
by blast
end
text ‹
We define the corestriction construction only for the case of sub-bicategories
determined by a set of objects of the ambient bicategory.
There are undoubtedly more general constructions, but this one is adequate for our
present needs.
›
locale corestricted_pseudofunctor =
C: bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C +
D: bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D +
F: pseudofunctor V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ +
D': subbicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ‹λμ. D.arr μ ∧ Obj (src⇩D μ) ∧ Obj (trg⇩D μ)›
for V⇩C :: "'c comp" (infixr "⋅⇩C" 55)
and H⇩C :: "'c comp" (infixr "⋆⇩C" 53)
and 𝖺⇩C :: "'c ⇒ 'c ⇒ 'c ⇒ 'c" ("𝖺⇩C[_, _, _]")
and 𝗂⇩C :: "'c ⇒ 'c" ("𝗂⇩C[_]")
and src⇩C :: "'c ⇒ 'c"
and trg⇩C :: "'c ⇒ 'c"
and V⇩D :: "'d comp" (infixr "⋅⇩D" 55)
and H⇩D :: "'d comp" (infixr "⋆⇩D" 53)
and 𝖺⇩D :: "'d ⇒ 'd ⇒ 'd ⇒ 'd" ("𝖺⇩D[_, _, _]")
and 𝗂⇩D :: "'d ⇒ 'd" ("𝗂⇩D[_]")
and src⇩D :: "'d ⇒ 'd"
and trg⇩D :: "'d ⇒ 'd"
and F :: "'c ⇒ 'd"
and Φ :: "'c * 'c ⇒ 'd"
and Obj :: "'d ⇒ bool" +
assumes preserves_arr: "⋀μ. C.arr μ ⟹ D'.arr (F μ)"
begin
abbreviation map
where "map ≡ F"
abbreviation cmp
where "cmp ≡ Φ"
interpretation "functor" V⇩C D'.comp F
using preserves_arr F.is_extensional D'.arr_char⇩S⇩b⇩C D'.dom_char⇩S⇩b⇩C D'.cod_char⇩S⇩b⇩C D'.comp_char
by (unfold_locales) auto
interpretation weak_arrow_of_homs V⇩C src⇩C trg⇩C D'.comp D'.src D'.trg F
proof
fix μ
assume μ: "C.arr μ"
obtain φ where φ: "«φ : F (src⇩C μ) ⇒⇩D src⇩D (F μ)» ∧ D.iso φ"
using μ F.weakly_preserves_src by auto
have 2: "D'.in_hom φ (F (src⇩C μ)) (D'.src (F μ))"
using μ φ D'.arr_char⇩S⇩b⇩C D'.dom_char⇩S⇩b⇩C D'.cod_char⇩S⇩b⇩C D'.src_def D.vconn_implies_hpar(1-2)
preserves_arr
by (metis (no_types, lifting) C.src.preserves_arr D'.in_hom_char⇩S⇩b⇩C D'.src.preserves_arr
D.arrI)
moreover have "D'.iso φ"
using 2 φ D'.iso_char⇩S⇩b⇩C D'.arr_char⇩S⇩b⇩C by fastforce
ultimately show "D'.isomorphic (F (src⇩C μ)) (D'.src (F μ))"
using D'.isomorphic_def by auto
obtain ψ where ψ: "«ψ : F (trg⇩C μ) ⇒⇩D trg⇩D (F μ)» ∧ D.iso ψ"
using μ F.weakly_preserves_trg by auto
have 2: "D'.in_hom ψ (F (trg⇩C μ)) (D'.trg (F μ))"
using μ ψ D'.arr_char⇩S⇩b⇩C D'.dom_char⇩S⇩b⇩C D'.cod_char⇩S⇩b⇩C D'.trg_def D.vconn_implies_hpar(1-2)
preserves_arr
by (metis (no_types, lifting) C.trg.preserves_arr D'.in_hom_char⇩S⇩b⇩C D'.trg.preserves_arr
D.arrI)
moreover have "D'.iso ψ"
using 2 ψ D'.iso_char⇩S⇩b⇩C D'.arr_char⇩S⇩b⇩C by fastforce
ultimately show "D'.isomorphic (F (trg⇩C μ)) (D'.trg (F μ))"
using D'.isomorphic_def by auto
qed
interpretation H⇩D⇩'oFF: composite_functor C.VV.comp D'.VV.comp D'.comp FF
‹λμν. D'.hcomp (fst μν) (snd μν)›
..
interpretation FoH⇩C: composite_functor C.VV.comp V⇩C D'.comp ‹λμν. fst μν ⋆⇩C snd μν›
F
..
interpretation natural_transformation C.VV.comp D'.comp H⇩D⇩'oFF.map FoH⇩C.map Φ
proof
show "⋀μν. ¬ C.VV.arr μν ⟹ Φ μν = D'.null"
by (simp add: F.Φ.is_extensional)
fix μν
assume μν: "C.VV.arr μν"
have 1: "D'.arr (Φ μν)"
using μν D'.arr_char⇩S⇩b⇩C F.Φ.is_natural_1 F.Φ.components_are_iso
by (metis (no_types, lifting) D.src_vcomp D.trg_vcomp FoH⇩C.preserves_arr
F.Φ.preserves_reflects_arr)
show "D'.dom (Φ μν) = H⇩D⇩'oFF.map (C.VV.dom μν)"
using 1 μν D'.dom_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C C.VV.dom_char⇩S⇩b⇩C F.FF_def FF_def D'.hcomp_def
by simp
show "D'.cod (Φ μν) = FoH⇩C.map (C.VV.cod μν)"
using 1 μν D'.cod_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C F.FF_def FF_def D'.hcomp_def by simp
show "D'.comp (FoH⇩C.map μν) (Φ (C.VV.dom μν)) = Φ μν"
using 1 μν D'.arr_char⇩S⇩b⇩C D'.comp_char C.VV.dom_char⇩S⇩b⇩C F.Φ.is_natural_1
C.VV.arr_dom D.src_vcomp D.trg_vcomp FoH⇩C.preserves_arr F.Φ.preserves_reflects_arr
by (metis (mono_tags, lifting))
show "D'.comp (Φ (C.VV.cod μν)) (H⇩D⇩'oFF.map μν) = Φ μν"
proof -
have "Obj (F.map⇩0 (trg⇩C (fst μν))) ∧ Obj (F.map⇩0 (trg⇩C (snd μν)))"
using μν C.VV.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting) C.src_trg C.trg.preserves_reflects_arr D'.arr_char⇩S⇩b⇩C
F.map⇩0_def preserves_hseq)
moreover have "Obj (F.map⇩0 (src⇩C (snd μν)))"
using μν C.VV.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting) C.src.preserves_reflects_arr C.trg_src D'.arr_char⇩S⇩b⇩C
F.map⇩0_def preserves_hseq)
ultimately show ?thesis
using μν 1 D'.arr_char⇩S⇩b⇩C D'.comp_char D'.hseq_char C.VV.arr_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C
C.VxV.cod_char FF_def F.FF_def D'.hcomp_char preserves_hseq
apply simp
using F.Φ.is_natural_2 by force
qed
qed
interpretation natural_isomorphism C.VV.comp D'.comp H⇩D⇩'oFF.map FoH⇩C.map Φ
apply unfold_locales
using D'.iso_char⇩S⇩b⇩C D'.arr_char⇩S⇩b⇩C by fastforce
sublocale pseudofunctor V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C D'.comp D'.hcomp D'.𝖺 𝗂⇩D D'.src D'.trg
F Φ
proof
fix f g h
assume f: "C.ide f" and g: "C.ide g" and h: "C.ide h"
and fg: "src⇩C f = trg⇩C g" and gh: "src⇩C g = trg⇩C h"
have "D'.comp (F 𝖺⇩C[f, g, h]) (D'.comp (Φ (f ⋆⇩C g, h)) (D'.hcomp (Φ (f, g)) (F h))) =
F 𝖺⇩C[f, g, h] ⋅⇩D Φ (f ⋆⇩C g, h) ⋅⇩D (Φ (f, g) ⋆⇩D F h)"
proof -
have 1: "D'.arr (cmp (f, g) ⋆⇩D map h)"
by (metis (mono_tags, lifting) C.ideD(1) D'.arr_char⇩S⇩b⇩C D'.hcomp_closed
F.Φ.preserves_reflects_arr F.cmp_simps(1-2) F.preserves_hseq
f fg g gh h preserves_reflects_arr)
moreover have 2: "D.seq (cmp (f ⋆⇩C g, h)) (cmp (f, g) ⋆⇩D map h)"
using 1 f g h fg gh D'.arr_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C F.FF_def
by (intro D.seqI) auto
moreover have "D'.arr (cmp (f ⋆⇩C g, h) ⋅⇩D (cmp (f, g) ⋆⇩D map h))"
using 1 2 D'.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting) D'.comp_char D'.seq_char⇩S⇩b⇩C D.seqE F.Φ.preserves_reflects_arr
preserves_reflects_arr)
ultimately show ?thesis
using f g h fg gh D'.dom_char⇩S⇩b⇩C D'.cod_char⇩S⇩b⇩C D'.comp_char D'.hcomp_def C.VV.arr_char⇩S⇩b⇩C
apply simp
by force
qed
also have "... = Φ (f, g ⋆⇩C h) ⋅⇩D (F f ⋆⇩D Φ (g, h)) ⋅⇩D 𝖺⇩D[F f, F g, F h]"
using f g h fg gh F.assoc_coherence [of f g h] by blast
also have "... = D'.comp (Φ (f, g ⋆⇩C h))
(D'.comp (D'.hcomp (F f) (Φ (g, h))) (D'.𝖺 (F f) (F g) (F h)))"
proof -
have "D.seq (map f ⋆⇩D cmp (g, h)) 𝖺⇩D[map f, map g, map h]"
using f g h fg gh C.VV.arr_char⇩S⇩b⇩C C.VV.dom_char⇩S⇩b⇩C C.VV.cod_char⇩S⇩b⇩C F.FF_def
by (intro D.seqI) auto
moreover have "D'.arr 𝖺⇩D[map f, map g, map h]"
using f g h fg gh D'.arr_char⇩S⇩b⇩C preserves_arr by auto
moreover have "D'.arr (map f ⋆⇩D cmp (g, h))"
using f g h fg gh
by (metis (no_types, lifting) D'.arr_char⇩S⇩b⇩C D.seqE D.vseq_implies_hpar(1)
D.vseq_implies_hpar(2) calculation(1-2))
moreover have "D'.arr ((map f ⋆⇩D cmp (g, h)) ⋅⇩D 𝖺⇩D[map f, map g, map h])"
using f g h fg gh
by (metis (no_types, lifting) D'.arr_char⇩S⇩b⇩C D'.comp_closed D.seqE
calculation(1-3))
moreover have "D.seq (cmp (f, g ⋆⇩C h))
((map f ⋆⇩D cmp (g, h)) ⋅⇩D 𝖺⇩D[map f, map g, map h])"
using f g h fg gh F.cmp_simps'(1) F.cmp_simps(4) F.cmp_simps(5) by auto
ultimately show ?thesis
using f g h fg gh C.VV.arr_char⇩S⇩b⇩C D'.VVV.arr_char⇩S⇩b⇩C D'.VV.arr_char⇩S⇩b⇩C D'.comp_char
D'.hcomp_def
by simp
qed
finally show "D'.comp (F 𝖺⇩C[f, g, h])
(D'.comp (Φ (f ⋆⇩C g, h)) (D'.hcomp (Φ (f, g)) (F h))) =
D'.comp (Φ (f, g ⋆⇩C h))
(D'.comp (D'.hcomp (F f) (Φ (g, h))) (D'.𝖺 (F f) (F g) (F h)))"
by blast
qed
lemma is_pseudofunctor:
shows "pseudofunctor V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C D'.comp D'.hcomp D'.𝖺 𝗂⇩D D'.src D'.trg F Φ"
..
lemma map⇩0_simp [simp]:
assumes "C.obj a"
shows "map⇩0 a = F.map⇩0 a"
using assms map⇩0_def D'.src_def by auto
lemma unit_char':
assumes "C.obj a"
shows "F.unit a = unit a"
proof (intro unit_eqI)
show "C.obj a" by fact
show 1: "D'.in_hom (F.unit a) (map⇩0 a) (map a)"
using D'.arr_char⇩S⇩b⇩C D'.in_hom_char⇩S⇩b⇩C assms unit_in_hom(2) by force
show "D'.iso (F.unit a)"
using assms D'.iso_char⇩S⇩b⇩C D'.arr_char⇩S⇩b⇩C F.unit_char(2)
‹D'.in_hom (F.unit a) (map⇩0 a) (map a)›
by auto
show "D'.comp (F.unit a) 𝗂⇩D[map⇩0 a] =
D'.comp (D'.comp (map 𝗂⇩C[a]) (cmp (a, a)))
(D'.hcomp (F.unit a) (F.unit a))"
proof -
have "D'.comp (F.unit a) 𝗂⇩D[map⇩0 a] = F.unit a ⋅⇩D 𝗂⇩D[src⇩D (map a)]"
using assms D'.comp_char D'.arr_char⇩S⇩b⇩C
apply simp
by (metis (no_types, lifting) C.obj_simps(1-2) F.preserves_src preserves_arr)
also have "... = (map 𝗂⇩C[a] ⋅⇩D cmp (a, a)) ⋅⇩D (F.unit a ⋆⇩D F.unit a)"
using assms F.unit_char(3) [of a] by auto
also have "... = D'.comp (D'.comp (map 𝗂⇩C[a]) (cmp (a, a)))
(D'.hcomp (F.unit a) (F.unit a))"
proof -
have "D'.arr (map 𝗂⇩C[a] ⋅⇩D cmp (a, a))"
using assms D'.comp_simp by auto
moreover have "D.seq (map 𝗂⇩C[a] ⋅⇩D cmp (a, a)) (F.unit a ⋆⇩D F.unit a)"
using assms C.VV.arr_char⇩S⇩b⇩C F.cmp_simps(4-5)
by (intro D.seqI) auto
ultimately show ?thesis
by (metis (no_types, lifting) "1" D'.comp_eqI' D'.hcomp_eqI' D'.hseqI'
D'.iso_is_arr D'.seq_char⇩S⇩b⇩C D'.vconn_implies_hpar(1-2)
𝗂_simps(1) ‹D'.iso (F.unit a)› assms map⇩0_simps(2-3))
qed
finally show ?thesis by blast
qed
qed
end
subsection "Equivalence Pseudofunctors"
text ‹
In this section, we define ``equivalence pseudofunctors'', which are pseudofunctors
that are locally fully faithful, locally essentially surjective, and biessentially
surjective on objects. In a later section, we will show that a pseudofunctor is
an equivalence pseudofunctor if and only if it can be extended to an equivalence
of bicategories.
The definition below requires that an equivalence pseudofunctor be (globally) faithful
with respect to vertical composition. Traditional formulations do not consider a
pseudofunctor as a single global functor, so we have to consider whether this condition
is too strong. In fact, a pseudofunctor (as defined here) is locally faithful if and
only if it is globally faithful.
›
context pseudofunctor
begin
definition locally_faithful
where "locally_faithful ≡
∀f g μ μ'. «μ : f ⇒⇩C g» ∧ «μ' : f ⇒⇩C g» ∧ F μ = F μ' ⟶ μ = μ'"
lemma locally_faithful_iff_faithful:
shows "locally_faithful ⟷ faithful_functor V⇩C V⇩D F"
proof
show "faithful_functor V⇩C V⇩D F ⟹ locally_faithful"
by (metis category.in_homE faithful_functor.is_faithful functor_axioms
functor_def locally_faithful_def)
show "locally_faithful ⟹ faithful_functor V⇩C V⇩D F"
proof -
assume 1: "locally_faithful"
show "faithful_functor V⇩C V⇩D F"
proof
fix μ μ'
assume par: "C.par μ μ'" and eq: "F μ = F μ'"
obtain f g where fg: "«μ : f ⇒⇩C g» ∧ «μ' : f ⇒⇩C g»"
using par by auto
show "μ = μ'"
using 1 fg locally_faithful_def eq by simp
qed
qed
qed
end
text ‹
In contrast, it is not true that a pseudofunctor that is locally full is also
globally full, because we can have ‹«ν : F h ⇒⇩D F k»› even if ‹h› and ‹k›
are not in the same hom-category. So it would be a mistake to require that an
equivalence functor be globally full.
›
locale equivalence_pseudofunctor =
pseudofunctor +
faithful_functor V⇩C V⇩D F +
assumes biessentially_surjective_on_objects:
"D.obj a' ⟹ ∃a. C.obj a ∧ D.equivalent_objects (map⇩0 a) a'"
and locally_essentially_surjective:
"⟦ C.obj a; C.obj b; «g : map⇩0 a →⇩D map⇩0 b»; D.ide g ⟧ ⟹
∃f. «f : a →⇩C b» ∧ C.ide f ∧ D.isomorphic (F f) g"
and locally_full:
"⟦ C.ide f; C.ide f'; src⇩C f = src⇩C f'; trg⇩C f = trg⇩C f'; «ν : F f ⇒⇩D F f'» ⟧ ⟹
∃μ. «μ : f ⇒⇩C f'» ∧ F μ = ν"
begin
lemma reflects_ide:
assumes "C.endo μ" and "D.ide (F μ)"
shows "C.ide μ"
using assms is_faithful [of "C.dom μ" μ] C.ide_char'
by (metis C.arr_dom C.cod_dom C.dom_dom C.seqE D.ide_char preserves_dom)
lemma reflects_iso:
assumes "C.arr μ" and "D.iso (F μ)"
shows "C.iso μ"
proof -
obtain μ' where μ': "«μ' : C.cod μ ⇒⇩C C.dom μ» ∧ F μ' = D.inv (F μ)"
using assms locally_full [of "C.cod μ" "C.dom μ" "D.inv (F μ)"]
D.inv_in_hom C.in_homE preserves_hom C.in_homI
by auto
have "C.inverse_arrows μ μ'"
using assms μ' reflects_ide
apply (intro C.inverse_arrowsI)
apply (metis C.cod_comp C.dom_comp C.ide_dom C.in_homE C.seqI D.comp_inv_arr'
faithful_functor_axioms faithful_functor_def functor.preserves_ide
as_nat_trans.preserves_comp_2 preserves_dom)
by (metis C.cod_comp C.dom_comp C.ide_cod C.in_homE C.seqI D.comp_arr_inv'
faithful_functor_axioms faithful_functor_def functor.preserves_ide
preserves_cod as_nat_trans.preserves_comp_2)
thus ?thesis by auto
qed
lemma reflects_isomorphic:
assumes "C.ide f" and "C.ide f'" and "src⇩C f = src⇩C f'" and "trg⇩C f = trg⇩C f'"
and "D.isomorphic (F f) (F f')"
shows "C.isomorphic f f'"
using assms C.isomorphic_def D.isomorphic_def locally_full reflects_iso C.arrI
by metis
lemma reflects_equivalence:
assumes "C.ide f" and "C.ide g"
and "«η : src⇩C f ⇒⇩C g ⋆⇩C f»" and "«ε : f ⋆⇩C g ⇒⇩C src⇩C g»"
and "equivalence_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D (F f) (F g)
(D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f))
(D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g))"
shows "equivalence_in_bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε"
proof -
interpret E': equivalence_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ‹F f› ‹F g›
‹D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f)›
‹D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g)›
using assms by auto
show ?thesis
proof
show "C.ide f"
using assms(1) by simp
show "C.ide g"
using assms(2) by simp
show "«η : src⇩C f ⇒⇩C g ⋆⇩C f»"
using assms(3) by simp
show "«ε : f ⋆⇩C g ⇒⇩C src⇩C g»"
using assms(4) by simp
have 0: "src⇩C f = trg⇩C g ∧ src⇩C g = trg⇩C f"
using ‹«η : src⇩C f ⇒⇩C g ⋆⇩C f»›
by (metis C.hseqE C.ideD(1) C.ide_cod C.ide_dom C.in_homE assms(4))
show "C.iso η"
proof -
have "D.iso (F η)"
proof -
have 1: "«D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f) : map⇩0 (src⇩C f) ⇒⇩D F g ⋆⇩D F f»"
using ‹C.ide f› ‹C.ide g› ‹«η : src⇩C f ⇒⇩C g ⋆⇩C f»›
unit_char cmp_in_hom cmp_components_are_iso
by (metis (mono_tags, lifting) C.ideD(1) E'.unit_in_vhom preserves_src)
have 2: "D.iso (Φ (g, f)) ∧ «Φ (g, f) : F g ⋆⇩D F f ⇒⇩D F (g ⋆⇩C f)»"
using 0 ‹C.ide f› ‹C.ide g› cmp_in_hom by simp
have 3: "D.iso (D.inv (unit (src⇩C f))) ∧
«D.inv (unit (src⇩C f)) : F (src⇩C f) ⇒⇩D map⇩0 (src⇩C f)»"
using ‹C.ide f› unit_char by simp
have "D.iso (Φ (g, f) ⋅⇩D (D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f)) ⋅⇩D
D.inv (unit (src⇩C f)))"
using 1 2 3 E'.unit_is_iso D.isos_compose by blast
moreover have "Φ (g, f) ⋅⇩D (D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f)) ⋅⇩D
D.inv (unit (src⇩C f)) =
F η"
proof -
have "Φ (g, f) ⋅⇩D (D.inv (Φ (g, f)) ⋅⇩D F η ⋅⇩D unit (src⇩C f)) ⋅⇩D
D.inv (unit (src⇩C f))
= (Φ (g, f) ⋅⇩D (D.inv (Φ (g, f))) ⋅⇩D F η ⋅⇩D (unit (src⇩C f)) ⋅⇩D
D.inv (unit (src⇩C f)))"
using D.comp_assoc by simp
also have "... = F (g ⋆⇩C f) ⋅⇩D F η ⋅⇩D F (src⇩C f)"
using 2 3 D.comp_arr_inv D.comp_inv_arr D.inv_is_inverse
by (metis C.ideD(1) C.obj_src D.comp_assoc D.dom_inv D.in_homE unit_char(2)
assms(1))
also have "... = F η"
using ‹«η : src⇩C f ⇒⇩C g ⋆⇩C f»› D.comp_arr_dom D.comp_cod_arr by auto
finally show ?thesis by simp
qed
ultimately show ?thesis by simp
qed
thus ?thesis
using assms reflects_iso by auto
qed
show "C.iso ε"
proof -
have "D.iso (F ε)"
proof -
have 1: "«D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g) : F f ⋆⇩D F g ⇒⇩D map⇩0 (src⇩C g)»"
using ‹C.ide f› ‹C.ide g› ‹«ε : f ⋆⇩C g ⇒⇩C src⇩C g»›
unit_char cmp_in_hom cmp_components_are_iso
by (metis (mono_tags, lifting) C.ideD(1) E'.counit_in_vhom preserves_src)
have 2: "D.iso (D.inv (Φ (f, g))) ∧
«D.inv (Φ (f, g)) : F (f ⋆⇩C g) ⇒⇩D F f ⋆⇩D F g»"
using 0 ‹C.ide f› ‹C.ide g› ‹«ε : f ⋆⇩C g ⇒⇩C src⇩C g»› cmp_in_hom(2) D.inv_in_hom
by simp
have 3: "D.iso (unit (trg⇩C f)) ∧ «unit (trg⇩C f) : map⇩0 (trg⇩C f) ⇒⇩D F (trg⇩C f)»"
using ‹C.ide f› unit_char by simp
have "D.iso (unit (trg⇩C f) ⋅⇩D (D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g)) ⋅⇩D
D.inv (Φ (f, g)))"
using 0 1 2 3 E'.counit_is_iso D.isos_compose
by (metis D.arrI D.cod_comp D.cod_inv D.seqI D.seqI')
moreover have "unit (trg⇩C f) ⋅⇩D (D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g)) ⋅⇩D
D.inv (Φ (f, g)) =
F ε"
proof -
have "unit (trg⇩C f) ⋅⇩D (D.inv (unit (trg⇩C f)) ⋅⇩D F ε ⋅⇩D Φ (f, g)) ⋅⇩D
D.inv (Φ (f, g)) =
(unit (trg⇩C f) ⋅⇩D D.inv (unit (trg⇩C f))) ⋅⇩D F ε ⋅⇩D (Φ (f, g) ⋅⇩D D.inv (Φ (f, g)))"
using D.comp_assoc by simp
also have "... = F (trg⇩C f) ⋅⇩D F ε ⋅⇩D F (f ⋆⇩C g)"
using 0 3 D.comp_arr_inv' D.comp_inv_arr'
by (simp add: C.VV.arr_char⇩S⇩b⇩C C.VV.ide_char⇩S⇩b⇩C assms(1-2))
also have "... = F ε"
using 0 ‹«ε : f ⋆⇩C g ⇒⇩C src⇩C g»› D.comp_arr_dom D.comp_cod_arr by auto
finally show ?thesis by simp
qed
ultimately show ?thesis by simp
qed
thus ?thesis
using assms reflects_iso by auto
qed
qed
qed
lemma reflects_equivalence_map:
assumes "C.ide f" and "D.equivalence_map (F f)"
shows "C.equivalence_map f"
proof -
obtain g' φ ψ where E': "equivalence_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D (F f) g' φ ψ"
using assms D.equivalence_map_def by auto
interpret E': equivalence_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ‹F f› g' φ ψ
using E' by auto
obtain g where g: "«g : trg⇩C f →⇩C src⇩C f» ∧ C.ide g ∧ D.isomorphic (F g) g'"
using assms E'.antipar locally_essentially_surjective [of "trg⇩C f" "src⇩C f" g']
by auto
obtain μ where μ: "«μ : g' ⇒⇩D F g» ∧ D.iso μ"
using g D.isomorphic_def D.isomorphic_symmetric by blast
interpret E'': equivalence_in_bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ‹F f› ‹F g›
‹(F g ⋆⇩D F f) ⋅⇩D (μ ⋆⇩D F f) ⋅⇩D φ›
‹ψ ⋅⇩D (D.inv (F f) ⋆⇩D g') ⋅⇩D (F f ⋆⇩D D.inv μ)›
using assms μ E'.equivalence_in_bicategory_axioms D.ide_is_iso
D.equivalence_respects_iso [of "F f" g' φ ψ "F f" "F f" μ "F g"]
by auto
let ?η' = "Φ (g, f) ⋅⇩D (F g ⋆⇩D F f) ⋅⇩D (μ ⋆⇩D F f) ⋅⇩D φ ⋅⇩D D.inv (unit (src⇩C f))"
have η': "«?η' : F (src⇩C f) ⇒⇩D F (g ⋆⇩C f)»"
using assms μ g unit_char E'.unit_in_hom(2) E'.antipar E''.antipar cmp_in_hom
apply (intro D.comp_in_homI)
apply auto
using E'.antipar(2) by blast
have iso_η': "D.iso ?η'"
using assms g μ η' E'.antipar unit_char
by (metis C.in_hhomE D.arrI D.inv_comp_left(2) D.inv_comp_right(2) D.iso_hcomp
D.iso_inv_iso D.isos_compose D.seqE E''.antipar(2) E''.unit_is_iso
E'.unit_is_iso as_nat_iso.components_are_iso cmp_components_are_iso)
let ?ε' = "unit (src⇩C g) ⋅⇩D ψ ⋅⇩D (D.inv (F f) ⋆⇩D g') ⋅⇩D (F f ⋆⇩D D.inv μ) ⋅⇩D
D.inv (Φ (f, g))"
have ε': "«?ε' : F (f ⋆⇩C g) ⇒⇩D F (trg⇩C f)»"
proof (intro D.comp_in_homI)
show "«D.inv (Φ (f, g)) : F (f ⋆⇩C g) ⇒⇩D F f ⋆⇩D F g»"
using assms g cmp_in_hom C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C by auto
show "«F f ⋆⇩D D.inv μ : F f ⋆⇩D F g ⇒⇩D F f ⋆⇩D g'»"
using assms g μ E''.antipar D.ide_in_hom(2) by auto
show "«D.inv (F f) ⋆⇩D g' : F f ⋆⇩D g' ⇒⇩D F f ⋆⇩D g'»"
using assms E'.antipar D.ide_is_iso by auto
show "«ψ : F f ⋆⇩D g' ⇒⇩D trg⇩D (F f)»"
using E'.counit_in_hom by simp
show "«unit (src⇩C g) : trg⇩D (F f) ⇒⇩D F (trg⇩C f)»"
using assms g unit_char by auto
qed
have iso_ε': "D.iso ?ε'"
proof -
have "D.iso (Φ (f, g))"
using assms g C.VV.ide_char⇩S⇩b⇩C C.VV.arr_char⇩S⇩b⇩C by auto
thus ?thesis
by (metis C.in_hhomE D.arrI D.hseq_char' D.ide_is_iso D.inv_comp_left(2)
D.inv_comp_right(2) D.iso_hcomp D.iso_inv_iso D.isos_compose D.seqE
D.seq_if_composable E''.counit_is_iso E'.counit_is_iso E'.ide_left
ε' μ g unit_char(2))
qed
obtain η where η: "«η : src⇩C f ⇒⇩C g ⋆⇩C f» ∧ F η = ?η'"
using assms g E'.antipar η' locally_full [of "src⇩C f" "g ⋆⇩C f" ?η']
by (metis C.ide_hcomp C.ideD(1) C.in_hhomE C.src.preserves_ide C.hcomp_simps(1-2)
C.src_trg C.trg_trg)
have iso_η: "C.iso η"
using η η' iso_η' reflects_iso by auto
have 1: "∃ε. «ε : f ⋆⇩C g ⇒⇩C src⇩C g» ∧ F ε = ?ε'"
using assms g ε' locally_full [of "f ⋆⇩C g" "src⇩C g" ?ε'] by force
obtain ε where ε: "«ε : f ⋆⇩C g ⇒⇩C src⇩C g» ∧ F ε = ?ε'"
using 1 by blast
have iso_ε: "C.iso ε"
using ε ε' iso_ε' reflects_iso by auto
have "equivalence_in_bicategory (⋅⇩C) (⋆⇩C) 𝖺⇩C 𝗂⇩C src⇩C trg⇩C f g η ε"
using assms g η ε iso_η iso_ε by (unfold_locales, auto)
thus ?thesis
using C.equivalence_map_def by auto
qed
lemma reflects_equivalent_objects:
assumes "C.obj a" and "C.obj b" and "D.equivalent_objects (map⇩0 a) (map⇩0 b)"
shows "C.equivalent_objects a b"
proof -
obtain f' where f': "«f' : map⇩0 a →⇩D map⇩0 b» ∧ D.equivalence_map f'"
using assms D.equivalent_objects_def D.equivalence_map_def by auto
obtain f where f: "«f : a →⇩C b» ∧ C.ide f ∧ D.isomorphic (F f) f'"
using assms f' locally_essentially_surjective [of a b f'] D.equivalence_map_is_ide
by auto
have "D.equivalence_map (F f)"
using f f' D.equivalence_map_preserved_by_iso [of f' "F f"] D.isomorphic_symmetric
by simp
hence "C.equivalence_map f"
using f f' reflects_equivalence_map [of f] by simp
thus ?thesis
using f C.equivalent_objects_def by auto
qed
end
text‹
For each pair of objects ‹a›, ‹b› of ‹C›, an equivalence pseudofunctor restricts
to an equivalence of categories between ‹C.hhom a b› and ‹D.hhom (map⇩0 a) (map⇩0 b)›.
›
locale equivalence_pseudofunctor_at_hom =
equivalence_pseudofunctor +
fixes a :: 'a and a' :: 'a
assumes obj_a: "C.obj a"
and obj_a': "C.obj a'"
begin
sublocale hhom⇩C: subcategory V⇩C ‹λμ. «μ : a →⇩C a'»›
using C.hhom_is_subcategory by simp
sublocale hhom⇩D: subcategory V⇩D ‹λμ. «μ : map⇩0 a →⇩D map⇩0 a'»›
using D.hhom_is_subcategory by simp
definition F⇩1
where "F⇩1 = (λμ. if hhom⇩C.arr μ then F μ else D.null)"
interpretation F⇩1: "functor" hhom⇩C.comp hhom⇩D.comp F⇩1
unfolding F⇩1_def
using hhom⇩C.arr_char⇩S⇩b⇩C hhom⇩D.arr_char⇩S⇩b⇩C hhom⇩C.dom_char⇩S⇩b⇩C hhom⇩D.dom_char⇩S⇩b⇩C
hhom⇩C.cod_char⇩S⇩b⇩C hhom⇩D.cod_char⇩S⇩b⇩C hhom⇩C.seq_char⇩S⇩b⇩C hhom⇩C.comp_char hhom⇩D.comp_char
by unfold_locales auto
interpretation F⇩1: fully_faithful_and_essentially_surjective_functor
hhom⇩C.comp hhom⇩D.comp F⇩1
proof
show "⋀μ μ'. ⟦hhom⇩C.par μ μ'; F⇩1 μ = F⇩1 μ'⟧ ⟹ μ = μ'"
unfolding F⇩1_def
using is_faithful hhom⇩C.dom_char⇩S⇩b⇩C hhom⇩D.dom_char⇩S⇩b⇩C hhom⇩C.cod_char⇩S⇩b⇩C hhom⇩D.cod_char⇩S⇩b⇩C
by (metis C.in_hhom_def hhom⇩C.arrE)
show "⋀f f' ν. ⟦hhom⇩C.ide f; hhom⇩C.ide f'; hhom⇩D.in_hom ν (F⇩1 f') (F⇩1 f)⟧
⟹ ∃μ. hhom⇩C.in_hom μ f' f ∧ F⇩1 μ = ν"
proof (unfold F⇩1_def)
fix f f' ν
assume f: "hhom⇩C.ide f" and f': "hhom⇩C.ide f'"
assume "hhom⇩D.in_hom ν (if hhom⇩C.arr f' then F f' else D.null)
(if hhom⇩C.arr f then F f else D.null)"
hence ν: "hhom⇩D.in_hom ν (F f') (F f)"
using f f' by simp
have "∃μ. hhom⇩C.in_hom μ f' f ∧ F μ = ν"
proof -
have 1: "src⇩C f' = src⇩C f ∧ trg⇩C f' = trg⇩C f"
using f f' hhom⇩C.ide_char by (metis C.in_hhomE hhom⇩C.arrE)
hence ex: "∃μ. C.in_hom μ f' f ∧ F μ = ν"
by (meson ν f f' hhom⇩D.in_hom_char⇩S⇩b⇩C horizontal_homs.hhom_is_subcategory
locally_full subcategory.ide_char⇩S⇩b⇩C weak_arrow_of_homs_axioms
weak_arrow_of_homs_def)
obtain μ where μ: "C.in_hom μ f' f ∧ F μ = ν"
using ex by blast
have "hhom⇩C.in_hom μ f' f"
by (metis C.arrI C.in_hhom_def C.vconn_implies_hpar(1-2) μ f f'
hhom⇩C.arr_char⇩S⇩b⇩C hhom⇩C.ide_char hhom⇩C.in_hom_char⇩S⇩b⇩C)
thus ?thesis
using μ by auto
qed
thus "∃μ. hhom⇩C.in_hom μ f' f ∧ (if hhom⇩C.arr μ then F μ else D.null) = ν"
by auto
qed
show "⋀g. hhom⇩D.ide g ⟹ ∃f. hhom⇩C.ide f ∧ hhom⇩D.isomorphic (F⇩1 f) g"
proof (unfold F⇩1_def)
fix g
assume g: "hhom⇩D.ide g"
show "∃f. hhom⇩C.ide f ∧ hhom⇩D.isomorphic (if hhom⇩C.arr f then F f else D.null) g"
proof -
have "C.obj a ∧ C.obj a'"
using obj_a obj_a' by simp
moreover have 1: "D.ide g ∧ «g : map⇩0 a →⇩D map⇩0 a'»"
using g obj_a obj_a' hhom⇩D.ide_char⇩S⇩b⇩C by auto
ultimately have 2: "∃f. C.in_hhom f a a' ∧ C.ide f ∧ D.isomorphic (F f) g"
using locally_essentially_surjective [of a a' g] by simp
obtain f φ where f: "C.in_hhom f a a' ∧ C.ide f ∧ D.in_hom φ (F f) g ∧ D.iso φ"
using 2 by auto
have "hhom⇩C.ide f"
using f hhom⇩C.ide_char⇩S⇩b⇩C hhom⇩C.arr_char⇩S⇩b⇩C by simp
moreover have "hhom⇩D.isomorphic (F f) g"
proof -
have "hhom⇩D.arr φ ∧ hhom⇩D.arr (D.inv φ)"
by (metis 1 D.arrI D.in_hhom_def D.vconn_implies_hpar(1-4) D.inv_in_homI
f hhom⇩D.arrI⇩S⇩b⇩C)
hence "hhom⇩D.in_hom φ (F f) g ∧ hhom⇩D.iso φ"
by (metis D.in_homE f hhom⇩D.cod_simp hhom⇩D.dom_simp hhom⇩D.in_homI hhom⇩D.iso_char⇩S⇩b⇩C)
thus ?thesis
unfolding hhom⇩D.isomorphic_def by blast
qed
ultimately show "∃f. hhom⇩C.ide f ∧
hhom⇩D.isomorphic (if hhom⇩C.arr f then F f else D.null) g"
by force
qed
qed
qed
lemma equivalence_functor_F⇩1:
shows "fully_faithful_and_essentially_surjective_functor hhom⇩C.comp hhom⇩D.comp F⇩1"
and "equivalence_functor hhom⇩C.comp hhom⇩D.comp F⇩1"
..
definition G⇩1
where "G⇩1 = (SOME G. ∃ηε.
adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G F⇩1 (fst ηε) (snd ηε))"
lemma G⇩1_props:
assumes "C.obj a" and "C.obj a'"
shows "∃η ε. adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G⇩1 F⇩1 η ε"
proof -
have "∃G. ∃ηε. adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G F⇩1 (fst ηε) (snd ηε)"
using F⇩1.extends_to_adjoint_equivalence by simp
hence "∃ηε. adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G⇩1 F⇩1 (fst ηε) (snd ηε)"
unfolding G⇩1_def
using someI_ex
[of "λG. ∃ηε. adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G F⇩1 (fst ηε) (snd ηε)"]
by blast
thus ?thesis by simp
qed
definition η
where "η = (SOME η. ∃ε. adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G⇩1 F⇩1 η ε)"
definition ε
where "ε = (SOME ε. adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G⇩1 F⇩1 η ε)"
lemma ηε_props:
shows "adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G⇩1 F⇩1 η ε"
using obj_a obj_a' η_def ε_def G⇩1_props
someI_ex [of "λη. ∃ε. adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G⇩1 F⇩1 η ε"]
someI_ex [of "λε. adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G⇩1 F⇩1 η ε"]
by simp
sublocale ηε: adjoint_equivalence hhom⇩C.comp hhom⇩D.comp G⇩1 F⇩1 η ε
using ηε_props by simp
sublocale ηε: meta_adjunction hhom⇩C.comp hhom⇩D.comp G⇩1 F⇩1 ηε.φ ηε.ψ
using ηε.induces_meta_adjunction by simp
end
context identity_pseudofunctor
begin
sublocale equivalence_pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B
map cmp
using B.isomorphic_reflexive B.arrI
apply unfold_locales
by (auto simp add: B.equivalent_objects_reflexive map⇩0_def B.obj_simps)
lemma is_equivalence_pseudofunctor:
shows "equivalence_pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B
map cmp"
..
end
locale composite_equivalence_pseudofunctor =
composite_pseudofunctor +
F: equivalence_pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C F Φ⇩F +
G: equivalence_pseudofunctor V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D G Φ⇩G
begin
interpretation faithful_functor V⇩B V⇩D ‹G o F›
using F.faithful_functor_axioms G.faithful_functor_axioms faithful_functors_compose
by blast
interpretation equivalence_pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D
‹G o F› cmp
proof
show "⋀c. D.obj c ⟹ ∃a. B.obj a ∧ D.equivalent_objects (map⇩0 a) c"
proof -
fix c
assume c: "D.obj c"
obtain b where b: "C.obj b ∧ D.equivalent_objects (G.map⇩0 b) c"
using c G.biessentially_surjective_on_objects by auto
obtain a where a: "B.obj a ∧ C.equivalent_objects (F.map⇩0 a) b"
using b F.biessentially_surjective_on_objects by auto
have "D.equivalent_objects (map⇩0 a) c"
using a b map⇩0_def G.preserves_equivalent_objects D.equivalent_objects_transitive
by fastforce
thus "∃a. B.obj a ∧ D.equivalent_objects (map⇩0 a) c"
using a by auto
qed
show "⋀a a' h. ⟦B.obj a; B.obj a'; «h : map⇩0 a →⇩D map⇩0 a'»; D.ide h⟧
⟹ ∃f. B.in_hhom f a a' ∧ B.ide f ∧ D.isomorphic ((G ∘ F) f) h"
proof -
fix a a' h
assume a: "B.obj a" and a': "B.obj a'"
and h_in_hom: "«h : map⇩0 a →⇩D map⇩0 a'»" and ide_h: "D.ide h"
obtain g
where g: "C.in_hhom g (F.map⇩0 a) (F.map⇩0 a') ∧ C.ide g ∧ D.isomorphic (G g) h"
using a a' h_in_hom ide_h map⇩0_def B.obj_simps
G.locally_essentially_surjective [of "F.map⇩0 a" "F.map⇩0 a'" h]
by auto
obtain f where f: "B.in_hhom f a a' ∧ B.ide f ∧ C.isomorphic (F f) g"
using a a' g F.locally_essentially_surjective by blast
have "D.isomorphic ((G o F) f) h"
by (metis D.isomorphic_transitive G.preserves_isomorphic comp_apply f g)
thus "∃f. B.in_hhom f a a' ∧ B.ide f ∧ D.isomorphic ((G ∘ F) f) h"
using f by auto
qed
show "⋀f f' ν. ⟦B.ide f; B.ide f'; src⇩B f = src⇩B f'; trg⇩B f = trg⇩B f';
«ν : (G ∘ F) f ⇒⇩D (G ∘ F) f'»⟧
⟹ ∃τ. «τ : f →⇩B f'» ∧ (G ∘ F) τ = ν"
proof -
fix f f' ν
assume f: "B.ide f" and f': "B.ide f'"
and src: "src⇩B f = src⇩B f'" and trg: "trg⇩B f = trg⇩B f'"
and ν: "«ν : (G ∘ F) f ⇒⇩D (G ∘ F) f'»"
have ν: "«ν : G (F f) ⇒⇩D G (F f')»"
using ν by simp
have 1: "src⇩C (F f) = src⇩C (F f') ∧ trg⇩C (F f) = trg⇩C (F f')"
using f f' src trg by simp
have 2: "∃μ. «μ : F f ⇒⇩C F f'» ∧ G μ = ν"
using f f' 1 ν G.locally_full F.preserves_ide by simp
obtain μ where μ: "«μ : F f ⇒⇩C F f'» ∧ G μ = ν"
using 2 by auto
obtain τ where τ: "«τ : f →⇩B f'» ∧ F τ = μ"
using f f' src trg 2 μ F.locally_full by blast
show "∃τ. «τ : f →⇩B f'» ∧ (G ∘ F) τ = ν"
using μ τ by auto
qed
qed
sublocale equivalence_pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D
‹G o F› cmp ..
lemma is_equivalence_pseudofunctor:
shows "equivalence_pseudofunctor V⇩B H⇩B 𝖺⇩B 𝗂⇩B src⇩B trg⇩B V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D
(G o F) cmp"
..
end
end