His MR changes
urFunctor to be functors from COFEs to OFEs, cameras, respectively unital cameras. Before they were functors that took mere OFEs. This is fully backwards compatibly, since in the end of the day, we always instantiate the functor with
iPreProp which is a COFE.
This change is useful if one wants to construct recursive ghost state, e.g. in work with @jihgfee we basically want to have ghost state that contains streams of
iProp, to model session types in a semantic way. For that, we instantiate Iris with something akin to the functor:
F(X) := μ Y. ▶ X ∗ ▶ Y
X will be the recursive occurrence for
In order to constructor the inner fixpoint,
μ Y. ▶ X ∗ ▶ Y, we use the COFE solver. However, for that to work, we need that
X to be a COFE, which we do not get with the current functor infrastructure. This MR fixes that.
Apart from this change, I tried to write some documentation, explaining the (updated) functor infrastructure.