Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
primitive_notions_._wat [2015/12/17 21:26] nikolaj |
primitive_notions_._wat [2016/04/05 15:05] nikolaj |
||
---|---|---|---|
Line 3: | Line 3: | ||
=== Thoughts === | === Thoughts === | ||
- | Here's some necessary ingrediences | + | Some necessary ingrediences in the end of the HoTT book. |
- | + | (In an old version, it was around p.44 and at the very end.) | |
- | https://hott.github.io/book/nightly/hott-online-1005-ge9c58d7.pdf#441 | + | |
A year ago I asked a relevant related question here | A year ago I asked a relevant related question here | ||
Line 15: | Line 14: | ||
E.g. adding 5+3 would be among the very first things to do. | E.g. adding 5+3 would be among the very first things to do. | ||
For educational purposes, talking about $\to, \times$ before more intricate concepts is also a good idea. | For educational purposes, talking about $\to, \times$ before more intricate concepts is also a good idea. | ||
- | As I thought about before, going bottom top with the typy/computational/constructive stuff should be a good idea. Then, for sets and cats, it's the other other way around. | + | As I thought about before, going bottom (Hands on stuff) to top (abstract minimalistic stuff) |
+ | with the typey/computational/constructive stuff should be a good idea. | ||
+ | Then, for sets and cats, it's the other other way around. | ||
=== Code === | === Code === | ||
Line 36: | Line 37: | ||
$0, 1, 2, 3, 4, 5, 6, 7, 8, 9$ | $0, 1, 2, 3, 4, 5, 6, 7, 8, 9$ | ||
- | $+, \cdot$ | + | $+, *$ |