> 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?

I am not sure what you mean by internally, but the way I usually motivate
univalence is: we can ask "which equalities (Id U X Y) are provable in
MLTT?"  The answer is: "only when X and Y are definitionally equal."  We
can ask: "when can we prove that (Id U X Y) is absurd?"  The answer turns
out to be: "exactly when X and Y are provably not isomorphic."  (The proof
that this is the most general answer is the proof that univalence is
consistent.)  So it seems natural to ask about the two extremes.  On the
one hand, the converse of the strictest equality we can have is the
equality reflection rule.  On the other extreme, the inverse of the weakest
equality rule is logically equivalent to univalence.

On Wed, Sep 7, 2016, 9:15 PM Michael Shulman <shu...@sandiego.edu> 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.
>
> --
> 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.
>