Structures · Category theory

CategoryTheory.HasSeparator

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

Defined in

Mathlib.CategoryTheory.Generator.Basic

Shape

One type argument · adds hasSeparator