<div dir="ltr">I'm trying to prove a basic fact about substitution and failing. What I'd like to prove is that substitution by the identity map is the identity, which should be straightforward. My failed proof is attached. Questions:<div><br></div><div>1. Why does Agda complain about my extensionality postulate? How do I fix it?</div><div><br></div><div>2. Is there a way to complete the proof without assuming extensionality?</div><div><br></div><div>Many thanks for your help. This group is invaluable! The New Year is a good time to take a moment to express my thanks to you all, both for your work in Agda (and related topics) and for your help.</div><div><br></div><div>Go well, -- P</div><div><br></div><div><br></div><div><br></div><div><br clear="all"><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div></div></div>