-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathplan.html
226 lines (193 loc) · 7.32 KB
/
plan.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN">
<HTML>
<head>
<link rel="stylesheet" href="css/style.css" type="text/css"/>
<meta http-equiv="Content-Type" content="text/html; charset=utf8">
</head>
<body>
<h1>Provisional schedule 2019</h1>
Caution: This schedule is provisional and may be adapted in real time.
<table>
<tr><td> 08-09 January : </td><td> Hugo Herbelin (Lectures 1 and 2)</td></tr>
<tr><td> 15-16 January : </td><td> Hugo Herbelin (Lectures 5 and 6)</td></tr>
<tr><td> 22-23 January : </td><td> Nicolas Tabareau (Lectures 3 and 4)</td></tr>
<tr><td> 29-30 January : </td><td> Nicolas Tabareau (Lectures 7)</td></tr>
<tr><td> 05 February : </td><td> Nicolas Tabareau (Lectures 8)</td></tr>
<tr><td> 06 February : </td><td> Hugo Herbelin (Lectures 9)</td></tr>
<tr><td> 12 February : </td><td> No class </td></tr>
<tr><td> 13 February : </td><td> Nicolas Tabareau (Lectures 11)</td></tr>
<tr><td> 19-20 February : </td><td> Hugo Herbelin (Lectures 10 and 13)</td></tr>
<tr><td> 26 February : </td><td> Nicolas Tabareau (Lectures 12)</td></tr>
<tr><td> 27 February : </td><td> Hugo Herbelin Lectures 16) </td></tr>
<tr><td> 05-06 March : </td><td> Hugo Herbelin (Lectures 17 and 18)</td></tr>
<tr><td> 13 March : </td><td> Hugo Herbelin</td></tr>
<tr><td> 13 March (special class on afternoon 2pm, 1014) : </td><td> Hugo Herbelin</td></tr>
<tr><td> 19 March : </td><td> Nicolas Tabareau (Lectures 14)</td></tr>
<tr><td> 20 March : </td><td> No class </td></tr>
<tr><td> 26-27 March : </td><td> Nicolas Tabareau (Lectures 15 and 21)</td></tr>
<tr><td> 02-03 April : </td><td> Nicolas Tabareau (Lectures 22 and 23)</td></tr>
</table>
<hr>
<table><tr><td>
1 General introduction, basics of Martin-Löf's intensional type theory
</td></tr><tr><td>- general context: unifying category theory, homotopy theory, logic and foundations of computer science, proofs-as-programs-as-morphisms, equality-proofs-as-paths-as-isomorphisms
</td></tr><tr><td>- quick overview of synthetic homotopy (equality proof = geometric path)
</td></tr><tr><td>- basics of Martin-Löf intensional type theory (universes, dependent function type, conversion rule, well-formed contexts)
</td></tr><tr><td>- connecting with the traditional approach to logic and λ-calculus (dependent function type playing the role of implication, function space, universal quantification)
</td></tr></table>
<hr>
<table><tr><td>
2 Basics of Martin-Löf intensional type theory (continued), examples
</td></tr><tr><td>- further basics of Martin-Löf intensional type theory (integers, identity type, sigma type)
</td></tr><tr><td>- connecting with the traditional approach to logic and λ-calculus (dependent sum type playing the role of conjunction, product, existential quantification)
</td></tr><tr><td>- examples of proofs, intensional axiom of choice, basic arithmetical properties
</td></tr></table>
<hr>
<table><tr><td>
3 (option a) Modèles catégoriques
</td></tr><tr><td>- catégories avec familles (CwF)
</td></tr><tr><td>- modèles de préfaisceau
</td></tr></table>
<hr>
<table><tr><td>
3 (option b) Propriétés fondamentales et théorie des types extensionnelle
</td></tr><tr><td>- canonicité, normalisation, préservation du typage par réduction, décidabilité du typage
</td></tr><tr><td>- règle de réflexion
</td></tr><tr><td>- implication de l'unicité des preuves d'identité (UIP)
</td></tr><tr><td>- typage indécidable
</td></tr></table>
<hr>
<table><tr><td>
4 Univers
</td></tr><tr><td>- hiérarchie d’univers
</td></tr><tr><td>- paradoxe de Hurkens
</td></tr><tr><td>- polymorphisme d'univers
</td></tr></table>
<hr>
<table><tr><td>
5 Types inductifs généraux, familles inductives
</td></tr><tr><td>- types inductifs de base
</td></tr><tr><td>- famille inductive, index, encodage/description de l’égalité
</td></tr><tr><td>- encodage imprédicatif (limitation de la règle d’élimination)
</td></tr></table>
<hr>
<table><tr><td>
6 Conversion typée/non typée et normalisation par évaluation
</td></tr></table>
<hr>
<table><tr><td>
7 HoTT, introduction
</td></tr><tr><td>- la correspondance type/espace, égalité/chemin HH/NT
</td></tr><tr><td>- espaces contractiles, h-niveaux,
</td></tr><tr><td>- discernabilité et indiscernabilité des preuves, notion de “mere propositions”
</td></tr><tr><td>- equivalences (diverses définitions)
</td></tr></table>
<hr>
<table><tr><td>
8 Structures supérieures des constructeurs de type
</td></tr><tr><td>- produits cartésiens
</td></tr><tr><td>- sommes dépendantes
</td></tr><tr><td>- produit dépendants et extensionnalité
</td></tr><tr><td>- univers et l’axiome d’univalence
</td></tr></table>
<hr>
<table><tr><td>
9 Negative types, built from destructors
</td></tr></table>
<hr>
<table><tr><td>
<!-- 10 Présentation de Coq et de comment tous ces concepts ont été implémentés-->
10 Smallest and greatest fixpoint of types
</td></tr></table>
<hr>
<table><tr><td>
11 Les n-types homotopiques
</td></tr><tr><td>- n-types
</td></tr><tr><td>- théorème d’Hedberg
</td></tr><tr><td>- n-troncation
</td></tr><tr><td>- n-connexion
</td></tr><tr><td>- système de factorisation
</td></tr><tr><td>- avec les sigmas
</td></tr><tr><td>- avec les cylindres (HIT)
</td></tr></table>
<hr>
<table><tr><td>
12 Homotopie synthétique
</td></tr><tr><td>- types inductifs supérieurs
</td></tr><tr><td>- intervalle et extensionnalité des fonctions
</td></tr><tr><td>- sphère
</td></tr><tr><td>- troncation
</td></tr><tr><td>- quotients
</td></tr><tr><td>- suspension
</td></tr><tr><td>- 𝝅<sub>1</sub>(S<sup>1</sup>) = Z
</td></tr></table>
<hr>
<table><tr><td>
13 Structure ω-groupoïde de l'égalité
</td></tr><tr><td>- définition de l'égalité par abstraction sur une direction
</td></tr></table>
<hr>
<table><tr><td>
14 Théorie des types à deux niveaux
</td></tr><tr><td>- définition avec la structure de 2 CwF
</td></tr><tr><td>- discussion des différentes façons de définir un catégorie dans ce cadre
</td></tr></table>
<hr>
<table><tr><td>
15 Catégorie de modèles
</td></tr><tr><td>- définition en HoTT
</td></tr><tr><td>- structure de modèle de Type
</td></tr><tr><td>- systèmes de factorisation faible
</td></tr></table>
<hr>
<table><tr><td>
16 Théorie des types cubiques
</td></tr><tr><td>- composition et transitivité
</td></tr><tr><td>- vers l'univalence
</td></tr></table>
<hr>
<table><tr><td>
17 Modèle cubique de HoTT
</td></tr></table>
<hr>
<table><tr><td>
18 Relecture de la logique en HoTT
</td></tr><tr><td>- logique des “mere propositions”
</td></tr><tr><td>- axiome du choix
</td></tr><tr><td>- logique classique
</td></tr><tr><td>- choix unique
</td></tr></table>
<hr>
<table><tr><td>
19 ?
</td></tr></table>
<hr>
<table><tr><td>
20 Théorie des ensembles en HoTT
</td></tr><tr><td>- catégorie des ensembles
</td></tr><tr><td>- cardinaux
</td></tr><tr><td>- ordinaux
</td></tr><tr><td>- hiérarchie cumulative
</td></tr></table>
<hr>
<table><tr><td>
21 ω-groupoïdes en général
</td></tr></table>
<hr>
<table><tr><td>
22 Traductions internes
</td></tr><tr><td>- résultats d’indépendance
</td></tr></table>
<hr>
<table><tr><td>
23 Traduction de forcing
</td></tr><tr><td>- traduction générale
</td></tr><tr><td>- théorie des types gardée
</td></tr><tr><td>- interprétation de la théorie des types cubiques
</td></tr></table>
<hr>
<table><tr><td>
24 Séance tampon
</td></tr></table>
</body>
</HTML>