Definition concat {V : UU} {E : V → V → UU} {u v w : V} (p : gpaths E u v) (q : gpaths E v w) : gpaths E u w := foldr (λ _ _ , cons) q p.
Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Subtypes.