I think there’s some pretty cool applications to be built upon homotopy type theory/ univalent foundations. One use case I’m working on is building a structured version control system that allows versioned documents to be translated to code at compile time. Think rich text translations or other static assets that you may want to change at runtime. One really interesting exploitation of the univalence axiom is that you can make hot updates to compiled code without having to recompile the entire system by knowing if the identity paths of the updated document state is a topological subset of the document used at compile time. If it is, you know the updated generated code is isomorphic with the compile time code, meaning it’s safe to swap out. That’s pretty mind blowing and (seems very) practical to me. Basically allows for higher order configuration editing.