(cross posted from Reddit https://www.reddit.com/r/dependent_types/comments/b1ts8b/firstorder_multi_arity_functions_in_dependent_type/?
Take Agda for example, functions of multi arity is "encoded" as functions of one argument returning functions. In the same sense one can "encode" a record type as iterated Sigmas, but Agda has primitive first-order record type.
Then the problem is, in the encoded case, one can talk about functions of multiple arities generally, like function extensionality https://github.com/agda/cubical/blob/master/Cubical/Core/Prelude.agda#L105 . to apply function extensionality to functions of multiple arity, one just iteratively apply it multiple times.
It turns out Sigma type has also some general properties like this: https://github.com/agda/cubical/blob/master/Cubical/Foundations/HLevels.agda#L66 . So if record type is also encoded, then one can use this to a record type of multiple fields, just iterate it multiple times. But in case of Agda one cannot do this, because record type is primitive to Agda.
So is there a dependent type theory that has primitive multi-arity function types?
Also can we extends such a theory so we can talk generally of functions of multiple arity and records of multiple field? One goal is to write down a definition of "isContrRecord" in this new theory.
Any related reference?