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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary using (Setoid; Rel)
module Cfe.Context.Base
{c ℓ} (over : Setoid c ℓ)
where
open import Cfe.Fin
open import Cfe.Type over using (Type) renaming (_≈_ to _≈ᵗ_; _≤_ to _≤ᵗ_)
open import Data.Fin hiding (_+_) renaming (zero to #0; suc to 1+_; _≤_ to _≤ᶠ_)
open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-inject₁)
open import Data.Nat using (ℕ; suc; _∸_; _+_)
open import Data.Nat.Properties using (+-suc)
open import Data.Product using (_×_)
open import Data.Vec using (Vec; []; insert)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise)
open import Level renaming (suc to lsuc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; module ≡-Reasoning)
open import Relation.Nullary.Decidable using (True)
private
variable
n : ℕ
------------------------------------------------------------------------
-- Definitions
infix 4 _⊐_
record Context n : Set (c ⊔ lsuc ℓ) where
constructor _⊐_
field
Γ,Δ : Vec (Type ℓ ℓ) n
guard : Fin (suc n)
open Context public
∙,∙ : Context 0
∙,∙ = [] ⊐ #0
------------------------------------------------------------------------
-- Insertions
wkn₂ : ∀ (ctx : Context n) → Fin< (1+ guard ctx) → Type ℓ ℓ → Context (suc n)
wkn₂ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (inject<! i) τ ⊐ 1+ g
wkn₁ : ∀ (ctx : Context n) → Fin> (guard ctx) → Type ℓ ℓ → Context (suc n)
wkn₁ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (raise> i) τ ⊐ inject₁ g
------------------------------------------------------------------------
-- Modifications
shift : ∀ (ctx : Context n) → Fin< (1+ guard ctx) → Context n
shift (Γ,Δ ⊐ _) i = Γ,Δ ⊐ inject<! i
------------------------------------------------------------------------
-- Relations
-- infix 4 _≈_ _≤_
_≈_ : Rel (Context n) _
(Γ,Δ₁ ⊐ g₁) ≈ (Γ,Δ₂ ⊐ g₂) = g₁ ≡ g₂ × Pointwise _≈ᵗ_ Γ,Δ₁ Γ,Δ₂
_≤_ : Rel (Context n) _
(Γ,Δ₁ ⊐ g₁) ≤ (Γ,Δ₂ ⊐ g₂) = g₂ ≤ᶠ g₁ × Pointwise _≤ᵗ_ Γ,Δ₁ Γ,Δ₂
|
