Theorems · Definition · category theory

CategoryTheory.MorphismProperty.CostructuredArrow.forget

{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} D] →
        (P : CategoryTheory.MorphismProperty D) →
          (Q : CategoryTheory.MorphismProperty C) →
            [inst_2 : Q.IsMultiplicative] →
              (F : CategoryTheory.Functor C D) →
                (X : D) → CategoryTheory.Functor (P.CostructuredArrow Q F X) (CategoryTheory.CostructuredArrow F X)

The forgetful functor from the subcategory P.CostructuredArrow Q F X.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Comma

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicative