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

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

Obviously the second side-remark overlooks the fact that we used
function extensionality to show that excluded middle implies the
existence of propositional truncations. Apologies. Hence the question of
whether hypothetical propositional truncations imply function
extensionality remains open (although I very much doubt that they do).
Martin

On 12/05/17 19:10, Martin Escardo wrote:
> On 02/05/17 20:04, Michael Shulman wrote:
>> Some thoughts:
>>
>> [...]
>>
>> - 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.
> 
> If you assume excluded middle (every proposition is empty or pointed),
> and function extensionality, then, as you know, every type X does have a
> propositional truncation, namely ¬¬X:=(X->0)->0.
> 
> The universal map is the evaluation map eta:X->¬¬X. If we have f:X->P
> for a proposition P, then we get ¬¬f:¬¬X->¬¬P by the functoriality of
> double-dualization. By excluded middle we have a map ¬¬P->P, which
> composed with ¬¬f gives a map f':¬¬X->P, which in turn establishes the
> universality of eta:X->¬¬X among maps of X into propositions (the
> uniqueness requirement relies on funext). Therefore, indeed, ¬¬X is the
> propositional truncation of X (or, more precisely, ¬¬X, together with
> eta:X->¬¬X and the extension procedure f |-> f' and its uniqueness give
> the propositional truncation of X).
> 
> (Side-remark. Conversely, if you forget the assumption of excluded
> middle, but remember the assumption of function extensionality, then the
> assumption that eta:X->¬¬X is the universal map of X into a proposition,
> for every X, implies excluded middle. (Exercise.) So, in general, the
> propositional truncation of X, if it exists, is wildly different from ¬¬X.)
> 
> 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?).
> 
> 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
>