  The axiom of extensionality is a common feature of all the systems discussed so far. However, in a context in which the computational content of a statement is considered to be crucial, an intensional theory might be more appropriate. For example, constructive type theory and explicit mathematics both encapsulate some form of intensionality. Intuitionistic set theories without extensionality have been considered in the literature (Friedman 1973a, Beeson 1985).  Their motivation, however, has been not computational but technical in nature, due to the difficulties that extensionality  brings about when studying metamathematical properties of intuitionistic set  theories. 