Theorems · Definition · category theory

CategoryTheory.MorphismProperty.CostructuredArrow.toOver

{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) →
          (F : CategoryTheory.Functor C D) → (X : D) → CategoryTheory.Functor (P.CostructuredArrow ⊤ F X) (P.Over ⊤ X)

Reinterpreting an F-costructured arrow F.obj A ⟶ X as an arrow over X.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Comma

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category