On Sun, Apr 1, 2012 at 7:10 PM, Christopher Done
<chrisdone@googlemail.com> wrote:
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.