Experiments on formalizing type theory in type theory using Cubical Agda. In particular, I'm playing with
- encodings of the syntax of type theory as a higher inductive type;
- category model for directed TT, and higher-dimensional models (groupoids, simplicial sets, ...)