Another thought is that Axiom is "not fully factored". There is
a logic and category theory concept called "the carrier". In
Axiom terms, this is the Rep aka the representation. Axiom
bundles the representation with the domain, which is reasonable.
However, representations are likely data structur
One of the struggles of working with first-class dependent types
is that they can be created "on the fly". Ideally, when used, the
type information can be "factored out" to yield a specialized
version that is more efficient. The idea is best described in a
book, called Partial Evaluation, which use
