On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:

--001a114dc8c4c62f3505515b85d0--

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.

=