liftHom₂AssociatorInv

Mathlib.Tactic.CategoryTheory.BicategoryCoherence

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.BicategoryCoherence.liftHom₂AssociatorInv

Lean4

instance liftHom₂AssociatorInv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) [LiftHom f] [LiftHom g] [LiftHom h] :
    LiftHom₂ (α_ f g h).inv where lift := (α_ (LiftHom.lift f) (LiftHom.lift g) (LiftHom.lift h)).inv

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

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

Разделы

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

Аффилиация

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