NOTE: Lambda Cube
First we have UTLC(untyped lambda calculus) to STLC(simply typed lambda calculus), by adding arrow type(\(\to\)): \(\lambda x:Nat.x\)
1. Lambda cube
Lambda cube starts from STLC.
1.1. STLC -> \(\lambda 2\)
Terms depend on Types: \(\lambda (a : *).\lambda (x:a).x\)
1.2. \(\lambda 2\) -> \(\lambda \omega\)
Types depend on Types: \(\lambda (a : *).a \to a\)
1.3. \(\lambda 2\) -> \(\lambda \Pi\) (\(\Pi\) type)
Types depend on Terms: \(\Pi (x : a).M\)
1.4. COC(calculus of construction)
Mix \(\Pi\) and \(\lambda\), type is term.
COC = \(\lambda 2\) + \(\lambda \omega\) + \(\lambda \Pi\)
1.5. CIC(calculus of inductive construction)
Introduce Inductive, e.g. data Nat = zero | suc Nat
CIC = COC + Inductive