Remark 4.1. Note that the word “set” in the logical framework does not coincide with the way it is used in Bishop’s constructive mathematics. To avoid this confusion, types together with equivalence relations are usually called “setoids” or “extensional sets” in intuitionistic type theory.