About Logic Interview with Emily Riehl
51:47 Question about set theory vs type theory. I don't know that there was ever a split. The impression I get is that type theory was developed as a way to reason formally about set theory, and then that structure turned out to fit well with constructive mathematics and intuitionistic logic. So the people who study type theory tend to be constructivists. See About Logic - Is Mathematics a Story? and Andrej Bauer - Models of intuitionism and computability . Subscribe to About Logic . Thorsten might have a chapter on this in his book, it's all about how people who can't count can decide whether or not two sets are the same size: Subscribe to Thorsten Altenkirch .