# Elimination rules of inductive types

Why does the elimination rule of inductive types sometimes allow the target type to depend on the inductive type and sometimes not? I am confused by that. Is it correct that it makes no difference in the presence of $$\Sigma$$-types?

Edit. Here is an example. Sometimes the elimination rule of sum types looks like this:

\begin{align} \frac{\Gamma \vdash C \,type\quad\Gamma,x:A\vdash t:C\quad\Gamma,y:B\vdash s:C}{\Gamma,z:A+B\vdash ind_+(z,x.t,y.s):C} \end{align}

while at other times it looks like this

\begin{align} \frac{\Gamma, z:A+B \vdash C \,type\quad\Gamma,x:A\vdash t:C\{inl(x)/z\}\quad\Gamma,y:B\vdash s:C\{inr(y)/z\}}{\Gamma,z:A+B\vdash ind_+(z,x.t,y.s):C} \end{align}

I also observed this with other types whose categorical semantic has a mapping out universal property. I.e. the empty type, natural numbers, quotients and so on.

• Can you provide the source of "sometimes allow ... and sometimes not"? This helps us address the actual problem (e.g. whether the presentation of the material you are reading is confusing or plain wrong).
– Trebor
Mar 7, 2023 at 15:48
• It seems that you are referring to the difference between recursion and induction in dependent type theory. Recursion is a special case of induction, and induction can be obtained from recursion using Sigma types and a proof of the expected behaviour of recursion. See math.stackexchange.com/questions/4382772/… Mar 7, 2023 at 20:34
• @L.Garde It seems like that is what I am looking for. I have added an example.
– Nico
Mar 7, 2023 at 21:15
• @L.Garde I find it hard to relate to the question, because there are universes and $\Pi$-types everywhere.
– Nico
Mar 7, 2023 at 21:18
• Yet another question great for cstheory.stackexchange! (I promise I'll leave other comments some day...)
– cody
Mar 24, 2023 at 20:22