WhiskerLeft

Mathlib.Tactic.CategoryTheory.Coherence.Normalize

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

Lean4

/-- Expressions of the form `f₁ ◁ ... ◁ fₙ ◁ η`. -/
inductive WhiskerLeft : Type/-- Construct the expression for a right-whiskered 2-morphism. -/

  | of (η : HorizontalComp) : WhiskerLeft/-- Construct the expression for `f ◁ η`. -/

  | whisker (e : Mor₂) (f : Atom₁) (η : WhiskerLeft) : WhiskerLeft
  deriving Inhabited

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

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

Разделы

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

Аффилиация

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