From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 7 Sep 2016 23:34:37 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> <143ade6b-1b68-36fe-a765-c54d9f6fac8c@googlemail.com> Subject: Re: [HoTT] A puzzle about "univalent equality" MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_201_1131443538.1473316477107" ------=_Part_201_1131443538.1473316477107 Content-Type: multipart/alternative; boundary="----=_Part_202_416924802.1473316477107" ------=_Part_202_416924802.1473316477107 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit True, the language does not provide this structure. But that doesn't mean it isn't in the model. Is there a problem interpreting ITT as all Zermelo-style sets, with identity as a subsingletons for equality? On Thursday, September 8, 2016 at 12:15:13 AM UTC-4, Michael Shulman wrote: > > Does "Zermelo-style set-theoretic equality" even make sense in MLTT? > Types don't have the global membership structure that Zermelo-sets do. > > On Wed, Sep 7, 2016 at 4:18 PM, Matt Oliveri > wrote: > > On Tuesday, September 6, 2016 at 6:14:24 PM UTC-4, Martin Hotzel Escardo > > wrote: > >> > >> Some people like the K-axiom for U because ... (let them fill the > answer). > > > > > > It allows you to interpret (within type theory) the types of ITT + K as > > types of U, and their elements as the corresponding elements. > (Conjecture?) > > Whereas without K, we don't know how to interpret ITT types as types of > U. > > In other words, K is a simple way to give ITT reflection. > > > >> Can we stare at the type (Id U X Y) objectively, mathematically, say > >> within intensional MLTT, where it was introduced, and, internally in > >> MLTT, ponder what it can be, and identify the only "compelling" thing > it > >> can be as the type of equivalences X~Y, where "compelling" is a notion > >> remote from univalence? > > > > > > How does Zermelo-style set-theoretic equality get ruled out as a > potential > > "compelling" meaning for identity? Of course, there's a potential > argument > > about what "compelling" ought to be getting at. You seem to not consider > > set-theoretic equality compelling, which I can play along with. > ------=_Part_202_416924802.1473316477107 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 7bit
True, the language does not provide this structure. But that doesn't mean it isn't in the model. Is there a problem interpreting ITT as all Zermelo-style sets, with identity as a subsingletons for equality?

On Thursday, September 8, 2016 at 12:15:13 AM UTC-4, Michael Shulman wrote:
Does "Zermelo-style set-theoretic equality" even make sense in MLTT?
Types don't have the global membership structure that Zermelo-sets do.

On Wed, Sep 7, 2016 at 4:18 PM, Matt Oliveri <atm...@gmail.com> wrote:
> On Tuesday, September 6, 2016 at 6:14:24 PM UTC-4, Martin Hotzel Escardo
> wrote:
>>
>> Some people like the K-axiom for U because ... (let them fill the answer).
>
>
> It allows you to interpret (within type theory) the types of ITT + K as
> types of U, and their elements as the corresponding elements. (Conjecture?)
> Whereas without K, we don't know how to interpret ITT types as types of U.
> In other words, K is a simple way to give ITT reflection.
>
>> Can we stare at the type (Id U X Y) objectively, mathematically, say
>> within intensional MLTT, where it was introduced, and, internally in
>> MLTT, ponder what it can be, and identify the only "compelling" thing it
>> can be as the type of equivalences X~Y, where "compelling" is a notion
>> remote from univalence?
>
>
> How does Zermelo-style set-theoretic equality get ruled out as a potential
> "compelling" meaning for identity? Of course, there's a potential argument
> about what "compelling" ought to be getting at. You seem to not consider
> set-theoretic equality compelling, which I can play along with.
------=_Part_202_416924802.1473316477107-- ------=_Part_201_1131443538.1473316477107--