A common use case is to only consider, say, Hausdorff spaces. It'd be slick to have the ability to filter out all non-T_2 spaces, and to appropriately filter the appearance of theorems. For people in the T_2 world, "paracompact if and only if fully normal" is correct, but assuming no separation axioms the theorem is actually "paracompact+T_2 if and only if fullyNormal+T_1" (or fullyT_4). Or maybe I'm only considering Lindelof T_1 spaces: "Metrizable if and only if regular and second countable" works in that context, although strictly speaking it's "Metrizable+Lindelof if and only if T_3+SecondCountable".
A common use case is to only consider, say, Hausdorff spaces. It'd be slick to have the ability to filter out all non-T_2 spaces, and to appropriately filter the appearance of theorems. For people in the T_2 world, "paracompact if and only if fully normal" is correct, but assuming no separation axioms the theorem is actually "paracompact+T_2 if and only if fullyNormal+T_1" (or fullyT_4). Or maybe I'm only considering Lindelof T_1 spaces: "Metrizable if and only if regular and second countable" works in that context, although strictly speaking it's "Metrizable+Lindelof if and only if T_3+SecondCountable".