We can look at types from a mathematical or a computing point of view.
Types in Computing
In computing we think of type as representing some type of data structure, this determines:
 How the memory is allocated to store the type.
 Type Safety  Allows checks to be made on what operations can be done on the data to provide some level of program validation.
See these pages for types as related to programming: 
Types in Mathematics
Types were originally added to set theory to try to resolve some paradoxes that arose. 
Type Theorys
Here are some atomic mathematical types with some examples of terms that may inhabit those types:
Type  Term  

Boolean  True False 

Natural Numbers  0,1,2...  
Real Numbers  0.582  
Set  a 
Type is a collection of terms having some common property.
Terms are values (or variables, or functions like the sum of other terms).
We can think of types as classifying values. If we know the type of somthing we have less information than knowing its value (and also its type). If we know a value without knowing its type, for example 0 (zero) we don't know if it is a natural number, or an integer, or a real number. Hence we don't know what operations might be valid to apply to it.
Types and terms are a similar (but different) concept to sets and elements. In both cases we think about it as a container relationship.
The ':' colon symbol is used to declare the type of a given term:
Type  Term  

M  x:M  typing declaration 
If the type is not declared, it can be inferred in some circumstances.
We can have a multiple level hierarchy of types. For instance, the type 'M' in the above table may itself have a type of 'Type' ( M:Type ). However giving all higher order types the type of 'Type' could theoretically lead to circular references and hence paradoxes. Some theories allow these 'Type's to be numbered to enforce a hierarchy of universes and prevent any circular references. (see kinds)
MartinLöf Type Theorys
These are 'constructive' type theories, that is, we can start with some atomic types as above and define compound types by building them up inductively.
There are a number of type theorys developed by Church, MartinLöf, etc. Such as:
 STT  Simple Type Theory.
 PTT  Polymorphic Type Theory.
 DTT  Dependent Type Theory.
We can start with some of the simpler ways of creating compound types.
Sum, Product and Exponent
A type theory with Sum, Product and Exponent type is related to a Cartesian Closed Category (CCC).
A term may be represented by some variable such as x,y... or a compound term using the following:
If 'M' and 'N' are valid terms, then the following are also valid terms:
Type  Term  

M[x]  We will use this notation to denote a term 'M' with multiple values depending on the value 'x'.  
Sum  A \/ B  <M,N>  This is a union of the two types. An instance will contain an instance of only one of the types. We can recover the contained types as follows:

Product  A /\ B  (M N)  This contains both of the types (like tuples) . An instance will contain an instance of all of the types. 
Exponent  A>B  λ x:M.N  This is a function from M to N. where x is an instance of 'M' and the function returns an instance of 'N' See lambda calculus. 
Where:
 M,N are terms, that is a base type or a compound type made up as some combination of the above. That is, they are inductively defined.
 x is an instance of 'M'
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 
Dependent Types
If 'M' and 'N' are valid type terms, then the following are also valid terms:
Type  Term  

Dependent Product  x:A>B  Πx:M.N[x] 

Dependent Sum  <x:A,B[x]>  Σx:M.N[x]  Strong sum type: expresses the concept of subset. 
Dependent Types in Programming
In the language 'Scala' we can define a type that is parameterised by another type (polymorphism) for instance:  List[T] 
This represents a list of any type, represented by 'T', for example a list of Integers or a list of boolean values.
However, Scala does not allow dependent products like say: Modulo[n:Integer] which would represent any modulo number system such as modulo 3 or modulo 27.
Dependent Types as Fibre Bundles.
The situation where a type depends on the value of another type is modeled by fibre bundles. We discuss fibre bundles on the page here. So a model of a vector category depends on its dimension: 
Type Theory and Logic
There are various approaches to this:
 CurryHoward correspondence.
 A logic is a logic over a type theory.
CurryHoward
There is a correspondence between constructive (intuitionistic) logic and propositional logic.
Constructive Logic  Type Theory  

proposition  type of its proofs  A proposition is true iff we have a proof of that proposition 
proof  an object of that type  
This does not work for more complicated type theorys and logics such as higher order logic.
Logic over a Type Theory
We treat logic as a metamathematics, that is a layer above the mathematics that allows us to apply axioms and rules to prove things about the mathematics.
Comprehension
Any collection of elements of the same type may form an object of the next higher type.
z'x[xz <> Φ(x)]
Concepts related to Type