parsing error

[fblanqui]

I don't understand why I get a parsing error with:

def Set : Type.
injective {|τ|} : (Set -> Type).
def {|ℕ|} : Type.
def 0 : {|ℕ|}.
def {|𝑰|} (a:Set) : {|ℕ|} -> {|τ|} a.

[ERROR CODE:702]  [zo.dk] [line:5 column:42] 
Parsing error: Unexpected token '.'.