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.