Skip to main content

Research Repository

Advanced Search

Relative monads formalised

Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo

Authors

James Chapman

Tarmo Uustalu



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 28, 2024
Journal Journal of Formalized Reasoning
Electronic ISSN 1972-5787
Publisher 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

Files





You might also like



Downloadable Citations