# 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? Commented Mar 16, 2019 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. Commented Mar 17, 2019 at 9:33
• You forgot the equalities ($\beta$-rule, and possibly $\eta$-rule if you want it). The paper explains the category-theoretic background. Commented Mar 17, 2019 at 13:41
• Yeah, I'm also looking for that. I've found a few references to the typing rules for W-types, but none for M-types. The best hint I got was from Agda's standard library, which implements both W-types and M-types (as inductive and coinductive types, respectively). Commented Jul 24, 2021 at 12:26

$$\frac{A:Type\quad x:A⊦B:Type}{(M x:A)B(x):Type}-\text{M-Formation}$$
$$\frac{C:Type\quad t: C\rightarrow \Sigma(a: A)(B[a / a]\rightarrow C)\quad c:C}{unfold(C,t,c):M}-\text{M-Introduction}$$
$$\frac{m:(M x:A)B(x)}{head(m):A\quad tail(m):B[head(m)/a]\rightarrow (M x:A)B(x)}-\text{M-Elimination}$$