------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed M-types (the dual of indexed W-types aka Petersson-Synek
-- trees).
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe --guardedness #-}
module Codata.Musical.M.Indexed where
open import Level using (Level; _⊔_)
open import Codata.Musical.Notation using (♭; ∞; ♯_)
open import Data.Product.Base using (_,_; proj₁; proj₂)
open import Data.Container.Indexed.Core
open import Function.Base using (_∘_)
open import Relation.Unary using (Pred; _⊆_)
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4