Re: [HoTT] Re: Foundational question about a large set of small sets

[Martin Escardo <escardo.martin@gmail.com>]

Interesting, Ulrik and Mike. Thanks! Martin

On 28/02/2021 15:13, Michael Shulman wrote:
> Yes, that's it.  And I guess you are right about leaving out the
> endoequivalences at level 1.
> 
> On Sun, Feb 28, 2021 at 4:45 AM Ulrik Buchholtz
> <ulrikbuchholtz@gmail.com> wrote:
>>> One can then get a
>>> counter-model to "there merely exists a set that covers Set" with
>>> presheaves on X * 1.
>>
>>
>> This I didn't check. But couldn't we here instead appeal to homotopy canonicity? Since Set is a closed type, if there is a proof of the mere existence of a set cover of Set, we could extract a specific term for one, and then obtain a contradiction in the above model.
> 
> Sure, but it seems a bit overkill to appeal to a hammer like homotopy
> canonicity when a simple presheaf countermodel would suffice.
> (Although I suppose there may be people on this list to whom the
> opposite would seem true....)  The semantic argument is that in
> presheaves on any category with a terminal object, the terminal object
> is projective, and thus the "existence principle" holds: any closed
> type whose propositional truncation is true is already globally
> inhabited.  (Of course, the semantic proof of canonicity is similar,
> using projectivity of 1 in a gluing category.)
> 

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/b21281e6-2de2-c126-f139-b7df3107078f%40gmail.com.