Algebra.Pregroup

Abstract

This repository hosts the formalisation of the theory of pregoups, as described by Joachim Lambek in his book From Word to Sentence: A Computational Algebraic Approach To Grammar, in Agda.

Technical Details

• the code was written for use with version 2.4.0 of the Agda standard library (though older versions should work);

• the code is released under an MIT license;

• see here for the code in fancy clickable html.