Newer
Older
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
70
71
72
73
74
75
76
77
78
79
module CBPV (Σv : Set) (Σc : Set) where
open import Data.Maybe
open import Relation.Binary.PropositionalEquality
data VType : Set
data CType : Set
data VType where
base : Σv -> VType
data CType where
base : Σc -> CType
data Nat : Set where
O : Nat
S : Nat -> Nat
data Fin : Nat -> Set where
fO : ∀ n -> Fin (S n)
fS : ∀ n -> Fin n -> Fin (S n)
record Iso (A B : Set) : Set where
field
to : A -> B
fro : B -> A
sect : ∀ (a : A) -> fro (to a) ≡ a
retr : ∀ (b : B) -> to (fro b) ≡ b
record FinSet : Set₁ where
field
X : Set
card : Nat
is-finite : Iso X (Fin card)
VCtx : FinSet -> Set
VCtx U = FinSet.X U -> VType
record VCCtx (U : FinSet) : Set where
constructor _/_
field
vvars : VCtx U
stoup : Maybe CType
ValSig : Set₁
ValSig = ∀ {U} -> VCtx U -> VType -> Set
CompSig : Set₁
CompSig = ∀ {U} -> VCCtx U -> CType -> Set
module Terms (Σtmv : ValSig) (Σtmc : CompSig) where
data _|-v_ {U} (Γ : VCtx U) : VType -> Set₁
data _|-c_ {U} : (ΓH : VCCtx U) -> CType -> Set₁
val-subst : ∀ U V -> VCtx U -> VCtx V -> Set₁
data _|-mayc_ : ∀ {U} -> VCCtx U -> Maybe CType -> Set₁
record comp-subst U V (ΓH : VCCtx U) (ΔH : VCCtx V) : Set₁
data _|-v_ {U} (Γ : VCtx U) where
var : ∀ (u : FinSet.X U) -> Γ |-v (Γ u)
base : ∀ V (Δ : VCtx V) A (f : Σtmv {V} Δ A) -> val-subst U V Γ Δ -> Γ |-v A
data _|-c_ {U} where
hole : ∀ (Γ : VCtx U) B -> (Γ / just B) |-c B
base : ∀ (ΓH : VCCtx U) V (ΔH : VCCtx V) B (p : Σtmc {V} ΔH B) -> comp-subst U V ΓH ΔH -> ΓH |-c B
val-subst U V Γ Δ = ∀ (v : FinSet.X V) -> _|-v_ {U} Γ (Δ v)
data _|-mayc_ where
done : ∀ U (ΓH : VCCtx U)-> ΓH |-mayc nothing
one : ∀ U (ΓH : VCCtx U) B -> ΓH |-c B -> ΓH |-mayc (just B)
record comp-subst U V ΓH ΔH where
inductive
field
vsubst : val-subst U V (VCCtx.vvars ΓH) (VCCtx.vvars ΔH)
csubst : ΓH |-mayc (VCCtx.stoup ΔH)
vv-substitute : ∀ U V (Γ : VCtx U)(Δ : VCtx V) A -> val-subst U V Γ Δ -> Δ |-v A -> Γ |-v A
vv-compose : ∀ U V W (Γ : VCtx U) (Δ : VCtx V) (E : VCtx W) -> val-subst W V E Δ -> val-subst V U Δ Γ -> val-subst W U E Γ
vv-substitute U V Γ Δ .(Δ u) δ (var u) = δ u
vv-substitute U V Γ Δ A δ (base V₁ Δ' .A f δ') = base V₁ Δ' A f (vv-compose V₁ V U _ _ _ δ δ')
vv-compose U V W Γ Δ E δ γ = λ v → vv-substitute _ _ _ _ _ δ (γ v)