A theorem prover and programming language with a homotopy type system. Comes with a nifty IntelliJ plugin.