W-type (the type of well-founded, labelled trees) [ag-000I]

{-# OPTIONS --cubical --guardedness --two-level --no-level-universe #-}
module ag-000I where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sum
open import Cubical.Data.Nat

data 𝟘 : Type where
data 𝟙 : Type where
  ⋆ : 𝟙

W-type (due to Martin-Löf) 是 well-founded, labelled trees 的型別。每棵 W-type 的樹都可以有無限多分支，但 path 都是有限長。W 有兩個參數

1. S : Type 表示 shape
2. P : S → Type 表示有 (P s)-many positions

W 是 strictly positive inductive types 的 universal type。

data W (S : Type) (P : S → Type) : Type where
  sup-W : (s : S) → (P s → W S P) → W S P

Example: 自然數

module natural-number where
  S = 𝟙 ⊎ 𝟙

  P : S → Type
  P (inl _) = 𝟘 -- therefore, in this direction cannot go further
  P (inr _) = 𝟙 -- this direction has one continuation

  N = W S P

  z : N
  z = sup-W (inl ⋆) λ ()
  s : N → N
  s n = sup-W (inr ⋆) λ ⋆ → n

  α : ℕ → N
  α zero = z
  α (suc n) = s (α n)
  β : N → ℕ
  β (sup-W (inl ⋆) x) = zero
  β (sup-W (inr ⋆) f) = suc (β (f ⋆))

  main : (n : ℕ) → β (α n) ≡ n
  main zero =
    β (α zero) ≡⟨ refl ⟩
    β z ≡⟨ refl ⟩
    zero ∎
  main (suc n) = cong suc (main n)

  main⁻¹ : (n : N) → α (β n) ≡ n
  main⁻¹ (sup-W (inl ⋆) f) =
    α (β (sup-W (inl ⋆) f)) ≡⟨ refl ⟩
    z                       ≡⟨ refl ⟩
    sup-W (inl ⋆) (λ ())    ≡⟨ cong (sup-W (inl ⋆)) (sym (funExt λ ())) ⟩
    sup-W (inl ⋆) f ∎
  main⁻¹ (sup-W (inr ⋆) f) =
    α (β (sup-W (inr ⋆) f))           ≡⟨ refl ⟩
    α (suc (β (f ⋆)))                 ≡⟨ refl ⟩
    s (α (β (f ⋆)))                   ≡⟨ refl ⟩
    sup-W (inr ⋆) (λ _ → α (β (f ⋆))) ≡⟨ cong (sup-W (inr ⋆)) (funExt t) ⟩
    sup-W (inr ⋆) f ∎
    where
    t : (x : 𝟙) → α (β (f ⋆)) ≡ f x
    t ⋆ = main⁻¹ (f ⋆)