Theorems · Definition · category theory

CategoryTheory.Functor.sections

{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] → (F : CategoryTheory.Functor J (Type w)) → Set ((j : J) → F.obj j)

The sections of a functor F : J ⥤ Type are the choices of a point u j : F.obj j for each j, such that F.map f (u j) = u j' for every morphism f : j ⟶ j'. We later use these to define limits in Type and in many concrete categories.

Defined in

Mathlib.CategoryTheory.Types.Basic

Cited by

140 results in Mathlib

Foundations

Depth 13 from the axioms, rests on 78 definitions · uses propext, Quot.sound

Assumes

CategoryTheory.Category