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
67
68
69
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary using (Setoid)
module Cfe.Judgement.Base
{c ℓ} (over : Setoid c ℓ)
where
open import Cfe.Expression over renaming (shift to shiftₑ)
open import Cfe.Type over renaming (_∙_ to _∙ₜ_; _∨_ to _∨ₜ_)
open import Cfe.Type.Construct.Lift over
open import Data.Fin as F
open import Data.Fin.Properties
open import Data.Nat as ℕ hiding (_⊔_)
open import Data.Nat.Properties
open import Data.Vec hiding (_⊛_) renaming (lookup to lookup′)
open import Level hiding (Lift) renaming (suc to lsuc)
open import Relation.Binary.PropositionalEquality
record Context n : Set (c ⊔ lsuc ℓ) where
field
m : ℕ
m≤n : m ℕ.≤ n
Γ : Vec (Type ℓ ℓ) (n ∸ m)
Δ : Vec (Type ℓ ℓ) m
-- Fin n → Fin n∸m
lookup : (i : Fin n) → toℕ i ≥ m → Type ℓ ℓ
lookup i i≥m = lookup′ Γ (reduce≥
(F.cast (begin-equality
n ≡˘⟨ m+n∸m≡n m n ⟩
m ℕ.+ n ∸ m ≡⟨ +-∸-assoc m m≤n ⟩
m ℕ.+ (n ∸ m) ∎) i)
(begin
m ≤⟨ i≥m ⟩
toℕ i ≡˘⟨ toℕ-cast _ i ⟩
toℕ (F.cast _ i) ∎))
where
open ≤-Reasoning
cons : ∀ {n} → Type ℓ ℓ → Context n → Context (suc n)
cons {n} τ Γ,Δ = record
{ m≤n = s≤s m≤n
; Γ = Γ
; Δ = τ ∷ Δ
}
where
open Context Γ,Δ
shift : ∀ {n} → Context n → Context n
shift {n} Γ,Δ = record
{ m≤n = z≤n
; Γ = subst (Vec (Type ℓ ℓ)) (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (Δ ++ Γ)
; Δ = []
}
where
open Context Γ,Δ
infix 2 _⊢_∶_
data _⊢_∶_ : {n : ℕ} → Context n → Expression n → Type ℓ ℓ → Set (c ⊔ lsuc ℓ) where
Eps : ∀ {n} {Γ,Δ : Context n} → Γ,Δ ⊢ ε ∶ Lift ℓ ℓ τε
Char : ∀ {n} {Γ,Δ : Context n} c → Γ,Δ ⊢ Char c ∶ Lift ℓ ℓ τ[ c ]
Bot : ∀ {n} {Γ,Δ : Context n} → Γ,Δ ⊢ ⊥ ∶ Lift ℓ ℓ τ⊥
Var : ∀ {n} {Γ,Δ : Context n} {i : Fin n} (i≥m : toℕ i ℕ.≥ Context.m Γ,Δ) → Γ,Δ ⊢ Var i ∶ Context.lookup Γ,Δ i i≥m
Fix : ∀ {n} {Γ,Δ : Context n} {e τ} → cons τ Γ,Δ ⊢ e ∶ τ → Γ,Δ ⊢ μ e ∶ τ
Cat : ∀ {n} {Γ,Δ : Context n} {e₁ e₂ τ₁ τ₂} → Γ,Δ ⊢ e₁ ∶ τ₁ → shift Γ,Δ ⊢ e₂ ∶ τ₂ → (τ₁⊛τ₂ : τ₁ ⊛ τ₂) → Γ,Δ ⊢ e₁ ∙ e₂ ∶ τ₁ ∙ₜ τ₂
Vee : ∀ {n} {Γ,Δ : Context n} {e₁ e₂ τ₁ τ₂} → Γ,Δ ⊢ e₁ ∶ τ₁ → Γ,Δ ⊢ e₂ ∶ τ₂ → (τ₁#τ₂ : τ₁ # τ₂) → Γ,Δ ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ₜ τ₂
|
