blob: bd11fada79d5304f53f670cddc7b991987b8ce19 (
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
|
module Core.Generic
import Core.Context
import Core.Declarative
import Core.Environment
import Core.Reduction
import Core.Term
import Core.Term.NormalForm
import Core.Term.Substitution
import Core.Thinning
import Core.Var
%prefix_record_projections off
-- Definition ------------------------------------------------------------------
record GenericEquality where
constructor MkEquality
TypeEq : forall sx. Env sx -> Term sx -> Term sx -> Type
TermEq : forall sx. Env sx -> Term sx -> Term sx -> Term sx -> Type
NtrlEq : forall sx. Env sx -> Term sx -> Term sx -> Term sx -> Type
interface IsGenericEquality (eq : GenericEquality) where
-- Subsumption
ntrlImpliesTermEq : eq.NtrlEq {sx} env t u a -> eq.TermEq env t u a
termImpliesTypeEq : eq.TermEq {sx} env a b Set -> eq.TypeEq env a b
eqImpliesTermConv : eq.TermEq {sx} env t u a -> TermConv env t u a
eqImpliesTypeConv : eq.TypeEq {sx} env a b -> TypeConv env a b
-- Partial Equivalence
ntrlSym : eq.NtrlEq {sx} env t u a -> eq.NtrlEq env u t a
ntrlTrans : eq.NtrlEq {sx} env t u a -> eq.NtrlEq env u v a -> eq.NtrlEq env t v a
termSym : eq.TermEq {sx} env t u a -> eq.TermEq env u t a
termTrans : eq.TermEq {sx} env t u a -> eq.TermEq env u v a -> eq.TermEq env t v a
typeSym : eq.TypeEq {sx} env a b -> eq.TypeEq env b a
typeTrans : eq.TypeEq {sx} env a b -> eq.TypeEq env b c -> eq.TypeEq env a c
-- Conversion
ntrlConv : eq.NtrlEq {sx} env t u a -> TypeConv env a b -> eq.NtrlEq env t u b
termConv : eq.TermEq {sx} env t u a -> TypeConv env a b -> eq.TermEq env t u b
-- Weakening
wknPresNtrlEq :
eq.NtrlEq {sx} env1 t u a ->
EnvWf env2 ->
IsExtension thin env2 env1 ->
eq.NtrlEq {sx = sy} env2 (wkn t thin) (wkn u thin) (wkn a thin)
wknPresTermEq :
eq.TermEq {sx} env1 t u a ->
EnvWf env2 ->
IsExtension thin env2 env1 ->
eq.TermEq {sx = sy} env2 (wkn t thin) (wkn u thin) (wkn a thin)
wknPresTypeEq :
eq.TypeEq {sx} env1 a b ->
EnvWf env2 ->
IsExtension thin env2 env1 ->
eq.TypeEq {sx = sy} env2 (wkn a thin) (wkn b thin)
-- Weak Head Expansion
typeExpansion :
TypeRed env a a' ->
TypeRed env b b' ->
Whnf a' ->
Whnf b' ->
eq.TypeEq {sx} env a' b' ->
eq.TypeEq env a b
termExpansion :
TypeRed env a b ->
TermRed env t t' b ->
TermRed env u u' b ->
Whnf b ->
Whnf t' ->
Whnf u' ->
eq.TermEq {sx} env t' u' b ->
eq.TermEq env t u a
-- Type Constructor Congruence
typeSet :
EnvWf env ->
---
eq.TypeEq {sx} env Set Set
typePi :
TypeWf env f ->
eq.TypeEq env f h ->
eq.TypeEq (env :< f) g e ->
---
eq.TypeEq {sx} env (Pi n f g) (Pi n h e)
-- Term Constructor Congruence and η
termPi :
TypeWf env f ->
eq.TermEq env f h Set ->
eq.TermEq (env :< f) g e Set ->
---
eq.TermEq {sx} env (Pi n f g) (Pi n h e) Set
termPiEta :
TypeWf env f ->
TermWf env t (Pi n f g) ->
TermWf env u (Pi n f g) ->
eq.TermEq (env :< f)
(App (wkn t (wkn1 _ n)) (Var Var.here))
(App (wkn u (wkn1 _ n)) (Var Var.here))
g ->
---
eq.TermEq {sx} env t u (Pi n f g)
-- Neutral Congruence
ntrlVar :
TermWf env (Var i) a ->
---
eq.NtrlEq {sx} env (Var i) (Var i) a
ntrlApp :
eq.NtrlEq env t u (Pi n f g) ->
eq.TermEq env a b f ->
---
eq.NtrlEq {sx} env (App t a) (App u b) (subst g (sub1 a))
-- Judgemental Equality --------------------------------------------------------
Judgemental : GenericEquality
Judgemental = MkEquality TypeConv TermConv TermConv
IsGenericEquality Judgemental where
ntrlImpliesTermEq = id
termImpliesTypeEq = LiftConv
eqImpliesTermConv = id
eqImpliesTypeConv = id
ntrlSym = SymTerm
ntrlTrans = TransTerm
termSym = SymTerm
termTrans = TransTerm
typeSym = SymType
typeTrans = TransType
ntrlConv = ConvTermConv
termConv = ConvTermConv
wknPresNtrlEq = wknPresTermConv
wknPresTermEq = wknPresTermConv
wknPresTypeEq = wknPresTypeConv
typeExpansion steps1 steps2 n m conv =
TransType (typeRedImpliesTypeConv steps1) $
TransType conv $
SymType (typeRedImpliesTypeConv steps2)
termExpansion steps1 steps2 steps3 n m k conv =
ConvTermConv
(TransTerm (termRedImpliesTermConv steps2) $
TransTerm conv $
SymTerm (termRedImpliesTermConv steps3))
(SymType $ typeRedImpliesTypeConv steps1)
typeSet = ReflType . SetType
typePi = PiTypeConv
termPi = PiTermConv
termPiEta = PiEta
ntrlVar = ReflTerm
ntrlApp = AppConv
|
