[Agda] exercice of Peter Dybjer

[Jesper Cockx]

Hi Michel,

Here's a hint for sym: starting from `x ≡ y`, if you can prove that `P z =
z ≡ x` holds for `z = x`, then you can use `subst` to prove that it also
holds for `z = y`. For `trans`, there is a similar trick but now you need
to choose `P` to be an implication between two identity types.

-- Jesper



On Sun, Mar 22, 2020 at 12:38 PM Michel Levy <michel.levy.imag at free.fr>
wrote:

> In the paper AgdaLectureNotes2018
> <http://www.cse.chalmers.se/~peterd/papers/AgdaLectureNotes2018.pdf> of
> Peter Dybjer, there is this exercise page 19
>
> Exercise: prove symmetry and transitivity using subst but without using
> pattern matching!
>
> I don't find the solution, can you help me to solve it ?
> --
> courriel : michel.levy.imag at free.fr
> mobile : 06 59 13 42 53
> web : michel.levy.imag.free.fr
> _______________________________________________
> 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/20200322/9b4017dd/attachment.html>