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

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

On 03/05/17 13:17, andrew....@gmail.com wrote:
> 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

Assuming funext to show that this is indeed a proposition.

This is equivalent to the large truncation of P+Q discussed in my
previous message. As I said, if a small truncation exists, it is
equivalent to the large truncation, which always exists for any type,
assuming funext.

Martin



> 
> 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
> 
> -- 
> You received this message because you are subscribed to the Google
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to HomotopyTypeThe...@googlegroups.com
> <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.