blob: 94fee5cc4d82f7e8172e90f923435c5fe72e26c1 (
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
|
{-# 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
|
