Post #4230140

I wish there were other implementations of 2-level type theory, not just MLTT (outer) / HoTT (inner) but rather OTT / MLTT, as it is quite hard to track down which is which... 😵