
Extensional Constructs in Intensional Type Theory
Martin Hofmann(Author)
Springer (Publisher)
Published on 23. May 1997
Book
Hardback
XII, 216 pages
978-3-540-76121-1 (ISBN)
Description
Extensional Constructs in Intensional Type Theory
presents a novel approach to the treatment of equality in Martin-Loef type theory (a basis for important work in mechanised mathematics and program verification). Martin Hofmann attempts to reconcile the two different ways that type theories deal with identity types. The book will be of interest particularly to researchers with mainly theoretical interests and implementors of type theory based proof assistants, and also fourth year undergraduates who will find it useful as part of an advanced course on type theory.
More details
Series
Edition
1st Edition.
Language
English
Place of publication
London
United Kingdom
Publishing group
Springer Berlin
Target group
College/higher education
Professional and scholarly
Research
Illustrations
biography
Dimensions
Height: 23.5 cm
Width: 15.5 cm
Weight
505 gr
ISBN-13
978-3-540-76121-1 (9783540761211)
DOI
10.1007/978-1-4471-0963-1
Schweitzer Classification
Other editions
Additional editions

Martin Hofmann
Extensional Constructs in Intensional Type Theory
E-Book
12/2012
Springer
€139.09
Available for download

Martin Hofmann
Extensional Constructs in Intensional Type Theory
Book
09/2011
Springer
€149.79
Shipment within 15-20 days
Content
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.