Re: [HoTT] Does MLTT have "or"?

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

On 03/05/17 15:48, stre...@mathematik.tu-darmstadt.de wrote:
>> What you are saying is that there is model where general propositional
>> truncations don't exist, but "or" does. Right?
> 
> yes
> 
>> How difficult is to get a model where "or" doesn't exist either?
> 
> depends on what "or" is! in my model Prop has or by impredicativity
> but this or doen't coincide with sums on the level of types.

I specified what "or" is in point (2) of the initial message of this thread:

(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.)

Here "proposition" means "type in which any two points are Id-equal".

Martin