flip

Mathlib.Control.Bifunctor

URI: https://scilib.ai/kg/mathlib#LawfulBifunctor.flip

Lean4

instance flip [LawfulBifunctor F] : LawfulBifunctor (flip F)
    where
  id_bimap := by simp [bimap, functor_norm]
  bimap_bimap := by simp [bimap, functor_norm]

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

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

Разделы

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

Аффилиация

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