let a : U = 1;
let b : U = 1;
let f : a -> b = \lambda x . x;
-- Arrows are equivalent to \Pi _: a. b
let p : a * b = 0, 0;
-- Arteries are equivalent to \Sigma _: a. b
const infer_my_type = 1, 1;
-- You can ask the compiler to infer the type directly