Definition append {V : UU} {E : V → V → UU} {u v w : V} (p : gpaths E u v) (e : E v w) : gpaths E u w := p ++ e::[].
Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Subtypes.