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

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

Community wiki

Top 50 recent answers are included

#### Related Tags

homotopy-type-theory × 127lo.logic × 49

type-theory × 46

ct.category-theory × 23

homotopy-theory × 22

at.algebraic-topology × 17

foundations × 16

higher-category-theory × 14

infinity-topos-theory × 11

reference-request × 9

soft-question × 8

constructive-mathematics × 6

cohomology × 4

infinity-categories × 4

ag.algebraic-geometry × 3

real-analysis × 3

computer-science × 3

mathematical-philosophy × 3

groupoids × 3

set-theory × 2

gn.general-topology × 2

homological-algebra × 2

computability-theory × 2

simplicial-stuff × 2

topos-theory × 2