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

open import Cat.Solver
open import Cat.Base

import Cat.Reasoning

open Cat.Reasoning using (Isomorphism ; id-iso)
open Precategory using (Ob)

module Cat.Univalent where

(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.

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 {A} {B} = Equiv (identity-system-gives-path r {a = A} {b = B})
  open Cat.Reasoning C hiding (id-iso) public
  iso→path :  {A B}  A  B  A  B
  iso→path = path→iso.to

  J-iso :  {} {A} (P :  B  A  B  Type )
         P A (id-iso C)
          {B} (p : A  B)  P B p
  J-iso {A} P pid {B} p = IdsJ r P pid p

  iso→path-id :  {A}  iso→path (id-iso C {A})  refl
  iso→path-id = to-path-refl r

  iso→path→iso :  {A B} (p : A  B)  path→iso (iso→path p)  p
  iso→path→iso p = from-pathp (r .to-path-over p)

  path→iso→path :  {A B} (p : A  B)  iso→path (path→iso p)  p
  path→iso→path p = J  B p  iso→path (path→iso p)  p)
    (ap (r .to-path) (transport-refl _)  to-path-refl r) p

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-groupoid (C .Precategory.Ob)
  Ob-is-groupoid x y =
    equiv→is-hlevel 2 iso→path (identity-system-gives-path r .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)\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)