Citing your link: > At this point, however, you may be feeling that type theory sounds very complicated. Lots of different ways to form types, each with their

Citing your link: > At this point, however, you may be feeling that type theory sounds very complicated. Lots of different ways to form types, each with their own rules for forming elements? Where is the simplicity and intuitiveness that we expect of a foundational theory? It's just not there, Mike. Type theory is neither simple nor intuitive, and it doesn't make a good foundation. Type theory certainly has advantages, but it gets lost in esoteric texts like Mike's. There are two simple advantages over set theory within first-order logic: general variable binding, and that things are kept separate, for example that a boolean is not a number. Now, how to do general variable binding without static types I show in [0]. How to still keep things separate, in [1]. All without having to divide the mathematical universe into static types.