Intuition behind UTT's internal logic

Question

The "internal logic" of type theory UTT is defined in LF as follows:

What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - we have the universe of propositions, and to every proposition (i.e., every object of type $Prop$) there corresponds a type of its proofs via $\textbf{Prf}$ (here, I also don't have intuition on why this would be a reasonable/useful thing to have); $\forall$ stands for the usual universal quantification. But what's the intuition behind $(9.4), (9.5), (9.6)$?

And by the way, what exactly does the term "internal logic" mean? Maybe there isn't a rigorous definition of this term, but for example why doesn't the "internal logic" described above say anything about predicative universes (which also exist in UTT; but they are described separately, after the introduction of internal logic)?

Answer 1

1. $\mathit{Prop}$ is a universe and $\mathrm{Prf}$ is its decoding function. (Often called $T$ for Tarski-style universe.)
2. $\Lambda$ is the introduction rule for universal quantification.
3. $\mathbf{E}_\forall$ is the elimination rule for universal quantification.
4. Equation (9.6) is the computation rule explaining what happens when we eliminate an introduction form.

You should compare these rules with the rules for universal quantifiers in type theory.

Internal logicis a broad term that cannot be explained in this answer. I will not even try.