Structures · Category theory

CategoryTheory.HasCoseparator

For a category C and an object G : C, G is a coseparator of C if the functor C(-, G) is faithful. While IsCoseparator G : Prop is the proposition that G is a coseparator of C, an HasCoseparator C : Prop is the proposition that such a coseparator exists. Note that HasCoseparator C is a proposition. It does not designate a favored coseparator and merely asserts the existence of one.

Defined in

Mathlib.CategoryTheory.Generator.Basic

Shape

One type argument · adds hasCoseparator