Most of my current work can be defined mathematically as abstract algebra. It is about structures that are often complex but the methods that I use are elementary except where the connections to other established areas of mathematics are concerned.
The main goal of this work is to advance the mathematical theory of dependent type theories to the level where it can be used for rigorous study of the complex type theories that are in use today and of the even more complex ones that will appear in the future. It is based on the approach that I envisioned in 2005-2009 and that is outlined in my 2010 CMU Lecture.
Dependent type theories appear today mostly in the "practical" form of computer programs that are using such theories, often vaguely specified, as their foundation. For example, if you ask someone from among the developers of the proof assistant Coq what ensures that a statement proved in Coq is mathematically meaningful and true they will tell you that Coq is based on the type theory that is called CIC (Calculus of Inductive Constructions) and that the "strong normalization theorem" for the CIC has been proved and, moreover, there is a program extraction mechanism that automatically translates any Coq code into an OCAML program and it shows that anything that you may write in Coq makes mathematical sense.
If you ask about abstract mathematical theorems such as a theorem about all groups that make assertions about non-inductive types or about proofs of mathematical theorems that use the law of excluded middle they may say that models of the CIC in set theory that satisfy the law of excluded middle for Prop have been constructed and that because of it anything that you prove in Coq is provable in set theory.
The mathematics that I currently work on is inspired by the need to verify the claims such as the one cited in the previous paragraph. I am trying to develop it in the way that I think the development of new mathematics will proceed in the future - I write papers, put them to the archive and submit to journals. At the same time I formalize the mathematics that is in the papers using Coq and the UniMath library.