Conal Elliott: Could you briefly explain the universal property in section 2 of Compiling to Categories? I don't understand the syntax of the formula given, notably the "double vee": `vh. h v f v g v v exl v h v f v exr v h v g`