proposition: Lemma path_operation_uncurry_to_curry `{Funext} {σ} (A : Carriers σ) {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ) : operation_curry A ss t o operation_uncurry A ss t == idmap.
proof: Proof. intro a. induction n; [reflexivity|]. funext x. refine (_ @ IHn (fstail ss) (a x)). refine (ap (operation_curry A (fstail ss) t) _). funext a'. simpl. unfold cons_dom, cons_dom'. rewrite compute_fin_ind_fin_zero. refine (ap (operation_uncurry A (fstail ss) t (a x)) _). funext i'. now rewrite compute_fin_ind_fsucc. Qed.
imports: HoTT.Algebra.Universal.Algebra HoTT.Types HoTT.Spaces.Finite HoTT.Spaces.Nat.Core