Generalize curry and uncurry

[langston-barrett]

I acknowledge this is a change to Foundations, so I leave it totally to your discretion @DanGrayson.

I see no harm in generalizing these definitions, though it also might be helpful to provide (several) non-dependent versions for simplicity. Some other changes would have to be made around the codebase before merging, either changing proofs to use a new non-dependent version or providing implicit arguments.

[DanGrayson]

I like the change, but it breaks some proofs, according to travis, such as this one:

COQC UniMath/Algebra/IteratedBinaryOperations.v
File "./UniMath/Algebra/IteratedBinaryOperations.v", line 460, characters 42-49:
Error:
In environment
n : nat
m : ⟦ n ⟧ → nat
k : ∏ i : ⟦ n ⟧, ⟦ m i ⟧ → nat
p : ∑ x : ⟦ n ⟧, ⟦ m x ⟧
Unable to unify "?Z0" with "?Z".

[langston-barrett]

@DanGrayson Right, that's what I was asking about. As I see it, we have two options:

1. Introduce another version of curry and uncurry for non-dependent functions and use this where the former versions used to be used.
2. Go through the proofs and explicitly add the Z parameter (which can't always be inferred, as seen in the error you posted).

What do you think?

[DanGrayson]

It turns out to be easy to specify that the third type family should be constant, so I suggest not having two versions of the functions, but applying this patch, instead:

diff --git a/UniMath/Algebra/IteratedBinaryOperations.v b/UniMath/Algebra/IteratedBinaryOperations.v
index dd7b7a75..e21d1706 100644
--- a/UniMath/Algebra/IteratedBinaryOperations.v
+++ b/UniMath/Algebra/IteratedBinaryOperations.v
@@ -457,7 +457,7 @@ Section NatCard.
   Defined.
 
   Corollary nat_plus_associativity' n (m:stn n->nat) (k:∏ i, stn (m i) -> nat) :
-    stnsum (λ i, stnsum (k i)) = stnsum (uncurry k ∘ lexicalEnumeration m).
+    stnsum (λ i, stnsum (k i)) = stnsum (uncurry (Z := λ _,_) k ∘ lexicalEnumeration m).
   Proof. intros. exact (nat_plus_associativity (uncurry k)). Defined.
 
   Lemma iterop_fun_nat {n:nat} (x:stn n->nat) : iterop_fun 0 add x = stnsum x.
diff --git a/UniMath/CategoryTheory/Inductives/Lists.v b/UniMath/CategoryTheory/Inductives/Lists.v
index 867d457e..a1175c8c 100644
--- a/UniMath/CategoryTheory/Inductives/Lists.v
+++ b/UniMath/CategoryTheory/Inductives/Lists.v
@@ -363,7 +363,7 @@ intros hF c L ccL HcL cc.
 use tpair.
 - transparent assert (HX : (cocone hF (hset_fun_space x HcL))).
   {  use mk_cocone.
-    * simpl; intro n; apply flip, curry, (pr1 cc).
+    * simpl; intro n; apply flip, (curry (Z := λ _,_)), (pr1 cc).
     * abstract (destruct cc as [f hf]; simpl; intros m n e;
                 rewrite <- (hf m n e); destruct e; simpl;
                 repeat (apply funextfun; intro); apply idpath).
@@ -389,7 +389,7 @@ use tpair.
     apply funextfun; intro xc; destruct xc as [x' c']; simpl;
     use (let g : HSET⟦colim (mk_ColimCocone hF c L ccL),
                                 hset_fun_space x HcL⟧ := _ in _);
-    [ simpl; apply flip, curry, t
+    [ simpl; apply flip, (curry (Z := λ _,_)), t
     | rewrite <- (colimArrowUnique _ _ _ g); [apply idpath | ];
       destruct cc as [f hf]; simpl in *;
       now intro n; simpl; rewrite <- (p n) ]

[langston-barrett]

Great, thanks for the patch! I've applied it and re-committed.

[mortberg]

lgtm