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
Legal notice, Privacy policy
