You know those "how to draw Bugs Bunny" art guides they used to include in children's art books? Where they begin with a circle with some guidelines and then do a whole bunch of stuff and the end result is Bugs Bunny? But you have no idea how they went from Point A to Point B? That's the same thing with Type Theory.

PROFESSOR: Well, you see, there are different objects, like strings and numbers, that are shaped differently, so we put them into different categories. Those are types! See how simple this is?

<a whole bunch of stuff later>

PROFESSOR: Now the endofunctor of the covariant types are jointly distributed under the free monoid, provided that the pullback doesn't reverberate the time fibration of the dependent type space.