Homotopy Type Theory: A synthetic approach to higher equalities

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)