I'm trying to construct a model of homotopy type theory, and in my development it seems like it would be helpful to assume that all types only have trivial paths below a given level (forgive my vocabulary, I am new to homotopy theory). So given

\begin{equation} X : U \\ a,b : X \\ p_0,q_0 : a=_X b \\ p_1,q_1 : p=_{a=b}q \\... \end{equation}

Is there always some $n$ such that for all $i > n$, $p_i = idp$, the identity path? If not, can you give an example of a type with nontrivial structure at all levels?


1 Answer 1


$\prod_{n\in\mathbb{N}} S^n$ certainly has nontrivial structure at all levels (i.e. "is not a homotopy $n$-type for any finite $n$"). In classical homotopy theory, even $S^2$ by itself has nontrivial structure at all levels (though $S^1$ doesn't), but I don't believe this has been proven in HoTT yet.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.