New answers tagged homotopy-type-theory
6
votes
Accepted
Why isn't $S^1$ contractible in homotopy type theory?
Perhaps this will help: in homotopy type theory, to say that $x$ and $y$ of type $A$ are different corresponds intuitively to the fact that they are in different connected components, i.e., there is ...
- 46.1k
5
votes
Why isn't $S^1$ contractible in homotopy type theory?
The question was answered by Noah Snyder in the comments: No, $S^1$ is not contractible.
It connected, so any point in $S^1$ is merely equal to $base$.
To prove that $S^1$ is not contractible, you ...
Top 50 recent answers are included