NLQ is a categorial grammar, a framework for describing the syntax and semantics of natural language. The farmework is based on the Lambek calculus, but has been extended with constructs for the analysis of qualitifiers following Chris Barker. The calculus is formalised in Agda (see doc/NLQ_Agda.lagda), and the formalisation has been translated to Haskell, together with an algorithm for proof search (see src/).