Hi there ice1000 or tizusa.
🌱 I have a blog, opensource-contributions, a resume, a research profile, an arXiv profile, and a codewars profile.🤔 I'm learning HoTT and is researching on its constructive interpretations, like cubical type theories. I'm also interested in 2LTT -- using XTT as the non-fibrant type theory might be a good idea?👨💻 I'm currently working on a dependently-typed programming language Aya with some interesting ideas. It's going to be a practical proof assistant with programming features.💬 Ask me about IDEs, type theories and implementation of (univalent) dependent type systems!