Homotopy Type Theory 讀書會

編輯歷史

時間	作者	版本
2015-12-06 05:08 – 05:11	Pomin Wu	r321 – r365
顯示 diff （5 行未修改）書籍: Homotopy Type Theory: Univalent Foundations of Mathematics + 電子版 http://homotopytypetheory.org/ Homotopy Type Theory （16 行未修改） Homotopy Theory * - + Algebraic Topology 第四章, Allen Hatcher http://www.math.cornell.edu/~hatcher/AT/ATpage.html *章節 Foundations （128 行未修改）
2015-12-06 03:52 – 04:17	HisnYi Chen	r117 – r320
顯示 diff Homotopy Type Theory 讀書會 - 前情提要 + 前情提要 + pm5 在數學小聚裡提到想找人一起讀 HoTT. 書籍: Homotopy Type Theory: Univalent Foundations of Mathematics - 什麼是 Homotopy Type Theory + Homotopy Type Theory Homotopy Type Theory is an interpretation of Martin-Löf’s intensional type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. As the natural logic of homotopy, type theory is also related to higher category theory as it is used e.g. in the notion of a higher topos. - 前置知識 + 前置知識 - Type Theory - Homotopy Theory + Type Theory + + Intuitionistic Type Theory, Martin-Löf + Proof and Types, Jean-Yves Girard + FLOLAC 14 型別與邏輯 (video), 柯向上 - 共筆 - I Foundations 15 - 1 Type theory 17 - 1.1 Type theory versus set theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 - 1.2 Function types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 - 1.3 Universes and families . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 - 1.4 Dependent function types (Π-types) . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 - 1.5 Product types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 - 1.6 Dependent pair types (Σ-types) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 - 1.7 Coproduct types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 - 1.8 The type of booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 - 1.9 The natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 - 1.10 Pattern matching and recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 - 1.11 Propositions as types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 - 1.12 Identity types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 - Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 - 2 Homotopy type theory 59 - 2.1 Types are higher groupoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 - 2.2 Functions are functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 - 2.3 Type families are fibrations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 - 2.4 Homotopies and equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 - 2.5 The higher groupoid structure of type formers . . . . . . . . . . . . . . . . . . . . . 79 - 2.6 Cartesian product types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 - 2.7 Σ-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 - 2.8 The unit type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 - 2.9 Π-types and the function extensionality axiom . . . . . . . . . . . . . . . . . . . . . 85 - 2.10 Universes and the univalence axiom . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 - 2.11 Identity type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 + 應用: Types and Programming Language, Benjamin + + 相關閒書: + 數學: 確定性的失落 + 數學邏輯奇幻之旅(漫畫) + Homotopy Theory + + + *章節 + Foundations + + 1 Type theory + 1.1 Type theory versus set theory + 1.2 Function types + 1.3 Universes and families + 1.4 Dependent function types (Π-types) + 1.5 Product types + 1.6 Dependent pair types (Σ-types) + 1.7 Coproduct types + 1.8 The type of booleans + 1.9 The natural numbers + 1.10 Pattern matching and recursion + 1.11 Propositions as types + 1.12 Identity types + + 2 Homotopy type theory + 2.1 Types are higher groupoids + 2.2 Functions are functors + 2.3 Type families are fibrations + 2.4 Homotopies and equivalences + 2.5 The higher groupoid structure of type formers + 2.6 Cartesian product types + 2.7 Σ-types + 2.8 The unit type + 2.9 Π-types and the function extensionality axiom + 2.10 Universes and the univalence axiom + 2.11 Identity type vi Contents - 2.12 Coproducts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 - 2.13 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 - 2.14 Example: equality of structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 - 2.15 Universal properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 - Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 - 3 Sets and logic 107 - 3.1 Sets and n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 - 3.2 Propositions as types? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 - 3.3 Mere propositions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 - 3.4 Classical vs. intuitionistic logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 - 3.5 Subsets and propositional resizing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 - 3.6 The logic of mere propositions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 - 3.7 Propositional truncation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 - 3.8 The axiom of choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 - 3.9 The principle of unique choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 - 3.10 When are propositions truncated? . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 - 3.11 Contractibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 - Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 - 4 Equivalences 129 - 4.1 Quasi-inverses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130 - 4.2 Half adjoint equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 - 4.3 Bi-invertible maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 - 4.4 Contractible fibers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 - 4.5 On the definition of equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 - 4.6 Surjections and embeddings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 - 4.7 Closure properties of equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 - 4.8 The object classifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 - 4.9 Univalence implies function extensionality . . . . . . . . . . . . . . . . . . . . . . . 144 - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146 - Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 - 5 Induction 149 - 5.1 Introduction to inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 - 5.2 Uniqueness of inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 - 5.3 W-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154 - 5.4 Inductive types are initial algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 - 5.5 Homotopy-inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160 - 5.6 The general syntax of inductive definitions . . . . . . . . . . . . . . . . . . . . . . . 164 - 5.7 Generalizations of inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168 - 5.8 Identity types and identity systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170 - Contents vii - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174 - Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175 - 6 Higher inductive types 177 - 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177 - 6.2 Induction principles and dependent paths . . . . . . . . . . . . . . . . . . . . . . . . 179 - 6.3 The interval . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184 - 6.4 Circles and spheres . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185 - 6.5 Suspensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 - 6.6 Cell complexes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190 - 6.7 Hubs and spokes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192 - 6.8 Pushouts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193 - 6.9 Truncations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196 - 6.10 Quotients . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199 - 6.11 Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 204 - 6.12 The flattening lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 209 - 6.13 The general syntax of higher inductive definitions . . . . . . . . . . . . . . . . . . . 214 - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216 - Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217 - 7 Homotopy n-types 219 - 7.1 Definition of n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219 - 7.2 Uniqueness of identity proofs and Hedberg’s theorem . . . . . . . . . . . . . . . . . 223 - 7.3 Truncations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226 - 7.4 Colimits of n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 232 - 7.5 Connectedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 236 - 7.6 Orthogonal factorization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 240 - 7.7 Modalities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 245 - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 249 - Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 250 - II Mathematics 253 - 8 Homotopy theory 255 - 8.1 π1(S - 1 - ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 259 - 8.2 Connectedness of suspensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267 - 8.3 πk≤n of an n-connected space and πk<n(S - n - ) . . . . . . . . . . . . . . . . . . . . . . . 268 - 8.4 Fiber sequences and the long exact sequence . . . . . . . . . . . . . . . . . . . . . . 269 - 8.5 The Hopf fibration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 273 - 8.6 The Freudenthal suspension theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . 279 - 8.7 The van Kampen theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 285 - 8.8 Whitehead’s theorem and Whitehead’s principle . . . . . . . . . . . . . . . . . . . . 294 - 8.9 A general statement of the encode-decode method . . . . . . . . . . . . . . . . . . . 297 + 2.12 Coproducts + 2.13 Natural numbers + 2.14 Example: equality of structures + 2.15 Universal properties + + 3 Sets and logic + 3.1 Sets and n-types + 3.2 Propositions as types? + 3.3 Mere propositions + 3.4 Classical vs. intuitionistic logic + 3.5 Subsets and propositional resizing + 3.6 The logic of mere propositions + 3.7 Propositional truncation + 3.8 The axiom of choice + 3.9 The principle of unique choice + 3.10 When are propositions truncated? + 3.11 Contractibility + + 4 Equivalences + 4.1 Quasi-inverses + 4.2 Half adjoint equivalences + 4.3 Bi-invertible maps + 4.4 Contractible fibers + 4.5 On the definition of equivalences + 4.6 Surjections and embeddings + 4.7 Closure properties of equivalences + 4.8 The object classifier + 4.9 Univalence implies function extensionality + + 5 Induction + 5.1 Introduction to inductive types + 5.2 Uniqueness of inductive types + 5.3 W-types + 5.4 Inductive types are initial algebras + 5.5 Homotopy-inductive types + 5.6 The general syntax of inductive definitions + 5.7 Generalizations of inductive types + 5.8 Identity types and identity systems + + 6 Higher inductive types + 6.1 Introduction + 6.2 Induction principles and dependent paths + 6.3 The interval + 6.4 Circles and spheres + 6.5 Suspensions + 6.6 Cell complexes + 6.7 Hubs and spokes + 6.8 Pushouts + 6.9 Truncations + 6.10 Quotients + 6.11 Algebra + 6.12 The flattening lemma + 6.13 The general syntax of higher inductive definitions + + 7 Homotopy n-types + 7.1 Definition of n-types + 7.2 Uniqueness of identity proofs and Hedberg’s theorem + 7.3 Truncations + 7.4 Colimits of n-types + 7.5 Connectedness + 7.6 Orthogonal factorization + 7.7 Modalities + + II Mathematics + + 8 Homotopy theory + 8.1 π1(S1) + 8.2 Connectedness of suspensions + 8.3 πk≤n of an n-connected space and πk<n(Sn) + 8.4 Fiber sequences and the long exact sequence + 8.5 The Hopf fibration + 8.6 The Freudenthal suspension theorem + 8.7 The van Kampen theorem + 8.8 Whitehead’s theorem and Whitehead’s principle + 8.9 A general statement of the encode-decode method viii Contents - 8.10 Additional Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 299 - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 300 - Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 301 + 8.10 Additional Results 9 Category theory 303 - 9.1 Categories and precategories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 304 - 9.2 Functors and transformations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 307 - 9.3 Adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 311 - 9.4 Equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 312 - 9.5 The Yoneda lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 318 - 9.6 Strict categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 321 - 9.7 †-categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 322 - 9.8 The structure identity principle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 323 - 9.9 The Rezk completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 326 - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 333 - Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 334 + 9.1 Categories and precategories + 9.2 Functors and transformations + 9.3 Adjunctions + 9.4 Equivalences + 9.5 The Yoneda lemma + 9.6 Strict categories + 9.7 †-categories + 9.8 The structure identity principle + 9.9 The Rezk completion 10 Set theory 337 - 10.1 The category of sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 337 - 10.2 Cardinal numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 346 - 10.3 Ordinal numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 349 - 10.4 Classical well-orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 356 - 10.5 The cumulative hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 358 - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 364 - Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 364 + 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 367 - 11.1 The field of rational numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 368 - 11.2 Dedekind reals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 368 - 11.3 Cauchy reals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 375 - 11.4 Comparison of Cauchy and Dedekind reals . . . . . . . . . . . . . . . . . . . . . . . 393 - 11.5 Compactness of the interval . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 395 - 11.6 The surreal numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 401 - Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 412 - Exercises . . . . . . . . . . . . . . . . + 11.1 The field 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
2015-12-06 03:52	(unknown)	r116
顯示 diff （164 行未修改）
2015-12-06 03:49 – 03:52	HisnYi Chen	r110 – r115
顯示 diff （14 行未修改） Homotopy Theory - 章節 + 共筆 + I Foundations 15 + 1 Type theory 17 + 1.1 Type theory versus set theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 + 1.2 Function types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 + 1.3 Universes and families . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 + 1.4 Dependent function types (Π-types) . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 + 1.5 Product types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 + 1.6 Dependent pair types (Σ-types) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 + 1.7 Coproduct types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 + 1.8 The type of booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 + 1.9 The natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 + 1.10 Pattern matching and recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 + 1.11 Propositions as types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 + 1.12 Identity types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 + Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 + 2 Homotopy type theory 59 + 2.1 Types are higher groupoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 + 2.2 Functions are functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 + 2.3 Type families are fibrations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 + 2.4 Homotopies and equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 + 2.5 The higher groupoid structure of type formers . . . . . . . . . . . . . . . . . . . . . 79 + 2.6 Cartesian product types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 + 2.7 Σ-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 + 2.8 The unit type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 + 2.9 Π-types and the function extensionality axiom . . . . . . . . . . . . . . . . . . . . . 85 + 2.10 Universes and the univalence axiom . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 + 2.11 Identity type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 + vi Contents + 2.12 Coproducts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 + 2.13 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 + 2.14 Example: equality of structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 + 2.15 Universal properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 + Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 + 3 Sets and logic 107 + 3.1 Sets and n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 + 3.2 Propositions as types? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 + 3.3 Mere propositions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 + 3.4 Classical vs. intuitionistic logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 + 3.5 Subsets and propositional resizing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 + 3.6 The logic of mere propositions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 + 3.7 Propositional truncation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 + 3.8 The axiom of choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 + 3.9 The principle of unique choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 + 3.10 When are propositions truncated? . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 + 3.11 Contractibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 + Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 + 4 Equivalences 129 + 4.1 Quasi-inverses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130 + 4.2 Half adjoint equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 + 4.3 Bi-invertible maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 + 4.4 Contractible fibers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 + 4.5 On the definition of equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 + 4.6 Surjections and embeddings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 + 4.7 Closure properties of equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 + 4.8 The object classifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 + 4.9 Univalence implies function extensionality . . . . . . . . . . . . . . . . . . . . . . . 144 + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146 + Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 + 5 Induction 149 + 5.1 Introduction to inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 + 5.2 Uniqueness of inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 + 5.3 W-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154 + 5.4 Inductive types are initial algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 + 5.5 Homotopy-inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160 + 5.6 The general syntax of inductive definitions . . . . . . . . . . . . . . . . . . . . . . . 164 + 5.7 Generalizations of inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168 + 5.8 Identity types and identity systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170 + Contents vii + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174 + Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175 + 6 Higher inductive types 177 + 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177 + 6.2 Induction principles and dependent paths . . . . . . . . . . . . . . . . . . . . . . . . 179 + 6.3 The interval . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184 + 6.4 Circles and spheres . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185 + 6.5 Suspensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 + 6.6 Cell complexes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190 + 6.7 Hubs and spokes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192 + 6.8 Pushouts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193 + 6.9 Truncations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196 + 6.10 Quotients . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199 + 6.11 Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 204 + 6.12 The flattening lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 209 + 6.13 The general syntax of higher inductive definitions . . . . . . . . . . . . . . . . . . . 214 + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216 + Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217 + 7 Homotopy n-types 219 + 7.1 Definition of n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219 + 7.2 Uniqueness of identity proofs and Hedberg’s theorem . . . . . . . . . . . . . . . . . 223 + 7.3 Truncations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226 + 7.4 Colimits of n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 232 + 7.5 Connectedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 236 + 7.6 Orthogonal factorization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 240 + 7.7 Modalities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 245 + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 249 + Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 250 + II Mathematics 253 + 8 Homotopy theory 255 + 8.1 π1(S + 1 + ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 259 + 8.2 Connectedness of suspensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267 + 8.3 πk≤n of an n-connected space and πk<n(S + n + ) . . . . . . . . . . . . . . . . . . . . . . . 268 + 8.4 Fiber sequences and the long exact sequence . . . . . . . . . . . . . . . . . . . . . . 269 + 8.5 The Hopf fibration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 273 + 8.6 The Freudenthal suspension theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . 279 + 8.7 The van Kampen theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 285 + 8.8 Whitehead’s theorem and Whitehead’s principle . . . . . . . . . . . . . . . . . . . . 294 + 8.9 A general statement of the encode-decode method . . . . . . . . . . . . . . . . . . . 297 + viii Contents + 8.10 Additional Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 299 + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 300 + Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 301 + 9 Category theory 303 + 9.1 Categories and precategories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 304 + 9.2 Functors and transformations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 307 + 9.3 Adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 311 + 9.4 Equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 312 + 9.5 The Yoneda lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 318 + 9.6 Strict categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 321 + 9.7 †-categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 322 + 9.8 The structure identity principle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 323 + 9.9 The Rezk completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 326 + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 333 + Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 334 + 10 Set theory 337 + 10.1 The category of sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 337 + 10.2 Cardinal numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 346 + 10.3 Ordinal numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 349 + 10.4 Classical well-orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 356 + 10.5 The cumulative hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 358 + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 364 + Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 364 + 11 Real numbers 367 + 11.1 The field of rational numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 368 + 11.2 Dedekind reals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 368 + 11.3 Cauchy reals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 375 + 11.4 Comparison of Cauchy and Dedekind reals . . . . . . . . . . . . . . . . . . . . . . . 393 + 11.5 Compactness of the interval . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 395 + 11.6 The surreal numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 401 + Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 412 + Exercises . . . . . . . . . . . . . . . .
2015-12-06 03:49	(unknown)	r109
顯示 diff （17 行未修改）
2015-12-06 03:49 – 03:49	HisnYi Chen	r90 – r108
顯示 diff （10 行未修改）前置知識 - - + + Type Theory + Homotopy Theory + + 章節
2015-12-06 03:49	(unknown)	r89
顯示 diff （13 行未修改）
2015-12-06 03:48 – 03:49	HisnYi Chen	r84 – r88
顯示 diff （9 行未修改） Homotopy Type Theory is an interpretation of Martin-Löf’s intensional type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. As the natural logic of homotopy, type theory is also related to higher category theory as it is used e.g. in the notion of a higher topos. - 箝制知 + 前置知識 + -
2015-12-06 03:48	(unknown)	r83
顯示 diff （12 行未修改）
2015-12-06 03:45 – 03:48	HisnYi Chen	r1 – r82
顯示 diff - Untitled + Homotopy Type Theory 讀書會 - This pad text is synchronized as you type, so that everyone viewing this page sees the same text. This allows you to collaborate seamlessly on documents! + 前情提要 + pm5 在數學小聚裡提到想找人一起讀 HoTT. + + 書籍: Homotopy Type Theory: Univalent Foundations of Mathematics + + 什麼是 Homotopy Type Theory + + Homotopy Type Theory is an interpretation of Martin-Löf’s intensional type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. As the natural logic of homotopy, type theory is also related to higher category theory as it is used e.g. in the notion of a higher topos. + + 箝制知
2015-12-06 03:45	(unknown)	r0
顯示 diff + Untitled + This pad text is synchronized as you type, so that everyone viewing this page sees the same text. This allows you to collaborate seamlessly on documents!