# When should ==\> be used over ++\> for morphisms?

**URL:** <https://discourse.rocq-prover.org/t/when-should-be-used-over-for-morphisms/2796>\
**Category:** Using Rocq\
**Created:** [August 16, 2025, 9:36pm UTC](https://discourse.rocq-prover.org/t/when-should-be-used-over-for-morphisms/2796 "2025-08-16T21:36:52Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![ia0](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ia0/32/1104_2.png) [@ia0](https://discourse.rocq-prover.org/u/ia0)\
**Post date:** [August 16, 2025, 9:36pm UTC](https://discourse.rocq-prover.org/t/when-should-be-used-over-for-morphisms/2796/1 "2025-08-16T21:36:52Z")

</div>

I’m trying to understand why the notation `R ==> S` has the same definition as `R ++> S`.

I would naively expect it to have a definition like `(fun x y => R x y \/ R y x) ++> S`, since according to the [documentation](https://rocq-prover.org/doc/V9.0.0/refman/addendum/generalized-rewriting.html#coq:tacn.setoid_rewrite:~:text=The%20special%20arrow%20%3D%3D%3E%20is%20used%20in%20signatures%20for%20morphisms%20that%20are%20both%20covariant%20and%20contravariant.):

> The special arrow `==>` is used in signatures for morphisms that are both covariant and contravariant.

I understand that for symmetric relations the distinction doesn’t matter. But for relations that are not symmetric, I believe it does.

When/why would one use `==>` over `++>`?

Here’s a development to illustrate what my question:

```coq
From Stdlib Require Import Setoid Morphisms.

(* Simple pre-order (implication on truth values). *)
Inductive P : Set := F | T.
Inductive R : P -> P -> Prop :=
| RFF : R F F
| RFT : R F T
| RTT : R T T
.
Lemma R_refl : reflexive P R.
Proof. intros [|]; auto using R. Qed.
Lemma R_not_sym : ~ (symmetric P R).
Proof. intro H; specialize (H F T RFT); inversion H. Qed.
Lemma R_trans : transitive P R.
Proof. intros [|] [|] [|]; auto using R. Qed.

(* Register the relation. *)
Add Relation P R
  reflexivity proved by R_refl
  transitivity proved by R_trans
  as pr.

(* Simple co- and contra-variant morphism (constant function). *)
Definition f (_ : P) : P := F.

Section fails.

  (* Register the morphism as co- and contra-variant. *)
  Add Morphism f with signature R ==> R as fm.
  (* But somehow only prove the co-variant part. *)
  Proof. intros; exact RFF. Qed.

  (* Co-variance works as expected. *)
  Goal forall x y, R x y -> R (f x) (f y).
  Proof. intros x y H; rewrite H; reflexivity. Qed.

  (* Contra-variance does not work (as expected?). *)
  Goal forall x y, R y x -> R (f x) (f y).
  Proof.
    intros x y H.
    (* Not sure how to read the error (if it expects symmetry or a missing morphism). *)
    Fail rewrite H.
  Abort.

End fails.

Section works.

  (* Register the morphism as co- and then contra-variant. *)
  Add Morphism f with signature R ++> R as fmp.
  Proof. intros; exact RFF. Qed.
  Add Morphism f with signature R --> R as fmn.
  Proof. intros; exact RFF. Qed.

  (* Co-variance still works as expected. *)
  Goal forall x y, R x y -> R (f x) (f y).
  Proof. intros x y H; rewrite H; reflexivity. Qed.

  (* Contra-variance now also works as expected. *)
  Goal forall x y, R y x -> R (f x) (f y).
  Proof. intros x y H; rewrite H; reflexivity. Qed.

End works.

Section naive.

  (* Define ==> as being both co- and contra-variant. *)
  Definition or_flip {T} (R : relation T) : relation T := fun x y => R x y \/ R y x.
  Notation "R ==> S" := (respectful (or_flip R) S) : signature_scope.

  (* Prove the morphism is both co- and contra-variant. *)
  Lemma m : Proper (R ==> R) f.
  Proof. intros x y _; exact RFF. Qed.

  (* Co-variance works using the left side of [or_flip]. *)
  Goal forall x y, R x y -> R (f x) (f y).
  Proof. intros x y H; apply m; left; exact H. Qed.

  (* Contra-variance works using the right side of [or_flip]. *)
  Goal forall x y, R y x -> R (f x) (f y).
  Proof. intros x y H; apply m; right; exact H. Qed.

End naive.

```

---

<div class="post-metadata">

**Author:** ![ia0](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ia0/32/1104_2.png) [@ia0](https://discourse.rocq-prover.org/u/ia0)\
**Post date:** [August 20, 2025, 2:00pm UTC](https://discourse.rocq-prover.org/t/when-should-be-used-over-for-morphisms/2796/2 "2025-08-20T14:00:38Z")

</div>

Actually, it’s possible to register the morphism a single time and still achieve both co- and contra-variance (this solution thus scales with the number of parameters to the morphism), by registering `R` and `flip R` as sub-relations of `or_flip R`. This is however twice slower to rewrite as registering the morphism twice.

```coq
Section works2.

  (* Define ==> as being both co- and contra-variant. *)
  Definition or_flip {T} (R : relation T) : relation T := fun x y => R x y \/ R y x.
  Notation "R ==> S" := (respectful (or_flip R) S) : signature_scope.

  (* Register R and flip R as subrelations of (or_flip R). *)
  Instance sub_or_flip {A} (R : relation A) : subrelation R (or_flip R).
  Proof. intros x y H; left; exact H. Qed.
  Instance sub_flip_or_flip {A} (R : relation A) : subrelation (flip R) (or_flip R).
  Proof. intros x y H; right; exact H. Qed.

  (* Register the morphism as co- and contra-variant. *)
  Add Morphism f with signature R ==> R as fm.
  Proof. intros; exact RFF. Qed.

  (* Co-variance works. *)
  Goal forall x y, R x y -> R (f x) (f y).
  Proof. intros x y H; rewrite H; reflexivity. Qed.

  (* Contra-variance works. *)
  Goal forall x y, R y x -> R (f x) (f y).
  Proof. intros x y H; rewrite H; reflexivity. Qed.

Reset works2.

```

(Note that all sections were supposed to be closed by `Reset` instead of `End` in the initial post, but I can’t edit it. This doesn’t change the results.)