Relative monads formalised

Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo

Abstract

Relative monads are a generalisation of ordinary monads where the underlying functor need not be an endofunctor. In this paper, we describe a formalisation of the basic theory of relative monads in the interactive theorem prover and dependently typed programming language Agda. The formalisation comprises the requisite basic category theory, the central concepts of the theory of relative monads and adjunctions, which are compared to their ordinary counterparts, and two running examples from programming theory.

Citation

Altenkirch, T., Chapman, J., & Uustalu, T. (2014). Relative monads formalised. Journal of Formalized Reasoning, 7(1), https://doi.org/10.6092/issn.1972-5787/4389

• Journal Article Type: Article
• Publication Date: Jan 1, 2014
• Deposit Date: Mar 2, 2015
• Publicly Available Date: Mar 2, 2015
• Journal: Journal of Formalized Reasoning
• Electronic ISSN: 1972-5787
• Publisher: Alma Mater Studiorum - Università di Bologna
• Peer Reviewed: Peer Reviewed
• Volume: 7
• Issue: 1
• DOI: https://doi.org/10.6092/issn.1972-5787/4389
• Public URL: https://nottingham-repository.worktribe.com/output/997864
• Publisher URL: http://jfr.unibo.it/article/view/4389
• Contract Date: Mar 2, 2015