Dan

A little work on equalizers in Agda : http://web.student.chalmers.se/~danr/Equalizer/Equalizer.html
Some about preimage : http://web.student.chalmers.se/~danr/Equalizer/Preimage.html
Free monoids in Agda : http://web.student.chalmers.se/~danr/FreeMonoid/FreeMonoid.html