instLifting₂Lift₂

Mathlib.CategoryTheory.Localization.Bifunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.instLifting₂Lift₂

Lean4

noncomputable instance : Lifting₂ L₁ L₂ W₁ W₂ F (lift₂ F hF L₁ L₂) where
  iso :=
    (curryObjProdComp _ _ _).symm ≪≫ curry.mapIso (fac (uncurry.obj F) hF (L₁.prod L₂)) ≪≫ currying.unitIso.symm.app F

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

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

Разделы

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

Аффилиация

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