Constructive and Non-Constructive Proofs in Agda (Part 3): Playing with Negation

In the previous post, we briefly introduced the reader to dependently typed programming and theorem proving in Agda. Now we present an empty type to work with constructive negation. We discuss Marko…...