Practical Foundations of Mathematics

Paul Taylor

Published by Cambridge University Press, 1999, ISBN 0 521 63107 6.

www.Paul Taylor. EU/Practical-Foundations

This summary explains which parts of the book are original research or novelties of exposition. The entire text is now accessible on the Web in an approximate HTML translation, so if you are reading the HTML version of this document you can go directly to the parts of the text to which it refers.

General description

Practical Foundations collects the methods of construction of the objects of twentieth century mathematics. Although it is mainly concerned with a framework essentially equivalent to intuitionistic ZF, the book looks forward to more subtle bases in categorical type theory and the machine representation of mathematics. Each idea is illustrated by wide-ranging examples, and followed critically along its natural path, transcending disciplinary boundaries between universal algebra, type theory, category theory, set theory, sheaf theory, topology and programming.

The first three chapters will be essential reading for the design of courses in discrete mathematics and reasoning, especially for the "box method" of proof taught successfully to first year informatics students. Chapters IV, V and VII are an introduction to categorical logic. Between the formal languages translations are provided which are fluent, showing how to write vernacular proofs that are sound in formal logics.

Chapter VI is a new approach to term algebras, induction and recursion, which have hitherto only been treated either naïvely or with set theory. The last two chapters prove in detail the equivalence of types and categories, in particular between generalised algebraic theories and categories with display maps.

Students and teachers of computing, mathematics and philosophy will find this book both readable and of lasting value as a reference work.

The book is an account of the foundations of mathematics (algebra) and theoretical computer science, from a modern constructive viewpoint. It is intended, amongst other things, to provide a bridge between the use of logic underlying mathematical constructions and its abstract study in disciplines such as the lambda calculus, predicate calculus, type theory and universal algebra. It began as the prerequisites for another book (Domains and Duality), so it contains very little domain theory itself, but it does treat the fundamental issues of the semantics of programming languages.

Mathematical and computing issues are interwoven. For example the classifying category for an algebraic theory is defined as a declarative programming language, which is in turn illustrated by the solution of cubic equations.

Category theory plays a major role in the book, but the abstract concepts are introduced on a "need to know" basis. Emphasis is placed on how functoriality, naturality, uniqueness, universality and pullback-stability carry the force of the constructions and properties (such as invariance under substitution), rather than allowing the reader to think that these are merely bureaucratic side conditions. Wherever possible, the poset analogues of categorical results are given first.

Excluded Middle is avoided, being largely irrelevant to algebra and category theory (these are often done "inside a topos"). However just as it is easier to teach a baby to swim before it has learnt the fear of water, so it is simpler to be constructive from the beginning with naive set theory than to recover it later with Kripke models or Grothendieck toposes.

Every result has been taken apart, sharpened, polished and re-assembled, so most of the sections contain material which is in some way original, and much of it could have been published individually. However much of the value of the book is that it deliberately blurs distinctions between disciplines, resolving numerous apparent conflicts of viewpoint which would never have been considered so thoroughly if they had been treated separately.

Introduction (from the book itself)

Foundations have acquired a bad name amongst mathematicians, because of the reductionist claim analogous to saying that the atomic chemistry of carbon, hydrogen, oxygen and nitrogen is enough to understand biology. Worse than this: whereas these elements are known with no question to be fundamental to life, the membership relation and the Sheffer stroke have no similar status in mathematics.

Our subject should be concerned with the basic idioms of argument and construction in mathematics and programming, and seek to explain these (as fundamental physics does) in terms of more general and basic phenomena. This is "discrete math for grown-ups."

A moderate form of the logicist thesis is established in the tradition from Weierstrass to Bourbaki, that mathematical discussions consist of the manipulation of assertions built using ∧, ∨, ⇒, ∀ and ∃. We shall show how the way in which mathematicians (and programmers) - rather than logicians - conduct such discussions really does correspond to a certain semi-formal system of proof in (intuitionistic) predicate calculus. The working mathematician who is aware of this correspondence will be more likely to make valid arguments, that others are able to follow. Automated deduction is still in its infancy, but such awareness may also be expected to help with computer-assisted construction, verification and dissemination of proofs.

One of the more absurd claims of extreme logicism was the reduction of the natural numbers to the predicate calculus. Now we have a richer view of what constitutes logic, based on a powerful analogy between types and propositions. In classical logic, as in classical physics, particles enact a logical script, but neither they nor the stage on which they perform are permanently altered by the experience. In the modern view, matter and its activity are created together, and are interchangeable (the observer also affects the experiment by the strength of the meta-logic).

This analogy, which also makes algebra, induction and recursion part of logic, is a structural part of this book, in that we always treat the simpler propositional or order-theoretic version of a phenomenon as well as the type or categorical form.

Besides this and the classical symmetry between ∧ and ∨ and between ∀ and ∃, the modern rules of logic exhibit one between introduction (proof, element) and elimination (consequence, function). These rules are part of an even wider picture, being examples of adjunctions.

This suggests a new understanding of foundations apart from the mere codification of mathematics in logical scripture. When the connectives and quantifiers have been characterised as (universal) properties of mathematical structures, we can ask what other structures admit these properties. Doing this for coproducts in particular reveals rather a lot of the elementary theory of algebra and topology. We also look for function spaces and universal quantifiers among topological spaces.

A large part of this book is category theory, but that is because for many applications this seems to me to be the most efficient heuristic tool for investigating structure, and comparing it in different examples. Plainly we all write mathematics in a symbolic fashion, so there is a need for fluent translations that render symbols and diagrams as part of the same language. However, it is not enough to see recursion as an example of the adjoint functor theorem, or the propositions-as-types analogy as a reflection of bicategories. We must also contrast the examples and give a full categorical account of symbolic notions like structural recursion.

You should not regard this book as yet another foundational prescription. I have deliberately not given any special status to any particular formal system, whether ancient or modern, because I regard them as the vehicles of meaning, not its cargo. I actually believe the (moderate) logicist thesis less than most mathematicians do. This book is not intended to be synthetic, but analytic - to ask what mathematics requires of logic, with a view to starting again from scratch.

Advice to the reader

Technical books are never written and seldom read sequentially. Of course you have to know what a category is to tackle Chapter V, but otherwise it is supposed to be possible to read any of at least the first six chapters on the basis of general mathematical experience alone; the people listed below were given individual chapters to read partly in order to ensure this. There is more continuity between sections, but again, if you get stuck, move on to the next one, as secondary material is included at the end of some sections (and sub-sections). The book is thoroughly indexed and cross-referenced to take you as quickly as possible to specific topics; when you have found what you want, the cross-references should be ignored.

The occasional anecdotes are not meant to be authoritative history. They are there to remind us that mathematics is a human activity, which is always done in some social and historical context, and to encourage the reader to trace its roots. The dates emphasise quite how late logic arrived on the mathematical scene. The footnotes are for colleagues, not general readers, and there are theses to be written à propos of the exercises.

The first three chapters should be accessible to final year undergraduates in mathematics and informatics; lecturers will be able to select appropriate sections themselves, but should warn students about parenthetical material. Most of the book is addressed to graduate students; Section 6.4 and the last two chapters are research material. I hope, however, that every reader will find interesting topics throughout the book.

Chapters IV, V and VII provide a course on category theory. Chapter III is valuable as a prelude since it contains many of the results (the adjoint functor theorem, for example) in much simpler form.

Sections 1.1-5 (not necessarily in that order), 2.3, 2.4, 2.7, 2.8, 3.1-5, 4.1-5 and 4.7 provide a course on the semantics of the λ-calculus.

For imperative languages, take Sections 1.4, 1.5, 4.1-6, 5.3, 5.5 and 6.4.

An advanced course on type theory would use Chapter IV as a basis, followed by Chapters V and IX with Sections 7.6, 7.7 to give semantic and syntactic points of view on similar issues.

Chapter VI and Section 9.6 discuss topics in symbolic logic from the point of view of category theory.

I. First Order Reasoning

1.1: Substitution
Variables; substitution, in tree and linear notation, with an informal account of structural recursion. The quantifiers as variable-binders; α-equivalence.
The substitution lemma (extended to include weakening) plays a much more important role in this book than is usual in accounts of syntax, being used as the equations in a sketch for the classifying category in Sections 4.3 and 8.2. Our notation for substitution is [a/x]^*t, since this is pullback along the morphism [a/x]. An explicit notation, [^(x)]^*, is also introduced for weakening.
1.2: Denotation and Description
The difference in meaning between a syntactic expression and its "value", either as a normal form or as an equivalence class. Platonism and Formalism.
Laws as reduction rules; definitions of confluence and normalisation (stated for the λ-calculus in Section 2.3 and proved in Section 7.7). Transitive closure, zig-zags, connected components of graphs.
A novel example, the Lineland Army (which is in fact the free monoid-with-a-monad), shows how the proofs of confluence and of associativity of composition of normal forms amount to the same thing.
Russell's theory of descriptions, using "the" when a predicate has at most one witness, that need not exist. Extending this usage to uniqueness up to isomorphism, for objects such as products that are defined by universal properties.
1.3: Functions and Relations
Binary relations, with the new notation R:X _\-^\ Y for R ⊂ X×Y, suggested by the adjunction that it induces between their powersets (Section 3.8).
Partial and total functional relations (following on from the theory of descriptions). Arity, source and target: everything is typed. Relational algebra and terminology, including idempotents.
1.4: Direct Reasoning
By direct reasoning I mean what you can do without changing the context. The language of predicate calculus; direct logical rules; the symmetry between introduction and elimination. The provability relation and sequent presentation; structural rules; Gentzen's work.
1.5: Proof Boxes
The indirect (context-changing) rules using proof boxes: introduction of `implies' and `for-all', elimination of `or' and `for-some'. Hypotheses and generic elements: how to avoid certain fallacies; empty domains; negativity of the hypothesis. Translation between natural deduction and sequent presentations. β-reduction of proofs.
1.6: Formal and Idiomatic Proof
By the vernacular I mean semi-formal mathematical proofs expressed in English, French, ... prose; the stress is on idioms. The correspondence between the rules of natural deduction and words such as `let', `put', `suppose', `if ... then', `otherwise' and `in any case'. Using lemmas instead of boxes.
A novel account of the phrase `there exists', which both asserts the quantified predicate and opens its elimination-box, which is open-ended. Hilbert's epsilon is unnecessary.
The scope rules for boxes; the distributive and Frobenius laws; invariance under substitution (a recurring theme throughout the book).
Idioms for definition and `without loss of generality'.
Historical discussion: Frege, Hilbert, Ja\'skowski, Gentzen, Fitch.
Model theory: a "three sides of a square" treatment of logic. Comments on teaching logic.
1.7: Automated Deduction
What can and cannot be done mechanically; the dangers of formalisation. Theoretical basis: uniform proofs (statement and citation only). Goal-driven heuristics, Horn clauses, resolution, databases, pending goals, backtracking, unification (see also Section 6.5).
Box-proof heuristics: an explicit recipe for constructing uniform proofs in the box method, based on teaching first year computer science students.
1.8: Classical and Intuitionistic Logic
A potpourri. Excluded middle in various forms; Venn diagrams; truth tables; the difficulty with material implication; the Sheffer stroke; transistor `nand' gates.
Intuitionism: Ockham, Brouwer, Kolmogorov, Gödel, Hilbert. The axiom of choice; history; dependent choice.
Logic in a topos; generic objects; syntactically constructed worlds.
°: Exercises I
Of course, the exercises develop some of the topics in the text: only the highlights and novelties are mentioned here. Bo Peep's theorem, without which there would be no point in using numbers for counting. Proof boxes for linear logic.

II. Types and Induction

°: Introduction to Chapter II
The historical analogies between set theory and programming languages in the development of types. Points lie on lines: they do not constitute them. The importance of functions such as evaluation and product projection, rather than the substance of the types.
2.1: Constructing the Number Systems
A rational reconstruction of the need for Zermelo's axioms in the Dedekind and Cauchy-Cantor constructions of the reals. Constructions of function-spaces, quotients by equivalence relations, projective spaces and ideals.
Similar constructions for unions, etc. The difference between the singleton set and the singleton subset.
The construction of X+Y ⊂ P(X)×P(Y).
2.2: Sets (Zermelo Type Theory)
Zermelo's axioms, but with cartesian product and singleton instead of unordered pairs and the empty set. Comparison with 1970s interpretation of set theory in elementary toposes. The introduction, elimination, beta and eta rules for products, comprehension and powerset.
Discussion of notation for comprehension, subsets, parametric sets.
Historical comments on the Zermelo-Fraenkel axioms: extensionality and replacement are not trivial, foundation is unnatural; cardinality; the Skolem paradox; the Wiener-Kuratowski pair formula.
2.3: Sums, Products and Function-Types
Introduction to the lambda calculus; contexts; structural rules. The superficial similarity between the beta rule and cut (substitution). The sum type; case analysis; matching; distributive law. The commuting conversions are called continuation rules and denoted by z throughout the book.
2.4: Propositions as Types
The Curry-Howard analogy: an overstatement to call it an isomorphism. Church numerals; the S and K combinators. The Heyting-Kolmogorov interpretation of conjunction as pairs, implication as functions, etc. Programs out of proofs. Skeptical discussion of the constructive existential quantifier, with the complex square root function as counterexample. The existence and disjunction properties. Friedman-Coquand constructive interpretation of classical logic; continuations. Term- and type-assignment; the Cn notation.
2.5: Induction and Recursion
A novel treatment of well founded relations motivated by the sub-argument relation implicit in any recursive program (that fits a fairly general recursive paradigm). Such programs are analysed into three phases: parsing, parallel recursive calls and evaluation; this corresponds to the commutative diagram that we call the recursion scheme for coalgebras for a functor in Section 6.3.
Correctness proofs for such recursive programs. (One example is Gauss's second proof of the algebraic completeness of C.)
Simple or primitive induction, course-of-values or complete induction.
Classical idioms: minimal counterexamples, descending chains. Historical comments: Euclid, Fermat. König's tree lemma, termination of recursive programs. Proof trees.
2.6: Constructions with Well Founded Relations
Some larger examples of proof boxes (Section 1.5) to show how to do inductive proofs using the intuitionistic induction scheme instead of classical methods.
Complexity measures such as loop variants are based on the fact that functions which preserve the relation reflect its well-foundedness. Applications, such as to weak normalisation for the simply typed lambda calculus. Initial segments; lexicographic and other products.
2.7: Lists and Structural Induction
Lists and natural numbers are treated in parallel, beginning with Peano's axioms; car and cdr; concatenation; fold, map and applications.
Zero, successor, nil and cons as introduction rules; primitive recursion as the elimination rule. Predecessor and pattern matching. Monoid actions. Recursion invariants.
2.8: Higher Order Logic
Another potpourri. First order model theory; its cardinality properties; non-standard analysis.
The type of propositions; definability of the quantifiers and connectives; Leibniz' principle.
Cantor's diagonalisation theorem for the powerset; Galileo's comments on the follow of extending ideas from the finite to the infinite.
Second order polymorphic lambda calculus (System F). Impredicativity; universal properties; Poincaré and Weyl's objections. Answering them by distinguishing between specification and implementation.
°: Exercises II
Equivalence of the Dedekind and Cauchy-Cantor constructions, classically and constructively. Conway's multiplication formula. The von Neumann hierarchy. Characterisation of (head) normal forms in the lambda calculus; de Bruijn indices; combinatory algebra. Injective endofunctions of Ω.

III. Posets and Lattices

This chapter does for posets everything that is later done for categories; this is not as straightforward as categorists sometimes claim (partly because adjectives correspond to nouns), so there is some disproportionately difficult material towards the end. Some residues remain of the original plan to write a book about domain theory.

3.1: Posets and Monotone Functions
Posets; preorders; examples. Trichotomous (total or linear orders) and their misleading terminology. Monotone functions; upper and lower subsets.
Representation of orders by subset-inclusion; presheaves and the Yoneda lemma for posets; quotient poset of a preorder.
3.2: Meets, Joins and Lattices
Greatest and maximal elements; meets and joins; Examples: and, or, hcf and lcm for ideals.
Preservation and creation of meets (categorical terminology). Yoneda embedding preserves meets but freely adds joins. Diagrams; equivalent joins; cofinality.
Semilattices; lattices; the distributive law and normal forms.
3.3: Fixed Points and Partial Functions
The meaning of the recursive definition of the factorial function, as a fixed point of a functional applied to partial functions; criticism of this in that it does not capture the recursive paradigm of Section 2.5.
The poset of partial functions; lifting; information order; the "Tarski" fixed point theorem; other fixed point results.
3.4: Domains
Directed diagrams; ideals; examples. Directed-complete posets (dcpos); ipos (=cpos); Scott continuity; lift algebras (Freyd).
The Scott topology in terms of closed subsets first, then open subsets; intuitionistic disparity between these; the Sierpi\'nski space; finitely generated (compact) elements; algebraic dcpos.
3.5: Products and Function-Spaces
The componentwise and pointwise orders. Joint continuity, with counterexample from real analysis.
Historical discussion of Scott's thesis: Ershov, Myhill-Shepherdson, Rice-Shapiro, Strachey. Plotkin: PCF, computational adequacy, parallel or, sequentiality, full abstraction. Cartesian closed categories of domains and spaces: L-domains, Kelley. Synthetic domain theory.
3.6: Adjunctions
Adjunctions and Galois connections (contravariant adjunctions); universal properties; composition; equivalence functions. The adjoint function theorem; complete join- and meet-semilattices. Embedding-projection pairs; frames and complete Heyting (semi)lattices.
3.7: Closure Conditions and Induction
Closure operations as idempotent adjunctions. Closure conditions; examples in algebra; logic programming.
This is an original account of the induction scheme for a system of closure conditions - the propositional analogue of structural recursion for types. This is more general than well founded induction (Section 2.5), as it is non-deterministic. Many examples of induction arise in this way, but are often coerced into induction on natural numbers (rank), even though no numbers actually occur in the problem. Park induction deduces properties of fixed points of Scott-continuous operations from the base case and the operation; this is generalised to monotone operations on condition that property is Scott-continuous, i.e. the subset that it defines is closed under directed joins. Exercise 6.53 relates this to Zermelo's proof of well-ordering.
3.8: Modalities and Galois Connections
How any binary relation R:X _\-^\ Y gives rise to covariant and contravariant adjunctions between P(X) and P(Y).
The covariant ones are modal operators, [] and < > . S4 logic, where R is an order relation. Transitive closure; simpler proofs for Section 2.6. Total and partial correctness of programs; the core of a subgroup. Quantifiers, when R is a function.
The contravariant adjunctions are Galois connections. Specialisation order, `enough'. Examples: separable presheaves, Dedekind cuts, Leibniz' principle, points in an open subset, convergent sequences in a closed subset, annihilator subspaces, centraliser subgroups, number fields.
3.9: Constructions with Closure Conditions
An introduction at the poset level to sheaves and classifying categories. The Lindenbaum algebra for conjunction; every semilattice classifies some Horn theory; algebraic lattices.
Adding and preserving joins (developed, initially, without the usual requirement of stability under meets); coverages (Grothendieck topologies); canonical; subcanonical. Examples: ideals, Smyth powerdomain. Joins that are stable under meet; nuclei; Tychonov product.
Summary of how the remainder of the book generalises from propositions to types.
°: Exercises III
Irreflexivity. Bekic's lemma. Zorn's lemma. Boundedly complete domains; L-domains. Saturated closure conditions. (Bi)simulations and powerdomains. Schröder-Bernstein theorem.
Several proofs of Tarski's fixed point theorem, including Pataraia's intuitionistic proofs for ipos. Well founded elements of a lattice equipped with a successor operation (cf. well founded coalgebras, Section 6.3).
Gluing (cf. Section 7.7).

IV. Cartesian Closed Categories

Despite its title, this chapter does not actually get on to CCCs and the lambda calculus until Section 4.7. However, this is then an application of the correspondence between syntax and category theory that has already been set up in Section 4.3 at the algebraic level.

In algebra and topology it is easy to see why groups and homomorphisms, or spaces and continuous functions, form categories, so why is this so difficult for type theory? In fact this difficulty is the result of making a head-on attack on the equivalence between lambda calculus and categories as two accounts of the notion of function, and of equating objects with types.

But categories do not axiomatise functions: they encapsulate associativity. What is the fundamental associative operation in type theory? It is (composition of) substitution, and (as we like to use lots of variables together) the objects are not types but contexts.

The category of contexts and substitutions (a phrase chosen to echo the mathematical examples) is generated by an elementary sketch (Sections 4.2-4.3) whose equations are defined by the substitution lemma in Section 1.1. In type theory, more precisely the sequent calculus, the generating morphisms are called cut and weakening.

The same sketch defines the direct declarative programming language, including assignments. This sketch has a covariant imperative action on states, and a contravariant action that is equivalent to Floyd-Hoare logic.

By going via a sketch, the construction of the classifying category of a language in a certain fragment of logic avoids the technical difficulties that always arise from combining recursive and associative definitions. The objects and generating morphisms of the sketch are given directly by the syntactic classes of contexts, types and terms in the language.

Having set this construction up at the algebraic level, we may easily apply it to any fragment of logic. The syntax is already a category, so we may ask straight away about any universal properties that hold inside it. In particular, Section 4.7 makes the connection very simply between the universal property of the exponential in category theory and the syntax for function-abstraction and function-types, with the beta and eta laws, in the lambda calculus.

The construction of the sketch is extended to generalised algebraic theories (dependent types) in Chapter VIII, and then the universal properties and type-theoretic rules for the quantifiers are investigated in Chapter IX. The correspondence between β, η and λ and the anatomy of an adjunction is set out in Section 7.2.

Returning to take a more critical look at the usual mathematical examples of categories, we notice that the "obviousness" that models and homomorphisms form categories is a peculiarity of (simply-typed) algebra: there is no single compelling notion of morphism for models of first order theories in general, or even for spaces or generalised algebras such as categories. In fact, the traditional motivation for the notion of category - collecting all the models and then trying to recover the theory - is as much a "three sides of a square" approach to logic as is classical model theory (Section 1.6).

The well known shortcomings of traditional category theory - the size problems, and the lack of extension from algebra to first order logic - disappear as soon as we recognise the classifying category (of contexts and substitutions) as the primary notion, and the category of models as a secondary one with limited applicability.

4.1: Categories
A fairly standard introduction to categories as congregations (with the usual list of examples) and as structures. The correspondence between order-theoretic and categorical notions. Historical examples of groups. Size issues.
4.2: Actions and Sketches
Actions of monoids; faithful actions; Rubik's cube; Cayley's theorem.
Elementary sketches; unary algebraic theories. Free theories; lists; paths through oriented graphs; regular grammars; automata; polyhedra. Commutative diagrams; Freyd's punctures.
Models; clones; free categories; soundness; completeness.
Canonical elementary language, which others call the "internal" language, but it is not internal in the sense of "internal category" etc.; I really prefer the word "proper" (in the sense of the French "propre"), but this is actually the same as "canonical (Grothendieck) topology" in Section 3.9.
4.3: Categories for Formal Languages
The direct declarative language: put (elsewhere known as let), discard, skip and composition. Covariant operational interpretation; initialisation; continuation; assignment.
Example: the solution of cubic equations by radicals.
Contravariant logical interpretation; Floyd-Hoare logic; pre-, post- and mid-conditions; weakest preconditions and substitution.
The substitution lemma and normal form theorem; in reverse: compilation; discussion of discard (which appeared in Floyd's paper).
The construction of the classifying category from an elementary sketch based on the substitution lemma: see above.
Display maps; terms as sections; discussion of the use of variables; open α-equivalence.
4.4: Functors
Definition; covariant; contravariant; monotone functions; homomorphisms; presheaves; semifunctors. Forgetful functors: forgetting structure, properties or both.
Classifying category for a unary theory, i.e. the free category on a sketch.
The force of functoriality: non-examples, isomorphism-invariants.
Full and faithful; essentially surjective; full and wide subcategories; equivalence functors; examples. Misleading uses of "forgetful".
Replete functors and subcategories, the definition being chosen to characterise those functors for with the strict and pseudo-pullbacks against any functor are weakly equivalent.
4.5: A Universal Property: Products
Continuation of the discussion of impredicativity and the Leibniz principle from Section 2.8, and of the definite article ("the") from Section 1.2; cf. superlatives and comparatives in French and Italian.
The quantified variable that occurs in universal properties defining right adjoints is, throughout the book, written as Γ (Gamma) - rather than a randomly chosen letter - to emphasise the connection with (unspecified) contexts in type theory. Θ (Theta) is used for left adjoints.
The terminal object; global elements; local (generalised) elements = terms in un unspecified context Γ; examples from recursion theory showing the difference; class of generators; well pointed (weak and strong senses); concrete.
Laboured proof of uniqueness up to unique isomorphism.
Binary products; examples; preservation and creation; left-associated multiple products.
Discussion of language in the use of the existence of products; the need or otherwise for Choice.
Universal properties define functors.
All universal properties are terminal objects; discussion of simple categorical constructions by analogy with modular programming.
4.6: Algebraic Theories
Definition; homomorphism; discussion of the need for uniqueness of products up to isomorphism, but not for a choice of them.
Examples: Horn theories; magma; context-free languages; internal monoids and groups; rings with modules; generators and relations. Non-examples: lists, fields, projective planes.
Semantics of expressions; Scott's semantic brackets; Yacc. The classifying category and its universal property; completeness.
4.7: Interpretation of the Lambda Calculus
The builds on the algebraic construction as described above. Initially, the raw lambda calculus (without the beta and eta rules) is considered, partly in order to dispel the common misconception that category theory is unable to do this; the use of 2-categories to handle reduction paths is mentioned in Exercise 4.34.
Raw cartesian closed structure in a category; naturality of abstraction with respect to substitution; Currying; interpretation. The beta- and eta-rules; universal property; exponential transposition; discussion of notation.
Examples: Heyting semilattices; C-monoids; Set, Pos, Dcpo. A "four-point plan" is given for verifying that such a category is cartesian closed, summing up the calculations from Section 3.5.
4.8: Natural Transformations
Definition; composition; middle-four interchange; functor categories. Examples: function evaluation and abstraction, product pairing and projections, algebra homomorphisms, products of groups and categories. Strong and weak equivalences; equivalence functors. Yoneda embedding and lemma; representable functors. 2-categories and bicategories; examples.
°: Exercises IV
Simplicial complexes. Karoubi idempotent completion. CSLat as a *-autonomous category; the associated cartesian closed category. Lawvere algebraic theories. Skeletal categories and groupoids. Homotopy categories (fundamental group of a space). Dinaturality; fixed point operators.

V. Limits and Colimits

This chapter shows how much of the familiar structure of algebra may be found simply by looking for the limits and colimits in various categories. The behaviour of these is rather more diverse than an abstract treatment of category theory may suggest. In particular it is shown why, in order to interpret if then else, coproducts must be stable and disjoint, as they are for sets but not for most algebras.

5.1: Pullbacks and Equalisers
Definitions; product; meet; most general unifier; intersection; inverse image; Church-Rosser theorem. Slice categories; substitution; equality objects; the graph of a function; pullback as a functor between slices.
5.2: Subobjects
Monos, epi, regular, split. Pullback and composition properties; The lattice of subobjects; well powered; subobject classifier; topos.
Sets of solutions of algebraic equations; conjunction; unique existential quantification; essentially algebraic theories; discussion (cf. Chapter VIII).
Special subobjects; class of supports (dominion); classifier (dominance); Examples: open, upper and recursively enumerable subsets.
5.3: Partial and Conditional Programs
In the category that was constructed in Section 4.3 from the direct declarative language, the objects were simply the types of the program variables and the logic played a superficial role. This is a surrender to the programmers' fallacy that the meaning of a program is given by machine instructions and the contents or program variables. Now the objects (called virtual objects because of the way that they are already implicit in programs) are the full contexts of predicate calculus: types and predicates.
By giving the Floyd-Hoare mid-conditions first class status, the category defined by a programming language looks increasingly like the category of sets and functions as used in mathematics. The types that naturally occur in algorithms are mathematical ones, given some machine representation as {[(x)\vec] ∈ N^k|φ[[(x)\vec]]}, where φ is the mid-condition. This section develops partial functions in terms of subobjects and applies them to if then else, which is shown in Section 5.5 to have the same categorical characterisation as disjoint unions of sets.
5.4: Coproducts and Pushouts
This section is about coproducts in categories that are unsuitable for interpreting conditional programs. It dispels the misconception that coproducts are merely dual products by exploring the many different ways in which they behave in categories of traditional interest in pure mathematics: those of algebras and spaces.
Definition; codiagonal; initial object; empty set. Disjoint union; Boolean type; variant fields; exceptions; overloading.
Abelian categories; zero map; biproduct or direct sum; non-distributivity. CMon-enriched (additive) categories; homological algebra; exactness. Limit-colimit coincidences.
Stone duality: the modularity or distributivity properties of congruence lattices in certain categories of algebras suggests that they should be seen as the opposites of categories of spaces. Coproducts in CRng and Frm as tensor products.
Van Kampen's theorem: the importance of free coproducts beyond symbolic logic.
5.5: Extensive Categories
Disjoint unions of sets axiomatised as stable disjoint coproducts appeared in the work of the Grothendieck school, but this section uses the Lawvere-Schanuel notion of extensive category. The account is based on that of Carboni, Cockett, Lack and Walters but the proofs are more efficient.
Distributivity; binary sums in type theory; strict initial object. Extensive categories; examples; equivalence with stable disjoint coproducts. Disjunctive theories; exceptions in programming languages.
5.6: Kernels, Quotients and Coequalisers
Kernel pair; examples: normal subgroups, ideals; congruences. Coequalisers and quotients; congruences and regular epis as the fixed points of a Galois connection.
Effective quotients in Set and Mod(L), where L is a finitary simply-typed algebraic theory; the need for Choice in the infinitary case; projectivity.
Constructing general coequalisers in Set; simpler construction by duality in CSLat.
5.7: Factorisation Systems
Orthogonality; factorisation and prefactorisation systems; stability under pullback.
Image factorisation into regular epis and monos; examples: congruences and quotients of algebras, separable field extensions, subspace and quotient topologies, dense subspaces, cofinal maps; non-examples because regular epis or monos do not compose.
Composition, cancellation and pullback properties. Example of a prefactorisation system in a poset. Special adjoint functor theorem.
5.8: Regular Categories
Lex (finite limit) categories; regular categories; effective regular (Barr-exact) categories; Abelian categories; prelogos; pretopos.
Examples and counterexamples: algebras, regular rings, compact Hausdorff spaces, posets. A regular category need not have coequalisers other than of congruences, and those that it does have need not be stable.
Regular epis compose in a regular category, giving image factorisation. Four notions of surjective function.
Relational algebra: the need for pullback-stability; allegories.
Unions; Heyting implication; division allegories; Lambek calculus. Pretoposes: the elementary properties of Set.
°: Exercises V
Split (absolute) coequalisers and pushouts. PERs. Subobject classifier for presheaves. p-categories. Coproduct of C₂ and C₃ in Gp. Pushouts of inclusions of sets, posets, domains, lower subsemilattices of a distributive lattice. Implementation of variant records. Converses of the relationships between pullbacks and coequalisers - some difficult diagram-chasing!

VI. Structural Recursion

6.1: Free Algebras for Free Theories
The problems with infinitary algebraic theories (5.6.9) arise from the laws, so do not apply to free theories. Internal theories; infinite arities expressed as objects in the model; internal systems of operations. Algebras and homomorphisms; expressed as algebras for a functor ev:T X→ X.
Equationally free, parsable and free algebras; the Peano and Lawvere axioms; Lambek and Smyth-Lehman lemmas. Lists and streams.
Infinitary conjunction and disjunction; validity in models of first order theories; strictness analysis.
Construction of (equationally) free algebras using powersets of lists.
6.2: Well Formed Formulae
Since type-theoretic rules involve pattern matching and side conditions, the syntactic classes that they generate are not full free algebras: they are not closed "upwards" under the algebraic operations, but they are closed "downwards" with respect to parsing. Such a subset of a free algebra is called a wff-system (well formed formulae). This section is a survey of the uses of wff-systems, with a view to constructing internal classifying categories, in particular with application to Gödel's incompleteness theorem (9.6.2).
Recursive covers; examples: Rubik's cube, provability, PERs, Collatz' problem.
Variables; many-sorted theories; the free category on a graph; Polish notation; free algebras for finitary theories; formation rules in type theories.
Discussion of infinitary theories with laws and the need for Choice; counterexample to the existence of constructive proofs for provable propositions; cf. Example 2.4.8, Theorem 5.6.9, Exercise 6.12.
6.3: The General Recursion Theorem
By the "general recursion theorem" I mean the traditional result from (the ordinals and) set theory that says that induction is sufficient for recursion. This section is original research that will also appear in more detail in a journal paper. It introduces well foundedness for a coalgebra parse: X→ T X for a functor in terms of a certain pullback diagram, and proves that from such a coalgebra there is a unique map satisfying Osius's categorical recursion scheme into any algebra for the same functor (cf. the recursive paradigm in Section 2.5). In particular this characterises the initial algebra for the functor as a well founded coalgebra whose structure map is an isomorphism. In the case of the covariant powerset functor, there is no initial algebra, but the extensional well founded coalgebras are transitive sets in the sense of set theory; this is extended to ordinals in Section 6.7. Exercises 6.23ff show how to deal with parameters.
6.4: Tail Recursion and Loop Programs
This is a development of the application of Set-like categories to imperative programming languages: thinking of a program as a partial function between sets of states, what categorical structure interprets while? In 1984, my answer was a coequaliser that is stable under pullback, but now I would draw an equivalent diagram that is a special case of the previous section.
Each exit state of the loop corresponds to a component of the transition graph with a fixed point. The idea of the the coequaliser is to get (mathematical) access to this component and its properties via the kernel of the coequaliser. The result depends on the exactness properties of a pretopos (Section 5.8), plus pullback-stability of the equivalence closure of a relation. The argument actually goes back to Frege's account of transitive closure in the Begriffsschrift, whilst the categorical property is Freyd's characterisation of N in terms of a coproduct and a coequaliser. Freyd's allegories are also used to extend the result to pretoposes that do not have all N-indexed unions.
The Floyd-Hoare correctness rules are justified on this basis. Exercise 6.26 shows, categorically, how to use an accumulator to reduce unary recursion (i.e. with at most one sub-call) to tail recursion.
6.5: Unification
This is an original account of unification (for the usual case of finitary free algebraic theories), with a smooth development from ideas of universal algebra to a very fast algorithm suitable for microcoding. Just as the kernel of any homomorphism is a congruence (both an equivalence relation and a subalgebra), so the kernel of a homomorphism between equationally free algebras is closed "downwards" with respect to parsing, from which the basic idea of matching in the unification algorithm follows, along with the "clash" failure. The mathematical idea is to form the closure of the given system of equations to form a parsing congruence, but we observe that closure under the operations and transitivity is redundant. The algorithm is read off from this result. The "occurs" failure arises from well-foundedness of the sub-argument relation in a free algebra.
6.6: Finiteness
The Kuratowski and discrete notions of finiteness are presented as yet another example of the propositions-types correspondence. They are also compared with the analogous notions in algebra of being finitely generated or presented (and with LFP categories). By analysis of the rules for the existential quantifier (cf. Section 1.6) in the definition of finiteness as listable, we find (perhaps surprisingly) that the usual classical idioms that a finite set can be assumed to be listed are formally valid, even in the case of Kuratowski-finiteness.
6.7: The Ordinals
The traditional theory of the ordinals is riddled with uses of excluded middle, and the account in my 1996 JSL paper Intuitionistic Sets and Ordinals is very complicated. There are in fact several different intuitionistic notions, differing in the construction and properties of the successor and the pre-conditions of transfinite induction and iteration. This section is a traditional account (successors, limits, predecessors, transfinite induction and recursion with parameters, rank, arithmetic, Cantor normal forms, equivalents of the axiom of choice), carefully phrased to be consistent with the intuitionistic version, but at the cost of some of the details. However, it ends with a summary of my JSL paper, the work of Joyal and Moerdijk, and the extension of the categorical theory in Section 6.3.
°: Exercises VI
Using the recursion scheme (as a commutative diagram) to transform programs. A new proof of κ²=κ for cardinals.

VII. Adjunctions

7.1: Examples of Universal Constructions
Colimits, free algebras, polynomials, discrete structure, completions and quotients, reflective subcategories, components, Mostowski's extensional quotient.
Co-universal properties: limits, exponentials, indiscriminate (indiscrete) structure, streams. Symmetric adjunctions: dual spaces, C-monoids, the Lineland Army. Two-sided adjunctions: splitting idempotents, Gp ⊂ Mon.
Classifying categories; universal property: models of a [] -theory in a category C with appropriate structure to interpret [] correspond to functors Cn^[]_L→C that preserve this structure. The analogy with polynomials; difficulties: structure defined by universal properties rather than being chosen, the axiom of replacement, what is a language morphism? Historical comments on classifying toposes.
7.2: Adjunctions
The equivalence amongst various notions of adjunction; reflective subcategories; representable functors.
An original treatment of the way in which each part of the anatomy of an adjunction (including the correspondence, unit, co-unit and triangle laws) corresponds to one of the type-theoretic rules. The difference in idiom between initial algebras and left adjoints. Adjoints in 2-categories; comments on how much commoner (and less remarkable) adjunctions are than novices suppose.
7.3: General Limits and Colimits
Diagram-shapes: definition and survey. Adjoints preserve (co)limits; applications. Comma categories; pseudo-pullbacks; final functors; examples. Equivalent colimits; Freyd's general adjoint functor theorem; solution-set condition; it's better to describe the adjunction explicitly.
7.4: Finding Limits and Free Algebras
Limits and colimits in topology and order theory: components, discrete structure, underlying set, indiscriminate structure; "soft" constructions of all limits and colimits in Sp and Frm apart from the topology on a limit (which can be seen "softly" in terms of fibrations, Section 9.2). Generators and relations; canonical language; computing colimits. Treating the system of relations as another (dependent-type) theory.
7.5: Monads
Algebras for functors and for monads: dynamic versus static; the categorical analogue of closure conditions and operations (Section 3.7); recursion for functors (Section 6.3).
Definition; algebras; the Kleisli and Eilenberg-Moore categories; examples: Rel ⊂ CSLat, vector spaces, domains and lift-algebras. Creating limits and (some) colimits; contractible coequalisers; Beck's theorem; Paré's theorem for the contravariant powerset. Applications: finitary theories; Linton; Kock-Zöbelein; transfinite recursion; Moggi; Beck homology.
7.6: From Semantics to Syntax
Given a category C with [] -structure (products, exponentials, etc.), this section shows how to construct the canonical language L ("internal" language elsewhere) so that C is equivalent to Cn^[]_L, the equivalence being strong or weak depending on whether the structure in C is chosen or just defined up to isomorphism.
Encoding operations; finite product sketches, interpretations; Horn theories (Section 3.9);
Subcanonical, weakly canonical and strongly canonical languages; how categorical equivalences preserve structure; conservativity; the equivalence theorem. This is an example of a situation that is obviously an adjunction, apart from naturality of the co-unit, which is the issue to be proved.
Proving conservativity syntactically (by normalisation) for products, sums and exponentials.
7.7: Gluing and Completeness
Also known as Artin-Wraith gluing, sconing or the Freyd cover, this is introduced as a survey of the things that you can prove by investigating adjunctions and pullbacks. Freyd's construction is used to prove the existence and disjunction properties, consistency an strong normalisation for the lambda calculus. It does, however, depend on the axiom of replacement (Section 9.6).
°: Exercises VII
Exponential ideals. Finitely related objects. Disjunctive theories. The 2-category of adjunctions in a 2-category; iterating this. Stable functors and candidates. Cartesian closed categories from models of linear logic.

VIII. Algebra with Dependent Types

This chapter investigates categories with display maps, which were introduced in my 1987 PhD thesis. It proves in detail (as my thesis did not) the equivalence between this notion and that of a generalised algebraic theory. Briefly, a display map forgets the last variable from a context, and pullback effects substitution. The category is generated by an elementary sketch, as in Section 4.3.

This structure is the generalisation of Freyd's notion of "essentially" algebraic theory (encoded as a category with all finite limits) that is needed when the syntactic and semantic categories do not have all such limits. It was needed in my thesis to define dependent products in categories of domains.

°: Introduction to Chapter VIII
The need for dependent types in mathematical arguments; historical comments on how these have been handled; Cartmell's contextual categories. Pitts's type-theoretic rules: these were my starting point, but after it had taken me two weeks and a double induction to prove the existence of identities in his category, I came up with the sketch construction in Sections 4.3 and 8.2.
8.1: The Language
Terms; equality of terms; dependent types; equality of types; the role of the object-language. The theory of categories as an example. The well-foundedness condition that the language must obey to justify the recursive construction of the interpretation. Stratified algebraic theories as a stronger such condition: the classifying category in this case is the top of a tower of fibrations, each of which is given by a simply typed theory internal to the level below.
8.2: The Category of Contexts
The construction of the sketch and the category. The objects (contexts); context equality; the generating morphisms: displays (weakening) and sections (cuts); the laws (displayed as diagrams). The normal form theorem. Proof that substitution is pullback.
8.3: Display Categories and Equality Types
Discussion of pullback-stable classes of maps in topology and elsewhere. Display maps. The extreme cases: products and all finite limits; equality types; discussion of the meaning of quantifiers with respect to equality types. Relative slices; the semantic version of the normalisation theorem.
8.4: Interpretation
A concise way of setting out the language in a categorical form, suitable for describing the interpretation. Histories of formation; interpretation. Description of the canonical language; completeness theorem. Using mixed categorical and type-theoretic notation.
°: Exercises VIII
Examples of stratified and non-stratified theories.

IX. The Quantifiers

The historical basis of the category theory contained in this chapter is the work of Lawvere on the quantifiers and of Bénabou on families of infinitary limits and colimits around 1970. These were both based on fibrations, which remain the most widely used tool of categorical logicians working in this area. Despite writing a thesis about them, I am a heretic in that I regard fibrations as an unnecessarily complicated language in which to work. I use display maps (Chapter VIII) instead.

One reason for my attitude is that my own interest was originally not in pure categorical logic, but the interpretation of polymorphic lambda calculi in categories of domains. These typically do not have all of even the basic structure (finite limits) that Bénabou-Lawvere categorical logic demanded. There is, however, a well defined, albeit slightly different question: how much of a language (for instance with dependent products) can one soundly interpret in a given category? This question is of the same form as asking what function-types (exponentials) exist in a category: there is a scheme of universal properties, and we want to know which instances of them are satisfied. Fibrations rightly ask that these properties be parametric, and invariant under substitution, but these conditions translate exactly into pullback-stability of the relevant universal properties.

In this way, Sections 9.3 and 9.4 demonstrate the precise translations between the type-theoretic rules (in the style of, say, Martin-Löf) and universal properties.

9.1: The Predicate Convention
Hitherto, the propositions-types dichotomy has been one between preorders and categories: whether we state as a fact that x ≤ y or distinguish arrows x→ y. As presented in this chapter, the categorical and type-theoretic rules are equally applicable to both situations. Where `propositions' and `types' now differ is in the roles that they play in the quantifiers: the range of the quantifier ∃x is a type, its body φ[x] is a proposition.
Overview of classes of display maps, fibrations, the syntactic quantifier formation rules, the indirect rules (∀ℑ and ∃E) as adjunctions, substitution and the Beck-Chevalley condition, the recursive definition of the interpretation functor.
9.2: Indexed and Fibred Categories
As I dislike fibrations but am surrounded by people who use them, I spent some time trying to understand for myself what they were for. Throwing the abstract categorical definition at the reader, as is usually done, does not explain this. The answer is that it captures the situation in which propositions (predicates) depend on typed-variables, but types do not depend on proofs. Several equivalent formulations are given, in terms of conservative extensions of (stratified) algebraic theories (Section 8.1) and classes of display maps. The usual definitions and Grothendieck construction are given.
However, the traditional categorical examples employ categories of models, whereas our explanation is in terms of syntax (classifying categories or categories of contexts and substitutions), so a result is sketched that shows how bifibrations of models arise from fibrations of theories. Restriction and induction of modules for rings arise in this way, as do the standard notions of variable domain, where x ≤ y gives rise to an embedding-projection pair between D[x] and D[y].
The terms prone and supine are introduced for the forward and backward orthogonals of vertical maps; prone maps are elsewhere called cartesian.
The fibrational technology was first introduced to describe topological group extensions. Discrete and geometric examples of split and non-split extensions are given. The cocycle condition and first cohomology group are recovered from their categorical versions.
9.3: Sums and Existential Quantification
In its progressively more complicated forms, the dependent sum arises as binary products, composition of display maps, a left adjoint to pullback and stable factorisation systems. The type-theoretic weak and strong sum rules are written in the categorical language developed in Chapters IV and VIII and thereby shown to be universal properties. The name verdict is introduced for the map that arises from the introduction rule, usually referred to as pairing, which is the unit of the adjunction; the letters ve stress the duality with ev for the dependent product. The Beck-Chavelley condition is invariance under cut, substitution or pullback. The required notion of factorisation system is shown to be slightly weaker than that introduced in Section 5.7. Open maps provide an example of the interpretation of dependent sums in topology.
9.4: Dependent Products
In the Bénabou-Lawvere presentation, the dependent product is the right adjoint to pullback, with the Beck-Chevalley condition, but again we translate the type-theoretic rules into universal properties described in various ways.
As I have said, I came into this subject from domain theory, though I am now interested in categories with similar "deficiencies" but constructed in different ways. In such categories, the semantic calculations are already rather difficult, perhaps involving non-trivial lattice theory or topology. For this reason, it is essential that the universal properties to be tested for the interpretation of type theory be as simple as it is possible to make them.
The literal type-theoretic formulation involves a certain complication, which turns out exactly to cancel the complication involving the Beck-Chevalley condition, with the effect that the strict definition is equivalent to a type-theoretically naïve one that also appears in the categorical literature from the 1970s with the name "exponentiability".
The last half of the section shows that an even more drastic simplification can be made, with the result that the Beck-Chevalley condition does the work for us, instead of being an extra burden, as it is with the notion of hyperdoctrine. The calculation of general dependent products can be reduced to (certain pullbacks and) so-called partial products, which are slightly more complicated than function-spaces, but not much. They first appeared, in geometric topology, in 1965, and, as people gradually notice their importance, more and more idioms of construction are being recognised as examples.
9.5: Comprehension and Powerset
Whereas I have argued that fibrations complicate the presentation of dependent sums and products, they are clearly the simplest way of understanding the axiom of comprehension: it is simply one of a string of adjoints that also involves the fibration functor itself. However, Exercises 9.45ff question the adequacy of this as an explanation of comprehension as a type-forming operation in set theory.
For higher-order logic, we distinguish between the name of a type or proposition and its substance, setting out the rules for the type of such names. When the eta (extensionality) law holds, proofs are anonymous and comprehension is available, the type of propositions is a support-classifier or dominance (Section 5.2). It is a topos-theoretic subobject classifier when all monos are classified by propositions, which happens iff all quantifiers are present.
The eta rule conflicts with other customs in type- and category theory, so the extent of its relevance to mathematics is discussed.
9.6: Universes
The whole development of the book is designed to be enough to build internal models of the world within itself. Amongst models are free ones (term models, capturing provability) and submodels, in which the names denote "small" objects, and the structure is the true structure. Gödel's incompleteness theorem shows that these are quite different.
An internal submodel is a type of types in the sense of the previous section. Russell's paradox shows that this cannot be the entire model, if this is to have equality and function-types in the traditional mathematical sense, but such things are possible in categories of domains.
The construction of submodels in set theory and domain theory is not possible within the Zermelo or topos axioms, but needs (part of) the axiom-scheme of replacement. Set theory obfuscates this axiom particularly badly, but it can be regarded as saying that we may form set-indexed unions of sets.
However, the axiom of replacement has a more profound significance in logic than this. In type theory, (part of) it is Mart-in-Löf's notion of universe. The force lies, not in the existence of a term model, but in the recursive construction of its interpretation. This is illustrated by the amazing power of the gluing construction (Section 7.7). As an original piece of research, I also give a categorical formulation of it, as a way of saying that transfinite iterated of functors exist, based on the categorical theory of ordinals in Sections 6.3 and 6.7.
°: Exercises IX
Various notions that are equivalent to fibrations, including cartesian factorisation systems (cf. Section 5.7). Limits and colimits calculated using fibrations; lax colimits. Equivalent forms of the Beck-Chevalley condition for sums. Applications of partial products, including to fundamental groups. Joyal-Moerdijk universes.

Bibliography

Includes items in philosophy of language as well as mathematics and computer science, in order to take the reader as far afield as possible. Short papers just containing one result that is already fully covered in the book are not included.

Index

A summary of the book in alphabetical order. Having done this twice now, equipped with makeindex and grep, I still think that compiling an index for a book is a black art.

This is www.PaulTaylor.EU/Practical-Foundations/summary.html and it was derived from prafm/summary.tex which was last modified on 22 July 2007.