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--