# Definition of M-type in type theory

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.

• Are you looking for something like this? – Andrej Bauer Mar 16 at 8:46
• 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. – Andrew Cann Mar 17 at 9:33
• You forgot the equalities ($\beta$-rule, and possibly $\eta$-rule if you want it). The paper explains the category-theoretic background. – Andrej Bauer Mar 17 at 13:41