From bf5fedb51726f62aa8f46505ebee87912ef10ce3 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 28 Dec 2023 12:41:57 +0000
Subject: Define syntax and equivalence.

---
 src/CBPV/Family.agda | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 src/CBPV/Family.agda

(limited to 'src/CBPV/Family.agda')

diff --git a/src/CBPV/Family.agda b/src/CBPV/Family.agda
new file mode 100644
index 0000000..94fee5c
--- /dev/null
+++ b/src/CBPV/Family.agda
@@ -0,0 +1,52 @@
+{-# OPTIONS --safe #-}
+
+module CBPV.Family where
+
+open import Data.List using (List; _++_)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.Product using (_,_) renaming (_×_ to _×′_)
+open import Level using (Level; suc; _⊔_)
+
+open import CBPV.Type
+
+private
+  variable
+    ℓ ℓ′ : Level
+
+Context : Set
+Context = List ValType
+
+ValFamily : (ℓ : Level) → Set (suc ℓ)
+ValFamily ℓ = Context → ValType → Set ℓ
+
+CompFamily : (ℓ : Level) → Set (suc ℓ)
+CompFamily ℓ = Context → CompType → Set ℓ
+
+δᵛ : Context → ValFamily ℓ → ValFamily ℓ
+δᵛ Δ V Γ A = V (Γ ++ Δ) A
+
+δᶜ : Context → CompFamily ℓ → CompFamily ℓ
+δᶜ Δ C Γ B = C (Γ ++ Δ) B
+
+infix 0 _⇒ᵛ_ _⇒ᶜ_ _~[_]↝ᵛ_ _~[_]↝ᶜ_
+
+_⇒ᵛ_ : ValFamily ℓ → ValFamily ℓ′ → Set (ℓ ⊔ ℓ′)
+V ⇒ᵛ V′ = ∀ {Γ A} → V Γ A → V′ Γ A
+
+_⇒ᶜ_ : CompFamily ℓ → CompFamily ℓ′ → Set (ℓ ⊔ ℓ′)
+C ⇒ᶜ C′ = ∀ {Γ B} → C Γ B → C′ Γ B
+
+_~[_]↝ᵛ_ : List ValType → ValFamily ℓ → Context → Set ℓ
+As ~[ V ]↝ᵛ Γ = ∀ {A} → A ∈ As → V Γ A
+
+_~[_]↝ᶜ_ : List CompType → CompFamily ℓ → Context → Set ℓ
+Bs ~[ C ]↝ᶜ Γ = ∀ {B} → B ∈ Bs → C Γ B
+
+I : ValFamily _
+I Γ A = A ∈ Γ
+
+⌞_⌟ᵛ : List (Context ×′ ValType) → ValFamily _
+⌞ Vs ⌟ᵛ Γ A = (Γ , A) ∈ Vs
+
+⌞_⌟ᶜ : List (Context ×′ CompType) → CompFamily _
+⌞ Cs ⌟ᶜ Γ B = (Γ , B) ∈ Cs
-- 
cgit v1.2.3