I have entered the following code in CoqIde:
Require Export Classical.
Require Export Description.
Inductive pbool : Type :=
T : pbool
| F : pbool
| U : pbool.
Variables s p e t f: Type.
Axiom classical_definite_description :
forall (A : Type) (P : A->pbool), inhabited A ->
{ x : A | (exists! x : A, P x) -> P x }.
I am working in a type theory with three truth values: true, false and undefined. Hence I created a type pbool
as above. However I also require a definite description (Hilbert's iota) operator that returns exactly one element from a set of objects.
In the axioms above I initially had Prop
and changed it to pbool
. I then receive the error that The term "P x0" has type "pbool" while it is expected to have type "Prop".
How can I change the definition of the description operator so that it works with pbool?
Prop
,Set
, and theType
hierarchy (and alsoSProp
if experimental strict propositions are enabled). If you want to shallow-embed a logic into Coq, you have to add axioms such that one of these existing sorts acts like your desired notion of proposition. I don't know whether this can be done in your case; you might have to tell us more about the logic you have in mind.