rightUnitor — Mathlib

English

There is a canonical right unitor functor: rightUnitor: C × Discrete(PUnit) ⥤ C which projects to the first component.

Русский

Существует правый унитор-функтор: rightUnitor: C × Discrete(PUnit) ⥤ C, который проецирует на первую компоненту.

LaTeX

$$$\\mathrm{rightUnitor}: C \\times \\mathrm{Discrete}(PUnit) \\to C$ with $\\mathrm{obj}(X,\\!\\*) = X$, $\\mathrm{map}(f, _) = f$$$

Lean4

/-- The right unitor functor `C × 1 ⥤ C` -/
@[simps]
def rightUnitor : C × Discrete (PUnit : Type w) ⥤ C
    where
  obj X := X.1
  map f := f.1

Похожие утверждения