Hereditarily finite sets in constructive type theory

Gert Smolka

Fachrichtung Informatik
Universität des Saarlandes, Saarbrücken

Wednesday, 31 August 2016, 16:00 (note the unusual weekday and time)
Cybernetica Bldg (Akadeemia tee 21), room B101


Slides from the talk [pdf]

Abstract: 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.

The talk is based on joint work with Kathrin Stark published in Proc. of ITP 2016.


Tarmo Uustalu
Last update 9 September 2016