Theorems · Definition · category theory

CategoryTheory.TwoSquare.CostructuredArrowDownwards

{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₄} →
                        CategoryTheory.TwoSquare T L R B →
                          {X₂ : C₂} → {X₃ : C₃} → (R.obj X₂ ⟶ B.obj X₃) → Type (max (max u₁ v₂) v₃)

Given w : TwoSquare T L R B and a morphism g : R.obj X₂ ⟶ B.obj X₃, this is the category CostructuredArrow (w.structuredArrowDownwards X₂) (StructuredArrow.mk g), see the constructor CostructuredArrowDownwards.mk for the data that is involved.

Defined in

Mathlib.CategoryTheory.GuitartExact.Basic

Cited by

30 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category