Here are some more atomic types, this time denoted in a more category theory way:
Type  Term  

0  ⊥  empty type (initial) 
1  ⊤  unit type (terminal) 
2  True False 
boolean 
Empty Type
Denoted 'empty' or 0 or bottom or __ .
We cannot introduce a term. If we do have a term then we can prove any other type. So we have no arrows in but we have arrows going out to every other type. 
as a negative type:
Notation
Rules
Types are defined by their formation, term introduction, term eliminator and computation rules:
Empty Type 


formation rule It exists 


term introduction rule 
There is no introduction rule  
term eliminator 


computation rule  There is no computation rule  
Local completeness rule 
mplemetations of Empty
Idrisfrom : Idrisdev/libs/prelude/Builtins.idr 
 The empty type, also known as the trivially false proposition.   Use `void` or `absurd` to prove anything if  you have a variable of type `Void` in scope. data Void : Type where  The eliminator for the `Void` type. void : Void > a 
from : coq/theories/Init/Datatypes.v 
(** [Empty_set] is a datatype with no inhabitant *) Inductive Empty_set : Set :=. 
Unit Type
Denoted 'unit' or 1 or top or T .
Unit is always true, we can introduce a term without any additional information. There is a sense that this is the inverse of the empty type:

The term of the unit type is thought of as the null tuple (). This is because of the way that it works with the product type:
(x,()) =_{β} (x)
In computing this equality does not hold exactly, however it is true upto isomorphism (or upto beta equality), that is, both sides of the equation contain the same information.
Can we use unit type to build enumeration types? Example 2=1+1. That would be more like a tuple with one element? unit(C)? which does not seem to be what we have here?
In the propositionsastypes approach the unit type corresponds to 'mere' propositions are the propositions in classical logic. This allows us to use the law of excluded middle when appropriate (for setlike structures).
The 'unit' type, in homotopy collapses to a point so, in that way, it is the most fundamental type.
Unit Type 


formation rule Unit type exists and does not depend on anything. 


term introduction rule Unit is always true, we can introduce a term without any additional information. 


term eliminator p:unit /\ c = c If we know how to produce a C using all the possible inputs that can go into a unit, then we can produce a C from any unit. 


computation rule When we evaluate the eliminator on a term of canonical form, we obtain the data that went into the eliminator associated with that form 


Local completeness rule 
Implemetations of Unit
Idrisfrom : Idrisdev/libs/prelude/Builtins.idr 
 The canonical singleelement type, also known as the trivially  true proposition. data Unit =  The trivial constructor for `()`. MkUnit 
from : coq/theories/Init/Datatypes.v 
(** [unit] is a singleton datatype with sole inhabitant [tt] *) Inductive unit : Set := tt : unit. 
2 (bool)
A set with two elements. This is the data type of Boolean algebra). It is like sum (either) where the terms are not necessarily types.
Unit Type 


formation rule Unit type exists and does not depend on anything. 


term introduction rule Lets call the two elements 'true' and 'false' as tends to be used in Boolean algebra. There is one constructor for each of these. 


term eliminator Like sum (either) the deconstructor requires a type 'C' and map a map from each of the elements to C. In practice we can implement this as a casestatement or even an ifthenelse. 


computation rule There are 2 equalities, one for 'false' and one for 'true' 


Local completeness rule 
Next Steps
Other types are discussed on the following pages: