Practical Foundations of Mathematics

Paul Taylor

IX. The Quantifiers

INTRODUCTION

9.1    THE PREDICATE CONVENTION

• Classes of display maps
• Fibrations
• The quantifier formation rules
• Adjointness in foundations
• Substitution and the Beck-Chevalley condition
• The recursive definition of interpretations

9.2    INDEXED AND FIBRED CATEGORIES

• Separating propositions from types
• Fibrations
• Models
• Coherence issues

9.3    SUMS AND EXISTENTIAL QUANTIFICATION

• Dependent sums and composition
• Sum-introduction
• Unsubstituted weak sums and the adjunction
• Substitution and the Beck-Chevalley condition
• Semantics and open maps
• Strong sums

9.4    DEPENDENT PRODUCTS

• Application and abstraction
• The adjunction, Beck-Chevalley condition and other forms
• Local cartesian closure
• Partial products
• Partial products suffice

9.5    COMPREHENSION AND POWERSET

• Comprehension
• The type of propositions

9.6    UNIVERSES

• Gödel's incompleteness theorem
• Full internal subcategories
• Russell's paradox
• The axiom-scheme of replacement
• Infinite limits and colimits
• Avoiding replacement
• Transfinite iteration and fixed points of functors

EXERCISES  IX