Categorical Proof Theory and Linear Logic

These are some very, very old notes from a course I gave in Prague, at  ESSLLI 1996.

The idea was to present enough basic category theory and enough basic proof theory to discuss the categorical modelling of Linear Logic and ... drum roll...introduce  Dialectica Categories.

(and yes, I also had high expectations of understanding enough about models of Linear Logic to be able to discuss them all and write a book, ha...)

 Now I have reduced my expectations and I simply would like to introduce enough category theory to make the categorical modelling of Intuitionistic Logic plausible (before I wanted to do both intuitionistic and linear logic).

But in compensation I would like to do this in four lectures only, as I wanted to keep the 5th lecture to introduce Glue Semantics,  in the style that a linear logician, especially  a budding one, would understand it. At least this is the plan.