blob: 99cc1ab6c666b00dd228f7ae19802779343edb93 (
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
|
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 a ->
---
EnvWf (env :< 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
|
