"geometric realization"

[Daniel R. Grayson]

Following up on the discussion today, in which Steve mentioned geometric realization, is there a general construction transforming types to types that would do the following?  It would accept as input the quotient of the real numbers, with the real numbers as constructed in Andrej's chapter, by the additive action of the group of integers; think of that as the classical circle.  It would produce as output the HIT circle.

[Michael Shulman]

The real numbers constructed in Andrej's chapter are just a set.
You'd need to first define some sort of "topology" on them in order to
expect to get something nontrivial. But it seems possible that from
any internally defined topological space (i.e. an hset together with a
topology on it), one could first build its singular simplicial hset,
then geometrically realize that as some sort of HIT. It might even be
achievable now, since we do know how to define (semi)simplicial hsets
(e.g. Richard's talk last week).

> --
> You received this message because you are subscribed to the Google Groups
> "IAS Univalent Foundations" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to univalent-founda...@googlegroups.com.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at
> http://groups.google.com/group/univalent-foundations?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[Peter LeFanu Lumsdaine]

On Tue, Mar 12, 2013 at 5:28 PM, Michael Shulman <virit...@gmail.com> wrote:

The real numbers constructed in Andrej's chapter are just a set.
You'd need to first define some sort of "topology" on them in order to
expect to get something nontrivial.  But it seems possible that from
any internally defined topological space (i.e. an hset together with a
topology on it), one could first build its singular simplicial hset,
then geometrically realize that as some sort of HIT.  It might even be
achievable now, since we do know how to define (semi)simplicial hsets
(e.g. Richard's talk last week).

On this last point: do we know how to realize a (semi-)simplicial hset as a type, though?

I thought we still had essentially the same problem as with defining diagrams over, and limits of, 1-categories — that while we can define the structures themselves by adding hset restrictions, one can’t get diagrams over them, or equivalently their limits/colimits, without running into the same old coherence issues.

–p.

[Michael Shulman]

We can't get diagrams of arbitrary types, but we can get diagrams of
hsets, which is all that this construction would need. I agree it's
not immediately obvious how to define the (homotopy) colimit of such a
thing -- hence why I said "might" -- but it could be that in the
semisimplicial case, at least, we could fudge this just enough to make
it work by inducting up dimensions.

[Urs Schreiber]

Hi,

There is another way to implement the notion of geometric realization
in HoTT, which might have its advantages.

To start with, notice that for example the infinity-topos over the
site of manifolds (topological or smooth) carries a higher modality S
which exhibits geometric realization of infinity-stacks in the
traditional sense (the "shape modality"
http://ncatlab.org/nlab/show/shape+modality).

Also, this infinity-topos has a ring object R which is such that S is
equivalently the localization functor at (-) x (R --> *). In
particular the geometric realization of R is contractible S(R) = *.
This R is not the interval type, but is a geometric analog of it. It
is much like the A in Voevodsky's A1-homotopy theory. It is a
"cohesive continuum object"
(http://ncatlab.org/nlab/show/continuum#InCohesiveHomotopyTypeTheory).

Similarly, the quotient R/Z is not the circle homotopy type BZ = *//Z,
but is a 0-type which is the actual geometric circle. Its geoemtric
realization is the homotopy circle

S( R/Z ) = *//Z = BZ

as soon as the shape modality respects the homotopy fiber sequence Z
--> R --> R//Z.

One can therefore try to implement "geometric realization" in homotopy
type theory by adding the above structure as axioms. This is what
cohesive homotopy type theory is about.

http://ncatlab.org/nlab/show/cohesive+homotopy+type+theory#GeometricSpacesAndTheirHomotopyTypes
.

Adding this simple axiom of geometric realization to HoTT goes a long
way. It implies much more than just geometric realization of circles
to homotopy circles. For instance it implies also all this structure
here: http://ncatlab.org/schreiber/show/Higher+geometric+prequantum+theory
(start looking at section 2.3 for the axioms of cohesion in HoTT).


Best,
Urs

[Michael Shulman]

I agree that that's very interesting, but it is of course doing
something entirely different from the original question.

[Urs Schreiber]

> I agree that that's very interesting, but it is of course doing
> something entirely different from the original question.

The silent suggestion is: possibly it's useful not to formalize the
real numbers as in the question, but instead to formalize a line
object as a cohesively contractible ring object.

Of course it depends on what exactly one is after.

But I'll be silent now. Maybe I shouldn't be posting here at all.
Sorry for the intrusion.

[Michael Shulman]

I think certainly it's useful, but it's going to be useful for
different things. Eventually, if using HoTT as a foundation for all
of mathematics, one might want to formalize the real numbers as in the
original question and then use them to *construct* the cohesive topos
models of type theory with their modalities.

[Daniel R. Grayson]

Re: "Adding this simple axiom of geometric realization to HoTT goes a long
way. "

Which simple axiom?

[Martin Escardo]

(I wasn't in the discussion today, as I am far away geographically.)

This discussion interests me very much for two (related) reasons:

(1) I have a long term interest in real-number computation /
constructive analysis.

(2) I have a long term interest in the view of types as (topological)
spaces (in which the reals automatically get, for computational
reasons, their natural topology).

(Both since the last millenium.) Homotopy type theory gives a new,
fresh view regarding both. But I feel that somehow the old and new
topological views have failed to interact in the way they should (and
I had very nice discussions with Bas and Thierry when I visited the
IAS a few weeks ago, with potentially interesting outcomes and
proposals by both).

I gave a talk at the IAS in which I explained the "old" topological
view, with Johnstone's topological topos as a model (among other
possible ones, mentioned and unmentioned).

For example, in this old view, the type N is a discrete space (with
discreteness manifested by decidable equality in the type theory), and
the Cantor type (N->2), with 2=1+1, is the Cantor space (topological
product of countably many copies of the discrete two-point space).

A question that I will get to in a moment is "how is the natural
topology on the (set?) of reals manifested in the type theory"? But
let me begin with a simpler question.

How is the Cantor topology of (N->2) manifested in the type theory
(independently of any intended model)? In two ways:

(1) Meta-mathematical (i.e. "about type theory"). E.g. every definable
function (N->2)->N is uniformly continuous, with continuity expressed
in type theory, but derived by meta-mathematical means. (So, you see,
even the compactness of (N->2) is manifested in the type theory, via
the uniformity of the continuity.)

(2) Mathematical (i.e. "in type theory"). E.g. if you have a
hypothetical (rather than defined) function (N->2)->N with a
hypothetical claim that it is not continuous, you (constructively) get
a Brouwerian counter-example or Aczelian taboo (a constructively
dubious instance of excluded middle which is neither provable nor
disprovable, such as (W)LPO (Bishop's (weak) principle of
omniscience), which e.g. solves the Halting problem).

We can summarize this as saying that functions (N->2)->N are
"secretly" (uniformly) continuous. You cannot prove that, you cannot
disprove that, but (i) there is a model in which this is true, and
(ii) if this were not true, the (basic) type theory would not be
constructive (in any reasonable sense).

(The model of (Kan) simplicial sets renders (N->2) discrete
(e.g. in its geometric realization), which is "wrong".)

This is similar to univalence. In the basic type theory (without any
axioms other than Martin-Loef's), it is neither provable or
disprovable, it has a model, and, moreover, it is (or should be) a
meta-theorem that any two isomorphic definable types satisfy the same
definable properties (has anyone tried to prove that?).

This is also similar to the interpretation of identity types as
paths. Secretely, identity types are path spaces. (Elaborate on this
point yourself.)

Now let's come back to "the" type of reals (whatever this ends up
being in Andrej's hands). It should be the case that all functions
R->R are "secretly" continuous in the above sense, but they will not
be provably continuous *unless* we postulate axioms in the sense of
the "old" style. But even if we don't postulate such axioms (we don't
need to), the definition of the type of reals *should* be compatible
with such old-style axioms (and models).

A feature of constructive mathematics, and constructive type theory in
particular, is that the independence of many propositions is a rule
rather than a shocking, undesired surprise. An art in constructive
meta-mathematics is to decide undecided mathematical statements by
more than just postulating them (or their negation), but also by
making them computationally good (e.g. by providing a computational
interpretation of univalence, continuity, bar recursion and
what-you-have).

Intuitively, but most like not in fact, a model reconciling the old
and new topological / homotopical views of type theory should consist
of *simplicial (Kan) spaces" rather than "simplicial (Kan) sets".

To have the reals (to be) defined by Andrej in the book to
(automatically) get the right topology one needs a model reconciling
the old and new views, as well as (workable, computationally
meaningful) axioms corresponding to it.

The claim I make is that many hsets (starting with (N->2)) have a
non-trivial (secret) topology that is unaccounted for both by the
(current) axioms and by the (current) models of HoTT. I say this
again: the geometric realization of (N->2) is discrete, which doesn't
account for what goes on in the type theory.

Before HoTT, I imagined types as topological space (with "topological"
refined in appropriate ways, e.g. via locales). After HoTT, I imagine
types as topological omega-groupoids, but I don't know what such
things are or could be.

Coming back to the original question, the geometric realization, at
the moment, ignores any existing topological structure in the
omega-groupoids (like (N->2) and R), and builds a topology based on
the algebraic data (in the tradition of algebraic topology, of
course). In fact, any hset gets to be discrete in its geometric
realization, and Andrej wants an hset of reals (and I want this hset,
like you, to automatically get the right topology).

I hope this makes just a little bit of sense. I apologize if I am
dumping a lot of thoughts and facts together without much elaboration.

Best,
Martin

[Michael Shulman]

On Tue, Mar 12, 2013 at 4:52 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> After HoTT, I imagine
> types as topological omega-groupoids, but I don't know what such
> things are or could be.

One thing that they could be is infinity-sheaves on a site of
topological spaces:

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

The particular notion discussed on that page is defined using a site
of "well-behaved" spaces, which is probably not what is wanted here.
But one might similarly consider infinity-sheaves on a site consisting
of spaces like 2^N.

[Michael Shulman]

... which means that you may actually be more interested in the
direction Urs was suggesting. (-:

[Andrej Bauer]

In a conversation with Dan today I mentioned something he found
illuminating, so perhaps I can write it on the list, too.

I always object when people say "discrete type" and they mean "hset".
A type only deserves to be called discrete if it behaves like a
discrete space, which means that the equality relation must be "open",
whatever that means. However, hsets are nowhere close to having this
quality (in general). There are hsets that cannot be decomposed into
two parts in *any* way. For example, the reals (whatever they turn out
to be in my hands) cannot be written as a disjoint sum of two
inhabited types. In other words, you cannot exhibit a non-constant map
R -> 2. For all practical purposes R is going to behave like a true
idecomposable continuum.

Exactly the same thing happens in any kind of intuitionistic math.
Intuitionistic sets are more like topological spaces and less like
classical sets.

Martin and I are on the same wavelength here. We both feel very
strongly that types *are* (also) topological spaces. The simplicial
sets model is highly misleading because it completely destroys the
topology (but keeps around the homotopy). For the same rason the
simplicial set model is misledaing when it comes to questions of
computation. We need a better model.

With kind regards,

Andrej

[Guillaume Brunerie]

Is it correct to say that if we had a constructive version of the
simplicial sets model (or any other constructive model of univalence),
then we could just interpret it in the topological topos and we would
get a topological + homotopical model (based on internal
(semi?)-simplicial sets to the topological topos)?

Guillaume

[Steve Awodey]

it seems we don't yet understand the relationship between the reals as a type-behaving-like-a-space, which has no non-constant maps to 2, and the hset of reals, which has very many such.
I think this calls for some more thought before just developing the reals in the usual constructive style.
perhaps the difference between your and Martin's intuitions about that construction, on the one hand, and the simplicial model, on the other,
is not just a defect in the latter, but is pointing to a defect in our understanding of the best way to formalize the real numbers in HoTT.

Steve

[Bas Spitters]

Maybe this should be compared to SDG instead of to the topological topos (?)

[Guillaume Brunerie]

On 2013/3/12 Steve Awodey <awo...@cmu.edu> wrote:
> it seems we don't yet understand the relationship between the reals as a type-behaving-like-a-space, which has no non-constant maps to 2, and the hset of reals, which has very many such.

No, there are not very many such, there is no way to define a
non-constant map from the hset of reals (the one being developped in
the last part of the book, using Cauchy sequences, and for which 0 and
1 are not equal) to 2, unless you allow axioms like excluded middle.
In the simplicial set model there are many such maps, but none of them
is definable in the type theory.

Guillaume

[Steve Awodey]

On Mar 12, 2013, at 10:29 PM, Guillaume Brunerie <guillaume...@gmail.com> wrote:

> On 2013/3/12 Steve Awodey <awo...@cmu.edu> wrote:
>> it seems we don't yet understand the relationship between the reals as a type-behaving-like-a-space, which has no non-constant maps to 2, and the hset of reals, which has very many such.
>
> No, there are not very many such, there is no way to define a
> non-constant map from the hset of reals (the one being developped in
> the last part of the book, using Cauchy sequences, and for which 0 and
> 1 are not equal) to 2, unless you allow axioms like excluded middle.
> In the simplicial set model there are many such maps, but none of them
> is definable in the type theory.
>

that's exactly my point: the construction currently given in the last part of the book -- which is the usual way of making the constructive reals -- produces something very different from the classical "set of real numbers".
I'm urging that we should step back and rethink this situation, in the hope that HoTT might provide a more useful resolution than merely repeating the old saw about constructive mathematics making the reals into an indivisible continuum, etc.

Steve

[Martin Escardo]

On 13/03/13 02:16, Guillaume Brunerie wrote:
> Is it correct to say that if we had a constructive version of the
> simplicial sets model (or any other constructive model of univalence),
> then we could just interpret it in the topological topos and we would
> get a topological + homotopical model (based on internal
> (semi?)-simplicial sets to the topological topos)?

Definitely. This was alluded to by "(Kan) simplicial space" in my message.

If the proof that Kan simplicial sets model univalence were constructive
(which I learned during my visit, from Thierry and Marc, that it can't
be) then you would be done in the enterprise of reconciling the "old"
and "new" topological views of types.

And the first parenthetical remark is also correct.

Best,
Martin

[Steve Awodey]

On Mar 12, 2013, at 11:03 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> If the proof that Kan simplicial sets model univalence were constructive (which I learned during my visit, from Thierry and Marc, that it can't be

what does this mean?

[Martin Escardo]

Regarding my parenthetical remark, ask Marc and Thierry. In summary, if
I understood what they explained to me, they get an argument that no
proof that Kan simplicial sets form a model with a univalent universe
can be constructive, by a clever and simple Kripke model. Marc wanted to
go further, and get away with a Brouwerian counter example, but I left
just after the discussion got interesting. I apologize to them, because
they may feel that their thoughts are not ready for public display, but
I inadvertently mentioned them in the heat of email exchanges. Sorry,
Marc & Thierry.

(Regarding the statement, I believe Guillaume explained it well and you
would agree with him.)

Best,
Martin

[Bas Spitters]

The remark is on p3 of the note that Thierry send to the list.
It is "difficult" to prove that B is Kan implies B^A is Kan.

On Tue, Mar 12, 2013 at 11:28 PM, Martin Escardo

[Steve Awodey]

On Mar 12, 2013, at 11:28 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

>
>
> On 13/03/13 03:11, Steve Awodey wrote:
>>
>> On Mar 12, 2013, at 11:03 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>>
>>> If the proof that Kan simplicial sets model univalence were constructive (which I learned during my visit, from Thierry and Marc, that it can't be
>>
>> what does this mean?
>
> Regarding my parenthetical remark, ask Marc and Thierry. In summary, if I understood what they explained to me, they get an argument that no proof that Kan simplicial sets form a model with a univalent universe can be constructive, by a clever and simple Kripke model. Marc wanted to go further, and get away with a Brouwerian counter example, but I left just after the discussion got interesting. I apologize to them, because they may feel that their thoughts are not ready for public display, but I inadvertently mentioned them in the heat of email exchanges. Sorry, Marc & Thierry.

very mysterious ….
sorry, but I don't accept secret results as arguments.

Are you trying to say that Univalence is somehow non-constructive?
I see no problem in principle with having a constructive model of univalence -- in fact, there is a very straightforward such model using internal groupoids.
The Kan simplicial set model can be seen as the infinity-groupoid generalization of this.
The main difficulty in internalizing this model lies in the notion of infinity gropoid, in my opinion, not in any principled obstruction involving constructivity.

Steve

[Guillaume Brunerie]

On 2013/3/12 Steve Awodey <awo...@cmu.edu> wrote:
> that's exactly my point: the construction currently given in the last part of the book -- which is the usual way of making the constructive reals -- produces something very different from the classical "set of real numbers".
> I'm urging that we should step back and rethink this situation, in the hope that HoTT might provide a more useful resolution than merely repeating the old saw about constructive mathematics making the reals into an indivisible continuum, etc.

I’m not sure I understand what you mean. Do you want a set of reals in
pure HoTT (no excluded middle or axiom of choice) where we can define
e.g. the characteristic function of {0}?

Guillaume

[Martin Escardo]

On 13/03/13 03:36, steve awodey wrote:
> Are you trying to say that Univalence is somehow non-constructive?

Not at all.

[Andrej Bauer]

> On 2013/3/12 Steve Awodey <awo...@cmu.edu> wrote:
> that's exactly my point: the construction currently given in the last part of the book -- which is the usual way of making the constructive reals -- produces something very different from the classical "set of real numbers".
> I'm urging that we should step back and rethink this situation, in the hope that HoTT might provide a more useful resolution than merely repeating the old saw about constructive mathematics making the reals into an indivisible continuum, etc.

To me the situation is perfectly clear. The real numbers in HoTT are
of the constructive idecomposable kind. This is *good* as it mans that
HoTT already captures some topological nature of the reals. Nobody
whines that there is no continuous map from R to 2, so why should we
worry about there being no such computable map?

But the argument for constructivity need not even involve reals.
Already Cantor space N -> 2 exhibits cohesion. For if it has decidable
equality then we can construct the Halting Oracle. (This is what
Martin calls a tabu.)

I do not understand what we should be "stepping back from" and what
there is to rethink. If you want a classical world you're free to
assume classical axioms. It is more honest to admit that HoTT, being a
constructive type theory, produces constructive mathematics.

With kind regards,

Andrej

[Andrej Bauer]

> On 2013/3/12 Steve Awodey <awo...@cmu.edu> wrote:
> that's exactly my point: the construction currently given in the last part of the book -- which is the usual way of making the constructive reals -- produces something very different from the classical "set of real numbers".
> I'm urging that we should step back and rethink this situation, in the hope that HoTT might provide a more useful resolution than merely repeating the old saw about constructive mathematics making the reals into an indivisible continuum, etc.

I would classify this as the third stage of accepting mathematics,
which is bargaining.

[Steve Awodey]

oh spare me, please.

in a Grothendieck topos of sheaves on a space, we have both the sheaf of real-valued functions (which is often the Dedekind reals), the Cauchy reals constructed internally, the Cauchy completion of the rationals, the ideal completion of the rationals ("McNeil completion"), the order completion of the field of fractions of the rationals, the "long interval" as a HIT, the constant sheaf of reals (which has the same infinitary FOL as the set-theoretic reals -- including all the same algebraic properties), the space 2^N of binary sequences, and lots of other reasonable candidates for a "type of reals".

these things can all have very different sets of points Hom(1, R), subobject lattices Hom(R, Omega), complemented subobjects Hom(R, 2), etc.

all I'm saying is that you shouldn't be so dogmatic (yes, it's getting personal now) about what the one "right" notion of reals ought to be, based on your prejudices -- er, intuitions -- from working in last-generation systems of extensional type theory. maybe it would be useful to consider some of the other possible "types of reals" in this new setting of intensional type theory with UA and HITs, before charging ahead with the usual development of constructive real numbers, with all its familiar problems and issues.

good night,

Steve

[Michael Shulman]

The problem of the multiple meanings of "discrete" is not new; it's
plagued some parts of category theory quietly for a while (e.g. is a
"discrete topological category" one with a discrete topology or one
with only identity arrows?). Of course, it has its origins in the
unfortunate (but historically, completely understandable)
identification of topological spaces with the infinity-groupoids that
they present. Since topologically-discrete topological spaces present
infinity-groupoids which are hsets, people started using "discrete"
for the latter as well without even realizing that it was a different
notion.

We may choose to reserve "discrete" for the topological meaning rather
than the categorical one, but I think we should be clear that it is a
choice, and a local one. By now, the word "discrete" has (at least)
two meanings in mathematics; we have no right to say that one of them
is correct and the other is wrong. I agree it's better to say "set"
when that's what we mean, becase it is unambiguous; maybe we can also
find an unambigous word for "discrete in the natural topology of
intuitionistic types". (I would particularly like this because yet
another notion of "discrete type" arises in cohesive HoTT, so it would
be nice to have the word available there too. Although as came up
earlier, this notion may not be completely unrelated to the
topological one.)

[Michael Shulman]

On Tue, Mar 12, 2013 at 9:25 PM, Steve Awodey <awo...@cmu.edu> wrote:
> the construction currently given in the last part of the book -- which is the usual way of making the constructive reals

No, it's not. The construction in section 10.2.1 uses higher
inductive-recursive types (the first real application of those that I
know of -- I guess maybe we'd better get busy figuring out whether
they exist in semantic models). It is similar to the usual
constructive approach using Cauchy sequences, but appears to be better
behaved in a way that only HITs make possible. I think this is a
really exciting development and worth pursuing! (Has anyone decided
exactly what this new construction produces in, say, sheaf models?)

I didn't think Andrej was being dogmatic about there being a unique
"the reals" in HoTT. His sketch of chapter 10 proposes to discuss
Dedekind reals as well as Cauchy reals, which are probably not the
same. (Is this known to be the case even for the HIT Cauchy reals? I
have heard that one can make the Cauchy reals agree with the Dedekind
reals by considering Cauchy filters or nets rather than sequences; is
this worth thinking about?) Rather, I thought Andrej was being
dogmatic about regarding intuitionistic sets as topologized. (-:

It seems to me a little disingenuous to say things like that the
constructive reals "are different from the classical reals". I think
one really means that they *might be* different from the classical
reals. Since adding an entirely consistent axiom (LEM) causes them to
become exactly the classical reals, we cannot assert definitely that
they are any different from the classical reals. Similarly, such
statements as "There are hsets that cannot be decomposed into two
parts in any way" are not true in the same way as "1+1=2" is, i.e.
they are not theorems of HoTT -- they are only theorems *about* HoTT.

You wouldn't say the axiom of choice is false in ZF; you would say
that ZF doesn't *prove* the axiom of choice, that it is consistent
with ZF to assume the axiom of choice to be false, etc. Similarly, I
would say instead that there are hsets which HoTT cannot *prove* to be
decomposable into two nontrivial parts.

In particular, even to a classical mathematician, the object that
Andrej is writing about in Chapter 10 is "the reals". It's just that
he's not assuming as many axioms as they would prefer to, and hence he
can't prove as much about it -- in particular, he can't prove that it
can be decomposed into any two nontrivial parts. It's interesting and
important that we can use topology (and topological models) to
quantify his inability to do this. But that doesn't mean that the
reader of Chapter 10 is forced to believe that "the set of reals"
necessarily comes with a nontrivial topology on it.

Mike

[Andrej Bauer]

I apologize for the joke turning into a jape on its way through email servers.

But we can turn this into a useful mathematical discussion, I hope. I
understand of course what sort of thing you're looking for. My point
is that if you ask for too much, you lose the computational content.

In a paper with Jens Blanck [1] we devoted some attention to how to
state completeness of a metric algebra so that it does not "bake in"
any computational content. This is possible, but one has to avoid
mentioning a distance function, because that in itself already imposes
a non-trivial computability structure, not to mention that it
presupposes real numbers R. The idea, following Fred Richman, and as
Dan pointed out to me today also Bourbaki, is to phrase metric as a
uniformity structure. When this is done carefully, see Definition 4 of
[1], the axioms are all negative formulas. In the language of HoTT
they are mere propositions. I shall use this notion of metric (which
in [1] is called a premetric), as it is imposes fewest assumptions on
what a metric space could be, and it does not even presuppose a notion
of real numbers.

Every example of "reals" you mentioned, as well as a host of others in
realizability models, is a complete metric space under this notion of
metric. For example "Nabla R", where Nabla : Set -> RT(A) is the
embedding of sets into a realizability topos, is a complete metric
space (Proposition 7 of [1]), even though Nabla R has absolutely zero
computational content (it satisfies Troelstra's uniformity principle).

Suppose R is a ring (of characteristic 0) with unit in which 2 is
invertible, and a complete metric space, such that the operations are
continuous w.r.t. to the metric. Again, all examples you mentioned
satisfy these conditions. Suppose furthermore that R can be written as
a union of two disjoint parts, one of which contains 0 and the other
all powers of 1/2. Then we can define the Halting Oracle as a map N ->
{0,1}. Therefore, we cannot have good computational properties
together with a decomposable complete ring (of characteristic 0 with
invertible 2). Once again, I am using a very weak notion of metric and
completeness that is going to be satisfied by just about any notion of
"reals" anyone is likely to propose.

Clearly, we have used too strong a notion of decomposability when we
asked that R be expressible as a disjoint union of two parts. We can
weaken this condition, for example we could say that there are two
disjoint parts A and B such that every x in R is merely in A or in B.
Such an object would then give us "merely LPO", so no harm is done to
computation.

Question 1: does "merely LPO"

forall f : nat -> 2, merely ((forall n, f n = 0) or merely (exists n, f n = 1))

hold in HoTT? Perhaps some other slight variant of it?

The construction of R in the HoTT book that Bas and I are working on
is not quite the same as the usual constructive ones. For example, the
archimedean axiom holds in a mere sense: for every real there merely
exists an integer above it. Consequently, every real can be merely
approximated by a rational (to a given precision). On the other hand,
Bas and I believe that this particular R is the minimal
Cauchy-complete field containing Q. So it is a very natural object to
consider whose computational properties hinge on the computational
meaning of "forall merely exists" statements.

Question 2: what is the computational content of "forall merely
exists" statements in HoTT, if any?

And a third question:

Question 3: is there a complete ring R of characteristic 0 in which 2
is invertible and such that R can be merely decomposed into two parts,
one of which contains 0 and the other all powers of 1/2?

In a realizability topos this is doable if we replace "merely" by "not
not", just use Nabla R. But this uses the fact that the not-not stable
truth values form an object, so the corresponding assumption in HoTT
would be impredicativity of mere propositions. Can we do it without
impredicativity?

So, I hope you see that I am not just speaking off the top of my head.
I have put considerable thought into constructions of real numbers,
and I am well aware of the possibilities, but more importantly, of the
limitations. And, as a matter of personal interest, I do not
particularly wish to look for versions of real numbers which we cannot
compute with, especially since my (of the top off my head) guess is
that the answers to the the questions are "no", "none" and "probably,
but what is it good for?".

With kind regards,

Andrej

[1] http://www.jucs.org/jucs_16_18/canonical_effective_subalgebras_of/jucs_16_18_2496_2522_bauer.pdf

[Sergey Melikhov]

> Martin and I are on the same wavelength here. We both feel very
> strongly that types *are* (also) topological spaces. The simplicial
> sets model is highly misleading because it completely destroys the
> topology (but keeps around the homotopy). For the same rason the
> simplicial set model is misledaing when it comes to questions of
> computation. We need a better model.

Let me point out that a first-order fragment of type theory
does have a model which appears to be satisfactory (in particular,
in that it has a univalent universe) from the topological view
advocated by Martin and Andrej.

This first order fragment naturally does not admit dependent
products over other dependent products, in particular, we cannot
write (A->B)->C in this fragment. Worse yet, we'll only allow
dependent products over a prescribed class of "quantifiable" types.
But it can be postulated that quantifiability is preserved by
conjunction, disjunction and even by negation, so that things like
"not (not A or B) or C" can be written for quantifiable A, B, C.
I don't include any inductive types in this fragment (I guess
they could be included, but without preserving quantifiability).

If we forget about the universe for a moment, there is an obvious
topological model for this first order fragment (which aparently
sits inside of Johnstone's topological topos mentioned by Martin):
metric spaces as types, with compact metric spaces as quantifiable
types, continuous maps as substitution maps, Hurewicz (or Serre,
if you like) fibrations as display maps, the usual function space
X^I as the identity type (the inclusion of X in X^I is a cofibration
if X is a metric space), and dependent products modelled by
the space of all continuous sections with the compact-open topology.

One could slightly enlarge this model, taking all locally compact
metric spaces as quantifiable types, and one could slightly extend
the fragment of type theory being modelled so as to include countable
non-dependent products and even some limited second-order formulas
like (N->2)->(N->N). But instead of these modifications let me do
a more interesting one.

So here is a model of the first-order fragment, which sits
inside the metric space model just described but also enjoys some
univalence. This is a drastic simplification of what I tried to
describe in my talk in February. I must say sorry for that, because
I now strongly doubt that anything other than this modest model
of the first-order fragment will come ever out of that talk.
(Of course, one can try extend this model to higher-order types,
which probably means going out of topological - and certainly
metrizable - spaces. But I'm not convinced that such extension
is bound to add more insight to our understanding of types.)

Quantifiable types will be all compact polyhedra; a [compact]
polyhedron
(in topology) is a metric space triangulable by a [finite] simplicial
complex (or, equivalently, by a finite simplicial set) and endowed with
an atlas of mutually compatible triangulations. Substitution maps
between
quantifiable types will be PL (=pecewise linear) maps; a map between
compact polyhedra A and B is PL it can be triangulated by a morphism of
simplicial complexes (or equivalently simplicial sets) with respect to
some triangulations from the atlases of A and B. General types will
be all PL spaces, which are generalizations of non-compact polyhedra
remembering precisely which maps of polyhedra into them are PL.
I'll refer to Chapter 2 of Zeeman's notes for the details:
http://www.maths.ed.ac.uk/~aar/papers/zeemanpl.pdf
(he calls PL maps "polymaps" and PL spaces "polyspaces", but
that terminology never gained much popularity). He also defines
PL maps between PL spaces, and these will be the substitution maps
of the model; the display maps will be those PL maps that are Serre
fibrations. The space of all PL maps from a polyhedron into
a polyhedron, or into any PL space, is a PL space satisfying
the exponential law (see Zeeman). This gives dependent products
over quantifiable types.

Display maps at least between quantifyable types (and I have reasons
to believe that between all types, but this needs a proof) are now
classified by the extension of Hatcher's "Whitehead space" including
non-compact polyhedra, which will therefore be the univalent universe.
I mentioned a construction of this extended Whitehead space
at the beginning of my talk in February, and the proof that it
classifies PL Serre fibrations of possibly non-compact polyhedra goes
along the lines of Steinberger's proof of the compact case
http://projecteuclid.org/euclid.mmj/1029003286
(see also folk.uio.no/rognes/papers/plmf.pdf now published as
http://press.princeton.edu/titles/10050.html). I'm writing up
the details.

The fact that the PL model doesn't naturally include universal
quantification over nat (i.e. countable non-dependent products)
is probably the most implausible here, but I manage to see it
as a feature rather than a bug. It seems to be saying that
natural numbers and univalence, as we currently understand them,
don't really fit well together, in the paradigm that constructive
means continuous. This is parallel to the result in Martin's talk.
I don't think that we can just safely ignore this problem.

All the best,
Sergey

[Martin Escardo]

Let's phrase these questions more objectively.

We have axioms A1, A2, A2, ... for "synthetic topology".

We have axioms B1, B2, B3, ... for "synthetic homotopy type theory".

In both cases, it is claimed (Brouwer, Voevodsky, and others) that these
axioms are more than just tools for specific disciplines of mathematics,
but rather have a foundational character, but let's not discuss
philosophical or foundational issues in this message. Let's just say
that both can be built on top of a lean, largely uncontroversial (if
impoverished) common constructive base. (Bishop didn't agree with
continuity axioms, but he accepted that he could only define continuous
functions, and adopted a lean foundation which deliberately is
consistent with non-constructive mathematics. MLTT is similar in this
respect.)

We have models M1, M2, ... for (various subsets of) the axioms Ai.
(Constructively and non-constructively built.)

We have models N1, N2, ... for (various subsets of) the axioms Bi.

The axioms Ai, moreover, have a computational, or operational, rendering.

The axioms Bi are expected to have a computational rendering. (I hope
they will, both theoretically and practically.)

Question 1. Are the axioms Ai and Bi consistent when put together?

(E.g. is the axiom that functions (N->2)->N are uniformly continuous
consistent with the univalence axiom? It should be, but we don't know.)

At the moment, no model validates the axioms Ai and Bi simultaneously.

Question 2. If so, do they have a common computational rendering?

This second question is not as silly as it may sound. Supposing Ai have
a computational rendering (as they do) and Bi have computational
rendering (as it seems to be happening with recent efforts), it doesn't
follow that they together have a computational rendering. The book
"Foundations of constructive mathematics" by Beeson has specific
examples where among two different sets of axioms each set has a
computational rendering, but the sets together are even inconsistent.

With Bas and Thierry we started to discuss two approaches. Assuming you
can constructively build models for Ai and for Bi, you can iterate these
constructions. Build a model for Ai, and then with this model further
build a model for Bi. Or the other way round. Cf. Guillaume's message.
Even better, start from the lean, uncontroversial constructive
foundation to build the models (this can be done for the (core of the)
Ai axioms).

Now, as far as the reals are concerned, Steve is absolutely right. Even
in topos theory the situation is uncomfortable:

(1) The Cauchy reals need not be Cauchy complete.

(2) The Dedekind reals are, but the smallest Cauchy complete subset
containing the rationals may be a proper subset.

(3) The closed unit interval (in either case) need not have the
Heine-Borel property.

(4) But the locale of reals, whose points are the Dedekind reals, does
always satisfy the Heine-Borel property for closed intervals.

(5) The complex numbers need not be algebraicly closed. Etc.

There is no reason why in (homotopy) type theory the situation
should/could be more comfortable in this respect (this is why I invoked
the Cantor type (N->2) in my topological discussion, as it is
uncontroversial). Moreover, homotopy type theory adds an extra dimension
(no pun intended) to this uncomfortable situation.

Best,
Martin

[Sergey Melikhov]

> Martin and I are on the same wavelength here. We both feel very
> strongly that types *are* (also) topological spaces. The simplicial
> sets model is highly misleading because it completely destroys the
> topology (but keeps around the homotopy). For the same rason the
> simplicial set model is misledaing when it comes to questions of
> computation. We need a better model.

P.S. An informal clarification to my previous message, which can be
taken as a high-level summary. Martin and Andrej propose to combat
what they see as a deficiency of the simplicial set model. Until
a few days ago, I have tried to keep away from this great problem,
and instead focus on what I saw as an entirely different, and
potentially more tractable deficiency of the same simplicial set
model, namely that Kan complexes have infinitely many non-degenerate
simplices unless they are h-sets (so one can't even honestly draw any
single type on a blackboard, with the exception of some h-sets).

But I have now convinced myself that one cannot do anything about
the second "deficiency" without also addressing the first one.
Very roughly, this is how the (informal) argument goes: finite
types necessitate subdivisions in the domain (these are related
to subdivisions in Kan's Ex^\infty functor), then pullback of
fibrations causes subdivisions also in the target space (with
Gambino and Garner's result on neccessity of WFS's ensuring that
they cannot be absorbed into display maps), and finally
the strictness of exponential law and of composition of
substituion maps forces inverse limits of subdivisions, so in
effect topology on terms of the type.

Sergey

[Martin Escardo]

On 13/03/13 00:07, Michael Shulman wrote:
> ... which means that you may actually be more interested in the
> direction Urs was suggesting. (-:

Yes, Urs' message is very interesting and related.

Martin

[Martin Escardo]

A proof is included here, for a change.

On 13/03/13 06:30, Andrej Bauer wrote:
> Clearly, we have used too strong a notion of decomposability when we
> asked that R be expressible as a disjoint union of two parts. We can
> weaken this condition, for example we could say that there are two
> disjoint parts A and B such that every x in R is merely in A or in B.
> Such an object would then give us "merely LPO", so no harm is done to
> computation.

"Merely LPO" implies "purely LPO".

> Question 1: does "merely LPO"
>
> forall f : nat -> 2, merely ((forall n, f n = 0) or merely (exists n, f n = 1))
>
> hold in HoTT?

I don't think so.

Here is the argument that "merely" and "purely" agree for LPO.

Write [-] for hpropositional truncation ("merely").

Firstly, [A+B] implies A+B if A and B are inconsistent hpropositions,
because A+B is an hproposition. So you can get rid of the outer
"merely". Similarly you can get rid of the "merely" prefixing the
universal, because this is already merely a mere proposition.

The bold claim is that you can get rid of the last "merely" prefixing Sigma.

I claim that [Sigma n:N, f n = 1] implies Sigma n:N, f n = 1.

Indeed, write (without the brackets, no mistake):

A := Sigma n:N, f n = 1

A' := Sigma n':N. f n' = 1 x Pi k < n', f k = 0

Then

A -> A'

(you can find the n' by induction on n using the decidability of
equality of 2).

And, because A' is an hproposition,

[A'] -> A'.

But trivially (by projection),

A' -> A,

and, by [-] functoriality,


[A]->[A'].

Hence [A] -> A by transitivity of implication.

Best,
Martin

[Thierry Coquand]

On Mar 12, 2013, at 11:28 PM, Martin Escardo wrote:

> On 13/03/13 03:11, Steve Awodey wrote:
>>
>> On Mar 12, 2013, at 11:03 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>>
>>> If the proof that Kan simplicial sets model univalence were constructive (which I learned during my visit, from Thierry and Marc, that it can't be
>>
>> what does this mean?

What we noticed with Marc was that the following

Proposition: If E -> \Delta^1 is a Kan fibration, there is a homotopy equivalence between the two fibers E(0) and E(1)

cannot be constructively valid, even if the Kan filling operations of the fibration are given explicitly,
since it is not valid in a Kripke (presheaf) model over the poset 0 <= 1 <= 2.
(It is constructively valid however if degeneracies in E are decidable.)

This does not mean that Univalence is not effective, but I believe this implies that Kan simplicial
sets cannot form a model of type theory constructively.

Thierry

[Steve Awodey]

puting aside the leap that Martin was trying make from this, I still have a hard time understanding the claim, because I don't know what a Kripke model of simplicial sets is.
is it just simplicial presheaves over the poset 3? what are the fibrations and the homotopy equivalences there -- the pointwise ones?
are you saying there is a Kan fibration E -->> Delta^1 in that category, in which the E(0) and E(1) are not homotopy equivalent?

once we start allowing simplicial sets to vary as (pre)sheaves, we should expect some differences from the classical case of "constant" sSets.
one way to make things more stable is by using *algebraic* kan complexes, that come with specified structure -- this is similar to using (higher) groupoids,
and is like the usual way of making a classical concept into a constructive one by specifying structure that was merely required to exist classically.

I would expect that the classical notion of kan simplicial set must be strengthened in this way in order to build a model of type theory constructively.

Steve

[Thierry Coquand]

> I would expect that the classical notion of kan simplicial set must be strengthened in this way in order to build a model of type theory constructively.

This is exactly the point of this counter-example.
It shows that one needs to refine the notion of Kan simplicial set in order to hope to have an effective model
(and that this notion cannot be used as it is constructively).

Thierry

[Michael Shulman]

On Tue, Mar 12, 2013 at 7:01 PM, Andrej Bauer <andrej...@andrej.com> wrote:
> We need a better model.

After Martin's talk, I proposed to consider the oo-topos of oo-sheaves
on the same site used to define Johnstone's topological topos. Like
any Grothendieck oo-topos, this admits a model of type theory with
HITs and homotopy-a-la-tarski univalent universes (is there a better
name for those?).

In particular, I asked whether the universes in that model are all
indiscrete. I think now the answer is "yes, but in an interesting
way". A convergent sequence of types is, of course, the same as a
fibration into the universal convergent sequence N_oo, which in the
oo-topos is just an arbitrary morphism into it. We can build such a
morphism from any sequence (A_i) of types and any type B, just by
considering the coproduct (\sum_i A_i) + B and mapping it to N+1 and
thence to N_oo. So any sequence in the universe converges to any
limit --- but it might do so in more than one way. (In the
topological topos, convergence is not a mere property, but comes with
witnesses.) Even the constant sequence at the unit type converges to
the unit type in two different ways: one is the identity N_oo -> N_oo,
while the other is N+1 -> N_oo.

Also, Johnstone showed in his paper that the Dedekind real numbers
object in his topological topos is simply the classical set of reals
with its usual (sequential) topology. I believe the topological topos
satisfies countable choice, so that the usual Cauchy real numbers
object coincides with the Dedekind one, and the HIT version should
probably be squeezed between the two.

Mike

[Martin Escardo]

Very interesting. I need to look at oo-toposes.

(I was aware that not only any sequence of types converges to any
desired type, but also in many ways. On particular case is interesting.
We can make 1's converge to 1 with witness X : Noo->U so that (1) Sigma
u : Noo, X u is isomorphic to N_oo, and (2) so that it is isomorphic to
N+1. Perhaps this is the same example you are describing, but I didn't
undertand your notation. Also, this is model-independent, "in type
theory". From this you conclude that in the model (topological topos)
the universe can't be topological, because on the full subcategory of
limit spaces convergence is unique.)

Best,
Martin

[Michael Shulman]

On Wed, Mar 13, 2013 at 10:11 AM, Martin Escardo
<m.es...@cs.bham.ac.uk> wrote:
> (I was aware that not only any sequence of types converges to any desired
> type, but also in many ways. On particular case is interesting. We can make
> 1's converge to 1 with witness X : Noo->U so that (1) Sigma u : Noo, X u is
> isomorphic to N_oo, and (2) so that it is isomorphic to N+1. Perhaps this is
> the same example you are describing, but I didn't undertand your notation.

Yes, it is.

[Marc....@ii.uib.no]

Steve wrote:
>
> puting aside the leap that Martin was trying make from this, I still
> have a hard time understanding the claim, because I don't know what
> a Kripke model of simplicial sets is.
> is it just simplicial presheaves over the poset 3? what are the
> fibrations and the homotopy equivalences there -- the pointwise ones?
> are you saying there is a Kan fibration E -->> Delta^1 in that
> category, in which the E(0) and E(1) are not homotopy equivalent?
>
> once we start allowing simplicial sets to vary as (pre)sheaves, we
> should expect some differences from the classical case of "constant"
> sSets.
> one way to make things more stable is by using *algebraic* kan
> complexes, that come with specified structure -- this is similar to
> using (higher) groupoids,
> and is like the usual way of making a classical concept into a
> constructive one by specifying structure that was merely required to
> exist classically.
>
> I would expect that the classical notion of kan simplicial set must
> be strengthened in this way in order to build a model of type theory
> constructively.
>
> Steve
>

To avoid any misunderstandings we attach a note which hopefully
describes this remark with all required definitions, as a precise
mathematical result.

There is then the question of how to interpret this result. We believe
that it shows that even if one adds the structure explicitly, one does
not get a satisfactory constructive definition.
We also believe that it shows that one needs to refine constructively
the notion of Kan simplicial set (either by refining the Kan filling
condition, or by taking away the degeneracy maps).

We look forward to a discussion with people more knowledgeable than we
on presheaves and Kan fibrations, preferably with a blackboard at
hand. Maybe one of the workshops has a time slot available?

Marc and Thierry

[Vladimir Voevodsky]

The connection between decidable degeneracies and homotopy theoretic properties is partly explained by Prop. 3.40, p.22 in
http://www.math.uiuc.edu/K-theory/0863/2007_09_09_delta_post.pdf .

V.

> --
> You received this message because you are subscribed to the Google Groups "IAS Univalent Foundations" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to univalent-founda...@googlegroups.com.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at http://groups.google.com/group/univalent-foundations?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

> <countermodel.pdf>

[Steve Awodey]

On Mar 14, 2013, at 9:30 AM, Marc....@ii.uib.no wrote:

that would be good.
maybe we need a bit of time to study the note, then we can schedule a meeting?

thanks,
Steve

[Michael Shulman]

On Mar 14, 2013 6:30 AM, <Marc....@ii.uib.no> wrote:
> There is then the question of how to interpret this result. We believe that it shows that even if one adds the structure explicitly, one does not get a satisfactory constructive definition.

It looks to me as though your counterexample could not be equipped with explicit structure. For at time 0, you would have to specify a filler for w and w, which would have to be sb, and at time 1, you would have to specify a filler for w and x, which would have to be v, but at time 2 w and x are identified but sb and v are not.

[Peter LeFanu Lumsdaine]

On Mar 14, 2013 6:30 AM, <Marc....@ii.uib.no> wrote:

> There is then the question of how to interpret this result. We believe that it shows that even if one adds the structure explicitly, one does not get a satisfactory constructive definition.

It looks to me as though your counterexample could not be equipped with explicit structure. For at time 0, you would have to specify a filler for w and w, which would have to be sb, and at time 1, you would have to specify a filler for w and x, which would have to be v, but at time 2 w and x are identified but sb and v are not.

I think this can be fixed by adding, from time 0, extra loops z, z' at b,b' (“fake degeneracies”), and then adding at time 2 the equation that v = v' = z = z'.

Now, all fillers taking values in the B fiber can be taken (at any time) among {z,z',v,v'}; so these will never conflict, since these are all identified as soon as their boundaries are.  Fillers taking values in other fibers don’t conflict for the same reason.

However, the original obstruction to finding a homotopy equivalence still applies.

Thankyou Marc and Thierry — it’s very nice to have an explicit counterexample to this point!  It’s not clear to me quite what it formally implies about what would need to be altered to constructivising the simplicial model, but it certainly justifies the kind of difficulties we’d been encountering on that front.

–p.

[Michael Shulman]

Thanks Peter. I suspected that some modification like that should be possible, but didn't have time to think of one.

From a model-categorical point of view, I think what this says is that not every simplicial set is constructively *cofibrant*. More generally, not every monomorphism is a cofibration. This means it's possible that not every pullback of a trivial cofibration along a fibration remains a trivial cofibration, and hence that not every dependent product of a fibration along a fibration remains a fibration. (The problem of exponentials was mentioned previously as well, of course.)

Mike

[awo...@andrew.cmu.edu]

> Thanks Peter. I suspected that some modification like that should be
> possible, but didn't have time to think of one.
>
> From a model-categorical point of view, I think what this says is that not
> every simplicial set is constructively *cofibrant*. More generally, not
> every monomorphism is a cofibration. This means it's possible that not
> every pullback of a trivial cofibration along a fibration remains a
> trivial
> cofibration, and hence that not every dependent product of a fibration
> along a fibration remains a fibration. (The problem of exponentials was
> mentioned previously as well, of course.)

that would be very illuminating w/r to Thierry's difficulties making
exponentials of Kan complexes constructively.
but can you elaborate on how to get from the "kripke model" to the failure
of cofibrancy, please?

Steve

[Michael Shulman]

I didn't mean non-cofibrancy follows specifically from the Kripke model, only from the conclusion that the fibers can't be proven homotopy equivalent. The theorem that this can be done classically can be encapsulated using lifting properties in a model category, but depending on cofibrancy of the objects involved for the lifts to exist. Hence, if something fails constructively, it seems probably to be cofibrancy.

[Thierry Coquand]

On Mar 14, 2013, at 12:29 PM, Peter LeFanu Lumsdaine wrote:

It looks to me as though your counterexample could not be equipped with explicit structure. For at time 0, you would have to specify a filler for w and w, which would have to be sb, and at time 1, you would have to specify a filler for w and x, which would have to be v, but at time 2 w and x are identified but sb and v are not.

I think this can be fixed by adding, from time 0, extra loops z, z' at b,b' (�fake degeneracies�), and then adding at time 2 the equation that v = v' = z = z'.

Now, all fillers taking values in the B fiber can be taken (at any time) among {z,z',v,v'}; so these will never conflict, since these are all identified as soon as their boundaries are.  Fillers taking values in other fibers don�t conflict for the same reason.

 Thanks!  The intuition is indeed  that the filler may be not degenerate even when one would expect it to be (like the filler for w and w).

We attach  an updated version.

 It is really nice to have had this note analyzed, proof-checked and corrected so quickly. This is even better than type-checking!

 Marc and Thierry

[Hugo Herbelin]

Hi,

About constructively defining simplicial sets, I would propose to
define them from their subsets of non-degenerate simplices and to
complete these sets with degenerate simplices afterwards.

Let Cn be a collection of sets of n-simplices in the usual sense. By
induction, we can, by classical reasoning, split Cn into Bn + Dn where
Dn := {u∈Cn | there is v∈Bp and s:Cp→Cn a degeneracy map s.t. u=s(v)},
and Bn := Cn\Dn.

Let's conversely call constructive simplicial set any collection of
sets Bn equipped with pre-face maps δi:Bn→C(n-1) where Cn := Bn+Dn is
defined by taking Dn := {(s,u)| p<n, u∈Bp, s:[p]→[n] surjective}, and
such that di∘dj=d(j-1)∘di [j>i] where the face maps di:Cn→C(n-1) are
defined by case using the standard identities:

di(id,u) = δi(u)
di(si∘s,u) = (s,u)
di(s(i-1)∘s,u) = (s,u)
di(sj∘s,u) = (s(j-1)∘s',u') [i<j and di(s,u)=(s',u')]
di(sj∘s,u) = (sj∘s',u') [i>j+1 and d(i-1)(s,u)=(s',u')]

(above, we write (id,u) for u∈Bn seen as an element of Cn; we also
interpret each s:[p]→[n] as some sequence s(i(p))∘...∘s(i(n-1))∘id
of atomic degeneracy maps in Δ).

Constructive simplicial sets are classically equivalent to simplicial
sets defined as presheaves but degeneracy is decidable in constructive
simplicial sets.

I don't see what could be wrong in doing this.

Hugo

[Peter LeFanu Lumsdaine]

I very much like this approach, but I’m not quite convinced that the objects it’s defining should be thought of as the constructive analogue of simplicial sets.  As you say, if we go to the fully classical setting, then they are equivalent to ssets defined as presheaves.  But if we go to the intermediate setting of extensional DTT, or topos logic, then in that setting, we know that simplicial sets defined as presheaves behave well in many ways (form a topos, have their extensional logic, etc), and they’re *not* equivalent to the objects you’re defining.

So in that setting, it seems maybe more natural to keep calling the presheaf ones “simplicial sets”, and then to consider the ones you describe above as an intermediate class lying between simplicial sets that are free on their semi-simplicial core, and all simplicial sets.  (They’re rather reminiscent of how computads form a subclass lying between Batanin–Leinster ω-categories that are free on globular sets, and all Batanin–Leinster ω-categories.)

One way of looking at this class: I think it’s what you get as the *algebraically cofibrant objects*, if you run the algebraic small object argument to construct an awfs on presheaf-simplicial-sets with the usual generating cofibrations (i.e. the inclusions δΔ[n] —> Δ[n].  That is, they’re the exactly the presheaf-simplicial-sets that are constructed just by starting from 0 and iteratively gluing in (arbitrary sets of) cells along their boundaries.  Does that sound right?

–p.

[Michael Shulman]

On Fri, Mar 15, 2013 at 9:24 AM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> One way of looking at this class: I think it’s what you get as the
> *algebraically cofibrant objects*, if you run the algebraic small object
> argument to construct an awfs on presheaf-simplicial-sets with the usual
> generating cofibrations (i.e. the inclusions δΔ[n] —> Δ[n].

Nice! That fits nicely with the observation that the failure of the
fibers of a Kan fibration to be homotopy equivalent is due to
non-cofibrancy of the simplicial sets involved.

> That is, they’re the exactly the presheaf-simplicial-sets that are
> constructed just by starting from 0 and iteratively gluing in
> (arbitrary sets of) cells along their boundaries.

Actually, those are the *cofree* algebraically cofibrant objects. The
general ones are more complicated; they might all be equivalent to
these, but I'm not sure.

Mike

[Andrew Polonsky]

If the proof that Kan simplicial sets model univalence were constructive (which I learned during my visit, from Thierry and Marc, that it can't be) then you would be done in the enterprise of reconciling the "old" and "new" topological views of types.

In the "topological" space of reals, there is a path from 0 to 1.  How would it reconcile?

[Andrej Bauer]

> In the "topological" space of reals, there is a path from 0 to 1. How would
> it reconcile?

We reconcile this by observing that there are two different
conceptions of path. You are talking about a path as a continuous
mapping from the closed interval [0,1], while in HoTT an element of
the identity type is also viewed as a path. There is no such HoTT-path
from 0 to 1 in the reals.

When Martin speaks of reconciliation of the old and new topological
views, he is not saying that all notions agree. In particular, he is
not saying that the "old" and "new" notions of paths agree. Far from
it. What he says is that the old and new views may coexist. Martin
will correct me if I am wrong.

With kind regards,

Andrej

[Martin Escardo]

I mean what Andrej says. Still in the same wave length. Martin

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

[Richard Garner]

Dear Hugo,

> About constructively defining simplicial sets, I would propose to
> define them from their subsets of non-degenerate simplices and to
> complete these sets with degenerate simplices afterwards.

Thanks for bringing this suggestion up! I now recall that I thought a little bit about this a while ago. As Peter L points out, these objects are the ``algebraically cofibrant'' simplicial sets. One way of characterising them is as follows: there's an adjunction between simplicial sets and semisimplicial sets, given by restriction and left Kan extension along the inclusion J : Delta_{inj} --> Delta. This adjunction induces a comonad on the category of simplicial sets; the coalgebras of this comonad are the objects you describe. Assuming classical logic, every object of the category of simplicial sets admits a unique coalgebra structure; though not every morphism admits a structure of coalgebra morphism---such morphisms are the simplicial maps which send non-degenerate simplices to non-degenerate simplices.

The interesting part is that the category of algebraically cofibrant objects ought to be a presheaf category [D^op, Set], where D is a direct category, one admitting an identity-reflecting functor to the ordinal omega. Thus for each n, it should be possible to write down in pure dependent type theory what it means to be a (fibrant) presheaf over the n-truncation of D.

The way one constructs D is as follows. There is an object 0, representing the type of 0-simplices, and an object 1, the type of non-degenerate 1-simplices. Now there are 8 different objects {2_U | U a subset of {01, 02, 12} } where 2_U is the type of non-degenerate 2-simplices for which the faces from U are degenerate. 

So, for example, we have 2_{}, the type of non-degenerate 2-simplices with all faces non-degenerate; and this has three projections to 1, picking out the three faces. On the other hand, we have 2_{01, 02, 12}, the type of non-degenerate 2-simplices with all faces degenerate; and this has no projections to 1, and only a single projection to 0, picking out the object on which the 1-dimensional faces are degenerate.

Continuing, there are rather a large number of objects representing the types of non-degenerate 3-simplices: each of the four two-dimensional faces of such a simplex can either be a non-degenerate 2-simplex of any one of the eight types listed above; or a singly degenerated non-degenerate 1-simplex (with two possible ways of forming the degeneracy); or a doubly degenerated 0-simplex. There are thus 11 different choices for the nature of each of the four two-dimensional faces, making 11^4 possible choices; in fact, not all of these choices are consistent, since there must be some compatibilities between the choices for the different faces (e.g. if the face {012} has the edge {12} degenerate, then the face {123} must also have the face {12} degenerate). Now we get an object 3_V in D for every consistent set of choices V \in 11^4, with appropriate projections to the lower-dimensional face data.

That is the basic idea of how we form D: but how should we make that precise? I haven't really checked anything but I think the following works.

Let T be the category whose objects are epimorphisms in Delta, and where a morphism from (s:n-->m) to (t:k-->l) is a monomorphism f: n --> k in Delta such that, for any x, y in {0, ..., n}, tf(x) = tf(y) implies s(x) = s(y); which says that ``s quotients n more than t quotients the image of n in k''. There is an obvious forgetful functor T --> Delta_{inj} given by taking domains, which has a section  i: Delta_{inj} --> T sending n to (1_n: n-->n) and sending f to f. Next, for every n in Delta, we can consider the poset E_n of all proper subobjects of n; it is isomorphic to the poset of proper subsets of {0,...,n}. There is an obvious functor E_n -> Delta / n.

We may now define the category D as follows. An object of D is some n in Delta, together with a factorisation of the functor E_n --> Delta / n through the forgetful T / i(n) --> Delta / n. A morphism (n, E_n --> T / i(n)) --> (m, E_m --> T / i(m)) is an injection f: n --> m in Delta such that the composite E_n --> E_m --> T / i(m) factors through T / i(f) : T / i(n) --> T / i(m).

D has a faithful forgetful functor to Delta_{inj}, and so is a direct category, since Delta_{inj} is. And now the claim is that [D^op, Set] is precisely the category of algebraically cofibrant simplicial sets.

I don't think any of this really depends on the fact we are working with simplicial sets; it seems like we could replace Delta by any other Reedy category which ``satisfies the Eilenberg-Zilber lemma'' (the definition of morphisms in T is the only part that looks like it may not generalise; but this definition can be restated in terms of the factorisation system on Delta induced by the Reedy structure).

Richard

On 15 March 2013 09:32, Hugo Herbelin <Hugo.H...@inria.fr> wrote:

Hi,

[Bas Spitters]

Dear Richard, Hugo,

These are related to the decidable Kan complexes that Thierry has been studying.
I believe the suggestion to look at them may have been due to Vladimir.
Since the degeneracies are freely added, I one may be able to work
with semi-simplicial Kan complexes instead.
This is in fact what Thierry is currently doing.

The explanation you give is very clear. Part of that story can be found here:
http://mathoverflow.net/questions/57653/degeneracies-for-semi-simplicial-kan-complexes
This one also seems related:
http://mathoverflow.net/questions/75094/semi-simplicial-versus-simplicial-sets-and-simplicial-categories

> I don't think any of this really depends on the fact we are working with
> simplicial sets; it seems like we could replace Delta by any other Reedy
> category which ``satisfies the Eilenberg-Zilber lemma'' (the definition of
> morphisms in T is the only part that looks like it may not generalise; but
> this definition can be restated in terms of the factorisation system on
> Delta induced by the Reedy structure).

As you probably know, such categories are studied here (sec 4).
http://arxiv.org/pdf/1110.1066

This is the paper where the notion of elegant Reedy category was introduced.
Mike Shulman has shown that presheaves over such categories satisfy univalence.

Best,

Bas

[Hugo Herbelin]

Thanks very much for all these comments. I now understand that this
construction has been around for a while.

Excuse my ignorance, then, but if I understand your messages
correctly, [D^op, Set] and [Δ^op, Set] coincide classically. Is that
right?

Then, why [D^op, Set] couldn't be the "correct" constructive notion of
simplicial sets, with the exponential of constructive simplicial sets
being the one of [D^op, Set]?

Hugo

[Michael Shulman]

On Tue, Mar 19, 2013 at 9:17 AM, Hugo Herbelin <hugo.h...@inria.fr> wrote:
> Excuse my ignorance, then, but if I understand your messages
> correctly, [D^op, Set] and [Δ^op, Set] coincide classically. Is that
> right?

No, Richard said that

> Assuming classical logic, every object of the category of simplicial sets admits a unique coalgebra structure; though not every morphism admits a structure of coalgebra morphism---such morphisms are the simplicial maps which send non-degenerate simplices to non-degenerate simplices.

So assuming his argument is correct that [D^op, Set] is equivalent to
the category of algebraically cofibrant simplicial sets, then it would
not be equivalent to [Δ^op, Set], but rather to the non-full
subcategory thereof determined by all the objects but only the
morphisms which preserve nondegeneracy.

(In general, two presheaf categories [A^op,Set] and [B^op,Set] are
equivalent if and only if A and B have equivalent Karoubi
completions.)

Mike

[Peter LeFanu Lumsdaine]

On Tue, Mar 19, 2013 at 9:17 AM, Hugo Herbelin <hugo.h...@inria.fr> wrote:

Thanks very much for all these comments. I now understand that this
construction has been around for a while.

(Parenthetically: I didn’t mean to suggest that this construction isn’t new, and I don’t think anyone else did either — category theory is doing its job, and providing a known general construction that this is an instance of, but this instance itself is still novel.)

–p.

[Benno van den Berg]

Dear all,

Let me try to revive this discussion by making a suggestion which is exactly dual to the one which was made by Hugo and Richard. The thing is that the forgetful functor i^*: SSets -> SSSets from simplicial sets to semisimplicial sets also has a right adjoint, which, as Peter and Thierry pointed out to me, is like doing logical relations or PERs. So where the left adjoint i_! takes the point of view that simplices without degeneracies are quite nice and we can always add these degeneracies later, the right adjoint i_* takes the point of view that these simplices do not really exist (like with symmetric and transitive relations: only the elements that are related to themselves truly exist).

Another reason why this looks good to me is that, unless I am very much mistaken, we can use the adjunction (i^*, i_*) to do transfer of model structures

http://ncatlab.org/nlab/show/transferred+model+structure

to lift the model structure from simplicial sets to one on semisimplicial sets. So the resulting model structure on SSSets would be one in which the fibrations have the RLP with respect to the *simplicial* Horn inclusions, the weak equivalence are those f for which i_* f is a weak equivalence, the generating cofibrations are the *simplicial* boundary maps and the cofibrant objects are the simplicial sets. At first this looked wrong or odd to me but now I think this is exactly right: at least it fits with the philosophy "only those elements which have all degeneracies truly exist". But the what is really good is that the existence of degeneracies is now a property of the nice objects: it is not part of the structure which needs to be carefully preserved at every step.

Originally, I was looking for a model structure on semisimplicial sets in a very semisimplicial spirit (with semisimplicial horns and boundary maps, for example) but that now looks hopeless to me. Mike and Peter had some pretty good obstructions and I attach one of my own which I find especially dispiriting.

Best,

Benno

2013/3/17 Richard Garner <richard...@mq.edu.au>