The core of a category #
The core of a category C
is the (non-full) subcategory of C
consisting of all objects,
and all isomorphisms. We construct it as a CategoryTheory.Groupoid
.
CategoryTheory.Core.inclusion : Core C ⥤ C
gives the faithful inclusion into the original
category.
Any functor F
from a groupoid G
into C
factors through CategoryTheory.Core C
,
but this is not functorial with respect to F
.
The core of a category C is the groupoid whose morphisms are all the isomorphisms of C.
Instances For
The core of a category is naturally included in the category.
Instances For
A functor from a groupoid to a category C factors through the core of C.
Instances For
We can functorially associate to any functor from a groupoid to the core of a category C
,
a functor from the groupoid to C
, simply by composing with the embedding Core C ⥤ C
.
Instances For
ofEquivFunctor m
lifts a type-level EquivFunctor
to a categorical functor Core (Type u₁) ⥤ Core (Type u₂)
.