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?
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.