[Agda] (¬_ ∘ P) Respects

Sergei Meshveliani mechvel at botik.ru
Mon Feb 17 15:53:01 CET 2014


(Suggestions and bug tracker on Standard library is on the Web.
But what is, please, the appropriate place to ask about  
Standard library features? to _discuss_ them?
)

People,
I need proofs for things like

  P Respects _≈_ → (¬_ ∘ P) Respects _≈_,
       
  x ≈ x' -> y ≈ y' -> x ∤ y -> x' ∤ y'   (for a generic "not divides").

And 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?

Thanks,

------
Sergei



More information about the Agda mailing list