Commit 9fb6751e authored by Dan Frumin's avatar Dan Frumin
Browse files

Add a `Proper` instance for ccompose.

parent b123b1a4
......@@ -604,6 +604,9 @@ Infix "◎" := ccompose (at level 40, left associativity).
Global Instance ccompose_ne {A B C} :
NonExpansive2 (@ccompose A B C).
Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
Global Instance ccompose_proper {A B C} :
Proper (() ==> () ==> ()) (@ccompose A B C).
Proof. apply ne_proper_2; apply _. Qed.
(* Function space maps *)
Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment