Theorems · Definition · category theory

CategoryTheory.Grothendieck.grothendieckTypeToCat

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (G : CategoryTheory.Functor C (Type w)) → CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat) ≌ G.Elements

The Grothendieck construction applied to a functor to Type (thought of as a functor to Cat by realising a type as a discrete category) is the same as the 'category of elements' construction.

Defined in

Mathlib.CategoryTheory.Grothendieck

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category