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

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)$ 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)