M types are types of coinductive trees on top of a dependent type theory.
In the presence of W types, natural numbers and Voevodsky's univalence axiom, indexed M types are definable. This is shown by [Ahrens et al. 2015].
Ahrens, Benedikt, Paolo Capriotti, and Régis Spadotti. 2015. ‘Non-Wellfounded Trees in Homotopy Type Theory’. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), edited by Thorsten Altenkirch, 38:17–30. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.TLCA.2015.17.
@InProceedings{ahrens_2015,
author = {Benedikt Ahrens and Paolo Capriotti and R{\'e}gis Spadotti},
title = {{Non-Wellfounded Trees in Homotopy Type Theory}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {17--30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
year = {2015},
volume = {38},
editor = {Thorsten Altenkirch},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
doi = {10.4230/LIPIcs.TLCA.2015.17},
}