We compare three categorical models of type theory with extensional constructs: setoids over extensional type theory; setoids over intensional type theory and a certain free exact category (the free '?W-pretopos'). By studying the amount of choice available in these categories, we are able show that they are distinct.