[hash-no-gal-fld]

I don't think you intended "propositionally" equal in your final sentence. Equality is data in HoTT. If you take the propositional truncation then you usually throw away too much.

[ebingdom]

Yeah, I only meant as opposed to judgmental equality, not the quality of being a proposition.