An agda formalisation of the transitive closure of block matrices (extended abstract). - Adam Sandberg Eriksson; Patrik Jansson (TyDe@ICFP, 2016)