[Agda] The joys and sorrows of abstraction

[Martin Escardo]

On 16/05/18 22:55, apostolis.xekoukoulotakis at gmail.com wrote:
> This is really scary, for good reason. It seems that we are in a better 
> position now than a few years ago.
> 
> I do remember as an undergraduate, thinking that all I need is to start 
> from the fundamentals of Mathematics and then prove all of the rest.
> Then , I found that the fundamentals were full of paradoxes.
> https://en.wikipedia.org/wiki/Foundations_of_mathematics#Foundational_crisis

Agda is an incarnation of both established type theories and frontier 
research on possible new type theories, and it is good that things are 
like this, because researchers can use it for experimentation.

But some other researchers would like to use Agda to work with 
established type theories.

It is good that Agda has some seat-belts such as --exact-split, --safe, 
and --without-K, for that purpose.

Further seat-belts would be welcome.

The point I was making was not about scariness but about awareness. If 
you use a feature beyond your type-theory expertise, consider whether 
this feature is well established, but unknown to you, or something 
experimental and perhaps not well-defined.

Martin