[Agda] termination by contradiction

[Dmytro Starosud]

Markov axiom (for Nat) doesn't leed to a total excluded third.
Constructive logic together with Markov axiom (for Nat) is still
constructive.
Here is really nice course
<http://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx#folderID=%2207756bb0-b872-4a4a-95b1-b77ad206dab3%22>
(and book <http://homotopytypetheory.org/book/>) explaining in very deep
details all that stuff with constructive vs classic vs whatever.

Dmytro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140701/e08e2324/attachment.html