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

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

On Sat, May 13, 2017 at 2:46 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> 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.

I should have said, a Boolean *extensive* coherent category.  Of
course, an arbitrary coherent category may not have all coproducts,
and if it has coproducts they may not be disjoint (e.g. the posetal
case).

>> 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