Does MLTT have "or"?

[Martin Escardo <escardo...@googlemail.com>]

Last week in a meeting I had a technical discussion with somebody, who
suggested to post the question here.

(1) Prove (internally) or disprove (as a meta-theorem, probably with a
counter-model) the following in (intensional) Martin-Loef Type Theory:

    * The poset of subsingletons (or propositions or truth values) has
      binary joins (or disjunction).

(We know it has binary meets and Heyting implication, which amounts to
saying it is a Heyting semilattice. Is it a lattice?)

(2) The question is whether given any two propositions P and Q we can
find a proposition R with P->R and Q->R such that for any proposition
R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of
P and Q.)

(3) Of course, if MLTT had propositional truncations ||-||, then the
answer would be R := ||P+Q||. But we can ask this question for MLTT
before we postulate propositional truncations as in (1)-(2).

(4) What is a model of intensional MLTT with a universe such that
||-|| doesn't exist?

More precisely, define, internally in intensional MLTT,

  hasTruncation(X:U) := Σ(X':U),
                            isProp(X')
                          × (X→X')
                          × Π(P:U), (isProp(P) × (X→P)) → (X'→P).

Is there a model, with universes, the falsifies this?

Preferably, we want models that falsify this but validate
function extensionality (and perhaps also propositional
extensionality).

Best,
Martin