[Agda] Q: Equational Reasoning

[Nils Anders Danielsson]

On 2009-05-27 20:25, Andrej Bauer wrote:
> I am trying to wrap my brain around this. It would greatly help if
> someone were kind enough to show how this is used to prove f(x,g(a)) =
> f(x,g(b)) from a = b. and what if we used setoids and we only knew
> that a and b are equivalent, and that f and g respect the
> equivalences?

Second part:

  open import Relation.Binary

  module Example (S : Setoid) where

  open Setoid S

  lemma : ∀ {f g a b x} →
          f Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_ →
          g Preserves _≈_ ⟶ _≈_ →
          a ≈ b → f x (g a) ≈ f x (g b)
  lemma f-pres g-pres a≈b = f-pres refl (g-pres a≈b)

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.