Theorems · Definition · category theory

CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (P : CategoryTheory.Limits.IndObjectPresentation A) →
        CategoryTheory.Functor P.I (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)

The canonical comparison functor between the indexing category of the presentation and the comma category CostructuredArrow yoneda A. This functor is always final.

Defined in

Mathlib.CategoryTheory.Limits.Indization.IndObject

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category