Re: [HoTT] A puzzle about "univalent equality"

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

Type theory does have set-theoretic models, of course.  But that
doesn't provide a notion of equality that makes sense *inside* MLTT,
compelling or otherwise.

On Wed, Sep 7, 2016 at 11:34 PM, Matt Oliveri <atm...@gmail.com> wrote:
> 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.
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.