-
Notifications
You must be signed in to change notification settings - Fork 0
/
plan.txt
36 lines (28 loc) · 1005 Bytes
/
plan.txt
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
colinks = lenses, optics, etc
links = charts
cartesian colinks = concrete lenses
closed/linear colinks = linear lenses
dependent colinks = dependent lenses
monoidal colinks = coend optics
? colinks = mixed optics
Chapter 0: preliminaries
- categories, monoidal categories, string diagrams, examples, coend calculus?
Chapter 1: "Concrete colinks" = can be defined without coends or dependent types
- cartesian colinks (X)
-- category structure (X)
-- examples:
---- destructive update lenses (X)
---- "naive backprop" = reverse derivatives of smooth maps (X)
-- universal properties (products, coproducts)
-- fibration structure
-- monoidal structure
-- "teleological" structure
---- string diagrams
-- lens laws
Chapter 2: Actegories and enriched categories
Chapter 3: closed/linear colinks
-- category structure
--- equivalence to cartesian colinks when cartesian closed
-- monoidal structure, teleological structure, string diagrams
Chapter 3: Para
Chapter 4: "Monoidal colinks" = mixed optics