module Chapter6.Desc.Levitation where

open import Level

open import Data.Unit
open import Data.Product

open import Category.Applicative
open import Category.Applicative.Indexed

open import Relation.Binary.PropositionalEquality

open import Chapter2.Logic
open import Chapter2.IProp

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint
open import Chapter4.Desc.Lifting
open import Chapter4.Desc.Induction

open import Chapter6.Desc


ψ : ∀{ℓ} → Desc ℓ → Desc' ℓ
ψ `var = `var'
ψ `1 = `1'
ψ (D `× D') = ψ D `×' ψ D'
ψ (D `+ D') = ψ D `+' ψ D'
ψ (`Σ S T) = `Σ' S λ s → ψ (T s)
ψ (`Π S T) = `Π' S λ s → ψ (T s)

private 
  record ⟨φ_⟩ {ℓ : Level}(D : Desc' ℓ) : Set (suc ℓ) where
    constructor return
    field 
      call : Desc ℓ
  open ⟨φ_⟩

  α : ∀{ℓ} → [_]^ {k = suc ℓ} (DescD ℓ) (λ D → ⟨φ D ⟩) ⇒ (λ D → ⟨φ ⟨ D ⟩ ⟩)
  α {i = `var` , lift tt} (lift tt) = return `var
  α {i = `1` , lift tt} (lift tt) = return `1
  α {i = `×` , D , D' , lift tt} (ihD , ihD' , lift tt) = return (call ihD `× call ihD')
  α {i = `+` , D , D' , lift tt} (ihD , ihD' , lift tt) = return (call ihD `+ call ihD')
  α {i = `Σ` , S , T , lift tt} (ih , lift tt) = return (`Σ S λ s → call (ih (lift s)))
  α {i = `Π` , S , T , lift tt} (ih , lift tt) = return (`Π S λ s → call (ih (lift s)))

  φh : ∀{ℓ} → (D : Desc' ℓ) → ⟨φ D ⟩
  φh {ℓ} = induction (DescD ℓ) (λ D → ⟨φ D ⟩) α 

φ : ∀{ℓ} (D : Desc' ℓ) → Desc ℓ
φ D = call (φh D)



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


⊢φ∘ψ : ∀ {ℓ}(D : Desc ℓ) → ⊢ φ (ψ D) ≡ D
⊢φ∘ψ `var = pf refl
⊢φ∘ψ `1 = pf refl
⊢φ∘ψ (A `× B) = cong₂ (λ x y → x `× y) <$> ⊢φ∘ψ A ⊛ ⊢φ∘ψ B
⊢φ∘ψ (A `+ B) = cong₂ (λ x y → x `+ y) <$> ⊢φ∘ψ A ⊛ ⊢φ∘ψ B
⊢φ∘ψ (`Σ S T) = cong (λ x → `Σ S x) <$> 
                    extensionality λ s → ⊢φ∘ψ (T s)
⊢φ∘ψ (`Π S T) = cong (λ x → `Π S x) <$> 
                    extensionality λ s → ⊢φ∘ψ (T s)