Unit is derived rather than primitive.

Thm*   Unit

Thm* a:Unit. a = 

There happen already to be other single element types. Propositions expressing equality and membership propositions are often represented as types that have a member iff they are true, and when they are true, the sole member is "*".
See Propositions

Def Unit == 0  

Def  == *

Thm* a:(0  ). a = *

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html