Mor₁

Mathlib.Tactic.CategoryTheory.Coherence.Datatypes

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

Lean4

/-- Expressions for 1-morphisms. -/
inductive Mor₁ : Type/-- `id e a` is the expression for `𝟙 a`, where `e` is the underlying lean expression. -/

  | id (e : Expr) (a : Obj) : Mor₁/--
`comp e f g` is the expression for `f ≫ g`, where `e` is the underlying lean expression. -/

  | comp (e : Expr) : Mor₁ → Mor₁ → Mor₁/-- The expression for an atomic 1-morphism. -/

  | of : Atom₁ → Mor₁
  deriving Inhabited

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

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

Разделы

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

Аффилиация

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