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)

Filter by
Sorted by
Tagged with
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 ...
Russoul's user avatar
  • 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., ...
KANG Rongji's user avatar