Introduction to Categories and Categorial Logic (draft)

Samson Abramsky and Nikos Tzevelekos......Page 1
1.1 Introduction......Page 7
1.1.1 From Elements To Arrows......Page 8
1.1.2 Categories Defined......Page 9
1.1.3 Diagrams in Categories......Page 10
1.1.4 Examples......Page 12
1.1.5 First Notions......Page 14
1.2.1 Initial and Terminal Objects......Page 17
1.2.2 Products and Coproducts......Page 19
1.2.3 Pullbacks and Equalisers......Page 24
1.3 Functors......Page 27
1.3.1 Basics......Page 28
1.3.2 Further Examples......Page 30
1.3.3 Contravariance......Page 32
1.3.4 Properties of Functors......Page 33
1.4.1 Basics......Page 35
1.4.2 Further Examples......Page 38
1.4.3 Functor Categories......Page 40
1.4.4 Exercises......Page 41
1.5 Universality and Adjoints......Page 42
1.5.1 Adjunctions for Posets......Page 43
1.5.2 Universal Arrows and Adjoints......Page 46
1.5.3 Limits and Colimits......Page 52
1.5.4 Exponentials......Page 53
1.5.5 Exercises......Page 55
1.6 The Curry-Howard Correspondence......Page 56
1.6.1 Logic......Page 57
1.6.2 Computation......Page 58
1.6.3 Simply-Typed -calculus......Page 62
1.6.4 Categories......Page 66
1.6.5 Categorical Semantics of Simply-Typed -calculus......Page 67
1.6.6 Completeness?......Page 70
1.7 Linearity......Page 73
1.7.1 Gentzen Sequent Calculus......Page 74
1.7.2 Linear Logic......Page 75
1.7.3 Linear Logic in Monoidal Categories......Page 78
1.7.4 Beyond the Multiplicatives......Page 82
1.7.5 Exercises......Page 84
1.8 Monads and Comonads......Page 85
1.8.1 Basics......Page 86
1.8.2 (Co)Monads of an Adjunction......Page 88
1.8.3 The Kleisli Construction......Page 89
1.8.4 Modelling of Linear Exponentials......Page 92
1.8.5 Exercises......Page 97
1.9 Review of Sets, Functions and Relations......Page 98
1.10 Guide to Further Reading......Page 100
References......Page 101