mkOfOplax

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pseudofunctor.StrongTrans.mkOfOplax

Lean4

/-- Construct a strong transformation of pseudofunctors from a strong transformation of the
underlying oplax functors. -/
@[simps]
def mkOfOplax (η : Oplax.StrongTrans F.toOplax G.toOplax) : StrongTrans F G
    where
  app := η.app
  naturality := η.naturality
  naturality_naturality θ := η.naturality_naturality θ
  naturality_id a := η.naturality_id a
  naturality_comp f g := η.naturality_comp f g

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

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

Разделы

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

Аффилиация

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