So for the past couple of months I've been reading more about directed type theory/homotopy type theory and trying to find a manageable sub-problem that I can honestly tackle at the moment.
I've been interested in what the general induction story should be for higher-dimensional type theory, particularly 2-dimensional type theory as presented either here or here. On the surface, writing down the rules of W-types and how they should transform seems rather straight forward - an iso between shapes should create an appropriate iso between W-types as should an iso between contents. The thing I'm not sure about is how to fit W-types into Garner's 2-dimensional type theory semantics. Of course, I think part of the problem is that I'm not really familiar with the general story of models for W-types in type theory.
Other than that, I helped organize and teach the very first Portland intro to programming for women workshop. Feedback from students has been extremely positive so far and I'm really glad to have been involved and look forward to continue organizing these events.
