WIP: concrete families

1 files changed, 0 insertions, 167 deletions

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