3 ms·
I don't think the argument is that it's impossible to mechanize proofs outside of HoTT---just that it's prettier and perhaps better there.
by tel 12y ago
I don't think the argument is that it's impossible to mechanize proofs outside of HoTT---just that it's prettier and perhaps better there.
- cscurmudgeon 12y ago"Prettier" is subjective.
- tel 12y agoAbsolutely. Never claimed otherwise.