PRINCIPIA MATHEMATICA

By ANTHONY CLARK

CONTENTS INTRODUCTION I FOUNDATIONS TYPE THEORY TYPE THEORY VERSUS SET THEORY FUNCTION TYPES UNIVERSES AND FAMILIES DEPENDENT FUNCTION TYPES (?-TYPES) PRODUCT TYPES DEPENDENT PAIR TYPES (?-TYPES) COPRODUCT TYPES THE TYPE OF BOOLEANS THE NATURAL NUMBERS 1 10 PATTERN MATCHING AND RECURSION 1 11 PROPOSITIONS AS TYPES 1 12 IDENTITY TYPES NOTES EXERCISES HOMOTOPY TYPE THEORY TYPES ARE HIGHER GROUPOIDS FUNCTIONS ARE FUNCTORS TYPE FAMILIES ARE ?BRATIONS HOMOTOPIES AND EQUIVALENCES THE HIGHER GROUPOID STRUCTURE OF TYPE FORMERS CARTESIAN PRODUCT TYPES ?-TYPES THE UNIT TYPE ?-TYPES AND THE FUNCTION EXTENSIONALITY AXIOM 2 10 UNIVERSES AND THE UNIVALENCE AXIOM 2 11 IDENTITY TYPE 2 12 COPRODUCTS 2 13 NATURAL NUMBERS 2 14 EXAMPLE: EQUALITY OF STRUCTURES 2 15 UNIVERSAL PROPERTIES SETS AND LOGIC SETS AND N-TYPES PROPOSITIONS AS TYPES? MERE PROPOSITIONS CLASSICAL VS INTUITIONISTIC LOGIC SUBSETS AND PROPOSITIONAL RESIZING THE LOGIC OF MERE PROPOSITIONS PROPOSITIONAL TRUNCATION THE AXIOM OF CHOICE THE PRINCIPLE OF UNIQUE CHOICE 3 10 WHEN ARE PROPOSITIONS TRUNCATED? 3 11 CONTRACTIBILITY EQUIVALENCES QUASI-INVERSES HALF ADJOINT EQUIVALENCES BI-INVERTIBLE MAPS CONTRACTIBLE ?BERS ON THE DE?NITION OF EQUIVALENCES SURJECTIONS AND EMBEDDINGS CLOSURE PROPERTIES OF EQUIVALENCES THE OBJECT CLASSI?ER UNIVALENCE IMPLIES FUNCTION EXTENSIONALITY INDUCTION INTRODUCTION TO INDUCTIVE TYPES UNIQUENESS OF INDUCTIVE TYPES W-TYPES INDUCTIVE TYPES ARE INITIAL ALGEBRAS HOMOTOPY-INDUCTIVE TYPES THE GENERAL SYNTAX OF INDUCTIVE DE?NITIONS GENERALIZATIONS OF INDUCTIVE TYPES IDENTITY TYPES AND IDENTITY SYSTEMS HIGHER INDUCTIVE TYPES INTRODUCTION INDUCTION PRINCIPLES AND DEPENDENT PATHS THE INTERVAL CIRCLES AND SPHERES SUSPENSIONS CELL COMPLEXES HUBS AND SPOKES PUSHOUTS TRUNCATIONS 6 10 QUOTIENTS 6 11 ALGEBRA 6 12 THE ?ATTENING LEMMA 6 13 THE GENERAL SYNTAX OF HIGHER INDUCTIVE DE?NITIONS HOMOTOPY N-TYPES DE?NITION OF N-TYPES UNIQUENESS OF IDENTITY PROOFS AND HEDBERG’S THEOREM COLIMITS OF N-TYPES CONNECTEDNESS ORTHOGONAL FACTORIZATION MODALITIES II MATHEMATICS HOMOTOPY THEORY ?1(S1) CONNECTEDNESS OF SUSPENSIONS ?K?N OF AN N-CONNECTED SPACE AND ?K<N(SN) FIBER SEQUENCES AND THE LONG EXACT SEQUENCE THE HOPF ?BRATION THE FREUDENTHAL SUSPENSION THEOREM THE VAN KAMPEN THEOREM WHITEHEAD’S THEOREM AND WHITEHEAD’S PRINCIPLE A GENERAL STATEMENT OF THE ENCODE-DECODE METHOD 8 10 ADDITIONAL RESULTS CATEGORY THEORY CATEGORIES AND PRECATEGORIES FUNCTORS AND TRANSFORMATIONS ADJUNCTIONS THE YONEDA LEMMA STRICT CATEGORIES †-CATEGORIES THE STRUCTURE IDENTITY PRINCIPLE THE REZK COMPLETION 10 SET THEORY 10 1 THE CATEGORY OF SETS 10 2 CARDINAL NUMBERS 10 3 ORDINAL NUMBERS 10 4 CLASSICAL WELL-ORDERINGS 10 5 THE CUMULATIVE HIERARCHY 11 REAL NUMBERS 11 1 THE ?ELD OF RATIONAL NUMBERS 11 2 DEDEKIND REALS 11 3 CAUCHY REALS 11 4 COMPARISON OF CAUCHY AND DEDEKIND REALS 11 5 COMPACTNESS OF THE INTERVAL 11 6 THE SURREAL NUMBERS