The strict bicategory of quasicategories

In this file we define a strict bicategory QCat.strictBicategory whose objects are quasicategories.

This strict category is defined from QCat.catEnrichedOrdinaryCategory which is the Cat-enriched ordinary category of quasicategories whose hom-categories are the homotopy categories of the simplicial internal homs, defined by applying hoFunctor : SSet ⥤ Cat.

As an enriched ordinary category, there is an equivalence QCat.forgetEnrichment.equiv between the underlying category and the full subcategory of quasicategories. Thus the 1-morphisms of QCat.strictBicategory are maps of simplicial sets.

Future work will use the fact that quasicategories define a cartesian closed subcategory of simplicial sets to identify the 2-morphisms of QCat.strictBicategory with homotopy classes of homotopies between them, defined using the simplicial interval Δ[1].

This strict bicategory serves as a setting to develop the formal category theory of quasicategories.

References

• Emily Riehl and Dominic Verity, Elements of ∞-Category Theory
• Emily Riehl and Dominic Verity, The 2-category theory of quasi-categories

@[reducible, inline]

abbrev SSet.QCat : Type (u_1 + 1)

QCat is the category of quasi-categories defined as the full subcategory of the category SSet of simplicial sets.

Equations

• SSet.QCat = CategoryTheory.ObjectProperty.FullSubcategory SSet.Quasicategory

noncomputable instance SSet.QCat.catEnrichedOrdinaryCategory : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat QCat

QCat obtains a Cat-enriched ordinary category structure by applying hoFunctor to the hom objects in its SSet-enriched ordinary structure.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SSet.QCat.forgetEnrichment.equiv : CategoryTheory.ForgetEnrichment CategoryTheory.Cat QCat ≌ QCat

The underlying category of the Cat-enriched ordinary category of quasicategories is equivalent to QCat.

Equations

• SSet.QCat.forgetEnrichment.equiv = CategoryTheory.ForgetEnrichment.equiv CategoryTheory.Cat

noncomputable instance SSet.QCat.bicategory : CategoryTheory.Bicategory QCat

The bicategory of quasicategories extracted from QCat.CatEnrichedOrdinaryCat.

Equations

• SSet.QCat.bicategory = CategoryTheory.CatEnrichedOrdinary.instBicategory

instance SSet.QCat.strictBicategory : CategoryTheory.Bicategory.Strict QCat

The strict bicategory of quasicategories extracted from QCat.CatEnrichedOrdinaryCat.