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?