Algebraic Type Theory, Part 1: Martin-Löf algebras

TL;DR

The paper develops an algebraic framework for dependent type theory by introducing Martin-Löf algebras (ML-algebras) within locally cartesian closed categories, showing how a map $\mathsf{u}: \dot{\mathsf{U}} \to \mathsf{U}$ equipped with structure for $1$, $\Sigma$, $\Pi$ (and Id-types) yields a polynomial endofunctor $\mathsf{P}_{\mathsf{u}}$ that coherently models type formers and substitution. Identity types are integrated via a Garner-style weak pullback construction, enabling extensional and intensional variants; examples include the subobject classifier and Hofmann–Streicher universes, illustrating how ML-algebras capture familiar type-theoretic semantics in an algebraic, Yoneda-friendly way. The core contribution connects ML-algebras to polynomial monads, providing a biequivalence with polynomial endofunctors and enabling a bicategorical treatment of polynomials, comprehension, and type equivalences through internal Equiv structures, univalence considerations, and a robust classification of maps. This framework unifies concepts from topos theory, algebraic set theory, and dependent type theory, offering a coherent, algebraic approach to coherence, substitution, and higher-type structure with potential for formalization in type-theoretic proof assistants. The results yield a concrete algebraic pathway to model and study dependent type theories with coherent operations and higher-dimensional equivalences, bridging categorical logic and type-theoretic semantics.

Abstract

A new algebraic treatment of dependent type theory is proposed using ideas derived from topos theory and algebraic set theory.

Theorems & Definitions (29)

• Definition 1
• Proposition 2: awodey:NMFiore:2012
• Lemma 3
• Definition 4
• Theorem 5
• Proposition 6
• proof
• Definition 7
• Definition 8
• Proposition 9