[Agda] A stupid question to start off the New Year

[Philip Wadler]

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:

1. Why does Agda complain about my extensionality postulate? How do I fix
it?

2. Is there a way to complete the proof without assuming extensionality?

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.

Go well, -- P




.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220103/25fbed47/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Substitution.lagda.md
Type: text/markdown
Size: 3481 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220103/25fbed47/attachment.bin>
-------------- next part --------------
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.