Arend: A theorem prover based on Homotopy Type Theory | Heykuki News