module Chapter5.Equivalence.ToContainer 
         {I J : Set}
       where

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

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

open import Chapter5.IDesc
open import Chapter5.Container


Shape : IDesc zeroL I → Set
Shape `1 = ⊤
Shape (`var i) = ⊤
Shape (D₁ `× D₂) = Shape D₁ × Shape D₂
Shape (`σ n T) = Σ[ k ∈ Fin n ] Shape (T k)
Shape (`Σ S T) = Σ[ s ∈ S ] Shape (T s)
Shape (`Π S T) = (s : S) → Shape (T s)
  
Pos : (D : IDesc zeroL I) → Shape D → Set
Pos `1 tt = ⊥
Pos (`var i) sh = ⊤
Pos (D₁ `× D₂) (d₁ , d₂) = Pos D₁ d₁ ⊎ Pos D₂ d₂
Pos (`σ n T) (k , t) = Pos (T k) t
Pos (`Σ S T) (s , t) = Pos (T s) t
Pos (`Π S T) f = Σ[ s ∈ S ]  Pos (T s) (f s)

Next : (D : IDesc zeroL I)(sh : Shape D) → Pos D sh → I
Next `1 sh ()
Next (`var j) tt tt = j
Next (D₁ `× D₂) (d₁ , d₂) (inj₁ p₁) = Next D₁ d₁ p₁
Next (D₁ `× D₂) (d₁ , d₂) (inj₂ p₂) = Next D₂ d₂ p₂
Next (`σ n T) (k , sh) ps = Next (T k) sh ps
Next (`Σ S T) (s , sh) ps = Next (T s) sh ps
Next (`Π S T) f (s , ps) = Next (T s) (f s) ps

⟨_⟩ : func zeroL I J → I ▸ J
⟨ D ⟩ = record { S = λ j → Shape (func.out D j)
               ; P = λ {j} sh → Pos (func.out D j) sh
               ; n = λ {j}{sh} ps → Next (func.out D j) sh ps }