Types as spaces

[Martin Escardo]

Before my involvement with HoTT, much of my research was about
understanding types as spaces, in the vein of Brouwer, Kleene, Scott,
and many others, and the relationship of this undertanding with
constructive mathematics and (the related, but different, field of)
computability theory. And I am still very much interested in that.

The understanding of types as spaces in HoTT is very different from
the above.

There seems to be very little interest, at present, to understand how
these two views of types as spaces relate to each other.

For example, we have two circles after one reads the HoTT book: The
official one, written S^1, and the the obvious subset "Circle" of R^2
where R is the set of real numbers as defined in the HoTT book.

There are no non-constant maps S^1 -> Circle (because Circle is a set,
and any map of S^1 into a set is constant) or Circle -> S^1 (that I
can see).

In any case, Circle is a set in HoTT. But it should be a space: for
example, it should be the case that all definable functions Circle ->
R^2 are continuous (in the usual sense of real analysis). I don't have
a (meta-)proof of this, but there are reasons to strongly conjecture
it (and I do).

In a similar vein, in Hott, (N->2) is a set, but I imagine it as the
Cantor space 2^N, so that e.g. potentially all functions 2^N -> N are
uniformly continuous. As an internal statement in MLTT, this statement
is undecided (and it should be in HoTT too, but I can't offer a
meta-proof at present). But it is a meta-theorem about MLTT that all
definable functions 2^N->N are uniformly continuous.

It is important to understand how the Old and New views of types as
spaces relate to each other, not only "intrinsically" (when reasoning
in type theory), but also "extrinsically" (when reasoning about type
theory). In particular, there is no known (natural or artificial)
model of MLTT simultaneously compatible with the Old and New views of
types. I know of no model that simultaneously validates univalence
and, say, the uniform continuity of all functions 2^N->N.

Now that we know that univalence is compatible with computation, via
the cubical model, it looks plausible that the Old and New views of
types can be reconciled.

But how?

Martin

[Michael Shulman]

This is exactly what cohesive HoTT is about. Cohesive oo-groupoids are oo-groupoids with 'extra topological structure', so that they have both the structure of a 'space' in the sense of topology and a 'space' in the sense of homotopy theory, but the two structures are 'orthogonal'. I haven't checked, but it seems likely to me that the cohesive models validate continuity principles. The nlab has stuff about some cohesive models like stacks on the site of euclidean spaces; I think at IAS I suggested we could also consider stacks on the site for the topological topos.

--
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+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Matt Oliveri]

I have some thoughts. I don't know if they're very good though; I don't know much about the topological viewpoint of computation.

On Tuesday, October 21, 2014 8:10:33 PM UTC-4, Martín Escardó wrote:

For example, we have two circles after one reads the HoTT book: The
official one, written S^1, and the the obvious subset "Circle" of R^2
where R is the set of real numbers as defined in the HoTT book.

There are no non-constant maps S^1 -> Circle (because Circle is a set,
and any map of S^1 into a set is constant) or Circle -> S^1 (that I
can see).

What if you defined (internal) paths and homotopies in terms of the interval of real numbers? Could you then define the fundamental groupoid of Circle as a HIT (whose points are the elements of the set Circle)? If so, then I figure at least S^1 -> Π(Circle) would work.

It is important to understand how the Old and New views of types as
spaces relate to each other, not only "intrinsically" (when reasoning
in type theory), but also "extrinsically" (when reasoning about type
theory). In particular, there is no known (natural or artificial)
model of MLTT simultaneously compatible with the Old and New views of
types. I know of no model that simultaneously validates univalence
and, say, the uniform continuity of all functions 2^N->N.

Now that we know that univalence is compatible with computation, via
the cubical model, it looks plausible that the Old and New views of
types can be reconciled.

But how?

Whatever form of continuity you're asking for, wouldn't it obtain a notion of homotopy in the usual way? And then hopefully you could use that homotopy theory as a model of HoTT. Something like (wild guess): Scott topology + constructive Cauchy real interval + topological space interpretation of HoTT. Maybe you'd need to use a subcategory of Top to ensure that we're only talking about Scott continuous functions?

So yeah, maybe this helps, maybe it makes no sense. I have no idea if/how it relates to Mike's suggestion.

[Urs Schreiber]

On 10/22/14, Michael Shulman <shu...@sandiego.edu> wrote:

> This is exactly what cohesive HoTT is about. Cohesive oo-groupoids are

Just to amplify: in the standard models [1,2] of cohesive HoTT [3] it
the shape modality takes it to the homotopy theoretic circle:

shape( R^2-{0} ) = S^1

Generally, the shape modality takes a topological manifold to its
fundamental infinity-groupoid, i.e. to its underlying bare homotopy
type.

[1] http://ncatlab.org/nlab/show/Euclidean-topological+infinity-groupoid
[2 http://ncatlab.org/nlab/show/smooth+infinity-groupoid]
[3] http://ncatlab.org/nlab/show/cohesive+homotopy+type+theory

>> 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.

[Andrej Bauer]

On Wed, Oct 22, 2014 at 5:54 AM, Urs Schreiber <urs.sc...@googlemail.com> wrote:

Just to amplify: in the standard models [1,2] of cohesive HoTT [3]  it
the shape modality takes it to the homotopy theoretic circle:

   shape( R^2-{0} ) = S^1

Generally, the shape modality takes a topological manifold to its
fundamental infinity-groupoid, i.e. to its underlying bare homotopy
type.

This is good progress towards Martin's goal (which I very much share), but we're not there yet.

Does univalence hold in the cohesive model?

I suppose the cohesive HoTT should be able to "see" internally that there are no discontinuous maps R -> R. By the way, is R really what we think it is? Does it magically obtain the Euclidean topology when constructed internally?

Also, what happens with the Cantor space? Are all maps (2 -> N) -> N continuous, either internally or externally? It should be easy to compute what the Cantor space looks like.

With kind regards,

Andrej

[Michael Shulman]

On Tue, Oct 21, 2014 at 11:16 PM, Andrej Bauer <andrej...@andrej.com> wrote:
> Does univalence hold in the cohesive model?

Univalence holds in all (oo,1)-topos models. However, we don't yet
have models of the cohesive toposes that have strict universes, only
weakly-a-la-Tarski ones.

> I suppose the cohesive HoTT should be able to "see" internally that there
> are no discontinuous maps R -> R. By the way, is R really what we think it
> is? Does it magically obtain the Euclidean topology when constructed
> internally?
>
> Also, what happens with the Cantor space? Are all maps (2 -> N) -> N
> continuous, either internally or externally?

After a little more thought, I realized that these questions pertain
only to hsets, so their answers should be the same as for the
corresponding ordinary 1-toposes. In other words, take any
Grothendieck 1-topos satisfying your favorite continuity principles
that pertain only to hsets (such as R and N); then the (oo,1)-topos of
oo-sheaves on the same site will be (weakly Tarski) univalent and also
satisfy the same continuity principles.

Mike

[David Roberts]

Regarding the relation between the spatial 1-type given by Circle and
S^1, we have a map in one direction, as long as we are careful what we
mean by map. I will work in the context of stacks over the site of
Euclidean spaces, and I will only need stacks associated to groupoids
internal to topological manifolds. S^1 "is" a topologically discrete
groupoid equivalent to the one-object groupoid with morphisms Z. Call
this * // Z. There is a groupoid |R // Z that is the integers acting
freely on the reals by addition in the usual way, and the space of
orbits is Circle. There is a span of internal functors (regarded as a
map of stacks from Circle to * // Z)

Circle <--- |R // Z --> * // Z

and the left one is an equivalence in the category of stacks. The
right one is not, but it is an equivalence after applying the shape
modality. Thus this span becomes an equivalence after applying the
shape modality, but not before. This reflects, as was pointed out, the
fact spaces and types qua homotopy types are in a sense orthogonal.
The type captures the homotopy type of the space, but loses the
geometry. If we considered the punctured plane or punctured closed
disc on the left, there are corresponding spans with right-most object
* // Z, and they all become equivalences after applying shape, but the
circle, the punctured plane and the punctured disc are not isomorphic
as spaces.

David

[Michael Shulman]

But is your "R" the same as the one defined *internally* in the model
by writing out the definition of real numbers as Dedekind cuts? I
think Andrej is right that that's not obvious. That's one reason I
suggested to use oo-stacks on the site of the topological topos, since
we know that in the topological topos the internal real numbers end up
actually having the correct topology.

[David Roberts]

Ah, I see the problem now. One needs to be able to say that |R is
contractible for what I wrote to make sense, presumably with respect
to some interval object, and then again one needs to know that this is
the correct interval, and not just the underlying set of real numbers
in [0,1] with no intrinsic topology etc.

Best,
David

[Martin Escardo]

On 22/10/14 04:54, Urs Schreiber wrote:
> On 10/22/14, Michael Shulman <shu...@sandiego.edu> wrote:
>
>> This is exactly what cohesive HoTT is about. Cohesive oo-groupoids are
>
>
> Just to amplify: in the standard models [1,2] of cohesive HoTT [3] it
> the shape modality takes it to the homotopy theoretic circle:
>
> shape( R^2-{0} ) = S^1

And so presumably we should also have shape(Circle)=S^1, but, on the
other hand, R^2-{0} and Circle should be different (because they are not
homeomorphic - one is topologically 2-dimensional and the other
1-dimensional).

> Generally, the shape modality takes a topological manifold to its
> fundamental infinity-groupoid, i.e. to its underlying bare homotopy
> type.

Ok, so in such models there is a map Circle -> S^1, because presumably
we always have a map X->shape(X)? (But this is assuming that R are the
correct reals.) What would be HoTT axioms for a shape modality?

Martin

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Martin Escardo]

On 22/10/14 07:20, Michael Shulman wrote:
> On Tue, Oct 21, 2014 at 11:16 PM, Andrej Bauer <andrej...@andrej.com> wrote:
>> Does univalence hold in the cohesive model?
>
> Univalence holds in all (oo,1)-topos models. However, we don't yet
> have models of the cohesive toposes that have strict universes, only
> weakly-a-la-Tarski ones.

But doesn't weakly-a-la-tarski mean that the judgemental-equality axioms
are not validated?

In that case we don't get a model of HoTT as described in the book, right?

So is univalance really compatible with e.g. the uniform continuity of
all maps (N->2)->N, or the epsilon-delta continuity of all maps R (for
the HoTT reals, or for the Dedekind reals)?

Martin

>
>> I suppose the cohesive HoTT should be able to "see" internally that there
>> are no discontinuous maps R -> R. By the way, is R really what we think it
>> is? Does it magically obtain the Euclidean topology when constructed
>> internally?
>>
>> Also, what happens with the Cantor space? Are all maps (2 -> N) -> N
>> continuous, either internally or externally?
>
> After a little more thought, I realized that these questions pertain
> only to hsets, so their answers should be the same as for the
> corresponding ordinary 1-toposes. In other words, take any
> Grothendieck 1-topos satisfying your favorite continuity principles
> that pertain only to hsets (such as R and N); then the (oo,1)-topos of
> oo-sheaves on the same site will be (weakly Tarski) univalent and also
> satisfy the same continuity principles.
>
> Mike
>

[Urs Schreiber]

> On 22/10/14 04:54, Urs Schreiber wrote:
>> On 10/22/14, Michael Shulman <shu...@sandiego.edu> wrote:
>>
>>> This is exactly what cohesive HoTT is about. Cohesive oo-groupoids are
>>
>>
>> Just to amplify: in the standard models [1,2] of cohesive HoTT [3]

>> the shape modality takes the geometric circle to the homotopy theoretic circle:

>>
>> shape( R^2-{0} ) = S^1

On 10/22/14, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> And so presumably we should also have shape(Circle)=S^1,

Yes.

> but, on the other hand, R^2-{0} and Circle should be different (because they are not
> homeomorphic - one is topologically 2-dimensional and the other
> 1-dimensional)

Yes!

>> Generally, the shape modality takes a topological manifold to its
>> fundamental infinity-groupoid, i.e. to its underlying bare homotopy
>> type.
>
> Ok, so in such models there is a map Circle -> S^1, because presumably
> we always have a map X->shape(X)?

Yes!! Shape is a monad, this map is its unit.

> (But this is assuming that R are the correct reals.)

Yes, I referred to the R in the "standard" models that I mentioned.

But there is a neat axiomatic way to characterize this R: it is the
object such that the shape modality is equivalent to localization at
this object, see
http://ncatlab.org/nlab/show/continuum#InCohesiveHomotopyTypeTheory

> What would be HoTT axioms for a shape modality?

Two ways to axiomatize it are given by Mike in our article:

http://ncatlab.org/schreiber/show/Quantum+gauge+field+theory+in+Cohesive+homotopy+type+theory

We used to prefer the second, but the first matches well with imposing
the axiom that there is a type A1 such that Shape is A1-localization,
as above.

The Coq code for these axioms is here

https://github.com/mikeshulman/HoTT/tree/modalities/Coq/Subcategories

But Mike keeps amplifying these days that he is in the process, and
maybe about to be done, with redoing this code from scratch and that
the new version will be much better and that anyone interested in
looking into this should wait just a tad longer for the new version to
be available.

[Martin Escardo]

Ok, thanks. Nice.

Seems to be indeed what I had in mind and an answer to my question "how".

So, for instance, "the universe is [topologically] indiscrete" is best
understood as a theorem of cohesive HoTT. Except that one would have to
see if the notion of indiscreteness considered in the quoted statement
is compatible with the abstract notion of indiscreteness in cohesive
HoTT as in the links you provided.

Martin

[Michael Shulman]

On Wed, Oct 22, 2014 at 1:46 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> But doesn't weakly-a-la-tarski mean that the judgemental-equality axioms are
> not validated?

Yes, the judgmental equalities that are not validated are things like

El(Pi A B) = forall (x:El A), El (B x).

instead we have only an equivalence

El(Pi A B) <~> forall (x:El A), El (B x).

(If I recall correctly, the cubical model also fails to satisfy some
different judgmental equalities that the book uses.)

> So is univalance really compatible with e.g. the uniform continuity of all
> maps (N->2)->N, or the epsilon-delta continuity of all maps R (for the HoTT
> reals, or for the Dedekind reals)?

Technically, you're right: we don't know. But I would be shocked if
one could derive a contradiction from making those equivalences into
judgmental equalities. (-:

Mike

[Michael Shulman]

On Wed, Oct 22, 2014 at 8:03 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> So, for instance, "the universe is [topologically] indiscrete" is best
> understood as a theorem of cohesive HoTT. Except that one would have to see
> if the notion of indiscreteness considered in the quoted statement is
> compatible with the abstract notion of indiscreteness in cohesive HoTT as in
> the links you provided.

In general, of course, they won't be the same. Cohesion is a very
general context which includes many different notions of
codiscreteness, and most of them won't be the same as the
internally-defined notion of "sequential indiscreteness".

However, it's reasonable to hope that sequential indiscreteness is at
least an *example* of cohesion. We could ask that question either
semantically (say, is the topological (oo-)topos cohesive?) or
internally (can we construct the cohesive modalities so that the sharp
types are the sequentially indiscrete ones?).

I think one thing is missing to start with: I don't see why the
topological topos would be locally connected, so there probably isn't
a shape modality. But it is a local topos, so it has sharp and flat
modalities, and the sharp types in that model should coincide with the
internally-defined sequentially indiscrete ones.

Internally, the question is more subtle. We could do an internal
localization at the map N + 1 -> N_oo, but can we *prove* internally
that we get a lex modality, and is there any way to even try to
construct a corresponding flat modality internally?

Mike

[Urs Schreiber]

On 10/22/14, Michael Shulman <shu...@sandiego.edu> wrote:

> I think one thing is missing to start with: I don't see why the
> topological topos would be locally connected, so there probably isn't
> a shape modality.

Yes, one would need to restrict to locally (higher-)connected
topological spaces. Some unfinished note is here:

http://ncatlab.org/nlab/show/locally+contractible+topological+infinity-groupoid

Curiously, this essentially the very origin of the idea of etale
homotopy type in Artin-Mazur's work: they define the etale homotopy
type of a topological space and then observe that it coincides with
the actual homotopy type of that topological space if it is locally
contractible. In this case their construction may be seen to reduce to
the derived colimit functor on simplicial sheaves, hence to the shape
modality.

[Martin Escardo]

Interesting!

M.

[Egbert Rijke]

instead we have only an equivalence

El(Pi A B) <~> forall (x:El A), El (B x).

A countermodel to the above equivalence is the graph model, the mentioned equivalence does not hold. For instance, take the graph A with one vertex and no edges. This graph has no terms, since the terminal graph is a graph with one vertex and one self-loop and terms are equivalently described as maps from the terminal graph. Now there are two different graph morphisms from A to A+A, but there is only one element in El(A) -> El(A+A).

The equivalence we do have is El(Pi A B) <~> El (P). 

With kind regards,

Egbert

 

(If I recall correctly, the cubical model also fails to satisfy some
different judgmental equalities that the book uses.)

> So is univalance really compatible with e.g. the uniform continuity of all
> maps (N->2)->N, or the epsilon-delta continuity of all maps R (for the HoTT
> reals, or for the Dedekind reals)?

Technically, you're right: we don't know.  But I would be shocked if
one could derive a contradiction from making those equivalences into
judgmental equalities.  (-:

Mike

[Michael Shulman]

"El" here means the Tarskian coercion from elements of the universe to
types, not the global sections functor.

[Egbert Rijke]

Ok, then it holds. I guess it just looked weird to me because indeed I think of El as a (general) global sections functor. 

Nevertheless, I think the equivalence El(Pi A B) <~> El(B) is the important one to consider, because that's the one that corresponds to the rules of dependent product types and Tarski-universes are about encoding type theory in a type. The one you mentioned is a mere property of El, but it is not expressing a rule of type theory.

(sorry for the duplicate, Mike)

[Michael Shulman]

Not really. )-: Probably the closest thing is section 2 of
http://ncatlab.org/schreiber/files/QFTinCohesiveHoTT.pdf
but it's very condensed.

On Wed, Oct 22, 2014 at 7:00 PM, Francisco Mota <fm...@cs.cornell.edu> wrote:
> Is there a soft introduction to cohesive HoTT, for people who have read the
> HoTT book and have a bit of familiarity with category theory, but no
> knowledge of cohesive (oo,1)-topoi?
>
> Now that I know that "types as spaces" (in the sense that Martín describes)
> is connected to "spaces as types" (in the oo-groupoid sense) by cohesion, I
> want to learn more about cohesion. Both of these are really powerful ways of
> thinking: "types as spaces" informs us about the possibilities and
> limitations of computation by drawing analogies to topology, and "spaces as
> types" introduces a powerful type theoretic method (path induction) to
> reason about spaces. In any case, this is my current perspective. I'd like
> to understand how these ideas are connected.
>
> Thanks in advance,
> Fran

[Egbert Rijke]

El(B) is the terms of B, which is a type in some context just like any other.

[Michael Shulman]

Sorry, I can't figure out what you mean. Here's the rule for El for a
Tarski universe U:

G |- A:U
---------------
G |- El(A) type

Now the Pi-formation rule on U is

G |- A:U G, x:El(A) |- B:U
-----------------------------
G |- Pi A B : U

We can therefore derive

G |- A:U G, x:El(A) |- B:U
-----------------------------
G |- El(Pi A B) type

and

G |- A:U G, x:El(A) |- B:U
------------------------------------
G |- A:U G, x:El(A) |- El(B) type
------------------------------------
G |- forall x:El(A), El(B(x)) type

With an ordinary Tarski universe, one of the rules of the theory is
that these two types would be judgmentally equal. A weakly Tarski
universe asserts instead that they are equivalent.

El(B) is a type in a different context than El(Pi A B), so they can't
be equivalent.

Mike

[Urs Schreiber]

To come back, for completeness, to the question in which models the
internal reals are represented by the external reals.

In MacLane-Moerdijk "Sheaves in Geometry and Logic", theorem 2 in
chapter VI, section 9 shows that this is the case in all the sheaf
toposes over full subcategories S of Top that include the real numbers
and which are closed under open subsets and finite limits.

But looking through the proof, it seems (but check) that closure under
open subsets and finite limits is needed only to guarantee that the
subcategory inherits a Grothendieck topology from Top. However, the
argument would seem to still go through if only a "coverage" were
inherited. If so, then this would include the cases

S = { locally contractible topological spaces }

and

S = { topological manifolds }

whose toposes and infinity-toposes are cohesive.

I made a note here:

http://ncatlab.org/nlab/show/real+numbers+object#InGrosToposOnTopologicalSpaces

But check. (Thanks to Zhen Lin Low and to David Roberts on the nForum
for sharing hints.)

On 10/22/14, Michael Shulman <shu...@sandiego.edu> wrote:

[Michael Shulman]

On Wed, Oct 22, 2014 at 11:37 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> However, it's reasonable to hope that sequential indiscreteness is at
> least an *example* of cohesion. We could ask that question either
> semantically (say, is the topological (oo-)topos cohesive?) or
> internally (can we construct the cohesive modalities so that the sharp
> types are the sequentially indiscrete ones?).
>
> I think one thing is missing to start with: I don't see why the
> topological topos would be locally connected, so there probably isn't
> a shape modality. But it is a local topos, so it has sharp and flat
> modalities, and the sharp types in that model should coincide with the
> internally-defined sequentially indiscrete ones.

An off-list discussion with Martin has revealed that the cohesive
notion of "indiscrete" is different from the meaning of "indiscrete"
in his theorem "the universe is indiscrete", even in the topological
topos. According to Martin's definition a type is indiscrete if every
sequence converges to every point in *some* way, but it might do so in
more than one way. Whereas the cohesively-indiscrete types in the
topological topos are those for which every sequence converges to
every point in *exactly* one way.

Internally, Martin's indiscrete types are those that are *injective*
with respect to N+1 -> N_oo, whereas to obtain a reflective
subuniverse we would want to consider those that are *local* with
respect to that map.

Mike

[Martin Escardo]

Since Mike mentioned this, here is a little bit more information about
the same sequence converging to the same point in more than one way:

On 30/10/14 18:12, Michael Shulman wrote:
> Internally, Martin's indiscrete types are those that are *injective*
> with respect to N+1 -> N_oo, whereas to obtain a reflective
> subuniverse we would want to consider those that are *local* with
> respect to that map.

The universe is injective with respect to embeddings (maps whose
fibers are propositions), and the above N+1 -> N_oo is an
embedding. (It is also a not-not-dense embedding: the complement of
its image is empty. But it is a surjection iff LPO holds.)

If f:X->Y is an embedding (it fibers are propositions), then any
g:X->U has two canonical extensions Y->U along f, which I write g/f
and g\f:

(g/f)(y) = Pi(w : f^{-1}(x)). g(pr1 w)
= Pi(x : X). (f(x) = y) -> g x.

(g\f)(y) = Sigma(w : f^{-1}(x)). g(pr1 w)
= Sigma(x : X). (f(x) = y) & g x.

We always have

(g\f)(y) -> h(y) -> (g/f)(y), (*)

for any extension h:Y->U of g along f, and g\f and g/f are extensions:

(g\f)(f x) = (g/f)(f x) = x. (**)

If y is not in the range of f (i.e. f x /= y for all x),

(g\f)(y)=0 and (g/f)(y)=1. (***)

Now, in the case of the embedding f:N+1 -> N_oo, there is no y that is
not in the range of f, and so (***) never applies.

This doesn't mean that (**) always applies. In fact:

g\f = g/f for all g:X-> U iff LPO.

It suffices to consider g = \lambda x.1 to see (=>), and the other
direction is clear. Hence not even the constant sequence 1 converges
to 1 in a unique way, unless LPO holds.

But LPO (in addition to being a constructive taboo) is rather
uninteresting in this context: Its weakening WLPO is equivalent to
saying that all types are indiscrete in the sense of being injective
over the map f:N+1 -> N_oo, and also to all types being indiscrete in
Mike's sense, in the sense of being f-local.

Martin

[Michael Shulman]

On Thu, Oct 30, 2014 at 2:45 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> If f:X->Y is an embedding (it fibers are propositions), then any
> g:X->U has two canonical extensions Y->U along f, which I write g/f
> and g\f:

In topos-theoretic language, with g reinterpreted as a type over X, we
are saying that the pullback functor E/Y -> E/X has both a left and a
right adjoint, and when f is an embedding both of these adjoints are
fully faithful, hence their unit and counit (respectively) are
equivalences.

> But LPO (in addition to being a constructive taboo) is rather
> uninteresting in this context: Its weakening WLPO is equivalent to
> saying that all types are indiscrete in the sense of being injective
> over the map f:N+1 -> N_oo, and also to all types being indiscrete in
> Mike's sense, in the sense of being f-local.

Interesting. So there are actually two different notions of "f-local"
worth considering here. The obvious internal notion of f-local
("precomposition with f is an equivalence on maps into X") corresponds
externally to locality at all maps of the form A × f.

There is a stronger notion which asserts that all maps into X out of
any fiber of f are constant, in the strong sense that const : X ->
(fib(f,b) -> X) is an equivalence. The homotopy-theoretic term for
const being an equivalence is that X is "fib(f,b)-null", so in this
case we could perhaps call X "fib(f)-null". Externally, this
correspond to locality at all *pullbacks* of f (note that the maps of
the form A × f are the pullbacks of f along product projections).

The advantage of the second notion is that while the f-local types
(for any map f, or indeed for any family of maps f) are a reflective
subuniverse, the fib(f)-null types are a modality. Moreover, if f is
an embedding, like N+1 -> N_oo, then the fib(f)-null types are a lex
modality, i.e. externally a subtopos. This is exactly what is assumed
of the codiscrete types in cohesive HoTT.

I would speculate that for f : N+1 -> N_oo, the subtopos of
fib(f)-null types should be the largest subtopos satisfying some sort
of principle of omniscience. By analogy, if f is the inclusion of the
decidable hprops into (an impredicative) hProp, then the fib(f)-null
types are the double-negation-sheaves, which form the largest Boolean
subtopos and the smallest dense subtopos.

Mike

[Martin Escardo]

On 30/10/14 23:30, Michael Shulman wrote:
> There is a stronger notion which asserts that all maps into X out of
> any fiber of f are constant, in the strong sense that const : X ->
> (fib(f,b) -> X) is an equivalence. The homotopy-theoretic term for
> const being an equivalence is that X is "fib(f,b)-null", so in this
> case we could perhaps call X "fib(f)-null". Externally, this
> correspond to locality at all *pullbacks* of f (note that the maps of
> the form A × f are the pullbacks of f along product projections).

(By the way, Johnstone says that an object X of a topos is D-discrete
if the map const:X->(D->X) is an isomorphism. So you are suggesting
the definition that X is indiscrete iff it is D-discrete for each
fiber D of f:N+1->Noo.)

I've also checked that the universe is f-local in this stronger sense
iff LPO:

The fibers of f are all propositions P such that not-not-P holds.

But now you can calculate easily that if const : U -> (P -> U) is an
equivalence for a proposition P, then P. If you unfold this for the
case where the P's are the fibers of f, then all the strong f-locality
of U means that all fibers of f "hold", which amounts precisely to LPO.

But with LPO, for any type (not only U), indiscrete as injectivity
over f, indiscrete as weakly f-local, and indiscrete as strongly
f-local, all coincide.

So the only way U can be indiscrete, in the absence of LPO, is in my
weak sense: every sequence of types converges to any type, but not
necessarily in a unique way.

However, notice that we cannot show that there is a sequence that
converges to a type in more than one way, because LPO potentially
holds, in the sense of being consistent, in which case, as we have
seen, any sequence converges to a point in at most one way.

> The advantage of the second notion is that while the f-local types
> (for any map f, or indeed for any family of maps f) are a reflective
> subuniverse, the fib(f)-null types are a modality. Moreover, if f is
> an embedding, like N+1 -> N_oo, then the fib(f)-null types are a lex
> modality, i.e. externally a subtopos. This is exactly what is assumed
> of the codiscrete types in cohesive HoTT.

Right. So the conclusion is that "the universe is indiscrete" (in my
weak sense) is not, after all, a theorem of cohesive HoTT.

> I would speculate that for f : N+1 -> N_oo, the subtopos of
> fib(f)-null types should be the largest subtopos satisfying some sort
> of principle of omniscience. By analogy, if f is the inclusion of the
> decidable hprops into (an impredicative) hProp, then the fib(f)-null
> types are the double-negation-sheaves, which form the largest Boolean
> subtopos and the smallest dense subtopos.

Interesting.

Martin