Idempotents in intensional type theory

TL;DR

This paper investigates the properties of idempotents in intensional Martin-Löf type theory, revealing conditions under which they split or do not, and connecting ideas from higher category theory and homotopy theory.

Contribution

It demonstrates that not all idempotents split in plain MLTT and introduces the concept of fully coherent idempotents, formalized in Coq, linking higher category theory with type theory.

Findings

Existence of non-splitting idempotents under univalence and propositional truncation

Splitting of idempotents depends on an additional coherence condition under function extensionality

Construction of the type of fully coherent idempotents

Abstract

We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct "the type of fully coherent idempotents", by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.