I recently learned something about induction principles (or eliminators) for inductive types (I assume non-higher inductive types in the following context), a topic I had postponed for many years LOL. By manually working through eliminators, I finally understand them and have implemented a generator for them in violet.

When we get an inductive type:

data Bool : U where
  true : Bool
  false : Bool

we collect its information:

Bool : U is a type without dependencies
true is a Bool, no telescope; false is similar

Here, I need to explain telescope tele, telescope is a list of bindings, for example, inductive type List define as

data List (A : U) : U where
  ...

then List has the type (A : U) -> U, the tele of this type is [{name="A"; bound=Universe}]. When we say apply k to a telescope, we mean the variables in the telescope are (assumed to be) available in the context, and we apply k to these variables. Take List as an example again: applying List to [(A : U)] will construct an application List A.

Now let's consider the type of Bool-elim

Bool-elim : (M : (i : Bool) -> U)
          -> (case-true : M true)
          -> (case-false : M false)
          -> (i : Bool)
          -> M i

To generate such type for inductive types, I separate the algorithm into the following parts:

The type of motive
The type of each case. This represents the how to compute part
The final what to compute part: an input of the inductive type that should result in the motive

To explain the algorithm, we need some conventions. D is the name of current inductive type, for example, data List (A : U) : U where ... has D = List, not D = List A

Motive part [local-0]

If no dependencies, D -> U is what we want!
otherwise, we need to apply them tele -> D tele -> U. For example, motive type of List is
```
(A : U) -> (List A) -> U
```

Case type [local-1]

For each case, we also need to see its telescope to decide the type of this case. For trivial case like true : Bool, we apply M on it

M true

But let's take a more complicated example Nat:

data Nat : U where
  zero : Nat
  suc : Nat -> Nat

suc is interesting, because Nat is there in the telescope, that's where special behavior is needed: the type we want here is

(x- : Nat) -> M x- -> M (suc x-)

But how do we figure out that x- uses D? My approach is to evaluate this variable in an open context. By having the runtime represent inductive types specially, I can see it stuck at IndType name spine (this internal representation), then compare the name with D.

When a binding in the telescope recursively use D, I need to apply M on it and insert this as a dependency of this case.

The final what to compute part is rather easy. By inserting the telescope of the inductive type itself and applying M to the telescope and input, we construct the type we expect.

However, though my algorithm produces reasonable results, my unification algorithm cannot solve all of them (it gets stuck in infinite loops or unifies incorrect terms), for example, identity type fall into an infinite loop, so that would be another one of my forever-postponed jobs LOL. Also, I have not yet generated the computation but only the type of eliminators; this should be done in the future.