I just saw Thorsten answered your e-mail. I'd better finish what I
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
adding two extensions:
* Definitional proof irrelevance
* Definitionally defining all coherence proofs to be refl and
coercions within the same type to be the identity.
Like Thorsten says, this is a bit tricky and makes evaluation and
equality mutually recursive - which is a bit odd. If you're looking
to understand OTT, I wouldn't get too worked up about this rule -
it's a bit technical and the really important stuff is in the first
I'm not sure if it helps, but here's a bit of Agda code
I certainly understood much more of the paper after writing the Agda.
I'm not sure if reading it will have quite the same effect, but it
might be worth a shot.
All the best,
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.