I'm not sure there is a reasonable choice for bool? : o -> o
that makes the translation from DHOL to HOL satisfy completeness.
Assuming HOL is classical and fully extensional, there are only
semantically four choices for bool?. Only the constantly true
one seems to have any chances of "working," but I doubt it
would satisfy what you want.

I think the main issue is with the contravariance of arrow types.
If A is a "subtype" of A', then A' -> B should be a "subtype" of A -> B.
An example I like to use is this one:

(fun f:Even -> Nat => f 1)

This should be "ill-typed" in DHOL, but is likely to look
"well-typed" after translating to HOL using unary predicates.

You have dependent types, not subtypes, but I think the same
kind of issue comes up. A dependent type like
b : a -> type
will essentially partition a simple type "b" into subtypes recognized
by b? x where x ranges over "a".

My real recommendation is to use pers (binary relations) instead
of unary predicates. (That's probably not a surprise to you.
I think you asked me "why use pers?" in Seattle in 2006 and
I didn't give you a satisfactory answer. I should've at least
said "contravariance of ->" but probably didn't.)

Instead of

a? : a -> o
have
a? : a -> a -> o

and have invariants that a? is a per.
Or, in general

(a t1 ... tn)? : a -> a -> o

as pers parameterized by the ti's.

(Pi x:A . B)? : (a -> b) -> (a -> b) -> o
    = (fun f g:a -> b => forall x y, A? x y -> B? (f x) (f y)) [Note: some x's might occur in B?]

bool? : o -> o -> o := fun x y:o => x = y.

So "bool?" isn't "everything" like in the unary case, but "in the middle"
between the smallest per (the empty relation) and the full per (the full relation).

Looking at the example
(fun f : Even -> Nat => f 1) :: (Even -> Nat) -> Nat
which should *not* hold in DHOL since "f 1" looks ill-typed,
it would translate using pers to HOL in a way like

(forall f g, (forall x y, Even? x y -> Nat? (f x) (g y)) -> Nat? (f 1) (g 1))

If Even? x y means x = y and x is even
and Nat? x y means x = y and x is a nat,
then this HOL proposition will be false (and hence unprovable).
It's false because f could be constant 0 and g could take evens to 0
and odds to 1.

Using unary predicates it would translate to

(forall f, (forall x, Even? x -> Nat? (f x)) -> Nat? (f 1))

which, well, maybe it's true or maybe it's false.
It being false depends on knowing there is at least one
thing of the right type where Nat? fails.

I spent a little time trying to modify this Even / Nat subtyping example
to be an example for dependent types, not subtypes, but it wasn't obvious
how to.

- C.