I would like to ask about people’s opinion on and experience with using axioms in Coq developments. Pragmatically, excluded middle, functional extensionality, proof irrelevance, make so many things easier. It seems so intuitive to think about programs in terms of classical logic and set theory. So …

What do you think of axioms?

SkySkimmer August 3, 2019, 3:28pm 10

cubical tt has FE and canonicity AFAIK

Gaëtan Gilbert