 Martin-Löf distinguishes carefully between proofs and derivations: a proof object is a witness to the fact that some proposition has been proved; whereas a derivation is the record of the construction of a proof object. Also, he exercises two basic forms (one dare not say “types” here) of judgement. The first is a relation between proof objects and propositions, the second a property of some propositions. In the first case, the judgement is either one that a proof object \(a\) is a witness to a proposition \(A\), or else one that two proof objects \(a\) and \(b\) are equal and both witness that \(A\) has been proved. The first case of the second form of judgement states that a proposition \(A\) is well-formed, and the second records that two propositions \(A\) and \(B\) are equal.