
1 Apr
2012
1 Apr
'12
1:10 p.m.
I actually read the first couple paragraphs and thought “sounds interesting I'll read it later”. After reading it properly, I lol'd.
After some initial feedback, I'm going to create a page for the Homotopy Extensional Records Proposal (HERP) on trac. There are really only a few remaining questions. 1) Having introduced homotopies, why not go all the way and introduce dependent records? In fact, are HERP and Dependent Extensional Records Proposal (DERP) already isomorphic? My suspicion is that HERP is isomorphic, but DERP is not.