------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed W-types aka Petersson-Synek trees
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.W.Indexed where

open import Level
open import Data.Container.Indexed.Core
open import Data.Product.Base using (_,_; Σ)
open import Relation.Unary

-- The family of indexed W-types.

module _ { c r} {O : Set } (C : Container O O c r) where

  open Container C

  data W (o : O) : Set (  c  r) where
    sup :  C  W o  W o

  -- Projections.

  head : W  Command
  head (sup (c , _)) = c

  tail :  {o} (w : W o) (r : Response (head w))  W (next (head w) r)
  tail (sup (_ , k)) r = k r

  -- Induction, (primitive) recursion and iteration.

  ind :  {} (P : Pred (Σ O W) ) 
        (∀ {o} (cs :  C  W o)   C P (o , cs)  P (o , sup cs)) 
         {o} (w : W o)  P (o , w)
  ind P φ (sup (c , k)) = φ (c , k)  r  ind P φ (k r))

  rec :  {} {X : Pred O }  ( C  (W  X)  X)  W  X
  rec φ (sup (c , k))= φ (c , λ r  (k r , rec φ (k r)))

  iter :  {} {X : Pred O }  ( C  X  X)  W  X
  iter φ (sup (c , k))= φ (c , λ r  iter φ (k r))