Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy

Cover
Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy
Copyright
Preface
Contents
Chapter 1: A Path to a New Logic
	1.1 First Encounters
	1.2 Next Steps
	1.3 Encounters with Ordinary Language Philosophy
		Definitional Equality
		Propositional Equality
	1.4 Quadrature
	1.5 Conclusion
Chapter 2: Dependent Types
	2.1 The Need for Types
	2.2 The Analogy between Logic and Arithmetic
	2.3 Dependent Sum and ‘and’
	2.4 Dependent Types
	2.5 Context and Dependency Structure
	2.6 Events as Basic Types
	2.7 Revisiting the Philosophical Literature
Chapter 3: Homotopy Types
	3.1 Introduction
	3.2 HoTT Components
		3.2.1 Identity Types
		3.2.2 The Type Hierarchy
		3.2.3 The Univalence Axiom
		3.2.4 Higher Inductive Types
	3.3 Definite Description in Natural Language
		3.3.1 Definite Description for any Type
		3.3.2 Definite Description for Dependent Types
	3.4 The Structure of A
		3.4.1 Places in a Structure
		3.4.2 Types Equipped with Structure
		3.4.3 The Complex Numbers
	3.5 Conclusion
Chapter 4: Modal Types
	4.1 Modalities as Monads
	4.2 Towards Modal HoTT
		4.2.1 General Types
		4.2.2 First-order Modal Logic and Barcan
		4.2.3 Contexts and Counterfactuals
	4.3 Temporal Type Theory
	4.4 Mode Theory
Chapter 5: Spatial Types
	5.1 Introduction
	5.2 Current Geometry
	5.3 Regaining the Philosophy of Geometry
		5.3.1 Weyl: The Essence of Space
		5.3.2 Cassirer: Beyond Intuition
	5.4 Capturing Modern Geometry
	5.5 Geometry in Modal HoTT
	5.6 Simplicity and Representability in Modal HoTT
	5.7 Conclusion
Chapter 6: Conclusion
Further Reading
	Category Theory
	Type Theory
	Homotopy Type Theory
	Modal Type Theory
	Miscellaneous
References
Index