Extensional Constructs in Intensional Type Theory

1. Introduction.- 1.1 Definitional and propositional equality.- 1.2 Extensional constructs.- 1.3 Method.- 1.3.1 The use of categorical models.- 1.3.2 Syntactic models.- 1.4 Applications.- 1.4.1 Application to machine-assisted theorem proving.- 1.5 Overview.- 2. Syntax and semantics of dependent types.- 2.1 Syntax for a core calculus.- 2.1.1 Raw syntax.- 2.1.2 Judgements.- 2.1.3 Notation.- 2.1.4 Derived rules and meta-theoretic properties.- 2.2 High-level syntax.- 2.2.1 Telescopes.- 2.2.2 Elements of telescopes and context morphisms.- 2.2.3 Definitions and substitution.- 2.3 Further type formers.- 2.3.1 Unit type.- 2.3.2 ?-types.- 2.3.3 Function and cartesian product types.- 2.3.4 The Calculus of Constructions.- 2.3.5 Universes.- 2.3.6 Quotient types.- 2.4 Abstract semantics of type theory.- 2.4.1 Syntactic categories with attributes.- 2.4.2 Type constructors.- 2.5 Interpreting the syntax.- 2.5.1 Partial interpretation.- 2.5.2 Soundness of the interpretation.- 2.6 Discussion and related work.- 3. Syntactic properties of propositional equality.- 3.1 Intensional type theory.- 3.1.1 Substitution.- 3.1.2 Uniqueness of identity.- 3.1.3 Functional extensionality.- 3.2 Extensional type theory.- 3.2.1 Comparison with Troelstra's presentation.- 3.2.2 Undecidability of extensional type theory.- 3.2.3 Interpreting extensional type theory in intensional type theory.- 3.2.4 An extension of TTI for which the interpretation in TTE is surjective.- 3.2.5 Conservativity of TTE over TTI.- 3.2.6 Discussion and extensions.- 3.2.7 Conservativity of quotient types and functional extensionality.- 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.3.1 Contexts.- 4.3.2 Families of specifications.- 4.3.3 Sections of specifications (deliverables).- 4.4 Model checking with Lego.- 4.4.1 Records in Lego.- 4.4.2 Deliverables in Lego.- 4.5 Type formers in the model D.- 4.5.1 Dependent products.- 4.5.2 Dependent sums.- 4.5.3 Natural numbers.- 4.5.4 The type of propositions.- 4.5.5 Proof irrelevance.- 4.5.6 Universes.- 4.6 Subset types.- 4.6.1 Subset types without impredicativity.- 4.6.2 A non-standard rule for subset types.- 4.7 Reinterpretation of the equality judgement.- 4.8 Related work.- 5. Extensionality and quotient types.- 5.1 The setoid model.- 5.1.1 Contexts of setoids.- 5.1.2 Implementing the setoid model S0 in Lego.- 5.1.3 Type formers in the setoid model.- 5.1.4 Propositions.- 5.1.5 Quotient types.- 5.1.6 Interpretation of quotient types in S0.- 5.1.7 A choice operator for quotient types.- 5.1.8 Type dependency and universes.- 5.2 The groupoid model.- 5.2.1 Groupoids.- 5.2.2 Interpretation of type formers.- 5.2.3 Uniqueness of identity.- 5.2.4 Propositional equality as isomorphism.- 5.3 A dependent setoid model.- 5.3.1 Families of setoids.- 5.3.2 Dependent product.- 5.3.3 The identity type.- 5.3.4 Inductive types.- 5.3.5 Quotient types.- 5.4 Discussion and related work.- 6. Applications.- 6.1 Tarski's fixpoint theorem.- 6.1.1 Discussion.- 6.2 Streams in type theory.- 6.3 Category theory in type theory.- 6.3.1 Categories in S0.- 6.3.2 Categories in S1.- 6.3.3 Discussion.- 6.4 Encoding of the coproduct type.- 6.4.1 Development in the setoid models.- 6.5 Some basic constructions with quotient types.- 6.5.1 Canonical factorisation of a function.- 6.5.2 Some categorical properties of S0.- 6.5.3 Subsets and quotients.- 6.5.4 Saturated subsets.- 6.5.5 Iterated quotients.- 6.5.6 Quotients and products.- 6.5.7 Quotients and function spaces.- 6.6 ? is co-continuous-intensionally.- 6.6.1 Parametrised limits of ?-chains.- 6.6.2 Development in TTE.- 6.6.3 Development in TTI.- 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.