Theorems · Definition · category theory

CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk

{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        (w : CategoryTheory.TwoSquare T L R B) →
                          {X₂ : C₂} →
                            {X₃ : C₃} →
                              (g : R.obj X₂ ⟶ B.obj X₃) →
                                (X₁ : C₁) →
                                  (a : X₂ ⟶ T.obj X₁) →
                                    (b : L.obj X₁ ⟶ X₃) →
                                      CategoryTheory.CategoryStruct.comp (R.map a)
                                            (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) =
                                          g →
                                        w.CostructuredArrowDownwards g

Constructor for objects in w.CostructuredArrowDownwards g.

Defined in

Mathlib.CategoryTheory.GuitartExact.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category