liftHom₂WhiskerRight

Mathlib.Tactic.CategoryTheory.BicategoryCoherence

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

Lean4

instance liftHom₂WhiskerRight {f g : a ⟶ b} (η : f ⟶ g) [LiftHom f] [LiftHom g] [LiftHom₂ η] {h : b ⟶ c} [LiftHom h] :
    LiftHom₂ (η ▷ h) where lift := LiftHom₂.lift η ▷ LiftHom.lift h

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

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

Разделы

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

Аффилиация

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