It outlines a justification of case analysis for dependent families of types, sketching its translation into conventional type theory (with a slightly augmented definition of equality).
However, it is fairly short on theory, and rather longer on making the propaganda case for programming in this style.
For both these reasons: the title.
The two gentlemen bearing the title are the stars of this evening's performance. (If you're not reading this in the evening, close the curtains.) Allow me to introduce them...