An embedding of Lambek Grishin calculus (and its transformations to Linear Logic) in Agda.