{-# OPTIONS --safe #-}

module Problem21 (Atom : Set) where

open import Data.List
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.Empty
open import Data.Nat
open import Data.Fin
open import Data.Fin.Patterns
open import Data.Product

data L : Set where
    ⟨_⟩ : Atom → L
    ⟨_⟩ᶜ : Atom → L
    _⊗_ : L → L → L
    _⅋_ : L → L → L
    ⊥' : L
    𝟙  : L

variable A B C : L
variable Δ Γ : List L
variable α β η : Atom

_ᶜ : L → L
⟨ A ⟩   ᶜ = ⟨ A ⟩ᶜ
⟨ A ⟩ᶜ  ᶜ = ⟨ A ⟩
(A ⊗ B) ᶜ = (A ᶜ) ⅋ (B ᶜ)
(A ⅋ B) ᶜ = (A ᶜ) ⊗ (B ᶜ)
𝟙       ᶜ = ⊥'
⊥'      ᶜ = 𝟙

_⊸_ : L → L → L
A ⊸ B = (A ᶜ) ⅋ B

infixl 2 ⊢_
data ⊢_ : List L → Set where
    one      : ⊢ [ 𝟙 ]
    identity : ⊢ ⟨ α ⟩ ∷ ⟨ α ⟩ᶜ ∷ []
    exch     :  (n : Fin (length Δ))
             → ⊢ lookup Δ n ∷ (Δ ─ n)
             → ⊢ Δ
    times    : (n : ℕ)
             → ⊢ A ∷ take n Δ
             → ⊢ B ∷ drop n Δ
             → ⊢ A ⊗ B ∷ Δ
    par      : ⊢ A ∷ B ∷ Δ
             → ⊢ A ⅋ B ∷ Δ
    bottom   : ⊢ Δ
             → ⊢ ⊥' ∷ Δ

    cut      : ⊢ A ∷ Δ
             → ⊢ A ᶜ ∷ Γ
             → ⊢ Δ ++ Γ

id : {A : L} → ⊢ A ∷ A ᶜ ∷ []
id {⟨ x ⟩} = identity
id {⟨ x ⟩ᶜ} = exch 1F identity
id {A ⊗ B} = exch 1F (par (exch 2F (times 1 (id {A}) (id {B}))))
id {A ⅋ B} = par (exch 2F (times 1 (exch 1F (id {A})) (exch 1F (id {B}))))
id {⊥'} = bottom one
id {𝟙} = exch 1F (bottom one)

id′ : {A : L} → ⊢ A ᶜ ∷ A ∷ []
id′ = exch 1F id

_≈_ : L → L → Set
A ≈ B = (⊢ [ A ] → ⊢ [ B ]) × (⊢ [ B ] → ⊢ [ A ])

lem₁ : ((A ⊗ B) ⊸ C) ≈ (A ⊸ (B ⊸ C))
lem₁ .proj₁ prf = cut prf (exch 1F (par (exch 1F (par (exch 2F (exch 3F (times 2 (times 1 id′ id′) id′)))))))
lem₁ .proj₂ prf = cut prf (exch 1F (par (par (exch 3F (times 1 id′ (times 1 id′ id′))))))

lem₂ : (A ⊸ (B ⅋ C)) ≈ ((A ⊸ B) ⅋ C)
lem₂ .proj₁ prf = cut prf (exch 1F (par (par (exch 3F (times 1 id′ (times 1 id′ id′))))))
lem₂ .proj₂ prf = cut prf (exch 1F (par (exch 1F (par (exch 2F (exch 3F (times 2 (times 1 id′ id′) id′)))))))

lem₃ : (A ⊸ B) ≈ ((B ᶜ) ⊸ (A ᶜ))
lem₃ .proj₁ prf = cut prf (exch 1F (par (exch 1F (exch 2F (times 1 id′ id)))))
lem₃ .proj₂ prf = cut prf (exch 1F (par (exch 1F (exch 2F (times 1 (exch 1F (cut id′ id)) id′)))))