(¬_ ∘ P) Respects

[mechvel]

Consider proofs for things like

  P Respects _≈_ → (¬_ ∘ P) Respects _≈_,

  x ≈ x' -> y ≈ y' -> x ∤ y -> x' ∤ y'   (for a generic "not divides").

I write for this:

  ¬respects : ∀ {α α= β} →  {A : Set α} → (_≈_ : Rel A α=) → Symmetric _≈_ →
                                           (P : A → Set β) → 
                                           P Respects _≈_ → (¬_ ∘ P) Respects _≈_
  ...
  ¬respects = ...

But has Standard library something for this?
If not, then needs it to have?

[mechvel]

I would rename ¬respects to respectsFor¬

[MatthewDaggitt]

Added in 22ed935