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 $x \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 
    (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 
    (iso→path iscat)
    (((_ , path→iso-is-equiv iscat) e⁻¹) .snd)
    ≅-is-set

We can characterise transport in the Hom-sets of categories using the path→iso equivalence. Transporting in $\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))
  where
    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)