https://www.paultaylor.eu/prafm/html/index.html

                Practical Foundations of Mathematics

                             Paul Taylor

                Practical Foundations of Mathematics

                             Paul Taylor

                     Cambridge University Press

INTRODUCTION

I    FIRST ORDER REASONING

    Introduction
1.1 Substitution
1.2 Denotation and Description
1.3 Functions and Relations
1.4 Direct Reasoning
1.5 Proof Boxes
1.6 Formal and Idiomatic Proof
1.7 Automated Deduction
1.8 Classical and Intuitionistic Logic
    Exercises  I

II    TYPES AND INDUCTION

    Introduction
2.1 Constructing the Number Systems
2.2 Sets (Zermelo Type Theory)
2.3 Sums, Products and Function-Types
2.4 Propositions as Types
2.5 Induction and Recursion
2.6 Constructions with Well Founded Relations
2.7 Lists and Structural Induction
2.8 Higher Order Logic
    Exercises  II

III    POSETS AND LATTICES

    Introduction
3.1 Posets and Monotone Functions
3.2 Meets, Joins and Lattices
3.3 Fixed Points and Partial Functions
3.4 Domains
3.5 Products and Function-Spaces
3.6 Adjunctions
3.7 Closure Conditions and Induction
3.8 Modalities and Galois Connections
3.9 Constructions with Closure Conditions
    Exercises  III

IV    CARTESIAN CLOSED CATEGORIES

    Introduction
4.1 Categories
4.2 Actions and Sketches
4.3 Categories for Formal Languages
4.4 Functors
4.5 A Universal Property: Products
4.6 Algebraic Theories
4.7 Interpretation of the Lambda Calculus
4.8 Natural Transformations
    Exercises  IV

V    LIMITS AND COLIMITS

    Introduction
5.1 Pullbacks and Equalisers
5.2 Subobjects
5.3 Partial and Conditional Programs
5.4 Coproducts and Pushouts
5.5 Extensive Categories
5.6 Kernels, Quotients and Coequalisers
5.7 Factorisation Systems
5.8 Regular Categories
    Exercises  V

VI    STRUCTURAL RECURSION

    Introduction
6.1 Free Algebras for Free Theories
6.2 Well Formed Formulae
6.3 The General Recursion Theorem
6.4 Tail Recursion and Loop Programs
6.5 Unification
6.6 Finiteness
6.7 The Ordinals
    Exercises  VI

VII    ADJUNCTIONS

    Introduction
7.1 Examples of Universal Constructions
7.2 Adjunctions
7.3 General Limits and Colimits
7.4 Finding Limits and Free Algebras
7.5 Monads
7.6 From Semantics to Syntax
7.7 Gluing and Completeness
    Exercises  VII

VIII    ALGEBRA WITH DEPENDENT TYPES

    Introduction
8.1 The Language
8.2 The Category of Contexts
8.3 Display Categories and Equality Types
8.4 Interpretation
    Exercises  VIII

IX    THE QUANTIFIERS

    Introduction
9.1 The Predicate Convention
9.2 Indexed and Fibred Categories
9.3 Sums and Existential Quantification
9.4 Dependent Products
9.5 Comprehension and Powerset
9.6 Universes
    Exercises  IX

BIBLIOGRAPHY

INDEX