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