let a : Type = 1;
let b : Type = 1;

-- Arrows are equivalent to \Pi _: a. b
let f : a -> b = \lambda x . x;

-- Asterisks are equivalent to \Sigma _: a. b
let p : a * b = 0, 0;

-- You can ask the compiler to infer the type directly
const infer_my_type = 1, 1;