Hi Robin,
thank you for your comments. Indeed we are currently revising this
paper, hence your comments are especially welcome.
I've been reading "Towards Observational Type Theory". I'm new to type
theory, so I have not been able to understand big chunks of the paper;
hopefully as I read wi
Hi Robin,
I just saw Thorsten answered your e-mail. I'd better finish what I
started though.
I'm not an expert on OTT, but here are a few thoughts.
The "real" rule for coercion is the one on page 3. It doesn't require
the types to be definitionally equal. Section 5 mainly speculates on
a
Hi Robin
I was just about to reply when I noticed Thorsten had...
Robin Green wrote:
I've been reading "Towards Observational Type Theory". I'm new to type
theory, so I have not been able to understand big chunks of the paper;
hopefully as I read wider I'll understand more of it.
However, one
