example.linear.p

let id : (0 A : Type) -> (1 _ : A) -> A = \A x. x;
let const : (0 A B : Type) -> (1 _ : A) -> (0 _ : B) -> A = \A B x y. x;

Type