From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC4PDJ5VRELBB3NQ53OAKGQEUJKHLXI@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.7 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-wr1-x437.google.com (mail-wr1-x437.google.com [IPv6:2a00:1450:4864:20::437]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 23274041 for ; Fri, 14 Sep 2018 11:15:59 +0000 (UTC) Received: by mail-wr1-x437.google.com with SMTP id a37-v6sf9559394wrc.5 for ; Fri, 14 Sep 2018 04:15:58 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1536923758; cv=pass; d=google.com; s=arc-20160816; b=YGGUQWzJzAH+7VC6MgKAX5SpRga/zbb8UBNxIeDnbJMv3hkvSfm6DyLR90o5p9Algc 9+p3BFT7PCtASqsyLGJGhv25MfCsVUGulEieQQR4IgdVrMq6NWqmrKQvjrJrm2R/Zs1i 7l0xitOw03W76DMEXFYdoMM2jAgna+l6dW5pOS/F4QSejWA7VIsd3+bGUlMO8V1LPn4U mqkzq+CPzfsMe3cjpvW2vdlhdAWA1oAqSRfECp+Ld+PTckSicw1O5tduv+Xyn8u3fWSj zyRSfn0ozspwejsGQutd4FOgH+NKs8CIH9wwjGmBvEIGdb7KWm+XMX85mK5eLoOn//6j 4ddg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:mime-version:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:sender:dkim-signature; bh=7Ah6TEcUuVs7mEAq9aLmRWPaELK8VS0ihTPl9Uf1mN4=; b=jZ4PkWK/DiU5yEs7vbh37quHweC0cXjr6WpaTqSYK+yWBEMepN0VfGoxeXUwkePgyQ 6FJRH0sbQlCc0ytI3dkDtnhHbmAcXYBOmZnaXuGtPTKiYcrKJfeAIsCzGyVZ9kmdnww0 BlWNBoYRH0RSPvKWrovTa1KsGsbOX/dBZ2mIjo+Qn+V0m5AhnBh+AJuJfNBcG7MJeS79 tfZ2x5ollpy/avcUNiBT7gJlgxa6e3Vw0YHFHrVfFAxbdo6Nblh8BRcwBRITJpZ/LZZy twQeykA+Rx4DbOqeOh65R5thx7MJU3AYdL3B+rZlR44T4Hdvx9KSTMeFs1muUXvzxPn7 oLuA== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=neutral (google.com: 129.16.226.132 is neither permitted nor denied by best guess record for domain of thierry.coquand@cse.gu.se) smtp.mailfrom=Thierry.Coquand@cse.gu.se DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=7Ah6TEcUuVs7mEAq9aLmRWPaELK8VS0ihTPl9Uf1mN4=; b=ObNredKV+dR9ogkCkRY9LE8blXihjRErnHOxOwN3w5C8OaVyXVlBgKZ9zK14RTscme f0AsAc3sKoYzECy1TdkLvVcv3OyJ9fn9qBX/dJMuAD4kaNx17fdRrgCUKsq7mOdtM6ne 4uLxwafTOP62dbsDTP/nftqLTLTyCZxMTLM19g5VrEBw8F9KaBhBjZuZf1ssIIv6IT8v gqtb8IuBg5uQO5EP+YIdreytH6xSS3J0MOj5ZFdEDueN7oOeGzR7Uer/AtN8sijwi+/n 8A0YFpmvSpysyg8j62pZmAqKddisRuZtWBTbYuTIlX95/rN08+8UVZrczympV4PuphD/ TvGw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=7Ah6TEcUuVs7mEAq9aLmRWPaELK8VS0ihTPl9Uf1mN4=; b=aVIg9i/JsCFBwM0sWwHNYejsWqkFOuEQvkdxOD/bX3R6TipuviPHhQ5clh93lBZzzU d+RIcqXTmjYej0Uw2VLhOBB4vQut5k0KCzvsjQIdwYX6X5JsRp5dKc2RgezqYBwd91O+ FRsU3FuVWWIPN7N/APe7Fh11A8w08sH6Qg664u1WGMR9vqcEvolkMxSTuzX5yPkq7ucp bmM8p4OLDxoL+lqfAqjGoxIhPRE9MyE1Z84VA0cmiEd6QhHz9mkW4nbS3e+WBVHHKD3F 79HRcWpDApnWis6KCs0HM6Br11t8hArXcIAQFpdrpq/G5ksIJr/nmN79G8QvIU6sxImy +02g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51AO3qD50Nj0QsSkC54aXp9SMNapNqilcJIVDIzBNMO5N2ssaLA+ UuNsbAKiiV6Mi2Vp6w2dTo0= X-Google-Smtp-Source: ANB0VdalifvHdiP8z71TDddJqzw9eZPreoGbI67CFNF5naGAAGHX6kpLVnoC7fGHNpTLwQziO/s9YQ== X-Received: by 2002:adf:9d1a:: with SMTP id k26-v6mr152747wre.4.1536923757932; Fri, 14 Sep 2018 04:15:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:103:: with SMTP id 3-v6ls407882wmb.7.canary-gmail; Fri, 14 Sep 2018 04:15:57 -0700 (PDT) X-Received: by 2002:a1c:9955:: with SMTP id b82-v6mr248845wme.30.1536923757342; Fri, 14 Sep 2018 04:15:57 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1536923757; cv=none; d=google.com; s=arc-20160816; b=U7n4A5uwevMdhsW5yaIYhEYn7JOtvqrfdHekpVEPFA2KPj4riWYPgM371V1J4KSpsX KRXB7X++wOruPG3QakCJlLroWadhs68giNDLSdXcts3XEucMInM3OAd+ImmcimGb8M4+ emMT4lqL9Oo1bQKJgFWm3d0/R5y8nRxtjlw9fQslReMY3XhKX6mfP4pL8lrOHwPl9zR4 97zHDOL+sk0Uka3kVCra18yb8G+bMXafH4nyGc3EflrFw8mbX0SUUC+WrmNWLEXOZWka 30uc7YlG9AJXUKDNvQqWSjnxQ57krsJktWfpEpcRYkmxWBcI5zrGbUKEVXdx543jSCuI rXfg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:to :from; bh=DqJ7SYhEZ/Kby0lhjlP5eeSPsadidI5YnVqt6XcpIHY=; b=QLiL/J5dBuaoGmJwcx7kLOOgp1YK5ZZa7hy3St1YvPeaCxFsBf0+o+GXoHxJoMO8f5 QKej+ew3o68iU6CQcNz2y9ruQCmMRv5rNhQFU/zQZedJpYYFEIJD8Hx/BxNVxAdjY/SD cw1PkUDkJ1URLfghxWzRwqX5jC9ZENyE78uwivPDGHjG22UWinjesfTNJOI3o+atkA69 IYQtRNIyJ157r3UoAlhEBBLKmHYA3Sw2fqS61EOHrI5pjrELAFAYSoxvg3ZmKaF1XPbN wxltNQ6tOyW41ofoTyPEIT4YjHEVtz0cN4nhFKw1vaRyfOKmVDeNQSByF4+eFVggc+tu 6Nsw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=neutral (google.com: 129.16.226.132 is neither permitted nor denied by best guess record for domain of thierry.coquand@cse.gu.se) smtp.mailfrom=Thierry.Coquand@cse.gu.se Received: from tyrell.ita.chalmers.se (tyrell.ita.chalmers.se. [129.16.226.132]) by gmr-mx.google.com with ESMTPS id y13-v6si273170wrd.3.2018.09.14.04.15.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Fri, 14 Sep 2018 04:15:57 -0700 (PDT) Received-SPF: neutral (google.com: 129.16.226.132 is neither permitted nor denied by best guess record for domain of thierry.coquand@cse.gu.se) client-ip=129.16.226.132; Received: from tyrell.ita.chalmers.se (129.16.226.132) by tyrell.ita.chalmers.se (129.16.226.132) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.1531.3; Fri, 14 Sep 2018 13:15:56 +0200 Received: from tyrell.ita.chalmers.se ([129.16.226.132]) by tyrell.ita.chalmers.se ([129.16.226.132]) with mapi id 15.01.1531.003; Fri, 14 Sep 2018 13:15:56 +0200 From: Thierry Coquand To: "HomotopyTypeTheory@googlegroups.com" Subject: Re: [HoTT] Semantics of higher inductive types Thread-Topic: [HoTT] Semantics of higher inductive types Thread-Index: AQHS1YRqrYjkQqJDokGDQZgyV4mF/aIP+LoAgAASs4CAAAJcAIAABOQAgAADgYCACQFfgIAAlVoAgti/EgA= Date: Fri, 14 Sep 2018 11:15:56 +0000 Message-ID: References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> <9F58F820-A54A-46E7-93DC-F814D4BEE0C6@cmu.edu> In-Reply-To: Accept-Language: en-US, sv-SE Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [129.16.10.245] Content-Type: multipart/alternative; boundary="_000_EA45D7F1FC164653B331FA0218FDD5DDchalmersse_" MIME-Version: 1.0 X-Original-Sender: thierry.coquand@cse.gu.se X-Original-Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 129.16.226.132 is neither permitted nor denied by best guess record for domain of thierry.coquand@cse.gu.se) smtp.mailfrom=Thierry.Coquand@cse.gu.se 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: , --_000_EA45D7F1FC164653B331FA0218FDD5DDchalmersse_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I wrote a short note to conf= irm Andrew=E2=80=99s message that indeed this technique works as well (using classical logic) for simplicial sets. This can now be = presented as a combination of various published results. (The originality is only in = 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, where= U is an univalent universe in the simplicial set model. Thierry On 7 Jun 2017, at 14:34, Andrew Swan > 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 se= ts, 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 find it in any of the writeups, but I seem to recall hearing = it presented at conferences.) The technique used in cubical type theory seems fairly flexible. I'm not su= re exactly how flexible, but I think I can get suspension to work in simpli= cial sets. In the below, throughout I use the characterisation of fibration= s as maps with the rlp against the pushout product of each monomorphism wit= h endpoint inclusion into the interval. WLOG there is also a uniformity con= dition - we have a choice of lift and "pulling back the monomorphism preser= ves the lift." Given a fibration X -> Y, you first freely add elements N and S together wi= th a path from N to S for each element of X (I think this is the same as wh= at you called pre suspension). Although the pre suspension is not a fibrati= on 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, o= ne can transport along the path to get something in the fibre of the other = endpoint. There should also be a "flattening" operation that takes a path q= in presuspension(X) over p in Y, and returns a path from q(1) to the trans= port along p of q(0) that lies entirely in the fibre of p(1). You then take the "weak fibrant replacement" of the pre suspension. A map = in simplicial sets is a fibration if and only if it has the rlp against eac= h pushout product of a monomorphism with an endpoint inclusion into the int= erval. 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 wi= th endpoint inclusion always has codomain B x I - then only consider those = lifting problems where the bottom map factors through the projection B x I = -> B. I think there are two ways to ensure that the operation of weak fibra= nt replacement is stable under pullback - one way is carry out the operatio= n "internally" in simplicial sets (viewed as a topos), and the other to use= the algebraic small object argument, ensuring that uniformity condition ab= ove is in the definition. The intuitive reason why this should be stable is= that the problem that stops the usual fibrant replacement from being stabl= e is that e.g. when we freely add the transport of a point along a path, p = we are adding a new element to the fibre of p(1) which depends on things ou= tside of that fibre, whereas with weak fibrant replacement we only add a fi= ller to an open box to a certain fibre if the original open box lies entire= ly in that fibre. In order to show that the suspension is fibrant one has to use both the str= ucture already present in pre suspension (transport and flattening) and the= additional structure added by weak fibrant replacement. The idea is to fol= low the same proof as for cubical type theory. It is enough to just show co= mposition 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 co= mposition. (And I think that last part should be an instance of a general r= esult along the lines of "if the monad of transport and flattening distribu= tes over a monad, then the fibrant replacement monad distributes over the c= oproduct of that monad with weak fibrant replacement"). 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 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* to,= but with the construction of Mike=E2=80=99s and my paper, they do. And ad= ding stronger conditions on the cardinal used won=E2=80=99t help. The prob= lem is that one takes a fibrant replacement to go from the =E2=80=9Cpre-sus= pension=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 siz= e of the *base* of the family. So the pre-suspension is small, but the sus= pension =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 mea= nt to suggest is problematic, not propositional truncation. The latter see= ms 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 cu= bical sets. (I don=E2=80=99t claim originality for this construction; I do= n=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 multip= le 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 modelle= d without a size blowup in any infinite-dimensional model except cubical se= ts, 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 find 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 ve= rtices=E2=80=9D, i.e. a subpresheaf S =E2=89=A4 =CE=94[n] containing all ve= rtices, 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 par= tial 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 under pullback in X. (Straightforward.) (3) In general, a fibration is a proposition in the type-theoretic sense if= f 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-de= generate simplices of Y_n are those whose =E2=80=9Cmissing=E2=80=9D simplic= es 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 m= any 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 t= hen 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 fibrati= ons=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. --=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. --_000_EA45D7F1FC164653B331FA0218FDD5DDchalmersse_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable

 I wrote a short note to confirm Andrew=E2=80= =99s message that indeed this technique 
works as well (using classical logic) for simplicial sets. = This can now be presented
as a combination of various published results. (The origina= lity is only in the presentation;
this essentially follows what is suggested in Andrew=E2=80= =99s message.)
 This provides a semantics of e.g. suspension as an op= eration U -> U, where U
is an univalent universe in the simplicial set model. =

 Thierry


On 7 Jun 2017, at 14:34, Andrew Swan <wakelin.swan@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.  (Am I right in remembering that this has been give= n for cubical sets?  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 not su= re exactly how flexible, but I think I can get suspension to work in simpli= cial sets. In the below, throughout I use the characterisation of fibration= s 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 together with a path from N to S for each element of X (I think thi= s is the same as what you called pre suspension). Although the pre suspensi= on 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 t= he pre suspension.  A map in simplicial sets is a fibration if and onl= y if it has the rlp against each pushout product of a monomorphism with an = endpoint inclusion 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 the structure already present in pre suspension (transport and fla= ttening) and the additional structure added by weak fibrant replacement. Th= e idea is to 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 Lu= msdaine <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.  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.  And adding stronger conditions on the cardinal used won=E2=80=99= t 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 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.  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 suspe= nsion that I meant to suggest is problematic, not propositional truncation.=   The latter seems a bit easier to do by ad hoc constructions; e.g. th= e 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 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 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 bee= n given for cubical sets?  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 blowu= p 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, together 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 ev= ident square commutes;

reindexing acts by taking pullbacks/inverse images of the d= omain 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 operation sending Y to Y =E2=80=94> |Y| =E2=80=94> X is (= coherently) stable up to isomorphism under pullback in X.  (Straightfo= rward.)

(3) In general, a fibration is a proposition in the type-th= eoretic 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 to= o hard to check.)

(4) The map |Y| =E2=80=94> X is a fibration, and a propo= sition.  (Straightforward, given (3), by concretely constructing the r= equired liftings.)

(5) The evident map Y =E2=80=94> |Y| over X is a cell co= mplex constructed from 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 simplices 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&g= t; 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 propos= itional 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 fibrations=E2=80=9D, or the universe of =E2=80=9Cdisplayed =CE= =B1-small fibrations=E2=80=9D, for =CE=B1 any infinite regular cardinal.&nb= sp; Then V carries an operation representing the construction of (1), and m= odelling propositional truncation.  (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.
--_000_EA45D7F1FC164653B331FA0218FDD5DDchalmersse_--