instFullForget — Mathlib

English

The forgetful functor from the category of finite types to the category of all types is full; equivalently, for any finite types X and Y, every function X → Y arises as a morphism in FintypeCat.

Русский

Забывающий функтор из категории конечных типов в категорию всех типов полно: любой отображение между двумя конечными типами реализуется как морфизм в FintypeCat.

LaTeX

$$$\forall X,Y\,\text{FinType},\ Hom_{\mathrm{FintypeCat}}(X,Y) \cong \ Hom_{\mathbf{Type}}(X,Y).$$$

Lean4

instance : (forget FintypeCat).Full :=
  inferInstanceAs <| FintypeCat.incl.Full

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