yet another learn on dependent type

dependent type is actually a type that depend on a value. There are three level of dependent type:

1. first order, include the dependent product type into simple typed lamda calculus. this make it to be system LF
2. second order , allow quantification over type constructor
3. higher order, this allow all four forms of abstraction from the lambda cube: functions from terms to terms, types to types, terms to types and types to terms. The system corresponds to the Calculus of constructions.this is coq now.