[Agda] Why dependent type theory?

Steven Shaw steven at steshaw.org
Tue Mar 3 23:43:41 CET 2020


An additional advantage of Type Theory is that it maintains the abstraction
barrier, whereas, in Set Theory, you can look inside to see how your
mathematical objects are encoded as sets.

>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200304/910e4614/attachment.html>


More information about the Agda mailing list