[Agda] With and the inspect idiom

[Conor McBride]

Hi Shin

You're entirely right. At some point in the
evolution of with as an unimplemented feature
of Epigram, we planned to support notations

   with blah   -- as usual

   with q : x = blah  -- naming both the
                      -- new pattern var x
                      -- abstracting blah
                      -- and the proof q
                      -- that x is blah

Of course, that relies on a hard-wired notion
of equality, which is a great way to start a
fight.

But it's not what I would do any more. Given
proof-irrelevance, (I claim) it becomes
reasonable just to add (a proof of) the
equation to the context whenever "with" is
used. However, that's just a particular
notational spin on the with+equation idea.

The essence of the idea is that the
with-expression (e : E) satisfies some
predicate P. I mean that we have some

   p : P e

and we would like to transform a problem

   ?0 : T e

to a problem

   ?1 : (x : E) -> P x -> T x

We may clearly take ?0 := ?1 e p and
carry on.

Perhaps there could be some notation
supporting this in general, which might
then be neutral with respect to people's
equality-related preferences.

But in the meantime, I suggest that we hold
a competition for the cheapest hack to
simulate with+equation. Two-with-and-trans
is a good start!

All the best

Conor