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.