Stream: math-comp users

Topic: ✔ countType vs choiceType

Alexander Gryzlov (Nov 03 2022 at 16:10):

countType is a subclass of choiceType

Cyril Cohen (Nov 03 2022 at 16:11):

Ana de Almeida Borges said:

Karl Palmskog said:

from what I can recall, one can get a countType from a choiceType nearly automatically at any point, and I don't think any finType is involved

How? Are choiceType and countType actually interchangeable?

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 countType.
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.

Notification Bot (Nov 03 2022 at 16:27):

Ana de Almeida Borges has marked this topic as resolved.

Last updated: Feb 08 2023 at 04:04 UTC