blob: 6a2c8bda25c20b07313f7344a2683912693b07a3 (
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
|
module Core.Declarative
import Core.Environment
import Core.Term
import Core.Term.Substitution
import Core.Term.Thinned
import Core.Thinning
-- Definition ------------------------------------------------------------------
data EnvWf : Env n -> Type
data TypeWf : Env n -> Term n -> Type
data TypeConv : Env n -> Term n -> Term n -> Type
data TermWf : Env n -> Term n -> Term n -> Type
data TermConv : Env n -> Term n -> Term n -> Term n -> Type
data EnvWf where
Lin : EnvWf [<]
(:<) : EnvWf env -> TypeWf env (expand a) -> EnvWf (env :< a)
data TypeWf where
SetTyWf :
EnvWf env ->
---
TypeWf env Set
PiTyWf :
TypeWf env a ->
TypeWf (env :< pure a) b ->
---
TypeWf env (Pi a b)
LiftWf :
TermWf env a Set ->
---
TypeWf env a
data TypeConv where
ReflTy :
TypeWf env a ->
---
TypeConv env a a
SymTy :
TypeConv env a b ->
---
TypeConv env b a
TransTy :
TypeConv env a b ->
TypeConv env b c ->
---
TypeConv env a c
PiConv :
TypeWf env a ->
TypeConv env a c ->
TypeConv (env :< pure a) b d ->
---
TypeConv env (Pi a b) (Pi c d)
LiftConv :
TermConv env a b Set ->
---
TypeConv env a b
data TermWf where
PiTmWf :
TermWf env a Set ->
TermWf (env :< pure a) b Set ->
---
TermWf env (Pi a b) Set
VarWf :
EnvWf env ->
---
TermWf env (Var i) (expand $ index env i)
AbsWf :
TypeWf env a ->
TermWf (env :< pure a) t b ->
---
TermWf env (Abs t) (Pi a b)
AppWf :
TermWf env t (Pi a b) ->
TermWf env u a ->
---
TermWf env (App t u) (subst b $ Wkn (id _) :< pure u)
ConvWf :
TermWf env t a ->
TypeConv env a b ->
---
TermWf env t b
data TermConv where
ReflTm :
TermWf env t a ->
---
TermConv env t t a
SymTm :
TermConv env t u a ->
---
TermConv env u t a
TransTm :
TermConv env t u a ->
TermConv env u v a ->
---
TermConv env t v a
AppConv :
TermConv env f g (Pi a b) ->
TermConv env t u a ->
---
TermConv env (App f t) (App g u) (subst b $ Wkn (id _) :< pure t)
PiTmConv :
TypeWf env a ->
TermConv env a c Set ->
TermConv (env :< pure a) b d Set ->
---
TermConv env (Pi a b) (Pi c d) Set
PiEta :
TypeWf env a ->
TermWf env t (Pi a b) ->
TermWf env u (Pi a b) ->
TermConv (env :< pure a)
(App (wkn t $ drop $ id _) (Var FZ))
(App (wkn u $ drop $ id _) (Var FZ))
b ->
---
TermConv env t u (Pi a b)
PiBeta :
TypeWf env a ->
TermWf (env :< pure a) t b ->
TermWf env u a ->
---
TermConv env
(App (Abs t) u)
(subst t $ Wkn (id _) :< pure u)
(subst g $ Wkn (id _) :< pure u)
ConvConv :
TermConv env t u a ->
TypeConv env a b ->
---
TermConv env t u b
|
