His MR changes cFunctor, rFunctor and 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.
Motivation
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(Where X will be the recursive occurrence for iProp).
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.
Documentation
Apart from this change, I tried to write some documentation, explaining the (updated) functor infrastructure.