Theorems · Theorem · category theory

CategoryTheory.Join.pseudofunctorLeft_mapComp_hom_toNatTrans_app

∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] {a b c : CategoryTheory.Cat} (x : a ⟶ b) (x_1 : b ⟶ c)
  (X : CategoryTheory.Join (↑a) D),
  ((CategoryTheory.Join.pseudofunctorLeft D).mapComp x x_1).hom.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp
      (match X with
      | CategoryTheory.Join.left x_2 =>
        CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (x_1.toFunctor.obj (x.toFunctor.obj x_2)))
      | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x))
      ((CategoryTheory.Join.mapPairComp x.toFunctor (CategoryTheory.Functor.id D) x_1.toFunctor
              (CategoryTheory.Functor.id D)).hom.app
        X)

Defined in

Mathlib.CategoryTheory.Join.Pseudofunctor

Cited by

0 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category