An Agda development of set theory inside homotopy type theory.
Forked from Håkon Gylterud / hott-set-theory
