search

CoqHott / coq-forcing

A plugin for Coq that implements the call-by-name forcing translation
12 stars 3 forks source link

Readability of the Yoneda encoding and of the forcing modality #5

Open herbelin opened 3 years ago

herbelin commented 3 years ago

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.