# nLab M-type

### Context

#### Induction

Could not include type induction - contents

# Contents

## Idea

The notion of M-type is the formal dual of that of W-type: a certain coinductive type.

The categorical semantics of an $M$-type is a terminal coalgebra of an endofunctor.

## References

• Benno van den Berg, de Marchi Non-well-founded trees in categories, APAL 146 (2007) 40–59.

Revised on October 4, 2012 23:53:53 by Urs Schreiber (82.169.65.155)