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
181
182
|
module Core.Generic
import Core.Declarative
import Core.Environment
import Core.Reduction
import Core.Term
import Core.Term.NormalForm
import Core.Term.Substitution
import Core.Term.Thinned
import Core.Thinning
%prefix_record_projections off
-- Definition ------------------------------------------------------------------
public export
record Equality where
constructor MkEquality
TypeEq : forall n. Env n -> Term n -> Term n -> Type
TermEq : forall n. Env n -> Term n -> Term n -> Term n -> Type
NtrlEq : forall n. Env n -> NeutralTerm n -> NeutralTerm n -> Term n -> Type
public export
interface IsEq (0 eq : Equality) where
-- Subsumption
ntrlEqImpliesTermEq :
{0 n, m : NeutralTerm k} ->
eq.NtrlEq env n m a ->
eq.TermEq env n.fst m.fst a
termEqImpliesTypeEq : eq.TermEq {n} env a b Set -> eq.TypeEq env a b
termEqImpliesConv : eq.TermEq {n} env t u a -> TermConv env t u a
typeEqImpliesConv : eq.TypeEq {n} env a b -> TypeConv env a b
-- Partial Equivalence
ntrlSym : eq.NtrlEq {n = k} env n m a -> eq.NtrlEq env m n a
ntrlTrans : eq.NtrlEq {n = k} env n1 n2 a -> eq.NtrlEq env n2 n3 a -> eq.NtrlEq env n1 n3 a
termSym : eq.TermEq {n} env t u a -> eq.TermEq env u t a
termTrans : eq.TermEq {n} env t u a -> eq.TermEq env u v a -> eq.TermEq env t v a
typeSym : eq.TypeEq {n} env a b -> eq.TypeEq env b a
typeTrans : eq.TypeEq {n} env a b -> eq.TypeEq env b c -> eq.TypeEq env a c
-- Conversion
ntrlConv : eq.NtrlEq {n = k} env n m a -> TypeConv env a b -> eq.NtrlEq env n m b
termConv : eq.TermEq {n} env t u a -> TypeConv env a b -> eq.TermEq env t u b
-- Weakening
wknNtrl :
eq.NtrlEq {n = j} env1 n m a ->
ExtendsWf thin env2 env1 ->
eq.NtrlEq {n = k} env2 (wkn n thin) (wkn m thin) (wkn a thin)
wknTerm :
eq.TermEq {n = m} env1 t u a ->
ExtendsWf thin env2 env1 ->
eq.TermEq {n} env2 (wkn t thin) (wkn u thin) (wkn a thin)
wknType :
eq.TypeEq {n = m} env1 a b ->
ExtendsWf thin env2 env1 ->
eq.TypeEq {n} env2 (wkn a thin) (wkn b thin)
-- Weak Head Expansion
expandTerm :
TermReduce env t t' a ->
TermReduce env u u' a ->
Whnf t' ->
Whnf u' ->
eq.TermEq {n} env t' u' a ->
eq.TermEq env t u a
expandType :
TypeReduce env a a' ->
TypeReduce env b b' ->
Whnf a' ->
Whnf b' ->
eq.TypeEq {n} env a' b' ->
eq.TypeEq env a b
-- Neutral Congruence
ntrlVar :
TermWf env (Var i) a ->
---
eq.NtrlEq {n} env (Element (Var i) Var) (Element (Var i) Var) a
ntrlApp :
{0 n, m : NeutralTerm k} ->
eq.NtrlEq env n m (Pi a b) ->
eq.TermEq env t u a ->
---
eq.NtrlEq env
(Element (App n.fst t) (App n.snd))
(Element (App m.fst u) (App m.snd))
(subst1 b t)
-- Term Congurence
termPi :
TypeWf env a ->
eq.TermEq env a c Set ->
eq.TermEq (env :< pure a) b d Set ->
---
eq.TermEq {n} env (Pi a b) (Pi c d) Set
termPiEta :
TypeWf env a ->
TermWf env t (Pi a b) ->
TermWf env u (Pi a b) ->
eq.TermEq (env :< pure a)
(App (wkn t $ drop $ id _) (Var FZ))
(App (wkn u $ drop $ id _) (Var FZ))
b ->
---
eq.TermEq {n} env t u (Pi a b)
-- Type Congruence
typeSet :
EnvWf env ->
---
eq.TypeEq {n} env Set Set
typePi :
TypeWf env a ->
eq.TypeEq env a c ->
eq.TypeEq (env :< pure a) b d ->
---
eq.TypeEq {n} env (Pi a b) (Pi c d)
export
ntrlEqImpliesTypeEq : IsEq eq => eq.NtrlEq {n = k} env n m Set -> eq.TypeEq env n.fst m.fst
ntrlEqImpliesTypeEq = termEqImpliesTypeEq . ntrlEqImpliesTermEq
-- Instance 1 ------------------------------------------------------------------
public export
Judgemental : Equality
Judgemental = MkEquality TypeConv TermConv (\env, n, m, a => TermConv env n.fst m.fst a)
judgeWknNtrl :
(Judgemental .NtrlEq) {n = j} env1 n m a ->
ExtendsWf thin env2 env1 ->
(Judgemental .NtrlEq) {n = k} env2 (wkn n thin) (wkn m thin) (wkn a thin)
judgeWknNtrl {n = Element t n, m = Element u m} = weakenTermConv
export
IsEq Judgemental where
-- Subsumption
ntrlEqImpliesTermEq = id
termEqImpliesTypeEq = LiftConv
termEqImpliesConv = id
typeEqImpliesConv = id
-- Partial Equivalence
ntrlSym = SymTm
ntrlTrans = TransTm
termSym = SymTm
termTrans = TransTm
typeSym = SymTy
typeTrans = TransTy
-- Conversion
ntrlConv = ConvConv
termConv = ConvConv
-- Weakening
wknNtrl = judgeWknNtrl
wknTerm = weakenTermConv
wknType = weakenTypeConv
-- Weak Head Expansion
expandTerm = \steps1, steps2, n, m, eq =>
TransTm (termRedImpliesConv steps1) $
TransTm eq $
SymTm (termRedImpliesConv steps2)
expandType = \steps1, steps2, n, m, eq =>
TransTy (typeRedImpliesConv steps1) $
TransTy eq $
SymTy (typeRedImpliesConv steps2)
-- Neutral Congruence
ntrlVar = ReflTm
ntrlApp = AppConv
-- Term Congurence
termPi = PiTmConv
termPiEta = PiEta
-- Type Congruence
typeSet = ReflTy . SetTyWf
typePi = PiConv
|
