[TYPES] Unit types and Dependent Type Theory

[Aaron Gray]

I am wondering the origins of unit types proper, types with a single
non void value originate from Dependent Type Theory or where they
developed independently ?

Any papers, references, or explanations as to their origin would be
much appreciated.

Many thanks in advance,

Aaron
-- 
Aaron Gray

Independent Open Source Software Engineer, Computer Language
Researcher, Information Theorist, and amateur computer scientist.