On 2011-04-08 13:02, Jean-Philippe Bernardy wrote: > syntax Σ A (λ x → B) = Σ[ x ∶ A ] B Note that the character which may look like a colon is /not/ the ASCII colon character, it is U+2236 (RATIO). If you are using the Agda input method, then you can insert this character by typing \:. -- /NAD