From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sun, 10 May 2020 08:35:17 -0700 (PDT) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <7b9eb7c9-040a-46e8-b470-28958f8d7713@googlegroups.com> In-Reply-To: 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> Subject: Re: [HoTT] Identity versus equality MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1205_1443226440.1589124917480" ------=_Part_1205_1443226440.1589124917480 Content-Type: multipart/alternative; boundary="----=_Part_1206_1038209094.1589124917480" ------=_Part_1206_1038209094.1589124917480 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Sunday, May 10, 2020 at 4:27:30 PM UTC+2, Nicolai Kraus wrote: > > I agree with Mike - sorry Ulrik :-) > For me, "everything is based on sets" would mean that every fibrant type= =20 > can be written as the realization of a (semi-) simplicial type, or=20 > something like this.=20 > No need to apologize: I know I was being slightly provocative by=20 juxtaposing a question about sets cover (SC) and a comment on 2-level type= =20 theory in this context, in order to provoke some discussion :-) Wouldn't you agree, however, that even though basic 2LTT is conservative=20 over HoTT, from a certain point of view, 2LTT privileges the =E2=80=9Cgroun= d floor=E2=80=9D=20 exosets? In your very nice paper, https://arxiv.org/abs/1705.03307, you=20 decorate the inner (fibrant, endo-) types as special, and leave the=20 exotypes undecorated, privileging the latter. While from a user's=20 perspective, however, it's the (inner) types that are=20 standard/mathematical, and the exotypes that are special. And regardless of the decorations, the mere fact that we bring in the=20 exoset level makes the theory harder to justify from the philosophical=20 position that general homotopy types are not reducible to sets. One can in= =20 fact see the conservativity result as foundational reduction (in the sense= =20 of https://math.stanford.edu/~feferman/papers/reductive.pdf section 5) from= =20 a system justified by the principle that everything is based on sets to a= =20 system justified by a framework where that isn't the case. Another connection is that it seems it should be easier to find an axiom,= =20 which might imply SC, that would allow us to construct the type of=20 semi-simplicial types, rather than such an axiom that doesn't imply SC. But= =20 I don't know any such axiom statable in book HoTT either way. BTW, you probably meant =E2=80=9Csimplicial set=E2=80=9D above. And yes, th= at kind of axiom=20 would be the strongest expression of =E2=80=9Ceverything is based sets=E2= =80=9D, and it=20 currently needs 2LTT to even be stated. Cheers, Ulrik ------=_Part_1206_1038209094.1589124917480 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
On Sunday, May 10, 2020 at 4:27:30 PM UTC+2, Nicolai Kraus= wrote:
I agree with Mike - sorry Ulrik :-)
For= me, "everything is based on sets" would mean that every fibrant = type can be written as the realization of a (semi-) simplicial type, or som= ething like this.=C2=A0

N= o 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 t= his context, in order to provoke some discussion :-)

Wouldn't you agree, however, that even though basic 2LTT is conserva= tive over HoTT, from a certain point of view, 2LTT privileges the =E2=80=9C= ground floor=E2=80=9D exosets? In your very nice paper, https://arxiv.org/a= bs/1705.03307, you decorate the inner (fibrant, endo-) types as special, an= d leave the exotypes undecorated, privileging the latter. While from a user= 's perspective, however, it's the (inner) types that are standard/m= athematical, and the exotypes that are special.

An= d regardless of the decorations, the mere fact that we bring in the exoset = level makes the theory harder to justify from the philosophical position th= at general homotopy types are not reducible to sets. One can in fact see th= e conservativity result as foundational reduction (in the sense of https://= math.stanford.edu/~feferman/papers/reductive.pdf section 5) from a system j= ustified by the principle that everything is based on sets to a system just= ified by a framework where that isn't the case.

Another connection is that it seems it should be easier to find an ax= iom, which might imply SC, that would allow us to construct the type of sem= i-simplicial types, rather than such an axiom that doesn't imply SC. Bu= t I don't know any such axiom statable in book HoTT either way.

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 sets=E2=80=9D, and it currently needs 2LTT to= even be stated.

Cheers,
Ulrik
=

------=_Part_1206_1038209094.1589124917480-- ------=_Part_1205_1443226440.1589124917480--