Definition gpaths_of_length {V : UU} (E : V → V → UU) (v w : V) (n : nat) : UU. Proof. revert v. induction n as [|n IH]. - intro v. exact (v = w). - intro v. exact (∑u, E v u × IH u). Defined.
Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Subtypes.