Update SSimplicial.v

Defining simplicial sets.  In the present arrangement, with Funext we should also get that cellClosure is an inverse to topFacet, though that rather takes the fun out of having all the binomial-lists and such...
Supposing the dependent version of nCkList can be got to work everywhere it needs to, then the type `Cells _ _` can perhaps be adjusted to
 ` { cell_facets : lSect (nCkList (names k) _ n) &  lSect (k => nCkSect (Zipper rels (cell_facets (S k)) (cell_facets k)) } ` or such-like.