P. Aczel and M. Rathjen. Notes on constructive set theory. Technical Report 40, Institut Mittag-Leffler, 2001.
 P. Aczel and M. Rathjen. Notes on constructive set theory. Book draft available at http://www1.maths.leeds.ac.uk/~rathjen/book.pdf, 2010.
 P. Choudhury. Constructive representation of nominal sets in agda. Master's thesis, Robinson College, University of Cambridge, June 2015. Available at https://www.cl.cam.ac.uk/~amp12/agda/choudhury/choudhury-dissertation.pdf.
 A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013.
 A. M. Pitts. Nominal presentation of cubical sets models of type theory. In H. Herbelin, P. Letouzey, and M. Sozeau, editors, 20th International Conference on Types for Proofs and Programs (TYPES 2014), Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
 M. Rathjen. Realizability for constructive Zermelo-Fraenkel set theory. In V. Stoltenberg-Hansen and J. Va¨a¨n¨anen, editors, Logic Colloquium '03. Association for Symbolic Logic, 2006.
 A. W. Swan. An algebraic weak factorisation system on 01-substitution sets: a constructive proof. arXiv:1409.1829, September 2014.