Joseph Helfer: First-Order Homotopical Logic
Time: Wed 2019-05-01 10.00 - 11.45
Location: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University
Participating: Joseph Helfer, Stanford University
Abstract: Our story begins with the observation that the Voevodsky–Awodey–Warren–Kapulkin–Lumsdaine homotopical semantics for type theory can also be used to give a very simple semantics for (intuitionistic) first-order logic. We will describe a “functorial” formulation of these semantics using the framework of structured Grothendieck fibrations, by showing that the fibration obtained by taking the fiberwise-homotopy-category of the codomain fibration over a (suitable) model category C has the structure needed to interpret intuitionistic first-order logic. We will then describe an abstract result about such structured fibrations which implies a “homotopy-invariance” property for the homotopical semantics. To do this, we must make sense of the notion “homotopy-equivalent structures” in the general context of the “fibrational” semantics. This leads us to describe a 2-categorical structure which is automatically present on the base category of a fibration (satisfying certain mild assumptions) — the 2-cells between f and g being “proofs (in the sense of the fibration) that f and g are equal — which in the case of interest recovers the usual 2-category of spaces.