Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Buzzard’s recent post on canonical isomorphism is interesting. I haven’t been following the Xena project. Am I right in thinking they are using Lean but not HoTT? If so, do people think HoTT can treat this canonicity issue properly?
They are essentially doing classical mathematics in Lean. Certainly not HoTT.
Mike Shulman had the idea (scroll to the end of the original post for the section “Postscript: which equalities can be made judgmental?”) that HoTT’s judgmental equality could be interpreted as a fully coherent system of paths. So maybe then, the canonical equivalences are the ones that are judgmentally equal to the identity. This way, you formally, absolutely cannot possibly get into trouble thinking of canonical equivalences as equality.
AFAIK though, it’s not known whether this interpretation actually works.
added pointer to
1 to 6 of 6