Type Theory Preliminaries

Accounts of Nuprl's type theory can be found in several sources [6][1][20][35][8].

• Basic Types
• Cartesian Products
• Function Types
• Propositions and Universes
• Subtypes and Finiteness
• Algebraic Structures and Dependent Types
• Reading Nuprl Proofs