quasicategories

Stream: maths

[Reid Barton]

I would be curious to see what a "plain formalization" of infinity categories looks like. HoTT is more of a "synthetic" formulation, a.k.a a shallow embedding, where you can't see outside the theory and so principles like univalence can be stated unqualified as axioms

Here is a very simple formalization of just the definition of a quasicategory; hopefully I got it right!
The preliminaries on category Δ are by Johan, from some time ago.

import data.fin order.basic
import category_theory.yoneda category_theory.full_subcategory

open category_theory

def simplex_category := ℕ

local notation `Δ` := simplex_category
local notation `[`n`]` := fin (n + 1)

instance : has_coe_to_sort (Δ) := {S := Type, coe := λ n, [n]}

def order_preserving_map (m n : Δ) := {f : m → n // monotone f}

instance {m n : Δ} : has_coe_to_fun (order_preserving_map m n) :=
{ F := λ _, m → n, coe := λ f, f.val }

instance : category Δ :=
{ hom := order_preserving_map,
  id := λ X, ⟨id, monotone_id⟩,
  comp := λ _ _ _ f g, ⟨g.val ∘ f.val, monotone_comp f.2 g.2⟩ }

def SSet := Δᵒᵖ ⥤ Type 0
instance : category SSet := by { dunfold SSet, apply_instance }

def simplex (n : ℕ) : SSet := yoneda.obj (n : Δ)

def misses_face {n m : Δ} (k : [n]) (f : [m] ⟶ [n]) : Prop :=
∃ i, i ≠ k ∧ ∀ j, f j ≠ i

lemma misses_face_preserved {n m' m : ℕ} (g : [m'] ⟶ [m]) (k : [n]) (f : [m] → [n]) :
  misses_face k f → misses_face k (f ∘ g) :=
λ ⟨i, hi₁, hi₂⟩, ⟨i, hi₁, λ j, hi₂ _⟩

def horn (n : ℕ) (k : [n]) : SSet :=
{ obj := λ m, {f : (simplex n).obj m // misses_face k f.val},
  map := λ m' m g, subtype.map ((simplex n).map g) (λ x, misses_face_preserved g k _) }

def horn_simplex_inclusion (n : ℕ) (k : [n]) : horn n k ⟶ simplex n :=
{ app := λ m, subtype.val }

def is_quasicategory (X : SSet) : Prop :=
∀ (n : Δ) (k : [n]), k.val ≠ 0 ∧ k.val ≠ n →
∀ p : horn n k ⟶ X, ∃ q : simplex n ⟶ X, horn_simplex_inclusion n k ≫ q = p

def QCat := {X : SSet // is_quasicategory X}
instance : category QCat := by { dunfold QCat, apply_instance }

[Johan Commelin]

This is similar to the definitions of Lurie, right?

[Johan Commelin]

I don't remember the term quasicategory, but the definitions seem familiar

[Reid Barton]

It's the same thing Lurie calls "$\infty$-categories", and one of several models for $(\infty, 1)$-categories. "Quasicategory" is the original, unambiguous name

[Johan Commelin]

Aha... that's good to know.

[Johan Commelin]

They seem to be useful gadgets.