  A model of Martin-L\"of extensional type theory with universes is formalized
in Agda, an interactive proof system based on Martin-L\"of intensional type
theory. This may be understood, we claim, as a solution to the old problem of
modelling the full extensional theory in the intensional theory. Types are
interpreted as setoids, and the model is therefore a setoid model. We solve the
problem of intepreting type universes by utilizing Aczel's type of iterative
sets, and show how it can be made into a setoid of small setoids containing the
necessary setoid constructions.
  In addition we interpret the bracket types of Awodey and Bauer. Further
quotient types should be interpretable.
