CATEGORIES, TYPES, AND STRUCTURES
1 1 CATEGORY: DEFINITION AND EXAMPLES 1 2 DIAGRAMS 1 3 CATEGORIES OUT OF CATEGORIES 1 4 MONIC, EPIC, AND PRINCIPAL MORPHISMS 1 5 SUBOBJECTS CONSTRUCTIONS 2 1 INITIAL AND TERMINAL OBJECTS 2 2 PRODUCTS AND COPRODUCTS 2 3 EXPONENTIALS 2 4 EXAMPLES OF CCCÕS 2 4 1 SCOTT DOMAINS 2 4 2 COHERENT DOMAINS 2 5 EQUALIZERS AND PULLBACKS 2 6 PARTIAL MORPHISMS AND COMPLETE OBJECTS 2 7 SUBOBJECT CLASSIFIERS AND TOPOI FUNCTORS AND NATURAL TRANSFORMATIONS 3 1 FUNCTORS 3 2 NATURAL TRANSFORMATIONS 3 3 CARTESIAN AND CARTESIAN CLOSED CATEGORIES REVISITED 3 4 MORE EXAMPLES OF CCCÕS 3 4 1 PARTIAL EQUIVALENCE RELATIONS 3 4 2 LIMIT AND FILTER SPACES 3 5 YONEDA'S LEMMA 3 6 PRESHEAVES CATEGORIES DERIVED FROM FUNCTORS AND NATURAL TRANSFORMATIONS 4 1 ALGEBRAS DERIVED FROM FUNCTORS 4 2 FROM MONOIDS TO MONADS 4 3 MONOIDAL AND MONOIDAL CLOSED CATEGORIES 4 4 MONOIDAL CATEGORIES AND LINEAR LOGIC UNIVERSAL ARROWS AND ADJUNCTIONS 5 1 UNIVERSAL ARROWS 5 2 FROM UNIVERSAL ARROWS TOWARD ADJUNCTIONS 5 3 ADJUNCTIONS 5 4 ADJUNCTIONS AND MONADS 5 5 MORE ON LINEAR LOGIC CONES AND LIMITS 6 1 LIMITS AND COLIMITS 6 2 SOME CONSTRUCTIONS REVISITED 6 3 EXISTENCE OF LIMITS 6 4 PRESERVATION AND CREATION OF LIMITS 6 5 W-LIMITS 7 1 INDEXED CATEGORIES 7 2 INTERNAL CATEGORY THEORY 7 3 INTERNAL PRESHEAVES 7 4 EXTERNALIZATION 7 5 INTERNALIZATION APPENDIX FORMULAE, TYPES, AND OBJECTS 8 1 L-NOTATION 8 2 THE TYPED L-CALCULUS WITH EXPLICIT PAIRS (LBHPT) 8 3 THE INTUITIONISTIC CALCULUS OF SEQUENTS 8 4 THE CUT-ELIMINATION THEOREM 8 5 CATEGORICAL SEMANTICS OF DERIVATIONS 8 6 THE CUT-ELIMINATION THEOREM REVISITED 8 7 CATEGORICAL SEMANTICS OF THE SIMPLY TYPED LAMBDA CALCULUS 8 8 FIXPOINT OPERATORS AND CCCS REFLEXIVE OBJECTS AND THE TYPE-FREE LAMBDA CALCULUS 9 1 COMBINATORY LOGIC 9 2 FROM CATEGORIES TO FUNCTIONALLY COMPLETE APPLICATIVE STRUCTURES 9 3 CATEGORICAL SEMANTICS OF THE L-CALCULUS 9 4 THE CATEGORICAL ABSTRACT MACHINE 9 5 FROM APPLICATIVE STRUCTURES TO CATEGORIES 9 6 TYPED AND APPLICATIVE STRUCTURES: APPLICATIONS AND EXAMPLES PART 1: PROVABLE ISOMORPHISMS OF TYPES PART 2: HIGHER TYPE OBJECTS AS MODELS OF THE TYPE-FREE L-CALCULUS RECURSIVE DOMAIN EQUATIONS 10 1 THE PROBLEM OF CONTRAVARIANT FUNCTORS 10 2 0-CATEGORIES SECOND ORDER LAMBDA CALCULUS 11 1 SYNTAX 11 2 THE EXTERNAL MODEL 11 3 THE EXTERNAL INTERPRETATION 11 4 THE INTERNAL MODEL 11 5 THE INTERNAL INTERPRETATION 11 6 RELATING MODELS