so this is where you would know better than I, but my impression was that cubical type theory was a very nice system that solves lots of the gross problems with things like setoids in Coq, albeit you're paying for this in having to learn a bit more up-front, maybe..?
Conversation
I like cubical, I think Idris 2 uses linear types though?
4
4
Yeah, Idris 2 is specifically non-cubical, e.g. there's type-case, so you can refute univalence.
There have been rumblings of getting extensionality by adding OTT to Idris 2 on slack, but I don't think anyone has committed to it yet.
3
4
Ohhhh is type case bad for univalence? Is there a place I can read up about this or is it a folklore thing?
1
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Oh cool!
…unless this actually meant as a joke? Sorry I'm not great at the subtle theory stuff 😅
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
'useful for computer science purposes' sounds like my cup of tea 🤩
What is the name of the “Angiuli-Favonia-Harper” paper?
1
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Show replies