open import Cat.Functor.Adjoint.Unique
open import Cat.Functor.Equivalence
open import Cat.Instances.Functor
open import Cat.Functor.Adjoint
open import Cat.Functor.Base
open import Cat.Univalent
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 F:Cβ†’DF : \mathcal{C} \to \mathcal{D} 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, FF’s action on objects F0F_0 is an equivalence, so by univalence it induces an equivalence C0≑D0\mathcal{C}_0 \equiv \mathcal{D}_0. 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 ungluei∨¬i(x){\mathrm{unglue}}_{i \lor \neg i}(x) is a term in D0\mathcal{D}_0 which evaluates to F0(x)F_0(x) when i=i1i = i1 or i=i0i = i0, so that the system described above can indeed be built. The introduction rule for hom is hom-glue: If we have a partial element ¬i⊒f:HomCxy\neg i \vdash f : {\mathbf{Hom}}_\mathcal{C} x y together with an element gg of base type satisfying definitionally ¬i⊒F1(f)=g\neg i \vdash F_1(f) = g, we may glue ff along gg to get an element of homi(x,y){\mathrm{hom}}_i(x, y).

  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 idC{{\mathrm{id}}_{}}_\mathcal{C} on the left and idD{{\mathrm{id}}_{}}_\mathcal{D} by gluin}_$ against the proof that FF 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 PP along the line homi{\mathrm{hom}}_i, in a way that agrees with the original categories. We do this by piecing together a square whose sides are the witness that PP is a proposition, and where the base is given by spreading (coe0β†’i) the proposition from C\mathcal{C} 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

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:

  1. Being univalent is a property of a precategory: Univalence is defined to mean that the relation Xβ‰…YX \cong Y is an identity system for the objects of C\mathcal{C}, 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)))

Then, since the spaces of equivalences C≅D\mathcal{C} \cong \mathcal{D} and isomorphisms C→D\mathcal{C} \to \mathcal{D} 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)

And now the aforementioned tiny result: All equivalences are fully faithful, and if both categories are univalent, the natural isomorphisms Fβˆ’1Fβ‰…IdF^{-1}F \cong {\mathrm{Id}} and FFβˆ’1β‰…IdFF^{-1} \cong {\mathrm{Id}} provide the necessary paths for showing that F0F_0 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) _

  1. Really, it’s a property of a pointed relation, but this does not make a difference here.β†©οΈŽ