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 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 few sections.

I'm not sure if it helps, but here's a bit of Agda code "implementing" OTT:


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.

Reply via email to