Readability of the Yoneda encoding and of the forcing modality

[herbelin]

Hi, when using Forcing Definition, one sees things like:

forall q, (forall R : Obj, Hom p R -> Hom q R)

Generalizing the example given in the test file, a forcing modality notation could also be obtained:

Notation "p ≤ q" := (forall (R : Obj), Hom p R -> Hom q R) (at level 70).
Definition Hom_force (p:Obj) (P:Obj -> Type) := forall q, q ≤ p -> P q.
Notation "▢_ p P" := (Hom_force p (fun p => P)) (at level 200, p ident, format "▢_ p  P").

The drawback is to have to introduce an indirection constant Hom_force.