blob: 503b61d3e163dc1090c36b6bc8e74256124b7172 (
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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
{-# OPTIONS --safe #-}
module CBPV.Axiom where
open import Data.List using (List; []; _∷_; [_]; map)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Membership.Propositional.Properties using (∈-map⁺)
open import Data.List.Relation.Unary.Any using () renaming (here to ↓_; there to ↑_)
open import Data.List.Relation.Unary.All using (_∷_; tabulate) renaming ([] to •⟩)
open import Data.Product using () renaming (_,_ to _⊩_)
open import Level using (0ℓ)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (refl)
open import CBPV.Family
open import CBPV.Term
open import CBPV.Type
pattern _∶_ a b = a ∷ b
pattern x₀ = var (↓ refl)
pattern x₁ = var (↑ ↓ refl)
pattern x₂ = var (↑ ↑ ↓ refl)
pattern x₃ = var (↑ ↑ ↑ ↓ refl)
pattern x₄ = var (↑ ↑ ↑ ↑ ↓ refl)
pattern x₅ = var (↑ ↑ ↑ ↑ ↑ ↓ refl)
pattern 𝔞⟨_ ε = mvar (↓ refl) ε
pattern 𝔟⟨_ ε = mvar (↑ ↓ refl) ε
pattern 𝔠⟨_ ε = mvar (↑ ↑ ↓ refl) ε
pattern 𝔡⟨_ ε = mvar (↑ ↑ ↑ ↓ refl) ε
pattern ◌ᵃ⟨_ ε = 𝔞⟨ ε
pattern ◌ᵇ⟨_ ε = 𝔟⟨ ε
pattern ◌ᶜ⟨_ ε = 𝔠⟨ ε
pattern ◌ᵈ⟨_ ε = 𝔡⟨ ε
infix 19 _⟩
infix 18 𝔞⟨_ 𝔟⟨_ 𝔠⟨_ 𝔡⟨_ ◌ᵃ⟨_ ◌ᵇ⟨_ ◌ᶜ⟨_ ◌ᵈ⟨_
infixr 18 ⟨_ _∶_
pattern 𝔞 = 𝔞⟨ •⟩
pattern 𝔟 = 𝔟⟨ •⟩
pattern 𝔠 = 𝔠⟨ •⟩
pattern 𝔡 = 𝔡⟨ •⟩
pattern ◌ᵃ = ◌ᵃ⟨ •⟩
pattern ◌ᵇ = ◌ᵇ⟨ •⟩
pattern ◌ᶜ = ◌ᶜ⟨ •⟩
pattern ◌ᵈ = ◌ᵈ⟨ •⟩
pattern _⟩ a = a ∶ •⟩
pattern ⟨_ as = as
pattern []⊩_ C = [] ⊩ C
pattern [_]⊩_ A C = (A ∷ []) ⊩ C
pattern [_•_]⊩_ A A′ C = (A ∷ A′ ∷ []) ⊩ C
private
variable
A A′ A′′ : ValType
B B′ : CompType
infix 0 _⨾_▹⊢ᵛ_≋_ _⨾_▹⊢ᶜ_≋_
data _⨾_▹⊢ᵛ_≋_ : ∀ Vs Cs {A} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᵛ A) 0ℓ
data _⨾_▹⊢ᶜ_≋_ : ∀ Vs Cs {B} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᶜ B) 0ℓ
data _⨾_▹⊢ᵛ_≋_ where
-- Structural
have : ([]⊩ A) ∷ ([ A ]⊩ A′) ∷ [] ⨾ [] ▹⊢ᵛ have 𝔞 be 𝔟⟨ x₀ ⟩ ≋ 𝔟⟨ 𝔞 ⟩
-- Beta
𝟙β : [ []⊩ A ] ⨾ [] ▹⊢ᵛ unpoint tt 𝔞 ≋ 𝔞
+β₁ :
([]⊩ A) ∷ ([ A ]⊩ A′′) ∷ ([ A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
untag (inl 𝔞) (𝔟⟨ x₀ ⟩) (𝔠⟨ x₀ ⟩)
≋
𝔟⟨ 𝔞 ⟩
+β₂ :
([]⊩ A′) ∷ ([ A ]⊩ A′′) ∷ ([ A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
untag (inr 𝔞) (𝔟⟨ x₀ ⟩) (𝔠⟨ x₀ ⟩)
≋
𝔠⟨ 𝔞 ⟩
×β :
([]⊩ A) ∷ ([]⊩ A′) ∷ ([ A • A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
unpair (𝔞 , 𝔟) (𝔠⟨ x₀ ∶ x₁ ⟩)
≋
𝔠⟨ 𝔞 ∶ 𝔟 ⟩
⟶β : ([]⊩ A) ∷ ([ A ]⊩ A′) ∷ [] ⨾ [] ▹⊢ᵛ 𝔞 ‵ ƛ 𝔟⟨ x₀ ⟩ ≋ 𝔟⟨ 𝔞 ⟩
-- Eta
Uη : [ []⊩ (U B) ] ⨾ [] ▹⊢ᵛ thunk (force 𝔞) ≋ 𝔞
𝟘η : ([]⊩ 𝟘) ∷ ([ 𝟘 ]⊩ A) ∷ [] ⨾ [] ▹⊢ᵛ absurd 𝔞 ≋ 𝔟⟨ 𝔞 ⟩
𝟙η : ([]⊩ 𝟙) ∷ ([ 𝟙 ]⊩ A) ∷ [] ⨾ [] ▹⊢ᵛ unpoint 𝔞 (𝔟⟨ tt ⟩) ≋ 𝔟⟨ 𝔞 ⟩
+η :
([]⊩ (A + A′)) ∷ ([ A + A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
untag 𝔞 (𝔟⟨ inl x₀ ⟩) (𝔟⟨ inr x₀ ⟩)
≋
𝔟⟨ 𝔞 ⟩
×η :
([]⊩ (A × A′)) ∷ ([ A × A′ ]⊩ A′′) ∷ [] ⨾ [] ▹⊢ᵛ
unpair 𝔞 (𝔟⟨ (x₀ , x₁) ⟩)
≋
𝔟⟨ 𝔞 ⟩
⟶η : [ []⊩ (A ⟶ A′) ] ⨾ [] ▹⊢ᵛ ƛ (x₀ ‵ 𝔞) ≋ 𝔞
data _⨾_▹⊢ᶜ_≋_ where
-- Structural
have : [ []⊩ A ] ⨾ [ [ A ]⊩ B ] ▹⊢ᶜ have 𝔞 be 𝔞⟨ x₀ ⟩ ≋ 𝔞⟨ 𝔞 ⟩
-- Beta
Uβ : [] ⨾ [ []⊩ B ] ▹⊢ᶜ force (thunk 𝔞) ≋ 𝔞
𝟙β : [] ⨾ [ []⊩ B ] ▹⊢ᶜ unpoint tt 𝔞 ≋ 𝔞
+β₁ :
[ []⊩ A ] ⨾ ([ A ]⊩ B) ∷ ([ A′ ]⊩ B) ∷ [] ▹⊢ᶜ
untag (inl 𝔞) (𝔞⟨ x₀ ⟩) (𝔟⟨ x₀ ⟩)
≋
𝔞⟨ 𝔞 ⟩
+β₂ :
[ []⊩ A′ ] ⨾ ([ A ]⊩ B) ∷ ([ A′ ]⊩ B) ∷ [] ▹⊢ᶜ
untag (inr 𝔞) (𝔞⟨ x₀ ⟩) (𝔟⟨ x₀ ⟩)
≋
𝔟⟨ 𝔞 ⟩
×β :
([]⊩ A) ∷ ([]⊩ A′) ∷ [] ⨾ [ [ A • A′ ]⊩ B ] ▹⊢ᶜ
unpair (𝔞 , 𝔟) (𝔞⟨ x₀ ∶ x₁ ⟩)
≋
𝔞⟨ 𝔞 ∶ 𝔟 ⟩
Fβ : [ []⊩ A ] ⨾ [ [ A ]⊩ B ] ▹⊢ᶜ return 𝔞 to 𝔞⟨ x₀ ⟩ ≋ 𝔞⟨ 𝔞 ⟩
×ᶜβ₁ : [] ⨾ ([]⊩ B) ∷ ([]⊩ B′) ∷ [] ▹⊢ᶜ π₁ (𝔞 , 𝔟) ≋ 𝔞
×ᶜβ₂ : [] ⨾ ([]⊩ B) ∷ ([]⊩ B′) ∷ [] ▹⊢ᶜ π₂ (𝔞 , 𝔟) ≋ 𝔟
⟶β : [ []⊩ A ] ⨾ [ [ A ]⊩ B ] ▹⊢ᶜ 𝔞 ‵ ƛ 𝔞⟨ x₀ ⟩ ≋ 𝔞⟨ 𝔞 ⟩
-- Eta
𝟘η : [ []⊩ 𝟘 ] ⨾ [ [ 𝟘 ]⊩ B ] ▹⊢ᶜ absurd 𝔞 ≋ 𝔞⟨ 𝔞 ⟩
𝟙η : [ []⊩ 𝟙 ] ⨾ [ [ 𝟙 ]⊩ B ] ▹⊢ᶜ unpoint 𝔞 (𝔞⟨ tt ⟩) ≋ 𝔞⟨ 𝔞 ⟩
+η :
[ []⊩ (A + A′) ] ⨾ [ [ A + A′ ]⊩ B ] ▹⊢ᶜ
untag 𝔞 (𝔞⟨ inl x₀ ⟩) (𝔞⟨ inr x₀ ⟩)
≋
𝔞⟨ 𝔞 ⟩
×η :
[ []⊩ (A × A′) ] ⨾ [ [ A × A′ ]⊩ B ] ▹⊢ᶜ
unpair 𝔞 (𝔞⟨ (x₀ , x₁) ⟩)
≋
𝔞⟨ 𝔞 ⟩
Fη : [] ⨾ [ []⊩ (F A) ] ▹⊢ᶜ 𝔞 to return x₀ ≋ 𝔞
𝟙ᶜη : [] ⨾ [ []⊩ 𝟙 ] ▹⊢ᶜ tt ≋ 𝔞
×ᶜη : [] ⨾ [ []⊩ (B × B′) ] ▹⊢ᶜ π₁ 𝔞 , π₂ 𝔞 ≋ 𝔞
⟶η : [] ⨾ [ []⊩ (A ⟶ B) ] ▹⊢ᶜ ƛ (x₀ ‵ 𝔞) ≋ 𝔞
-- Sequencing
to-to :
[] ⨾ ([]⊩ (F A)) ∷ ([ A ]⊩ (F A′)) ∷ ([ A′ ]⊩ B) ∷ [] ▹⊢ᶜ
(𝔞 to 𝔟⟨ x₀ ⟩) to 𝔠⟨ x₀ ⟩
≋
𝔞 to (𝔟⟨ x₀ ⟩ to 𝔠⟨ x₀ ⟩)
to-π₁ :
[] ⨾ ([]⊩ (F A)) ∷ ([ A ]⊩ (B × B′)) ∷ [] ▹⊢ᶜ
π₁ (𝔞 to 𝔟⟨ x₀ ⟩)
≋
𝔞 to π₁ (𝔟⟨ x₀ ⟩)
to-π₂ :
[] ⨾ ([]⊩ (F A)) ∷ ([ A ]⊩ (B × B′)) ∷ [] ▹⊢ᶜ
π₂ (𝔞 to 𝔟⟨ x₀ ⟩)
≋
𝔞 to π₂ (𝔟⟨ x₀ ⟩)
to-‵ :
[ []⊩ A ] ⨾ ([]⊩ (F A′)) ∷ ([ A′ ]⊩ (A ⟶ B)) ∷ [] ▹⊢ᶜ
𝔞 ‵ (𝔞 to 𝔟⟨ x₀ ⟩)
≋
𝔞 to 𝔞 ‵ 𝔟⟨ x₀ ⟩
|
