What colour is it?

• punctuation is black, so as not to make an issue of it
• type constructors (declared and computed) are blue, because they are upper class: they are well-behaved (hopefully, you can decide typechecking, with no side-effects to boot), nor do they do any work (notionally, they get erased at run-time; you can't do cases on types), they own terms
• term constructors are red, because terms are working class: you can do case analysis on them, their criminality depends on the liberality of the regime
• holes (metavariables) are orange because they represent problems, solved by turning them into...
• definitions (lets), which are therefore green; elimination constants are also green, because we may imagine them to be defined by pattern matching
• other identifiers (eg, lambda-/Pi-bound variables and pattern variables) are magenta because that's the only other colour of slide pen I can stand, hence
• things I wish to discredit are either shown as photocopied ASCII in Courier font which is slightly too small to read, or, when handwritten, in yellow or (if legibility is essential) brown

• index of these slides
• Conor's home page