This is the code for (Villa Isaza 2014), in which we study some of the applications of category theory to functional programming, particularly in the context of the Haskell functional programming language, and the Agda dependently typed functional programming language and proof assistant.

Villa Isaza, Juan Pedro (2014). Category Theory Applied to Functional Programming. Undergraduate project. EAFIT. URL: http://bit.ly/1cq5fwN.

The Haskell code was tested with GHC 7.6.3. Most of it corresponds to or is based on standard Haskell code, and can be used as it is. See src/Cain.hs.

The Agda code was tested with:

• Agda 2.3.2.2 and the Agda standard library 0.7
• Agda 2.5.1.1 and the Agda standard library 0.12

See src/Abel.agda.

For more information, send an email to [email protected].