Regarding the Universal Constant Map

[Gershom B]

In the work on “The Geometry of Constancy” [1] Escardo and Coquand
construct a HIT they call the “Universal Constant Map” with the
following constructors.

B: X -> S(X)
l: (x : X) -> (y : X) -> B x = B y

Compare this to a HIT for -1 truncation:

|| : X -> |X|
t : (x : |X|) -> (y : |X|) -> x = y

These feel very similar, though of course they act quite differently.

In particular, here are some things that I understand to be true:

Maps out of S(X) are equivalent to weakly constant functions out of X,
i.e. functions f : X -> A such that (a1 : A) -> (a2 : A) -> f(a1) =
f(a2).

Meanwhile, maps out of |X| are equivalent to weakly constant functions
out of X under the condition that they are maps into a 0-type, and in
general are equivalent to coherently constant functions out of X. [2]

for any inhabited X, S(X) is 0-connected, but not contractible (i.e.
its set truncation is contractible but it has at least one nontrivial
loop -- i.e. it is at least a 1-type)
for any inhabited X, |X| is 0-connected and also contractible (i.e.
its loop space is contractible and hence it has no nontrivial loop --
i.e. it is at most a -1-type)

We can give a map |X| -> S(X) iff all weakly constant functions X -> A
factor through |X|.
We can give a map S(X) -> |X| always.

Here are a few more observations:

S is not idempotent.

Just as S(1) is literally S1, it seems that S(S1) should be the torus
(I worked a sketch of this out with Thomas Lawler and Dan Bornside).

More easily, S(2) is a point with three loops, S(3) is a point with
seven loops, and for any finite set N, it seems S(N) should be a point
with N^2-1 loops.

Call S UCM_-1. We should be able to give a UCM_0 exhibiting
1-coherence — i.e. the property given by Kraus as coh that
Pi_(a1,a2,a3) mc(a1,a2) . mc(a2,a3) = mc(a1,a3) where mc is the
modulus of constancy, i.e. the second projection of the sigma type
isWeaklyConstant(f).

For inhabited X, UCM_0(X) should have the property that it is
1-connected but has at least one nontrivial 2-loop; i.e. it is at
least a 2-type. UCM_0(1) is S2.

Question: what is UCM_0(S1)? UCM_0(S2)?

So here are some further questions, with varying levels of speculation.

1) Under the condition maps both ways (|X| -> S(X) and S(X) -> |X|)
exist, what can we say about their relationship? What is the induced
function S(X) -> S(X) factoring through |X|?

Repeat this question, but now with UCM_0 in place of S. Now repeat
this question about maps UCM_0(X) -> UCM_-1(X) and vice versa.

2) Is there an alternative way to define UCM_n, more similar to how |
|_n is defined in chapter 7 of the book? I.e. we give | |_n in terms
of point and path constructors indexed on the n+1 sphere. Can we give
UCM_n in terms of path constructors similarly indexed on some type?
Perhaps on the n-truncation of X? (Speculation: perhaps,
unfortunately, the correct way to do this is semi-simplical types)

2b) (extremely speculative) Can we think of UCM_n as a "connection"
operator in the sense of the "truncation" operator ||_n? I.e. as
giving for any type X, and related type UCM_n(x) that is n-connected?
If not (likely), is it "half" of one? I.e. call such a "connection"
operator C_n. Could we then factor all functions X -> C_n(X) through
UCM_n(X)?

2c) (largely unrelated) Assume we had C_n (We should be able to get
this through the construction of the Whitehead tower?). Then: is there
an equivalent to 7.6 that holds for data rather than functions -- i.e.
all types X factor into (|X|_n, C(X)_n) for any n?

3) Conjecture: UCM_oo (if it could be defined to exist) should be
equivalent to |X|.

4) What is the equivalent to UCM_-1 for the case when we wish to
examine 0-truncation? Call it SS. It should be given by something like
the following?

B : X -> SS(X)
l: (a : X) -> (p : a = a) -> (q : a = a) -> apB p = apB q

Observation SS(1), like UCM_0(1), should yield S2.

What things can we say about SS in general? Does this approach suggest
a way to build SS_1?

In any case, if these are not the precise questions to ask, are there
other interesting things that can be done and said regarding the
properties of the UCM and its generalizations, and I suppose the
analogies and lack thereof to truncation?

Cheers,
Gershom

(thanks to Nicolai Kraus for some preliminary comments on this that
clarified some obvious mistakes, and solidified some questions into
observations -- in particular regarding the existence and properties
of UCM_0).

[1]: Precis: http://www.cs.bham.ac.uk/~mhe/papers/geometryOfConstancy.pdf
and Slides: http://www.cs.bham.ac.uk/~mhe/papers/geometryOfConstancyHoTTUF2015.pdf

[2]: “The General Universal Property of the Propositional Truncation,”
Kraus — http://arxiv.org/abs/1411.2682

[Gershom B]

On Thu, Jul 16, 2015 at 6:52 PM, Gershom B <gers...@gmail.com> wrote:

>
> More easily, S(2) is a point with three loops, S(3) is a point with
> seven loops, and for any finite set N, it seems S(N) should be a point
> with N^2-1 loops.

Dan Bornside just emailed me and let me know he thinks we got the
formula wrong. Rather, he suspects S(N) should have loops given by
n*(n^2+5)/6, as the sum of the 0,1,2 simplicies of the n-1 simplex.
(i.e. https://oeis.org/A004006).

--Gershom

[Nicolai Kraus]

This is a very nice collection of observations. I have also thought
about some of these points before, and some others are new to me. I'd
like to make some comments:

On 16/07/15 23:52, Gershom B wrote:
> Just as S(1) is literally S1, it seems that S(S1) should be the torus
> (I worked a sketch of this out with Thomas Lawler and Dan Bornside).

Ah, this is nice. I would have expected S(S1) to be something more
complicated, but admittedly, I have not really spent much time on the
question. Is there an easy argument?

> More easily, S(2) is a point with three loops, S(3) is a point with
> seven loops, and for any finite set N, it seems S(N) should be a point
> with N^2-1 loops.

Oh, but 3^2-1 is not 7 ;-)
I think it's N^2 - N + 1, because you can use (N-1) of the N^2 paths to
'contract' the N points into a single one (N-1 paths can be chosen so
that they form a spanning tree); then, the other N^2 - N + 1 are loops.

> Call S UCM_-1. We should be able to give a UCM_0 exhibiting
> 1-coherence — i.e. the property given by Kraus as coh that
> Pi_(a1,a2,a3) mc(a1,a2) . mc(a2,a3) = mc(a1,a3) where mc is the
> modulus of constancy, i.e. the second projection of the sigma type
> isWeaklyConstant(f).
>
> For inhabited X, UCM_0(X) should have the property that it is
> 1-connected but has at least one nontrivial 2-loop; i.e. it is at
> least a 2-type. UCM_0(1) is S2.
>
> Question: what is UCM_0(S1)? UCM_0(S2)?

Hmm, do I understand it correctly if I assume that UCM_n is a HIT with
(n+1) constructors? If so, then || UCM_n(X) ||_{n+1} is equivalent to ||
X ||_{-1} (this is essentially the "finite case" of my talk).
I have not thought about the question what those UCM_n(X) are for some
concrete choice of X. I just want to add that this is very related to
something that we have discussed in Warsaw in the "round table/open
problems" session: Thorsten and I have proposed the open problem to show
that any HIT is equivalent to one where the path-constructors (i.e. all
constructors that do not construct points) are non-recursive (i.e. its
arguments have no quantification over the HIT that is currently
defined); this might be the case, but it might also be the case that
this statement needs to be weakened. I said we had an idea how to
formulate truncation operators without recursion (Truncation operators
seem to be a canonical choice of HITs with path-constructors that do use
recursion). I have then learnt that Floris van Doorn has already
implemented propositional truncation as non-recursive HIT in the new
proof assistant LEAN, his idea is to use
... UCM_-1 ( UCM_-1 ( UCM_-1 (X) ) ) ...
as ||X||_{-1}; I would expect that the higher truncations can be done in
a similar way (but it would probably be more tedious). The idea here is
to iterate UCM_-1 omega times.
This is not the same idea as the one of Thorsten and me, because we want
to use
... UCM'_2 (UCM'_1 (UCM'_0 (UCM'_{-1} (X)))) ...,
where UCM'_n(X) is a HIT with only two constructors with the property
that || UCM_n(X) ||_{n+1} is equivalent to || X ||_n; consequently, the
idea is to "move" the nontrivial stuff one level higher in every step.
This is basically an application of arXiv:1507.01150, while Floris'
formalization is on GitHub [*].
As far as I know, Egbert has also done something related (there has been
a discussion some days ago on this list).

Best regards,
Nicolai

[*]
https://github.com/fpvandoorn/leansnippets/blob/master/propositional_truncation.hlean

[Michael Shulman]

On Thu, Jul 16, 2015 at 8:50 PM, Nicolai Kraus <nicola...@gmail.com> wrote:
> (Truncation operators seem to be a canonical
> choice of HITs with path-constructors that do use recursion).

Another, more general, choice would be localizations. (The
n-truncation is the localization at the map S^{n+1} -> 1.)

> I have then
> learnt that Floris van Doorn has already implemented propositional
> truncation as non-recursive HIT in the new proof assistant LEAN, his idea is
> to use
> ... UCM_-1 ( UCM_-1 ( UCM_-1 (X) ) ) ...
> as ||X||_{-1}

This is really nice! I hope there will be a blog post or paper about it soon.

Mike

[Martin Escardo]

Yes, this is really nice and I am looking forward to seeing a blog post
and paper by Floris.

Another remark is that not only ||X|| is the colimit of the diagram

X->S(X)->S(S(X))->...

as Nicolai says above and Floris has shown, but also this gives a notion
of coherently constant map, namely a cocone for this diagram, as
emphasized by Nicolas Tabareau during the HoTT/UF workshop, such that a
a map X->A factors through ||X|| if and only if it is coherently constant.

Also, as emphasized by some people in various discussions during and
after the workshop, this is an example where infinitely many coherences
can be given in HoTT.

Martin

[Andrej Bauer]

On Fri, Jul 17, 2015 at 12:52 AM, Gershom B <gers...@gmail.com> wrote:
> More easily, S(2) is a point with three loops, S(3) is a point with
> seven loops, and for any finite set N, it seems S(N) should be a point
> with N^2-1 loops.

In what sense are you counting anything here?

When you say that S(2) is a point with "three loops", are you actually
counting the generators of the loop spaces? If there is a loop l,
don't you get l^n for every n? Or are you saying that there's an
equation l^3 = id?

A more subtle question is whether you're counting the loops internally
or externally. If internally, then you need to prove a statement such
as "the loop space is equivalent to unit + unit + unit". If it's
exernal, then what are you counting? If this were category theory you
could say "global points" or some such, but it's not.

With kind regards,

Andrej

[Peter LeFanu Lumsdaine]

I would read it as “…equivalent to the type generated by a point with k loops,” i.e. a statement about generators of the loop space; so as such, certainly an internal statement.  And I’d agree with Mike’s correction of the formula as n^2 – n + 1.

Very nice collection of observations, in any case!  And extremely nice also to see Floris’ non-recursive construction of the propositional truncation here.

–p.

[Floris van Doorn]

Thanks Nicolai for pointing toward my construction of the propositional truncation. I'll write a blog post and probably also a paper about it soon (I'm now on holiday, but I'll write it immediately after I return).

Best,

Floris

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Gershom B]

On July 17, 2015 at 5:40:38 AM, Peter LeFanu Lumsdaine (p.l.lu...@gmail.com) wrote:
>
> I would read it as “…equivalent to the type generated by a point with k
> loops,” i.e. a statement about generators of the loop space; so as such,
> certainly an internal statement. And I’d agree with Mike’s correction of
> the formula as n^2 – n + 1.

Yes, that was the intended sense. And Nicolai’s correction of the formula is indeed likely the correct one (Dan again just emailed me this morning suggesting the same thing). 

On July 16, 2015 at 11:50:57 PM, Nicolai Kraus (nicola...@gmail.com) wrote:
> On 16/07/15 23:52, Gershom B wrote:

> > Just as S(1) is literally S1, it seems that S(S1) should be the torus
> > (I worked a sketch of this out with Thomas Lawler and Dan Bornside).
> 

> Ah, this is nice. I would have expected S(S1) to be something more
> complicated, but admittedly, I have not really spent much time on the
> question. Is there an easy argument?

I suppose “until it is in Coq it ain’t true” but the sketch of the idea is that one takes S of the interval rather than 1 directly. Thus, rather than S1 directly, we get instead a cylinder (which is, of course, homotopic). We then lift through S the “gluing” of the two ends of the interval to produce S1, and observe that this should correspond to the joining of the two open ends of the cylinder to form a torus.

My other half-intuition here is that the base and generating path constructor of S at base correspond to equipping S(base) with one further non-trivial loop. However, we must now add “the rest of the loops” generated by l. These are obtained by sweeping out the new non-trivial loop along the loop generated by "apB loop”, yielding a torus. (and of course when one collapses the homotopical loops back down we arrive at just the product of two copies of S1).

There something of a purely type-theoretic moral justification as well, given by the universal property. Something along the lines of: “weakly constant functions out of S1 are equivalent to functions out of S(S1), and we know all functions out of S1 must give the coherence condition of S1, and we know the coherence condition of S1 does not provide enough data for weak constancy, so they must provide a second coherence condition, and this amounts to providing another generating loop.”

Cheers,
Gershom

[Michael Shulman]

On Fri, Jul 17, 2015 at 6:38 AM, Gershom B <gers...@gmail.com> wrote:
>> > Just as S(1) is literally S1, it seems that S(S1) should be the torus
>> > (I worked a sketch of this out with Thomas Lawler and Dan Bornside).

Hmm... I don't see it.

S(X) is the homotopy coequalizer of the two product projections X × X
⇉ X. In classical homotopy theory, the homotopy coequalizer of two
maps A ⇉ B can be computed as the homotopy pushout of A ← A+A → B,
which in turn is the ordinary pushout of A×I ← A+A → B. In other
words, we take a cylinder on A and glue its two ends to B according to
the two maps A → B.

Now, if we were taking the homotopy coequalizer of two copies of the
*identity* map S^1 → S^1, then this would be gluing together the two
ends of a cylinder, yielding a torus. But the homotopy coequalizer of
the product projections S^1 × S^1 ⇉ S^1 seems more complicated: we
take a thickened torus, squish one of its boundaries along its
equators and the other along its meridians, and then glue them
together.

Mike

[Martin Escardo]

While we are at it, can anybody "picture" the space S(s=base) for an
arbitrary s:S^1? (This space occurs in our slides mentioned by Gershom.)

As soon as we get hold of a point p:s=base of the path space, we know
that (s=base)=Z.

So the first question is what is S(Z).

But, more generally, can we describe S(s=base) using torsor machinery in
the way Dan Grayson did for S(1), so that we can more or less
"visualize" S(s=base).

Martin

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

[Martin Escardo]

On 17/07/15 21:30, Martin Escardo wrote:
> While we are at it, can anybody "picture" the space S(s=base) for an
> arbitrary s:S^1? (This space occurs in our slides mentioned by Gershom.)
>
> As soon as we get hold of a point p:s=base of the path space, we know
> that (s=base)=Z.
>
> So the first question is what is S(Z).
>
> But, more generally, can we describe S(s=base) using torsor machinery in
> the way Dan Grayson did for S(1), so that we can more or less
> "visualize" S(s=base).

One reason I want to "visualize" this space is that although we can't
know a point of s=base naturally in s, we can always know a point of
S(s=base) naturally in s. What is this point?

For comparison, consider the same question for ||s=base|| replacing
S(s=base). The answer is tautological for the torsor description of S^1.

Is there a construction of S(s=base), analogous to the construction of
S^1 with torsors, that allows us to see directly a point of S(s=base)?

Martin

[Gershom B]

On Fri, Jul 17, 2015 at 4:30 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> While we are at it, can anybody "picture" the space S(s=base) for an
> arbitrary s:S^1? (This space occurs in our slides mentioned by Gershom.)
>

> So the first question is what is S(Z).

By a couple of arguments I suspect this is a point equipped with
w-many generating paths?

For one, by the combinatorial argument with the (now corrected)
formula for any N we get a point with N^2-N+1 generating paths, so we
may be able to just observe that goes to infinity, and that it appears
there is no reason for the structure there to collapse.

For another, take Mike's very helpful observation that we can
construct S(X) as a pushout of

X^2 × I ← X^2+X^2 → X^2

Now substitute Z for X, and I think that using the fact that Z^2 = Z
and Z + Z = Z, we can simplify and get a pushout of

Z × I ← Z → Z

and it seems we can proceed from there?

> As soon as we get hold of a point p:s=base of the path space, we know
> that (s=base)=Z.

This is where I have a very basic question. Do we need to get hold of
such a point to know that (s=base) = Z or can we know it in some
"generic" sense? The latter would help account for how the
construction in your slides goes through...

--Gershom

p.s. After Mike's post I am now again properly confused as to exactly
what S(S1) is. The interesting thing is that the case of 1 and the
case of Z seem special in the same way -- that the triviality of the
product and coproduct help simplify things. However, working through
the coequalizer construction I have thus far been unable to convince
myself that it is at least not potentially the torus :-)

[Martin Escardo]

On 17/07/15 23:01, Gershom B wrote:
> On Fri, Jul 17, 2015 at 4:30 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> While we are at it, can anybody "picture" the space S(s=base) for an
>> arbitrary s:S^1? (This space occurs in our slides mentioned by Gershom.)
>>
>> So the first question is what is S(Z).
>

> By a couple of arguments I suspect [...]

I will think about your suspicions.

> This is where I have a very basic question. Do we need to get hold of
> such a point to know that (s=base) = Z or can we know it in some
> "generic" sense?

What this means is that s=base -> (s=base)=Z.

The particular equality obtained in the conclusion depends on the
particular equality given in the hypothesis. It is here that I think
the view of S^1 as a type of torsors helps. Think about this: the type
s=base should always be the integers, thought of as a discrete line of
points, except that we don't know which point is taken to be the
origin. As soon as we know any point of this line, we can take it to
be the origin. This is, roughly, in outline, what the torsor
description of S^1 amounts to.

For background, see Baez tutorial:
http://math.ucr.edu/home/baez/torsors.html

For the construction, see Grayson's message:
https://groups.google.com/d/msg/homotopytypetheory/hE1eY-v_Kes/ofpOKOld9a4J

Martin

[Peter LeFanu Lumsdaine]

Here is a way to visualise S(S(1)).  Stand with your feet directly in front of each other (as in Warrior Pose, if you do yoga), and your arms out horizontally sideways.  Now your hands and feet form the vertices of a tetrahedron, with a “top edge” (you arms), “bottom edge” (line of your feet), “front face” (hands to front foot), “back face” (hands to rear foot), “left face” (left hand to both feet), and “right face” (similarly).

Start with this tetrahedron (as a solid, i.e. including its interior).  Now (a) identify the left and right face with each other (in the most obvious way); (b) identify the front and back face with each other (similarly); and (c) identify the top edge (left hand to right hand) with the bottom edge (rear foot to front foot).

The resulting object is S(S(1)).

Less anatomically: as per Mike’s post, S(X) can be seen as a quotient of X x X x I, identifying (x,t,0) with (t,y,1), for any t,x,y.

Applied to X = S(1) = S^1, and considering S1 itself as I with the endpoints identified, this tells us that S(S(1)) is a quotient of the cube I x I x I, where we quotient by the relations

(a) (0,y,z) ~ (1,y,z)

(b) (x,0,z) ~ (x,1,z)

(c) (x,t,0) ~ (t,y,1)

(for all x,y,z,t as appropriate).

Orient the z-axis vertically upwards, the x-axis left-to-right, the y-axis forwards.  Consider (c) first; and see it as occurring in three steps.  First, identify (x,t,0) with (x',t,0) for all x,x'.  (NOT adding paths now, but literally quotienting.)  This squeezes the bottom face of the cube to a single front-to-back line.  Secondly, identify (t,y,1) with (t,y',1), for each y,y'; this squeezes the top face to a left-to-right line.  So we’ve now collapsed the cube to the tetrahedron you made with your hands and feet.  The relations (a), (b), and the remaining part of (c) now say: the front and back faces are identified; the left and right faces are identified; and the top and bottom edges are identified.

The representation as a tetrahedron with faces/edges identified can be seen as finite presentation of a simplicial set (just 6 non-degenerate simplices), allowing a rough-and-ready calculation of homology.  If I’ve done this right, it comes out giving H^3(S(S(1)) = Z, whereas H^3(T^2) = 0.  So I don’t think it’s equivalent to the torus; but it’s a reasonably tractable object!

–p.

p.s. apologies for mixing up Nicolai and Mike in my previous message

[Martin Escardo]

Nice! Can you perform the same gymnastics and mathematics to explain
S(s=base) and what its mysterious canonical point is?

Martin

> <mailto:HomotopyTypeTheory%2Bunsu...@googlegroups.com>.

> For more options, visit https://groups.google.com/d/optout.
>
>

[Peter LeFanu Lumsdaine]

On Sat, Jul 18, 2015 at 1:39 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

Nice! Can you perform the same gymnastics and mathematics to explain
S(s=base) and what its mysterious canonical point is?

Actually, yes, I think!  No yoga this time though (unless possibly with millipedes?)

First: recall that (s=base), as s varies, looks like the (vertical-axis) helix fibred over the (horizontal) circle, with each fibre a copy of Z, but rising by 1 as one transports around the circle.

Now think of a single copy of Z for a moment.  When we embed it into S(Z), we add lots of paths, but among them, we add a path from n to suc(n), for each n; so inside S(Z), there’s a line, which includes Z.

Now, when we look at S(s=base), varying over s, we are doing that in each fiber of the helix.  So in particular, those lines show that the helix now lives inside a *cylinder* (still vertical-axis) living inside S(s=base).  And the cylinder has an obvious section.  This section, I think, becomes the “canonical point” of S(s=base).

Does that seem to match up right?

–p.

[Martin Escardo]

On 18/07/15 09:03, Peter LeFanu Lumsdaine wrote:
> On Sat, Jul 18, 2015 at 1:39 AM, Martin Escardo <m.es...@cs.bham.ac.uk
> <mailto:m.es...@cs.bham.ac.uk>> wrote:
>
> Nice! Can you perform the same gymnastics and mathematics to explain
> S(s=base) and what its mysterious canonical point is?
>
>
> Actually, yes, I think! No yoga this time though (unless possibly with
> millipedes?)
>
> First: recall that (s=base), as s varies, looks like the (vertical-axis)
> helix fibred over the (horizontal) circle, with each fibre a copy of Z,
> but rising by 1 as one transports around the circle.
>
> Now think of a single copy of Z for a moment. When we embed it into
> S(Z), we add lots of paths, but among them, we add a path from n to
> suc(n), for each n; so inside S(Z), there’s a line, which includes Z.
>
> Now, when we look at S(s=base), varying over s, we are doing that in
> each fiber of the helix. So in particular, those lines show that the
> helix now lives inside a *cylinder* (still vertical-axis) living inside
> S(s=base). And the cylinder has an obvious section. This section, I
> think, becomes the “canonical point” of S(s=base).

Interesting sight of S(s=base).

I would be nice to have a more explicit description of S(s=base), in
HoTT, like the explicit description of S^1 with torsors, as an
alternative to the HIT description, to try to see whether this matches
up right. The description as a HIT of course is useful, as any
description of anything by a universal property, but not necessarily for
"visualization" purposes.

Thanks for offering this visualization.

Martin

> <mailto:m.es...@cs.bham.ac.uk <mailto:m.es...@cs.bham.ac.uk>>>

> > <mailto:HomotopyTypeTheory%2Bunsu...@googlegroups.com
> <mailto:HomotopyTypeTheory%252Buns...@googlegroups.com>>.

> > For more options, visit https://groups.google.com/d/optout.
> >
> >
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe
>
>