> How is this useful? It seems as though we're talking about a `filter` at the type level. Whatever properties we might like to prove about a random set of ty

> How is this useful? It seems as though we're talking about a `filter` at the type level. Whatever properties we might like to prove about a random set of types would seem more easily expressed in a positive, rather than negative, mode.