Merge pull request #591 from mikeshulman/biinv-naming

Conform to naming conventions a bit better
PathSplit maps as another variety of equivalence
Use pointwise pathsplitness in reflective subuniverses
build repleteness into UnitSubuniverses
start the recursion in PathSplit at a more sensible place