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