Definition foldr {V : UU} {E : V → V → UU} {w : V} {B : V → UU} (f : ∏{u v}, E u v → B v → B u) (b : B w) : ∏{u : V}, gpaths E u w → B u. Proof. apply gpaths_ind. exact b. exact (λ u v e _ b, f u v e b). Defined.
Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Subtypes.