English
The canonical equivalences between Mon (Type u) and MonCat(u), and between Grp_(Type u) and GrpCat(u), are compatible with the forgetful functors to MonCat and to Mon(Type u). In particular, forgetting first or after these equivalences yields naturally isomorphic (indeed identical) functors.
Русский
Канонические эквивалентности между Mon(Type u) и MonCat(u) и между Grp_(Type u) и GrpCat(u) совместимы со забывающими функторaми к MonCat и к Mon(Type u). В частности, забывать структуру до или после этих эквивалентностей даёт естественно изоморфные (по существу тождественные) функторы.
LaTeX
$$$\\text{forget}_{\\mathrm{GrpCat} \\to \\mathrm{MonCat}} \\circ GrpTypeEquivalenceGrp.functor \\cong \\Grp_.forget_{\\mathrm{Mon}(\\mathrm{Type}\\ u)} \\circ \\mathrm{MonTypeEquivalenceMon.functor}$$$
Lean4
/-- The equivalences `Mon (Type u) ≌ MonCat.{u}` and `Grp_ (Type u) ≌ GrpCat.{u}`
are naturally compatible with the forgetful functors to `MonCat` and `Mon (Type u)`.
-/
noncomputable def grpTypeEquivalenceGrpForget :
GrpTypeEquivalenceGrp.functor ⋙ forget₂ GrpCat MonCat ≅ Grp_.forget₂Mon (Type u) ⋙ MonTypeEquivalenceMon.functor :=
Iso.refl _
