Traditionally, in Computer Science, sets are assumed to be the basis of a type theory, together with Boolean logic. In this version of type theory, we do not need sets or Boolean logic; intuitionism is enough ("no principle of excluded middle required"). The underlying math is Topos Theory, but you are not required to be even aware of its existence. The theory is described using diagrams, not the traditional (and tricky) deduction rules. The resulting theory turns out to have dependent types. A simple "real-life" example or two will illustrate all this.