  Bishop's informal set theory is briefly discussed and compared to Lawvere's
Elementary Theory of the Category of Sets (ETCS). We then present a
constructive and predicative version of ETCS, whose standard model is based on
the constructive type theory of Martin-L\"of. The theory, CETCS, provides a
structuralist foundation for constructive mathematics in the style of Bishop.
