Lambda the Ultimate

A question from proggit:

"Is there a more, uh, layperson-oriented explanation of some of the concepts available? I'm trying to figure out how things work and I've got a good grasp of the simpler dependent type examples (like the second factorial function on the website) but the texts I've found assume knowledge of far too much terminology especially regarding the theorem proving and I can't really follow them."