Notes written while consulting for the Higher Order Company
- w-types: a note about W-types
- q: the start of a draft describing an affine lambda calculus with W-types
- sar: "schematic affine recursion", for a usable terminating affine lambda calculus with natural-number recursion