I would like to focus on the following part of the question:
I'd like to use such a construction to formalise universal algebra and apply the constructions and theorems of this theory to some concrete varieties (like boolean algebras, lattices, groups).
Let us forget about formalization for a moment and recall how universal algebra is done mathematically. We shall use an unusually high level of precision to expose a piece of invisible mathematics that is making formalization difficult.
Given a number $n \in \mathbb{N}$, let $[n] = \{k \in \mathbb{N} \mid k < n\}$ be the set of numbers smaller than it.
A signature $\Sigma = (n, a)$ is a number $n \in \mathbb{N}$ with a map $a : [n] \to \mathbb{N}$. Intuitively $\Sigma$ describes an algebraic structure with $n$ operations, where the $i$-th operation has arity $a(i)$.
Remark: One would traditionally write $\Sigma$ as an $n$-tuple $(a(0), \ldots, a(n-1))$ of numbers, but we want to avoid ellipsis $\ldots$ and keep the level of precision high.
Let us continue. A $\Sigma$-structure $(S, f)$ is a set $S$ with a map $f : \prod_{i \in [n]} S^{[a(i)]} \to S$. Thus for each $i \in [n]$ we have a map $f_i : S^{[a(i)]} \to S$. This is a perfectly good general definition that works well when we want to prove theorems about all structures for an arbitrary signature $\Sigma$.
However, taking the definition literally and applying it directly to specific examples results in a great deal of clumsiness. Here's an example.
Example 1: Consider the signature $\Sigma = (3, \lambda i. i)$. Let $G = ([7], f)$ be the $\Sigma$-structure with $f : \prod_{i \in [3]} [7]^{[i]} \to [7]$ defined by
\begin{align*}
f_0(u) &= 0, \\
f_1(u) &= 7 - u(0), \\
f_2(u) &= (u(0) + u(1)) \mathbin{\mathrm{mod}} 7.
\end{align*}
If you squint and think a bit, you will recognize that $G$ is a convoluted way of defining a cyclic group of order 7. Normal people define it as follows.
Example 2: Define $\mathbb{Z}_7 = ([7], e, i, m)$ where $e = 0$, $i : [7] \to [7]$ is defined by $i(k) = 7 - k$ and $m : [7] \times [7] \to [7]$ is defined by $m(k,m) = (k + m) \mathbin{\mathrm{mod}} 7$.
Examples 1 and 2 both define "essentially the same" structure. More precisely, there is an isomorphism
$$\textstyle
\left(\prod_{i \in [3]} [7]^{[i]} \to [7]\right) \cong
[7] \times [7]^{[7]} \times [7]^{[7] \times [7]}
$$
which can be used to translate between $G$ and $\mathbb{Z}_7$. However, you will not be able to find a book on universal algebra which does so explicitly. The formal difference between $G$ and $\mathbb{Z}_7$ is considered inessential, and identification of $G$ and $\mathbb{Z}_7$ convenient and harmless.
We may put back on our formalization hats. All of the ingredients above can be formalized in a straightforward way, except the identification of $G$ and $\mathbb{Z}_7$. The damn machine demands mathematical precision. So we are in an unfortunate situation that we know how to formalize both a general theory universal algebra and concrete examples of algebraic structures, but the two parts do not fit together easily.
I have no solution to offer, I just wanted to explain that this was a problem in formalization of invisible mathematics. If anyone knows a good solution, I would be interested to hear it.
A^n
is usually written asfin n -> A
; does this work for your purposes? $\endgroup$(fin n.succ -> A) -> B
toA -> (fin n -> A) -> B
, but I'm tempted to say that may be a bit annoying. $\endgroup$