Relative Monads Formalised

Authors

  • Thorsten Altenkirch University of Nottingham
  • James Chapman Institute of Cybernetics, Tallinn
  • Tarmo Uustalu Institute of Cybernetics, Tallinn

DOI:

https://doi.org/10.6092/issn.1972-5787/4389

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. 

Downloads

Published

2014-07-17

How to Cite

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

Issue

Vol. 7 No. 1 (2014)

Section

Articles

License

Copyright (c) 2014 Thorsten Altenkirch, James Chapman, Tarmo Uustalu

Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.

Creative Commons License

This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy