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?



Are there types with nontrivial paths in all dimensions? (HoTT)
$\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.


