Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I was wondering, famously because the internal language of a topos is not classical it is possible to add classically inconsistent axioms, such as the Kock-Lawvere axiom. Can something similar occur with HoTT?
At this new axioms section it points out that we may add things like Whitehead’s axiom, but this goes in the direction of making things more classical. How about something which relies on the constructive aspect of HoTT?
Hmm, or might modalities play this role?
Yes, “Axiom R” in my realcohesion paper is a nonclassical axiom, inconsistent with full LEM. It doesn’t require higher homotopy, but it becomes much more powerful in the presence of it.
Added another
1 to 5 of 5