Are there types with nontrivial paths in all dimensions? (HoTT)

Question

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?

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.