Start section on fibrational framework for nested alternating fixed points.
Show how the predicate transformer is built in the univariate case and how it is extended to the multivariate case.

1st slide : title page
2nd slide : bisimulations
3rd slide : fibrations