Explicit limits and colimits

This file applies the general API for explicit limits and colimits in CompHausLike P (see the file Mathlib/Topology/Category/CompHausLike/Limits.lean) to the special case of CompHaus.

instance CompHaus.instHasExplicitPullbacksTrue : CompHausLike.HasExplicitPullbacks fun (x : TopCat) => True

instance CompHaus.instHasExplicitFiniteCoproductsTrue : CompHausLike.HasExplicitFiniteCoproducts fun (x : TopCat) => True

@[reducible, inline]

abbrev CompHaus.isTerminalPUnit : CategoryTheory.Limits.IsTerminal (of PUnit.{u + 1})

A one-element space is terminal in CompHaus

noncomputable def CompHaus.terminalIsoPUnit : ⊤_ CompHaus ≅ of PUnit.{u + 1}

The isomorphism from an arbitrary terminal object of CompHaus to a one-element space.