Theorems · Definition · category theory

CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor

{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 : B.op.obj X₃ ⟶ R.op.obj X₂) →
                                CategoryTheory.Functor (w.op.StructuredArrowRightwards g)ᵒᵖ
                                  (w.CostructuredArrowDownwards g.unop)

Auxiliary definition for structuredArrowRightwardsOpEquivalence.

Defined in

Mathlib.CategoryTheory.GuitartExact.Opposite

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category