open import 1Lab.Prelude hiding (_∘_ ; id)

open import Cat.Solver
open import Cat.Base

module Cat.Univalent {o h} (C : Precategory o h) where

open import Cat.Morphism C

(Univalent) Categories🔗

In much the same way that a partial order is a preorder where xyyxx=yx \le y \land y \le x \to x = y, a category is a precategory where isomorphic objects are identified. This is a generalisation of the univalence axiom to arbitrary categories, and, indeed, it’s phrased in the same way: asking for a canonically defined map to be an equivalence.

A precategory is a category precisely when the type (Σ[ B ∈ _ ] C [ A ≅ B ]) is contractible. This implies that the type A ≡ B is equivalent to the type C [ A ≃ B ], for any pair of objects A, B in the category. This is because Σ[ B ∈ _ ] (A ≡ _) is also contractible. Further, the type C [ A ≃ B ] satisfies J, by the same argument used to construct EquivJ.

is-category : Type _
is-category =  A  is-contr (Σ[ B  _ ] A  B)

This notion of univalent category corresponds to the usual notion — which is having the canonical map from paths to isomorphisms be an equivalence — by the following argument: Since the types (Σ[ B ∈ _ ] C [ A ≅ B ]) and Σ[ B ∈ _ ] A ≣ B, the action of path→iso on total spaces is an equivalence; Hence path→iso is an equivalence.

path→iso :  {A B}  A  B  A  B
path→iso {A = A} p = transport  i  A  p i) id-iso

First we define, exactly as in the book, the canonical map path→iso.

path→iso-is-equiv : is-category   {A B}  is-equiv (path→iso {A = A} {B = B})
path→iso-is-equiv iscat {A} {B} = total→equiv is-equiv-total where
  P Q : Precategory.Ob C  Type _
  P B = A  B
  Q B = A  B

We consider the map path→iso as a fibrewise equivalence between the two families A ≡ - and C [ A ≅ - ]. This lets us reduce the problem of proving that path→iso is an equivalence to the problem of proving that it induces an equivalence of total spaces.

  is-equiv-total : is-equiv (total {P = P} {Q = Q}  A p  path→iso p))
  is-equiv-total =
    is-contr→is-equiv (contr (A , λ i  A) Singleton-is-contr)
                      (iscat _)

Since the total spaces are contractible (Σ P by path induction, Σ Q by the assumption that C is a category) any map between them is an equivalence. This implies that we can turn categorical isomorphisms into paths of objects:

iso→path : is-category
           {A B}
          A  B
          A  B
iso→path cat = is-equiv→is-iso (path→iso-is-equiv cat) .is-iso.inv

Not only is it necessary for the map iso→path to be an equivalence for a precategory to be univalent, having spaces of isomorphisms equivalent to spaces of identifications is also a sufficient condition:

iso≃path→is-category : (∀ {A B}  (A  B)  (A  B))  is-category
iso≃path→is-category iso≃path A =
  equiv→is-hlevel 0
    (total λ x  iso≃path .fst)
    (equiv→total λ {x}  iso≃path .snd)
    (contr (A , λ i  A) Singleton-is-contr)

Furthermore, we have that this function is an equivalence, and so the type of objects in a univalent category is at most a groupoid. We use the fact that h-levels are closed under equivalences and that dependent sums preserve h-levels.

Ob-is-groupoid : is-category  is-groupoid (C .Precategory.Ob)
Ob-is-groupoid iscat x y =
  equiv→is-hlevel 2
    (iso→path iscat)
    (((_ , path→iso-is-equiv iscat) e⁻¹) .snd)

We can characterise transport in the Hom-sets of categories using the path→iso equivalence. Transporting in hom(p i,q i)\hom(p\ i, q\ i) is equivalent to turning the paths into isomorphisms and pre/post-composing:

Hom-transport :  {A B C D} (p : A  C) (q : B  D) (h : Hom A B)
               transport  i  Hom (p i) (q i)) h
               path→iso q .to  h  path→iso p .from
Hom-transport {A = A} {B} {D = D} p q h i =
  comp  j  Hom (p (i  j)) (q (i  j)))
        { j (i = i0)  coe0→i  k  Hom (p (j  k)) (q (j  k))) j h
          ; j (i = i1)  path→iso q .to  h  path→iso p .from
       (hcomp  { j (i = i0)  idl (idr h j) j
                 ; j (i = i1)  q′ i1  h  p′ i1
              (q′ i  h  p′ i))
    p′ : PathP _ id (path→iso p .from)
    p′ i = coe0→i  j  Hom (p (i  j)) A) i id

    q′ : PathP _ id (path→iso q .to)
    q′ i = coe0→i  j  Hom B (q (i  j))) i id

This lets us quickly turn paths between compositions into dependent paths in Hom-sets.

Hom-pathp :  {A B C D} {p : A  C} {q : B  D} {h : Hom A B} {h' : Hom C D}
           path→iso q .to  h  path→iso p .from  h'
           PathP  i  Hom (p i) (q i)) h h'
Hom-pathp {p = p} {q} {h} {h'} prf =
  to-pathp (subst (_≡ h') (sym (Hom-transport p q h)) prf)