PHOAS with extrinsic typing?
The standard well-formed-related predicate can be relatively easily extended to handle untyped PHOAS.  The main subtlety is how to handle reduction at the type level.  Here's a start of a two-place relation for well-typed in Coq:

Require Import Coq.Lists.List.
Reserved Infix "@" (left associativity, at level 11).
Local Open Scope list_scope.

Inductive expr {var : Set} : Set :=
| Var (v : var)
| U : expr
| Pi (s : expr) (d : var -&gt; expr)
| Abs (tx : expr) (f : var -&gt; expr)
| App (f x : expr).
Declare Scope expr_scope.
Delimit Scope expr_scope with expr.
Infix "@" := App : expr_scope.

Inductive wf {var1 var2} : list ((@expr var1 (* t1 *)) * var1 * (@expr var2) (* t2 *) * var2) -&gt; @expr var1 (* t1 *) -&gt; @expr var1 -&gt; @expr var2 (* t2 *) -&gt; @expr var2 -&gt; Prop :=
| wf_Var {G t1 v1 t2 v2} : List.In (t1, v1, t2, v2) G -&gt; wf G t1 (Var v1) t2 (Var v2)
| wf_U {G} : wf G U U U U
| wf_Pi {G s1 s2 d1 d2}
  : wf G U s1 U s2
    -&gt; (forall v1 v2,
           wf ((s1, v1, s2, v2) :: G)
              U (d1 v1) U (d2 v2))
    -&gt; wf G U (Pi s1 d1) U (Pi s2 d2)
| wf_Abs {G s1 s2 d1 d2 f1 f2}
  : wf G U s1 U s2
    -&gt; (forall v1 v2,
           wf ((s1, v1, s2, v2) :: G)
              (d1 v1) (f1 v1) (d2 v2) (f2 v2))
    -&gt; wf G (Pi s1 d1) (Abs s1 f1) (Pi s2 d2) (Abs s2 f2)
| wf_App {G s1 d1 s2 d2 f1 x1 f2 x2}
  : wf G (Pi s1 d1) f1 (Pi s2 d2) f2
    -&gt; wf G s1 x1 s2 x2
    -&gt; wf G (App (Abs s1 d1) x1) (App f1 x1) (App (Abs s2 d2) x2) (App f2 x2)
| wf_App_nd {G s1 d1 s2 d2 f1 x1 f2 x2}
  : wf G (Pi s1 (fun _ =&gt; d1)) f1 (Pi s2 (fun _ =&gt; d2)) f2
    -&gt; wf G s1 x1 s2 x2
    -&gt; wf G d1 (App f1 x1) d2 (App f2 x2).