Can this formulation be trivially extended for each constructor by simply adding a Ci for an additional inductive case?
Yes. I can't provide a general nor a technical answer, but a while ago I was trying to solve a similar problem and someone helped me by providing a visualization of the general procedure. This helped me a lot, so I'll reproduce it here in the case it helps you too.
Generating the elimination principle
Given an inductive type of the form (using Agda syntax):
data Foo : (index_0 : I_0) -> ... (index_N : I_N) -> Set where
ctor_0 : (field_0 : F_0) -> ... (field_N : F_N) -> ret_0
...
ctor_N : (field_0 : F_0) -> ... (field_N : F_N) -> ret_N
Its elimination is, generally, in that form:
let Foo_match =
-- Index arguments
(index_0 : I_0) -> ...
(index_N : I_N) ->
-- Scrutinee
(X : Foo index_0 ... index_n) ->
-- Motive
(P :
(index_0 : I_0) -> ...
(index_n : I_N) ->
(witness : Foo I_0 ... I_N) ->
Set) ->
-- Constructor arguments
(ctor_0 :
(field_0 : F_0) -> ...
(field_N : F_N) ->
ret_0[Foo/P] (ctor_0 field_0 ... field_N)) ->
(ctor_N :
(field_0 : F_0) -> ...
(field_N : F_N) ->
ret_N[Foo/P] (ctor_N field_0 ... field_N)) ->
-- Result type
P index_0 ... index_N X
Where [Foo/P]
means we replace the constructor type by the variable P
in ret_N
.
Example
If our type is:
data Vect : (A : Set) -> (n : Nat) -> Set where
cons : (A : Set) -> (n : Nat) -> (x : A) -> (xs : Vect A n) -> Vect A (succ n)
nil : (A : Set) -> Vect A zero
Then we get:
let Vect_match =
-- Index arguments
(A : Set) -> ...
(n : Nat) ->
-- Scrutinee
(X : Vect A n) ->
-- Motive
(P : (A : Set) -> (n : Nat) -> Vect A n -> Set) ->
-- Constructor arguments
(cons :
(A : Set) ->
(n : Nat) ->
(x : A) ->
(xs : Vect A n) ->
P A (succ n) (cons A n x xs)) ->
(nil :
P A zero nil) ->
-- Result type
P A n X
Note: I've not included parameters, but they're trivial. They work like indices, except they're not included on the constructors. I've also not included the inductive argument, so this is not actually the elimination principle, just total pattern-matching. You can get induction by applying Foo_match
recursively to sub terms. Problem is I don't remember out of my head its shape, but someone is welcome to edit in.