DiscreteGraphicMonoids.indexMartin Escardo and Paulo Oliva, April 2024
Following Lawvere [1], we show that lists without repetitions over a
discrete type form the free discrete graphic monoid, where a monoid is
called graphic if it satisfies the identity xyx=xy.
From this we conclude, in a standard way, that lists without
repetitions form a monad.
We thank Jonas Frey for giving us this reference:
[1] F. William Lawvere. Display of graphs and their applications, as
exemplified by 2-categories and the Hegelian "taco". Proceedings
of the first international conference on algebraic methodology and
software technology University of Iowa, May 22-24 1989, Iowa City,
pp. 51-74.
https://github.com/mattearnshaw/lawvere/blob/master/pdfs/1989-display-of-graphics-and-their-applications-exemplifed-by-2-categories-and-the-hegelian-taco.pdf
\begin{code}
{-# OPTIONS --safe --without-K #-}
module DiscreteGraphicMonoids.index where
import DiscreteGraphicMonoids.Type
import DiscreteGraphicMonoids.ListsWithoutRepetitions
import DiscreteGraphicMonoids.LWRDGM
import DiscreteGraphicMonoids.Free
import DiscreteGraphicMonoids.Monad
import DiscreteGraphicMonoids.AffineMonad
import DiscreteGraphicMonoids.ListsWithoutRepetitionsMore
\end{code}
1. The module Type defines the type of discrete graphic monoids.
2. The module ListsWithoutRepetitions investigates lists without
repetitions over discrete types.
3. The module LWRDGM shows that lists without repetitions over a
discrete type form a discrete graphic monoid.
4. The module Free shows that lists without repetitions over a discrete
type form the free discrete graphic monoid.
5. The module Monad uses this, in a standard way, to show that lists
without repetitions form a monad. (TODO. The algebras of the monad
are, up to equivalence, the graphic monoids, again in a standard
way.)
6. The module AffineMonad shows that non-empty lists without
repetitions form an affine submonad of the above.
7. The module ListsWithoutRepetitionsMore includes additional facts
about lists without repetitions that are not needed for our main
results.