Mid November I participated in the  31:st Agda Implementors' Meeting in Edinburgh. I presented work in progress about
  "Dimension analysis and graded algebras" (video, Agda source code)
The talks were recorded (and streamed by https://www.twitch.tv/omelkonian).

During the code sprints I focused on porting some Haskell code to Agda with the aim to use (and find bugs in) the tool agda2hs. The idea is that if I stick to the supported subset of Agda for the "runnable" part I can extract working Haskell code, and also formalize some proofs about the code. The code I worked on porting is for a paper on Level-p-complexity of boolean functions (with a case study on iterated two-level majority).

One session I had a good time exploring the BNFC Agda backend together with Phil Wadler. We started from earlier Haskell code using BNFC-meta (stackage). (A longer term dream would be to have BNFC-meta-like embedded language definitions including quoting in Agda...)

I also got the opportunity to hear several other presentations and discussions about hot topics in the Agda world and what needs to be done next.

Practical things include Agda library management, support for continuous integration, and improving Agda's editor integration.
 
An interesting historical detail is that I was also in the very first Agda meeting in 2004 when I was PhD advisor of Ulf Norell and Nils Anders Danielsson, two of the main Agda developers. Time flies!

PS. My first ever use of a github action in any language was for Agda during this week. Baby steps by a newbie to CI: patrikja/testAgdaCI
Thanks to the hard work by Wen Kokke.
2022-12-15 update: Now the talk source code is also up on github with active CI.