As I explicitly state in the answer you reference, if we're modeling a language with a cumulative hierarchy within LF, then the $El$ of LF has no particular relation to the $T_0$ in the object language. As I state there, they aren't even the same kind of thing in that context.

More generally, by design the type structure of LF is not reflected in the object language. We want to use LF to describe any language we desire which may or may not have pi types or universes or may have pi types/universes that work in a different way than in LF. The reason LF has pi types and a universe is because that is what is useful for manipulating contexts and derivations. The reason it has one universe and not an infinite hierarchy is because one suffices for its goals. Ironically, part of the reason LF has one universe is to clearly separate what is and is not part of the object language. If we add a list type constructor, then $\mathsf{List}(A)$ is a type of our object language and in LF is $\mathsf{List}:(A:\mathsf{Type})\mathsf{Type}$. But we don't have $(A:\mathsf{Type})\mathsf{List}(A):\mathsf{Type}$ so $\mathsf{List}((A:\mathsf{Type})\mathsf{List}(A))$ is nonsense as desired. We don't want the pi types of the meta-language to show up as types in the object language.

Oh, this makes things much clearer. (I know you partially restated what you had said in your answer, but sometimes restatements are very helpful, and this is one such case.) So essentially Luo chooses to use the symnol $El$ instead of $T_0$ when defining LF itself, and when we use LF to define other type theories, we use the notation $T_i$. I'm not sure if I got your point with $(A:Type)List(A):Type$, though (but I'll keep re-reading that part as I progress with my understanding of type theory).

But anyway, is it correct that the two universes in CoC would be defined in LF by saying the following?

$$U_0 : \textbf{Type}, \ T_0: (U_0)\textbf{Type}, \ U_1:\textbf{Type}, \ u_0: U_1, \ T_1: (U_1)\textbf{Type}, \ T_1(u_0)=U_0 : \textbf{Type}$$

And if there $T_0$ isn't really used here (i.e., there are no any computation rules like $T_0(\text{something})=\text{something}$), do we still need to declare the constant $T_0$?

You are correct with that being how you would axiomatize two Tarski-style universes. You do need $T_0$ much as LF needs $El$. Because it gets cluttered, invocations of $El$ are suppresed, but they should actually be all over the place. For example, the type of the identity function would be written like $(A:\mathsf{Type})(x:A)A$, but technically it should be $(A:\mathsf{Type})(x:El(A))El(A)$. Also, in practice, as illustrated in the universes paper, whenever you introduce a type within the object language, you'll need to introduce a code for it as well and an equation relating the code and the type, e.g. the $T_0(\mathsf{nat})=\mathsf{Nat}$ where $\mathsf{nat}:\mathcal U_0$. The reason the LF descriptions don't typically add such equations for $El$ is we have no need or desire to reflect the object language's types into LF types. To the object language, the elements of LF's $\mathsf{Type}$ are the types, but to LF they are just codes.

Thank you, now the purpose of declaring the constant $T_0$ is clear. Regarding $(A:Type)(x:El(A))El(A)$, to check my understanding, is the term $(A:Type)(x:A)A$ ill-formed in LF because it is not possible to prove that $\Gamma \vdash (x:A)A \textbf{ kind}$ for any $\Gamma$ using the derivation rules in LF, and so it's not of the form $(x:K)K'$? In contrast, it is possible to prove that $A:Type \vdash (x:El(A))El(A) \textbf{ kind}$, and as a result, the LF-term $(A:Type)(x:El(A))El(A) $ is of the form $(x:K)K'$ where $x=A$, $K=Type$, $K' = (x:El(A))El(A)$. And in general, when declaring a constant $C:L$ in the object theory, $L$ should be derivable from the empty context using LF rules; otherwise, $L$ won't be well-formed, right?

Yes, this is basically correct. The only caveat is you need to factor in how later defined constants can depend on earlier defined constants. One approach (which I dislike but is technically fine) is to have later constants declared with respect to a context containing all earlier constants, so the context may not be empty if this approach is taken. It is still constrained, though. You'd still need to derive the result in a given context, not just any context.