How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)? For systems without dependent types, like Hindley-Milner type system, the types correspond to formulas of intuitionistic logic. There we know that its models are Heyting algebras, and in particular, to disprove a formula, we can restrict to one Heyting algebra where each formula is represented by an open subset of $\mathbb{R}$.

For example, if we want to show that $\forall\alpha.\alpha\lor(\alpha\rightarrow\bot)$ is not inhabited, we construct a mapping $\phi$ from formulas to open subsets of $\mathbb{R}$ by defining:
\begin{align}
\phi(\alpha) &amp;= (-\infty, 0)
\end{align}
Then
\begin{align}
\phi(\alpha\rightarrow\bot) &amp;= \mbox{int}( [0, \infty) ) \\ &amp; = (0,\infty) \\
\phi(\alpha\lor(\alpha\rightarrow\bot)) &amp;= (-\infty, 0) \cup (0,\infty) \\
  &amp;= \mathbb{R} \setminus {0}.
\end{align}
This shows that the original formula cannot be provable, since we have a model where it's not true, or equivalently (by Curry-Howard isomorphism) the type cannot be inhabited.

Another possibility would be to use Kriepke frames.



Are there any similar methods for systems with dependent types? Like some generalization of Heyting algebras or Kripke frames?

Note: I'm not asking for a decision procedure, I know there cannot be any. I'm asking just for a mechanism that allows to witness unprovability of a formula - to convince someone that it's unprovable.
That a formula is not provable can essentially be done in two ways. With some luck we might be able to show within type theory that the formula implies one which is already known to be not provable. The other way is to find a model in which the formula is invalid, and this can be quite hard. For example, it took a very long time to find the groupoid model of dependent type theory, which was the first to invalidate uniqueness of identity proofs.

The question "what is a model of dependent type theory?" has a somewhat complicated answer. If you ignore certain properties of substitution, a model is a locally cartesian closed category, and that might be the simplest answer. If you want a "real" model, then there are several options, see the nLab page on categorical models of dependent type theory. In any case, the answer is always a bit complicated because dependent type theory is a fairly complex formal system.

If I were to suggest just one article on the subject, I would probably recommend the original paper by Robert Seely, "Locally cartesian closed categories and type theory". If I were to suggest another one, it would probably be one that explains what needs to be corrected in Seely's paper, e.g., Martin Hoffman's "On the Interpretation of Type Theory in Locally Cartesian Closed Categories".

A recent important advance in this area is the realization that homotopy-theoretic models are also models of dependent type theory, see homotopytypetheory.org references. This provides a wealth of possibilities, but one must now learn homotopy theory to get hands on the models.