let a: Πx: bool. bool = λx. x; -- Pi, lambda let b: bool ✖ bool × bool = (1, 1, 1); -- Multiplication, both OK let c: Σx: bool. bool = bla; -- Sigma let d: bool → bool = split { True _ ⇒ False 0 | False _ ⇒ True 0 }; -- Arrows