Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Implication of walking isomorphism ≅ single object?

Madeleine Birchfield (Mar 16 2025 at 18:36):

Ryo Suzuki said:

It might be related to the notion of path induction in HoTT, but I don’t know much about it…

In HoTT, there is the unit type $1$ and the interval type $\mathbb{I}$. Functions from $1$ to a type $A$ correspond to elements in $A$, while functions from $\mathbb{I}$ to $A$ correspond to paths / identifications / equalities in $A$, which are always invertible by path induction. One can prove that $1$ and $\mathbb{I}$ are both singletons (i.e. contractible types) and thus equivalent to each other

If we interpret types $A$ as $\infty$-groupoids, then elements of types are objects in $\infty$-groupoids, while paths of types are 1-morphisms of $\infty$-groupoids, which are always isomorphisms by definition of $\infty$-groupoid. $1$ is the terminal $\infty$-groupoid, while $\mathbb{I}$ is the walking isomorphism.

Alex Kreitzberg (Mar 16 2025 at 18:47):

I tried to change the title to be less confusing.

Alex Kreitzberg (Mar 16 2025 at 18:51):

Hah! Although after understanding Madeleine's point better, I guess the old title still worked - nevermind XD.