id₁?

Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Bicategory.id₁?

Lean4

/-- Check that `e` is definitionally equal to `𝟙 a`. -/
def id₁? (e : Expr) : BicategoryM (Option Obj) := do
  let ctx ← read
  let _bicat := ctx.instBicategory
  let a : Q($ctx.B) ← mkFreshExprMVar ctx.B
  if ← withDefault <| isDefEq e q(𝟙 $a) then
    return some ⟨← instantiateMVars a⟩
  else
    return none

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

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

Разделы

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

Аффилиация

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