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.
Best Answer
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.