Theorems · Definition · category theory

CategoryTheory.Grothendieck.grothendieckTypeToCatInverse

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

Auxiliary definition for grothendieckTypeToCat, to speed up elaboration.

Defined in

Mathlib.CategoryTheory.Grothendieck

Cited by

9 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category