## References * [[nLab:Erik Palmgren]], _Bishop's set theory_ (2005) ([pdf](http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/palmgren.pdf)) {#Palmgren05} * [[nLab:Erik Palmgren]], _Constructivist and Structuralist Foundations: Bishop’s and Lawvere’s Theories of Sets_ (2009) ([web](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.158.8166)) The formalization of Bishop set is reviewed for instance in section 3 of * [[nLab:Thierry Coquand]], [[nLab:Arnaud Spiwack]], _Towards constructive homological algebra in type theory_ ([pdf](http://assert-false.net/arnaud/papers/Towards%20constructive%20homological%20algebra%20in%20type%20theory.pdf)) {#CoquandSpiwack}