module Enum where

open import Level renaming (zero to zeroL ; suc to sucL)
open import Function

open import Data.Unit
open import Data.Nat
open import Data.Fin
open import Data.Sum
open import Data.Product

UId : Set
UId = ⊤

Enum : Set
Enum = ℕ

EnumT : Enum → Set
EnumT = Fin

π : ∀{ℓ} (E : Enum)(T : EnumT E → Set ℓ) → Set ℓ
π zero T = Lift ⊤
π (suc E) T = T zero × π E (T ∘ suc)

appπ : ∀{ℓ}{E : Enum}{T : EnumT E → Set ℓ} →
       (f : π E T)(e : EnumT E) → T e
appπ (t , _) zero = t
appπ (_ , f) (suc e) = appπ f e

σ : ∀{ℓ} (E : Enum)(T : EnumT E → Set ℓ) → Set ℓ
σ E T = Σ[ e ∈ EnumT E ] T e

σmap : ∀{ℓ}{E : Enum}{T T' : EnumT E → Set ℓ} →
       (f : (e : EnumT E) → T e → T' e) →
       σ E T → σ E T'
σmap f (k , t) = (k , f k t)

δEnum : (E : Enum) → EnumT E → Enum
δEnum zero ()
δEnum (suc E) zero = E
δEnum (suc E) (suc k) = suc (δEnum E k)

δf : ∀{E}{ℓ}{X : Set ℓ} → (e : EnumT E) → (EnumT E → X) → EnumT (δEnum E e) → X
δf {zero} () f k
δf {suc E} zero f k = f (suc k)
δf {suc n} (suc e) f zero = f zero
δf {suc n} (suc e) f (suc k) = δf e (f ∘ suc) k