Constructive models of Martin-Löf type theory with extensionality I am trying to find a justification for homotopy type theory. Of course, I understand that there is value for certain types of mathematicians, but I would like to understand why computer scientists should bother with it. In my understanding, a constructive model of MLTT with extensionality would be satisfactory, but I would like to understand whether the higher structure is necessary. This comes down to the following question:
Does there exist a constructive model of Martin-Löf type theory satisfying 

  
*
  
*functional extensionality
  
*uniqueness of identity proofs (UIP)?
  

Alternatively, we could relax these conditions to something like

  
*
  
*a "weak" form of univalence (eg. univalence is only satisfied in a base universe, but not in some higher universe) or some other form of extensionality
  
*finitely truncated universes (ie. h-levels are bounded in each universe).
  

I suspect such a model satisfying the former conditions is not known to exist. However it seems more likely that weaker conditions like the latter might be possible.
 A: I'm not exactly sure what you think the difficulty is. Here are some (supersets of) models that come to mind, although I admit they're not super precise:


*

*Any constructive set theory that is a ΠW-pretopos with as many universes as you want in your type theory.

*Interpret types as setoids (type together with an equivalence relation) in a second type theory with the rest of the structure you want. Use point-wise equality for the pi type setoid.


In fact, Martin-löf has a variation of type theory, extensional type theory, that has extensional equality of functions and, necessarily, uniqueness of identity proofs (this is because the identity type gets 'reflected' back into the judgmental equality, rather than using something like the J rule, which kind of erases any structure). It's just as constructive as intensional type theory.
If you want something that looks more like intensional type theory, there was extensive work years ago on "Observational Type Theory" (OTT) by several people. The goal there was to have something that is recognizably like intensional type theory, in that it has something like the J rule for making use of identity proofs, but allow more extensional principles to be included in the identity type, like function extensionality. There was also a story for quotients and coinductive types, I believe. And it also had uniqueness of identity proofs, because that makes certain things 'easy.'
In fact, I think you can kind of see OTT as a precursor to cubical type theory (CTT). A major difference is that CTT is a lot more complicated because it doesn't have uniqueness of identity proofs, and has to have all sorts of constructions that make sure computationally relevant information is passed around and accessible in the identity types. OTT was able to get away without any of this, because any higher structure was intended to be crushed, so the main trick was to ensure that no one actually computationally depended on the value of an identity type. Instead CTT has to actually represent all this computationally relevant information.
Looping back to the models, people actually do #2 manually in e.g. Coq, using setoids to have the notion of 'equality' they actually want, when the intensional equality is not good enough. So obviously that is useful to some people.
However, if (as seems like might be implicit in your question) you think that homotopy/cubical type theory is useless to 'normal' computer scientists as long as there is an intensional type theory with function extensionality and UIP (and quotients, and ...), I think that's mistaken.
