The category of open sets in a topological space. #
Really it's a 2-functor from (spaces, continuous functions, equalities)
to (categories, functors, natural isomorphisms).
We don't attempt to set up the full theory here, but do provide the natural isomorphisms
mapId : map (𝟙 X) ≅ 𝟭 (opens X) and
mapComp : map (f ≫ g) ≅ map g ⋙ map f.
Beyond that, there's a collection of simp lemmas for working with these constructions.
Opens X has a partial order, it automatically receives a
Unfortunately, because we do not allow morphisms in
U ⟶ V are not just proofs
U ≤ V, but rather
ULift (PLift (U ≤ V)).
We now construct as morphisms various inclusions of open sets.
Opens X ⥤ Opens X given by taking preimages under the identity function
is naturally isomorphic to the identity functor.
The natural isomorphism between taking preimages under
f ≫ g, and the composite
of taking preimages under
g, then preimages under