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 (

**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.

**°****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 Ω.

**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).

**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.

**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*pre*factorisation 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*_{2}and*C*_{3}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!

**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 list*able*, 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 κ^{2}=κ for cardinals.

**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.

**°****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.

**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.

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.