Non-Wellfounded Trees in Homotopy Type Theory

Definition of M-types via Universal Property

M-Types

Example 6

Stream(A) ≡ M(A, 𝟏). P(X) = A × X.

Derivability of M-Types