blob: e5d27e2cc8f9b7e3c3ec3990b64c04c0f2a48933 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
{-# 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′)))))
|
