A formalisation of the theory of pregoups, as described by Joachim Lambek, in Agda.