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

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

On Fri, May 12, 2017 at 11:10 AM, Martin Escardo
<escardo...@googlemail.com> wrote:
> The above argument relies on having a universe (first, to formulate
> excluded middle and funext, and, second, to formulate and prove the
> universality of eta).
>
> *** What is the interaction (if any) of excluded middle with regularity,
> in your thought above? It seems to me that adding a universe is playing
> a role. It is different to say externally that all morphisms have
> images, than to say this internally using a universe (or am I wrong?).

Three replies:

1. I don't think the argument technically relies on having a universe.
LEM, funext, and the universality of eta are usually stated internally
by quantifying over a universe, but they can also be stated as rules
with type judgments as premises, and I believe the proof of
universality goes through as a derivation of one rule from others.

2. In general, saying something internally is different from saying it
externally, but I think that for images (and more generally for
universal properties that are stable under pullback and descent) there
is no difference.  In such cases saying it internally with a universe
is the same as saying it externally for the "universal case", which
implies its external truth in all other cases.  (You can also say it
"internally" without a universe using stack semantics.)

3. A Boolean coherent category automatically has a subobject
classifier, namely 1+1.  Thus, if it is also cartesian closed, it is
automatically a topos.

> A second side-remark is this, which I realized just now while writing
> this, although I have known the above for several years:
>
> We know that the addition of propositional truncations as a rule, with
> certain stipulated definitional equalities, as in the HoTT book, gives
> function extensionality.
>
> A number of us (including Nicolai and me), asked whether hypothetical
> propositional truncations (which cannot come with stipulated
> definitional equalities) also give funext.
>
> The above argument shows that hypothetical propositional truncations
> definitely cannot give function extensionality. For, if this were the
> case, excluded middle would also imply function extensionality. But we
> know that this is not the case.
>
> Best,
> Martin