Theorems · Definition · category theory

CategoryTheory.Presieve.cocone

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (S : CategoryTheory.Presieve X) → CategoryTheory.Limits.Cocone S.diagram

Given a sieve S on X : C, its associated cocone S.cocone is defined to be the natural cocone over the diagram defined above with cocone point X.

Defined in

Mathlib.CategoryTheory.Sites.Sieves

Cited by

23 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category