Update 'agda w type stuff'

agda-w-type-stuff.md

@@ -7,13 +7,12 @@ 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
-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
+postulate ⊥-funext : (f : ⊥ → B) → f ≡ λ ()
 ```
 
 # ℕ
@@ -38,12 +37,15 @@ module Nat where
   elim : (P : Nat → Set) →
          P zero → (∀ {n} → P n → P (suc n)) →
          ∀ n → P n
-  elim P pz ps = induction P λ where
+  elim P pz ps = induction P $ p _ where
-    {#zero , _} (all ih) → subst (λ f → P (sup (#zero , f))) ⊥-funext pz
+    p : ∀ t → □ (Tag ▷ Child) P t → P (sup t)
-    {#suc  , n} (all ih) → ps (ih tt)
+    p (#zero , f) _        rewrite ⊥-funext f = pz
+    p (#suc  , _) (all ih) = ps $ ih _
 ```
 
-# List
+# list
+
+non recursive arguments can be put in `A`.
 
 ```agda
 module List where
@@ -57,8 +59,11 @@ module List where
   Child #nil  = ⊥
   Child #cons = ⊤
 
+  Body : Set → Set
+  Body A = Σ[ t ∈ Tag ] (Field A t)
+
   List : Set → Set
-  List A = W (Σ Tag (Field A) ▷ Child ∘ fst)
+  List A = W (Body A ▷ Child ∘ proj₁)
 
   nil : List A
   nil = sup ((#nil , tt) , λ ())
@@ -68,16 +73,17 @@ module List where
   x ∷ xs = sup ((#cons , x) , const xs)
 
   elim : (P : List A → Set) →
-         (pn : P nil) →
+         P nil → (∀ x {xs} → P xs → P (x ∷ xs)) →
-         (pc : (x : A) {xs : List A} → P xs → P (x ∷ xs)) →
          ∀ xs → P xs
-  elim P pn pc = induction P $ λ where
+  elim {A} P pn pc = induction P $ p _ where
-    {(#nil , tt) , rec} _ →
+    p : ∀ t → □ (Body A ▷ Child ∘ proj₁) P t → P (sup t)
-      subst (λ f → P (sup ((#nil , tt) , f))) ⊥-funext pn
+    p ((#nil  , _) , f) (all ih) rewrite ⊥-funext f = pn
-    {(#cons , x) , xs′} (all ih) → pc x (ih tt)
+    p ((#cons , x) , f) (all ih) = pc x (ih _)
 ```
 
-# indexed w
+# indexed w-types
+
+see e.g. <https://github.com/jashug/IWTypes>
 
 ```agda
 record Desc : Set₁ where
@@ -89,7 +95,7 @@ record Desc : Set₁ where
     child : ∀ {T} → Child T → Index
 
 module IndexedW (𝒟 : Desc) where
-  open Desc 𝒟
+  open Desc 𝒟 public
 
   T′ : Set
   T′ = W (Tag ▷ Child)
@@ -102,54 +108,54 @@ module IndexedW (𝒟 : Desc) where
   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
+  isup t f = sup (t , proj₁ ∘ f) , refl , proj₂ ∘ f
 
-  module _ (P : ∀ {i} → T i → Set)
+  iinduction : (P : ∀ {𝑖} → T 𝑖 → Set)
-           (s : ∀ t f → (∀ c → P (f c)) → P (isup t f)) where
+               (s : ∀ t f → (∀ c → P (f c)) → P (isup t f)) →
-    iinduction′ : ∀ {𝑖} t (p : wf t 𝑖) → P (t , p)
+               ∀ {𝑖} (t : T 𝑖) → P t
-    iinduction′ t p =
+  iinduction P s (t , φ) = induction P′ (p _) t φ where
-      induction (λ t → ∀ {𝑖} (p : wf t 𝑖) → P (t , p))
+    P′ : T′ → Set
-      (λ where
+    P′ t = ∀ {𝑖} (φ : wf t 𝑖) → P (t , φ)
-        {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
+    p : ∀ t → □ (Tag ▷ Child) P′ t → ∀ {𝑖} φ → P (sup t , φ)
-    iinduction (t , p) = iinduction′ t p
+    p (t , f) (all ih) (refl , φ′) =
+      s t (λ c → f c , φ′ c) (λ c → ih c (φ′ c))
 ```
 
-# fin (indexed)
+# fin
+
+the elim doesn't actually compute properly because `⊥-funext` gets
+stuck. oh well. not a problem for quox >:3
 
 ```agda
 module Fin where
   open Nat public using (Nat; #zero; #suc)
     renaming (zero to nzero; suc to nsuc)
 
-  desc : Desc
+  module FinW =
-  desc = let open Desc in λ where
+    IndexedW (let open Desc in λ where
-    .Index           → Nat
+      .Index           → Nat
-    .Tag             → Nat.Tag × Nat
+      .Tag             → Nat.Tag × Nat
-    .Child (t , _)   → Nat.Child t
+      .Child (t , _)   → Nat.Child t
-    .this  (_ , n)   → Nat.suc n
+      .this  (_ , n)   → Nat.suc n
-    .child {_ , n} c → n
+      .child {_ , n} c → n)
 
-  open module Fin-W = IndexedW desc using (iinduction; isup)
+  Fin = FinW.T
-  open Fin-W public using () renaming (T to Fin)
 
   private variable n : Nat
 
   zero : Fin (nsuc n)
-  zero {n} = (sup ((#zero , n) , λ ())) , refl , λ ()
+  zero = FinW.isup (#zero , _) (λ ())
 
   suc : Fin n → Fin (nsuc n)
-  suc {n} (i , p) = (sup ((#suc , n) , const i)) , refl , const p
+  suc i = FinW.isup (#suc , _) (const i)
 
   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
+  elim P pz ps = FinW.iinduction P p where
-    (#zero , n) f _  → subst (λ f → P (isup (#zero , n) f)) ⊥-funext pz
+    p : ∀ t f → (∀ c → P (f c)) → P (FinW.isup t f)
-    (#suc  , n) f ih → ps (f tt) (ih tt)
+    p (#zero , n) f ih rewrite ⊥-funext f = pz
-```
+    p (#suc  , n) f ih = ps (f _) (ih _)
+```