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