diff --git a/docs/algebra.tex b/docs/algebra.tex index 9cfed25eaca982e31b347286ce1b1b4eabe61bd7..3ba0967042888774ba91ee1af53f50d672ba8acc 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -37,7 +37,8 @@ Elements that cannot be distinguished by programs within $n$ steps remain indist The category $\OFEs$ consists of OFEs as objects, and non-expansive functions as arrows. \end{defn} -Note that $\OFEs$ is cartesian closed. In particular: +Note that $\OFEs$ is bicartesian closed, \ie it has all sums, products and exponentials as well as an initial and a terminal object. +In particular: \begin{defn} Given two OFEs $\ofe$ and $\ofeB$, the set of non-expansive functions $\set{f : \ofe \nfn \ofeB}$ is itself an OFE with \begin{align*}