From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 7 Sep 2016 16:18:33 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: <143ade6b-1b68-36fe-a765-c54d9f6fac8c@googlemail.com> 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_5076_1984120461.1473290313607" ------=_Part_5076_1984120461.1473290313607 Content-Type: multipart/alternative; boundary="----=_Part_5077_2040261928.1473290313616" ------=_Part_5077_2040261928.1473290313616 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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_5077_2040261928.1473290313616 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 7bit
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_5077_2040261928.1473290313616-- ------=_Part_5076_1984120461.1473290313607--