instCoeSortFGModuleCatType — Mathlib

English

There is a canonical CoeSort structure on FGModuleCat R via FGModuleCat.carrier, i.e., objects of FGModuleCat can be regarded as types directly.

Русский

Существует каноническая структура приведения типов через FGModuleCat.carrier, благодаря чему объекты FGModuleCat можно рассматривать как типы напрямую.

LaTeX

$$$\\text{CoeSort}(FGModuleCat(R),\\,\\mathrm{Type}) \\,=\\, \\mathrm{FGModuleCat.carrier}$$$

Lean4

instance : CoeSort (FGModuleCat.{v} R) (Type v) :=
  ⟨FGModuleCat.carrier⟩

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