Extending Homotopy Type Theory with Linear Type Formers

by Mitchell Riley

Abstract

Homotopy Type Theory allows us to reason about the homotopy theory of spaces in a type-theoretic language. Unfortunately, not all mathematical problems can be reduced to homotopy theory, so we would like to extend HoTT with tools that let us discuss extra structure that is present in particular models. The first example of this was Shulman’s Cohesive HoTT, where a couple of new unary type formers let us talk about “discrete” and “codiscrete” spaces, enabling a type theoretic proof of Brouwer’s Fixed Point Theorem. In this talk I will demonstrate an extension in a different direction: adding linear tensors and homs, with the aim of giving us a convenient way to manipulate “spectra”, the central objects of stable homotopy theory.

This is joint work with Dan Licata.

School of Computer and Cyber Sciences Augusta University