1. Introduction. - 1. 1 Definitional and propositional equality. - 1. 2 Extensional constructs. - 1. 3 Method. - 1. 4 Applications. - 1. 5 Overview. - 2. Syntax and semantics of dependent types. - 2. 1 Syntax for a core calculus. - 2. 2 High-level syntax. - 2. 3 Further type formers. - 2. 4 Abstract semantics of type theory. - 2. 5 Interpreting the syntax. - 2. 6 Discussion and related work. - 3. Syntactic properties of propositional equality. - 3. 1 Intensional type theory. - 3. 2 Extensional type theory. - 3. 3 Related work. - 4. Proof irrelevance and subset types. - 4. 1 The refinement approach. - 4. 2 The deliverables approach. - 4. 3 The deliverables model. - 4. 4 Model checking with Lego. - 4. 5 Type formers in the model D. - 4. 6 Subset types. - 4. 7 Reinterpretation of the equality judgement. - 4. 8 Related work. - 5. Extensionality and quotient types. - 5. 1 The setoid model. - 5. 2 The groupoid model. - 5. 3 A dependent setoid model. - 5. 4 Discussion and related work. - 6. Applications. - 6. 1 Tarski's fixpoint theorem. - 6. 2 Streams in type theory. - 6. 3 Category theory in type theory. - 6. 4 Encoding of the coproduct type. - 6. 5 Some basic constructions with quotient types. - 6. 6 ? is co-continuousintensionally. - 7. Conclusions and further work. - A. 1 Extensionality axioms. - A. 2 Quotient types. - A. 3 Further axioms. - Appendix B. Syntax. - Appendix C. A glossary of type theories. - Appendix D. Index of symbols. Language: English