English
The forgetful functor from MonCat to Type is corepresentable via a coyoneda isomorphism with ULift(Nat) and Multiplicative Nat; i.e., coyoneda.obj(op(of(ULift Multiplicative Nat))) ≅ forget MonCat.
Русский
Забывающий функтор из MonCat в Type является ядром представления через кoyoneda-изоморфизм с ULift(Nat) и Multiplicative Nat; т.е.Coyoneda.obj(op(of(ULift(Multiplicative Nat)))) ≅ forget MonCat.
LaTeX
$$$\text{coyoneda.obj} (\mathrm{op}(\mathrm{of}(\mathrm{ULift}(\mathrm{Multiplicative}\ \mathbb{N})))) \cong \mathrm{forget\ MonCat}$$$
Lean4
/-- The forgetful functor `MonCat.{u} ⥤ Type u` is corepresentable. -/
def coyonedaObjIsoForget : coyoneda.obj (op (of (ULift.{u} (Multiplicative ℕ)))) ≅ forget MonCat.{u} :=
NatIso.ofComponents fun M ↦ (ConcreteCategory.homEquiv.trans (uliftPowersHom M.carrier).symm).toIso
