Homotopy-initial algebras in type theory

TL;DR

This paper introduces homotopy-initial algebras in type theory, providing a new perspective on inductive types through homotopy-theoretic and univalent foundations, and characterizes W-types as homotopy-initial algebras.

Contribution

It defines homotopy-initial algebras using a type-theoretic contractibility condition and characterizes W-types as instances of these algebras.

Findings

Homotopy-initial algebras are characterized by a contractibility condition.

W-types are shown to be equivalent to homotopy-initial algebras.

The approach replaces traditional category-theoretic universal properties.

Abstract

We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition which replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterises the types that are equivalent to W-types as homotopy-initial algebras.