The category Discrete PUnit
#
We define star : C ⥤ Discrete PUnit
sending everything to PUnit.star
,
show that any two functors to Discrete PUnit
are naturally isomorphic,
and construct the equivalence (Discrete PUnit ⥤ C) ≌ C
.
The constant functor sending everything to PUnit.star
.
Instances For
Any two functors to Discrete PUnit
are isomorphic.
Instances For
Any two functors to Discrete PUnit
are equal.
You probably want to use punitExt
instead of this.
The functor from Discrete PUnit
sending everything to the given object.
Instances For
Functors from Discrete PUnit
are equivalent to the category itself.
Instances For
A category being equivalent to PUnit
is equivalent to it having a unique morphism between
any two objects. (In fact, such a category is also a groupoid;
see CategoryTheory.Groupoid.ofHomUnique
)