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.
Conversation
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
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.
To be clear, this was done ages ago in Idris 1, so I'm not sure if there's been any changes in Idris 2 to the way mutual blocks work.
1