mathlibdocumentation

Equipping a type with the discrete topology is left adjoint to the forgetful functor Top ⥤ Type.
Equipping a type with the trivial topology is right adjoint to the forgetful functor Top ⥤ Type.