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 
> <javascript:>> 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.
>