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

[Michael Shulman <shu...@sandiego.edu>]

Some thoughts:

- If in addition to function extensionality and propositional
extensionality we assume propositional resizing, then ||-|| is
constructible using the standard argument that an elementary topos is
a regular category.

- A model of MLTT with function extensionality but no universes is
given by any locally cartesian closed category (perhaps with
coproducts if we have binary sum types).  It seems that surely not
every lccc with coproducts is a regular category -- though I don't
have an example ready to hand, let alone an example that also has
universes.


On Tue, May 2, 2017 at 2:09 AM, 'Martin Escardo' via Homotopy Type
Theory <HomotopyT...@googlegroups.com> 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.
> For more options, visit https://groups.google.com/d/optout.