Trying a slightly (not very) different presentation of simplicials,
but want SSimplicial to be handy if wanted.

More basic-like fixpoints in nCk and generalLists.

Signed-off-by: jcmckeown <jesse@sockwright>
We really don't like having to deal with equations in the computations;
it's usually preferable to construct the concomitant equivalences
instead, especially if they unfold/simplify nicely. Nonetheless, it's
good to know/construct that the equations are also there; and so here is
a library of some comforting equations.

Signed-off-by: jcmckeown <jesse@sockwright>
We now really do have all the needed framework for the semisimplicial type
presented by a relational semisimplicial complex.

We have tried to avoid even mentioning equality, for the sake of having
proof terms with good behaviour under partial evaluation; part of this is
explicitly constructing the coinhabitation arguments that would be provided
by transport [ and which, with Funext and Univalence, conversely provide
the identification to transport over ]

There are, however, one or two spots where transport is used, though I'm
sure these could be eliminated as well, and I don't know what effect
keeping them will have on the next layers of development.

lList has been adjusted so as to more-closely resemble nCkList; I don't
know if this is important.

nCkEqns does have equations in it, but it is mostly about most of the
coinhabitations mentioned above.