# Kathrin Stark

## Research Immersion Lab: Hereditarily Finite Sets in Constructive Type Theory

**Author:** Kathrin Stark, joint work with Gert Smolka

**Advisor:** Prof. Dr. Gert Smolka

## Abstract

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

Kathrin Stark,
Thu Oct 27 17:33:19 2016