<div dir="ltr">Hi Sergei,<div> Can you open standard library suggestions like this on the stdlib git repository? Probably a better place to discuss them.</div><div>Thanks,</div><div>Matthew</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Mar 24, 2018 at 10:33 AM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Standard library developers,<br>
<br>
(I am sorry, if this was discussed earlier)<br>
<br>
Standard library provides  map-cong, map-id, map-compose<br>
as related to the propositional equality _≡_.<br>
But the case of  List over Setoid  is highly usable.<br>
<br>
And I suggest this:<br>
<br>
------------------------------<wbr>------------------------------<wbr>-----------<br>
module OfMapsToSetoid {α β β=} (A : Set α) (S : Setoid β β=)<br>
 where<br>
 open Setoid S using (_≈_)<br>
               renaming (Carrier to B; reflexive to ≈reflexive;<br>
                         refl to ≈refl; sym to ≈sym; trans to ≈trans)<br>
 infixl 2 _≈∘_<br>
<br>
 _≈∘_ :  Rel (A → B) _<br>
 f ≈∘ g =  (x : A) → f x ≈ g x<br>
<br>
 ≈∘refl : Reflexive _≈∘_<br>
 ≈∘refl _ = ≈refl<br>
<br>
 ≈∘reflexive : _≡_ ⇒ _≈∘_<br>
 ≈∘reflexive {x} refl =  ≈∘refl {x}<br>
<br>
 ≈∘sym : Symmetric _≈∘_<br>
 ≈∘sym f≈∘g =  ≈sym ∘ f≈∘g<br>
<br>
 ≈∘trans : Transitive _≈∘_<br>
 ≈∘trans f≈∘g g≈∘h x =  ≈trans (f≈∘g x) (g≈∘h x)<br>
<br>
 ≈∘Equiv : IsEquivalence _≈∘_<br>
 ≈∘Equiv = record{ refl  = \{x}         → ≈∘refl {x}<br>
                 ; sym   = \{x} {y}     → ≈∘sym {x} {y}<br>
                 ; trans = \{x} {y} {z} → ≈∘trans {x} {y} {z} }<br>
<br>
 ≈∘Setoid : Setoid (α ⊔ β) (α ⊔ β=)<br>
 ≈∘Setoid = record{ Carrier       = A → B<br>
                  ; _≈_           = _≈∘_<br>
                  ; isEquivalence = ≈∘Equiv }<br>
<br>
 lSetoid = ListPoint.setoid S<br>
<br>
 open Setoid lSetoid using () renaming (_≈_ to _=l_; refl to =l-refl)<br>
<br>
 gen-map-cong : {f g : A → B} → f ≈∘ g → (xs : List A) →<br>
                                                    map f xs =l map g xs<br>
 gen-map-cong _    []       =  =l-refl<br>
 gen-map-cong f≈∘g (x ∷ xs) =  (f≈∘g x) ∷p (gen-map-cong f≈∘g xs)<br>
<br>
 ...<br>
------------------------------<wbr>----------------------------<br>
<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>