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
|
module Thinned
import Control.Order
import Control.Relation
import public Thinning
%prefix_record_projections off
-- Definition ------------------------------------------------------------------
||| Data embedded in a wider context via a thinning.
public export
record Thinned (t : SnocList a -> Type) (sx : SnocList a) where
constructor Over
{0 support : SnocList a}
value : t support
thin : support `Thins` sx
%name Thinned v, u
||| An equivalence relation on thinned objects.
public export
data (<~>) : Thinned t sx -> Thinned t sx -> Type where
UpToThin :
{0 v : t sx} ->
{0 thin1, thin2 : sx `Thins` sy} ->
thin1 <~> thin2 ->
(<~>) {t} (v `Over` thin1) (v `Over` thin2)
%name Thinned.(<~>) prf
export (.supportPrf) :
{0 v, u : Thinned t sx} ->
v <~> u ->
v.support = u.support
(UpToThin prf) .supportPrf = Refl
export (.valuePrf) :
{0 v, u : Thinned t sx} ->
(e : v <~> u) ->
v.value = (rewrite e.supportPrf in u.value)
(UpToThin prf) .valuePrf = Refl
export (.thinPrf) :
{0 v, u : Thinned t sx} ->
(e : v <~> u) ->
v.thin <~> (rewrite e.supportPrf in u.thin)
(UpToThin prf) .thinPrf = prf
--- Properties
export
irrelevantEquiv :
{0 v, u : Thinned t sx} ->
(0 prf : v <~> u) ->
v <~> u
irrelevantEquiv {v = v `Over` thin1, u = u `Over` thin2} prf =
rewrite prf.supportPrf in
rewrite prf.valuePrf in
UpToThin (rewrite sym prf.supportPrf in irrelevantEquiv prf.thinPrf)
export
Reflexive (Thinned t sx) (<~>) where
reflexive {x = t `Over` thin} = UpToThin reflexive
export
Symmetric (Thinned t sx) (<~>) where
symmetric (UpToThin prf) = UpToThin (symmetric prf)
export
Transitive (Thinned t sx) (<~>) where
transitive (UpToThin prf1) (UpToThin prf2) = UpToThin (transitive prf1 prf2)
export
Equivalence (Thinned t sx) (<~>) where
export
Preorder (Thinned t sx) (<~>) where
-- Operations ------------------------------------------------------------------
||| Map the underlying value.
public export
map : (forall sx. t sx -> u sx) -> Thinned t sx -> Thinned u sx
map f (value `Over` thin) = f value `Over` thin
||| Weaken the surrounding context.
public export
wkn : Thinned t sx -> sx `Thins` sy -> Thinned t sy
wkn (value `Over` thin') thin = value `Over` thin . thin'
||| Shift the surrounding context.
public export
shift : Thinned t sx -> Thinned t (sx :< x)
shift (value `Over` thin) = value `Over` Drop thin
--- Properties
export
mapCong :
{0 t, u : SnocList a -> Type} ->
(0 f : forall sx. t sx -> u sx) ->
{0 v1, v2 : Thinned t sx} ->
v1 <~> v2 ->
map f v1 <~> map f v2
mapCong f (UpToThin prf) = UpToThin prf
export
shiftCong : {0 v, u : Thinned t sx} -> v <~> u -> shift v <~> shift u
shiftCong (UpToThin prf) = UpToThin (dropCong prf)
-- Pairs -----------------------------------------------------------------------
||| Product of two values ensuring the whole context is used.
public export
record Pair (t, u : SnocList a -> Type) (sx : SnocList a) where
constructor MakePair
fst : Thinned t sx
snd : Thinned u sx
0 cover : Covering fst.thin snd.thin
||| Smart constructor for thinned pairs.
export
MkPair : Thinned t sx -> Thinned u sx -> Thinned (Pair t u) sx
MkPair (v `Over` thin1) (u `Over` thin2) =
let cp = coprod thin1 thin2 in
MakePair (v `Over` cp.thin1') (u `Over` cp.thin2') cp.cover `Over` cp.factor
--- Properties
export
mkPairCong :
{0 v1, w1 : Thinned t sx} ->
{0 v2, w2 : Thinned u sx} ->
v1 <~> w1 ->
v2 <~> w2 ->
MkPair v1 v2 <~> MkPair w1 w2
|
