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)