open import Level

module Chapter6.IDesc.Levitation 
         {ℓ k : Level}
         {I : Set k}
       where

open import Level
  renaming ( zero to zeroL
           ; suc to sucL )
open import Data.Unit
open import Data.Product

open import Category.Applicative

open import Relation.Binary.PropositionalEquality

open import Chapter2.Logic
open import Chapter2.IProp

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.Lifting
open import Chapter5.IDesc.Induction

open import Chapter6.IDesc


ψ : IDesc ℓ I → IDesc' ℓ I
ψ (`var i) = `var' i
ψ `1 = `1'
ψ (D `× D') = ψ D `×' ψ D'
ψ (`σ n T) = `σ' n λ k → ψ (T k)
ψ (`Σ S T) = `Σ' S λ s → ψ (T s)
ψ (`Π S T) = `Π' S λ s → ψ (T s)

private 
  record ⟨φ_⟩ (D : IDesc' ℓ I) : Set (k ⊔ (sucL ℓ)) where
    constructor return
    field 
      call : IDesc ℓ I
  open ⟨φ_⟩

  α : [ IDescD ℓ I ]^ (λ D → ⟨φ D ⟩) ⇒ (λ D → ⟨φ ⟨ proj₂ D ⟩ ⟩)
  α {_ , `var` , (lift i) , lift tt} (lift tt) = return (`var i)
  α {_ , `1` , lift tt} (lift tt) = return `1
  α {_ , `×` , D , D' , (lift tt)} (ihD , ihD' , lift tt) = return (call ihD `× call ihD')
  α {_ , `σ` , lift n , T , lift tt} (ih , lift tt) = return (`σ n λ k → call (ih (lift k)))
  α {_ , `Σ` , lift S , T , lift tt} (ih , lift tt) = return (`Σ S λ s → call (ih (lift (lift s))))
  α {_ , `Π` , lift S , T , lift tt} (ih , lift tt) = return (`Π S λ s → call (ih (lift (lift s))))

  φh : (D : IDesc' ℓ I) → ⟨φ D ⟩
  φh = induction (IDescD ℓ I) (λ D → ⟨φ D ⟩) (λ {i}{xs} → α {i , xs})

φ : (D : IDesc' ℓ I) → IDesc ℓ I
φ D = call (φh D)

⊢ψ∘φ : ∀ (D : IDesc' ℓ I) → ⊢ ψ (φ D) ≡ D
⊢ψ∘φ ⟨ `var` , i , lift tt ⟩ = pf refl
⊢ψ∘φ ⟨ `1` , lift tt ⟩ = pf refl
⊢ψ∘φ ⟨ `×` , A , B , lift tt ⟩ = 
  cong₂ (λ x y → ⟨ `×` , x , y , lift {ℓ = k ⊔ sucL ℓ} tt ⟩) <$> ⊢ψ∘φ A ⊛ ⊢ψ∘φ B 
⊢ψ∘φ ⟨ `σ` , E , T , lift tt ⟩ = 
  cong (λ x → ⟨ `σ` , E , x , lift {ℓ = k ⊔ sucL ℓ} tt ⟩) <$> 
         extensionality (λ e → ⊢ψ∘φ (T e))
⊢ψ∘φ ⟨ `Σ` , S , T , lift tt ⟩ = 
    cong (λ x → ⟨ `Σ` , S , x , lift {ℓ = k ⊔ sucL ℓ} tt ⟩) <$> 
         extensionality (λ s → ⊢ψ∘φ (T s))
⊢ψ∘φ ⟨ `Π` , S , T , lift tt ⟩ = 
    cong (λ x → ⟨ `Π` , S , x , lift {ℓ = k ⊔ sucL ℓ} tt ⟩) <$> 
         extensionality (λ s → ⊢ψ∘φ (T s))


⊢φ∘ψ : ∀ (D : IDesc ℓ I) → ⊢ φ (ψ D) ≡ D
⊢φ∘ψ (`var i) = pf refl
⊢φ∘ψ `1 = pf refl
⊢φ∘ψ (A `× B) = cong₂ (λ x y → x `× y) <$> ⊢φ∘ψ A ⊛ ⊢φ∘ψ B 
⊢φ∘ψ (`σ E T) = cong (λ x → `σ E x) <$> extensionality λ e → ⊢φ∘ψ (T e)
⊢φ∘ψ (`Σ S T) = cong (λ x → `Σ S x) <$> extensionality λ s → ⊢φ∘ψ (T s)
⊢φ∘ψ (`Π S T) = cong (λ x → `Π S x) <$> extensionality λ s → ⊢φ∘ψ (T s)