module Cat.Univalent where

(Univalent) categories🔗

In much the same way that a partial order is a preorder where $x \leq y \land y \leq 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.

We define a precategory to be univalent when it can be equipped when its family of isomorphisms is an identity system.

is-category : ∀ {o h} (C : Precategory o h) → Type (o ⊔ h)
is-category C = is-identity-system (Isomorphism C) (λ a → id-iso C)

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
  : ∀ {o h} {C : Precategory o h} {A B}
  → A ≡ B → Isomorphism C A B
path→iso {C = C} {A} p = transport (λ i → Isomorphism C A (p i)) (id-iso C)

module Univalent' {o h} {C : Precategory o h} (r : is-category C) where
  module path→iso = Ids r
    renaming ( to            to iso→path
             ; J             to J-iso
             ; to-refl       to iso→path-id
             ; η             to iso→path→iso
             ; ε             to path→iso→path
             )

  open Cat.Reasoning C hiding (id-iso) public

  open path→iso
    using ( iso→path ; J-iso ; iso→path-id ; iso→path→iso ; path→iso→path )
    public

Furthermore, since the h-level of the relation behind an identity system determines the h-level of the type it applies to, we have that the space of objects in any univalent category is a groupoid:

  Ob-is-groupoid : is-groupoid ⌞ C ⌟
  Ob-is-groupoid = path→iso.hlevel 2 λ _ _ → hlevel 2

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:

module _ {o h} (C : Precategory o h) where
  open Cat.Reasoning C hiding (id-iso ; Isomorphism)
  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))) (∂ i) λ where
      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
      j (j = i0) → hcomp (∂ i) λ where
        j (i = i0) → idl (idr h j) j
        j (i = i1) → q' i1 ∘ h ∘ p' i1
        j (j = i0) → 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)