From c06793b0186c2691ef565cb982ca62067f32c4bd Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 10 Apr 2017 20:34:04 -0400 Subject: [PATCH] add lessons file --- lessons.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 lessons.md diff --git a/lessons.md b/lessons.md new file mode 100644 index 0000000..6dd7030 --- /dev/null +++ b/lessons.md @@ -0,0 +1,19 @@ +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