An abstract set theory library for Agda. Explore it interactively here. Its key features are:
- it contains many standard constructions of set theory and various proofs
- the theory is axiomatic, so it can be instantiated by various models, e.g. lists or unary predicates
- decidability properties can depend on the model
The main objective of this library is to provide a set theory whose proofs are fairly standard while allowing for instantiations that can be used without extra overhead compared to non-dependently typed data structures. This is not true if sets are modeled as unary predicates for example, since for X : Set ℕ, properties such as 0 ∈ X are not decidable in general. If we call the property DecEq X → ∀ x X → Dec (x ∈ X) type-based decidability, then we have the following table of features of models:
| Model | Type-based decidability | Axiom of infinity | Axiom of finiteness |
|---|---|---|---|
| List | ✓ | ❌ | ✓ |
| Unary predicates | ❌ | ✓ | ❌ |