Definition currify {n: nat} {v: vec UU n} {B: UU} (f: hvec v → B): iterfun v B. Proof. revert n v f. refine (vec_ind _ _ _). - intros. exact (f tt). - intros x n xs IHxs f. simpl in f. simpl. intro a. exact (IHxs (λ l, f (a,, l))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.