From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.88.7 with SMTP id m7mr4254418ywb.19.1496828412552; Wed, 07 Jun 2017 02:40:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.39.72 with SMTP id r66ls4891579ota.15.gmail; Wed, 07 Jun 2017 02:40:12 -0700 (PDT) X-Received: by 10.129.174.67 with SMTP id g3mr3962588ywk.66.1496828412070; Wed, 07 Jun 2017 02:40:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1496828412; cv=none; d=google.com; s=arc-20160816; b=kNP8KPdV4+kkVYC7/eQNw9SjsP6nCF+5wHnr/rheqX3P4luqyP2JvaTsfqkF9uSj/R 1huXm7Qkfse86Gi9wXeMmqVI71Cx3rv8mSuLdR9VPrquAIE8b0fxWyE4ozvQ3H0Xv/sd IT06ocaufXw9AR/iZjRbd9LxtWPYH+9XbU0+el17ugSmpgttUTVlxpSK/aPdnaz3TRPY fQ34vZWJ1YOQTPKKrBdux0DXA3Fo+8X4ViufwO01qRexCumlVZ/0SGIB/WkP+G7+ya6M iV7C05fsvUA4KBwS3JjY2BqMX8Tc2JE7S7Luvnug5UuM0q4EY/8CODThPiK7WPxqCtr7 VFsg== 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:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=vyWolDEy/HPQY3poQjUBmh/riE4tDm5wjpsFOdsJQRo=; b=IuCfpHyr69CAbrRTJNXfvO3T9fMdqI85qQvVYAzeM3yNKWik8Ee3F5Jxq3OhvDq90u raE/2mhg8RZZElq0RJ/oI0a5pUbyFUYJAiDoZfvTyMc/n8y5fabzg8VtEcWH/V7VJi0U ZulHn3akmZq9M2WTDzTyGa0eybMVovumk3tydeB8cc7zUyS8q3rCMqeLwTNqlUk+f5mL jrA9I1yovOyLWk+W7Sij8O67mMDwNhhCRevXibeh9y3h7vUGarkq0hhytGWjgJKNiYX8 YewZRh3141AyemfV+EMXsiWsgOQ/kNJnEi9cJ1aAV1VRupDgceAcEaRgJgwzGeuz6DUr P4CQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::232 as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vk0-x232.google.com (mail-vk0-x232.google.com. [2607:f8b0:400c:c05::232]) by gmr-mx.google.com with ESMTPS id n1si23636vke.0.2017.06.07.02.40.12 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Jun 2017 02:40:12 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::232 as permitted sender) client-ip=2607:f8b0:400c:c05::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::232 as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-vk0-x232.google.com with SMTP id p85so2898006vkd.3 for ; Wed, 07 Jun 2017 02:40:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=vyWolDEy/HPQY3poQjUBmh/riE4tDm5wjpsFOdsJQRo=; b=a75cKb+qQfwRRvVvrb4YHSWl5cXfmihQsuGqEASuBH+E2M1oxmtPTFOpk3dO6kQGJX autPnGxRHw+4EK35A7kPRX9J119AsnRKLD29Vxk5mg0BG89b7q4KgdRjc5S/s/Aky0z+ Bpzx9qvad70vce+yT4V+bAjQb5dltdME8wx554285KHJWm/WFuyO9FccDC5AoUmPyv0f 1uMcJ+Pge6v9UEDh2qaxCBfjznRFfIZsYVW/rlcPd5wS2WZl1/l1+mJFvFtE5zTEygFL e38npniuTJgOfp7M42s0yzqy79+wf/VMkCbUM5ZEFr1nbgfHyMq+Ibz8s0IpE15GzQ36 kbcw== X-Gm-Message-State: AODbwcBvLki+oMPOHrQ7pJSBCyyTf3GN+/H9B8YHb+MYFO70HIAUEm1x 9frkQQOLS/W6c9zYIYD99Uhm23/4mQ== X-Received: by 10.31.205.1 with SMTP id d1mr15081152vkg.98.1496828411783; Wed, 07 Jun 2017 02:40:11 -0700 (PDT) MIME-Version: 1.0 Received: by 10.176.22.216 with HTTP; Wed, 7 Jun 2017 02:40:11 -0700 (PDT) In-Reply-To: References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> <9F58F820-A54A-46E7-93DC-F814D4BEE0C6@cmu.edu> From: Peter LeFanu Lumsdaine Date: Wed, 7 Jun 2017 11:40:11 +0200 Message-ID: Subject: Re: [HoTT] Semantics of higher inductive types To: Steve Awodey Cc: Michael Shulman , Thierry Coquand , homotopy Type Theory Content-Type: multipart/alternative; boundary="001a114dc8c4c62f3505515b85d0" --001a114dc8c4c62f3505515b85d0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine < p.l.lu...@gmail.com> wrote: > On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey wrote: > > > > you mean the propositional truncation or suspension operations might > lead to cardinals outside of a Grothendieck Universe? > > Exactly, yes. There=E2=80=99s no reason I know of to think they *need* t= o, but > with the construction of Mike=E2=80=99s and my paper, they do. And addin= g stronger > conditions on the cardinal used won=E2=80=99t help. The problem is that = one takes > a fibrant replacement to go from the =E2=80=9Cpre-suspension=E2=80=9D to = the suspension > (more precisely: a (TC,F) factorisation, to go from the universal family = of > pre-suspensions to the universal family of suspensions); and fibrant > replacement blows up the fibers to be the size of the *base* of the > family. So the pre-suspension is small, but the suspension =E2=80=94 alt= hough > essentially small =E2=80=94 ends up as large as the universe one=E2=80=99= s using. > I realise I was a bit unclear here: it=E2=80=99s only suspension that I mea= nt to suggest is problematic, not propositional truncation. The latter seems a bit easier to do by ad hoc constructions; e.g. the construction below does it in simplicial sets, and I think a similar thing may work also in cubical sets. (I don=E2=80=99t claim originality for this construction; I don=E2= =80=99t think I learned it from anywhere, but I do recall discussing it with people who were already aware of it or something similar (I think at least Mike, Thierry, and Simon Huber, at various times?), so I think multiple people may have noticed it independently.) So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach =E2=80=94 it=E2= =80=99s the simplest HIT which as far as I know hasn=E2=80=99t been modelled without a = size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT=E2=80=99s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can=E2=80=99t fin= d it in any of the writeups, but I seem to recall hearing it presented at conferences.) Construction of propositional truncation without size blowup in simplicial sets: (1) Given a fibration Y =E2=80=94> X, define |Y| =E2=80=94> X as follows: an element of |Y|_n consists of an n-simplex x : =CE=94[n] =E2=80=94> X, to= gether with a =E2=80=9Cpartial lift of x into Y, defined at least on all vertices=E2=80= =9D, i.e. a subpresheaf S =E2=89=A4 =CE=94[n] containing all vertices, and a map y : S = =E2=80=94> Y such that the evident square commutes; reindexing acts by taking pullbacks/inverse images of the domain of the partial lift (i.e. the usual composition of a partial map with a total map)= . (2) There=E2=80=99s an evident map Y =E2=80=94> |Y| over X; and the operati= on sending Y to Y =E2=80=94> |Y| =E2=80=94> X is (coherently) stable up to isomorphism unde= r pullback in X. (Straightforward.) (3) In general, a fibration is a proposition in the type-theoretic sense iff it=E2=80=99s orthogonal to the boundary inclusions =CE=B4[n] =E2=80=94>= =CE=94[n] for all n > 0. (Non-trivial but not too hard to check.) (4) The map |Y| =E2=80=94> X is a fibration, and a proposition. (Straightf= orward, given (3), by concretely constructing the required liftings.) (5) The evident map Y =E2=80=94> |Y| over X is a cell complex constructed f= rom boundary inclusions =CE=B4[n] =E2=80=94> =CE=94[n] with n > 0. To see this: take the filtration of |Y| by subobjects Y_n, where the non-degenerate simplices of Y_n are those whose =E2=80=9Cmissing=E2=80=9D s= implices are all of dimension =E2=89=A4n. Then Y_0 =3D Y, and the non-degenerate simplices = of Y_{n+1} that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the inclusion Y_n =E2=80=94> Y_{n+1} may be seen as gluing on many copies of = =CE=B4[n+1] =E2=80=94> =CE=94[n+1]. (6) The map Y =E2=80=94> |Y| is orthogonal to all propositional fibrations,= stably in X. (Orthogonality is immediate from (3) and (5); stability is then by (2).) (7) Let V be either the universe of =E2=80=9Cwell-ordered =CE=B1-small fibr= ations=E2=80=9D, or the universe of =E2=80=9Cdisplayed =CE=B1-small fibrations=E2=80=9D, for = =CE=B1 any infinite regular cardinal. Then V carries an operation representing the construction of (1), and modelling propositional truncation. (Lengthy to spell out in full, but straightforward given (2), (6).) =E2=80=93p. --001a114dc8c4c62f3505515b85d0 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:
On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <awo...@cmu.edu> wrote:
>
&= gt; you mean the propositional truncation or suspension operations might le= ad to cardinals outside of a Grothendieck Universe?

Exactly, = yes.=C2=A0 There=E2=80=99s no reason I know of to think they *need* to, but= with the construction of Mike=E2=80=99s and my paper, they do.=C2=A0 And a= dding stronger conditions on the cardinal used won=E2=80=99t help.=C2=A0 Th= e problem is that one takes a fibrant replacement to go from the =E2=80=9Cp= re-suspension=E2=80=9D to the suspension (more precisely: a (TC,F) factoris= ation, to go from the universal family of pre-suspensions to the universal = family of suspensions); and fibrant replacement blows up the fibers to be t= he size of the *base* of the family.=C2=A0 So the pre-suspension is small, = but the suspension =E2=80=94 although essentially small =E2=80=94 ends up a= s large as the universe one=E2=80=99s using.

I realise I was a bit unclear here: it=E2=80=99s only suspension th= at I meant to suggest is problematic, not propositional truncation.=C2=A0 T= he latter seems a bit easier to do by ad hoc constructions; e.g. the constr= uction below does it in simplicial sets, and I think a similar thing may wo= rk also in cubical sets. =C2=A0(I don=E2=80=99t claim originality for this = construction; I don=E2=80=99t think I learned it from anywhere, but I do re= call discussing it with people who were already aware of it or something si= milar (I think at least Mike, Thierry, and Simon Huber, at various times?),= so I think multiple people may have noticed it independently.)
<= br>
So suspension (or more generally pushouts/coequalisers) is wh= at would make a really good test case for any proposed general approach =E2= =80=94 it=E2=80=99s the simplest HIT which as far as I know hasn=E2=80=99t = been modelled without a size blowup in any infinite-dimensional model excep= t cubical sets, under any of the approaches to modelling HIT=E2=80=99s prop= osed so far. =C2=A0(Am I right in remembering that this has been given for = cubical sets?=C2=A0 I can=E2=80=99t find it in any of the writeups, but I s= eem to recall hearing it presented at conferences.)

Construction of propositional truncation without size blowup in simpl= icial sets:

(1) =C2=A0Given a fibration Y =E2=80= =94> X, define |Y| =E2=80=94> X as follows:

an element of |Y|_n consists of an n-simplex x : =CE=94[n] =E2=80= =94> X, together with a =E2=80=9Cpartial lift of x into Y, defined at le= ast on all vertices=E2=80=9D, i.e. a subpresheaf S =E2=89=A4 =CE=94[n] cont= aining all vertices, and a map y : S =E2=80=94> Y such that the evident = square commutes;

reindexing acts by taking pullbac= ks/inverse images of the domain of the partial lift (i.e. the usual composi= tion of a partial map with a total map).

(2) There= =E2=80=99s an evident map Y =E2=80=94> |Y| over X; and the operation sen= ding Y to Y =E2=80=94> |Y| =E2=80=94> X is (coherently) stable up to = isomorphism under pullback in X. =C2=A0(Straightforward.)

(3) In general, a fibration is a proposition in the type-theoretic = sense iff it=E2=80=99s orthogonal to the boundary inclusions =CE=B4[n] =E2= =80=94> =CE=94[n] for all n > 0. =C2=A0(Non-trivial but not too hard = to check.)

(4) The map |Y| =E2=80=94> X is = a fibration, and a proposition. =C2=A0(Straightforward, given (3), by concr= etely constructing the required liftings.)

(5) The= evident map Y =E2=80=94> |Y| over X is a cell complex constructed from = boundary inclusions =CE=B4[n] =E2=80=94> =CE=94[n] with n > 0.
<= div>
To see this: take the filtration of |Y| by subobjects Y_= n, where the non-degenerate simplices of Y_n are those whose =E2=80=9Cmissi= ng=E2=80=9D simplices are all of dimension =E2=89=A4n.=C2=A0 Then Y_0 =3D Y= , and the non-degenerate simplices of Y_{n+1} that are not in Y_n are all {= n+1}-cells with boundary in Y_n, so the inclusion Y_n =E2=80=94> Y_{n+1}= may be seen as gluing on many copies of =CE=B4[n+1] =E2=80=94> =CE=94[n= +1].

(6) The map Y =E2=80=94> |Y| is orthogonal= to all propositional fibrations, stably in X. =C2=A0(Orthogonality is imme= diate from (3) and (5); stability is then by (2).)

(7) Let V be either the universe of =E2=80=9Cwell-ordered =CE=B1-small fib= rations=E2=80=9D, or the universe of =E2=80=9Cdisplayed =CE=B1-small fibrat= ions=E2=80=9D, for =CE=B1 any infinite regular cardinal.=C2=A0 Then V carri= es an operation representing the construction of (1), and modelling proposi= tional truncation. =C2=A0(Lengthy to spell out in full, but straightforward= given (2), (6).)


=E2=80=93p.
=



--001a114dc8c4c62f3505515b85d0--