Commit fc9e25a5 authored by Ralf Jung's avatar Ralf Jung

OFEs are bicartesian closed

parent 48c7dfca
Pipeline #5626 passed with stages
in 5 minutes and 56 seconds
......@@ -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*}
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment