Implementing Categorical Notions of Partiality and Delay in Agda

To see a full list of all the modules go to:

open import Everything

For my bachelor thesis I am implementing categorical notions of partiality in agda using the agda-categories library. The repo for this project can be found here. This is an implementation of this paper by Sergey Goncharov: arxiv

Index

Preliminaries

The work takes place in an ambient category that fits our needs:

open import Category.Ambient

We add the notion of equational lifting monad (by Bucalo et al.) to this library, ideally it will be introduced to agda-categories in the future:

open import Monad.EquationalLifting

Maybe Monad

We start out by looking at the maybe monad (X + 1) and showing that it is an equational lifting monad.

open import Monad.Instance.Maybe
open import Monad.Instance.Maybe.Strong
open import Monad.Instance.Maybe.Commutative
open import Monad.Instance.Maybe.EquationalLifting

Delay Monad

Next up is Capretta’s Delay Monad. We proof that it is strong and commutative.

open import Monad.Instance.Delay
open import Monad.Instance.Delay.Strong
open import Monad.Instance.Delay.Commutative

Monad K

The goal of this last section is to formalize an equational lifting monad K that generalizes both the maybe monad and the delay monad.

To do so we first need to look at iteration structures, i.e. functor algebras with an iteration operator, these are called Elgot Algebras.

open import Algebra.Elgot

Afterwards we also introduce categories of iteration algebras with iteration preserving morphisms:

open import Category.Construction.ElgotAlgebras

we can form products and exponentials in a canonical way:

open import Category.Construction.ElgotAlgebras.Products
open import Category.Construction.ElgotAlgebras.Exponentials

Free Elgot algebras are free objects in the category of Elgot algebras, we will be needing a notion of stability for them:

open import Algebra.Elgot.Free
open import Algebra.Elgot.Stable

In a CCC stability follows directly

open import Algebra.Elgot.Properties

With this in hand we can now define KX as a free Elgot algebra and proof that under stability it is a strong monad.

open import Monad.Instance.K
open import Monad.Instance.K.Strong

and with this we can show that K is and equational lifting monad, i.e. a commutative monad satisfying the equational lifting law:

open import Monad.Instance.K.Commutative
open import Monad.Instance.K.EquationalLifting

and lastly we formalize the notion of (strong) pre-Elgot monad and show that K is the initial (strong) pre-Elgot monad.

open import Monad.PreElgot
open import Category.Construction.PreElgotMonads
open import Category.Construction.StrongPreElgotMonads
open import Monad.Instance.K.PreElgot
open import Monad.Instance.K.StrongPreElgot

A case study on setoids

Lastly we do a case study on the category of setoids.

First we look at the (quotiented) delay monad on setoids:

open import Monad.Instance.Setoids.Delay

and then we show that it is an instance of K on setoids:

open import Monad.Instance.Setoids.K