use fromFunc to define union
-rw-r--r-- 11 .gitignore
-rw-r--r-- 23435 Bidir.agda
-rw-r--r-- 6487 FinMap.agda