srcM

Mathlib.Tactic.CategoryTheory.Coherence.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.BicategoryLike.Mor₂Iso.srcM

Lean4

/-- The domain of a 2-isomorphism. -/
def srcM {m : Type → Type} [Monad m] [MonadMor₁ m] : Mor₂Iso → m Mor₁
  | .structuralAtom α => α.srcM
  | .comp _ f .. => return f
  | .whiskerLeft _ f g .. => do
    comp₁M f g
  | .whiskerRight _ f _ _ h => do
    comp₁M f h
  | .horizontalComp _ f₁ _ f₂ .. => do
    comp₁M f₁ f₂
  | .inv _ _ g _ => return g
  | .coherenceComp _ f .. => return f
  | .of η => return η.src

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

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

Разделы

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

Аффилиация

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