If you don't mind the proposition living in a higher universe, then 
certainly the impredicative encoding will do:

P\/Q  :=  ∏(X:U) isProp(X) -> (P -> X) -> (Q -> X) -> X

satisfies

P -> P\/Q
Q -> P\/Q
isProp(R) -> (P->R) -> (Q->R) -> (P\/Q -> R)

Best,
Andrew

On Tuesday, May 2, 2017 at 12:45:41 PM UTC-4, Martin Hotzel Escardo wrote:
>
> 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 
>