James Ladyman (Bristol): “The Hole Argument and Homotopy Type Theory”

Abstract: It has been argued that thinking in terms of univalent Homotopy Type Theory (HoTT) blocks the Hole Argument. Here’s a quick sketch of the argument: Very crudely, Univalence says that “Equivalence is Identity”. Since diffeomorphism is the equivalence relation on models, under Univalence all models in an equivalence class will be identified. Thus models related by the hole diffeomorphism will necessarily represent the same possible world. So no Hole Argument. In this talk I consider how this kind of argument might be made rigorous and whether it works. I argue that HoTT can be used to block the hole argument but that, contrary to what is some have claimed, it does not automatically do so.

James Ladyman is Professor of Philosophy at the University of Bristol, and former editor of the British Journal for the Philosophy of Science.