Homotopy Type Theory: A synthetic approach to higher equalities

TL;DR

This paper introduces Homotopy Type Theory and Univalent Foundations, presenting a synthetic approach to understanding higher equalities in mathematics and logic, aimed at philosophers and foundational researchers.

Contribution

It provides an accessible introduction to Homotopy Type Theory and Univalent Foundations, emphasizing their significance for philosophical and foundational studies.

Findings

Introduces Homotopy Type Theory as a new foundation for mathematics

Explains the concept of higher equalities in a synthetic framework

Highlights the relevance of Univalent Foundations for philosophical inquiry

Abstract

This is an introduction to Homotopy Type Theory and Univalent Foundations for philosophers, written as a chapter for the book "Categories for the Working Philosopher" (ed. Elaine Landry)