Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance

Contents......Page 4
Voorwoord......Page 8
Vulgariserende samenvatting......Page 10
English abstract......Page 12
Nederlandstalige abstract......Page 14
1.1 Dependent type theory......Page 18
1.2 Homotopy type theory......Page 22
1.3.1 Two-dimensional directed type theory......Page 23
1.3.2 Other related work......Page 25
1.3.3 Directed homotopy type theory......Page 26
1.3.4 Contributions......Page 28
2.1 Judgements and contexts......Page 30
2.2 Structural inference rules......Page 35
2.3 Universe types......Page 37
2.4 Non-dependent function types......Page 38
2.5 Dependent function types......Page 42
2.6 Intermezzo: equivalences and function extensionality......Page 44
2.7 Inductive types and the coproduct......Page 45
2.8 Lists......Page 51
2.9 The naturals......Page 53
2.10 The family of finite sets......Page 55
2.11 The product......Page 57
2.12.1 The opposite of a type......Page 61
2.12.2 The core of a type......Page 64
2.12.3 Bridged groupoids......Page 66
2.12.4 The localization of a type......Page 67
2.12.5 Bridgeless groupoids......Page 69
2.13 Dependent pair types......Page 70
2.14 Inductive type families: some examples......Page 74
2.15 The identity type......Page 81
2.16 The morphism type......Page 87
2.17 W-types......Page 91
2.18 Higher inductive types......Page 92
3.1 Types are higher categories......Page 94
3.2 Functions are functors......Page 99
3.3 Equivalences, isomorphisms and transport......Page 103
3.4.1 In symmetric HoTT......Page 108
3.4.2 In directed HoTT......Page 112
3.5.1 Discussion......Page 122
3.5.2 Attempts to define bridges......Page 124
3.5.3 An axiomatic treatment of bridges......Page 127
3.6 Homotopies and natural transformations......Page 130
3.7 Groupoids......Page 133
3.8.1 The coproduct......Page 136
3.8.2 The naturals......Page 137
3.8.3 The opposite......Page 139
3.8.5 The localization......Page 140
3.8.7 Dependent pair types......Page 142
3.8.8 Dependent function types......Page 145
3.8.9 Universe types and univalence......Page 147
3.9.1 Category theory in HoTT......Page 150
3.9.2 Categorical univalence......Page 151
3.9.3 Univalence in directed HoTT......Page 153
4 Exploring semantics and consistency......Page 156
4.1 Basic preparations......Page 157
4.2.1 Interpreting types......Page 161
4.2.2 Functorial behaviour......Page 164
4.3 Interpreting axioms......Page 165
4.4 Conclusion......Page 166
5.1 Morphisms and morphisms......Page 168
5.3 Discussion and further work......Page 170
Bibliography......Page 172
List of Symbols and Abbreviations......Page 174
Index......Page 178