feat(FreeM): relate indexed and polynomial free monads

[dtumad]

Adds PFunctor.ofFamily F, whose shapes pair an answer type ι with an operation F ι, and an equivalence Cslib.FreeM F α ≃ (PFunctor.ofFamily F).FreeM α. Both directions are monad morphisms and commute with foldFreeM and liftM, so programs over indexed effects can use the polynomial API without changing Cslib.FreeM, at the cost of raising the shape universe to max (u + 1) v. The same polynomial appears in PolyFun as Context.toPFunctor.

AI agents were used to adapt VCVio definitions/proofs to Cslib definitions and conventions.

[SamuelSchlesinger]

Can you motivate this a bit more for me?

[dtumad]

Can you motivate this a bit more for me?

We currently have both PFunctor.FreeM and plain FreeM, that are fundamentally the same object but with different universe levels, but both can represent well-founded computations with oracle access. This is just to have a bridge for later lemmas to move between them to re-use an existing proof when it is written with one in particular language.

I guess in general a IsFreeM F M type-class that asserts the universal property could also accomplish something similar.

[SamuelSchlesinger]

I had some branches where I unified these in some way or another, I can also dig them up. It might have been the class approach, I forget.