I think calling the type of natural numbers ℕ instead of Natural is causing the confusion. Students would be less tempted to write {1,2} ⊆ Natural as the righ

I think calling the type of natural numbers ℕ instead of Natural is causing the confusion. Students would be less tempted to write {1,2} ⊆ Natural as the right side looks like a type name rather than a value . Haskell helps to maintain the distinction by using capitals for type names and lower case for variable names. I would seem natural to write: naturals :: Set Natural naturals = {0,1..} {1,2} ⊆ naturals