Categorical Logic and Type Theory
, Bart Jacobs
I. Intro to Fibered Category Theory
1.1 Fibrations