Theorems · Definition · category theory

CategoryTheory.Sum.functorEquivFunctorCompSndIso

{A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {A' : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
        {B : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} B] →
            (CategoryTheory.Sum.functorEquiv A A' B).functor.comp
                (CategoryTheory.Prod.snd (CategoryTheory.Functor A B) (CategoryTheory.Functor A' B)) ≅
              (CategoryTheory.Functor.whiskeringLeft A' (A ⊕ A') B).obj (CategoryTheory.Sum.inr_ A A')

Composing the forward direction of functorEquiv with the second projection is the same as precomposition with inr_ A A'.

Defined in

Mathlib.CategoryTheory.Sums.Products

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category