[Agda] Why dependent type theory?

[Steven Shaw]

I really enjoyed the following video with Thorsten Altenkirch which speaks
informally about Type Theory and Set Theory:

  https://youtu.be/qT8NyyRgLDQ

The follow-up video has some further commentary https://youtu.be/SknxggwRPzU
.

Since you're writing a thesis with a focus on Coq, I'm sure you
understand the details. You might enjoy the informal distinctions between
Type Theory and Constructive Mathematics vs Set Theory and Classical Logic.

I would summarise that Constructive Mathematics (using Type Theory) is
better because it provides more confidence in your proofs.

Best,
Steve.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200304/52a63817/attachment.html>