algebra.tex 15.9 KB
 Ralf Jung committed Dec 10, 2017 1 \section{Algebraic Structures}  Ralf Jung committed Jan 31, 2016 2   Ralf Jung committed Dec 05, 2016 3 \subsection{OFE}  Ralf Jung committed Feb 29, 2016 4   Ralf Jung committed Dec 05, 2016 5 The model of Iris lives in the category of \emph{Ordered Families of Equivalences} (OFEs).  Ralf Jung committed Mar 12, 2016 6 This definition varies slightly from the original one in~\cite{catlogic}.  Ralf Jung committed Mar 15, 2016 7   Ralf Jung committed Feb 29, 2016 8 \begin{defn}  Ralf Jung committed Dec 05, 2016 9  An \emph{ordered family of equivalences} (OFE) is a tuple $(\ofe, ({\nequiv{n}} \subseteq \ofe \times \ofe)_{n \in \nat})$ satisfying  Ralf Jung committed Feb 29, 2016 10  \begin{align*}  Ralf Jung committed Dec 05, 2016 11 12 13  \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{ofe-equiv} \\ \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{ofe-mono} \\ \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{ofe-limit}  Ralf Jung committed Feb 29, 2016 14 15 16  \end{align*} \end{defn}  Ralf Jung committed Dec 05, 2016 17 18 The key intuition behind OFEs is that elements $x$ and $y$ are $n$-equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps. In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{ofe-mono})---and in the limit, it agrees with plain equality (\ruleref{ofe-limit}).  Ralf Jung committed Feb 29, 2016 19   Ralf Jung committed Mar 07, 2016 20 \begin{defn}  Ralf Jung committed Dec 05, 2016 21 22 23 24  An element $x \in \ofe$ of an OFE is called \emph{discrete} if $\All y \in \ofe. x \nequiv{0} y \Ra x = y$ An OFE $A$ is called \emph{discrete} if all its elements are discrete. For a set $X$, we write $\Delta X$ for the discrete OFE with $x \nequiv{n} x' \eqdef x = x'$  Ralf Jung committed Mar 07, 2016 25 26 27 \end{defn} \begin{defn}  Ralf Jung committed Dec 05, 2016 28 29  A function $f : \ofe \to \ofeB$ between two OFEs is \emph{non-expansive} (written $f : \ofe \nfn \ofeB$) if $\All n, x \in \ofe, y \in \ofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y)$  Ralf Jung committed Mar 07, 2016 30  It is \emph{contractive} if  Ralf Jung committed Dec 05, 2016 31  $\All n, x \in \ofe, y \in \ofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y)$  Ralf Jung committed Mar 07, 2016 32 \end{defn}  Ralf Jung committed Mar 15, 2016 33 34 Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data. Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$.  Ralf Jung committed Mar 07, 2016 35 36  \begin{defn}  Ralf Jung committed Dec 05, 2016 37  The category $\OFEs$ consists of OFEs as objects, and non-expansive functions as arrows.  Ralf Jung committed Mar 07, 2016 38 \end{defn}  Ralf Jung committed Mar 11, 2016 39   Ralf Jung committed Nov 28, 2017 40 41 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:  Ralf Jung committed Mar 11, 2016 42 \begin{defn}  Ralf Jung committed Dec 05, 2016 43  Given two OFEs $\ofe$ and $\ofeB$, the set of non-expansive functions $\set{f : \ofe \nfn \ofeB}$ is itself an OFE with  Ralf Jung committed Mar 11, 2016 44  \begin{align*}  Ralf Jung committed Dec 05, 2016 45  f \nequiv{n} g \eqdef{}& \All x \in \ofe. f(x) \nequiv{n} g(x)  Ralf Jung committed Mar 11, 2016 46 47  \end{align*} \end{defn}  Ralf Jung committed Mar 07, 2016 48 49  \begin{defn}  Ralf Jung committed Dec 05, 2016 50  A (bi)functor $F : \OFEs \to \OFEs$ is called \emph{locally non-expansive} if its action $F_1$ on arrows is itself a non-expansive map.  Ralf Jung committed Mar 07, 2016 51 52  Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map. \end{defn}  Ralf Jung committed Mar 11, 2016 53 The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.  Ralf Jung committed Mar 11, 2016 54 Note that the composition of non-expansive (bi)functors is non-expansive, and the composition of a non-expansive and a contractive (bi)functor is contractive.  Ralf Jung committed Dec 05, 2016 55   Ralf Jung committed Dec 08, 2017 56 57 58 59 60 61 62 63 64 65 One very important OFE is the OFE of \emph{step-indexed propositions}: For every step-index, such a proposition either holds or does not hold. Moreover, if a propositions holds for some $n$, it also has to hold for all smaller step-indices. \begin{align*} \SProp \eqdef{}& \psetdown{\nat} \\ \eqdef{}& \setComp{X \in \pset{\nat}}{ \All n, m. n \geq m \Ra n \in X \Ra m \in X } \\ X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y \\ X \nincl{n} Y \eqdef{}& \All m \leq n. m \in X \Ra m \in Y \end{align*}  Ralf Jung committed Dec 05, 2016 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 \subsection{COFE} COFEs are \emph{complete OFEs}, which means that we can take limits of arbitrary chains. \begin{defn}[Chain] Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}$ of equivalence relations, a \emph{chain} is a function $c : \nat \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$. \end{defn} \begin{defn} A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe : \OFEs, \lim : \chain(\cofe) \to \cofe)$ satisfying \begin{align*} \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl} \end{align*} \end{defn} \begin{defn} The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. \end{defn} The function space $\ofe \nfn \cofeB$ is a COFE if $\cofeB$ is a COFE (\ie the domain $\ofe$ can actually be just an OFE).  Robbert Krebbers committed Dec 10, 2017 86 $\SProp$ as defined above is complete, \ie it is a COFE.  Ralf Jung committed Dec 05, 2016 87 88 89  Completeness is necessary to take fixed-points.  Robbert Krebbers committed Dec 10, 2017 90 91 92 \begin{thm}[Banach's fixed-point] \label{thm:banach} Given an inhabited COFE $\ofe$ and a contractive function $f : \ofe \to \ofe$, there exists a unique fixed-point $\fixp_T f$ such that $f(\fixp_T f) = \fixp_T f$.  93 Moreover, this theorem also holds if $f$ is just non-expansive, and $f^k$ is contractive for an arbitrary $k$.  Robbert Krebbers committed Dec 10, 2017 94 95 96 97 98 99 100 101 \end{thm} \begin{thm}[America and Rutten~\cite{America-Rutten:JCSS89,birkedal:metric-space}] \label{thm:america_rutten} Let $1$ be the discrete COFE on the unit type: $1 \eqdef \Delta \{ () \}$. Given a locally contractive bifunctor $G : \COFEs^{\textrm{op}} \times \COFEs \to \COFEs$, and provided that $$G(1, 1)$$ is inhabited, then there exists a unique\footnote{Uniqueness is not proven in Coq.} COFE $\ofe$ such that $G(\ofe^{\textrm{op}}, \ofe) \cong \ofe$ (\ie the two are isomorphic in $\COFEs$). \end{thm}  Ralf Jung committed Mar 07, 2016 102 103 104  \subsection{RA}  Ralf Jung committed Mar 12, 2016 105 106 \begin{defn} A \emph{resource algebra} (RA) is a tuple \\  Ralf Jung committed Dec 08, 2017 107  $(\monoid, \mvalFull : \monoid \to \mProp, \mcore{{-}}:  Ralf Jung committed Jul 25, 2016 108  \monoid \to \maybe\monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying:  Ralf Jung committed Mar 12, 2016 109 110 111  \begin{align*} \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{ra-assoc} \\ \All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{ra-comm} \\  Ralf Jung committed Jul 25, 2016 112 113 114  \All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\ \All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\ \All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\  Ralf Jung committed Dec 08, 2017 115  \All \melt, \meltB.& \mvalFull(\melt \mtimes \meltB) \Ra \mvalFull(\melt) \tagH{ra-valid-op} \\  Ralf Jung committed Mar 12, 2016 116  \text{where}\qquad %\qquad\\  Ralf Jung committed Jul 25, 2016 117  \maybe\monoid \eqdef{}& \monoid \uplus \set{\mnocore} \qquad\qquad\qquad \melt^? \mtimes \mnocore \eqdef \mnocore \mtimes \melt^? \eqdef \melt^? \\  Ralf Jung committed Jul 25, 2016 118  \melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}  Ralf Jung committed Mar 12, 2016 119 120  \end{align*} \end{defn}  Ralf Jung committed Dec 08, 2017 121 122 123 Here, $\mProp$ is the set of (meta-level) propositions. Think of \texttt{Prop} in Coq or $\mathbb{B}$ in classical mathematics.  Ralf Jung committed Mar 15, 2016 124 125 RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two key differences: \begin{enumerate}  Ralf Jung committed Dec 08, 2017 126 127 \item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}). These valid elements are identified by the \emph{validity predicate} $\mvalFull$.  Ralf Jung committed Mar 15, 2016 128   Robbert Krebbers committed Dec 10, 2017 129 This take on partiality is necessary when defining the structure of \emph{higher-order} ghost state, \emph{cameras}, in the next subsection.  Ralf Jung committed Jul 25, 2016 130 131 132 133 134  \item Instead of a single unit that is an identity to every element, we allow for an arbitrary number of units, via a function $\mcore{{-}}$ assigning to an element $\melt$ its \emph{(duplicable) core} $\mcore\melt$, as demanded by \ruleref{ra-core-id}. We further demand that $\mcore{{-}}$ is idempotent (\ruleref{ra-core-idem}) and monotone (\ruleref{ra-core-mono}) with respect to the \emph{extension order}, defined similarly to that for PCMs (\ruleref{ra-incl}).  Ralf Jung committed Jul 25, 2016 135  Notice that the domain of the core is $\maybe\monoid$, a set that adds a dummy element $\mnocore$ to $\monoid$.  Ralf Jung committed Jul 25, 2016 136 137 138 139 140 141 142 % (This corresponds to the option type.) Thus, the core can be \emph{partial}: not all elements need to have a unit. We use the metavariable $\maybe\melt$ to indicate elements of $\maybe\monoid$. We also lift the composition $(\mtimes)$ to $\maybe\monoid$. Partial cores help us to build interesting composite RAs from smaller primitives. Notice also that the core of an RA is a strict generalization of the unit that any PCM must provide, since $\mcore{{-}}$ can always be picked as a constant function.  Ralf Jung committed Mar 15, 2016 143 144 \end{enumerate}  Ralf Jung committed Mar 12, 2016 145 146 147  \begin{defn} It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if  Ralf Jung committed Jun 29, 2018 148  $\All \maybe{\melt_\f} \in \maybe\monoid. \mvalFull(\melt \mtimes \maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. \mvalFull(\meltB \mtimes \maybe{\melt_\f})$  Ralf Jung committed Mar 12, 2016 149 150 151  We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. \end{defn}  Robbert Krebbers committed Dec 10, 2017 152 The proposition $\melt \mupd \meltsB$ says that every element $\maybe{\melt_\f}$ compatible with $\melt$ (we also call such elements \emph{frames}), must also be compatible with some $\meltB \in \meltsB$.  Ralf Jung committed Jul 25, 2016 153 Notice that $\maybe{\melt_\f}$ could be $\mnocore$, so the frame-preserving update can also be applied to elements that have \emph{no} frame.  Ralf Jung committed Mar 15, 2016 154 155 Intuitively, this means that whatever assumptions the rest of the program is making about the state of $\gname$, if these assumptions are compatible with $\melt$, then updating to $\meltB$ will not invalidate any of these assumptions. Since Iris ensures that the global ghost state is valid, this means that we can soundly update the ghost state from $\melt$ to a non-deterministically picked $\meltB \in \meltsB$.  Ralf Jung committed Mar 07, 2016 156   Robbert Krebbers committed Dec 10, 2017 157 \subsection{Cameras}  Ralf Jung committed Feb 29, 2016 158 159  \begin{defn}  Robbert Krebbers committed Dec 10, 2017 160  A \emph{camera} is a tuple $(\monoid : \OFEs, \mval : \monoid \nfn \SProp, \mcore{{-}}: \monoid \nfn \maybe\monoid,\\ (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:  Ralf Jung committed Feb 29, 2016 161  \begin{align*}  Robbert Krebbers committed Dec 10, 2017 162 163 164 165 166 167  \All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{camera-assoc} \\ \All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{camera-comm} \\ \All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{camera-core-id} \\ \All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{camera-core-idem} \\ \All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{camera-core-mono} \\ \All \melt, \meltB.& \mval(\melt \mtimes \meltB) \subseteq \mval(\melt) \tagH{camera-valid-op} \\  Ralf Jung committed Dec 08, 2017 168  \All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$n \in \mval(\melt) \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\  Robbert Krebbers committed Dec 10, 2017 169  &\Exists \meltC_1, \meltC_2. \melt = \meltC_1 \mtimes \meltC_2 \land \meltC_1 \nequiv{n} \meltB_1 \land \meltC_2 \nequiv{n} \meltB_2 \tagH{camera-extend} \\  Ralf Jung committed Feb 29, 2016 170  \text{where}\qquad\qquad\\  Robbert Krebbers committed Dec 10, 2017 171 172  \melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{camera-incl} \\ \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{camera-inclN}  Ralf Jung committed Feb 29, 2016 173 174 175  \end{align*} \end{defn}  Robbert Krebbers committed Dec 10, 2017 176 177 178 179 180 This is a natural generalization of RAs over OFEs\footnote{The reader may wonder why on earth we call them cameras''. The reason, which may not be entirely convincing, is that camera'' was originally just used as a comfortable pronunciation of CMRA'', the name used in earlier Iris papers. CMRA was originally supposed to be an acronym for complete metric resource algebras'' (or something like that), but we were never very satisfied with it and thus ended up never spelling it out. To make matters worse, the complete'' part of CMRA is now downright misleading, for whereas previously the carrier of a CMRA was required to be a COFE (complete OFE), we have relaxed that restriction and permit it to be an (incomplete) OFE. For these reasons, we have decided to stick with the name camera'', for purposes of continuity, but to drop any pretense that it stands for something.}.  Ralf Jung committed Mar 10, 2016 181 All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.  Ralf Jung committed Dec 08, 2017 182 183 We define the plain $\mvalFull$ as the limit'' of the step-indexed approximation: $\mvalFull(\melt) \eqdef \All n. n \in \mval(\melt)$  Ralf Jung committed Feb 29, 2016 184   Robbert Krebbers committed Dec 10, 2017 185 \paragraph{The extension axiom (\ruleref{camera-extend}).}  Ralf Jung committed Feb 29, 2016 186 187 188 Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq. The purpose of this axiom is to compute $\melt_1$, $\melt_2$ completing the following square:  Ralf Jung committed Mar 10, 2016 189 % RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so  Ralf Jung committed Feb 29, 2016 190 191 192 193 194 195 196 197 198 199 200 201 202 203 \begin{center} \begin{tikzpicture}[every edge/.style={draw=none}] \node (a) at (0, 0) {$\melt$}; \node (b) at (1.7, 0) {$\meltB$}; \node (b12) at (1.7, -1) {$\meltB_1 \mtimes \meltB_2$}; \node (a12) at (0, -1) {$\melt_1 \mtimes \melt_2$}; \path (a) edge node {$\nequiv{n}$} (b); \path (a12) edge node {$\nequiv{n}$} (b12); \path (a) edge node [rotate=90] {$=$} (a12); \path (b) edge node [rotate=90] {$=$} (b12); \end{tikzpicture}\end{center} where the $n$-equivalence at the bottom is meant to apply to the pairs of elements, \ie we demand $\melt_1 \nequiv{n} \meltB_1$ and $\melt_2 \nequiv{n} \meltB_2$. In other words, extension carries the decomposition of $\meltB$ into $\meltB_1$ and $\meltB_2$ over the $n$-equivalence of $\melt$ and $\meltB$, and yields a corresponding decomposition of $\melt$ into $\melt_1$ and $\melt_2$.  Ralf Jung committed Jul 25, 2016 204 This operation is needed to prove that $\later$ commutes with separating conjunction:  Ralf Jung committed Feb 29, 2016 205 \begin{mathpar}  Ralf Jung committed Jul 25, 2016 206  \axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB}  Ralf Jung committed Feb 29, 2016 207 208 \end{mathpar}  Ralf Jung committed Mar 08, 2016 209 \begin{defn}  Robbert Krebbers committed Dec 10, 2017 210  An element $\munit$ of a camera $\monoid$ is called the \emph{unit} of $\monoid$ if it satisfies the following conditions:  Ralf Jung committed Mar 08, 2016 211  \begin{enumerate}[itemsep=0pt]  Ralf Jung committed Dec 08, 2017 212  \item $\munit$ is valid: \\ $\All n. n \in \mval(\munit)$  Ralf Jung committed Mar 08, 2016 213  \item $\munit$ is a left-identity of the operation: \\  Ralf Jung committed Mar 08, 2016 214  $\All \melt \in M. \munit \mtimes \melt = \melt$  Ralf Jung committed Jul 25, 2016 215  \item $\munit$ is its own core: \\ $\mcore\munit = \munit$  Ralf Jung committed Mar 08, 2016 216 217 218  \end{enumerate} \end{defn}  Robbert Krebbers committed Dec 10, 2017 219 \begin{lem}\label{lem:camera-unit-total-core}  Ralf Jung committed Jul 25, 2016 220 221 222  If $\monoid$ has a unit $\munit$, then the core $\mcore{{-}}$ is total, \ie $\All\melt. \mcore\melt \in \monoid$. \end{lem}  Ralf Jung committed Mar 07, 2016 223 224 \begin{defn} It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if  Ralf Jung committed Dec 08, 2017 225  $\All n, \maybe{\melt_\f}. n \in \mval(\melt \mtimes \maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. n \in\mval(\meltB \mtimes \maybe{\melt_\f})$  Ralf Jung committed Mar 07, 2016 226 227 228 229 230  We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. \end{defn} Note that for RAs, this and the RA-based definition of a frame-preserving update coincide.  Ralf Jung committed Mar 08, 2016 231 \begin{defn}  Robbert Krebbers committed Dec 10, 2017 232  A camera $\monoid$ is \emph{discrete} if it satisfies the following conditions:  Ralf Jung committed Mar 08, 2016 233 234  \begin{enumerate}[itemsep=0pt] \item $\monoid$ is a discrete COFE  Ralf Jung committed Mar 16, 2016 235  \item $\mval$ ignores the step-index: \\  Ralf Jung committed Dec 08, 2017 236  $\All \melt \in \monoid. 0 \in \mval(\melt) \Ra \All n. n \in \mval(\melt)$  Ralf Jung committed Mar 08, 2016 237 238  \end{enumerate} \end{defn}  Robbert Krebbers committed Dec 10, 2017 239 240 Note that every RA is a discrete camera, by picking the discrete COFE for the equivalence relation. Furthermore, discrete cameras can be turned into RAs by ignoring their COFE structure, as well as the step-index of $\mval$.  Ralf Jung committed Mar 07, 2016 241   Robbert Krebbers committed Dec 10, 2017 242 243 \begin{defn}[Camera homomorphism] A function $f : \monoid_1 \to \monoid_2$ between two cameras is \emph{a camera homomorphism} if it satisfies the following conditions:  Ralf Jung committed Mar 08, 2016 244  \begin{enumerate}[itemsep=0pt]  Ralf Jung committed Mar 07, 2016 245  \item $f$ is non-expansive  Ralf Jung committed Nov 23, 2017 246 247 248 249  \item $f$ commutes with composition:\\ $\All \melt_1 \in \monoid_1, \melt_2 \in \monoid_1. f(\melt_1) \mtimes f(\melt_2) = f(\melt_1 \mtimes \melt_2)$ \item $f$ commutes with the core:\\ $\All \melt \in \monoid_1. \mcore{f(\melt)} = f(\mcore{\melt})$  Ralf Jung committed Mar 07, 2016 250  \item $f$ preserves validity: \\  Ralf Jung committed Dec 08, 2017 251  $\All n, \melt \in \monoid_1. n \in \mval(\melt) \Ra n \in \mval(f(\melt))$  Ralf Jung committed Mar 07, 2016 252 253 254 255  \end{enumerate} \end{defn} \begin{defn}  Robbert Krebbers committed Dec 10, 2017 256  The category $\CMRAs$ consists of cameras as objects, and monotone functions as arrows.  Ralf Jung committed Mar 07, 2016 257 \end{defn}  Ralf Jung committed Dec 05, 2016 258 Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\OFEs$.  Ralf Jung committed Mar 09, 2016 259 The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.  Ralf Jung committed Aug 04, 2016 260 %TODO: Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.  Ralf Jung committed Feb 29, 2016 261   Ralf Jung committed Jan 31, 2016 262 263 264 265 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: