Axiom allows the user to dynamically create dependent types. For example, matrix(3,3) is a 3x3 matrix. This may seem trivial but it is not.
Consider that to construct the "domain" (as it is called in Axiom) of 3x3 matrices you need to evaluate the arguments. Again, in this case it is trivial but, in general, it is not. Among other things it defines what functions are available to manipulate 3x3 matrices, e.g. inverse. Several issues arise. One is the "representation" (aka "carriers" in logic-speak). There is no reason to assume that the entries are integers. In the new Axiom (aka SANE) the "representation" is orthogonal to the domain and can be specified at construction. Axiom allows matrices that contain anything. When constructing a new matrix, e.g. [[2.3,...],[4.4,...]..] the entries may be from other "domains", in this case the floats. But they could just as well be polynomials. So from matrix(3,3) you need to dynamically construct matrix(3,3,FLOAT). Another issue is inheriting theorems and definitions that support the newly constructed domain. In the new Axiom, the theorems and definitions are associated with the "category hierarchy". They are inherited based on the dynamically constructed domain. These are available to prove functions in the constructed domain. A matrix(3,3) is commutative but matrix(3,4) is not. The property of commutativity is inherited from the hierarchy but only for square matrices. This has to be decided at the time the domain is constructed. This allows proofs of functions in the 3x3 domain to use the commutative theorems of square matrices. These are not available for functions in the 3x4 domain. So, clearly, we need to evaluate the arguments when constructing the domain. Ah, but evaluating the arguments of a dependent type is NOT trivial in general. You could, for example, construct domains which contain themselves in the argument, such as matrix(matrix(... More fun exists because one could, for example, introduce a new "category" into the hierarchy that has additional definitions and theorems related to square matrices over some new domain. These have to be dynamically inherited in particular cases. Worse yet, the elements don't have to be PROP but could be anywhere in the type hierarchy. The elements could be functors, for example. I've spent a great deal of time pondering these problems. My current "solution path" involves constructing objects in CLOS (Common Lisp Object System) which allows me to achieve very fine-grained control due to the MOP (Meta Object Protocol). In addition, I'm trying to make the domains as "declarative" as possible so that most of the details are not hidden in obscure code. CLOS allows both dynamic construction and dynamic re-shaping. I have no idea how LEAN4 will handle these without the MOP. Are you aware of any LEAN4 design documents that addresses these questions?