From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC4PDJ5VRELBB7FVZDOQKGQED2UTQBY@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wm1-x338.google.com (mail-wm1-x338.google.com [IPv6:2a00:1450:4864:20::338]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id cde9b486 for ; Mon, 1 Oct 2018 13:02:53 +0000 (UTC) Received: by mail-wm1-x338.google.com with SMTP id y131-v6sf3259509wmd.5 for ; Mon, 01 Oct 2018 06:02:53 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1538398972; cv=pass; d=google.com; s=arc-20160816; b=YTmFufco7R75SQ95TkJ0FCi2MAFlL5Uo/QaU2HsFnPmti3OVoEdLpfglEvbdLMvK6z N1W6lA5g3TydygLxOsiSK07N0pKfJZFO61WEq1CY6qFoAJ8iuY6EA4Uw/m+7dhAj655n e3Qij5zfugNlbdW3ctaBl3pAEEI82MkQu+v1uTv3AUD0eiVzbASUfAcIaGeXJ2GAZctQ /MSCeLeHx9vpN0HoT7kIZJ84PHwuBelUMgGPzMwQwSyDVMbDShw8Dqjd8qX88KX1OAfQ DyC6Z9hGLqP5pWhHbl/zd658UPiu33ZkIxXFd4fPAwq6cF5KMmvIc4CCJ6wCeswVjuUv fTLA== 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:cc:to:from:sender:dkim-signature; bh=9Q7jHbUCxpEjBYCtwo+nVkbU+6O0qpx+zQkthDc2I6Q=; b=bbv2QWs4iTOC+Aicp52KL6Zh7HG5+CGRy+kWmn9Dke9ZAvCCmsyQipBoGZ+KDu03aN 5XgOBX48rq62K+0vsOlHVN2AYxFUOCALTswbZnpiu+lUnxWQMjE+yXRsJ3XYaeP4Hl9z 3RJ6BolaYRuUtGPeiLNQlMObt9jKGtH8c4ubxiH6VRwq6tLYn5biU5dJPFF0hiJaWn7O JcEygzZ3UpH/C/Y8jUb/SPOkkm25y1rXNiLEZ45Z43fBKibwpp1lqHLvrE0jZreF7Tvt pLHW4B/5rvqfOBDWqKTnscR0F1OnEOzZButnB8W/Fvky+z1q006SZ6Sro1J3vW6y0OMT 8mXA== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=neutral (google.com: 129.16.226.136 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:cc: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=9Q7jHbUCxpEjBYCtwo+nVkbU+6O0qpx+zQkthDc2I6Q=; b=TQmNmAMjF499Uz1+JnQRpgNUWqCP9f4nlEt7XIF7ixqzFyBI2R4RFGnz1ela52ZRrk ZHmgO7TMkSV3Zy+elROqtWTflBXX9ZKk8xa28MfqYIO07G/6yvU11yb+ubyOzRj0eXYD Cn51nnK8ljASZEf2u8b5aSsP4nG6797ElHyA4UB1LXVc8blko0zVAI1bqaObJJ0/0PCv 6mXDu+UNkfpnf2Ha2idRy7UCf15URWLL0uibosXNi9efDHddRFn5bwwcqGGcUEAGq5P3 uCeDJCjFbUu7KLMnAjp/BRFa4KLpE9EQtmt3ZTeHMJqt8KfsQ5vLEUGT9v9SnC4wjAKD LLEw== 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:cc: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=9Q7jHbUCxpEjBYCtwo+nVkbU+6O0qpx+zQkthDc2I6Q=; b=OeGdu1JJiuxJHGShh0gkmChz2v3EBkCSDceix+t4p9cALloDtWaor+0UlQD4ClQExA pVMVNI/ecJGI8ORdfnFyQ4zK/YzDYmCjgxqiD7+/WQfFuCjDRwBkqvsa3ji5k3Th/cqk ZnB1RM4kNev6mwDflBP1I0ZcJHX960tZa+NLoG19+aTA5BAXuPLU9t6EuNMX4+7DqSdq yv+3fQBvhawnztZo0xDAPyS7gWQrBTUvulx4A+V6iuMwztbEnlKkLQseGe6Zjk6WCQud VX4iAr3oHBB6NMLfSHrc5CS3kDuE2HJ7j7Y91ofO7Iv2ZIPgQ2Kz996zuiAvCwYrEy/9 G+sA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfohNbhn8gDk/0lUOFgkRtlh4udhIuDyXsu7B7g4+C/fz0AdRUegK IOFSYBFU3bB/vZucBJpT+hQ= X-Google-Smtp-Source: ACcGV60yJfz5BON/D9Ok0o0PCfA2SaVxjg4W6+ABBUBGlZbcyZVfVQM3AHvQ5wu08Sq0976voBoZ4A== X-Received: by 2002:adf:8223:: with SMTP id 32-v6mr130864wrb.4.1538398972843; Mon, 01 Oct 2018 06:02:52 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a7b:c056:: with SMTP id u22-v6ls6596521wmc.2.gmail; Mon, 01 Oct 2018 06:02:52 -0700 (PDT) X-Received: by 2002:a1c:13ce:: with SMTP id 197-v6mr546888wmt.5.1538398972175; Mon, 01 Oct 2018 06:02:52 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1538398972; cv=none; d=google.com; s=arc-20160816; b=Wo0RZWwsoCJvf11MHUzeTizjNhx0kJwdntjv7YbiCx6K+mpRbeAPV36stgJs0CHays 7IyaTcPo2N67OsPgtqmzUldY8olOR87lJloOjyWYN9KDRmDqN65R6PwVa/MQ/XfuzZNo dBPzWpgXJDy2VxHSA/3hAjcrM6V8T1rfbc9SjIL0yMOjoZDqe/1vrEDWkuH1xslXWJHI +2ju+94+4lc6C/kzg+LnTwroTam8olPaEt7l+RtaTl5Ntg8dmfRF+j5mRkE9OpdEQuBZ rVWtqJoWQ4lLDCaEJsESBhb5ywcF+qch47jCnryCPmV+Jddp5Qzm+OeiSrRn+IIKtSis Ug8g== 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:cc:to :from; bh=jIA7gsu3jdYVE8OnHqRt++mJFzaNuaoaIl4FstInOF4=; b=guwouVGsI2VL2a0S3jZnQLADJnJu5w5LPJ5n4GOZSyi0zLFUUOo86+bUbUvxzXXFf5 gFwZ5SdF759ABIQAx+AXp5jC0pGeL8hDCeu7qajBNxHs7MFlpDBy0jEWb5lR0LydapQR NMwRJo1EK3YHolyyLS9D0TSf3Sz6IldYghVJKJx586eqFXRESCho/alCnVdfm7cFERcC AK0AvqjQLNgQ7q3QxuS8yl1NClDQFIZ8+d/10I5+Mnhv6DJrJgVNzWq10To9KlMJwNrZ eNCr1NcPaSquNEyGTyn9OEAU7xgc/nGLidTjT58sbIbbadTifCump3GQ2sTolDMxVCIw em6Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=neutral (google.com: 129.16.226.136 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 baratheon.ita.chalmers.se (baratheon.ita.chalmers.se. [129.16.226.136]) by gmr-mx.google.com with ESMTPS id a8-v6si558627wro.0.2018.10.01.06.02.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Mon, 01 Oct 2018 06:02:52 -0700 (PDT) Received-SPF: neutral (google.com: 129.16.226.136 is neither permitted nor denied by best guess record for domain of thierry.coquand@cse.gu.se) client-ip=129.16.226.136; Received: from tyrell.ita.chalmers.se (129.16.226.132) by baratheon.ita.chalmers.se (129.16.226.136) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.1531.3; Mon, 1 Oct 2018 15:02:51 +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; Mon, 1 Oct 2018 15:02:51 +0200 From: Thierry Coquand To: Andrew Swan CC: Homotopy Type Theory Subject: Re: [HoTT] Semantics of higher inductive types Thread-Topic: [HoTT] Semantics of higher inductive types Thread-Index: AQHS1YRqrYjkQqJDokGDQZgyV4mF/aIP+LoAgAASs4CAAAJcAIAABOQAgAADgYCACQFfgIAAlVoAgti/EgCAADKTAIAaov4A Date: Mon, 1 Oct 2018 13:02:51 +0000 Message-ID: <25DCC554-4E04-47A9-8FEF-789F06C23AE1@chalmers.se> References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> <9F58F820-A54A-46E7-93DC-F814D4BEE0C6@cmu.edu> <33261a39-2351-4e56-a745-204334128862@googlegroups.com> In-Reply-To: <33261a39-2351-4e56-a745-204334128862@googlegroups.com> 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_25DCC5544E0447A98FEF789F06C23AE1chalmersse_" 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.136 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_25DCC5544E0447A98FEF789F06C23AE1chalmersse_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Following the previous note on semantics of HIT in the simplicial set mode= l, I looked a little more at the formal system which is similar to cubical type theory = (based on distributive lattices) but where the filling operation is treated as a -constant- (witho= ut any computation rule). This formal system has models in simplicial and cubical sets. It is possible to show for this system a canonicity theorem, similar to Vo= evodsky=E2=80=99s conjecture: a closed term of type Bool is -path equal- to 0 or 1. (With a similar statement for = natural numbers.) A corollary of this result is that the value of such a closed term is the = same in all models. Hence we know that the computation of such a closed term in various extensions wh= ere we can compute the filling operation will give the same value (and the same value which we= get in simplicial set; so e.g. Brunerie constant has to be +/-2 in the model based on de Morgan algebras). This is proved using the sconing technique as described in https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p= .html As is stated there, the problem for using this technique to solve Voevodsk= y=E2=80=99s conjecture is that there s no apparent way to associate (in a =E2=80=9Cstrict=E2=80=9D way) a simpli= cial/cubical set to a closed type in dependent type theory with identity types. This issue disappears here thanks to the use of higher dimensional syntax. I wrote a proof which is th= e result of several discussions with Simon Huber and Christian Sattler on this topic. The proof can be done effectively using the cubical set mode= l, or non effectively using the simplicial set model. Maybe a similar result can be proved for simplicial/cubical tribes. Thierry On 14 Sep 2018, at 16:16, Andrew Swan > wrote: Thanks for writing out the note. I'll also make a few remarks about how my = more recent work connects with these things. 1. The initial Susp X algebras, and I think in fact all of the initial alge= bras appearing in the Coquand-Huber-Mortberg paper, can be constructed by c= ombining finite colimits and W types with reductions (as appearing in this = paper). From this it follows that they ex= ist not just in cubical sets and simplicial sets, but any topos that satisf= ies WISC, and for the special case of presheaf categories with locally deci= dable cofibrations they can be constructed without using WISC or exact quot= ients. I think the latter can be viewed as a generalisation of the Coquand-= Huber-Mortberg definition. 2. In my post and again in the W-types with reductions paper I suggested us= ing Christian's generalised notion of lifting property for commutative squa= res. I still think this works, but I now lean towards other ways of looking= at it. I didn't really emphasise this in the paper, but it follows from th= e 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 given a map f = : X -> Y, we can either view it as a map in the slice category C/1 and fact= orise it there or as a map into the terminal object in the slice category C= /Y. The latter is necessarily stable under pullback, and I think 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 argument. In this case the proofs in th= e Coquand-Huber-Mortberg paper generalise pretty much directly with very li= ttle modification. 3. I still find the situation in simplicial sets a little strange, in parti= cular the need to switch back and forth between the different notions of fi= bration, although it does work as far as I can tell. 4. I made some remarks before about universal lifting problems. These now a= ppear in the paper Lifting Problems in Grothendieck Fibrations . Best, Andrew On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote: 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. -- 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. --=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_25DCC5544E0447A98FEF789F06C23AE1chalmersse_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable
 Following the previous note on semantics of HIT in th= e simplicial set model, I looked
a little more at the formal system which is similar to cubi= cal type theory (based on distributive
lattices) but where the filling operation is treated as a -= constant- (without any  computation rule).

 This formal system has models in simplicial and cubic= al sets.

 It is possible to show for this system a canonicity t= heorem, similar to Voevodsky=E2=80=99s conjecture: a closed
term of type Bool is -path equal- to 0 or 1. (With a simila= r statement for natural numbers.)

 A corollary of this result is that the value of such = a closed term is the same in all models. Hence
we know that the computation of such a closed term in vario= us extensions where we can compute
the filling operation will give the same value (and the sam= e value which we get in simplicial set; so e.g. 
Brunerie constant has to be +/-2 in the model based on = de Morgan algebras).

 This is proved using the sconing technique as describ= ed in

https://golem.ph.utexas.edu/ca= tegory/2013/04/scones_logical_relations_and_p.html

 As is stated there, the problem for using this techni= que to solve Voevodsky=E2=80=99s conjecture is that there
s no apparent way to associate (in a =E2=80=9Cstrict=E2=80= =9D way) a simplicial/cubical set to a closed type in dependent 
type theory with identity types. 

 This issue disappears here thanks to the use of highe= r dimensional syntax.

 I wrote a proof which is the result of several discussions with Simon Huber = and Christian Sattler
on this topic. The proof can be done effectively using the = cubical set model, or non effectively using the simplicial
set model.
 Maybe a similar result can be proved for simplicial/c= ubical tribes.

 Thierry


On 14 Sep 2018, at 16:16, Andrew Swan <wakelin.swan@gmail.com> wrote:
Thanks for writing out the note. I'll also make a few remarks about how my = more recent work connects with these things.

1. The initial Susp X algebras, and I think in fact all of = the initial algebras appearing in the Coquand-Huber-Mortberg paper, can be = constructed by combining finite colimits and W types with reductions (as ap= pearing in this paper). From this 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 categories with locally decidable cofibrations they can b= e constructed without using WISC or exact quotients. I think the latter can be viewed as a generalisation o= f the Coquand-Huber-Mortberg definition.

2. In my post and again in the W-types with reductions pape= r I suggested using Christian's generalised notion of lifting property for = commutative squares. I still think this works, but I now lean towards other= ways of looking at it. I didn't really emphasise this in the paper, but it follows from the general theory that o= ne 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 fibrat= ion for each slice category C/Y. Then given a map f : X -> Y, we can either view it as a map in the slic= e category C/1 and factorise it there or as a map into the terminal object = in the slice category C/Y. The latter is necessarily stable under pullback,= and I think works out the same as "freely adding a homogeneous filling operator."

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

3. I still find the situation in simplicial sets a little s= trange, in particular the need to switch back and forth between the differe= nt notions of fibration, although it does work as far as I can tell.

4. I made some remarks before about universal lifting probl= ems. These now appear in the paper Lifting Problems in Grothendieck Fibrations .=

Best,
Andrew


On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote:

 I wrote a short note=  to confirm Andrew=E2=80=99s message that indeed this technique&nb= sp;
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 <wakel= i...@gmail.com> wrote:<= /div>
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><= /span> wrote:
On Thu, Jun 1, 2017 at 6:56 PM= , Steve Awodey <awo...@cmu.edu> wr= ote:
>
> 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 &quo= t;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an ema= il to HomotopyTypeTheory+unsubscribe@googlegrou= ps.com.
For more options, visit https://groups.google.com/d/optout.<= /div>

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