[Agda] `Pointwise' over Setoid

[Sergei Meshveliani]

Dear Standard library developers,

(I am sorry, if this was discussed earlier)

Standard library provides map-cong, map-id, map-compose
as related to the propositional equality _≡_.
But the case of List over Setoid is highly usable.

And I suggest this:

-----------------------------------------------------------------------
module OfMapsToSetoid {α β β=} (A : Set α) (S : Setoid β β=)
where
open Setoid S using (_≈_)
renaming (Carrier to B; reflexive to ≈reflexive;
refl to ≈refl; sym to ≈sym; trans to ≈trans)
infixl 2 _≈∘_

_≈∘_ : Rel (A → B) _
f ≈∘ g = (x : A) → f x ≈ g x

≈∘refl : Reflexive _≈∘_
≈∘refl _ = ≈refl

≈∘reflexive : _≡_ ⇒ _≈∘_
≈∘reflexive {x} refl = ≈∘refl {x}

≈∘sym : Symmetric _≈∘_
≈∘sym f≈∘g = ≈sym ∘ f≈∘g

≈∘trans : Transitive _≈∘_
≈∘trans f≈∘g g≈∘h x = ≈trans (f≈∘g x) (g≈∘h x)

≈∘Equiv : IsEquivalence _≈∘_
≈∘Equiv = record{ refl = \{x} → ≈∘refl {x}
; sym = \{x} {y} → ≈∘sym {x} {y}
; trans = \{x} {y} {z} → ≈∘trans {x} {y} {z} }

≈∘Setoid : Setoid (α ⊔ β) (α ⊔ β=)
≈∘Setoid = record{ Carrier = A → B
; _≈_ = _≈∘_
; isEquivalence = ≈∘Equiv }

lSetoid = ListPoint.setoid S

open Setoid lSetoid using () renaming (_≈_ to _=l_; refl to =l-refl)

gen-map-cong : {f g : A → B} → f ≈∘ g → (xs : List A) →
map f xs =l map g xs
gen-map-cong _ [] = =l-refl
gen-map-cong f≈∘g (x ∷ xs) = (f≈∘g x) ∷p (gen-map-cong f≈∘g xs)

...
----------------------------------------------------------


Regards,

------
Sergei

[Matthew Daggitt]

Hi Sergei,
Can you open standard library suggestions like this on the stdlib git
repository? Probably a better place to discuss them.
Thanks,
Matthew

Post by Sergei Meshveliani
Dear Standard library developers,
(I am sorry, if this was discussed earlier)
Standard library provides map-cong, map-id, map-compose
as related to the propositional equality _≡_.
But the case of List over Setoid is highly usable.
-----------------------------------------------------------------------
module OfMapsToSetoid {α β β=} (A : Set α) (S : Setoid β β=)
where
open Setoid S using (_≈_)
renaming (Carrier to B; reflexive to ≈reflexive;
refl to ≈refl; sym to ≈sym; trans to ≈trans)
infixl 2 _≈∘_
_≈∘_ : Rel (A → B) _
f ≈∘ g = (x : A) → f x ≈ g x
≈∘refl : Reflexive _≈∘_
≈∘refl _ = ≈refl
≈∘reflexive : _≡_ ⇒ _≈∘_
≈∘reflexive {x} refl = ≈∘refl {x}
≈∘sym : Symmetric _≈∘_
≈∘sym f≈∘g = ≈sym ∘ f≈∘g
≈∘trans : Transitive _≈∘_
≈∘trans f≈∘g g≈∘h x = ≈trans (f≈∘g x) (g≈∘h x)
≈∘Equiv : IsEquivalence _≈∘_
≈∘Equiv = record{ refl = \{x} → ≈∘refl {x}
; sym = \{x} {y} → ≈∘sym {x} {y}
; trans = \{x} {y} {z} → ≈∘trans {x} {y} {z} }
≈∘Setoid : Setoid (α ⊔ β) (α ⊔ β=)
≈∘Setoid = record{ Carrier = A → B
; _≈_ = _≈∘_
; isEquivalence = ≈∘Equiv }
lSetoid = ListPoint.setoid S
open Setoid lSetoid using () renaming (_≈_ to _=l_; refl to =l-refl)
gen-map-cong : {f g : A → B} → f ≈∘ g → (xs : List A) →
map f xs =l map g xs
gen-map-cong _ [] = =l-refl
gen-map-cong f≈∘g (x ∷ xs) = (f≈∘g x) ∷p (gen-map-cong f≈∘g xs)
...
----------------------------------------------------------
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda