Update 'agda w-type stuff'

agda-w-type-stuff.md

@@ -0,0 +1,155 @@
+```agda
+module _ where
+
+open import Function
+open import Data.Container hiding (refl)
+open import Data.Container.Relation.Unary.All
+open import Data.W
+open import Data.Empty
+open import Data.Unit
+open import Relation.Nullary
+open import Data.Product renaming (proj₁ to fst; proj₂ to snd)
+open import Relation.Binary.PropositionalEquality
+
+variable A B : Set
+
+postulate ⊥-funext : {f g : ⊥ → B} → f ≡ g
+```
+
+# ℕ
+
+```agda
+module Nat where
+  data Tag : Set where #zero #suc : Tag
+
+  Child : Tag → Set
+  Child #zero = ⊥
+  Child #suc  = ⊤
+
+  Nat : Set
+  Nat = W (Tag ▷ Child)
+
+  zero : Nat
+  zero = sup (#zero , λ ())
+
+  suc : Nat → Nat
+  suc n = sup (#suc , const n)
+
+  elim : (P : Nat → Set) →
+         P zero → (∀ {n} → P n → P (suc n)) →
+         ∀ n → P n
+  elim P pz ps = induction P λ where
+    {#zero , _} (all ih) → subst (λ f → P (sup (#zero , f))) ⊥-funext pz
+    {#suc  , n} (all ih) → ps (ih tt)
+```
+
+# List
+
+```agda
+module List where
+  data Tag : Set where #nil #cons : Tag
+
+  Field : Set → Tag → Set
+  Field _ #nil  = ⊤
+  Field A #cons = A
+
+  Child : Tag → Set
+  Child #nil  = ⊥
+  Child #cons = ⊤
+
+  List : Set → Set
+  List A = W (Σ Tag (Field A) ▷ Child ∘ fst)
+
+  nil : List A
+  nil = sup ((#nil , tt) , λ ())
+
+  infixr 5 _∷_
+  _∷_ : A → List A → List A
+  x ∷ xs = sup ((#cons , x) , const xs)
+
+  elim : (P : List A → Set) →
+         (pn : P nil) →
+         (pc : (x : A) {xs : List A} → P xs → P (x ∷ xs)) →
+         ∀ xs → P xs
+  elim P pn pc = induction P $ λ where
+    {(#nil , tt) , rec} _ →
+      subst (λ f → P (sup ((#nil , tt) , f))) ⊥-funext pn
+    {(#cons , x) , xs′} (all ih) → pc x (ih tt)
+```
+
+# indexed w
+
+```agda
+record Desc : Set₁ where
+  field
+    Index : Set
+    Tag   : Set
+    Child : Tag → Set
+    this  : Tag → Index
+    child : ∀ {T} → Child T → Index
+
+module IndexedW (𝒟 : Desc) where
+  open Desc 𝒟
+
+  T′ : Set
+  T′ = W (Tag ▷ Child)
+
+  wf : T′ → Index → Set
+  wf = induction _ λ where
+    {t , _} (all ih) 𝑖 → (this t ≡ 𝑖) × (∀ c → ih c (child c))
+
+  T : Index → Set
+  T 𝑖 = Σ[ x ∈ T′ ] (wf x 𝑖)
+
+  isup : (t : Tag) (f : (c : Child t) → T (child c)) → T (this t)
+  isup t f = sup (t , fst ∘ f) , refl , snd ∘ f
+
+  module _ (P : ∀ {i} → T i → Set)
+           (s : ∀ t f → (∀ c → P (f c)) → P (isup t f)) where
+    iinduction′ : ∀ {𝑖} t (p : wf t 𝑖) → P (t , p)
+    iinduction′ t p =
+      induction (λ t → ∀ {𝑖} (p : wf t 𝑖) → P (t , p))
+      (λ where
+        {t , f} (all ih) (refl , eq-ih) →
+          s t (λ c → f c , eq-ih c)
+              (λ c → ih c (eq-ih c)))
+      t p
+
+    iinduction : ∀ {𝑖} (x : T 𝑖) → P x
+    iinduction (t , p) = iinduction′ t p
+```
+
+# fin (indexed)
+
+```agda
+module Fin where
+  open Nat public using (Nat; #zero; #suc)
+    renaming (zero to nzero; suc to nsuc)
+
+  desc : Desc
+  desc = let open Desc in λ where
+    .Index           → Nat
+    .Tag             → Nat.Tag × Nat
+    .Child (t , _)   → Nat.Child t
+    .this  (_ , n)   → Nat.suc n
+    .child {_ , n} c → n
+
+  open module Fin-W = IndexedW desc using (iinduction; isup)
+  open Fin-W public using () renaming (T to Fin)
+
+  private variable n : Nat
+
+  zero : Fin (nsuc n)
+  zero {n} = (sup ((#zero , n) , λ ())) , refl , λ ()
+
+  suc : Fin n → Fin (nsuc n)
+  suc {n} (i , p) = (sup ((#suc , n) , const i)) , refl , const p
+
+  elim : (P : ∀ {n} → Fin n → Set) →
+         (∀ {n} → P (zero {n})) →
+         (∀ {n} (i : Fin n) → P i → P (suc i)) →
+         (i : Fin n) → P i
+  elim P pz ps = iinduction P λ where
+    (#zero , n) f _  → subst (λ f → P (isup (#zero , n) f)) ⊥-funext pz
+    (#suc  , n) f ih → ps (f tt) (ih tt)
+```