>>13666627Not if you interpret as the squashed variant of the existential type, or the one in Prop if you were in CIC. In general, this type does not enjoy choice.
If you extend your theory with classical logic in propositions it then makes perfect sense because there are no such choice functions in general but it's fine to merely accept their existence.
