Two-open one-closed topology as a limit

Stream: maths

[Robert Maxton]

As part of proving that (relative) CW complexes are T2, I've co-opted ncatlab's categorification of the concept, defining

inductive Discrete2 : Type u where | zero | one
instance : TopologicalSpace Discrete2 := ⊥
instance : DiscreteTopology Discrete2 := ⟨rfl⟩

inductive O2C1 : Type u where | left | zero | right
instance : TopologicalSpace O2C1 := generateFrom {{O2C1.left}, {O2C1.right}}

and proving that a space X is T2 iff every mono of Discrete2 ⟶ X extends through a X ⟶ of O2C1.

[Aaron Liu]

Discrete2 is just Bool, right?

[Robert Maxton]

However, using this definition requires, obviously, a lot of creating morphisms into O2C1 out of disjoint open sets. And I do have a reasonably convenient way of doing that... but it's very set-theoretic, taking explicit IsOpen s, IsOpen t, Disjoint s t, and it feels silly doing that if I already have those sets represented as morphisms anyway

[Aaron Liu]

well, ULift.{u} Bool

[Robert Maxton]

Almost, yeah. The ULift was annoying enough that I just made my own type so I wouldn't have to remember it lol

[Robert Maxton]

anyway, looking at O2C1 categorically, it is a sort of limit, in that it has the right kind of universal property: the type (s t : X ⟶ of (ULift Prop)) ×' IsInitial (pullback s t) is equivalent to the type of morphisms X ⟶ of O2C1. But for the life of me I can't see how to turn the LHS into a nice cone for it to be a limit over.

[Robert Maxton]

There are of course other ways to phrase the disjointness in a categorical way -- in terms of the subobject lattice, say. Actually, I don't have another good candidate; the subobject lattice would require s, t to be Mono, which isn't what we want. If we had a good enough spelling, maybe I could just make a custom .lift the way docs#CategoryTheory.EffectiveEpi has a custom .desc, but I haven't seen a spelling that looks sufficiently painless enough to use yet...