Comp

Mathlib.Control.Functor

URI: https://scilib.ai/kg/mathlib#Functor.Comp

Lean4

/-- `Functor.Comp` is a wrapper around `Function.Comp` for types.
It prevents Lean's type class resolution mechanism from trying
a `Functor (Comp F id)` when `Functor F` would do. -/
def Comp (F : Type u → Type w) (G : Type v → Type u) (α : Type v) : Type w :=
  F <| G α

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

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

Разделы

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

Аффилиация

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