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
I dunno I’ve always felt the induction-recursion approach was a tad clunky, but maybe that’s because you can’t really have ‘open inductive types’.