this repo includes some of the practice exercises from PLFA:
  plfa.part1.Peano: associativity and distributivity proofs of + and * over +
  plfa.part1.Relations: ≤ properties, trichotomy, even/odd proofs, bitstrings
  plfa.part1.Relationsbinary: exercises (marked stretch) about bitstrings
  plfa.part1.Negation: <-irreflexive, trichotomy with ≡/<, ⊎-dual-×
  plfa.part1.Quantifiers: ∀-distrib-×, (∃[ x ] (x + y ≡ z)) ⇔ (y ≤ z), ∃-distrib-⊎
  plfa.part1.Decidable: a few exercises, mostly copypasted definitions
  plfa.part1.Lists: reverse-distrib-++, sum-downFrom, Any-++-⇔, All-++-≃

  plfa.part2.Lambda: _[_:=_]′, mul, ⊢mul
  plfa.part2.Properties: ⊢mul, automatic normalization of terms in ⊢mul-eval

but also just some exploratory agda "sketches" in sandbox/