  This is the second in a series of papers extending Martin-L\"{o}f's meaning
explanation of dependent type theory to account for higher-dimensional types.
We build on the cubical realizability framework for simple types developed in
Part I, and extend it to a meaning explanation of dependent higher-dimensional
type theory. This extension requires generalizing the computational Kan
condition given in Part I, and considering the action of type families on
paths. We define identification types, which classify identifications (paths)
in a type, and dependent function and pair types. The main result is a
canonicity theorem, which states that a closed term of boolean type evaluates
to either true or false. This result establishes the first computational
interpretation of higher dependent type theory by giving a deterministic
operational semantics for its programs, including operations that realize the
Kan condition.
