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?

`countType`

is a subclass of `choiceType`

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 involvedHow? 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.

Ana de Almeida Borges has marked this topic as resolved.

Last updated: Jul 23 2024 at 20:01 UTC