StructuralAtom

Mathlib.Tactic.CategoryTheory.Coherence.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.BicategoryLike.StructuralAtom

Lean4

/-- Expressions for atomic structural 2-morphisms. -/
inductive StructuralAtom : Type/-- The expression for the associator `α_ f g h`. -/

  | associator (e : Expr) (f g h : Mor₁) : StructuralAtom/-- The expression for the left unitor `λ_ f`. -/

  | leftUnitor (e : Expr) (f : Mor₁) : StructuralAtom/-- The expression for the right unitor `ρ_ f`. -/

  | rightUnitor (e : Expr) (f : Mor₁) : StructuralAtom
  | id (e : Expr) (f : Mor₁) : StructuralAtom
  | coherenceHom (α : CoherenceHom) : StructuralAtom
  deriving Inhabited

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

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

Разделы

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

Аффилиация

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