write hajimeni
A proof of Yoneda lemma (outcome of Agda Implementors Meeting XIV), by Yoshiki Kinoshita.