[Agda] `Pointwise' over Setoid

[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

On Sat, Mar 24, 2018 at 10:33 AM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180324/02e5a475/attachment.html>