Strict Segal simplicial sets are quasicategories

In AlgebraicTopology.SimplicialSet.StrictSegal, we define the strict Segal condition on a simplicial set X. We say that X is strict Segal if its simplices are uniquely determined by their spine.

In this file, we prove that any simplicial set satisfying the strict Segal condition is a quasicategory.

theorem SSet.StrictSegal.quasicategory {X : SSet} (sx : X.StrictSegal) : X.Quasicategory

Any StrictSegal simplicial set is a Quasicategory.

instance SSet.StrictSegal.quasicategory' (X : SSet) [X.IsStrictSegal] : X.Quasicategory

Any simplicial set satisfying IsStrictSegal is a Quasicategory.