diff --git a/docs/algebra.tex b/docs/algebra.tex index 3295ade48b2e28050a976a3cbe9061587b77d659..6d75e415f47d314eda8cc3a5b65948e53d090df6 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -18,6 +18,8 @@ \ralf{Copy the explanation from the paper, when that one is more polished.} +\ralf{Describe non-expansive, contractive, category $\COFEs$, later, locally non-expansive/contractive, black later.} + \subsection{CMRA} \begin{defn} @@ -83,6 +85,8 @@ This operation is needed to prove that $\later$ commutes with existential quanti \end{mathpar} (This assumes that the type $\type$ is non-empty.) +\ralf{Describe monotone, category $\CMRAs$.} + %%% Local Variables: %%% mode: latex