Truncation levels in homotopy type theory

✍ Scribed by Nicolai Kraus

• Year: 2015
• Tongue: English
• Leaves: 210
• Series: PhD thesis at University of Nottingham
• Edition: version 2 Dec 2015
• Category: Library

✦ Table of Contents

Summary......Page 3
Acknowledgements......Page 5
Contents......Page 7
Introduction......Page 9
Historical Outline......Page 10
A brief introduction to truncation levels and operations......Page 14
Overview over Our Results......Page 16
Computer-Verified Formalisations......Page 20
Declaration of Authorship and Previous Publications......Page 23
Martin-Löf Type Theory......Page 25
Constructions with Propositional Equality......Page 31
Homotopy Type Theory......Page 42
A Word on Ambiguity Avoidance and Readability......Page 47
Hedberg's Theorem Revisited......Page 51
Generalisations to Higher Levels......Page 57
Collapsible Types have Split Support......Page 59
Populatedness......Page 63
Comparison of Notions of Existence......Page 66
The Limitations of Weak Constancy......Page 77
Factorisation for Special Cases......Page 80
On the Computation Rule of the Propositional Truncation......Page 87
The Interval......Page 88
Judgmental Factorisation......Page 91
An Invertibility Puzzle......Page 93
Background of the Problem......Page 97
The First Cases......Page 101
Pointed Types......Page 103
Homotopically Complicated Types......Page 105
A Solution with the ``Wrapping'' Approach......Page 109
Connectedness......Page 112
Combining the Results......Page 120
The General Universal Properties of Truncations......Page 123
A First Few Special Cases......Page 127
Fibration Categories, Inverse Diagrams, and Reedy Limits......Page 132
Subdiagrams......Page 136
Equality Diagrams......Page 138
The Equality Semisimplicial Type......Page 139
Fibrant Diagrams of Natural Transformations......Page 143
Extending Semi-Simplicial Types......Page 145
The Main Theorem......Page 149
Finite Cases......Page 155
Elimination Principles for Higher Truncations......Page 158
The Big Picture: Solved and Unsolved Cases......Page 169
The Problem of Formalising Infinite Structures......Page 175
Semi-Simplicial Types......Page 176
Yoneda Groupoids......Page 185
Set-Based Groupoids......Page 191
Further Notes on Related Work and Conclusions......Page 194
Bibliography......Page 201