From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.56.4 with SMTP id f4mr1507753pga.29.1494799542697; Sun, 14 May 2017 15:05:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.68.164 with SMTP id v36ls11917161ote.28.gmail; Sun, 14 May 2017 15:05:42 -0700 (PDT) X-Received: by 10.31.136.71 with SMTP id k68mr1197075vkd.8.1494799542155; Sun, 14 May 2017 15:05:42 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1494799542; cv=none; d=google.com; s=arc-20160816; b=s9H6HsxdlKgwkmTwTkPRRJnKwmxizB9LIRPktmhxWAb3qmoBcB7bGaWWt72j1Y/pmG 30YLScFriwG6LbIOqEjZy/PKujJE9wW0dJo8bfSiLOrOsvMT+jNECPZ9odXXahUGqAoH dRlCA5mCTupXVM++noQY1wgxzWfWSR2mpazdonwy6ANjf3hITTLWCNqULnA1xj7Y8Ezl bY9FFHFGMPq5m/nUlpyZY757MKKmx8jkAWlPBSWITIjbHHGXX6s4IoHQ2d7MmdEQ1Ai6 uBSCFb+2gEfPsg5ZdwiZl/KawuGHf5Ab5vzA0QlMm5k+xGi5Udzx1aU9Bkd+gomIUTI0 SbGA== 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=9XpPDGq7OGABMFfffRUecLmqEJ0tva6dQZNj9jPz6ag=; b=fjH5oGB5PoJAxxKXC8Qw8bGw6CnjMXP3Dvxb9cpTv8ZsEFfc4SfsQe63SJZKczt28m SYas+lVxxM1KwcuDc7ZEe0LchUTqMRAJ1U4DOnK/cNLkdaI+SGvmeehFxEc7J7+LdMff tmSHJ+Llxnx147Mf8hoDLHJ5OU3RAtBjCV7Sx3hCW/UjL6mIMconErPsqhXjtR7ws31m sOa1Norp/IvmlMeryzUcJLgMTqZaKHr8PfiC2eOxmVaEWjECRlMEGVtRDWxlTOoplstY jN14P0PFJoFL5tt20cjptOqAyDqBdkEg8FoWZdpKbrJOGzEgyGIXn04V9UcrMQ9zmUxI 5cfA== 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::231 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x231.google.com (mail-yb0-x231.google.com. [2607:f8b0:4002:c09::231]) by gmr-mx.google.com with ESMTPS id u18si768475ywc.3.2017.05.14.15.05.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 14 May 2017 15:05:42 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::231 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c09::231 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x231.google.com with SMTP id 132so5431623ybq.1 for ; Sun, 14 May 2017 15:05:42 -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=9XpPDGq7OGABMFfffRUecLmqEJ0tva6dQZNj9jPz6ag=; b=z8ONqQ+eVWq4qDABXx+/CwadnJb2HsvbDGjEKiIGG4+tx/GzTNYo4S+Bcifa/FbrxK PcK5eyjmKYrqVIAOmq/88Wtrb2UicdYflvVwRHax1ZUtfiGNbMieOPQ50R5vdrqyxy0I /xneDAvcv8nRgi3vymIgpqppkkAWYlIPziCpvsMkL2H+LW5IAt0XWs22Om1y+Rgmrbgw iX2j6VjkV958DrU1WiZxAfYvS8Dn9yB3TNMK0IQBKHK4yfvBu8NWFUbOB3cpqzbtZ+ed cBosnFv7h80AOYrzIJCrdF9+UNARkJ10MPBvt+zanYq/W569fRCf1mirArOHl+dcQMGU OEpw== X-Gm-Message-State: AODbwcDRcpPiYrjK859ZY8q4ndSnXPnWbtbaOX70jnsW4ZxMGrH9CPP6 pu8xX2gAsGkiFIuwuYE= X-Received: by 10.37.202.2 with SMTP id a2mr2573485ybg.129.1494799541655; Sun, 14 May 2017 15:05:41 -0700 (PDT) Return-Path: Received: from mail-yw0-f182.google.com (mail-yw0-f182.google.com. [209.85.161.182]) by smtp.gmail.com with ESMTPSA id l20sm507797ywa.38.2017.05.14.15.05.40 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 14 May 2017 15:05:41 -0700 (PDT) Received: by mail-yw0-f182.google.com with SMTP id b68so29941463ywe.3 for ; Sun, 14 May 2017 15:05:40 -0700 (PDT) X-Received: by 10.129.145.69 with SMTP id i66mr2455229ywg.229.1494799540644; Sun, 14 May 2017 15:05:40 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.207.1 with HTTP; Sun, 14 May 2017 15:05:20 -0700 (PDT) In-Reply-To: References: <6D5827E3-C1D9-4097-88B0-7EE210239602@chalmers.se> From: Michael Shulman Date: Sun, 14 May 2017 15:05:20 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] cubical stacks To: Bas Spitters Cc: Thierry Coquand , homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I think it is sort of the opposite. Here we are seeing the oo-exact completion of a 1-category, whereas they start with an (oo,1)-category and construct the 1-exact completion of its homotopy 1-category in a "homotopy" way. On Sun, May 14, 2017 at 12:44 PM, Bas Spitters wrote= : > Thanks Mike. This is very informative. > > Is your oo-exact completion related to the homotopy exact completion by > Benno and Ieke? > https://arxiv.org/abs/1603.02456 > > On Sun, May 14, 2017 at 11:53 AM, Michael Shulman > wrote: >> >> This is very nice. I have two questions/comments: >> >> 1. I would not expect the "stack" model to inherit inductive types >> like coproducts, natural numbers objects, W-types, and HITs with >> judgmental computation rules. In general I don't think these >> operations will preserve stacks, and you can apply the monad to >> stackify them but the result will only inherit a universal property up >> to equivalence within stacks. Is that right? >> >> 2. I agree that the word "stack" is appropriate for the internal >> construction, which is a categorification of Lawvere-Tierney sheaves, >> for which the word "sheaf" is often used. However, when performed >> inside the "cubical presheaves on a space" model, I don't believe it >> produces oo-stacks in the usual sense of the external set theory, >> because "cubical presheaves on a space" with this sort of "pointwise >> homotopy theory" don't present the homotopy theory of oo-presheaves on >> that space, at least not without some extra fibrancy condition. I >> think they are better regarded as a sort of "oo-exact completion" of >> the 1-category of presheaves. >> >> >> On Thu, May 4, 2017 at 10:31 AM, Thierry Coquand >> wrote: >> > In this message, I would like to present quickly a generalisation >> > the groupoid stack model of type theory to a oo-stack model of cubical >> > type >> > theory >> > (hence of type theory with a hierarchy of univalent universes), which >> > was >> > made possible by several discussions with Christian Sattler. >> > This might be interesting since, even classically, it was not known so >> > far >> > if >> > oo-stacks form a model of type theory with a hierarchy of univalent >> > universes. >> > >> > The model is best described as a general method for >> > building internal models of type theory >> > (in the style of this paper of Pierre-Marie P=C3=A9drot and Nicolas Ta= bareau, >> > but for cubical type theory). >> > >> > Given a family of types F(c), non necessarily fibrant, over a base ty= pe >> > Cov, >> > we associate the family of (definitional) monads D_c (X) =3D X^{F(c)} >> > with >> > unit maps m_c : X -> D_c(X). >> > We say that Cov,F is a -covering family- iff >> > each D_c is an idempotent monad, i.e. D_c(m) is path equal to m: D_c(X= ) >> > -> >> > D_c^2(X). >> > In this case, we can see Cov as a set of coverings and D_c(X) as the >> > type of >> > descent >> > data for X for the covering c. >> > We define X to be a -stack- iff each map >> > m_c is an equivalence. It is possible to show that being a stack is >> > preserved >> > by all operations of cubical type theory, and, using the fact that D_c >> > is >> > idempotent, >> > that the universe of stacks is itself a stack. >> > The following note contains a summary of these discussions, with an >> > example >> > of >> > a covering family Cov,F. >> > >> > Thierry >> > >> > -- >> > 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > >