From fc9e25a5edc867b40cea6725220b2127a0bdced0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 28 Nov 2017 17:46:17 +0100
Subject: [PATCH] OFEs are bicartesian closed

---
 docs/algebra.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/docs/algebra.tex b/docs/algebra.tex
index 9cfed25ea..3ba096704 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*}
-- 
GitLab