Do you know why that is the case? Nominal logic is usually presented as a sheaf model (i.e., as the internal language of the Schanuel topos), which models a constructive dependent type theory. Is there a problem when constructing a universe?
I'm probably the wrong person to discuss this question with. I don't know more than I've written above. All I know about this is from conversations with Christian Urban, who implemented Nominal Isabelle. It was a while back, maybe the problem of implementing nominal techniques in constructive type theory in an effective way (i.e. doesn't put additional burden on automation) has been solved by now.
The problem as I understand it is this.
Let's say you have a theory T in the formal language given by
signature S.
- In HOL you extend T to T' and S to S', but the deltas between T and
T', and S and S' are small, and largely generic. This is possible
because almost everything handling nominal can be done using double
negation.
- In CoC you extend T to T' and S to S', but the deltas between T and
T', and S and S' are huge, and largely non generic.
