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-pl1-x63e.google.com (mail-pl1-x63e.google.com [IPv6:2607:f8b0:4864:20::63e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0e82621f for ; Sat, 10 Nov 2018 18:12:13 +0000 (UTC) Received: by mail-pl1-x63e.google.com with SMTP id 34-v6sf3718236plf.6 for ; Sat, 10 Nov 2018 10:12:13 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541873532; cv=pass; d=google.com; s=arc-20160816; b=yvIAvPLWHrnI9IAetlE4qkV8w+ki71rSqgRpnVPWKFC7AAbG9ivhIaVSP6oViYZXoC ADqVhGoLmUyiEzhEYSPb/xvCIWaSs/cxDRqzTZmxRzPnCvsnmoYqLrPyUSffn04Y1HBD 8zQButPxVdhEp9CuSw0tJnPOPta/TVoAMzuCcsEhqslnAcrgUQsdRYaQ0xM7KhM7BAKQ E7F8+2ynGd1ePRUuYJxUKOVd4Wwgzer3XJxDEIatCUg+Dr4EqM983AkOuOf97/t/avXP dVXgX1RLbPYjn6WL/8aHM3qTmpORnnWmwwF3W4J0B+UDBisXX1Py1OWuJzFozaNXyCyg bIlg== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=VhJv2Lf/oY7j3uqMTnStLM5ozgm5zRqgyQ5ln3ok28g=; b=ZbZ7JbsjMwrLDuvfuJpa5N6+THDwJTOE6Pq8R35bI2GPtOGdvJe7HqL3K0hkrdSmbi oGdF2GROCBwIEsaTbQwBZ2iSYOUAO+EbVQpKU5NeLiTtATfi0dqAmavBzxzWT6rqdG/a MPmJd0Q+prJnZ7gtFgSUYQnLTguEDyjAOJjr+3Gci48Vad6/5X5NX78nSkOcVPkbk2NT +LIQARRvBqkv1QbUZ3mEmiRq31wJBzOuW6c3PSoACxv0iyg9HfcoNR/9Wsp4iYZqww8I EdAAvqinBZdy1tmrRTWAppZ6aI/3bjcS8LwrCBVN6kco5nkqFeKQ5LKgBzlLvFCHgazM F9cA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=k3oyJ3yM; spf=pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::731 as permitted sender) smtp.mailfrom=gabriel.scherer@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=VhJv2Lf/oY7j3uqMTnStLM5ozgm5zRqgyQ5ln3ok28g=; b=YmLpb0WuW6fQy4mMBerMnQSXCgbWys+gnRb9cwacsZwtnm7uhq8A80OhLJ6rKcUU7J bm4tIZbNKK7KJlQuh63UQE+p1W7AOpFoFgekTZqPfhEY2i+KPSiYdYj84jbgkcafj7Eb LksHppDRs9gu6lArbgHJUxufe2NUhEDx682a8uRsO5IM+2vEx0Pn9XP7HLsL6s9BnYON q8EvHM8zvtcZF2fTjQ79cf8g9UNnhqWlGUAhTLzpva6+R5c2T4SZPYKc7ylkgfSM93Go IHpiD7no5yO9NzqecrKQSdCi+NAL6MWzr0E6vl5H6bLLJ0kOaMPLONnej8MRdOb+UY3M mlvg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=VhJv2Lf/oY7j3uqMTnStLM5ozgm5zRqgyQ5ln3ok28g=; b=UjkecDKxgRPGEd2zs42PXhvo7csZiQlcPTZcCzAC6HMZkSNoFlrsH7Py6qfJ+nKbpb y15B26aFwO2PXyBEBtibiqaRSxW+xbq+l8Ygm6IdA1s/LfkRXFUoOEddalhtwq7wHNxW 2ZqvacBuORp24OcFSQiUsPMRmh49tXsv/mCctyYcGN5Nr18OO4DmI4NmNjpQhXK2O2VH SwsmdUIRI6YGyXV23deXqfpdr1uvjHj2eC7LQRKMt/L5AhOpy1buFqTrPYzRx4W8rEP0 YC2I6WOBZE3G5CsaHmmsjZDypyGRouknd8XVd6VyTKY1okEW6IzKWvAJXvNVUwyhUWUE 3ZdQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=VhJv2Lf/oY7j3uqMTnStLM5ozgm5zRqgyQ5ln3ok28g=; b=H2VgcEAYBd5fmO/9c10jrPIjF1xLEZFz6Zt1TcGaw2DYT0pMeBbT686b/rEeIO9HvS 7KQx0IDAQAN/L4w+hgeQL0/aRh+yZjC/E0Hq7DwhgxTQmamY56HPjW7rHXwwhnE3UmST JdxuJAzFpDcNVV/vMtlvsg/VvHoG6/TThhsHjTwysIp1Rl1zejdm7zURpZlf0WZTX2EA GKflNJlYEZbCKzkac/BI6bvrJju0zJq8vfwaItw6SNUysDkeAYXjaL6GwoPBwkU4GNJ9 PKalF0hm0wXOtol9QKMDJ6XihSEiUAdsazJoFviIOyR6TYt6oi5jXpKIglsdRygipOsX 6A4w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIiPCXMm/Xv6b+QeFMYkFAmdo+CpgPIRmWIqS4mgp+u/HcMIelk w5X1CSkXRkPTumVJIJZV0gI= X-Google-Smtp-Source: AJdET5dYImt7beopNWC1gq2dxiD1pmSx4cKmG7Sbx6KH5dG2TsGVFRjm7vE9nihf6i1uU5Q/JcUkXA== X-Received: by 2002:a63:6158:: with SMTP id v85mr38412pgb.7.1541873531885; Sat, 10 Nov 2018 10:12:11 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:4692:: with SMTP id o18-v6ls1652310pfi.11.gmail; Sat, 10 Nov 2018 10:12:11 -0800 (PST) X-Received: by 2002:a63:d813:: with SMTP id b19mr1369214pgh.85.1541873531331; Sat, 10 Nov 2018 10:12:11 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541873531; cv=none; d=google.com; s=arc-20160816; b=GmQIwUjVpfAxfHPxK10UU0SsYBkJG1E7FjXOXASKTdAxugkoz8qhMqPGn4nokbCdLg AqjO1rK+8Sx2XidJ//+NnhGlJODNuCO/QHy4nAXSAH5Gg4DtyonwwMKdMD5BvKe/pyrF U0Itv7LNomjeEH0dwSJ9kn6BbhVRUwAZ5GZF7vCNwHwRHgZt2Odt1dnkuYaV7S/pKBj/ 3BYg7ZS1SYyuoGkPfHfcqyCqLNOYqPTFH61D/wycYUS3E84QhUIAlyqB7oNYJ05ZK8ZS nXG8oNBRVuUdRPHkHh1oxdBxvRpbXApaNhRN2SoT6zWN4pFzOanqEVDrq0LDcu/34HGS V3rQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=iYo2CZeYcQOzKEeNxqjj5O/Rmwqz6iXrGqbqCqiXnis=; b=mvqXiP/E741jKHGOgD49ytOCN+ZVinBMI6xBXwraMldqt8qmuLzsm6Y15I+bmOd6xC M0ZmVnzkLAJ1vQt1qRvhNED3lWAoq7TfDUFj0VB/RTsFT13+KdaWaQEC/8NpQkCMTX7s Oqnk+Ni4eVeSSwj1SCUgYgb1TgreqdS9tZsrJXlrrnbQv0xciDerVGmD4SqXpqZsfh3T YfBHP+23jO2TE5lxvMgFsoZdl4yGgiWm8BmRVnnKhmSySTT2UKHGPB1l/S2EiBWRi88T 8NYEKXn8mmcKSxDRvjDzJ/HwHLVOeIw8rrvXCxSieH2GcvWV/QCqz0uaSbUPf/5Tj15f /Xqw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=k3oyJ3yM; spf=pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::731 as permitted sender) smtp.mailfrom=gabriel.scherer@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qk1-x731.google.com (mail-qk1-x731.google.com. [2607:f8b0:4864:20::731]) by gmr-mx.google.com with ESMTPS id o9-v6si415522pfi.5.2018.11.10.10.12.11 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 10 Nov 2018 10:12:11 -0800 (PST) Received-SPF: pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::731 as permitted sender) client-ip=2607:f8b0:4864:20::731; Received: by mail-qk1-x731.google.com with SMTP id o89so7160961qko.0 for ; Sat, 10 Nov 2018 10:12:11 -0800 (PST) X-Received: by 2002:a37:2b5b:: with SMTP id r88mr13086665qkh.336.1541873530843; Sat, 10 Nov 2018 10:12:10 -0800 (PST) MIME-Version: 1.0 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> <7cb8b1b0-482a-41a5-98ce-b6014f750712@googlegroups.com> In-Reply-To: <7cb8b1b0-482a-41a5-98ce-b6014f750712@googlegroups.com> From: Gabriel Scherer Date: Sat, 10 Nov 2018 19:21:34 +0100 Message-ID: Subject: Re: [HoTT] Semantics of higher inductive types To: andersmortberg@gmail.com Cc: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000183a27057a536899" X-Original-Sender: gabriel.scherer@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=k3oyJ3yM; spf=pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::731 as permitted sender) smtp.mailfrom=gabriel.scherer@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --000000000000183a27057a536899 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I wouldn't compare your proposal (if I understand it correctly) with vm_compute and native_compute, which only make reductions that are valid for Coq's beta-reduction. They are implemented differently and reduce terms in different ways, but they must not change the theory of equality of the system. On Sat, Nov 10, 2018 at 4:52 PM Anders M=C3=B6rtberg wrote: > This is very exciting! > > Around the time when Thierry sent his message I did a little experiment > where I made comp compute to a value in cubicaltt (this means that it is > 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 > unglue is an equivalence) goes through as it is: > > > https://github.com/mortberg/cubicaltt/blob/compval/examples/compval.ctt#L= 330 > > The same holds for the proof of univalence using 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 course break, for example the direc= t > 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 missing or are unknown from > the proposed type theories for univalent type theory so far, in particula= r: > > - It has a model in Kan simplicial sets and a constructive model in > ("Dedekind"/distributive lattice) cubical sets > > - It satisfies homotopy canonicity so that we know that all terms of type > nat "compute" to the same numerals in these models > > - It has Id types (with strict computation for J) and univalence is a > theorem for these types > > - As comp doesn't compute the implementation of the type theory is much > simpler and type checking is very fast compared to regular cubicaltt > > > The only downside is that it doesn't have "strict" canonicity (not 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 implement = a > closed term evaluator inspired by the cubical set model for computing the= se > numerals (much like how Coq has vm/native_compute for efficient computati= on > of closed terms). Finally my little experiment indicates that having a co= mp > which doesn't compute doesn't affect the practical usability of this syst= em > too much either. > > -- > Anders > > PS: Note that I didn't remove reversals in my small experiment as it woul= d > require a bit more hacking and I didn't have time to do it, but there is = no > fundamental problem in doing this and from my experience with cartesian > cubical type theory it is not too bad in practice either (we would 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: >> >> Following the previous note on semantics of HIT in the simplicial set >> model, 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- >> (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 >> 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.) >> >> 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 >> where 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_an= d_p.html >> >> As is stated there, the problem for using this technique 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 sim= plicial/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 >> 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/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 >> algebras appearing in the Coquand-Huber-Mortberg paper, can be construct= ed >> by combining finite colimits and W types with reductions (as appearing i= n >> this paper ). From this it follows >> that they exist not just in cubical sets and simplicial sets, but any to= pos >> that satisfies WISC, and for the special case of presheaf categories wit= h >> locally decidable cofibrations they can be constructed without using WIS= C >> or exact quotients. 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 >> 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 follo= ws >> from the general theory that one obtains not just an awfs, but a fibred >> awfs over the codomain fibration. This gives an awfs, and thereby a noti= on >> 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 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 >> directly, without going via the small object argument. In this case the >> proofs in the Coquand-Huber-Mortberg paper generalise pretty much direct= ly >> with very 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 notio= ns >> of fibration, although it does work as far as I can tell. >> >> 4. I made some remarks before about universal lifting problems. These no= w >> 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 >>> 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 modelled witho= ut a size >>>> blowup in any infinite-dimensional model except cubical sets, under an= y of >>>> the approaches to modelling HIT=E2=80=99s proposed so far. (Am I righ= t in >>>> remembering that this has been given for cubical sets? I can=E2=80=99= t 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 no= t >>> sure exactly how flexible, but I think I can get suspension to work in >>> simplicial sets. In the below, throughout I use the characterisation of >>> fibrations as maps with the rlp against the pushout product of each >>> monomorphism with endpoint inclusion into the interval. WLOG there is a= lso >>> 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 togethe= r >>> with a path from N to S for each element of X (I think this is the same= 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 exp= ect >>> 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 fibr= e 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 transport along p of q(0) that lies entirely in the fibre o= f >>> 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 aga= inst >>> each pushout product of a monomorphism with an endpoint inclusion into = the >>> interval. In fibrant replacement you freely add a diagonal lift for eac= h >>> 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 inclusion always has codomain B x I - then only conside= r >>> those lifting problems where the bottom map factors through the project= ion >>> B x I -> B. I think there are two ways to ensure that 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 uniform= ity >>> condition above is in the definition. The intuitive reason why this sho= uld >>> be stable is that the problem that stops the usual fibrant replacement = from >>> being stable is that e.g. when we freely add the transport of a point a= long >>> a path, p we are adding a new element to the fibre of p(1) which depend= s 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 in 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 flattening) = and >>> the additional structure added by weak fibrant replacement. The 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 fi= nd >>> the composition. (And I think that last part should be an instance of a >>> general result along the lines of "if the monad of transport and flatte= ning >>> distributes over a monad, then the fibrant replacement monad distribute= s >>> 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: >>>> >>>> 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 migh= t >>>>> lead to cardinals outside of a Grothendieck Universe? >>>>> >>>>> Exactly, yes. There=E2=80=99s no reason I know of to think they *nee= d* to, >>>>> but with the construction of Mike=E2=80=99s and my paper, they do. A= nd adding >>>>> stronger conditions on the cardinal used won=E2=80=99t help. The pro= blem is that >>>>> one takes a fibrant replacement to go from the =E2=80=9Cpre-suspensio= n=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 s= ize 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 suspension that = I meant >>>> to suggest is problematic, not propositional truncation. The latter s= eems >>>> a bit easier to do by ad hoc constructions; e.g. the construction belo= w >>>> 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 constructio= n; I don=E2=80=99t >>>> think I learned it from anywhere, but I do recall discussing it with p= eople >>>> who were already aware of it or something similar (I think at least Mi= ke, >>>> Thierry, and Simon Huber, at various times?), so I think multiple peop= le >>>> 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 witho= ut a size >>>> blowup in any infinite-dimensional model except cubical sets, under an= y of >>>> the approaches to modelling HIT=E2=80=99s proposed so far. (Am I righ= t in >>>> remembering that this has been given for cubical sets? I can=E2=80=99= t 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 foll= ows: >>>> >>>> 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 vert= ices=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 evident square 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= map). >>>> >>>> (2) There=E2=80=99s an evident map Y =E2=80=94> |Y| over X; and the op= eration sending Y >>>> to Y =E2=80=94> |Y| =E2=80=94> X is (coherently) stable up to isomorph= ism under pullback in >>>> X. (Straightforward.) >>>> >>>> (3) In general, a fibration is a proposition in the type-theoretic >>>> 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 too hard to check.) >>>> >>>> (4) The map |Y| =E2=80=94> X is a fibration, and a proposition. >>>> (Straightforward, given (3), by concretely constructing the required >>>> liftings.) >>>> >>>> (5) The evident map Y =E2=80=94> |Y| over X is a cell complex construc= ted 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 simpl= ices 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 fibrat= ions, >>>> 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. 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >> >> >> -- > 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 > 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. --000000000000183a27057a536899 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I wouldn't compare your proposal (if I understand it c= orrectly) with vm_compute and native_compute, which only make reductions th= at are valid for Coq's beta-reduction. They are implemented differently= and reduce terms in different ways, but they must not change the theory of= equality of the system.

On Sat, Nov 10, 2018 at 4:52 PM Anders M=C3=B6rtberg <andersmortberg@gmail.com> wrote= :
This is ver= y exciting!

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


What I then reali= zed was that the full proof of univalence (using that unglue is an equivale= nce) goes through as it is:


The same holds for the proof of = univalence using 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 m= atter in these proofs (note that we still have the equations for how "= comp^i A [phi -> u] u0" computes under phi : FF). However some proo= fs did of course 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 syst= em that Thierry describes in his message has many very good properties that= have been missing or are unknown from the proposed type theories for univa= lent type theory so far, in particular:

- It has a= model in Kan simplicial sets and a constructive model in ("Dedekind&q= uot;/distributive lattice) cubical sets

- It = satisfies homotopy canonicity so that we know that all terms of type nat &q= uot;compute" to the same numerals in these models

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

- As comp doesn't compu= te the implementation of the type theory is much simpler and type checking = is very fast compared to regular cubicaltt

The only downside is that it doesn't have "strict"= ; canonicity (not 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 pract= ice as we can implement a closed term evaluator inspired by the cubical set= model for computing these numerals (much like how Coq has vm/native_comput= e for efficient computation of closed terms). Finally my little experiment = indicates that having a comp which doesn't compute doesn't affect t= he practical usability of this system too much either.

--
Anders

PS: Note that I = didn't remove 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 Grothendieck Fibratio= ns=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 A= ndrew=E2=80=99s message that indeed this technique=C2=A0
works as well (using classical logic) for simplicial sets. This can no= w be presented
as a combination of various published results. (The originality is onl= y in the presentation;
this essentially follows what is suggested in Andrew=E2=80=99s message= .)
=C2=A0This provides a semantics of e.g. suspension as an operation U -= > U, where U
is an univalent universe in the simplicial set model.=C2=A0

=C2=A0Thierry


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

So suspension (or more generally pushouts/coequalisers) is what would make = a really good test case for any proposed general approach =E2=80=94 it=E2= =80=99s the simplest HIT which as far as I know hasn=E2=80=99t been modelle= d without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT=E2=80=99= s proposed so far. =C2=A0(Am I right in remembering that this has been give= n for cubical sets?=C2=A0 I can=E2=80=99t find it in any of the writeups, b= ut I seem to recall hearing it presented at conferences.)

The technique used in cubical type theory seems fairly flexible. I'm no= t sure exactly how flexible, but I think I can get suspension to work in si= mplicial sets. In the below, throughout I use the characterisation of fibra= tions as maps with the rlp against the pushout product of each monomorphism with endpoint inclusion into the inte= rval. WLOG there is also a uniformity condition - we have a choice of lift = and "pulling back the monomorphism preserves the lift."

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

You then take the "weak fibrant replacement" of the pre susp= ension.=C2=A0 A 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=A0HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit=C2=A0https://groups.google.com/d/optout.

--
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 https://groups.google.com/d/optout.

--
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.
--000000000000183a27057a536899--