The forget functor is corepresentable #
The forgetful functor AddCommMonCat.{u} ⥤ Type u
is corepresentable
by ULift ℕ
. Similar results are obtained for the variants CommMonCat
, AddMonCat
and MonCat
.
(ULift ℕ →+ G) ≃ G
#
These universe-monomorphic variants of multiplesHom
/powersHom
are put here since they
shouldn't be useful outside of category theory.
Monoid homomorphisms from ULift (Multiplicative ℕ)
are defined by the image
of Multiplicative.ofAdd 1
.
Equations
Instances For
The equivalence (Multiplicative ℕ →* α) ≃ α
for any monoid α
.
Equations
Instances For
The equivalence (ULift (Multiplicative ℕ) →* α) ≃ α
for any monoid α
.
Equations
Instances For
The equivalence (ℤ →+ α) ≃ α
for any additive group α
.
Equations
Instances For
The equivalence (ULift ℕ →+ α) ≃ α
for any additive monoid α
.
Equations
Instances For
The forgetful functor MonCat.{u} ⥤ Type u
is corepresentable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forgetful functor CommMonCat.{u} ⥤ Type u
is corepresentable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forgetful functor AddMonCat.{u} ⥤ Type u
is corepresentable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forgetful functor AddCommMonCat.{u} ⥤ Type u
is corepresentable.
Equations
- One or more equations did not get rendered due to their size.