Type Theory and the Bonrock Tarski Paradox

type theory recently came up as an alternative way to look at the underlying construction of mathematics. The most of math today works on the foundations of set theory, which is just like categorizing objects by sets. Some of these axioms can lead to very strange results. Have you heard of the Bonrock Tarski paradox? No.