From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, 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-ot1-x33b.google.com (mail-ot1-x33b.google.com [IPv6:2607:f8b0:4864:20::33b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4927533b for ; Sat, 10 Nov 2018 15:52:07 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id h1sf3242706oti.6 for ; Sat, 10 Nov 2018 07:52:07 -0800 (PST) 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=K8UV3/5aau/wMm50LqnkrdD1dNsviz8+MZznTVyg8NQ=; b=Z2DdqAJzo3F3nQigo1fCJFzkub6J5JhH+5EPTpi965b+3keiGQsDtFQEtgPXjo2Fw0 LA3ityRDba0KsnAxxT0U7cIQGZo2f6mki3EGbRwhnnyoKxT2Ymi8oXhCU7OYxNhgRzD9 26Ryht4R85NHkpNZV1HWoExoyqdRdy1EDbDs+handmZZ9ZHcu50YvanG7pZuEM22s6oe al9YPhYLLpw2J5qb4/SRutlXq/qR3eWzwUfj7WbK51Cez6yTbp1acmRN8ugxTgwQYo7J aBcuJtfwC9SPc7wnAMUl46pQOs8z4ikO/bDqLvnrlCNb/AgDQH5vnlFTRZErloAfJYrH KMGw== 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=K8UV3/5aau/wMm50LqnkrdD1dNsviz8+MZznTVyg8NQ=; b=LIc+2kFy5z6XKbGX1zXD/bdTmFM0+O05cMZgEDSaFtM3UWfD7LPN2tnDF3ie8BaZv0 80RyHoqQu0Zq9GsoYus9nXMn1r7phWrZOUdxLs+1Bvsg2ebEFG0b4cgyIkceVTRsOfYz dqyjqR6d94GYugU0dJohDIStKBfs7Jyo3g4yEjHn9DQkxmFidAYqJ1R0dnI7UJhOFLgI gfvgxh+oXD4ytQWMdyLJd7GiF8+b3E5t/N2cUeQybAiCeHVPv7pzjwbAzfP4d2sZ2rDT xlYEnxP6lNsDfLSjos2O9fORQueZqpochytAybo62AHWSV+dKWK6fTwjvBJDiwD4qULa R+IQ== 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=K8UV3/5aau/wMm50LqnkrdD1dNsviz8+MZznTVyg8NQ=; b=VXlwdPertOvHg7PDT8VkNQjQ6qC3bG+VKw7xApge/0j5nUjWvpyG1Wh5RswawavRnP jKhZaiSbxWxaSVmTSEqPGoCC4F0C/BZiO5EaUy+iSOU09NMg5ZnRpSRAyTIurK6q8IQb fJa8nkiPMBN0Q/jP6/wn9OOZ7kwRP0L4M4ELJt8CXKMY9UiSLaYppqVbEGH1jpKOy97P rrf/tk586UVbtXNNW8qKmEY4LIcv34dCHelRCznjmeP/xX7yzrZQMxx5myme9PbFHzd1 vk6zBRSDZDG06PcfIcPcr5yGIZNmrwj3wD73tAGK6yEjGWqMP1LXnJUw7gZ3K+s2zCru qyIg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gL88lLHrAwL+q3bVZrM7bgNBGYf68/csrLPxhBevpYmtofJT+Ky 4SP450nZYorE88z+g0GxKG4= X-Google-Smtp-Source: AJdET5foHe/JKLyngD+B5bqJTj2n4pbsIvLyDQOnUyIC1JPPJ7eZSPQKL+Rgb1amUewRWsPRtfrYJw== X-Received: by 2002:a9d:2c22:: with SMTP id f31mr26560otb.4.1541865124989; Sat, 10 Nov 2018 07:52:04 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:760a:: with SMTP id k10ls1984204otl.3.gmail; Sat, 10 Nov 2018 07:52:04 -0800 (PST) X-Received: by 2002:a9d:5ad:: with SMTP id 42mr167336otd.0.1541865124196; Sat, 10 Nov 2018 07:52:04 -0800 (PST) Date: Sat, 10 Nov 2018 07:52:03 -0800 (PST) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: <7cb8b1b0-482a-41a5-98ce-b6014f750712@googlegroups.com> In-Reply-To: <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> <25DCC554-4E04-47A9-8FEF-789F06C23AE1@chalmers.se> Subject: Re: [HoTT] Semantics of higher inductive types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1302_1738435546.1541865123361" X-Original-Sender: andersmortberg@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_1302_1738435546.1541865123361 Content-Type: multipart/alternative; boundary="----=_Part_1303_220548040.1541865123361" ------=_Part_1303_220548040.1541865123361 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable This is very exciting!=20 Around the time when Thierry sent his message I did a little experiment=20 where I made comp compute to a value in cubicaltt (this means that it is=20 not defined by cases on the type as in the CCHM paper): https://github.com/mortberg/cubicaltt/tree/compval What I then realized was that the full proof of univalence (using that=20 unglue is an equivalence) goes through as it is: https://github.com/mortberg/cubicaltt/blob/compval/examples/compval.ctt#L33= 0 The same holds for the proof of univalence using Id everywhere. This was a= =20 bit surprising to me at first as it shows that none of the computation=20 rules for comp by case on the type matter in these proofs (note that we=20 still have the equations for how "comp^i A [phi -> u] u0" computes under=20 phi : FF). However some proofs did of course break, for example the direct= =20 proof of "uabeta" which relies on how comp in Glue computes in the CCHM=20 cubical set model.=20 So it seems to me like the system that Thierry describes in his message has= =20 many very good properties that have been missing or are unknown from the=20 proposed type theories for univalent type theory so far, in particular: - It has a model in Kan simplicial sets and a constructive model in=20 ("Dedekind"/distributive lattice) cubical sets - It satisfies homotopy canonicity so that we know that all terms of type= =20 nat "compute" to the same numerals in these models - It has Id types (with strict computation for J) and univalence is a=20 theorem for these types - As comp doesn't compute the implementation of the type theory is much=20 simpler and type checking is very fast compared to regular cubicaltt The only downside is that it doesn't have "strict" canonicity (not all=20 closed terms of type nat are judgmentally equal to a numeral), but I don't= =20 think that this is too much of a problem in practice as we can implement a= =20 closed term evaluator inspired by the cubical set model for computing these= =20 numerals (much like how Coq has vm/native_compute for efficient computation= =20 of closed terms). Finally my little experiment indicates that having a comp= =20 which doesn't compute doesn't affect the practical usability of this system= =20 too much either. -- Anders PS: Note that I didn't remove reversals in my small experiment as it would= =20 require a bit more hacking and I didn't have time to do it, but there is no= =20 fundamental problem in doing this and from my experience with cartesian=20 cubical type theory it is not too bad in practice either (we would drop=20 reversals and instead have comp 0->1 and comp 1->0).=20 On Monday, October 1, 2018 at 9:02:53 AM UTC-4, coquand wrote: > > Following the previous note on semantics of HIT in the simplicial set=20 > model, I looked > a little more at the formal system which is similar to cubical type theor= y=20 > (based on distributive > lattices) but where the filling operation is treated as a -constant-=20 > (without 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= =20 > Voevodsky=E2=80=99s conjecture: a closed > term of type Bool is -path equal- to 0 or 1. (With a similar statement fo= r=20 > natural numbers.) > > A corollary of this result is that the value of such a closed term is th= e=20 > same in all models. Hence > we know that the computation of such a closed term in various extensions= =20 > where we can compute > the filling operation will give the same value (and the same value which= =20 > we get in simplicial set; so e.g.=20 > 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=20 > Voevodsky=E2=80=99s conjecture is that there > s no apparent way to associate (in a =E2=80=9Cstrict=E2=80=9D way) a simp= licial/cubical=20 > set to a closed type in dependent=20 > type theory with identity types.=20 > > This issue disappears here thanks to the use of higher dimensional synta= x. > > I wrote a proof which is= =20 > the result of several discussions with Simon Huber and Christian Sattler > on this topic. The proof can be done effectively using the cubical set=20 > model, 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 >= =20 > wrote: > > Thanks for writing out the note. I'll also make a few remarks about how m= y=20 > more recent work connects with these things.=20 > > 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 constructe= d=20 > by combining finite colimits and W types with reductions (as appearing in= this=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 follow= s=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 notio= n=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=20 > directly, without going via the small object argument. In this case the= =20 > proofs in the Coquand-Huber-Mortberg paper generalise pretty much directl= y=20 > with very 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 notion= s=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:=20 >> >> >> 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= =20 >> be presented >> as a combination of various published results. (The originality is only= =20 >> 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,=20 >> where U >> is an univalent universe in the simplicial set model.=20 >> >> Thierry >> >> >> On 7 Jun 2017, at 14:34, Andrew Swan wrote: >> >> 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 withou= t 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 al= so=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 = as=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 expe= ct=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= =20 >> map in simplicial sets is a fibration if and only if it has the rlp agai= nst=20 >> each pushout product of a monomorphism with an endpoint inclusion into t= he=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 = for=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 projecti= on=20 >> B x I -> B. I think there are two ways to ensure that the operation of w= eak=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 uniformi= ty=20 >> condition above is in the definition. The intuitive reason why this shou= ld=20 >> be stable is that the problem that stops the usual fibrant replacement f= rom=20 >> being stable is that e.g. when we freely add the transport of a point al= ong=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 o= nly=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) a= nd=20 >> the additional structure added by weak fibrant replacement. The idea is = to=20 >> follow the same proof as for cubical type theory. It is enough to just s= how=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 fin= d=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 flatten= ing=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 ad= ding stronger=20 >>>> conditions on the cardinal used won=E2=80=99t help. The problem is th= at one takes=20 >>>> a fibrant replacement to go from the =E2=80=9Cpre-suspension=E2=80=9D = to the suspension=20 >>>> (more precisely: a (TC,F) factorisation, to go from the universal fami= ly 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 = although=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 d= oes=20 >>> it in simplicial sets, and I think a similar thing may work also in cub= ical=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 peopl= e=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 withou= t 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 follo= ws: >>> >>> an element of |Y|_n consists of an n-simplex x : =CE=94[n] =E2=80=94> X= , together=20 >>> with a =E2=80=9Cpartial lift of x into Y, defined at least on all verti= ces=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 = map). >>> >>> (2) There=E2=80=99s an evident map Y =E2=80=94> |Y| over X; and the ope= ration sending Y=20 >>> to Y =E2=80=94> |Y| =E2=80=94> X is (coherently) stable up to isomorphi= sm under pullback in=20 >>> X. (Straightforward.) >>> >>> (3) In general, a fibration is a proposition in the type-theoretic sens= e=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 construct= ed 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 simpli= ces 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 o= f =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 fibrati= ons,=20 >>> stably in X. (Orthogonality is immediate from (3) and (5); stability i= s=20 >>> then by (2).) >>> >>> (7) Let V be either the universe of =E2=80=9Cwell-ordered =CE=B1-small = fibrations=E2=80=9D,=20 >>> or the universe of =E2=80=9Cdisplayed =CE=B1-small fibrations=E2=80=9D,= for =CE=B1 any infinite=20 >>> regular cardinal. Then V carries an operation representing the=20 >>> construction of (1), and modelling propositional truncation. (Lengthy = to=20 >>> 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= =20 > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= =20 > email 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. ------=_Part_1303_220548040.1541865123361 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
This is very exciting!

= Around the time when Thierry sent his message I did a little experiment whe= re I made comp compute to a value in cubicaltt (this means that it is not d= efined by cases on the type as in the CCHM paper):

https://github.com/mortberg/cubicaltt/tree/compval

What I then realized was that the full proof of univalence (using tha= t unglue is an equivalence) goes through as it is:

https://github.com/mortberg/cubicaltt/blob/compval/examples/compval.ctt#L3= 30

The same holds for the proof of univalence usin= g Id everywhere. This was a bit surprising to me at first as it shows that = none of the computation rules for comp by case on the type matter in these = proofs (note that we still have the equations for how "comp^i A [phi -= > u] u0" computes under phi : FF). However some proofs did of cours= e break, for example the direct proof of "uabeta" which relies on= how comp in Glue computes in the CCHM cubical set model.

So it seems to me like the system that Thierry= describes in his message has many very good properties that have been miss= ing or are unknown from the proposed type theories for univalent type theor= y so far, in particular:

- It has a model in Kan s= implicial sets and a constructive model in ("Dedekind"/distributi= ve lattice) cubical sets

- It satisfies homot= opy canonicity so that we know that all terms of type nat "compute&quo= t; to the same numerals in these models

- It= has Id types (with strict computation for J) and univalence is a theorem f= or these types

- As comp doesn't compute the implemen= tation of the type theory is much simpler and type checking is very fast co= mpared to regular cubicaltt


The= only downside is that it doesn't have "strict" canonicity (n= ot all closed terms of type nat are judgmentally equal to a numeral), but I= don't think that this is too much of a problem in practice as we can i= mplement a closed term evaluator inspired by the cubical set model for comp= uting these numerals (much like how Coq has vm/native_compute for efficient= computation of closed terms). Finally my little experiment indicates that = having a comp which doesn't compute doesn't affect the practical us= ability of this system too much either.

--
Anders

PS: Note that I didn't remo= ve reversals in my small experiment as it would require a bit more hacking and I didn't have time to do it, but there= =20 is no fundamental problem in doing this and from my experience with=20 cartesian cubical type theory it is not too bad in practice either (we woul= d drop reversals and instead have comp 0->1 and comp 1->0).


On Monday, October 1, 2018 at 9:02:53 AM UTC= -4, coquand wrote:
=C2=A0Following the previous note on semantics of HIT in the simplicia= l set model, I looked
a little more at the formal system which is similar to cubical type th= eory (based on distributive
lattices) but where the filling operation is treated as a -constant- (= without any =C2=A0computation rule).

=C2=A0This formal system has models in simplicial and cubical sets.

=C2=A0It is possible to show for this system a canonicity theorem, sim= ilar to Voevodsky=E2=80=99s conjecture: a closed
term of type Bool is -path equal- to 0 or 1. (With a similar statement= for natural numbers.)

=C2=A0A corollary of this result is that the value of such a closed te= rm is the same in all models. Hence
we know that the computation of such a closed term in various extensio= ns where we can compute
the filling operation will give the same value (and the same value whi= ch we get in simplicial set; so e.g.=C2=A0
Brunerie constant has to be +/-2 in the model based on de Morgan algeb= ras).

=C2=A0This is proved using the sconing technique as described in


=C2=A0As is stated there, the problem for using this technique to solv= e Voevodsky=E2=80=99s conjecture is that there
s no apparent way to associate (in a =E2=80=9Cstrict=E2=80=9D way) a s= implicial/cubical set to a closed type in dependent=C2=A0
type theory with identity types.=C2=A0

=C2=A0This issue disappears here thanks to the use of higher dimension= al syntax.

=C2=A0I wrote a proof=C2=A0which 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.
=C2=A0Maybe a similar result can be proved for simplicial/cubical trib= es.

=C2=A0Thierry


On 14 Sep 2018, at 16:16, Andrew Swan <wakeli...@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 appearing in<= span>=C2=A0this 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 paper I suggest= ed using Christian's generalised notion of lifting property for commuta= tive squares. I still think this works, but I now lean towards other ways o= f 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 reductions dire= ctly, without going via the small object argument. In this case the proofs = in the Coquand-Huber-Mortberg paper generalise pretty much directly with ve= ry little modification.

3. I still find the situation in simplicial sets a little strange, in = particular 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=A0Lifting Problems in Grothendi= eck Fibrations=C2=A0.

Best,
Andrew


On Friday, 14 September 2018 13: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> wro= te:

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=C2=A0<p.l.lu...@gmail.co= m>=C2=A0wrote:
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.





--=C2=A0
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=C2=A0Homo= topyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit=C2=A0https://groups.google.com/d/o= ptout.

--
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_1303_220548040.1541865123361-- ------=_Part_1302_1738435546.1541865123361--