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.

  : βˆ€ {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

    : βˆ€ 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) β†’ }) (inS (hcomp (βˆ‚ i) Ξ» where
    j (i = i0) β†’ F .F-id (~ j)
    j (i = i1) β†’
    j (j = i0) β†’

  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
      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:

  : βˆ€ {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)
    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 (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:

  : βˆ€ {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 =
    (fst , (Subset-proj-embedding (Ξ» x β†’ is-identity-system-is-prop)))

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.

  : βˆ€ {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)
      (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 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.β†©οΈŽ