If you have "Homotopy Type Theory" than does a more traditional "Homotopy Set Theory" exist too?
I think the simplest axiomization would be something like ZFC extended with a set of intervals with a nontrivial set of identities. I assume there would be difficulties with such a simple approach though.