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>