tgtM

Mathlib.Tactic.CategoryTheory.Coherence.Datatypes

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

Lean4

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

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

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

Разделы

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

Аффилиация

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