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
and which has been formalised in
and in the work
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.
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
<
Thierry...@cse.gu.se> 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
HomotopyTypeTheory+unsu...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.