@book{SWP--2006--03,
author    ={Chad Edward Brown}
title     ={Dependently Typed Set Theory},
publisher ={{SEKI Publications}},
series    ={{SEKI-Working-Paper SWP--2006--03 (ISSN 1860--5931)}},
address   ={Saarland Univ.},
year      ={2006},
note      ={},
abstract  ={Dependently Typed Set Theory (DeTSeT) is untyped set theory encoded in a dependent type theory.
The dependent type theory includes proof irrelevance and a special
$\Sigma$-type between objects and proofs.  This allows one to create a ``class type''
from any predicate on the untyped universe of sets.
Given this rich type structure, one can represent partial functions as total functions
on the appropriately restricted domain.
Set theory can be encoded as a finite signature in the type theory.
Furthermore, the signature is essentially
second-order (in the $\lambda$-calculus sense).
We develop the basic theory of DeTSeT and a signature for Mathematics.
}}