# Zulip Chat Archive

## Stream: maths

### Topic: quasicategories

#### Reid Barton (May 11 2019 at 01:48):

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 (May 11 2019 at 03:44):

This is similar to the definitions of Lurie, right?

#### Johan Commelin (May 11 2019 at 03:45):

I don't remember the term `quasicategory`

, but the definitions seem familiar

#### Reid Barton (May 11 2019 at 03:49):

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 (May 11 2019 at 03:50):

Aha... that's good to know.

#### Johan Commelin (May 11 2019 at 03:50):

They seem to be useful gadgets.

Last updated: May 18 2021 at 08:14 UTC