[Agda] a tutorial for proof by coinduction

[Pierre Lescanne (en)]

Does there exist a tutorial for proofs by coinduction ?

I am looking for something a little like Chapter 13 of the Coq'Art ?

-- 
Regards,

---------------------------
Pierre Lescanne (Emeritus Professor)
LIP / École normale supérieure de Lyon
46 allée d'Italie
69364 LYON Cedex 07, France
tél: +33 6 85 70 94 31
http://perso.ens-lyon.fr/pierre.lescanne/
---------------------------