Chuangjie Xu, April 2017

We simplify T terms by removing (some) noncomputational information,
i.e. the parts of type (equivalent to) ①.  For example, a term

    t : 𝟙 → ℕ × 𝟙

will be simplified to

    pr₁ (t ⋆) : ℕ

\begin{code}

module Simp where

open import Preliminaries
open import DataTypes
open import H

\end{code}

Type equality is decidable.

\begin{code}

Ty-dec : (σ τ : Ty) → σ ≡ τ + σ ≢ τ
Ty-dec ① ① = inl refl
Ty-dec ① ② = inr (λ ())
Ty-dec ① Ⓝ = inr (λ ())
Ty-dec ① (τ *) = inr (λ ())
Ty-dec ① (τ ⊠ τ₁) = inr (λ ())
Ty-dec ① (τ ⇾ τ₁) = inr (λ ())
Ty-dec ② ① = inr (λ ())
Ty-dec ② ② = inl refl
Ty-dec ② Ⓝ = inr (λ ())
Ty-dec ② (τ *) = inr (λ ())
Ty-dec ② (τ ⊠ τ₁) = inr (λ ())
Ty-dec ② (τ ⇾ τ₁) = inr (λ ())
Ty-dec Ⓝ ① = inr (λ ())
Ty-dec Ⓝ ② = inr (λ ())
Ty-dec Ⓝ Ⓝ = inl refl
Ty-dec Ⓝ (τ *) = inr (λ ())
Ty-dec Ⓝ (τ ⊠ τ₁) = inr (λ ())
Ty-dec Ⓝ (τ ⇾ τ₁) = inr (λ ())
Ty-dec (σ *) ① = inr (λ ())
Ty-dec (σ *) ② = inr (λ ())
Ty-dec (σ *) Ⓝ = inr (λ ())
Ty-dec (σ *) (τ *) = case (λ e → inl (*⁼ e)) (λ f → inr (λ e → f (lm e))) (Ty-dec σ τ)
 where
  lm : {A B : Ty} → A * ≡ B * → A ≡ B
  lm refl = refl
Ty-dec (σ *) (τ ⊠ τ₁) = inr (λ ())
Ty-dec (σ *) (τ ⇾ τ₁) = inr (λ ())
Ty-dec (σ ⊠ σ₁) ① = inr (λ ())
Ty-dec (σ ⊠ σ₁) ② = inr (λ ())
Ty-dec (σ ⊠ σ₁) Ⓝ = inr (λ ())
Ty-dec (σ ⊠ σ₁) (τ *) = inr (λ ())
Ty-dec (σ ⊠ σ₁) (τ ⊠ τ₁) = case (λ e → case (λ e₁ → inl (⊠⁼ e e₁)) (λ f → inr (λ e₁ → f (lm₁ e₁))) (Ty-dec σ₁ τ₁))
                                (λ f → inr (λ e → f (lm₀ e)))
                                (Ty-dec σ τ)
 where
  lm₀ : {A A' B B' : Ty} → (A ⊠ A') ≡ (B ⊠ B') → A ≡ B
  lm₀ refl = refl
  lm₁ : {A A' B B' : Ty} → (A ⊠ A') ≡ (B ⊠ B') → A' ≡ B'
  lm₁ refl = refl  
Ty-dec (σ ⊠ σ₁) (τ ⇾ τ₁) = inr (λ ())
Ty-dec (σ ⇾ σ₁) ① = inr (λ ())
Ty-dec (σ ⇾ σ₁) ② = inr (λ ())
Ty-dec (σ ⇾ σ₁) Ⓝ = inr (λ ())
Ty-dec (σ ⇾ σ₁) (τ *) = inr (λ ())
Ty-dec (σ ⇾ σ₁) (τ ⊠ τ₁) = inr (λ ())
Ty-dec (σ ⇾ σ₁) (τ ⇾ τ₁) = case (λ e → case (λ e₁ → inl (⇾⁼ e e₁)) (λ f → inr (λ e₁ → f (lm₁ e₁))) (Ty-dec σ₁ τ₁))
                                (λ f → inr (λ e → f (lm₀ e)))
                                (Ty-dec σ τ)
 where
  lm₀ : {A A' B B' : Ty} → (A ⇾ A') ≡ (B ⇾ B') → A ≡ B
  lm₀ refl = refl
  lm₁ : {A A' B B' : Ty} → (A ⇾ A') ≡ (B ⇾ B') → A' ≡ B'
  lm₁ refl = refl

\end{code}

A special case function for defining the simpᴹ/backᴹ function.

\begin{code}

careⁱʳ : {A C : Set} → C → C → A + ¬ A → C
careⁱʳ c₀ c₁ (inl _) = c₀
careⁱʳ c₀ c₁ (inr _) = c₁

Lemma[careⁱʳ]₀ : {A C : Set} {c₀ c₁ : C}
           → A   → (w : A + ¬ A) → careⁱʳ c₀ c₁ w ≡ c₀
Lemma[careⁱʳ]₀ a (inl _) = refl
Lemma[careⁱʳ]₀ a (inr f) = 𝟘-elim (f a)

Lemma[careⁱʳ]₁ : {A C : Set} {c₀ c₁ : C}
           → ¬ A → (w : A + ¬ A) → careⁱʳ c₀ c₁ w ≡ c₁
Lemma[careⁱʳ]₁ f (inl a) = 𝟘-elim (f a)
Lemma[careⁱʳ]₁ f (inr _) = refl

\end{code}

Simplcareⁱʳy types

\begin{code}

simpᵀ : Ty → Ty
simpᵀ ① = ①
simpᵀ ② = ②
simpᵀ Ⓝ = Ⓝ
simpᵀ (σ *) = careⁱʳ ① (σᵀ *) (Ty-dec σᵀ ①)
 where
  σᵀ : Ty
  σᵀ = simpᵀ σ
simpᵀ (σ ⊠ τ) = careⁱʳ τᵀ (careⁱʳ σᵀ (σᵀ ⊠ τᵀ) (Ty-dec τᵀ ①)) (Ty-dec σᵀ ①)
 where
  σᵀ τᵀ : Ty
  σᵀ = simpᵀ σ
  τᵀ = simpᵀ τ
simpᵀ (σ ⇾ τ) = careⁱʳ τᵀ (careⁱʳ ① (σᵀ ⇾ τᵀ) (Ty-dec τᵀ ①)) (Ty-dec σᵀ ①)
 where
  σᵀ τᵀ : Ty
  σᵀ = simpᵀ σ
  τᵀ = simpᵀ τ

\end{code}

Simplcareⁱʳy terms

\begin{code}

simpᴹ : (σ : Ty) → ⟦ σ ⟧ʸ → ⟦ simpᵀ σ ⟧ʸ
backᴹ : (σ : Ty) → ⟦ simpᵀ σ ⟧ʸ → ⟦ σ ⟧ʸ
simpᴹ ① t = ⋆
simpᴹ Ⓝ t = t
simpᴹ ② t = t
simpᴹ (σ *) t = case c₀ c₁ (Ty-dec σᵀ ①)
 where
  σᵀ : Ty
  σᵀ = simpᵀ σ
  c₀ : σᵀ ≡ ① → ⟦ simpᵀ (σ *) ⟧ʸ
  c₀ e = transport ⟦_⟧ʸ (sym claim) ⋆
   where
    claim : simpᵀ (σ *) ≡ ①
    claim = Lemma[careⁱʳ]₀ e (Ty-dec σᵀ ①)
  c₁ : σᵀ ≢ ① → ⟦ simpᵀ (σ *) ⟧ʸ
  c₁ f = transport ⟦_⟧ʸ (sym claim) tᴹ
   where
    claim : simpᵀ (σ *) ≡ σᵀ *
    claim = Lemma[careⁱʳ]₁ f (Ty-dec σᵀ ①)
    tᴹ : ⟦ σᵀ * ⟧ʸ
    tᴹ = recᴸ ε (λ x ys → ys ₊ simpᴹ σ x) t
simpᴹ (σ ⊠ τ) (t₀ , t₁) = case c₀ c₁ (Ty-dec σᵀ ①)
 where
  σᵀ τᵀ : Ty
  σᵀ = simpᵀ σ
  τᵀ = simpᵀ τ
  c₀ : σᵀ ≡ ① → ⟦ simpᵀ (σ ⊠ τ) ⟧ʸ
  c₀ e = transport ⟦_⟧ʸ (sym claim) tᴹ
   where
    claim : simpᵀ (σ ⊠ τ) ≡ τᵀ
    claim = Lemma[careⁱʳ]₀ e (Ty-dec σᵀ ①)
    tᴹ : ⟦ τᵀ ⟧ʸ
    tᴹ = simpᴹ τ t₁
  c₁ : σᵀ ≢ ① → ⟦ simpᵀ (σ ⊠ τ) ⟧ʸ
  c₁ f = case d₀ d₁ (Ty-dec τᵀ ①)
   where
    claim₀ : simpᵀ (σ ⊠ τ) ≡ careⁱʳ σᵀ (σᵀ ⊠ τᵀ) (Ty-dec τᵀ ①)
    claim₀ = Lemma[careⁱʳ]₁ f (Ty-dec σᵀ ①)
    d₀ : τᵀ ≡ ① → ⟦ simpᵀ (σ ⊠ τ) ⟧ʸ
    d₀ e' = transport ⟦_⟧ʸ (sym claim₂) tᴹ
     where
      claim₁ : careⁱʳ σᵀ (σᵀ ⊠ τᵀ) (Ty-dec τᵀ ①) ≡ σᵀ
      claim₁ = Lemma[careⁱʳ]₀ e' (Ty-dec τᵀ ①)
      claim₂ : simpᵀ (σ ⊠ τ) ≡ σᵀ
      claim₂ = trans claim₀ claim₁
      tᴹ : ⟦ σᵀ ⟧ʸ
      tᴹ = simpᴹ σ t₀
    d₁ : τᵀ ≢ ① → ⟦ simpᵀ (σ ⊠ τ) ⟧ʸ
    d₁ f' = transport ⟦_⟧ʸ (sym claim₂) tᴹ
     where
      claim₁ : careⁱʳ σᵀ (σᵀ ⊠ τᵀ) (Ty-dec τᵀ ①) ≡ σᵀ ⊠ τᵀ
      claim₁ = Lemma[careⁱʳ]₁ f' (Ty-dec τᵀ ①)
      claim₂ : simpᵀ (σ ⊠ τ) ≡ σᵀ ⊠ τᵀ
      claim₂ = trans claim₀ claim₁
      tᴹ : ⟦ σᵀ ⊠ τᵀ ⟧ʸ
      tᴹ = simpᴹ σ t₀ , simpᴹ τ t₁
simpᴹ (σ ⇾ τ) t = case c₀ c₁ (Ty-dec σᵀ ①)
 where
  σᵀ τᵀ : Ty
  σᵀ = simpᵀ σ
  τᵀ = simpᵀ τ
  c₀ : σᵀ ≡ ① → ⟦ simpᵀ (σ ⇾ τ) ⟧ʸ
  c₀ e = transport ⟦_⟧ʸ (sym claim) tᴹ
   where
    claim : simpᵀ (σ ⇾ τ) ≡ τᵀ
    claim = Lemma[careⁱʳ]₀ e (Ty-dec σᵀ ①)
    tᴹ : ⟦ τᵀ ⟧ʸ
    tᴹ = simpᴹ τ (t (⟦𝒄⟧ σ))
  c₁ : σᵀ ≢ ① → ⟦ simpᵀ (σ ⇾ τ) ⟧ʸ
  c₁ f = case d₀ d₁ (Ty-dec τᵀ ①)
   where
    claim₀ : simpᵀ (σ ⇾ τ) ≡ careⁱʳ ① (σᵀ ⇾ τᵀ) (Ty-dec τᵀ ①)
    claim₀ = Lemma[careⁱʳ]₁ f (Ty-dec σᵀ ①)
    d₀ : τᵀ ≡ ① → ⟦ simpᵀ (σ ⇾ τ) ⟧ʸ
    d₀ e' = transport ⟦_⟧ʸ (sym claim₂) ⋆
     where
      claim₁ : careⁱʳ ① (σᵀ ⇾ τᵀ) (Ty-dec τᵀ ①) ≡ ①
      claim₁ = Lemma[careⁱʳ]₀ e' (Ty-dec τᵀ ①)
      claim₂ : simpᵀ (σ ⇾ τ) ≡ ①
      claim₂ = trans claim₀ claim₁
    d₁ : τᵀ ≢ ① → ⟦ simpᵀ (σ ⇾ τ) ⟧ʸ
    d₁ f' = transport ⟦_⟧ʸ (sym claim₂) tᴹ
     where
      claim₁ : careⁱʳ ① (σᵀ ⇾ τᵀ) (Ty-dec τᵀ ①) ≡ σᵀ ⇾ τᵀ
      claim₁ = Lemma[careⁱʳ]₁ f' (Ty-dec τᵀ ①)
      claim₂ : simpᵀ (σ ⇾ τ) ≡ σᵀ ⇾ τᵀ
      claim₂ = trans claim₀ claim₁
      tᴹ : ⟦ σᵀ ⇾ τᵀ ⟧ʸ
      tᴹ x = simpᴹ τ (t (backᴹ σ x))

backᴹ ① t = ⋆
backᴹ Ⓝ t = t
backᴹ ② t = t
backᴹ (σ *) t = case c₀ c₁ (Ty-dec σᵀ ①)
 where
  σᵀ : Ty
  σᵀ = simpᵀ σ
  c₀ : σᵀ ≡ ① → ⟦ σ * ⟧ʸ
  c₀ e = ε
  c₁ : σᵀ ≢ ① → ⟦ σ * ⟧ʸ
  c₁ f = recᴸ ε (λ x ys → ys ₊ backᴹ σ x) u
   where
    claim : simpᵀ (σ *) ≡ σᵀ *
    claim = Lemma[careⁱʳ]₁ f (Ty-dec σᵀ ①)
    u : ⟦ σᵀ * ⟧ʸ
    u = transport ⟦_⟧ʸ claim t
backᴹ (σ ⊠ τ) t = case c₀ c₁ (Ty-dec σᵀ ①)
 where
  σᵀ τᵀ : Ty
  σᵀ = simpᵀ σ
  τᵀ = simpᵀ τ
  c₀ : σᵀ ≡ ① → ⟦ σ ⊠ τ ⟧ʸ
  c₀ e = ⟦𝒄⟧ σ , backᴹ τ u
   where
    claim : simpᵀ (σ ⊠ τ) ≡ τᵀ
    claim = Lemma[careⁱʳ]₀ e (Ty-dec σᵀ ①)
    u : ⟦ τᵀ ⟧ʸ
    u = transport ⟦_⟧ʸ claim t
  c₁ : σᵀ ≢ ① → ⟦ σ ⊠ τ ⟧ʸ
  c₁ f = case d₀ d₁ (Ty-dec τᵀ ①)
   where
    claim₀ : simpᵀ (σ ⊠ τ) ≡ careⁱʳ σᵀ (σᵀ ⊠ τᵀ) (Ty-dec τᵀ ①)
    claim₀ = Lemma[careⁱʳ]₁ f (Ty-dec σᵀ ①)
    d₀ : τᵀ ≡ ① → ⟦ σ ⊠ τ ⟧ʸ
    d₀ e' = backᴹ σ u , ⟦𝒄⟧ τ
     where
      claim₁ : careⁱʳ σᵀ (σᵀ ⊠ τᵀ) (Ty-dec τᵀ ①) ≡ σᵀ
      claim₁ = Lemma[careⁱʳ]₀ e' (Ty-dec τᵀ ①)
      claim₂ : simpᵀ (σ ⊠ τ) ≡ σᵀ
      claim₂ = trans claim₀ claim₁
      u : ⟦ σᵀ ⟧ʸ
      u = transport ⟦_⟧ʸ claim₂ t
    d₁ : τᵀ ≢ ① → ⟦ σ ⊠ τ ⟧ʸ
    d₁ f' = backᴹ σ (pr₁ u) , backᴹ τ (pr₂ u)
     where
      claim₁ : careⁱʳ σᵀ (σᵀ ⊠ τᵀ) (Ty-dec τᵀ ①) ≡ σᵀ ⊠ τᵀ
      claim₁ = Lemma[careⁱʳ]₁ f' (Ty-dec τᵀ ①)
      claim₂ : simpᵀ (σ ⊠ τ) ≡ σᵀ ⊠ τᵀ
      claim₂ = trans claim₀ claim₁
      u : ⟦ σᵀ ⊠ τᵀ ⟧ʸ
      u = transport ⟦_⟧ʸ claim₂ t
backᴹ (σ ⇾ τ) t = case c₀ c₁ (Ty-dec σᵀ ①)
 where
  σᵀ τᵀ : Ty
  σᵀ = simpᵀ σ
  τᵀ = simpᵀ τ
  c₀ : σᵀ ≡ ① → ⟦ σ ⇾ τ ⟧ʸ
  c₀ e = λ _ → backᴹ τ u
   where
    claim : simpᵀ (σ ⇾ τ) ≡ τᵀ
    claim = Lemma[careⁱʳ]₀ e (Ty-dec σᵀ ①)
    u : ⟦ τᵀ ⟧ʸ
    u = transport ⟦_⟧ʸ claim t
  c₁ : σᵀ ≢ ① → ⟦ σ ⇾ τ ⟧ʸ
  c₁ f = case d₀ d₁ (Ty-dec τᵀ ①)
   where
    claim₀ : simpᵀ (σ ⇾ τ) ≡ careⁱʳ ① (σᵀ ⇾ τᵀ) (Ty-dec τᵀ ①)
    claim₀ = Lemma[careⁱʳ]₁ f (Ty-dec σᵀ ①)
    d₀ : τᵀ ≡ ① → ⟦ σ ⇾ τ ⟧ʸ
    d₀ _ = ⟦𝒄⟧ (σ ⇾ τ)
    d₁ : τᵀ ≢ ① → ⟦ σ ⇾ τ ⟧ʸ
    d₁ f' = λ x → backᴹ τ (u (simpᴹ σ x))
     where
      claim₁ : careⁱʳ ① (σᵀ ⇾ τᵀ) (Ty-dec τᵀ ①) ≡ σᵀ ⇾ τᵀ
      claim₁ = Lemma[careⁱʳ]₁ f' (Ty-dec τᵀ ①)
      claim₂ : simpᵀ (σ ⇾ τ) ≡ σᵀ ⇾ τᵀ
      claim₂ = trans claim₀ claim₁
      u : ⟦ σᵀ ⇾ τᵀ ⟧ʸ
      u = transport ⟦_⟧ʸ claim₂ t

\end{code}