One of the most important ideas of the four functor formalism was the proof that a projective morphism\ is lower transversal (satisfies a generalized analog of the proper base change theorem). Unfortunately no complete proof remained but all of the main ideas are contained in these notes:

1998-11-13-notes.pdf

1998-11-21-notes.pdf

2002-01-08-notes.pdf