Table of Contents

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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 Data.Product
open import Relation.Binary.PropositionalEquality

variable A B : Set

postulate ⊥-funext : (f : ⊥ → B) → f ≡ λ ()

ℕ

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 $ p _ where
    p : ∀ t → □ (Tag ▷ Child) P t → P (sup t)
    p (#zero , f) _        rewrite ⊥-funext f = pz
    p (#suc  , _) (all ih) = ps $ ih _

list

non recursive arguments can be put in A.

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 = ⊤

  Body : Set → Set
  Body A = Σ[ t ∈ Tag ] (Field A t)

  List : Set → Set
  List A = W (Body A ▷ Child ∘ proj₁)

  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) →
         P nil → (∀ x {xs} → P xs → P (x ∷ xs)) →
         ∀ xs → P xs
  elim {A} P pn pc = induction P $ p _ where
    p : ∀ t → □ (Body A ▷ Child ∘ proj₁) P t → P (sup t)
    p ((#nil  , _) , f) (all ih) rewrite ⊥-funext f = pn
    p ((#cons , x) , f) (all ih) = pc x (ih _)

indexed w-types

see e.g. https://github.com/jashug/IWTypes

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 𝒟 public

  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 , proj₁ ∘ f) , refl , proj₂ ∘ f

  iinduction : (P : ∀ {𝑖} → T 𝑖 → Set)
               (s : ∀ t f → (∀ c → P (f c)) → P (isup t f)) →
               ∀ {𝑖} (t : T 𝑖) → P t
  iinduction P s (t , φ) = induction P′ (p _) t φ where
    P′ : T′ → Set
    P′ t = ∀ {𝑖} (φ : wf t 𝑖) → P (t , φ)

    p : ∀ t → □ (Tag ▷ Child) P′ t → ∀ {𝑖} φ → P (sup t , φ)
    p (t , f) (all ih) (refl , φ′) =
      s t (λ c → f c , φ′ c) (λ c → ih c (φ′ c))

fin

the elim doesn't actually compute properly because ⊥-funext gets stuck. oh well. not a problem for quox >:3

module Fin where
  open Nat public using (Nat; #zero; #suc)
    renaming (zero to nzero; suc to nsuc)

  module FinW =
    IndexedW (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)

  Fin = FinW.T

  private variable n : Nat

  zero : Fin (nsuc n)
  zero = FinW.isup (#zero , _) (λ ())

  suc : Fin n → Fin (nsuc n)
  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 = FinW.iinduction P p where
    p : ∀ t f → (∀ c → P (f c)) → P (FinW.isup t f)
    p (#zero , n) f ih rewrite ⊥-funext f = pz
    p (#suc  , n) f ih = ps (f _) (ih _)