[Agda] A philosophical question on absurd.

[Peter Hancock]

On 28/08/2020 16:08, Thorsten Altenkirch wrote:
> from false follows everything

It might be (a little) better to say that *anything* whatever holds of an inhabitant of False.

With a universe, or large elimination we can define a type-valued function
Anything(x) : Type (x : False).
Then the "strong" eliminator for False gives us
(Pi x : False) Anything(x)

Hank