From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.46.71.207 with SMTP id u198mr515952lja.2.1473308113359;
        Wed, 07 Sep 2016 21:15:13 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.46.69.7 with SMTP id s7ls42142lja.11.gmail; Wed, 07 Sep 2016
 21:15:12 -0700 (PDT)
X-Received: by 10.25.78.12 with SMTP id c12mr513392lfb.1.1473308112510;
        Wed, 07 Sep 2016 21:15:12 -0700 (PDT)
Return-Path: <shu...@sandiego.edu>
Received: from mail-lf0-x234.google.com (mail-lf0-x234.google.com. [2a00:1450:4010:c07::234])
        by gmr-mx.google.com with ESMTPS id 82si435332wmg.3.2016.09.07.21.15.12
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Wed, 07 Sep 2016 21:15:12 -0700 (PDT)
Received-SPF: neutral (google.com: 2a00:1450:4010:c07::234 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2a00:1450:4010:c07::234;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@sandiego-edu.20150623.gappssmtp.com;
       spf=neutral (google.com: 2a00:1450:4010:c07::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu
Received: by mail-lf0-x234.google.com with SMTP id u14so12306769lfd.1
        for <HomotopyT...@googlegroups.com>; Wed, 07 Sep 2016 21:15:12 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=sandiego-edu.20150623.gappssmtp.com; s=20150623;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to
         :cc;
        bh=iqnxcA1ManGTa910YkmKLRx82T6Y0RRhhwpxeE/wXRM=;
        b=R/AJLNNNvBbz90YLlabC3k0Ncv2pBE53JwKWQ2emTKBPlzoBUj93vJMNyPNmy0qaVT
         11e5kt/+W1F1ZuGYJWd/V+GMfyLjn2k2LZWtREYaTQoP99rHAfxkxY9HrBScUfUb/jsw
         DmiPK/rD3b4Kyly0PPKcqLXRe7JG3l/SmOM1qliNj3gPXIBFAovPXYhUD9MXnZJC/GJU
         4dSJHucDMLUdDO5mDvcggOOTpAMW1qUn79t9toUTbWXf6r2vuAnB9qoKbh5Ywc8+oAZ4
         UstNWDLkwFBtflGOrHDmElebmAKx8pQJSKZDVcRo3ctbyIwm2WJOVCdHecXV9piyqLtN
         xhgg==
X-Gm-Message-State: AE9vXwOJ3eO0Q5gPuZe09KXSkPzIzOFnbkVFRNysV5qLuAA7NmgyNogIDhvNkBos2JYYBiAo
X-Received: by 10.25.149.140 with SMTP id x134mr875348lfd.76.1473308111902;
        Wed, 07 Sep 2016 21:15:11 -0700 (PDT)
Return-Path: <shu...@sandiego.edu>
Received: from mail-lf0-f51.google.com (mail-lf0-f51.google.com. [209.85.215.51])
        by smtp.gmail.com with ESMTPSA id s62sm7238745lja.7.2016.09.07.21.15.11
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Wed, 07 Sep 2016 21:15:11 -0700 (PDT)
Received: by mail-lf0-f51.google.com with SMTP id l131so12253073lfl.2
        for <HomotopyT...@googlegroups.com>; Wed, 07 Sep 2016 21:15:11 -0700 (PDT)
X-Received: by 10.25.44.142 with SMTP id s136mr700856lfs.156.1473308110633;
 Wed, 07 Sep 2016 21:15:10 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.25.149.14 with HTTP; Wed, 7 Sep 2016 21:14:50 -0700 (PDT)
In-Reply-To: <a88b7834-5ce8-47d6-803a-d2a98ed27084@googlegroups.com>
References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com>
 <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> <CABcT7WBZo8bt6dtfDowd2nOYrtLPwsCC4Yxara1sZ5_oHeUQFw@mail.gmail.com>
 <CAOvivQwgfVzH9N_JhgdjB4KC5+LmMEjAJpO-mKo_Mm70OOgr4w@mail.gmail.com>
 <CAAkwb-mYObk7m+FwBosiPcbm9p7mo2z5Lw-3LUtg4Di2X-pYxg@mail.gmail.com>
 <CABcT7WDg9P8GcAfihWz4mF-upkzzo1sjneax2nKedutMHUpzzg@mail.gmail.com>
 <143ade6b-1b68-36fe-a765-c54d9f6fac8c@googlemail.com> <a88b7834-5ce8-47d6-803a-d2a98ed27084@googlegroups.com>
From: Michael Shulman <shu...@sandiego.edu>
Date: Wed, 7 Sep 2016 21:14:50 -0700
X-Gmail-Original-Message-ID: <CAOvivQxFDPaVL0iwDR=sBMWa+Zmh56jatW...@mail.gmail.com>
Message-ID: <CAOvivQxFDPaVL0iwDR=sBMWa+Zmh56jatW24-Bv7n0ar4FvaSA@mail.gmail.com>
Subject: Re: [HoTT] A puzzle about "univalent equality"
To: Matt Oliveri <atm...@gmail.com>
Cc: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: text/plain; charset=UTF-8

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.