blob: 4a279237c5a5b023f3f45d5bc2089d7e0e8b12fe (
plain)
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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
|
module Core.Declarative
import Core.Context
import Core.Name
import Core.Term
import Core.Term.Environment
import Core.Term.Substitution
import Core.Thinning
import Core.Var
import Data.Nat
public export
data EnvWf : Env sx -> Type
public export
data TypeWf : Env sx -> Term sx -> Type
public export
data TypeConv : Env sx -> Term sx -> Term sx -> Type
public export
data TermWf : Env sx -> Term sx -> Term sx -> Type
public export
data TermConv : Env sx -> Term sx -> Term sx -> Term sx -> Type
data EnvWf where
Lin :
---
EnvWf [<]
(:<) :
EnvWf env ->
TypeWf env (wkn a thin) ->
---
EnvWf (Add env thin a)
data TypeWf where
SetType :
EnvWf env ->
---
TypeWf env Set
PiType :
TypeWf env f ->
TypeWf (env :< f) g ->
---
TypeWf env (Pi n f g)
LiftType :
TermWf env a Set ->
---
TypeWf env a
data TypeConv where
ReflType :
TypeWf env a ->
---
TypeConv env a a
SymType :
TypeConv env a b ->
---
TypeConv env b a
TransType :
TypeConv env a b ->
TypeConv env b c ->
---
TypeConv env a c
PiTypeConv :
TypeWf env f ->
TypeConv env f h ->
TypeConv (env :< f) g e ->
---
TypeConv env (Pi n f g) (Pi n h e)
LiftConv :
TermConv env a b Set ->
---
TypeConv env a b
data TermWf where
VarTerm :
EnvWf env ->
---
TermWf env (Var i) (index env i)
PiTerm :
TermWf env f Set ->
TermWf (env :< f) g Set ->
---
TermWf env (Pi n f g) Set
AbsTerm :
TypeWf env f ->
TermWf (env :< f) t g ->
---
TermWf env (Abs n t) (Pi n f g)
AppTerm :
TermWf env t (Pi n f g) ->
TermWf env u f ->
---
TermWf env (App t u) (subst g $ sub1 u)
ConvTerm :
TermWf env t a ->
TypeConv env a b ->
---
TermWf env t b
data TermConv where
ReflTerm :
TermWf env t a ->
---
TermConv env t t a
SymTerm :
TermConv env t u a ->
---
TermConv env u t a
TransTerm :
TermConv env t u a ->
TermConv env u v a ->
---
TermConv env t v a
ConvTermConv :
TermConv env t u a ->
TypeConv env a b ->
---
TermConv env t u b
PiTermConv :
TypeWf env f ->
TermConv env f h Set ->
TermConv (env :< f) g e Set ->
---
TermConv env (Pi n f g) (Pi n h e) Set
PiBeta :
TypeWf env f ->
TermWf (env :< f) t g ->
TermWf env u f ->
---
TermConv env (App (Abs n t) u) (subst t $ sub1 u) (subst g $ sub1 u)
PiEta :
TypeWf env f ->
TermWf env t (Pi n f g) ->
TermWf env u (Pi n f g) ->
TermConv (env :< f) (App (wkn t $ drop (id _) n) a) (App (wkn u $ drop (id _) n) a) g ->
---
TermConv env t u (Pi n f g)
AppConv :
TermConv env t u (Pi n f g) ->
TermConv env a b f ->
---
TermConv env (App t a) (App u b) (subst g $ sub1 a)
%name EnvWf wf
%name TypeWf wf
%name TypeConv conv
%name TermWf wf
%name TermConv conv
-- Well Formed Environment -----------------------------------------------------
typeWfImpliesEnvWf : TypeWf env a -> EnvWf env
typeConvImpliesEnvWf : TypeConv env a b -> EnvWf env
termWfImpliesEnvWf : TermWf env t a -> EnvWf env
termConvImpliesEnvWf : TermConv env t u a -> EnvWf env
typeWfImpliesEnvWf (SetType envWf) = envWf
typeWfImpliesEnvWf (PiType wf wf1) = typeWfImpliesEnvWf wf
typeWfImpliesEnvWf (LiftType wf) = termWfImpliesEnvWf wf
typeConvImpliesEnvWf (ReflType wf) = typeWfImpliesEnvWf wf
typeConvImpliesEnvWf (SymType conv) = typeConvImpliesEnvWf conv
typeConvImpliesEnvWf (TransType conv conv1) = typeConvImpliesEnvWf conv
typeConvImpliesEnvWf (PiTypeConv wf conv conv1) = typeConvImpliesEnvWf conv
typeConvImpliesEnvWf (LiftConv conv) = termConvImpliesEnvWf conv
termWfImpliesEnvWf (VarTerm envWf) = envWf
termWfImpliesEnvWf (PiTerm wf wf1) = termWfImpliesEnvWf wf
termWfImpliesEnvWf (AbsTerm wf wf1) = typeWfImpliesEnvWf wf
termWfImpliesEnvWf (AppTerm wf wf1) = termWfImpliesEnvWf wf
termWfImpliesEnvWf (ConvTerm wf conv) = termWfImpliesEnvWf wf
termConvImpliesEnvWf (ReflTerm wf) = termWfImpliesEnvWf wf
termConvImpliesEnvWf (SymTerm conv) = termConvImpliesEnvWf conv
termConvImpliesEnvWf (TransTerm conv conv1) = termConvImpliesEnvWf conv
termConvImpliesEnvWf (ConvTermConv conv conv1) = termConvImpliesEnvWf conv
termConvImpliesEnvWf (PiTermConv wf conv conv1) = termConvImpliesEnvWf conv
termConvImpliesEnvWf (PiBeta wf wf1 wf2) = typeWfImpliesEnvWf wf
termConvImpliesEnvWf (PiEta wf wf1 wf2 conv) = typeWfImpliesEnvWf wf
termConvImpliesEnvWf (AppConv conv conv1) = termConvImpliesEnvWf conv
|
