Defining infinitely many functions in one mutual recursion is precisely what Open Recursion a la Berger is.

First let's take a look on usual well-founded recursion. In type-theoretic setting, there is an inductive type (family) defined by a set of typed constructors. Terms defined by these constructors are by definition finite chains of constructors. If one substitutes a correspondingly typed function for each constructor and performs all reductions, one gets a value, that's how terms can be recursively transformed. Seen from the other perspective, this process can be described filling a dictionary step by step. All terms arising from inductive type family can be enumerated, the relation _is-subterm-of_ is well-founded by definition. In course of recursion, the dictionary term->value is filled step by step by a function that performs case analysis on the root constructor of the term can look up the dictionary entries for its subterms. Wellfoundness of the subterm relation guarantees that this process eventually fills every entry in the dictionary.

Open recursion works on possibly infinite sequences, such that truncations of the sequences are wellfounded, but the sequences as whole are not. (In type theoretic setting this idea can be used to work with untruncated higher inductive type families.) In this case the dictionary-filling performs case analysis on root constructors of the first n entries (n unbounded but guaranteed to be finite), is allowed to perform dictionary lookup for the subterms of inspected truncation and to transform the tail in a computable way. The ability to look unbounded but fixed number of terms ahead makes the thing ill-defined if any recursion rules were allowed, but as long as recursion rules are totally-computable, open recursion is total and productive: computable inbound sequences (in particular the truncated ones) produce computable results.

Now let's try to apply this idea to higher inductive types. Arguably simplest higher inductive type is the sphere S¹:

For performing recursion we need the following dataFamilyS¹: base : S¹ loop : base = base

StructureS¹-recdata: *TargetType : S¹ -> Type base-img : TargetType base loop-img : base-img =[TargetType loop]= base-img

(We allow for the following abuse of notation: any function f: A -> B can be applied not only to values of the type A, but also on paths p over A, p : (*x: A, *y: A, x = y), the result being action of p on paths of B. We use the mixfix operator of heterogenious equality x =[p]= y, where p is a path X = Y, x: X, y: Y.)

Using r : S¹-recdata you can eliminate both values x : (x : S¹) and paths l: (x = y) for (x, y : S¹). Since S¹ is 2-truncated it suffices to have two eliminators:

S¹-elim : (r : S¹-recdata) -> (x : S¹) -> (r.TargetType x) βloop/elim : (r : S¹-recdata) -> (S¹-elim r) loop = r.loop-imgFor 3-truncated type T we would also need a transformer for CoherentlyEqualVec 3 T = (a, b, c : T, d : a = b, e : b = c, f : d = e), and so on. In general one would like to have a transformer for coherently equal vectors of any length, preferably even infinite one. Infinite coherently equal vectors can be equivalently described as coherently constant functions, const C = (T : Type, f : ||T|| -> C) which naturally leads to the following type of recursor:

C-elim: (r : C-recdata) -> (x : const C) -> r.TargetType x(Here we extend the above mentioned abuse of notation allowing functions f: A -> B to be applied to const A, resulting in const B, i.e. we perform application of paths to paths on all levels.)

To transit to open recursion, we just supply "ready eliminator" restricted to the corresponding constructor to each constructor eliminator, just like this:

whereStructureS¹-recdata: *TargetType : S¹ -> Type base-img : {coh-elim (TargetType base)} -> TargetType base loop-img : {coh-elim (TargetType loop)} -> base-img =[Target-Type loop]= base-img

coh-elim : {C : Type} -> (T : C -> Type) -> (s : C) -> (c : const (s = s)) -> T cFor truncated types this is certainly trivial, but for nontruncated ones it's far from being so. In particular, open recursion should be able to express definition of heriditary substitution of unbounded level, so combining it with induction would lead to definition of semi-simplicial types and alike.