instHasTerminal — Mathlib

English

The category of comonoids has a terminal object, namely the forgetful image of the trivial comonoid on the terminal object of the base category.

Русский

Категория комоноидов имеет терминальный объект, который получается из тривиального комоноида на терминальном объекте базовой категории.

LaTeX

$$$\text{HasTerminal}(\text{Comon } C)$$$

Lean4

instance : HasTerminal (Comon C) :=
  hasTerminal_of_unique (trivial C)

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