# Practical Foundations of Mathematics

### Paul Taylor

Practical Foundations of Mathematics

# Practical Foundations of Mathematics

### Paul Taylor

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

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

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
3.7
Closure Conditions and Induction
3.8
Modalities and Galois Connections
3.9
Constructions with Closure Conditions
Exercises  III

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

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

Introduction
6.1
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

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

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

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