Formalising Type-Logical Grammars in Agda