root2 We show root 2 is irrational using Agda. We use the Agda version 2.6.2, and Agda stdlib verion 2.0.