Zulip Chat Archive

Stream: maths

Topic: quasicategories


view this post on Zulip 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 }

view this post on Zulip Johan Commelin (May 11 2019 at 03:44):

This is similar to the definitions of Lurie, right?

view this post on Zulip Johan Commelin (May 11 2019 at 03:45):

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

view this post on Zulip Reid Barton (May 11 2019 at 03:49):

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

view this post on Zulip Johan Commelin (May 11 2019 at 03:50):

Aha... that's good to know.

view this post on Zulip Johan Commelin (May 11 2019 at 03:50):

They seem to be useful gadgets.


Last updated: May 18 2021 at 08:14 UTC