mkHasForget₂

Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom

URI: https://scilib.ai/kg/mathlib#CategoryTheory.UnbundledHom.mkHasForget₂

Lean4

/-- A custom constructor for forgetful functor
between concrete categories defined using `UnbundledHom`. -/
def mkHasForget₂ : HasForget₂ (Bundled c) (Bundled c') :=
  BundledHom.mkHasForget₂ obj (fun f => ⟨f.val, map f.property⟩) fun _ => rfl

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

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

Разделы

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

Аффилиация

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