Aqira Aqira is a happy little theorem prover, also a toy that evolves. Currently based on MLTT. License MIT