λ(T : Type) → { a : Bool, b : T }