Una fibración de Grothendieck (o categoría fibrada) es un funtor
tal que para cualquier
existe un morfismo cartesiano
p ( ϕ ) = f
es cartesiano sobre el morfismo
p ( f ) = u
y además para cualquier
p ( g ) = u ∘ w
{\displaystyle p(g)=u\circ w}
{\displaystyle h\colon p(Z)\to J}
p ( h ) = w
f ∘ h = g
Decimos que el funtor
es una fibración de Grothendieck si para cada morfismo de la forma
existe un morfismo cartesiano sobre él.
r e d
cuyos objetos son pares determinados por un conjunto y un subconjunto suyo
Podemos interpretar cada uno de los objetos de la categoría como un predicado sobre los elementos del conjunto
: el predicado que cumplen sólo aquellos elementos que pertenecen al subconjunto
viene determinado por una función
{\displaystyle u(X)\subseteq Y}
; es decir, que puede restringirse a
r e d
es una fibración de Grothendieck.
podemos construir el morfismo cartesiano
determinado por un producto fibrado de la inclusión
Este morfismo es cartesiano debido a la propiedad universal del producto fibrado.