Salvage work from #885 #1516
Description
In #885, @EgbertRijke did a lot of amazing refactoring work to synthetic-homotopy-theory, but sadly never managed to finish the PR. It would be amazing if someone took the time to see what is there and perhaps start to incrementally salvage some of it.