Clarify set of classes related to fmap

[YaZko]

The current axiomatization requires early on 6 classes related to fmap and respectively sum and product types: FmapFst, FmapSnd, RelProd, FmapInl, FmapInr, RelSum.

First remark: one could expect a more general proof rule about fmap, explaining once and for all how computations defined as fmaps can be proven related. Consider to this end the following relation that takes the image of a relation by a pure function:

Variant fmapR {A1 A2 B1 B2: Type}
        (f : A1 -> B1)
        (g : A2 -> B2)
        (RA : relationH A1 A2) : relationH B1 B2 :=
    | fmapR_build a1 a2 : RA a1 a2 -> fmapR f g RA (f a1) (g a2).

And hence the single “unifying” well-formedness condition for fmap stating that if two computations have a relation as post, then their fmaps have the image of the relation by the functions as post:

  Class FmapEQmR : Prop :=
    fmap_eqmr :
      forall {A1 A2 B1 B2: Type}
        (f : A1 -> B1)
        (g : A2 -> B2)
        (RA : relationH A1 A2)
        (m1 : m A1) (m2: m A2),
        eqmR RA m1 m2 ->
        eqmR (fmapR f g RA) (f <$> m1) (g <$> m2).

Assuming that eqmR is monotonous (Proper_eqmR_mono), one can derive generically from FmapEQmR the four "forward" rules FmapFst, FmapSnd, FmapInl and FmapInr.

Second remark: I do not see a similar generalization for the backward rules RelProd and RelSum, they seem to have a different status.

Third remark: as things are defined currently, we do not say anything about arbitrary Functor, but define things specifically against the monadic fmap instance. And for this instance, assuming the Proper_bind and RetFinal properties, we can simply derive generically the FmapEQmR instance: hence as things are currently setup, FmapFst, FmapSnd, FmapInl and FmapInr could be simply proven rather than required.

Finally, we should see how things relate to FmapInv and FmapInvRet as well.