# mathlibdocumentation

topology.category.Top.adjunctions

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

Equations

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

Equations