Many thanks for the question and the comment. After I sent my message, I realised that the note can be seen as a (new) example of the situation you described in http://uf-ias-2012.wikispaces.com/file/view/modalitt.pdf and which has been formalised in https://hott.github.io/HoTT/coqdoc-html/HoTT.Modalities.Lex.html and in the work https://jfr.unibo.it/article/view/6232 The point is that one can apply this technique to presheaf models of cubical type theory. (Note that they are not examples of “open” modality in general since one does exponentiation w.r.t. a cubical presheaf which may not be fibrant.) And this is possible since the cubical set model generalise directly to the general presheaf case (contrary to the simplicial set model). For question 1, indeed, we have looked only at special “extreme” cases precisely in order to address the issue you mention: -when the space is “connected” (e.g. unit interval) where the constant presheaf N already satisfies the stack condition, and -when the space is totally disconnected (e.g. Cantor space) where we need to impose an extra condition (to have an inverse of the m map for this kind of covering which is strictly right inverse) in order to interpret the elimination rule in a strict way. Note that one can combine the two conditions: for instance, the case the space which is the product of the unit interval and Cantor space or the case of a site used to interpret constructively the algebraic closure of a field (which is the site of etale algebra over the field where a cover is either disconnected given by an idempotent element of the algebra, or connected given by a separable algebraic extension). For comment 2, this is related to the remark you made ~ 1 year ago that the type of h-propositions in the presheaf model is not equivalent to the to the presheaf of truth-values \Omega. It is indeed possible to prove this with the following example. If one considers the poset w / \ w0 w1 \ / w01 the presheaf model over this poset has classically the following 6 truth-values (classically there are only 2 truth values 0 and 1), which describe \Omega w: 0 w0 : 0 w1 :0 w01 : 0 w: 0 w0 : 0 w1 :0 w01 : 1 w: 0 w0 : 1 w1 :0 w01 : 1 w: 0 w0 : 0 w1 :1 w01 : 1 w: 0 w0 : 1 w1 :1 w01 : 1 w: 1 w0 : 1 w1 :1 w01 : 1 If we consider in this model the groupoid G which is empty at level w, has a point a0 at level w0, a point a1 at level w1 and a path a0 -> a1 at level w01, this groupoid G is a proposition which is not equivalent to any of these propositions in \Omega, and so (since the cubical nerve of this groupoid is fibrant in the model) this shows that the canonical map \Omega -------> hProp(U) = Sigma (X:U) isProp X is not an equivalence. (This is to be compared with the situation for the corresponding injective simplicial model structure where, surprisingly, the nerve of G is not fibrant.) I was thinking of fibrant cubical pre sheaves as pre sheaves of oo-groupoids (since one can think of a fibrant cubical set as an oo-groupoid), hence I mentioned "oo-stacks” but this should be avoided if, as you write, what is described is too far from the standard notion oo-stacks. I only hope that the note gives some examples of “sheaf" models of type theory with the axiom of univalence, which can be used in the same way sheaf models are used for higher order logic. On 14 May 2017, at 11:53, 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édrot and Nicolas Tabareau, 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) = 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.