module Cat.Functor.Equivalence.Path where
Paths between categoriesπ
We know that, in a univalent category, paths between objects are the same thing as isomorphisms. A natural question to follow up is: what are the paths between univalent categories? We prove that the space of functors whose mappings on objects and on morphisms are both equivalences (βisomorphisms of precategoriesβ) is an identity system on the space of precategories.
The first thing we need to establish is that an isomorphism of
precategories induces a path between its domain and codomain categories.
This is essentially an application of univalence, done in direct cubical
style. In particular, we use Glue directly rather than ua
to construct the path between Hom families.
Precategory-path : β {o β} {C D : Precategory o β} (F : Functor C D) β is-precat-iso F β C β‘ D Precategory-path {o = o} {β} {C} {D} F p = path where module C = Precategory C module D = Precategory D open is-precat-iso p renaming (has-is-iso to obβ ; has-is-ff to homβ)
By assumption, βs action on objects is an equivalence, so by univalence it induces an equivalence . The path between Hom-sets is slightly more complicated. It is, essentially, the dashed line in the diagram
obl : β i β Type o obl i = ua (Fβ F , obβ) i sys : β i (x y : obl i) β Partial (i β¨ ~ i) _ sys i x y (i = i0) = C.Hom x y , Fβ F , homβ sys i x y (i = i1) = D.Hom x y , (Ξ» x β x) , id-equiv hom : PathP (Ξ» i β obl i β obl i β Type β) C.Hom D.Hom hom i x y = Glue (D.Hom (unglue (i β¨ ~ i) x) (unglue (i β¨ ~ i) y)) (sys i x y)
Note that is a term in which evaluates to when or , so that the system described above can indeed be built. The introduction rule for hom is hom-glue: If we have a partial element together with an element of base type satisfying definitionally , we may glue along to get an element of .
hom-glue : β i (x y : obl i) β (f : PartialP {a = β} (~ i) Ξ» { (i = i0) β C.Hom x y }) β (g : D.Hom (unglue (i β¨ ~ i) x) (unglue (i β¨ ~ i) y) [ (~ i) β¦ (Ξ» { (i = i0) β Fβ F (f 1=1) }) ]) β hom i x y hom-glue i x y f g = glue-inc _ {Tf = sys i x y} (Ξ» { (i = i0) β f 1=1 ; (i = i1) β outS g }) (inS (outS g))
To obtain these definitional extensions of a morphism in C, we use homogeneous composition, together with the functor laws. For example, below, we obtain a line which definitionally extends on the left and by gluing against the proof that preserves identity.
idh : β i x β hom i x x idh i x = hom-glue i x x (Ξ» { (i = i0) β C.id }) (inS (hcomp (β i) Ξ» where j (i = i0) β F .F-id (~ j) j (i = i1) β D.id j (j = i0) β D.id)) circ : β i x y z β hom i y z β hom i x y β hom i x z circ i x y z f g = hom-glue i x z (Ξ» { (i = i0) β f C.β g }) (inS (hcomp (β i) Ξ» where j (i = i0) β F .F-β f g (~ j) j (i = i1) β f D.β g j (j = i0) β unglue (i β¨ ~ i) f D.β unglue (i β¨ ~ i) g))
The last trick is extending a proposition along the line , in a way that agrees with the original categories. We do this by piecing together a square whose sides are the witness that is a proposition, and where the base is given by spreading (coe0βi) the proposition from throughout the line. We only include the case for Hom-set since it is instructive and the other laws are not any more enlightening.
hom-is-set : β i a b β is-set (hom i a b) hom-is-set i a b = hcomp (β i) Ξ» where k (k = i0) β extended k (i = i0) β is-hlevel-is-prop 2 extended (C.Hom-set a b) k k (i = i1) β is-hlevel-is-prop 2 extended (D.Hom-set a b) k where extended = coe0βi (Ξ» i β (a b : obl i) β is-set (hom i a b)) i C.Hom-set a b open Precategory path : C β‘ D path i .Ob = obl i path i .Hom = hom i path i .Hom-set a b = hom-is-set i a b path i .id {x} = idh i x path i ._β_ {x} {y} {z} f g = circ i x y z f g
path i .idr {x} {y} f = hcomp (β i) Ξ» where k (k = i0) β extended k (i = i0) β C.Hom-set x y (f C.β C.id) f extended (C.idr f) k k (i = i1) β D.Hom-set x y (f D.β D.id) f extended (D.idr f) k where extended = coe0βi (Ξ» i β (x y : obl i) (f : hom i x y) β circ i x x y f (idh i x) β‘ f) i (Ξ» x y f β C.idr f) x y f path i .idl {x} {y} f = hcomp (β i) Ξ» where k (k = i0) β extended k (i = i0) β C.Hom-set x y (C.id C.β f) f extended (C.idl f) k k (i = i1) β D.Hom-set x y (D.id D.β f) f extended (D.idl f) k where extended = coe0βi (Ξ» i β (x y : obl i) (f : hom i x y) β circ i x y y (idh i y) f β‘ f) i (Ξ» x y f β C.idl f) x y f path i .assoc {w} {x} {y} {z} f g h = hcomp (β i) Ξ» where k (k = i0) β extended k (i = i0) β C.Hom-set w z (f C.β g C.β h) ((f C.β g) C.β h) extended (C.assoc f g h) k k (i = i1) β D.Hom-set w z (f D.β g D.β h) ((f D.β g) D.β h) extended (D.assoc f g h) k where extended = coe0βi (Ξ» i β (w x y z : obl i) (f : hom i y z) (g : hom i x y) (h : hom i w x) β circ i w y z f (circ i w x y g h) β‘ circ i w x z (circ i x y z f g) h) i (Ξ» _ _ _ _ f g h β C.assoc f g h) w x y z f g h
To conclude that isomorphisms of precategories are an identity system, we must now prove that the operation Precategory-path above trivialises the isomorphism we started with. This is mostly straightforward, but the proof that the action on morphisms is preserved requires a boring calculation:
Precategory-identity-system : β {o β} β is-identity-system {A = Precategory o β} (Ξ» C D β Ξ£ (Functor C D) is-precat-iso) (Ξ» a β Id , iso id-equiv id-equiv) Precategory-identity-system .to-path (F , i) = Precategory-path F i Precategory-identity-system .to-path-over {C} {D} (F , i) = Ξ£-prop-pathp (Ξ» _ _ β hlevel 1) $ Functor-pathp (Ξ» p β pathβua-pathp _ (Ξ» j β F.β (p j))) (Ξ» {x} {y} β homs x y) where module C = Cat.Reasoning C module D = Cat.Reasoning D module F = Functor F homs : β x y (r : β j β C.Hom (x j) (y j)) β PathP _ _ _ homs x y f = to-pathp $ transport (Ξ» iβ β D.Hom (F.β (x iβ)) (F.β (y iβ))) (F.β (f i0)) β‘β¨ Hom-transport D (Ξ» i β F.β (x i)) (Ξ» i β F.β (y i)) (F.β (f i0)) β©β‘ _ D.β F.β (f i0) D.β _ β‘β¨ ap D.to (ap-Fβ-to-iso F (Ξ» i β y i)) D.β©ββ¨ (refl D.β©ββ¨ ap D.from (ap-Fβ-to-iso F (Ξ» i β x i))) β©β‘ F.β _ D.β F.β (f i0) D.β F.β _ β‘Λβ¨ D.reflβ©ββ¨ F.F-β _ _ β©β‘Λ (F.β _ D.β F.β (f i0 C.β _)) β‘Λβ¨ F.F-β _ _ β©β‘Λ F.β (_ C.β f i0 C.β _) β‘Λβ¨ ap F.β (Hom-transport C (Ξ» i β x i) (Ξ» i β y i) (f i0)) β©β‘Λ F.β (coe0β1 (Ξ» z β C.Hom (x z) (y z)) (f i0)) β‘β¨ ap F.β (from-pathp (Ξ» i β f i)) β©β‘ F.β (f i1) β
Note that we did not need to concern ourselves with the actual witness that the functor is an isomorphism, since being an isomorphism is a proposition.
For univalent categoriesπ
Now we want to characterise the space of paths between univalent categories, as a refinement of the identity system constructed above. There are two observations that will allow us to do this like magic:
Being univalent is a property of a precategory: Univalence is defined to mean that the relation is an identity system for the objects of , and βbeing an identity systemβ is a property of a relation1
Between univalent categories, being an adjoint equivalence is a property of a functor, and it is logically equivalent to being an isomorphism of the underlying precategories.
Putting this together is a matter of piecing pre-existing lemmas together. The first half of the construction is by observing that the map (of types) which forgets univalence for a given category is an embedding, so that we may compute an identity system on univalent categories by pulling back that of precategories:
Category-identity-system-pre : β {o β} β is-identity-system {A = Ξ£ (Precategory o β) is-category} (Ξ» C D β Ξ£ (Functor (C .fst) (D .fst)) is-precat-iso) (Ξ» a β Id , iso id-equiv id-equiv) Category-identity-system-pre = pullback-identity-system Precategory-identity-system (fst , (Subset-proj-embedding (Ξ» x β is-identity-system-is-prop)))
module _ {o oβ² β ββ²} {C : Precategory o β} {D : Precategory oβ² ββ²} (F : Functor C D) (eqv : is-equivalence F) where private open is-equivalence eqv module C = Cat.Reasoning C module D = Cat.Reasoning D module F = Fr F open _=>_
Then, since the spaces of equivalences and isomorphisms are both defined as the total space of a predicate on the same types, it suffices to show that the predicates are equivalent pointwise, which follows by propositional extensionality and a tiny result to adjust an equivalence into an isomorphism.
Category-identity-system : β {o β} β is-identity-system {A = Ξ£ (Precategory o β) is-category} (Ξ» C D β Ξ£ (Functor (C .fst) (D .fst)) is-equivalence) (Ξ» a β Id , Id-is-equivalence) Category-identity-system = transfer-identity-system Category-identity-system-pre (Ξ» x y β Ξ£-ap-snd Ξ» F β prop-ext! {bprop = is-equivalence-is-prop (x .snd) F} is-precat-isoβis-equivalence (eqvβiso (x .snd) (y .snd) F))
To show that this equivalence sends βreflexivityβ to βreflexivityβ, all that matters is the functor (since being an equivalence is a proposition), and the functor is definitionally preserved.
(Ξ» x β Ξ£-prop-path (is-equivalence-is-prop (x .snd)) refl)
where module _ {C D : Precategory _ _} (ccat : is-category C) (dcat : is-category D) (F : Functor C D) (eqv : is-equivalence F) where open is-precat-iso open is-equivalence
And now the aforementioned tiny result: All equivalences are fully faithful, and if both categories are univalent, the natural isomorphisms and provide the necessary paths for showing that is an equivalence of types.
eqvβiso : is-precat-iso F eqvβiso .has-is-ff = is-equivalenceβis-ff F eqv eqvβiso .has-is-iso = is-isoβis-equiv Ξ» where .is-iso.inv β eqv .Fβ»ΒΉ .Fβ .is-iso.rinv x β dcat .to-path $ Nat-isoβIso (FβFβ»ΒΉβ Id eqv) _ .is-iso.linv x β sym $ ccat .to-path $ Nat-isoβIso (Idβ Fβ»ΒΉβF eqv) _
Really, itβs a property of a pointed relation, but this does not make a difference here.β©οΈ