Just a note, nowadays people tend to use : to denote the type of a value in type theory, while ∈ is used in set theory to denote that a value is a member of a set.