Theorems · Definition · category theory

CategoryTheory.Limits.Types.Small.limitCone

{J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) → [Small.{u, max u v} ↑F.sections] → CategoryTheory.Limits.Cone F

(internal implementation) the limit cone of a functor, implemented as flat sections of a pi type

Defined in

Mathlib.CategoryTheory.Limits.Types.Limits

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategorySmall