1
------------------------------------------------------------------------
2
------------------------------------------------------------------------
4
{-# OPTIONS --universe-polymorphism #-}
10
module Data.Context {u e} (Uni : Universe u e) where
12
open Universe.Universe Uni
14
open import Data.Product as Prod
19
------------------------------------------------------------------------
27
data Ctxt : Set (u ⊔ e) where
29
_▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt
31
-- Semantic types: maps from environments to universe codes.
33
Type : Ctxt → Set (u ⊔ e)
36
-- Interpretation of contexts: environments.
40
Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (σ γ)
43
Term-like : (ℓ : Level) → Set _
44
Term-like ℓ = (Γ : Ctxt) → Type Γ → Set ℓ
48
Value Γ σ = (γ : Env Γ) → El (σ γ)
50
------------------------------------------------------------------------
55
_⇨_ : Ctxt → Ctxt → Set _
61
_⇨₁_ : ∀ {Γ} → Type Γ → Type Γ → Set _
62
σ ⇨₁ τ = ∀ {γ} → El (τ γ) → El (σ γ)
68
_/_ : ∀ {Γ Δ} → Type Γ → Γ ⇨ Δ → Type Δ
74
_/v_ : ∀ {Γ Δ σ} → Value Γ σ → (ρ : Γ ⇨ Δ) → Value Δ (σ / ρ)
78
wk : ∀ {Γ σ} → Γ ⇨ Γ ▻ σ
84
_►_ : ∀ {Γ Δ σ} (ρ : Γ ⇨ Δ) → Value Δ (σ / ρ) → Γ ▻ σ ⇨ Δ
88
sub : ∀ {Γ σ} → Value Γ σ → Γ ▻ σ ⇨ Γ
94
_↑_ : ∀ {Γ Δ σ τ} (ρ : Γ ⇨ Δ) → σ / ρ ⇨₁ τ → Γ ▻ σ ⇨ Δ ▻ τ
100
_↑ : ∀ {Γ Δ σ} (ρ : Γ ⇨ Δ) → Γ ▻ σ ⇨ Δ ▻ σ / ρ
103
------------------------------------------------------------------------
108
data _∋_ : Term-like (u ⊔ e) where
109
zero : ∀ {Γ σ} → Γ ▻ σ ∋ σ / wk
110
suc : ∀ {Γ σ τ} (x : Γ ∋ σ) → Γ ▻ τ ∋ σ / wk
113
lookup : ∀ {Γ σ} → Γ ∋ σ → Value Γ σ
114
lookup zero (γ , v) = v
115
lookup (suc x) (γ , v) = lookup x γ
120
_/∋_ : ∀ {Γ Δ σ} → Γ ∋ σ → (ρ : Γ ⇨ Δ) → Value Δ (σ / ρ)
121
x /∋ ρ = lookup x /v ρ
123
------------------------------------------------------------------------
127
-- Context extensions.
131
data Ctxt⁺ (Γ : Ctxt) : Set (u ⊔ e) where
133
_▻_ : (Γ⁺ : Ctxt⁺ Γ) (σ : Type (Γ ++ Γ⁺)) → Ctxt⁺ Γ
135
-- Appends a context extension to a context.
139
_++_ : (Γ : Ctxt) → Ctxt⁺ Γ → Ctxt
141
Γ ++ (Γ⁺ ▻ σ) = (Γ ++ Γ⁺) ▻ σ
145
-- Application of substitutions to context extensions.
149
_/⁺_ : ∀ {Γ Δ} → Ctxt⁺ Γ → Γ ⇨ Δ → Ctxt⁺ Δ
151
(Γ⁺ ▻ σ) /⁺ ρ = Γ⁺ /⁺ ρ ▻ σ / ρ ↑⋆ Γ⁺
153
-- N-ary lifting of substitutions.
157
_↑⋆_ : ∀ {Γ Δ} (ρ : Γ ⇨ Δ) → ∀ Γ⁺ → Γ ++ Γ⁺ ⇨ Δ ++ Γ⁺ /⁺ ρ
159
ρ ↑⋆ (Γ⁺ ▻ σ) = (ρ ↑⋆ Γ⁺) ↑
added
removed
src/Data/Context.agda
