{-
-- M type implemetation based on
-- https://arxiv.org/pdf/1504.02949.pdf
-- "Non-wellfounded trees in Homotopy Type Theory"
-- Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
-}
{-# OPTIONS --guardedness --safe #-}
module Cubical.Codata.M.M where

open import Cubical.Codata.M.M.Base public
open import Cubical.Codata.M.M.Properties public