1
------------------------------------------------------------------------
2
-- Contexts, variables, substitutions, etc.
3
------------------------------------------------------------------------
5
{-# OPTIONS --universe-polymorphism #-}
7
-- Based on Conor McBride's "Outrageous but Meaningful Coincidences:
8
-- Dependent type-safe syntax and evaluation".
10
-- The contexts and variables are parametrised by a universe.
14
module Data.Context {u e} (Uni : Universe u e) where
16
open Universe.Universe Uni
18
open import Data.Product as Prod
23
------------------------------------------------------------------------
24
-- Contexts and "types"
32
data Ctxt : Set (u ⊔ e) where
34
_▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt
36
-- Semantic types: maps from environments to universe codes.
38
Type : Ctxt → Set (u ⊔ e)
41
-- Interpretation of contexts: environments.
45
Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (σ γ)
47
-- Type signature for variables, terms, etc.
49
Term-like : (ℓ : Level) → Set _
50
Term-like ℓ = (Γ : Ctxt) → Type Γ → Set ℓ
52
-- Semantic values: maps from environments to universe values.
55
Value Γ σ = (γ : Env Γ) → El (σ γ)
57
------------------------------------------------------------------------
60
-- Semantic substitutions or context morphisms: maps from environments
65
_⇨_ : Ctxt → Ctxt → Set _
68
-- Maps between types.
72
_⇨₁_ : ∀ {Γ} → Type Γ → Type Γ → Set _
73
σ ⇨₁ τ = ∀ {γ} → El (τ γ) → El (σ γ)
75
-- Application of substitutions to types.
77
-- Note that this operation is composition of functions. I have chosen
78
-- not to give a separate name to the identity substitution, which is
79
-- simply the identity function, nor to reverse composition of
80
-- substitutions, which is composition of functions.
84
_/_ : ∀ {Γ Δ} → Type Γ → Γ ⇨ Δ → Type Δ
87
-- Application of substitutions to values.
91
_/v_ : ∀ {Γ Δ σ} → Value Γ σ → (ρ : Γ ⇨ Δ) → Value Δ (σ / ρ)
96
wk : ∀ {Γ σ} → Γ ⇨ Γ ▻ σ
99
-- Extends a substitution with another value.
103
_►_ : ∀ {Γ Δ σ} (ρ : Γ ⇨ Δ) → Value Δ (σ / ρ) → Γ ▻ σ ⇨ Δ
106
-- A substitution which only replaces the first "variable".
108
sub : ∀ {Γ σ} → Value Γ σ → Γ ▻ σ ⇨ Γ
111
-- One can construct a substitution between two non-empty contexts by
112
-- supplying two functions, one which handles the last element and one
113
-- which handles the rest.
117
_↑_ : ∀ {Γ Δ σ τ} (ρ : Γ ⇨ Δ) → σ / ρ ⇨₁ τ → Γ ▻ σ ⇨ Δ ▻ τ
124
_↑ : ∀ {Γ Δ σ} (ρ : Γ ⇨ Δ) → Γ ▻ σ ⇨ Δ ▻ σ / ρ
127
------------------------------------------------------------------------
130
-- Variables (de Bruijn indices).
134
data _∋_ : Term-like (u ⊔ e) where
135
zero : ∀ {Γ σ} → Γ ▻ σ ∋ σ / wk
136
suc : ∀ {Γ σ τ} (x : Γ ∋ σ) → Γ ▻ τ ∋ σ / wk
138
-- Interpretation of variables: a lookup function.
140
lookup : ∀ {Γ σ} → Γ ∋ σ → Value Γ σ
141
lookup zero (γ , v) = v
142
lookup (suc x) (γ , v) = lookup x γ
144
-- Application of substitutions to variables.
148
_/∋_ : ∀ {Γ Δ σ} → Γ ∋ σ → (ρ : Γ ⇨ Δ) → Value Δ (σ / ρ)
149
x /∋ ρ = lookup x /v ρ
151
------------------------------------------------------------------------
152
-- Context extensions
156
-- Context extensions.
160
data Ctxt⁺ (Γ : Ctxt) : Set (u ⊔ e) where
162
_▻_ : (Γ⁺ : Ctxt⁺ Γ) (σ : Type (Γ ++ Γ⁺)) → Ctxt⁺ Γ
164
-- Appends a context extension to a context.
168
_++_ : (Γ : Ctxt) → Ctxt⁺ Γ → Ctxt
170
Γ ++ (Γ⁺ ▻ σ) = (Γ ++ Γ⁺) ▻ σ
174
-- Application of substitutions to context extensions.
178
_/⁺_ : ∀ {Γ Δ} → Ctxt⁺ Γ → Γ ⇨ Δ → Ctxt⁺ Δ
180
(Γ⁺ ▻ σ) /⁺ ρ = Γ⁺ /⁺ ρ ▻ σ / ρ ↑⋆ Γ⁺
182
-- N-ary lifting of substitutions.
186
_↑⋆_ : ∀ {Γ Δ} (ρ : Γ ⇨ Δ) → ∀ Γ⁺ → Γ ++ Γ⁺ ⇨ Δ ++ Γ⁺ /⁺ ρ
188
ρ ↑⋆ (Γ⁺ ▻ σ) = (ρ ↑⋆ Γ⁺) ↑
added
removed
src/Data/Context.agda
