proposition: Remark mirror_edge_adj : @fun_adjunction mirror G face edge (finv edge) G.
proof: Proof. apply: strict_adjunction=> //; try apply: faceI; try exact: (@cedgeC dual). by apply/subsetP => x _; rewrite -(@nodeK G x) codom_f. by move=> x y _ /=; rewrite (inj_eq faceI) (finv_eq_can edgeK). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)