Add global filters

[jamesdabbs]

For now, let users express "I only ever care about T_2 spaces". Eventually this should expand to let the user specify which axiom set they are working in.

[StevenClontz]

We'll need an Axiom model for the secondary goal.

---
name: Axiom of Constructability
slug: constructability
references: [whatever format we use, points to a textbook/article defining it explicitly]
implies:
    - list of axioms it implies (e.g. CH)
---

The assertion \(V=L\) that every set is constructable.

Then we can let users add a list of assumptions to spaces and theorems, which are ignored in the viewer unless the axiom is toggled. Of course, spaces/theorems without axioms should exist/hold under ZFC, the "default" theory used by most of my peers.

[jamesdabbs]

Axioms are going to be tricky to model, because toggling an axiom doesn't just hide / show stuff, but will change the value of some traits. So we'll either need to store parallel copies of the trait table that you swap between as you change axiom sets, or do more recomputing on the fly than we're currently doing. It's feasible, but it'll be some work.

[StevenClontz]

Well, I'd imagine we'd add a

required_axioms:
    - A123456

list of axioms on each space/trait that requires those axioms. If no axioms are assumed, these are ignored by the viewer, but they appear when sufficient axioms are assumed. Actually, better yet, they appear as "Paracompact (assuming Axiom of Constructability)". Which means we might also have "~Paracompact (assuming Martin's Axiom)".

All this said, I'm happy with saying in ZFC land for a while, and working with topics in general topology that don't rely heavily on independence results.