Structural equality for inductive types

Zippy.agda

module Zippy where

data Desc : Set₁ where
  `σ : (A : Set) (d : A → Desc) → Desc
  `r : Desc → Desc
  `q : Desc

open import Size
open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality

⟦_⟧_ : Desc → Set → Set
⟦ `σ A d ⟧ X = Σ[ a ∈ A ] ⟦ d a ⟧ X
⟦ `r d   ⟧ X = X × ⟦ d ⟧ X
⟦ `q     ⟧ X = ⊤

Zip : (d : Desc) {X Y : Set} (R : X → Y → Set) → ⟦ d ⟧ X → ⟦ d ⟧ Y → Set
Zip (`σ A d)  R (a , t) (b , u) = Σ[ eq ∈ b ≡ a ]
                                  Zip (d a) R t (subst (λ a → ⟦ d a ⟧ _) eq u)
Zip (`r d)    R (x , t) (y , u) = R x y × Zip d R t u
Zip `q        R t       u       = ⊤

data μ (d : Desc) : Size → Set where
  con : {i : Size} → ⟦ d ⟧ (μ d) i → μ d (↑ i)

Eq : (d : Desc) → {i : Size} → μ d i → μ d i → Set
Eq d (con t) (con u) = Zip d (Eq d) t u