I'm reading this thesis by Michael Warren on Homotopy Type Theory. I'm really a newbie to the field and got puzzled right in the beginning, where the following rule appears:
A little bit before he writes down the legal 'forms of judgement':
So is there missing '$:{\text type}$' at the end of the of the bottom judgement in the rule? He was pretty clear about which notational conventions and abbreviations he uses (for example, all inference rules are written with the empty context for simplicity), so I'm unsure if he was just sloppy at this point or if something more substantial is going on...
This looks like a minor omission to me. I would read it as follows:
$$\frac{x\colon C \vdash A(x)\colon \mathrm{type}\quad x: C \vdash a(x),b(x) : A(x) \quad \vdash c: C}{ \vdash (\mathrm{Id}_{A(x)}(a(x),b(x)))[c/x] = \mathrm{Id}_{A(c)}(a(c),b(c))\,\colon\,\mathrm{type} }\,\textrm{(Id coherence)}$$
There is also an unmatched parenthesis in the "$\mathrm{Id}_{A(c))}$" on the right hand side of the equation... Don't get bogged down in all these notational details, and try to read it using your "internal type-inference algorithms".