1  λ(a : Type) → λ(b : Type) → { _1 : a, _2 : b }