Lemma gpaths_ind {V : UU} {E : V → V → UU} {w : V} (P : ∏{u}, gpaths E u w → UU) (H1 : P []) (H2 : ∏{u v} (e : E u v) (p : gpaths E v w), P p → P (e :: p)) {u : V} (p : gpaths E u w) : P p. Proof. induction p as [n p]. revert u p. induction n as [|n IH]. - induction p. exact H1. - induction p as [v x]. induction x as [e p]. apply (H2 _ _ _ (n,, p)). apply IH. Defined.
Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Subtypes.