I skimmed the PDF of the book but am drawing blank as to its connection to an application. Perhaps it's used for verification of concepts, similar to how formal methods in CS (e.g. TLA+) are used to conceptually check algorithms?
- https://softwareengineering.stackexchange.com/questions/2623...
- https://www.reddit.com/r/haskell/comments/6nxgkc/similaritie...
- https://bartoszmilewski.com/category/homotopy-type-theory/
From the software engineering point of view a type is something of which you can say whether something is a member of the type. And the same thing can be set about sets.
Even within "Set Theory" (as an umbrella term), there are several axiomatizations of sets that define in different ways what a set is, how sets come into existence, what it means for an element to belong to a set, and what are the allowed ways to conclude that it does or does not.
The link posted in a sibling comment by @empath75 goes into more detail.