David Corfield Modal Homotopy Type Theory

A book that has appeared with Oxford University Press in 2020.

Modal homotopy type theory: The prospect of a new logic for philosophy.

Pages for each chapter will add further reflections.

Chapters

1. Chapter 1 A path to a new logic
2. Chapter 2 Dependent types, pdf
3. Chapter 3 Homotopy types
4. Chapter 4 Modal types
5. Chapter 5 Spatial types

Errata

p. 83 ‘Saying ‘There are $n$ $A$s’‘ should be ‘Saying ‘There are $2$ $A$s’’.

p. 85, final line: ‘or by designating an element, $\mathcal{U}$, by, say, $B$’ should be ‘or by designating an element of $\mathcal{U}$ by, say, $B$’

p. 86 ‘by the elimination rule for identity types, described in 3.1.1’ should be ‘by the elimination rule for identity types, described in 3.2.1’

Automorphisms of complex numbers.

Quadruple of adjunctions between $Top$ and $Set$.