We axiomatize hereditarily finite sets in constructive type theory and show that all models of the axiomatization are isomorphic. The axiomatization takes the empty set and adjunction as primitives and comes with a strong induction principle. Based on the axiomatization, we construct the set operations of ZF and develop the basic theory of finite ordinals and cardinality. We construct a model of the axiomatization as a quotient of an inductive type of binary trees. The development is carried out in Coq.

- Paper, ITP 2016 (Slides ITP 2016; Slides Tallinn 2016)
- Browse Coq formalisation (Coq 8.5)
- Download Coq sources (compile with Coq 8.5)