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.

instance SSet.StrictSegal.quasicategory {X : SSet} [X.StrictSegal] : X.Quasicategory

Any StrictSegal simplicial set is a Quasicategory.