module _ where
{-
"Quotienting the Delay Monad by Weak Bisimilarity"
by James Chapman, Tarmo Uustalu, Niccolo Veltri
We show an Agda formalization of the delay monad quotiented by weak
bisimilarity in Martin-LĆ¶f type theory extended with quotient types a
la Hofmann and employing the axiom of countable choice.
The code type checks with Agda version 2.4.3 and standard library
version 0.9.
The formalization is structured as follows:
-}
open import Prerequisites
{-
We introduce the type theory under consideration (Section 2) and
quotient types (Section 4 without Lemma 3).
-}
open import AC
{-
The full axiom of choice implies that box is a split epimorphism
which in turn implies LEM. (Propositions 4 and 3).
-}
open import AComega
{-
The axiom of countable choice and its interaction with quotient types
(Section 6).
-}
open import DelayMonad
{-
Delay monad and weak bisimilarity (Section 3 and Lemma 3).
-}
open import DelayStream
{-
Delayed computations as streams (Section 7.1).
-}
open QuotientD
open import Multiplication liftD liftβD liftLargeD liftβLargeD
{-
Delay type quotiented by weak bisimilarity is a monad:
unit and multiplication (Section 7.2).
-}
open import MonadLaws liftD liftβD liftLargeD liftβLargeD
{-
Delay type quotiented by weak bisimilarity is a monad:
monad laws (not in the paper).
-}
open import CPOs
{-
Definition of CPO and continuous map (Section 9.1).
-}
open import DelayCPO
open import DelayFreeCPO
{-
The delay datatype applied to a type X is the free CPO over
X up to weak bisimilarity (Section 9.2).
-}
open import DelayCPOQuot
open import DelayFreeCPOQuot
{-
Lifting the construction above to the quotient, showing that the
quotiented delay datatype applied to a type X is the free CPO over
X (Section 9.3).
-}
open import Sierpinski
{-
Free countably-complete join semilattice on 1 and proof that the
partial map classifier associated with it is a monad (Proposition 8
of Section 10).
In this file we use the option type-in-type. It is not difficult (but
rather boring) to switch to a universe-polymorphic version of the
file.
-}