open import Cat.Functor.Adjoint.Unique
open import Cat.Functor.Equivalence
open import Cat.Instances.Functor
open import Cat.Prelude

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning

open Functor

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, 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 (and thus has type and when (and thus has type 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! $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:

1. 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

2. 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 = Functor 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 (hlevel 1) (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       $isoβΏβiso (FβFβ»ΒΉβ Id eqv) _ .is-iso.linv x β sym$ ccat .to-path \$ isoβΏβiso (IdβFβ»ΒΉβF eqv) _


1. Really, itβs a property of a pointed relation, but this does not make a difference here.β©οΈ