Kathrin Stark

Saarland University Computer Science

Research Immersion Lab: Hereditarily Finite Sets in Constructive Type Theory

Author: Kathrin Stark, joint work with Gert Smolka
Advisor: Prof. Dr. Gert Smolka


We discuss a categorical axiomatization of Hereditarily Finite Sets in constructive type theory with adjunction and the empty set as disjoint primitive operations. The type of sets is assumed to be discrete and we assume a recursor without equations given. Inside the theory we then define the usual set operations as union, the power set, transitive closure, separation, replacement, choice and cardinality. The axiomatization is isomorphic to a quotient of the inductive type of binary trees.
More information is available on the current project page .

Attached Documents

Legal notice, Privacy policy