! !

we will normally write F f for F (f).

Let P : ¡ ! be an op¯bration with opcleavage ·. De¯ne F : ¡ Cat by !

FF{1 F (C) is the ¯ber over C for each object C of .

FF{2 For f : C ¡ D in and X an object of F (C), F f(X) is de¯ned to be the

!

codomain of the arrow ·(f; X).

FF{3 For f : C ¡ D in and u : X ¡ X 0 in F (C), F f (u) is the unique arrow

! !

0

from F f (X ) to F f (X ) given by OA{2 for which

F f(u) ± ·(f; X) = ·(f; X 0) ± u

4.1.8 Proposition Let P : ¡ ! be an op¯bration with cleavage ·. For any

arrow f : C ¡ D in , F f : F (C) ¡ F (D) as de¯ned by FF{1 through FF{3

! !

is a functor. Moreover, if · is a splitting, then F is a functor from to Cat.

Proof. Let u : X ¡ X 0 and v : X 0 ¡ X 00 in F (C). Then

! !

F f (v) ± ·(f; X 0 ) ± u

F f (v) ± F f (u) ± ·(f; X) =

(4.3)

·(f; X 00) ± v ± u

=

by two applications of FF{3. But then by the uniqueness part of FF{3, F f (v) ±

F f(u) must be F f (v ± u). This proves F f preserves composition. We leave the

preservation of identities to you.

42 Fibrations

Now suppose · is a splitting. Let f : C ¡ D and g : D ¡ E in , and let

! !

u : X ¡ X 0 in F (C). Then F (g ± f )(u) is the unique arrow from F (g ± f)(X)

!

(the codomain of ·(g ± f; X)) to F (g ± f)(X 0 ) (the codomain of ·(g ± f; X 0)) for

which

F (g ± f )(u) ± ·(g ± f; X) = ·(g ± f; X 0) ± u

Since · is a splitting, this says

F (g ± f)(u) ± ·(g; F f (X)) ± ·(f; X) = ·(g; F f (X 0 )) ± ·(f; X 0 ) ± u

By FF{3, the right side is

·(g; F f (X 0)) ± F f(u) ± ·(f; X)

Applying FF{3 with g and F f (u) instead of f and u, this is the same as

F g[F f (u)] ± ·(g; F f (X)) ± ·(f; X)

which is

F g[F f (u)] ± ·(g ± f; X)

because · is a splitting. Using the uniqueness requirement in FF{3, this means

F (g ± f )(u) = F g[F f(u)], so that F preserves composition. Again, we leave

preservation of the identity to you.

In a similar way, split ¯brations give functors op ¡ Cat. Let P :

! ¡

!

op

¡ Cat by

!

be a ¯bration with cleavage °. De¯ne F :

FF0{1 F (C) is the ¯ber over C for each object C of .

FF0{2 For f : C ¡ D in and Y an object of F (D), F f (Y ) is de¯ned to be the

!

domain of the arrow °(f; Y ).

FF0{3 For f : C ¡ D in and u : Y ¡ Y 0 in F (D), F f (u) is the unique arrow

! !

0

from F f (Y ) to F f (Y ) given by CA{2 for which

°(f; Y 0 ) ± F f (u) = u ± °(f; Y )

4.1.9 Proposition Let P : ¡ ! be a ¯bration with cleavage ·. For any

arrow f : C ¡ D in , F f : F (C) ¡ F (D) as de¯ned by FF{1 through FF{3

! !

is a functor. Moreover, if ° is a splitting, then F is a functor from op to Cat.

The proof is similar to those of Proposition ES 4.1.8 and is left as an exercise.

4.1.10 Exercises

¡

!

1. Verify that for any functor P : and object C of , the ¯ber over an

object C is a subcategory of .

2. Prove Proposition ES 4.1.9.

4.2 The Grothendieck construction 43

3. Let Á : Z4 ¡ Z2 be the homomorphism de¯ned in Exercise 2 of Section 2.9.

!

a. Show that the functor from C(Z4 ) to C(Z2 ) induced by Á is a ¯bration and

an op¯bration. (If you know about groups, this is an instance of the fact that

every surjective group homomorphism is a ¯bration and an op¯bration.)

b. Show that Á is not a split ¯bration or op¯bration.

4. Let be a category with pullbacks and its arrow category. For an arrow

f : A ¡ B (object of ) let P (f) = B. For an arrow (h; k) : f ¡ g (where g : C

! !

¡ D in ) in , let P (h; k) = k.

!

¡

! is a functor.

a. Show that P :

b. Show that P is a ¯bration.

4.2 The Grothendieck construction

The Grothendieck construction is a way of producing ¯brations. It generalizes

the semidirect product construction for monoids, which is de¯ned here. Hyland

and Pitts [1989] use the Grothendieck construction to construct categories that

are models of the calculus of constructions, a system due to Coquand and Huet

[1988] that provides a way of handling polymorphism essentially by quantifying

over types. (See also [Coquand, 1988], [Ehrhard, 1988] and [Asperti and Martini,

1992].)

The construction can be applied to either set-valued functors or category-

¡ Set or F :

! ¡ Cat, it con-

!

valued functors. Given such a functor F :

structs a category G( ; F ) and a functor from G( ; F ) to . When F is set-

valued we will write G0 instead of G. We will look at the set-valued case ¯rst,

since it is simpler.

be a small category and let F : ¡ Set be a functor. For each

!

4.2.1 Let

object C of , F (C) is a set, and for each arrow f : C ¡ D, F (f) : F (C) ¡ f(D)

! !

is a set function. There is no set of all sets or set of all set functions, but, since

is small, there certainly is a set consisting of all the elements of all the sets

F (C), and similarly there is a set consisting of all the functions F (f). In other

¡ Set requires only a

!

words, although Set is large, the description of F :

small amount of data. (`Small' and `large' are used here in the technical sense,

referring to whether or not a set of data is involved. See 1.3.4.)

By contrast, to describe a functor G : Set ¡ ! would require a large amount of

data { an object of for each set, and so on.

We will formalize these observations about F : ¡ Set by taking the disjoint

!

union of all the sets of the form F (C) for all objects C of . The elements of

this disjoint union can be represented as pairs (x; C) for all objects C of and

elements x 2 F (C). (Thus we construct the disjoint union of sets by labeling

44 Fibrations

the elements. The disjoint union is the construction in Set corresponding to the

categorical concept of `sum', discussed in Section 5.4.)

We must do more than this to capture the functorial nature of F { what it

does to arrows of . The category G0( ; F ) constructed by the Grothendieck

construction does capture this structure, and its set of objects is the disjoint

union just mentioned.

4.2.2 If we were to draw a picture to explain what F does, the result might be

Diagram (ES 4.4), in which f : C ¡ C 0 and g : C 0 ¡ C 00 are arrows of

! ! and x

and x0 are elements of F (C) and F (C 0 ) respectively. The box over each object C