I was doing some web searches to see if I could answer Todd Trimble’s questions here. As usual, instead of answers I found more papers to read and no time to read them.
On constructive set theory:
- Notes on Constructive Set Theory by Peter Aczel and Michael Rathjen. Aczel is the inventor of CZF, a constructive analogue of ZF.
- Programming in Martin-LÃ¶f’s Type Theory by Bengt NordstrÃ¶m, Kent Petersson, and Jan M. Smith. Martin-LÃ¶f’s Type Theory is apparently one of the few theories that is uncontroversially constructive.
- Predicative topos theory and models for constructive set theory by Benno van den Berg. This is a Ph.D. thesis that tries to weaken the notion of topos appropriately.
On realizability and the effective topos: