Not signed in (Sign In)

# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Sign in using OpenID

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

1. Page created, but author did not leave any comments.

Anonymous

2. added info about the circle type

Anonymous

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeJun 8th 2022

fixed some grammar and touched the wording in the Definition-section

3. Adding link to Jordan curve

Anonymous

4. Adding coequalizer definition of the circle type

Anonymous

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeJan 30th 2023

tried to bring some logical order back into the list of references.

• CommentRowNumber7.
• CommentAuthorGuest
• CommentTimeMar 1st 2023

This page says:

Its induction principle says that for any $P:S^1\to Type$ equipped with a point $base' : P(base)$ and a dependent path $loop':base'= base'$, there is $f:\prod_{(x:S^1)} P(x)$ such that:

Should it instead say $loop' : tr^{loop}_P(base') = base'$, or $loop' : base' =^{loop}_{P} base'$, or “dependent path $loop':base'= base'$ over $loop$”, or something like that? Does it matter?

Adrian

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeMar 2nd 2023
• (edited Mar 2nd 2023)

I think that’s right, there is a transport involved. That’s what the link dependent path is referring to. For the moment i have added (here) the missing $=_{loop}$-subscript and a pointer to UFP13, p. 177.

Ideally I would like to polish up the whole presentation (which is due to the notorious “Anonymous”, in revision 5) but not now.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeMar 2nd 2023

On whether it matters: I expected it does. While I haven’t tried to write out a formal argument, a quick idea goes as follows:

In the higher induction principle of the suspension type $\mathrm{S}S^0$ there is certainly such dependent identifications involved, namely along the two “meridian” paths from the “north pole” to the “south pole”: by the general rules of higher inductive types, but also because here it would not even type-check otherwise. But then for the evident map $S^1 \to \mathrm{S}S^0$ to be an equivalence, there must be a corresponding dependent identification also in the induction principle of $S^1$.

Add your comments
• Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
• To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

• (Help)