According to nLab, M-types are the dual of W-types. What are the introduction and elimination rules for M-types?

Edit: For example, the formation/introduction/elimination rules for W-types are:

$$\frac{A:Type\quad x:A⊦B:Type}{(W x:A)B(x):Type}-\text{W-Formation}$$

$$\frac{a:A\quad t:B(a)\rightarrow W}{sup(a,t):W}-\text{W-Introduction}$$

$$\frac{w:W⊦C(w):Type\\ x:A,u:B(x)\rightarrow W, v:(\Pi y:B(x))C(u(y))⊦c(x,u,v)C(sup(x,u))}{w:W⊦wrec(w,c):C(w)}-\text{W-Elimination}$$

I'm wondering what the corresponding rules for M-types are.

  • $\begingroup$ Are you looking for something like this? $\endgroup$ – Andrej Bauer Mar 16 '19 at 8:46
  • $\begingroup$ Hi. I found that paper but I couldn't find a plain definition of M-types in it in terms that I understand. I'm looking for something more like the above (I've edited the question). Thanks for always answering my questions here and on reddit btw. $\endgroup$ – Andrew Cann Mar 17 '19 at 9:33
  • $\begingroup$ You forgot the equalities ($\beta$-rule, and possibly $\eta$-rule if you want it). The paper explains the category-theoretic background. $\endgroup$ – Andrej Bauer Mar 17 '19 at 13:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.