circle

[Vladimir Voevodsky]

Another thought which is a result of looking into the philosophical side of UF.

We say that S^1 (e.g. K(Z,1) as Grayson defined it or as a HIT) is a circle.

This is a little misleading. In fact, S^1 is the *pointed* circle.

The real ideal circle should be "the same everywhere" in particular it should not have a distinguished point.

This suggests that such a circle C as a type should probably contain no objects but if we add its object to the context then it should be possible to establish its equivalence with S^1.

(It also should be consistent to assume that it has an object).

V.

PS I have a vague feeling that this might be connected with something like continuous or differentiable homotopy type theory.

[Martin Escardo]

Can we show that if we replace the base point of the HoTT-book circle by
any (hypothetical) point and a suitable loop, then the universal
property of the pointed circle is still satisfied? This would mean that
the HoTT-book S^1 is the same everywhere. M.

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

[Vladimir Voevodsky]

May be one can say as follows:

Consider the hypothetical model of type theory in the infty-topos of homotopy types over BU(1). There is a canonical circle bundle over BU(1). This is the C I am talking about.

V.

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

[Michael Shulman]

"This" C cannot be uniquely characterized inside of type theory,
however, so we cannot give it a definite article.

[Peter LeFanu Lumsdaine]

Interesting question!  Besides what Vladimir suggests, I’d think that an “abstract circle” should be merely inhabited (either as one of its axioms, or a consequence of them).  Two equivalent suggestions for axiomatising them:

Definition AbstractCircle := { X : Type & merely (X <~> S1) }.

where S1 is the usual (pointed, oriented) circle HIT, and "merely" is (–1)-truncation; or, to avoid assuming that S1 exists,

Definition AbstractCircle := { X : Type & merely ( [all the data (base,loop,elim,comp x2) of the usual S1 ] ) }.

With either of these, the type of abstract circles should be connected but not contractible (assuming univalence): it will be the connected component of S1 in the universe, i.e. BAut(S1), so (classically) B(U(1) x C_2), if I’m not mistaken.  (C_2 appears since the automorphisms can be orientation-reversing).

Here’s a puzzle: suppose we’re given an abstract circle, by the second definition above.   Can we construct a circle, in the usual HIT sense?  We need to assume (–1)-truncation exists for the definition, but don’t assume Univalence (since that would let us use Dan G’s construction of the circle) or any other HIT’s.

Second puzzle: can we define AbstractCircle without assuming propositional truncation?

–p.

[Michael Shulman]

On Wed, May 14, 2014 at 11:00 AM, Martin Escardo
<m.es...@cs.bham.ac.uk> wrote:
> Can we show that if we replace the base point of the HoTT-book circle by any
> (hypothetical) point and a suitable loop, then the universal property of the
> pointed circle is still satisfied?

Yes, I think we can.

Suppose given x:S1. First we need to construct a "suitable" loop. If
we had p:x=base, then we could of course use p.loop.!p. We don't
necessarily have such a p for an arbitrary x, but we do have
||x=base|| since S1 is connected. Thus, by unique choice, it suffices
to uniquely characterize "p.loop.!p" in a way independent of p. This
is possible: it's the unique q:x=x such that for any p:x=base we have
q.p = p.loop. This fact, and the uniqueness, follow from
commutativity of the loop space of S1 (i.e. Z).

Write loop_x for the path x=x defined above; now the question is
whether (S1,x,loop_x) has the same universal property as
(S1,base,loop). If we had p:x=base, then this would be true, since we
could transport the universal property of the latter along p (and
loop_x = p_*(loop)). But, again, we have ||x=base||, and the
universal property can be expressed as a mere proposition (e.g. that
the map (S1->Y) -> Sum(y:Y)(y=y), defined by evaluating at x and
loop_x, is an equivalence), so truncation-elim suffices.

Mike

[Michael Shulman]

On Wed, May 14, 2014 at 1:57 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> but don’t assume
> Univalence (since that would let us use Dan G’s construction of the circle)

Can that construction of the circle by univalence be shown to have the
universal property of the HIT S^1, without assuming that the latter
exists?

[Michael Shulman]

On Wed, May 14, 2014 at 1:57 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:

> Definition AbstractCircle := { X : Type & merely ( [all the data
> (base,loop,elim,comp x2) of the usual S1 ] ) }.
>

> Here’s a puzzle: suppose we’re given an abstract circle, by the second
> definition above. Can we construct a circle, in the usual HIT sense?

There is also a "yes" answer using univalence "directly" rather than
via some other construction of a circle. Namely, since any two
circles (with the same UP) are equivalent, by univalence the type of
all circles is a mere proposition. And since an abstract circle is
merely a circle, if we have an abstract circle then the type of
circles is merely inhabited, hence inhabited.

Mike

[Daniel R. Grayson]

Yes, it can, see definitions at and following https://github.com/UniMath/UniMath/blob/d58142900c95092cbea044589abd4a7277f3729c/UniMath/Ktheory/Circle.v#L223

The version there is for simple recursion.  I expect the same outline to work for dependent circle induction.

[Martin Escardo]

Nice way of getting the suitable loop.

Martin

[Peter LeFanu Lumsdaine]

On Wed, May 14, 2014 at 11:00 AM, Martin Escardo
<m.es...@cs.bham.ac.uk> wrote:
> Can we show that if we replace the base point of the HoTT-book circle by any
> (hypothetical) point and a suitable loop, then the universal property of the
> pointed circle is still satisfied?

 

On Wed, May 14, 2014 at 11:12 PM, Michael Shulman <shu...@sandiego.edu> wrote:

 

Yes, I think we can.

Suppose given x:S1.  First we need to construct a "suitable" loop.  

An alternative and perhaps simpler way to get the suitable loop is by eliminating on x: in case x=base, we use the canonical loop there, and for the loop case, we end up needing to show that loop.loop.!loop = loop.

Or we can attack the whole problem differently.  Instead of starting by constructing the loop, we can directly construct for each x:S1 an equivalence e_x : S1 <~> S1 with a path alpha_x : e_x (base) = x.  In the case x=base, we of course use (id S1, refl).  For the loop clause, we need to show

transport loop (id S1, refl) = (id S1, refl)

Working out how the transport acts, this amounts to showing

(id S1, refl) = (id S1, loop)

which comes down to giving a pair

{ h : id S1 = id S1 & ap10 h x = loop }

for which we use the usual "spin" homotopy.  So we now have, for each x, an automorphism sending base to x; so now we can transfer the original universal property along this equivalence, either by univalence or by hand.

Yet another approach would be to eliminate on x immediately, into the whole main goal "some loop at x, along with an eliminator and comp functions”! But then it seems like the transport one has to deal with might get rather horrific…

–p.

[Vladimir Voevodsky]

Yes. It is the main theorem of Dan's formalization.

V.

[Vladimir Voevodsky]

The small/large issues can be easily controlled with resizing rules. And for this particular issue I think that weak resizing (which can be directly justified by the standard model) is sufficient.

V.


On May 14, 2014, at 11:22 PM, steve awodey <steve...@icloud.com> wrote:

> good question.
> the impredicative (“polymorphic”) construction does not require there to already be a circle — but it only has the right UP with respect to small types, and it is (a priori) large. I think this is also the case for Dan’s torsor circle?

[Michael Shulman]

Has anyone written out this theorem in a form that a human can read?

[Peter LeFanu Lumsdaine]

On Thu, May 15, 2014 at 6:51 PM, Michael Shulman <shu...@sandiego.edu> wrote:

Has anyone written out this theorem in a form that a human can read?

I don’t know, but Dan has explained it to me over lunch on napkins, and I remember it being a very nice human-comprehensible proof.  If he doesn’t have a chance to do so sooner (and doesn’t object), then I can try to reconstruct a sketch of it here, probably some time tomorrow.

–p.

expla

[Daniel R. Grayson]

Here's a proof sketch, perhaps from what was on the napkins so long ago.

We define BG to be the type of left G-torsors, pointed by the trivial G-torsor provided

by left multiplication on the underlying set of G, with the proof of nonemptiness provided

by the unit element of G.  First one proves, using the structure

identity principle or using the Rezk completion theorem, that Loops BG <~> G.

Now we let Z be the group of integers and define Circle to be BZ.  We let Loop be

the loop at the basepoint of Circle provided by univalence applied to the translation

by +1 (or by -1).

Let Y be a type, let y:Y, and let l:y=y.  We want a map r:Circle->Y.

Now consider, for each T:Circle, the type GH(T) whose elements consist of three

things: a point y':Y; for each t:T a path p_t : y'=y; and for each t:T an 

equation p_t * l = p_(1+t).  One proves GH(T) is contractible.  Let X be the total

space of GH.  It maps by projection on the first factor to Circle by an equivalence,

and by projection on the point y' to Y.  Composing the inverse of the first map

with the second map gives the desired map r:Circle->Y.

Here is how you prove GH(T) is contractible.  Contractibility is a proposition, T is

nonempty, and nonemptiness of T is the propositional truncation of T, so we may

assume we have t:T, hence that T is the trivial torsor defined above.  Now make an

element of GH(T) by taking y' to be y and by taking p_t to be the t-th power of l, thinking of

t as an integer.  Now show every pair of elements of GH(T) are equal.  Do that

by showing that an element of GH(T) is determined by (y',p_0) -- by induction over nat,

the paths p_n for n>0 are determined, and by induction over nat

again, the paths p_n for n<0 are also determined uniquely.  But all pairs of the form

(y',p_0) are equal to each other.

The proof that the resulting map r sends Loop to l is a computation, currently

sort of messy, but the basic idea is that transport along Loop of the element of GH(T) constructed

above substitutes t+1 for t, and thus amounts to composing all the paths p_t with l,

and in particular to composing p_0 with l, so when projecting onto the variable endpoint of

p_0 we see l.

[Michael Shulman]

Very nice; thanks!! Let me guess how to modify this for the induction
principle.

On Thu, May 15, 2014 at 10:56 AM, Daniel R. Grayson <d...@math.uiuc.edu> wrote:
> Let Y be a type, let y:Y, and let l:y=y. We want a map r:Circle->Y.

Let Y : Circle -> Type be a family, with y:Y(Z) and l:y=_{Loop} y.

> Now consider, for each T:Circle, the type GH(T) whose elements consist of
> three
> things: a point y':Y; for each t:T a path p_t : y'=y; and for each t:T an
> equation p_t * l = p_(1+t).

For each T:Circle, let GH(T) consist of three things: a point y':Y(T),
for each t:T a path p_t : y' =_{f(t)} y, and for each t:T an equation
p_t * l =_{?} p_(1+t). Here f(t) : T = Z is induced by univalence
from the equivalence between T and the trivial Z-torsor Z under which
t corresponds to 0, and for the latter equation to make sense we need
to prove that f(t) o Loop = f(1+t).

Now the rest of the proof should be basically the same. Right?

How about adding this to the wiki page
http://ncatlab.org/homotopytypetheory/show/circle
?

[Daniel R. Grayson]

Yes, that sounds like what I had in mind, but I didn't write it down.

By the way, the map r:Circle->Y sends the base point to y by definition, not

just propositionally.

I'll add it to the wiki page -- thanks for the suggestion.

[Michael Shulman]

How far can this be generalized? I bet you can do a wedge of
decidably many circles, using the free group on that many generators.

On Thu, May 15, 2014 at 12:13 PM, Daniel R. Grayson <d...@math.uiuc.edu> wrote:
> Yes, that sounds like what I had in mind, but I didn't write it down.
>
> By the way, the map r:Circle->Y sends the base point to y by definition, not
> just propositionally.
>
> I'll add it to the wiki page -- thanks for the suggestion.
>
>

[Steve Awodey]

he gave a lovely talk about it in synthetic style here in Paris — he should write it up for the blog, or the next edition of the book!

[Steve Awodey]

Ah yes — the wiki is a good place for it too.