Imported Upstream version 0.8

1 files changed, 42 insertions, 0 deletions

diff --git a/src/Data/M/Indexed.agda b/src/Data/M/Indexed.agda
new file mode 100644
index 0000000..efd87f9
--- /dev/null
+++ b/src/Data/M/Indexed.agda
@@ -0,0 +1,42 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Indexed M-types (the dual of indexed W-types aka Petersson-Synek
+-- trees).
+------------------------------------------------------------------------
+
+module Data.M.Indexed where
+
+open import Level
+open import Coinduction
+open import Data.Product
+open import Data.Container.Indexed.Core
+open import Function
+open import Relation.Unary
+
+-- The family of indexed M-types.
+
+module _ {ℓ c r} {O : Set ℓ} (C : Container O O c r) where
+
+  data M (o : O) : Set (ℓ ⊔ c ⊔ r) where
+    inf : ⟦ C ⟧ (∞ ∘ M) o → M o
+
+  open Container C
+
+  -- Projections.
+
+  head : M ⊆ Command
+  head (inf (c , _)) = c
+
+  tail : ∀ {o} (m : M o) (r : Response (head m)) → M (next (head m) r)
+  tail (inf (_ , k)) r = ♭ (k r)
+
+  force : M ⊆ ⟦ C ⟧ M
+  force (inf (c , k)) = c , λ r → ♭ (k r)
+
+  -- Coiteration.
+
+  coit : ∀ {ℓ} {X : Pred O ℓ} → X ⊆ ⟦ C ⟧ X → X ⊆ M
+  coit ψ x = inf (proj₁ cs , λ r → ♯ coit ψ (proj₂ cs r))
+    where
+    cs = ψ x