From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.4.77 with SMTP id 74mr16322881ioe.54.1496876822524; Wed, 07 Jun 2017 16:07:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.11.227 with SMTP id 90ls4461812oth.3.gmail; Wed, 07 Jun 2017 16:07:02 -0700 (PDT) X-Received: by 10.129.70.131 with SMTP id t125mr6238532ywa.94.1496876822022; Wed, 07 Jun 2017 16:07:02 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1496876821; cv=none; d=google.com; s=arc-20160816; b=0cYpuX/UXT2UEgJNZsefuDa9pOFl7GWy/80oZd53YBVGp/cfNA3MhhdN/47vZf7sRX 2WiSx1ZRa7Sv5jsc1xvidk1vYEHKcemZX0sICO4c/+8jlhDWr+VA8AadCEwVWazu81eQ k5BpmEo1YwTP24kV6La0Kc2N2TqHP5Sx7GgaQ0IngqXYf5/qT1bJZNeFA5S0az15fBXZ lvBjsmMvl8AIRf15h8jPr08Xk3xDF6GDLWy6IaM5mKkvDWcUJOTzysjTSpzPNb1R/6Dh MW1TCHNBsa2KoiYpm1VEDrZIcSPDbC96uLWOvHoPxEqnZgvWltbtgv1nTrTjOKyv7OOe 2Udg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=+fKWA4YFXI+9w3aXVt3zvThusiYkxoPoi0UnI1k/nkg=; b=sG8Wpw66JdIEtD6SEmsb9SpSvD2yxEbN3jltAdcVif9L/waasvQcdQIjLiV2DJQZqs 5W9omeLvKyaPq1hSfKg7eL+Tllk543Yx/aMH3zBKTHC9kRWih7Z+QKRiVsttB4YGcNLI QEiodlBGGUE/5GPCYqsRkYylVQbra1Ai5L1C4GasloCXkMU11T61/QcrvtDmw+H7Y5PT 5IcxLEzNFxGBevfomkn73Ulk4Ho3CIZO4w9c1XphBCehoSqVblp4nKNZLncNbAXcu5bh quljZDzGqjKbsz4xLHxJE+IVccruzUBeILkp1kcnDfhYc5wkU06kGR9LGhIdJHa9lHIf FtYA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x234.google.com (mail-yw0-x234.google.com. [2607:f8b0:4002:c05::234]) by gmr-mx.google.com with ESMTPS id l135si178663ywb.10.2017.06.07.16.07.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Jun 2017 16:07:01 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::234 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x234.google.com with SMTP id 141so8185350ywe.2 for ; Wed, 07 Jun 2017 16:07:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=+fKWA4YFXI+9w3aXVt3zvThusiYkxoPoi0UnI1k/nkg=; b=yYv9Yeumn7+WUvOZt7qW8XT9NL4o7BLsseznqTNxasMKKsiLyDis/OsiAs1GV9UMHn Ky/MOH1jiqktVVmqSljYJpquQDM5Ob7PB9aWmVQd5C3GR6zWB2hlYii6qvDemZwRjHjM YZiegdF4KOZ0K2ap/laMCs17Qb/PwBypz87v1dWrBM2xNf5/9dXUPuPgAVQ+668XYE1o rEKI+LUIKWFFeWhlv1cygpCSxUgEcYqYzMcjDWs/+F0/yA/YO77r1B50VlyyNzmrQoxz Md4kOMLYRj7aWc4zFqFJteTtJ9Q5psNjgy6d/tK13r1ZxICvP8r08oyu/N+/UvMjwpz3 yZIw== X-Gm-Message-State: AODbwcBToRodQQurjihng4yVLuUu3nECNUnX+fl4rIEbzwAwkgXpwkKG L0rGeVBreBbSfNei218= X-Received: by 10.13.230.3 with SMTP id p3mr8916831ywe.177.1496876821410; Wed, 07 Jun 2017 16:07:01 -0700 (PDT) Return-Path: Received: from mail-yb0-f177.google.com (mail-yb0-f177.google.com. [209.85.213.177]) by smtp.gmail.com with ESMTPSA id q206sm1203695ywc.35.2017.06.07.16.07.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Jun 2017 16:07:00 -0700 (PDT) Received: by mail-yb0-f177.google.com with SMTP id o9so6108872yba.3 for ; Wed, 07 Jun 2017 16:07:00 -0700 (PDT) X-Received: by 10.37.170.229 with SMTP id t92mr9050102ybi.5.1496876819887; Wed, 07 Jun 2017 16:06:59 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.18.215 with HTTP; Wed, 7 Jun 2017 16:06:39 -0700 (PDT) In-Reply-To: References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> <9F58F820-A54A-46E7-93DC-F814D4BEE0C6@cmu.edu> From: Michael Shulman Date: Wed, 7 Jun 2017 17:06:39 -0600 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Semantics of higher inductive types To: Andrew Swan Cc: Homotopy Type Theory , Steve Awodey , Thierry Coquand Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Wed, Jun 7, 2017 at 12:34 PM, Andrew Swan wrote: > The technique used in cubical type theory seems fairly flexible. I'm not > 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 als= o a > uniformity condition - we have a choice of lift and "pulling back the > monomorphism preserves the lift." Why is there no LOG in this? > 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 this is the same a= s > what you called pre suspension). Although the pre suspension is not a > fibration in general, it does have some of the properties you might expec= t > 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 should also be a "flattening" operation that ta= kes > 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 of p(1). > > You then take the "weak fibrant replacement" of the pre suspension. A ma= p > in simplicial sets is a fibration if and only if it has the rlp against e= ach > 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 f= or > some of these lifting problems. The pushout product of a monomorphism A -= > B > with endpoint inclusion always has codomain B x I - then only consider th= ose > 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 > fibrant replacement is stable under pullback - one way is carry out the > operation "internally" in simplicial sets (viewed as a topos), and the ot= her > to use the algebraic small object argument, ensuring that uniformity > condition above is in the definition. The intuitive reason why this shoul= d > be stable is that the problem that stops the usual fibrant replacement fr= om > being stable is that e.g. when we freely add the transport of a point alo= ng > 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 on= ly > add a filler to an open box to a certain fibre if the original open box l= ies > 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) 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 sh= ow > composition and then derive filling. So to define the composition of an o= pen > 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 gener= al > result along the lines of "if the monad of transport and flattening > distributes over a monad, then the fibrant replacement monad distributes > 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 >> 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 add= ing stronger >>> conditions on the cardinal used won=E2=80=99t help. The problem is tha= t one takes a >>> fibrant replacement to go from the =E2=80=9Cpre-suspension=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 size of the *base* of the fam= ily. >>> So the pre-suspension is small, but the suspension =E2=80=94 although e= ssentially >>> 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 seems = a >> bit easier to do by ad hoc constructions; e.g. the construction below do= es >> it in simplicial sets, and I think a similar thing may work also in cubi= cal >> sets. (I don=E2=80=99t claim originality for this construction; I don= =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 multiple people may have >> noticed it independently.) >> >> So suspension (or more generally pushouts/coequalisers) is what would ma= ke >> 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 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 simplici= al >> sets: >> >> (1) Given a fibration Y =E2=80=94> X, define |Y| =E2=80=94> X as follow= s: >> >> an element of |Y|_n consists of an n-simplex x : =CE=94[n] =E2=80=94> X,= together with >> 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 evident square commutes; >> >> reindexing acts by taking pullbacks/inverse images of the domain of the >> partial lift (i.e. the usual composition of a partial map with a total m= ap). >> >> (2) There=E2=80=99s an evident map Y =E2=80=94> |Y| over X; and the oper= ation sending Y to >> Y =E2=80=94> |Y| =E2=80=94> X is (coherently) stable up to isomorphism u= nder 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. (Straig= htforward, >> given (3), by concretely constructing the required liftings.) >> >> (5) The evident map Y =E2=80=94> |Y| over X is a cell complex constructe= d 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 simplic= es 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 fibratio= ns, stably >> in X. (Orthogonality is immediate from (3) and (5); stability is then b= y >> (2).) >> >> (7) Let V be either the universe of =E2=80=9Cwell-ordered =CE=B1-small f= ibrations=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 Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.