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:
--001a114dc8c4c62f3505515b85d0--