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.