From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:90a:ba88:: with SMTP id t8mr17356920pjr.182.1589136980923; Sun, 10 May 2020 11:56:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:191c:: with SMTP id z28ls2916579pgl.11.gmail; Sun, 10 May 2020 11:56:19 -0700 (PDT) X-Received: by 2002:aa7:8743:: with SMTP id g3mr12837201pfo.218.1589136979365; Sun, 10 May 2020 11:56:19 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589136979; cv=none; d=google.com; s=arc-20160816; b=aTyeEIBXIOKXzRM39HoaB+zGBJzd7K2oaTF+Qh1MGKuLkPr6n1eXWMGGmF3udSKmOQ 7WgLaaCCC0O2EehvL3jDltGFqyfQAue3eBSTpGLzJ/6bQYc1a99PuiwwOOQwHZj7BmQ/ 879KDQAFVIWnzKtj/vMzIzhEY/kHCm2OP6jExldla+ZldxHVC+IgX/PIuhgBndUXVd2o Gtc+9RquYgz/6603woxf4K55qRFoLddEPykCp1vyNbry4RyekX9fKBwtseq07JeJRHie C+QL4k8D+D56hL2CDGdnoEJ4cSqd7oNvEo3l3B2vDmhXOI4QwCo/fqXAlceGg+h1N3LC DuBA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=9E+wlqnwHbjkpdTaxjQHr0NDCZbLwo9G8SE6TrLG2uE=; b=XLmbRVj4yGfmjbuS7OhwqxCD93gAcY7cSmTHypbDBeD4z50lrGeYcH/+EW+8F04K7/ VClfkxSNlNihGhEiqPIMXzSjVdjVLQhdr0vu2IOaUJKqRftV+JHZGfXCs6ThLMaVR+5F 0KxfgPxL2KMqwG9O689haa0p12l+oIVZS4iy0dzcnTEX9rmOsfYpmujEtxJ5bVqzlHvJ vqEPM4GngA1U848DDAOgBhOnjF1MbXqXQ/vH2qX7exF7WtJj8ZlOFEisljmGmXpKGT4+ P3NVomUQTrBcF7D5enCwgsYQf5JHBrGcJPfU+s5xA82L3gJgxbRhXndM07V4n8t/fipw ANpQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=C43iYERF; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::334 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-ot1-x334.google.com (mail-ot1-x334.google.com. [2607:f8b0:4864:20::334]) by gmr-mx.google.com with ESMTPS id z5si428504pgu.0.2020.05.10.11.56.19 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 11:56:19 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::334 as permitted sender) client-ip=2607:f8b0:4864:20::334; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=C43iYERF; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::334 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-ot1-x334.google.com with SMTP id t3so5807608otp.3 for ; Sun, 10 May 2020 11:56:19 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=9E+wlqnwHbjkpdTaxjQHr0NDCZbLwo9G8SE6TrLG2uE=; b=C43iYERFZEsmUjMrYig/xLj60w+qHgfstx2q1FNIFVVWH+owJc3Qo4k/CQC+dAF4BX ycahCdFwoDgxAsPyMnTJ+dwYUGCNPARZ/Zz1c/eUXyNH/g2i9ZB7iaQ+Wl/tF/fSacSr KSf/Kzp1g5ydNmzTKj02mi4EjK0kHk2vwHdc8i/lX1ZLQkSSlyHyY04/oefCsP7gpw5q SdREWKmhzYcKmtNqxxr1jXQPlhDipqLC9J+oobTc0upK5Q9djhgSeF3t1PFO/UZJNvm0 ElBxuYFA2Izdu9uwEKME6x4cdYi3ajhy9APCYk/zuhBCjwYbShr0ASLF5aamFbl8rkkG lPIQ== X-Gm-Message-State: AGi0PuabSbhRfZXGMKqNlysy4P5fhxLmXNYIVVguPNftuH2r/XD0SQi0 U+4jSj0Lnv12GUUWJ9po/Wns4C+0D+ZtEyshgx7pvYvAsVGxYg== X-Received: by 2002:a9d:7082:: with SMTP id l2mr9609336otj.361.1589136979044; Sun, 10 May 2020 11:56:19 -0700 (PDT) MIME-Version: 1.0 References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> <7b9eb7c9-040a-46e8-b470-28958f8d7713@googlegroups.com> In-Reply-To: <7b9eb7c9-040a-46e8-b470-28958f8d7713@googlegroups.com> From: Nicolai Kraus Date: Sun, 10 May 2020 19:56:07 +0100 Message-ID: Subject: Re: [HoTT] Identity versus equality To: Ulrik Buchholtz Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000022b0d005a54fc987" --00000000000022b0d005a54fc987 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Sun, May 10, 2020 at 4:35 PM Ulrik Buchholtz wrote: > No need to apologize: I know I was being slightly provocative by > juxtaposing a question about sets cover (SC) and a comment on 2-level typ= e > theory in this context, in order to provoke some discussion :-) > It worked :-) > Wouldn't you agree, however, that even though basic 2LTT is conservative > over HoTT, from a certain point of view, 2LTT privileges the =E2=80=9Cgro= und floor=E2=80=9D > exosets? In your very nice paper, https://arxiv.org/abs/1705.03307, you > decorate the inner (fibrant, endo-) types as special, and leave the > exotypes undecorated, privileging the latter. While from a user's > perspective, however, it's the (inner) types that are > standard/mathematical, and the exotypes that are special. > I think I see where you are coming from. But for me, decorating the inner types as special was simply a pragmatic choice, not a philosophical one. Since most/all statements in the paper are "proper" 2LTT, there are more exo- / outer types involved than endo- / inner ones. But as a user, one is interested in the fibrant types (and maybe even assumes that they coincide with the inner theory), and only adds some small exo-sprinkles like "exo-Nat is cofibrant"; then, it makes sense to decorate the exo-types instead, as e.g. in https://arxiv.org/abs/2004.06572 And maybe it would be less confusing if we did the same in the paper that you linked to. I'm not sure. > And regardless of the decorations, the mere fact that we bring in the > exoset level makes the theory harder to justify from the philosophical > position that general homotopy types are not reducible to sets. One can i= n > fact see the conservativity result as foundational reduction (in the sens= e > of https://math.stanford.edu/~feferman/papers/reductive.pdf section 5) > from a system justified by the principle that everything is based on sets > to a system justified by a framework where that isn't the case. > That's interesting, thanks for the link! > Another connection is that it seems it should be easier to find an axiom, > which might imply SC, that would allow us to construct the type of > semi-simplicial types, rather than such an axiom that doesn't imply SC. B= ut > I don't know any such axiom statable in book HoTT either way. > Good question. > BTW, you probably meant =E2=80=9Csimplicial set=E2=80=9D above. And yes, = that kind of > axiom would be the strongest expression of =E2=80=9Ceverything is based s= ets=E2=80=9D, and > it currently needs 2LTT to even be stated. > You're right, I meant "set". (Otherwise it'd be silly, a type X is the realization of the [fibrant replacement of] the constant presheaf X.) Nicolai > Cheers, > Ulrik > > -- > 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 HomotopyT...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/7b9eb7c9-040a-46e8-b= 470-28958f8d7713%40googlegroups.com > > . > --00000000000022b0d005a54fc987 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Sun, May 10, 2020 at 4:35 PM Ulrik Buc= hholtz <ulrikbu...@gmail.com= > wrote:
No need to apologize: I know I= was being slightly provocative by juxtaposing a question about sets cover = (SC) and a comment on 2-level type theory in this context, in order to prov= oke some discussion :-)

It work= ed :-)
=C2=A0
Wouldn't you agree, however, that even though= basic 2LTT is conservative over HoTT, from a certain point of view, 2LTT p= rivileges the =E2=80=9Cground floor=E2=80=9D exosets? In your very nice pap= er, https://= arxiv.org/abs/1705.03307, you decorate the inner (fibrant, endo-) types= as special, and leave the exotypes undecorated, privileging the latter. Wh= ile from a user's perspective, however, it's the (inner) types that= are standard/mathematical, and the exotypes that are special.

I think I see where you are coming from= . But for me, decorating the inner types as special was simply a pragmatic = choice, not a philosophical one. Since most/all statements in the paper are= "proper" 2LTT, there are more exo- / outer types involved than e= ndo- / inner ones. But as a user, one is interested in the fibrant types (a= nd maybe even assumes that they coincide=C2=A0with the inner theory), and o= nly adds some small exo-sprinkles like "exo-Nat is cofibrant"; th= en, it makes sense to decorate the exo-types instead, as e.g. in=C2=A0https://arxiv.org/abs/2004.06572

That's interesting, thank= s for the link!
=C2=A0
Another connection is that it= seems it should be easier to find an axiom, which might imply SC, that wou= ld allow us to construct the type of semi-simplicial types, rather than suc= h an axiom that doesn't imply SC. But I don't know any such axiom s= tatable in book HoTT either way.

Good question.
=C2=A0
BTW, you probably meant = =E2=80=9Csimplicial set=E2=80=9D above. And yes, that kind of axiom would b= e the strongest expression of =E2=80=9Ceverything is based sets=E2=80=9D, a= nd it currently needs 2LTT to even be stated.
<= div>
You're right, I meant "set". (Otherwise it= 'd be silly, a type X is the realization of the [fibrant replacement of= ] the constant presheaf X.)
=C2=A0
Nicolai
=

Cheers,
Ulrik

=

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyT...@googlegroups.com.
To view this discussion on the web visit ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/7b9eb7c9-040a-46e8-b470-= 28958f8d7713%40googlegroups.com.
--00000000000022b0d005a54fc987--