Yes, terms in Prop are routinely defined nonconstructively, but this is all happening within the context of a constructive (or at least very much not set-theoretic) metatheory. So for instance LEM gets derived from choice by Diaconescu’s theorem, types are conventionally supposed to be constructive, you sometimes have to care about definitional vs. propositional equality, etc.
Yes, terms in
Propare routinely defined nonconstructively, but this is all happening within the context of a constructive (or at least very much not set-theoretic) metatheory. So for instance LEM gets derived from choice by Diaconescu’s theorem, types are conventionally supposed to be constructive, you sometimes have to care about definitional vs. propositional equality, etc.