Definition reverse {V : UU} {E : V → V → UU} (H : issymmetric E) {u v : V} (p : gpaths E u v) : gpaths E v u. Proof. revert u p. apply gpaths_ind. - exact []. - intros u u' e p q. exact (append q (invmap (H u' u) e)). Defined.
Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Subtypes.