hasForgetToType

Mathlib.CategoryTheory.ConcreteCategory.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.hasForgetToType

Lean4

/-- Every forgetful functor factors through the identity functor. This is not a global instance as
    it is prone to creating type class resolution loops. -/
def hasForgetToType (C : Type u) [Category.{v} C] [HasForget.{w} C] : HasForget₂ C (Type w)
    where
  forget₂ := forget C
  forget_comp := Functor.comp_id _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru