Theorems · Definition · category theory

CategoryTheory.CommaMorphism.casesOn

{A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {X Y : CategoryTheory.Comma L R} →
                  {motive : CategoryTheory.CommaMorphism X Y → Sort u} →
                    (t : CategoryTheory.CommaMorphism X Y) →
                      ((left : X.left ⟶ Y.left) →
                          (right : X.right ⟶ Y.right) →
                            (w :
                                CategoryTheory.CategoryStruct.comp (L.map left) Y.hom =
                                  CategoryTheory.CategoryStruct.comp X.hom (R.map right)) →
                              motive { left := left, right := right, w := w }) →
                        motive t

Defined in

Mathlib.CategoryTheory.Comma.Basic

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category