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.

  • 1
    $\begingroup$ 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). $\endgroup$
    – Trebor
    Mar 7, 2023 at 15:48
  • 5
    $\begingroup$ 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/… $\endgroup$
    – L. Garde
    Mar 7, 2023 at 20:34
  • $\begingroup$ @L.Garde It seems like that is what I am looking for. I have added an example. $\endgroup$
    – Nico
    Mar 7, 2023 at 21:15
  • $\begingroup$ @L.Garde I find it hard to relate to the question, because there are universes and $\Pi$-types everywhere. $\endgroup$
    – Nico
    Mar 7, 2023 at 21:18
  • $\begingroup$ Yet another question great for cstheory.stackexchange! (I promise I'll leave other comments some day...) $\endgroup$
    – cody
    Mar 24, 2023 at 20:22


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.