Thanks for writing out the note. I'll also make a few =
remarks about how my more recent work connects with these things.

<= /div>

2. In my post and again in the W-types with reductions paper I suggested =
using Christian's generalised notion of lifting property for commutativ=
e squares. I still think this works, but I now lean towards other ways of l=
ooking at it. I didn't really emphasise this in the paper, but it follo=
ws from the general theory that one obtains not just an awfs, but a fibred =
awfs over the codomain fibration. This gives an awfs, and thereby a notion =
of trivial cofibration and fibration for each slice category C/Y. Then give=
n a map f : X -> Y, we can either view it as a map in the slice category=
C/1 and factorise it there or as a map into the terminal object in the sli=
ce category C/Y. The latter is necessarily stable under pullback, and I thi=
nk works out the same as "freely adding a homogeneous filling operator=
."

3. I still find the situation in simplicial sets a little strange, in par=
ticular the need to switch back and forth between the different notions of =
fibration, although it does work as far as I can tell.

<= /div>

1. The initial Susp X algebras, and I think in fact all of the in=
itial algebras appearing in the Coquand-Huber-Mortberg paper, can be constr=
ucted by combining finite colimits and W types with reductions (as appearin=
g in this paper). From thi=
s it follows that they exist not just in cubical sets and simplicial sets, =
but any topos that satisfies WISC, and for the special case of presheaf cat=
egories with locally decidable cofibrations they can be constructed without=
using WISC or exact quotients. I think the latter can be viewed as a gener=
alisation of the Coquand-Huber-Mortberg definition.

Alternatively, it is also possible to use =
W types with reductions directly, without going via the small object argume=
nt. In this case the proofs in the Coquand-Huber-Mortberg paper generalise =
pretty much directly with very little modification.

4. I made some remarks before about universal lifting problems. These =
now appear in the paper=C2=A0L=
ifting Problems in Grothendieck Fibrations=C2=A0.

Andrew

On Friday, 14 September 2018 1= 3:15:58 UTC+2, coquand wrote:

=C2=A0I wrote a short=C2=A0note=C2=A0to confirm Andrew=E2=80=99s message that indeed this= technique=C2=A0works as well (using classical logic) for simplicial sets. This can no= w be presentedas a combination of various published results. (The originality is onl= y in the presentation;this essentially follows what is suggested in Andrew=E2=80=99s message= .)=C2=A0This provides a semantics of e.g. suspension as an operation U -= > U, where Uis an univalent universe in the simplicial set model.=C2=A0

=C2=A0Thierry

On 7 Jun 2017, at 14:34, Andrew Swan <wakeli...@gmail.com> wrote:=

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 modelle= d without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT=E2=80=99= s proposed so far. =C2=A0(Am I right in remembering that this has been give= n for cubical sets?=C2=A0 I can=E2=80=99t find it in any of the writeups, b= ut I seem to recall hearing it presented at conferences.)The technique used in cubical type theory seems fairly flexible. I'm no= t sure exactly how flexible, but I think I can get suspension to work in si= mplicial sets. In the below, throughout I use the characterisation of fibra= tions as maps with the rlp against the pushout product of each monomorphism with endpoint inclusion into the inte= rval. WLOG there is also a uniformity condition - we have a choice of lift = and "pulling back the monomorphism preserves the lift."

Given a fibration X -> Y, you first freely add elements N and S tog= ether with a path from N to S for each element of X (I think this is the sa= me as what you called pre suspension). Although the pre suspension is not a= fibration in general, it does have some of the properties you might expect from a fibration. Given = a path in Y, and an element in the fibre of an endpoint, one can transport = along the path to get something in the fibre of the other endpoint. There s= hould also be a "flattening" operation that takes a path q in presuspension(X) over p in Y, and returns a path fr= om q(1) to the transport along p of q(0) that lies entirely in the fibre of= p(1).

You then take the "weak fibrant replacement" of the pre susp= ension. =C2=A0A map in simplicial sets is a fibration if and only if it has= the rlp against each pushout product of a monomorphism with an endpoint in= clusion into the interval. In fibrant replacement you freely add a diagonal lift for each such lifting problems.= In weak fibrant replacement you only add fillers for some of these lifting= problems. The pushout product of a monomorphism A -> B with endpoint in= clusion always has codomain B x I - then only consider those lifting problems where the bottom map factors thr= ough the projection B x I -> B. I think there are two ways to ensure tha= t the operation of weak fibrant replacement is stable under pullback - one = way is carry out the operation "internally" in simplicial sets (viewed as a topos), and the other to use the algebraic= small object argument, ensuring that uniformity condition above is in the = definition. The intuitive reason why this should be stable is that the prob= lem that stops the usual fibrant replacement from being stable is that e.g. when we freely add the transpor= t of a point along a path, p we are adding a new element to the fibre of p(= 1) which depends on things outside of that fibre, whereas with weak fibrant= replacement we only add a filler to an open box to a certain fibre if the original open box lies entirely i= n that fibre.

In order to show that the suspension is fibrant one has to use both th= e structure already present in pre suspension (transport and flattening) an= d the additional structure added by weak fibrant replacement. The idea is t= o follow the same proof as for cubical type theory. It is enough to just show composition and then= derive filling. So to define the composition of an open box, first flatten= it, then use the weak fibration structure to find the composition. (And I = think that last part should be an instance of a general result along the lines of "if the monad of tran= sport and flattening distributes over a monad, then the fibrant replacement= monad distributes over the coproduct of that monad with weak fibrant repla= cement").

Best,Andrew

On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine wrote: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:

>

> you mean the propositional truncation or suspension operations might l= ead to cardinals outside of a Grothendieck Universe?

Exactly, yes.=C2=A0 There=E2=80=99s no reason I know of to think the= y *need* to, but with the construction of Mike=E2=80=99s and my paper, they= do.=C2=A0 And adding stronger conditions on the cardinal used won=E2=80=99= t help.=C2=A0 The problem is that one takes a fibrant replacement to go from the =E2=80=9Cpre-suspension=E2=80=9D to the suspension (more precisel= y: a (TC,F) factorisation, to go from the universal family of pre-suspensio= ns to the universal family of suspensions); and fibrant replacement blows u= p the fibers to be the 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 as large as the universe one= =E2=80=99s using.

I realise I was a bit unclear here: it=E2=80=99s only suspension that = I meant to suggest is problematic, not propositional truncation.=C2=A0 The = latter seems a bit easier to do by ad hoc constructions; e.g. the construct= ion below does it in simplicial sets, and I think a similar thing may work also in cubical sets. =C2=A0(I don=E2= =80=99t claim originality for this construction; I don=E2=80=99t think I le= arned 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 multi= ple 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 mode= lled 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. =C2=A0(Am I right in remembering that this has bee= n given for cubical sets?=C2=A0 I can=E2=80=99t find it in any of the write= ups, but I seem to recall hearing it presented at conferences.)

Construction of propositional truncation without size blowup in simpli= cial 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&g= t; X, together with a =E2=80=9Cpartial lift of x into Y, defined at least o= n all vertices=E2=80=9D, i.e. a subpresheaf S =E2=89=A4 =CE=94[n] containin= g all vertices, and a map y : S =E2=80=94> Y such that the evident squar= e commutes;

reindexing acts by taking pullbacks/inverse images of the domain of th= e partial lift (i.e. the usual composition of a partial map with a total ma= p).

(2) There=E2=80=99s an evident map Y =E2=80=94> |Y| over X; and the= operation sending 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 sen= se 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 concretely constructing the required lif= tings.)

(5) The evident map Y =E2=80=94> |Y| over X is a cell complex const= ructed from boundary inclusions =CE=B4[n] =E2=80=94> =CE=94[n] with n &g= t; 0.

To see this: take the filtration of |Y| by subobjects Y_n, where the n= on-degenerate simplices of Y_n are those whose =E2=80=9Cmissing=E2=80=9D si= mplices 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 fib= rations, stably in X. =C2=A0(Orthogonality is immediate from (3) and (5); s= tability is then by (2).)

(7) Let V be either the universe of =E2=80=9Cwell-ordered =CE=B1-small= fibrations=E2=80=9D, or the universe of =E2=80=9Cdisplayed =CE=B1-small fi= brations=E2=80=9D, for =CE=B1 any infinite regular cardinal.=C2=A0 Then V c= arries an operation representing the construction of (1), and modelling pro= positional truncation. =C2=A0(Lengthy to spell out in full, but straightforward given= (2), (6).)

=E2=80=93p.

You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.

To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.

For more options, visit http= s://groups.google.com/d/optout.

------=_Part_868_1514392559.1536934600125-- ------=_Part_867_1212351387.1536934600125--