This question already has an answer here:
Reading Lurie's Higher topos theory got me thinking, if we can think of $(\infty,1)-$categories as (1-)categories enriched over $\infty$-groupoid, then wouldn't the internal definition of an $(\infty,1)$-category in Homotopy type theory be the usual univalent category but with homs as usual types instead of sets?
This seems to correspond to the notion of category in the HoTT library although technically the HoTT book defines a category to have hom-sets instead of types.
The first higher category I can think of is $\infty$-groupoid where the type of objects is simply $\mathcal U_0$, and then morphisms are the types $X \to Y$ which I am assuming isn't truncated or anything. Then the circle $S^1$ defined as a higher inductive type is in this category. And the hom-type $S^1\to S^1$ is some sort of elimator of the HIT for $S^1$ which is itself a HIT.
This (I think) obviously only works if our ambient category is $\infty$-groupoid itself (which is some form of HoTT). I am not sure this applies to all $\infty$-toposes.