NormalizedHom

Mathlib.Tactic.CategoryTheory.Coherence.Datatypes

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

Lean4

/-- Type of normalized 1-morphisms `((... ≫ h) ≫ g) ≫ f`. -/
inductive NormalizedHom : Type/-- The identity 1-morphism `𝟙 a`. -/

  | nil (e : Mor₁) (a : Obj) : NormalizedHom/--
The `cons` composes an atomic 1-morphism at the end of a normalized 1-morphism. -/

  | cons (e : Mor₁) : NormalizedHom → Atom₁ → NormalizedHom
  deriving Inhabited

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

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

Разделы

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

Аффилиация

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