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
This Tweet is from a suspended account. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
This Tweet is from a suspended account. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Yup, it does!
This Tweet is from a suspended account. Learn more
Yeah, I think so - not sure what Idris 2 does. Ie. it's not like Agda where you need to forward-declare stuff mutually recursive stuff.
1
1
Show replies