What is the most intuitive dependent type theory I could learn? I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles on dependent typing.

Many type theory discussions seem to focus on adding incremental features to previous type systems, not "what's the next large generalization up from type system X?". Dependent types seem to be the next large generalization from System F, but I have yet to find the intuitive, canonical dependently typed language. The many references to Calculus of (inductive) Constructions makes me think CoC is that language, but the explanations of the language I have seen don't seem very clear or intuitive to me.

I am expecting/guessing such a language would have features like: (and please let me know if anything in particular jumps out as confused or unrealistic)


Generalized abstraction (can have functions from any domain in the type hierarchy to other, kind -> term, term->type''' etc.)
Has an infinite hierarchy of typing (terms : types : types' : types'' : ...)
A minimum number of basic elements. I am imagining that the language only asserts a single element for each level. For example it might assert that (() : Unit : Type : Type' : ...). Other elements are built from these elements. 
Sum and product types are derivable.


I am also looking for an explanation of that language which ideally would discuss:


The relationship between abstraction and quantification in that language. If they are not unified, then explain why they are not unified.
The infinite type hierarchy explicitly


I am asking this question because I want to learn dependent type theory but also because I want to put together a guide that, assuming a little CS background, teaches the use of and how to understand proof assistants and dependently typed languages.

(Cross posted to Reddit)
There are a few different ways of approaching this:


Dependent Type Theory.
This is probably not the easiest way of learning about dependent types, but you could look at the Calculus of Constructions papers and their variants, Pure Type Systems, and Martin Hofmann's article on the Syntax and Semantics of Dependent Types, for example.
Theorem proving. Firstly, take a look at my answer to a related question: How would I go about learning the underlying theory of the Coq proof assistant?. 
Programming with dependent types. Looking at recent languages with dependent types  such as Epigram or Agda or less recent ones such as Dependent ML and writing some programs will help solidify the ideas. Epigram, for example, is extremely clean in design. Another angle is to see how dependent types are implemented. One practical dependent type theory is $\Pi\Sigma$: Dependent Types without the sugar. Several PhD theses are devoted to programming with dependent type theory: Dan Licata's, Nils Anders Danielsson's, Ulf Norrel's, Susmit Sarkar's, among others. And of course there's Adam Chlipala's book, given in Marc Hamann's answer.


I'd be inclined to start with programming, before moving to using theorem proving, then start exploring the more theoretical issues.