A Type Theory that assumes: Axiom of Extensionality Axiom of Regularity Axiom of Schema of Specification Axiom of Pairing Axiom of Union Axiom of Infinity Axiom of Schema of Replacement Axiom of Power Set Axiom of Choice