In the sequel we will present several extensions of type theory. To keep the presentation uniform we will however not use the logical framework presentation of type theory, but will use the same notation as in section 2.