From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDDNRA4JSMHRBSMF57OAKGQEIR7EK4Q@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-ot1-x33f.google.com (mail-ot1-x33f.google.com [IPv6:2607:f8b0:4864:20::33f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 9d38bcf1 for ; Fri, 14 Sep 2018 14:16:42 +0000 (UTC) Received: by mail-ot1-x33f.google.com with SMTP id t46-v6sf3853825otf.13 for ; Fri, 14 Sep 2018 07:16:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=GfHuQ43Es+aXVYNDCgyIiJW2p+gMwc/M/Yov+ic1DSA=; b=P5DzEEKFjIaaT+TvgAZGL93spJWA/rYb1DMVuFfCUlk0vs+nf8P4ue9W5OTIPbbDHB 7un6X7RNexdptTb3o2ZGKjtmHrOGcG1rt73DUE20OW0kzdxWNXpMlgIdxWZCKnmXaEpl ItvOn8Uqcs6HSKfXSrnSYxE3MCIxZ2DkCiP9RLkGyGVYtxSanxR/g1/I8wwsxXZdREBM fP4nVKze68wml6cTNrI0Rgi9Ipqj0R/DRZp4GJo0EiERr9Sqp+1U4if6K3dXRuGlMPfB vU7S4HNt9idphGCxZEHUsCVNFGVtwTlwvSH2uRyjLGZTTABUvGPS1IF9CoQsFtjTiSAf +rlg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=GfHuQ43Es+aXVYNDCgyIiJW2p+gMwc/M/Yov+ic1DSA=; b=Mtwi0zW+FcwBwXIW7Murp/3h1jpic6rz2SxzbnvmJrIjyMHCRaRYy4Ws9Vr7qcedth juQaCqHptBwmUx0M/e27L9k46KV+JChqitbD1ygYDCltETaARxvcqu0CrG4xvoIhcAp3 U3DymaZ8LGhBUsihw0h5CNttI4e9NNyiq9oVeiN28huyXS7HkcLFI77Dn/5Dj/Fh+/HG a1P/019OPxdgP3L/2sJveUNmQOq6TvIElBHU2Ausl4UK66TL3Xg4HoJ36Bft031xyNhG DXlqZEXS8VCc7GxU3TrTudj3M8c0d/s6Rjv7CDAQZM7wpyDPUjaUgvYmrmX+kj+JF3pM h3ew== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=GfHuQ43Es+aXVYNDCgyIiJW2p+gMwc/M/Yov+ic1DSA=; b=atBp/3Ibj7yJlZKlYXkFd1C9/8lrmTiMgT9GHYqmfAyHmHO7SqpTiUl3pNDXttJPnb xdJLguzoa+JqBqcDOY6NjULA09mSXj1sC8KN0zj0hRX2OpMK851PciBQlGm9U9EQxCI7 GhYeS7h7BEOWUuH87zsYQKygRNlUkFHCuhVeIxBOI3dH6JlWmO77Sr3IAaY2BWTnGgKz R7SQnqiDdWF9IA2ouXNfR70vfgDhKglnP4u3pTnLU6F0urteIY5mUwULhM2YuSMI9JAv JmbebzTJoUAQFrVe51WpMDvX8Y6DgDW3kJv73eQQStPfK38IqlX7Mr1VfildArTl2GDR F0Eg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51AoOE0whrtxmuMlFlEQTXZUKPnYrhN6n342hdKA2gZwf8bzZqdc PUIfC4+P7a/wNwZx5k0ZbXk= X-Google-Smtp-Source: ANB0VdbJ+KEsADVzJ3Q6JBBEkcG+biMDZsD1VWceIO7XtZBqrS/SheYQ9nuuU+N1/yzicwV0C+7sTQ== X-Received: by 2002:a9d:4c8d:: with SMTP id m13-v6mr62493otf.6.1536934601404; Fri, 14 Sep 2018 07:16:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:6554:: with SMTP id q20-v6ls1468820otl.8.gmail; Fri, 14 Sep 2018 07:16:41 -0700 (PDT) X-Received: by 2002:a9d:5c02:: with SMTP id o2-v6mr63700otk.7.1536934600750; Fri, 14 Sep 2018 07:16:40 -0700 (PDT) Date: Fri, 14 Sep 2018 07:16:40 -0700 (PDT) From: Andrew Swan To: Homotopy Type Theory Message-Id: <33261a39-2351-4e56-a745-204334128862@googlegroups.com> 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> Subject: Re: [HoTT] Semantics of higher inductive types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_867_1212351387.1536934600125" X-Original-Sender: wakelin.swan@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_867_1212351387.1536934600125 Content-Type: multipart/alternative; boundary="----=_Part_868_1514392559.1536934600125" ------=_Part_868_1514392559.1536934600125 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thanks for writing out the note. I'll also make a few remarks about how my= =20 more recent work connects with these things. 1. The initial Susp X algebras, and I think in fact all of the initial=20 algebras appearing in the Coquand-Huber-Mortberg paper, can be constructed= =20 by combining finite colimits and W types with reductions (as appearing in t= his=20 paper ). From this it follows that they= =20 exist not just in cubical sets and simplicial sets, but any topos that=20 satisfies WISC, and for the special case of presheaf categories with=20 locally decidable cofibrations they can be constructed without using WISC= =20 or exact quotients. I think the latter can be viewed as a generalisation of= =20 the Coquand-Huber-Mortberg definition. 2. In my post and again in the W-types with reductions paper I suggested=20 using Christian's generalised notion of lifting property for commutative=20 squares. I still think this works, but I now lean towards other ways of=20 looking at it. I didn't really emphasise this in the paper, but it follows= =20 from the general theory that one obtains not just an awfs, but a fibred=20 awfs over the codomain fibration. This gives an awfs, and thereby a notion= =20 of trivial cofibration and fibration for each slice category C/Y. Then=20 given a map f : X -> Y, we can either view it as a map in the slice=20 category C/1 and factorise it there or as a map into the terminal object in= =20 the slice category C/Y. The latter is necessarily stable under pullback,=20 and I think works out the same as "freely adding a homogeneous filling=20 operator." Alternatively, it is also possible to use W types with reductions directly,= =20 without going via the small object argument. In this case the proofs in the= =20 Coquand-Huber-Mortberg paper generalise pretty much directly with very=20 little modification. 3. I still find the situation in simplicial sets a little strange, in=20 particular the need to switch back and forth between the different notions= =20 of fibration, although it does work as far as I can tell. 4. I made some remarks before about universal lifting problems. These now= =20 appear in the paper Lifting Problems in Grothendieck Fibrations=20 . Best, Andrew On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote: > > > I wrote a short note to= =20 > confirm Andrew=E2=80=99s message that indeed this technique=20 > works as well (using classical logic) for simplicial sets. This can now b= e=20 > presented > as a combination of various published results. (The originality is only i= n=20 > the presentation; > this essentially follows what is suggested in Andrew=E2=80=99s message.) > This provides a semantics of e.g. suspension as an operation U -> U,=20 > where U > is an univalent universe in the simplicial set model.=20 > > Thierry > > > On 7 Jun 2017, at 14:34, Andrew Swan >= =20 > wrote: > > So suspension (or more generally pushouts/coequalisers) is what would mak= e=20 >> a really good test case for any proposed general approach =E2=80=94 it= =E2=80=99s the=20 >> simplest HIT which as far as I know hasn=E2=80=99t been modelled without= a size=20 >> blowup in any infinite-dimensional model except cubical sets, under any = of=20 >> the approaches to modelling HIT=E2=80=99s proposed so far. (Am I right = in=20 >> remembering that this has been given for cubical sets? I can=E2=80=99t = find it in=20 >> any of the writeups, but I seem to recall hearing it presented at=20 >> conferences.) > > > The technique used in cubical type theory seems fairly flexible. I'm not= =20 > sure exactly how flexible, but I think I can get suspension to work in=20 > simplicial sets. In the below, throughout I use the characterisation of= =20 > fibrations as maps with the rlp against the pushout product of each=20 > monomorphism with endpoint inclusion into the interval. WLOG there is als= o=20 > a uniformity condition - we have a choice of lift and "pulling back the= =20 > monomorphism preserves the lift."=20 > > Given a fibration X -> Y, you first freely add elements N and S together= =20 > with a path from N to S for each element of X (I think this is the same a= s=20 > what you called pre suspension). Although the pre suspension is not a=20 > fibration in general, it does have some of the properties you might expec= t=20 > from a fibration. Given a path in Y, and an element in the fibre of an=20 > endpoint, one can transport along the path to get something in the fibre = of=20 > the other endpoint. There should also be a "flattening" operation that=20 > takes a path q in presuspension(X) over p in Y, and returns a path from= =20 > q(1) to the transport along p of q(0) that lies entirely in the fibre of= =20 > p(1). > > You then take the "weak fibrant replacement" of the pre suspension. A ma= p=20 > in simplicial sets is a fibration if and only if it has the rlp against= =20 > each pushout product of a monomorphism with an endpoint inclusion into th= e=20 > interval. In fibrant replacement you freely add a diagonal lift for each= =20 > such lifting problems. In weak fibrant replacement you only add fillers f= or=20 > some of these lifting problems. The pushout product of a monomorphism A -= >=20 > B with endpoint inclusion always has codomain B x I - then only consider= =20 > those lifting problems where the bottom map factors through the projectio= n=20 > B x I -> B. I think there are two ways to ensure that the operation of we= ak=20 > fibrant replacement is stable under pullback - one way is carry out the= =20 > operation "internally" in simplicial sets (viewed as a topos), and the=20 > other to use the algebraic small object argument, ensuring that uniformit= y=20 > condition above is in the definition. The intuitive reason why this shoul= d=20 > be stable is that the problem that stops the usual fibrant replacement fr= om=20 > being stable is that e.g. when we freely add the transport of a point alo= ng=20 > a path, p we are adding a new element to the fibre of p(1) which depends = on=20 > things outside of that fibre, whereas with weak fibrant replacement we on= ly=20 > add a filler to an open box to a certain fibre if the original open box= =20 > lies entirely in that fibre. > > In order to show that the suspension is fibrant one has to use both the= =20 > structure already present in pre suspension (transport and flattening) an= d=20 > the additional structure added by weak fibrant replacement. The idea is t= o=20 > follow the same proof as for cubical type theory. It is enough to just sh= ow=20 > composition and then derive filling. So to define the composition of an= =20 > open box, first flatten it, then use the weak fibration structure to find= =20 > the composition. (And I think that last part should be an instance of a= =20 > general result along the lines of "if the monad of transport and flatteni= ng=20 > distributes over a monad, then the fibrant replacement monad distributes= =20 > over the coproduct of that monad with weak fibrant replacement"). > > > Best, > Andrew > > > On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine wrote:= =20 >> >> 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= =20 >>> lead to cardinals outside of a Grothendieck Universe? >>> >>> Exactly, yes. There=E2=80=99s no reason I know of to think they *need*= to, but=20 >>> with the construction of Mike=E2=80=99s and my paper, they do. And add= ing stronger=20 >>> conditions on the cardinal used won=E2=80=99t help. The problem is tha= t one takes=20 >>> a fibrant replacement to go from the =E2=80=9Cpre-suspension=E2=80=9D t= o the suspension=20 >>> (more precisely: a (TC,F) factorisation, to go from the universal famil= y of=20 >>> pre-suspensions to the universal family of suspensions); and fibrant=20 >>> replacement blows up the fibers to be the size of the *base* of the=20 >>> family. So the pre-suspension is small, but the suspension =E2=80=94 a= lthough=20 >>> 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=20 >> suggest is problematic, not propositional truncation. The latter seems = a=20 >> bit easier to do by ad hoc constructions; e.g. the construction below do= es=20 >> it in simplicial sets, and I think a similar thing may work also in cubi= cal=20 >> sets. (I don=E2=80=99t claim originality for this construction; I don= =E2=80=99t think I=20 >> learned it from anywhere, but I do recall discussing it with people who= =20 >> were already aware of it or something similar (I think at least Mike,=20 >> Thierry, and Simon Huber, at various times?), so I think multiple people= =20 >> may have noticed it independently.) >> >> So suspension (or more generally pushouts/coequalisers) is what would=20 >> make a really good test case for any proposed general approach =E2=80=94= it=E2=80=99s the=20 >> simplest HIT which as far as I know hasn=E2=80=99t been modelled without= a size=20 >> blowup in any infinite-dimensional model except cubical sets, under any = of=20 >> the approaches to modelling HIT=E2=80=99s proposed so far. (Am I right = in=20 >> remembering that this has been given for cubical sets? I can=E2=80=99t = find it in=20 >> any of the writeups, but I seem to recall hearing it presented at=20 >> conferences.) >> >> Construction of propositional truncation without size blowup in=20 >> simplicial sets: >> >> (1) Given a fibration Y =E2=80=94> X, define |Y| =E2=80=94> X as follow= s: >> >> an element of |Y|_n consists of an n-simplex x : =CE=94[n] =E2=80=94> X,= together with=20 >> a =E2=80=9Cpartial lift of x into Y, defined at least on all vertices=E2= =80=9D, i.e. a=20 >> subpresheaf S =E2=89=A4 =CE=94[n] containing all vertices, and a map y := S =E2=80=94> Y such=20 >> that the evident square commutes; >> >> reindexing acts by taking pullbacks/inverse images of the domain of the= =20 >> partial lift (i.e. the usual composition of a partial map with a total m= ap). >> >> (2) There=E2=80=99s an evident map Y =E2=80=94> |Y| over X; and the oper= ation sending Y=20 >> to Y =E2=80=94> |Y| =E2=80=94> X is (coherently) stable up to isomorphis= m under pullback in=20 >> X. (Straightforward.) >> >> (3) In general, a fibration is a proposition in the type-theoretic sense= =20 >> iff it=E2=80=99s orthogonal to the boundary inclusions =CE=B4[n] =E2=80= =94> =CE=94[n] for all n > 0.=20 >> (Non-trivial but not too hard to check.) >> >> (4) The map |Y| =E2=80=94> X is a fibration, and a proposition.=20 >> (Straightforward, given (3), by concretely constructing the required=20 >> liftings.) >> >> (5) The evident map Y =E2=80=94> |Y| over X is a cell complex constructe= d from=20 >> 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=20 >> non-degenerate simplices of Y_n are those whose =E2=80=9Cmissing=E2=80= =9D simplices are all=20 >> of dimension =E2=89=A4n. Then Y_0 =3D Y, and the non-degenerate simplic= es of Y_{n+1}=20 >> that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the=20 >> 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>=20 >> =CE=94[n+1]. >> >> (6) The map Y =E2=80=94> |Y| is orthogonal to all propositional fibratio= ns,=20 >> stably in X. (Orthogonality is immediate from (3) and (5); stability is= =20 >> then by (2).) >> >> (7) Let V be either the universe of =E2=80=9Cwell-ordered =CE=B1-small f= ibrations=E2=80=9D, or=20 >> the universe of =E2=80=9Cdisplayed =CE=B1-small fibrations=E2=80=9D, for= =CE=B1 any infinite regular=20 >> cardinal. Then V carries an operation representing the construction of= =20 >> (1), and modelling propositional truncation. (Lengthy to spell out in= =20 >> full, but straightforward given (2), (6).) >> >> >> =E2=80=93p. >> >> >> >> > --=20 You received this message because you are subscribed to the Google Groups "= 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 https://groups.google.com/d/optout. ------=_Part_868_1514392559.1536934600125 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks for writing out the note. I'll also make a few = remarks about how my more recent work connects with these things.

<= /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.

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= ."

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.

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.

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

<= div>Best,
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=A0
works as well (using classical logic) for simplicial sets. This can no= w be presented
as 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 U
is 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--