toAppExpr

Mathlib.Tactic.CategoryTheory.ToApp

URI: https://scilib.ai/kg/mathlib#CategoryTheory.toAppExpr

Lean4

/-- Given morphisms `f g : C ⟶ D` in the bicategory `Cat`, and an equation `η = θ` between 2-morphisms
(possibly after a `∀` binder), produce the equation `∀ (X : C), f.app X = g.app X`, and simplify
it using basic lemmas about `NatTrans.app`. -/
def toAppExpr (e : Expr) : MetaM Expr := do
  mapForallTelescope
      (fun e => do
        simpType catAppSimp (← mkAppM ``NatTrans.congr_app #[e]))
      e

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

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

Разделы

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

Аффилиация

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