judgmental and propositional statements in homotopy type theory In homotopy type theory one has to distinguish between judgmental and propositional statements, eg
in case of $a: A$ ("$a$ has type $A$") and equalities $a =_p b, a=_A b$. That is, are a judgemental and propositional "$x$ has type $X$" statement, und there are also a judgmental and propositional equality.
I not know how can I evolve an intuition on how to distinguish them. What I read is that generally a statement is propositional if it is "internal" in the theory, while judgmental means that the
statement is "external" in the sense that it is "about" the theory itself and therefore cannot be derived (or say better "constructed") in the theory. On the other hand what does it concretely mean that a statment is "internal" to the theory?
If we try to think about it in case of our "toy examples" $a: A$ and the two equalities, that's sounds strange. How can $a: A$ be simultaneously a internal and external statement? How it can be an internal and external statement (that is "within" the theory and "about")? The same question arises on judgmental and propositional equalities.
Is there a conventional way how one should distinguish between them? Sorry if the question is too broad and indifferent, I think it's hard to find a key to approach these two crucial concepts.
 A: Mark's answer is good, but let me add just a bit more.
Zeroth, this distinction belongs to all dependent type theories and has nothing particular to do with HoTT.
First, in the particular context of HoTT, I don't like the word "propositional" here because in HoTT a special role is played by the types with at most one element, which we call "(mere) propositions", whereas the so-called "propositional equality" need not be a proposition in this sense.  So I prefer "typal equality".
Secondly, there is no typal version of $a:A$.  It is only and always a judgment.  This is in contrast to ZFC, where set-membership $a\in A$ is only and always a proposition.  The corresponding judgment in ZFC is "$a$ is a set", which is trivial since every object in ZFC is a set.  In type theory there are different types of things that are classified by their types: the elements of a function-type $A\to B$ are functions, the elements of a product-type $A\times B$ are pairs, and so on.  So the judgment $a:A$ indicates what type of thing $a$ is, by virtue of having been given a valid definition (or by assumption), before we even start to draw conclusions about it.
Thirdly, a nice analogy (at least) for the difference between definitional/judgmental equality and typal/propositional equality (suggested by Steve Awodey) is that between equality of sense and reference.  Judgmental equality is equality of sense: two expressions are judgmentally equal if they can be seen to be the same by simple syntactic manipulation of their definitions.  In particular, it is not a "mathematical" concept because it is a statement about the syntactic form of a description of an object rather than the object itself.  Typal equality is equality of reference: two objects, which may be referred to by expressions, are in fact the same object.
A: There are two kinds of judgements in Homotopy Type Theory.
The first is a "typing judgement". This is a judgement of the form $a : A$.
The second is "judgemental equality". This is a judgement of the form $a \equiv_A b$.
Propositions in homotopy type theory are represented as types. This means that whenever $a : A$ and $b : A$, $a =_A b$ is a type.
There is no type $a \equiv_A b$.
All reasoning done within homotopy type theory is done using propositions-as-types. For example, let's say that I wanted to show that $a = b$ implies $f(a) = f(b)$.
The type theory statement of this would be $a =_A b \to f(a) =_B f(b)$ (assuming that $f : A \to B$). This is actually a type - the type of all functions which take an element of $a =_A b$ and return an element of $f(a) =_B f(b)$.
Because $a \equiv_A b$ is not a type, there is no type $a \equiv_A b \to f(a) \equiv_B f(b)$.
This suggests that all reasoning within homotopy type theory should be done using propositional equality because the propositions involving equality cannot even be stated using only judgemental equality.
Another example: let's say we want to show that for all $n : \mathbb{N}$, $n + 0 = n$. To even phrase this problem at all, we would have to phrase it as $\prod\limits_{n : \mathbb{N}} n + 0 =_{\mathbb{N}} n$. It is not even possible to state the problem without using propositional equality.
Judgemental equalities are useful for the purposes of definitional computations. For example, part of the defition of $+$ is that $0 + n = n$ for all $n$. In this case, because this is a definitional equality, we actually have $0 + n \equiv_{\mathbb{N}} n$ for every term $n : \mathbb{N}$. So a lot of definitional simplifications are done using judgemental equality.
On the other hand, it is not within the definition of $+$ that $n + 0 = n$. Therefore, it cannot be shown that $n + 0 \equiv_{\mathbb{N}} 0$ for every term $n : \mathbb{N}$.
So a better way to think about judgemental equality is definitional equality. When one thing is defined to be equal to another, the equality is judgemental. Otherwise, the equality is propositional.
