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

[Conor McBride]

Hi Phil

> On 3 Jan 2022, at 16:24, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> 
> 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?

For a start, Agda's moaning about the implicits that it can't infer in your with-expression.
No type is pushed in to with-expressions, so there's nothing that will determing the
missing information. I'm not sure with is what you need, but even if you were to use
rewrite, the same would pertain. However...

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

...you might consider making Henry Ford's extensional generalization of your goal. Any
substitution will *behave* as the identity on terms if it *behaves* like the identity on
variables, regardless of whether it's your *favourite* identity substitution. That statement
pushes readily under lambda, because it talks about "any substitution", leaving you with
an "as long as it behaves like the identity" condition to discharge.

Cheers

Conor

> 
> 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/
> 
> <Substitution.lagda.md>The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda