• foldrl-simpler.agda

  all the proofs that i did in RG, but just as agda without much explanation about what's going on. it also includes a proof that if you have an f at A -> A -> A that's associative and commutative, that implies that it has the Δ property

• foldrl.agda

  the same whole work up, but with the version of the proof that invoves rev before I noticed that I didn't need to make the detour

• live-23-feb.agda

  what I wrote live in RG

• patter.md

  the script / notes that i worked up for myself in getting ready for RG.

• readme.md

  this file