fact: Record hypermap := Hypermap { dart :> finType; edge : dart -> dart; node : dart -> dart; face : dart -> dart; _ : cancel3 edge node face }.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)