%PDF-1.4 % 4 0 obj <> endobj 7 0 obj (Synthesis) endobj 8 0 obj <> endobj 11 0 obj (General context) endobj 12 0 obj <> endobj 15 0 obj (Problem statement) endobj 16 0 obj <> endobj 19 0 obj (Contribution) endobj 20 0 obj <> endobj 23 0 obj (Arguments in favour of what has been done) endobj 24 0 obj <> endobj 27 0 obj (Results and prospects) endobj 28 0 obj <> endobj 31 0 obj (Acknowledgments) endobj 32 0 obj <> endobj 35 0 obj (Introduction) endobj 36 0 obj <> endobj 39 0 obj (Motivation) endobj 40 0 obj <> endobj 43 0 obj (What is wrong with set theory) endobj 44 0 obj <> endobj 47 0 obj (Type Theory) endobj 48 0 obj <> endobj 51 0 obj (Homotopy Type Theory) endobj 52 0 obj <> endobj 55 0 obj (Category Theory) endobj 56 0 obj <> endobj 59 0 obj (The Basics) endobj 60 0 obj <> endobj 63 0 obj (Definition) endobj 64 0 obj <> endobj 67 0 obj (Principle of duality) endobj 68 0 obj <> endobj 71 0 obj (Commutative diagrams) endobj 72 0 obj <> endobj 75 0 obj (Functors and Natural Transformations) endobj 76 0 obj <> endobj 79 0 obj (Functors) endobj 80 0 obj <> endobj 83 0 obj (Natural Transformations) endobj 84 0 obj <> endobj 87 0 obj (Adjointness) endobj 88 0 obj <> endobj 91 0 obj (Universal Properties) endobj 92 0 obj <> endobj 95 0 obj (Initial and terminal objects) endobj 96 0 obj <> endobj 99 0 obj (Products and pullbacks) endobj 100 0 obj <> endobj 103 0 obj (Limits) endobj 104 0 obj <> endobj 107 0 obj (Other categorical constructions) endobj 108 0 obj <> endobj 111 0 obj (Slice and coslice categories) endobj 112 0 obj <> endobj 115 0 obj (Category of elements) endobj 116 0 obj <> endobj 119 0 obj (Groupoids) endobj 120 0 obj <> endobj 123 0 obj (Syntax of Dependent Type Theory) endobj 124 0 obj <> endobj 127 0 obj (Basics) endobj 128 0 obj <> endobj 131 0 obj (Contexts) endobj 132 0 obj <> endobj 135 0 obj (Types and Terms) endobj 136 0 obj <> endobj 139 0 obj (Judgements) endobj 140 0 obj <> endobj 143 0 obj (Introducing brand new types and terms) endobj 144 0 obj <> endobj 147 0 obj (\134Pi-Types / Dependent function types) endobj 148 0 obj <> endobj 151 0 obj (Intensional Equality) endobj 152 0 obj <> endobj 155 0 obj (Eliminators and recursors) endobj 156 0 obj <> endobj 159 0 obj (Substitutions) endobj 160 0 obj <> endobj 163 0 obj (Categorical semantics of Type Theory) endobj 164 0 obj <> endobj 167 0 obj (Categories with Families) endobj 168 0 obj <> endobj 171 0 obj (CwF-morphisms) endobj 172 0 obj <> endobj 175 0 obj (Globular ω-groupoids) endobj 176 0 obj <> endobj 179 0 obj (Globular sets) endobj 180 0 obj <> endobj 183 0 obj (Laws and Structure of ω-groupoids) endobj 184 0 obj <> endobj 187 0 obj (Strict 𝜔-groupoids) endobj 188 0 obj <> endobj 191 0 obj (Weak 𝜔-groupoids: handmade partial construction) endobj 192 0 obj <> endobj 195 0 obj (G1) endobj 196 0 obj <> endobj 199 0 obj (G2) endobj 200 0 obj <> endobj 203 0 obj (Strict ω-groupoids: a categorical definition) endobj 204 0 obj <> endobj 207 0 obj (It all boils down to 2-categories) endobj 208 0 obj <> endobj 211 0 obj (2-Categories) endobj 212 0 obj <> endobj 215 0 obj (Strict ω-groupoids) endobj 216 0 obj <> endobj 219 0 obj (Brunerie Type Theory comes in) endobj 220 0 obj <> endobj 223 0 obj (Brunerie globular weak ω-groupoids) endobj 224 0 obj <> endobj 227 0 obj (CwFs with additional structure) endobj 228 0 obj <> endobj 231 0 obj (CwFs with Identity and Base Type) endobj 232 0 obj <> endobj 235 0 obj (Brunerie CwFs) endobj 236 0 obj <> endobj 239 0 obj (Syntaxes as initial objects) endobj 240 0 obj <> endobj 243 0 obj (Brunerie globular weak ω-groupoids) endobj 244 0 obj <> endobj 247 0 obj (Definition) endobj 248 0 obj <> endobj 251 0 obj (Types are Brunerie globular weak ω-groupoids) endobj 252 0 obj <> endobj 255 0 obj (Agda Implementation) endobj 256 0 obj <> endobj 259 0 obj (Conclusion) endobj 260 0 obj <> endobj 263 0 obj (Bibliography) endobj 264 0 obj <> endobj 267 0 obj (Articles) endobj 268 0 obj <> endobj 271 0 obj (Books) endobj 272 0 obj <> endobj 275 0 obj (Appendix) endobj 276 0 obj <> endobj 279 0 obj (\134Sigma-Types / Dependent pair types) endobj 280 0 obj <> endobj 283 0 obj (Categorical origin) endobj 284 0 obj <> endobj 287 0 obj (When Category Theory enters the scene) endobj 288 0 obj <> endobj 291 0 obj (Product Type: A×B) endobj 292 0 obj <> endobj 295 0 obj (Recursor) endobj 296 0 obj <> endobj 299 0 obj (Induction) endobj 300 0 obj <> endobj 303 0 obj (Towards the eliminator) endobj 304 0 obj <> endobj 308 0 obj <> stream xڵVM6W˙!$x0!6_]AֈI_wb8muG]pP҈?Fμ"͙b2bռ˞M]sVr Sݏ9YR.{^?ֿoof{AxYQgzr$kb6HKd3'k?~ɼ]ֱ Te7??T{u+LG>zRWVT%NQR]EC7暡dnYgqNODKH3c /iG\u zXyG7YĚ