michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

merge the two lessons files

Browse source
This commit is contained in:
Floris van Doorn 2017-07-17 14:11:21 +01:00
parent 3f68115d25
commit 1eec8e65dc
2 changed files with 5 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Notes/lessons.md
View file

@ -7,6 +7,7 @@ Some of these things still need to be changes, some of them are already changed,
- Type classes don't work well together with bundled structures and coercions in Lean (the instance is_contr_unit will not unify with (is_contr punit). - Type classes don't work well together with bundled structures and coercions in Lean (the instance is_contr_unit will not unify with (is_contr punit).
- Overloading doesn't work well in Lean (mostly by degrading error messages) - Overloading doesn't work well in Lean (mostly by degrading error messages)
- avoid rec_on, don't formulate induction principles using "on", the order of arguments is worse - avoid rec_on, don't formulate induction principles using "on", the order of arguments is worse
- squares of maps, pointed maps and similar objects should be defined with operations on them. Squares of maps should be a structure, because we don't want that `hsquare t b l r` is definitionally equal to `hsquare (r ∘ t) b l id`.
- It is useful to do categorical properties more uniformly. Define a 1-coherent ∞-category, which is a precategory (or category?) where the homs are not assumed to be sets. Examples include - It is useful to do categorical properties more uniformly. Define a 1-coherent ∞-category, which is a precategory (or category?) where the homs are not assumed to be sets. Examples include
+ `Type` (with `→`), + `Type` (with `→`),
+ `A → B` (with `~`), + `A → B` (with `~`),
@ -16,4 +17,7 @@ Some of these things still need to be changes, some of them are already changed,
+ spectrum (with `→ₛ`) + spectrum (with `→ₛ`)
+ ... + ...
You cannot formulate everything in this, but it would be useful to compose natural transformations (instead of composing functions and manually show naturality). You cannot formulate everything in this, but it would be useful to compose natural transformations (instead of composing functions and manually show naturality).
Disadvantage: doesn't work Disadvantage: doesn't work for everything, at some point you have to resort to higher categorical reasoning. Also, it might be challenging to formulate things like functoriality of pi's and sigma's.
- Type class inference for equivalences doesn't really work in Lean, since it recognizes that `f ∘ id` is definitionally `f`, hence it can always apply `is_equiv_compose` and get trapped in a loop.
- Coercions should all be defined *immediately* after defining a structure, *before* declaring any
instances. This is because the coercion graph is updated after each declared coercion.

19
lessons.md
View file

@ -1,19 +0,0 @@
Things I would do differently with hindsight:
* Make pointed dependent maps primitive:
```lean
structure ppi (A : Type*) (P : A → Type) (p : P pt) :=
(to_fun : Π a : A, P a)
(resp_pt : to_fun (Point A) = p)
```
(maybe the last argument should be `[p : pointed (P pt)]`). Define pointed (non-dependent) maps as a special case.
Note: assuming `P : A → Type*` is not general enough.
* Use squares, also for maps, pointed maps, ... heavily
* Type classes for equivalences don't really work
* Coercions should all be defined *immediately* after defining a structure, *before* declaring any
instances. This is because the coercion graph is updated after each declared coercion.
* [maybe] make bundled structures primitive