/ Identity / Type
Type
1  λ(a : Type) → a