Theorems · Definition · category theory

CategoryTheory.Limits.Types.coneOfSection

{J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J (Type u)} → {s : (j : J) → F.obj j} → s ∈ F.sections → CategoryTheory.Limits.Cone F

Given a section of a functor F into Type*, construct a cone over F with PUnit as the cone point.

Defined in

Mathlib.CategoryTheory.Limits.Types.Limits

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category