FOM: Challenge axioms, final draft

[Jaap van Oosten]

Colin,

to get nontriviality it's shorter (Important to Simpson!!)
just to require s \neq id (for s:N->N). No need to formally
require 1+1.

Cheers,

Jaap van Oosten