From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.175.102 with SMTP id x38mr323224ywj.165.1494755659601; Sun, 14 May 2017 02:54:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.18.206 with SMTP id 75ls3277070ios.22.gmail; Sun, 14 May 2017 02:54:18 -0700 (PDT) X-Received: by 10.99.65.66 with SMTP id o63mr333525pga.146.1494755658748; Sun, 14 May 2017 02:54:18 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1494755658; cv=none; d=google.com; s=arc-20160816; b=GhefFfButtb5B6/ZN90c2tL9hPIpsq38lA7uERMAKdq3aXcS8k+kI9I6cfKMo8JAej NJmqFGS5kTSmVy/yVS0Ctytxu5vIW9VkZxR1XZErMPBKWeL3cIY6oqWHxvhqW9IzyeYE OUzq6X0cgkw2FMDqceoiBSpmfkQHFJiNMYZETZLrwmANZdeLoCWDG24dGWixBH+HWrV+ M6/korBrqsbQes5pyexA0WE2vzYhF5WW1+dtT3iKWz7nUZmHh5Jm0XT9vyKtyPF80R09 19XDPaxvhgBBnCXQqcwnfZdA6seR9Y5rYUQpIEbO/sdnQhdIXy/dbayU3Ag2hLpu5Ahd s4ZQ== 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=mLZJxyuUBtoZxX4CnBopwYzz2+di0BcA0vrUBCjx1Lg=; b=xcPwl0how8Gpm/1R+vvX73M78kXY6AbYSqyOainBPsiRIx1rgMcCMT6D+K5uyLM30L 1BPzelYVUVueofc7+ANZu2EEW+NB+GW/PWr5j5ptj6OMoFMXSn+ZHe+HiM563Jh03b4y 33qaZSKGiIIATwwrxEf/39IyA8BoI1wxx+l0CzVnvtAPApj9kLG6/G7FTrIoCj2iAYxj KBATn0lJ5h673oudbQWyBC9SyzbrrrxHVCJFaRTKug0G5T/Abs4h11Ec8Prk50fILqYG pJqmL7HvHBS9WNyECn3bqswDoi3LheQuNuKinNTvIfElXREw+QpPMjd2MRCuptdN6TI9 f/BQ== 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::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x22e.google.com (mail-yw0-x22e.google.com. [2607:f8b0:4002:c05::22e]) by gmr-mx.google.com with ESMTPS id u18si662847ywc.3.2017.05.14.02.54.18 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 14 May 2017 02:54:18 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22e is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c05::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x22e.google.com with SMTP id l14so26638647ywk.1 for ; Sun, 14 May 2017 02:54:18 -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=mLZJxyuUBtoZxX4CnBopwYzz2+di0BcA0vrUBCjx1Lg=; b=jISbC7IMOY0Z4tG15kQhggPZSKzxf2u1bK8LheA3gn2r3WVQdoucl++JsC3YCxFUCs 13IDF4chxtmI5LTP3EkZK9Arh+LoYXSb9JeTED601yJH2/8wQeVli1vCLUTzZRTEl0Lp 13ch2wzwlcDVwo+dMbGnGReVlq5/p3wvzQq3vsb4yhnYTYcFt4doebfkyplmtHPkz3hu D7I68eI9VXS3KYs1zA/4c9hiHaAHGGd85Y5gGKrouULaaV27O/skh+n59UbfcaU+jkYK heztm2XNfa4RT+inMTjlBYQvi1KM99TAv1EI4uC2O63aTAPvc4w/TRas1uVqdZnkpuvM E81Q== X-Gm-Message-State: AODbwcAYwyajpoYSqVg7dLfKQtunxSB3wU1aKVBCLiOirG2VQhhUQejl 4pprzC1o26GdXloNlPU= X-Received: by 10.129.153.8 with SMTP id q8mr486962ywg.134.1494755658138; Sun, 14 May 2017 02:54:18 -0700 (PDT) Return-Path: Received: from mail-yw0-f173.google.com (mail-yw0-f173.google.com. [209.85.161.173]) by smtp.gmail.com with ESMTPSA id b78sm880685ywh.73.2017.05.14.02.54.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 14 May 2017 02:54:17 -0700 (PDT) Received: by mail-yw0-f173.google.com with SMTP id 203so26562456ywe.0 for ; Sun, 14 May 2017 02:54:17 -0700 (PDT) X-Received: by 10.13.207.3 with SMTP id r3mr527382ywd.63.1494755657499; Sun, 14 May 2017 02:54:17 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.207.1 with HTTP; Sun, 14 May 2017 02:53:57 -0700 (PDT) In-Reply-To: <6D5827E3-C1D9-4097-88B0-7EE210239602@chalmers.se> References: <6D5827E3-C1D9-4097-88B0-7EE210239602@chalmers.se> From: Michael Shulman Date: Sun, 14 May 2017 02:53:57 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] cubical stacks To: Thierry Coquand Cc: homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 ty= pe > 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 fa= r > 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 Tabar= eau, > but for cubical type theory). > > Given a family of types F(c), non necessarily fibrant, over a base type > Cov, > we associate the family of (definitional) monads D_c (X) =3D X^{F(c)} wi= th > 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 exam= ple > 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.