[Agda] Path to success with Agda?

[Peter Hancock]

On 29/08/2022 22:13, Ignat Insarov wrote:
> I have no problem learning Type Theory by itself, since there are great books
> out there. Σ types, eliminators, you name it — no problem. My problem seems to
> be rooted in the technical difficulties that are specific to Agda — the pattern
> matching algorithm and the ill-typed with-abstractions.

> I have no problem learning Type Theory by itself, since there are great books
> out there. Σ types, eliminators, you name it — no problem. My problem seems to
> be rooted in the technical difficulties that are specific to Agda — the pattern
> matching algorithm and the ill-typed with-abstractions.

There are things in Agda, connected with pattern-matching, that are not in
"Type Theory" (as in "you name it, no problem").

In my experience these are usually subtly connected with the empty type
(which has its own eliminator).

I've never entirely understood "with-abstraction", although it makes some superficial sense,
but have tried to stick with original Martin-Lof type theory.

It would be good to sort this out, once and for all, whatever the outcome.

Thank you for your eloquent message!

P