Theorems · Definition · category theory

CategoryTheory.Comma.costructuredArrowSndInclusion

{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) →
                (b : B) →
                  CategoryTheory.Functor (CategoryTheory.CostructuredArrow L (R.obj b))
                    (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b)

The functor from the costructured arrow category on L over R.obj b to the costructured arrow category on snd L R over b : B.

Defined in

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category