diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex index b8d55d0fd6249636244263d094b789a78286630c..c774af1077f8aaf39a7cfc3ccbc74535f21e2e44 100644 --- a/docs/ghost-state.tex +++ b/docs/ghost-state.tex @@ -174,7 +174,7 @@ The purpose of this section is to describe how we solve these issues. \paragraph{Picking the resources.} The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources. -To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs^\op \times \OFEs \to \CMRAs)_{i \in \mathcal{I}}$. +To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs^\op \times \COFEs \to \CMRAs)_{i \in \mathcal{I}}$. (This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.) From this, we construct the bifunctor defining the overall resources as follows: