countType is a subclass of
Ana de Almeida Borges said:
Karl Palmskog said:
from what I can recall, one can get a
choiceTypenearly automatically at any point, and I don't think any
Without adding any axiom to Coq, in a closed context, I do not think there is a concrete
choiceType that couldn't be turned into a
However when adding a general choice axiom (as in mathcomp analysis) every type can be equipped with a
choiceType, while assuming any type could be
countType would easily lead to contradiction. In particular we can equip the classical reals with a
choiceType and use the normal mathcomp structures without any trouble.
Ana de Almeida Borges has marked this topic as resolved.
Last updated: Feb 08 2023 at 04:04 UTC