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