Define syntax and equivalence.

1 files changed, 167 insertions, 0 deletions

diff --git a/src/CBPV/Axiom.agda b/src/CBPV/Axiom.agda
new file mode 100644
index 0000000..503b61d
--- /dev/null
+++ b/src/CBPV/Axiom.agda
@@ -0,0 +1,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₀ ⟩