Thanks, Peter and @mike-shulman. I mean models of ITT without univalence or funext, and "good old-fashioned set model" in Peter's answer and ones in Mike's answer are what I want. I shouldn't have used the word "HoTT".

@user40276 Thanks. Then what forms a filter in this case? Directed subsets of a poset?

By mapping $* \mapsto *, \Box_1 \mapsto \Box, \Box_2 \mapsto \Box, \Box_3 \mapsto \triangle$, one can show that System U (and hence $\lambda\ast$) is also inconsistent. The product rule $(\triangle, \Box, \Box)$ corresponds to $(\Box_3, \Box_2, \Box_2)$ in $\lambda$Z.

One can construct the type $U := \Pi (X: \Box_2) (X \to X \to \ast) \to X \to \ast$ of the universe and the relation $\mathsf{elt}\colon U \to U \to \ast$ over $U$, and construct arbitrary sets by the axiom schema of separation. By adding $(\Box_3, \Box_2, \Box_2) \in R$ to $\lambda$Z, one has $U \colon \Box_2$, which leads to the inconsistency.