module Cat.Univalent where
(Univalent) categories🔗
In much the same way that a partial order is a preorder where 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 category to be univalent when its family of isomorphisms is an identity system. As usual, this natively cubical phrasing gives us slightly better definitional control over both the paths and the coherences that go into making a category univalent, but by a standard argument about identity systems, this is equivalent to the “book” notion.
is-category : ∀ {o h} (C : Precategory o h) → Type (o ⊔ h) is-category C = is-identity-system (Isomorphism C) (λ a → id-iso C)
We set aside some helpers specifically for working with the assumption that a category is univalent.
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
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)
Hom-transport-id : ∀ {A C D} (p : A ≡ C) (q : A ≡ D) → transport (λ i → Hom (p i) (q i)) id ≡ path→iso q .to ∘ path→iso p .from Hom-transport-id p q = Hom-transport p q _ ∙ ap (path→iso q .to ∘_) (idl _) Hom-transport-refll-id : ∀ {A B} (q : A ≡ B) → transport (λ i → Hom A (q i)) id ≡ path→iso q .to Hom-transport-refll-id p = Hom-transport-id refl p ∙ elimr (transport-refl _) Hom-transport-reflr-id : ∀ {A B} (q : A ≡ B) → transport (λ i → Hom (q i) A) id ≡ path→iso q .from Hom-transport-reflr-id p = Hom-transport-id p refl ∙ eliml (transport-refl _) Hom-pathp-refll : ∀ {A B C} {p : A ≡ C} {h : Hom A B} {h' : Hom C B} → h ∘ path→iso p .from ≡ h' → PathP (λ i → Hom (p i) B) h h' Hom-pathp-refll prf = Hom-pathp (ap₂ _∘_ (transport-refl id) refl ∙∙ idl _ ∙∙ prf) Hom-pathp-reflr : ∀ {A B D} {q : B ≡ D} {h : Hom A B} {h' : Hom A D} → path→iso q .to ∘ h ≡ h' → PathP (λ i → Hom A (q i)) h h' Hom-pathp-reflr {q = q} prf = Hom-pathp (ap (path→iso q .to ∘_) (ap₂ _∘_ refl (transport-refl _)) ∙∙ ap₂ _∘_ refl (idr _) ∙∙ prf) Hom-pathp-id : ∀ {A B C} {p : B ≡ A} {q : B ≡ C} {h' : Hom A C} → PathP (λ i → Hom (p i) (q i)) (id {B}) h' → path→iso q .to ∘ path→iso p .from ≡ h' Hom-pathp-id {p = p} {q} {h} prf = J' (λ B A p → ∀ {C} (q : B ≡ C) {h' : Hom A C} → PathP (λ i → Hom (p i) (q i)) (id {B}) h' → path→iso q .to ∘ path→iso p .from ≡ h') (λ x q prf → ap₂ _∘_ refl (transport-refl _) ∙∙ idr _ ∙∙ from-pathp prf) p q prf path→to-∙ : ∀ {A B C} (p : A ≡ B) (q : B ≡ C) → path→iso (p ∙ q) .to ≡ path→iso q .to ∘ path→iso p .to path→to-∙ {A = A} p q = J (λ B p → ∀ {C} (q : B ≡ C) → path→iso (p ∙ q) .to ≡ path→iso q .to ∘ path→iso p .to) (λ q → subst-∙ (λ e → Hom A e) refl q _ ∙ ap (subst (λ e → Hom A e) q) (transport-refl id) ∙ sym (idr _) ∙ ap₂ _∘_ refl (sym (transport-refl id)) ) p q path→from-∙ : ∀ {A B C} (p : A ≡ B) (q : B ≡ C) → path→iso (p ∙ q) .from ≡ path→iso p .from ∘ path→iso q .from path→from-∙ {A = A} p q = J (λ B p → ∀ {C} (q : B ≡ C) → path→iso (p ∙ q) .from ≡ path→iso p .from ∘ path→iso q .from) (λ q → subst-∙ (λ e → Hom e _) refl q _ ∙∙ ap (subst (λ e → Hom e _) q) (transport-refl id) ∙∙ sym (idl _) ∙ ap₂ _∘_ (sym (transport-refl id)) refl ) p q path→iso-∙ : ∀ {A B C} (p : A ≡ B) (q : B ≡ C) → path→iso (p ∙ q) ≡ path→iso p ∙Iso path→iso q path→iso-∙ p q = ext (path→to-∙ p q) path→to-sym : ∀ {A B} (p : A ≡ B) → path→iso p .from ≡ path→iso (sym p) .to path→to-sym = J (λ B p → path→iso p .from ≡ path→iso (sym p) .to) refl from-pathp-to : ∀ {A B C} (p : A ≡ B) {f g} → PathP (λ i → Hom C (p i)) f g → path→iso p .to ∘ f ≡ g from-pathp-to {C = C} p q = J (λ B p → ∀ {f g} → PathP (λ i → Hom C (p i)) f g → path→iso p .to ∘ f ≡ g) (λ q → eliml (transport-refl _) ∙ q) p q from-pathp-from : ∀ {A B C} (p : A ≡ B) {f g} → PathP (λ i → Hom C (p i)) f g → path→iso (sym p) .from ∘ f ≡ g from-pathp-from {C = C} p q = ap₂ _∘_ (path→to-sym (sym p)) refl ∙ from-pathp-to p q from-pathp-from' : ∀ {A B C} (p : A ≡ B) {f g} → PathP (λ i → Hom (p i) C) f g → f ∘ path→iso p .from ≡ g from-pathp-from' {C = C} p q = J (λ B p → ∀ {f g} → PathP (λ i → Hom (p i) C) f g → f ∘ path→iso p .from ≡ g) (λ q → elimr (transport-refl _) ∙ q) p q from-pathp-to' : ∀ {A B C} (p : A ≡ B) {f g} → PathP (λ i → Hom (p i) C) f g → f ∘ path→iso (sym p) .to ≡ g from-pathp-to' {C = C} p q = ap₂ _∘_ refl (sym (path→to-sym p)) ∙ from-pathp-from' p q module Univalent {o h} {C : Precategory o h} (r : is-category C) where open Univalent' r public Hom-pathp-refll-iso : ∀ {A B C} {p : A ≅ C} {h : Hom A B} {h' : Hom C B} → h ∘ p .from ≡ h' → PathP (λ i → Hom (iso→path p i) B) h h' Hom-pathp-refll-iso prf = Hom-pathp-refll C (ap₂ _∘_ refl (ap from (iso→path→iso _)) ∙ prf) Hom-pathp-reflr-iso : ∀ {A B D} {q : B ≅ D} {h : Hom A B} {h' : Hom A D} → q .to ∘ h ≡ h' → PathP (λ i → Hom A (iso→path q i)) h h' Hom-pathp-reflr-iso prf = Hom-pathp-reflr C (ap₂ _∘_ (ap to (iso→path→iso _)) refl ∙ prf) Hom-pathp-iso : ∀ {A B C D} {p : A ≅ C} {q : B ≅ D} {h : Hom A B} {h' : Hom C D} → q .to ∘ h ∘ p .from ≡ h' → PathP (λ i → Hom (iso→path p i) (iso→path q i)) h h' Hom-pathp-iso {p = p} {q} {h} {h'} prf = Hom-pathp C (ap₂ _∘_ (ap to (iso→path→iso _)) (ap₂ _∘_ refl (ap from (iso→path→iso _))) ∙ prf)