The nerve of a category is a quasicategory

In AlgebraicTopology.Quasicategory.StrictSegal, we show that any strict Segal simplicial set is a quasicategory. In AlgebraicTopology.SimplicialSet.StrictSegal, we show that the nerve of a category satisfies the strict Segal condition.

In this file, we prove as a direct consequence that the nerve of a category is a quasicategory.

instance CategoryTheory.Nerve.quasicategory {C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.nerve C).Quasicategory

By virtue of satisfying the StrictSegal condition, the nerve of a category is a Quasicategory.