First-order homotopical logic

TL;DR

This paper develops a homotopy-theoretic interpretation of first-order logic using categorical methods, demonstrating homotopy invariance through advanced fibrational techniques inspired by Homotopy Type Theory.

Contribution

It introduces a novel categorical framework for interpreting first-order logic homotopically, extending existing theories with a new invariance proof based on 2-dimensional fibrations.

Findings

Homotopy invariance of the interpretation established

Categorical formulation using Grothendieck fibrations

Extension to 2-dimensional fibrations for invariance proof

Abstract

We introduce a homotopy-theoretic interpretation of intuitionistic first-order logic based on ideas from Homotopy Type Theory. We provide a categorical formulation of this interpretation using the framework of Grothendieck fibrations. We then use this formulation to prove the central property of this interpretation, namely homotopy invariance. To do this, we use the result from arXiv:1905.10690 that any Grothendieck fibration of the kind being considered can automatically be upgraded to a 2-dimensional fibration, after which the invariance property is reduced to an abstract theorem concerning pseudonatural transformations of morphisms into 2-dimensional fibrations.