From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.50.163 with SMTP id u32mr1155066otb.28.1496756136585; Tue, 06 Jun 2017 06:35:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.211.197 with SMTP id n188ls3036807itg.22.canary-gmail; Tue, 06 Jun 2017 06:35:35 -0700 (PDT) X-Received: by 10.99.127.14 with SMTP id a14mr13656361pgd.162.1496756135330; Tue, 06 Jun 2017 06:35:35 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1496756135; cv=none; d=google.com; s=arc-20160816; b=deWuxZViw0tsizWoEtlX0HRq0gYRUH2+zMHWXhEbqSwkxrA1FOXIuK73ldd7moF+w1 Ru0PwEu0gTeXMzOOQ2OExjWz1sZ4J7InbqcqpSPyW8pkHO4jbSpUFE91ZtuVK+IhU0s8 bGB4v7TK79kwYf4O6YJVTVtfDTqXaLFpy24WqbihXUIME3pkFGmYn7SKZqkkz+9OfWit +NYEtDRkiEXd0ZlX134jXYQ3iI6bep3jgaVSEFX6hDdWUH0RNon8nMsvRe+39k5TILjy 0ieS2I4dWz6w1QaQBiBN9XUoRJBlKaqI/BN+tAQVRlUjtn3AgEb7CKaMgAWljXu0/Pl3 90LA== 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=QMMyLTZXGSX29M1fbw2OBFx2WzfuS288PUplKW+q/Wk=; b=LEj+p8Bcn5C5qULzCaAefrabUzh+AKb4puVMjoAeD2QVhWPGJMWQI7yf/UcWSqZ4Af mRRor5BvuvhcIRSv8GNU+rzWv72JVFq36QU0YD1XiXjezkoIvdZR+Fx81B4Ab+CNV3Rf YbL7UMioBUNMw0MT4FaCwSyk1V7Dc8TEV0D7y+M3+pHTxIyiqGWexhaymn6IztEDWESy eesO/cLraRaI/1Y+ljc79MAl23Qerk+QAtiCNUYOVK3iyeld3SfFJYq489cnJly03fLd nBAWiaGxqCUsv+bTFQTUCTNd0tsxeqFx1NzOaxQBE+tuVD77g58X/sTUdR9mfNfDFCn1 k5dA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c09::229 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x229.google.com (mail-yb0-x229.google.com. [2607:f8b0:4002:c09::229]) by gmr-mx.google.com with ESMTPS id t127si932329ywa.0.2017.06.06.06.35.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 06 Jun 2017 06:35:35 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::229 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c09::229 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x229.google.com with SMTP id 4so15279758ybl.1 for ; Tue, 06 Jun 2017 06:35:35 -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=QMMyLTZXGSX29M1fbw2OBFx2WzfuS288PUplKW+q/Wk=; b=RqjCFNo2HsPB8sr6KDfOR2NTDKgHKqlfS3lTdGgrkyT3GMccthqgO5tm04DoL1/IyV YKAmqK/nYXp3KrKNDTNpbPKZoA8h+jw3D5bnMJTuaPFJ74hP82SYjmH7bGXI1Cw5oU5c PgBnTNX4CPSpzumhIhbcBVGJ6+VYzdfVkfx58xayOvAKVdsF+XgJyVR8kkxBUJdPDBMo 1vsJpwdQaLbxCP4jL07hQJMmxVbDfW8xdiM4Bzh5g40/KpTHaa6xtTt2tc3hXhO0UtTX 4lsPpVsq7+xosEGNvwxV++obkGrTmXjgl2QEd/KS6T2s7csVbkoq/NwqWqJmfOIRb3NH kIdQ== X-Gm-Message-State: AODbwcDaphO1S2xCa5xYFFsWIMwdP0MXMz516MijE9/0TytoJ0jJCO7g 2CV48RSTTcngG2e5Pck= X-Received: by 10.37.81.67 with SMTP id f64mr2867564ybb.22.1496756134462; Tue, 06 Jun 2017 06:35:34 -0700 (PDT) Return-Path: Received: from mail-yw0-f171.google.com (mail-yw0-f171.google.com. [209.85.161.171]) by smtp.gmail.com with ESMTPSA id 203sm16040235ywp.0.2017.06.06.06.35.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 06 Jun 2017 06:35:34 -0700 (PDT) Received: by mail-yw0-f171.google.com with SMTP id l14so67097062ywk.1 for ; Tue, 06 Jun 2017 06:35:34 -0700 (PDT) X-Received: by 10.13.231.70 with SMTP id q67mr3067790ywe.58.1496756133579; Tue, 06 Jun 2017 06:35:33 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.18.215 with HTTP; Tue, 6 Jun 2017 06:35:13 -0700 (PDT) In-Reply-To: <1c2cb641-89e3-444d-aa0c-cb8ccb79cf3c@googlegroups.com> References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> <9F58F820-A54A-46E7-93DC-F814D4BEE0C6@cmu.edu> <2efaa818-9ed1-459f-a3a5-a274d19e6a96@googlegroups.com> <1c2cb641-89e3-444d-aa0c-cb8ccb79cf3c@googlegroups.com> From: Michael Shulman Date: Tue, 6 Jun 2017 07:35:13 -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 I'll be interested to see if you can make it work! But I'd be much more interested if there is something that can be done in a general class of models, rather than a particular one like cubical or simplicial sets. On Tue, Jun 6, 2017 at 4:03 AM, Andrew Swan wrote: > Actually, I've just noticed that doesn't quite work - I want to say that = a > map is a weak fibration if it has a (uniform choice of) diagonal fillers = for > lifting problems against generating cofibrations where the bottom map > factors through the projection I x V -> V, but that doesn't seem to be > cofibrantly generated. Maybe it's still possible to do something like > fibrant replacement anyway. > > Andrew > > > On Tuesday, 6 June 2017 11:19:37 UTC+2, Andrew Swan wrote: >> >> I've been thinking a bit about abstract ways of looking at the HITs in >> cubical type theory, and I don't have a complete proof, but I think actu= ally >> the same sort of thing should work for simplicial sets. >> >> We already know that the fibrations in the usual model structure on >> simplicial sets can be defined as maps with the rlp against the pushout >> product of generating cofibrations with interval endpoint inclusions (in >> Christian's new paper on model structures he cites for this result Chapt= er >> IV, section 2 of P. Gabriel and M. Zisman. Calculus of fractions and >> homotopy theory, but I'm not familiar with the proof myself). >> >> Now a generating trivial cofibration is the pushout product of a >> generating cofibration with endpoint inclusion, so its codomain is of th= e >> form I x V, where V is the codomain of the generating cofibration (which= for >> cubical sets and simplicial sets is representable). Then we get another = map >> by composing with projection I x V -> V, which is a retract of the >> generating trivial cofibration and so also a trivial cofibration. If a m= ap >> has the rlp against all such maps, then call it a weak fibration. Then I >> think the resulting awfs of "weak fibrant replacement" should be stable >> under pullback (although of course, the right maps in the factorisation = are >> only weak fibrations, not fibrations in general). >> >> Then eg for propositional truncation, construct the "fibrant truncation" >> monad by the coproduct of truncation monad with weak fibrant replacement= . In >> general, given a map X -> Y, the map ||X|| -> Y will only be a weak >> fibration, but if X -> Y is fibration then I think the map ||X|| -> Y sh= ould >> be also. I think the way to formulate this would be as a distributive la= w - >> the fibrant replacement monad distributes over the (truncation + weak >> fibrant replacement) monad. It looks to me like the same thing that work= s in >> cubical sets should also work here - first define a "box flattening" >> operation for any fibration (i.e. the operation labelled as "forward" in >> Thierry's note), then show that this operation lifts through the HIT >> constructors to give a box flattening operation on the HIT, then show th= at >> in general weak fibration plus box flattening implies fibration, (Maybe = one >> way to do this would be to note that the cubical set argument is mostly = done >> internally in cubical type theory, and simplicial sets model cubical typ= e >> theory by Orton & Pitts, Axioms for Modelling Cubical Type Theory in a >> Topos) >> >> Best, >> Andrew >> >> >> >> On Thursday, 1 June 2017 18:08:58 UTC+2, 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. >>> >>> So here=E2=80=99s a very precise problem which is as far as I know open= : >>> >>> (*) Construct an operation =CE=A3 : U =E2=80=93> U, where U is Voevodsk= y=E2=80=99s universe, >>> together with appropriate maps N, S : =C3=9B =E2=80=93> =C3=9B over =CE= =A3, and a homotopy m from N >>> to S over =CE=A3, which together exhibit U as =E2=80=9Cclosed under sus= pension=E2=80=9D. >>> >>> I asked a related question on mathoverflow a couple of years ago: >>> https://mathoverflow.net/questions/219588/pullback-stable-model-of-fibr= ewise-suspension-of-fibrations-in-simplicial-sets >>> David White suggested he could see an answer to that question (which wo= uld >>> probably also answer (*) here) based on the comments by Karol Szumi=C5= =82o and >>> Tyler Lawson, using the adjunction with Top, but I wasn=E2=80=99t quite= able to >>> piece it together. >>> >>> =E2=80=93p. >>> >>> > >>> > > On Jun 1, 2017, at 11:38 AM, Michael Shulman >>> > > wrote: >>> > > >>> > > Do we actually know that the Kan simplicial set model has a *univer= se >>> > > closed under* even simple HITs? It's not trivial because this woul= d >>> > > mean we could (say) propositionally truncate or suspend the generic >>> > > small Kan fibration and get another *small* Kan fibration, whereas >>> > > the >>> > > base of these fibrations is not small, and fibrant replacement >>> > > doesn't >>> > > in general preserve smallness of fibrations with large base spaces. >>> > > >>> > > (Also, the current L-S paper doesn't quite give a general syntactic >>> > > scheme, only a general semantic framework with suggestive >>> > > implications >>> > > for the corresponding syntax.) >>> > > >>> > > >>> > > >>> > > On Thu, Jun 1, 2017 at 8:30 AM, Steve Awodey wrote= : >>> > >> >>> > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand >>> > >> wrote: >>> > >> >>> > >> If we are only interested in providing one -particular- model of >>> > >> HITs, >>> > >> the paper >>> > >> on cubical type theory describes a way to interpret HIT togethe= r >>> > >> with a >>> > >> univalent >>> > >> universe which is stable by HIT operations. This gives in particul= ar >>> > >> the >>> > >> consistency >>> > >> and the proof theoretic power of this extension of type theory. >>> > >> >>> > >> >>> > >> but the Kan simplicial set model already does this =E2=80=94 right= ? >>> > >> don=E2=80=99t get me wrong =E2=80=94 I love the cubes, and they ha= ve lots of nice >>> > >> properties >>> > >> for models of HoTT >>> > >> =E2=80=94 but there was never really a question of the consistency= or >>> > >> coherence of >>> > >> simple HITs like propositional truncation or suspension. >>> > >> >>> > >> the advance in the L-S paper is to give a general scheme for >>> > >> defining HITs >>> > >> syntactically >>> > >> (a definition, if you like, of what a HIT is, rather than a family >>> > >> of >>> > >> examples), >>> > >> and then a general description of the semantics of these, >>> > >> in a range of models of the basic theory. >>> > >> >>> > >> Steve >>> > >> >>> > >> >>> > >> The approach uses an operation of =E2=80=9Cflattening an open bo= x=E2=80=9D, which >>> > >> solves >>> > >> in >>> > >> this case the issue of interpreting HIT with parameters (such as >>> > >> propositional >>> > >> truncation or suspension) without any coherence issue. >>> > >> Since the syntax used in this paper is so close to the semantics, >>> > >> we >>> > >> limited >>> > >> ourselves to a syntactical presentation of this interpretation. B= ut >>> > >> it can >>> > >> directly >>> > >> be transformed to a semantical interpretation, as explained in the >>> > >> following >>> > >> note >>> > >> (which also incorporates a nice simplification of the operation of >>> > >> flattering >>> > >> an open box noticed by my coauthors). I also try to make more >>> > >> explicit in >>> > >> the note >>> > >> what is the problem solved by the =E2=80=9Cflattening boxes=E2=80= =9D method. >>> > >> >>> > >> Only the cases of the spheres and propositional truncation are >>> > >> described, >>> > >> but one >>> > >> would expect the method to generalise to other HITs covered e.g. i= n >>> > >> the HoTT >>> > >> book. >>> > >> >>> > >> On 25 May 2017, at 20:25, Michael Shulman >>> > >> wrote: >>> > >> >>> > >> The following long-awaited paper is now available: >>> > >> >>> > >> Semantics of higher inductive types >>> > >> Peter LeFanu Lumsdaine, Mike Shulman >>> > >> https://arxiv.org/abs/1705.07088 >>> > >> >>> > >> From the abstract: >>> > >> >>> > >> We introduce the notion of *cell monad with parameters*: a >>> > >> semantically-defined scheme for specifying homotopically >>> > >> well-behaved >>> > >> notions of structure. We then show that any suitable model categor= y >>> > >> has *weakly stable typal initial algebras* for any cell monad with >>> > >> parameters. When combined with the local universes construction to >>> > >> obtain strict stability, this specializes to give models of specif= ic >>> > >> higher inductive types, including spheres, the torus, pushout type= s, >>> > >> truncations, the James construction, and general localisations. >>> > >> >>> > >> Our results apply in any sufficiently nice Quillen model category, >>> > >> including any right proper simplicial Cisinski model category (suc= h >>> > >> as >>> > >> simplicial sets) and any locally presentable locally cartesian >>> > >> closed >>> > >> category (such as sets) with its trivial model structure. In >>> > >> particular, any locally presentable locally cartesian closed >>> > >> (=E2=88=9E,1)-category is presented by some model category to whic= h our >>> > >> results apply. >>> > >> >>> > >> -- >>> > >> 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. >>> > >> >>> > >> >>> > >> >>> > >> -- >>> > >> 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. >>> > >> >>> > >> >>> > >> -- >>> > >> 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. >>> > > >>> > > -- >>> > > 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. >>> > >>> > -- >>> > 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, sen= d >>> > an email to HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.