Questions tagged [constructive-mathematics]
Broadly speaking, constructive mathematics is mathematics done without the principle of excluded middle, or other principles, such as the full axiom of choice, that imply it, hence without “non-constructive” methods of formal proof, such as proof by contradiction. This is in contrast to classical mathematics, where such principles are taken to hold. (from nLab)
2
questions
3
votes
2
answers
88
views
State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types
I don't think a particular choice of such type theory matters much.
Extensional MLTT, SetoidTT, OTT, HoTT, HOTT, CuTT -- they all support quotient types.
Reals is supposed to be a Set (in HoTT ...
- 163
17
votes
2
answers
261
views
Is there computational interpretation for countable choice?
I've wondered how a type theory/proof assistant could manage to add countable choice (or its dependent choice version) as something primitive as well as to keep the computational properties, e.g., ...
- 660