blob: 37b6b36504817bd9763db199749d7c2ad2574c88 (
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
|
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))
|
