Set quotients by dependent products of finite families of equivalence relations

[lowasser]

A step short of applying these to finite sequences, but slightly more general. The finite sequence version will come as a follow-up.

[malarbol]

Hi! Just wanted to point out the module https://unimath.github.io/agda-unimath/foundation.tuples-of-types.html which defines

tuple-types : (l : Level) (n : ℕ) → UU (lsuc l)
tuple-types l n = Fin n → UU l

It seems that we should either remove it, or rename it to fit the new name scheme, in particular the difference between tuple / fin-sequence which makes this definition of tuple-types quite wrong.

[lowasser]

I am definitely in agreement that there's cleanup that needs to be done on some of the older types -- the entire multivariable-inputs family as well -- but I'm saving that for separate PRs.

[malarbol]

I am definitely in agreement that there's cleanup that needs to be done on some of the older types -- the entire multivariable-inputs family as well -- but I'm saving that for separate PRs.

Yes, I stumbled upon multivariable-inputs recently and was quite surprised it was defined as iterated cartesian products instead of the more natural (i : Fin n) → A i. Is it part of the refactoring you have in mind?

[lowasser]

Yes. I'm not convinced we need multivariable-inputs at this point or that it's a clear name for anything, and I'm mostly inclined to replace it with dependent functions where possible, but I'm trying in this PR to do the bare minimum to avoid naming conflicts with the alternatives.