3 ms·

Yes. Also it includes topology.

• TheAsprngHacker 7y ago
  Calling it topology can be misleading, as HoTT only considers types as spaces in the sense of homotopy equivalence.