> I don't agree that what's being described here "is the HoTT point of view". I am no expert in HoTT, so I certainly defer to what sounds like your expertise h

> I don't agree that what's being described here "is the HoTT point of view". I am no expert in HoTT, so I certainly defer to what sounds like your expertise here. I should probably have said something closer to the weaker statement "this reminds me of HoTT", which hopefully is not incorrect—although you're right that what I really had in mind was proof relevance.