Post #1948799

@jeanas @jhostert recently I've been pondering a little about how one could approach exposition of HoTT/UF, and I think that presenting the Hofmann-Streicher 1-groupoid model of MLTT could actually be a good stepping stone for gaining some intuition of what the whole "proof-relevant equality" business is all about...