improve readability by introducing EqInst
-rw-r--r-- 11 .gitignore
-rw-r--r-- 4308 Bidir.agda