It is impossible to ignore the set theoretic type aspects, because the whole foundation of strong arrows is based on being able to negate a type. If I don't exp

It is impossible to ignore the set theoretic type aspects, because the whole foundation of strong arrows is based on being able to negate a type. If I don't explain the set theory bits, then the rest of the article falls apart. I could perhaps rearrange some of those sections but that doesn't change my main argument: the type system is not being designed for type theoretic people. At best, you could say the _article_ focus too much on theory, rather than on the practical bits.