ofLawfulFunctor

Mathlib.Control.EquivFunctor

URI: https://scilib.ai/kg/mathlib#EquivFunctor.ofLawfulFunctor

Lean4

instance (priority := 100) ofLawfulFunctor (f : Type u₀ → Type u₁) [Functor f] [LawfulFunctor f] : EquivFunctor f
    where
  map {_ _} e := Functor.map e
  map_refl'
    α := by
    ext
    apply LawfulFunctor.id_map
  map_trans' {α β γ} k
    h := by
    ext x
    apply LawfulFunctor.comp_map k h x

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

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

Разделы

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

Аффилиация

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