blob: 51947e0391d910e79150311855fea48abf1069db (
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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
module Core.Thinning
import Data.Fin
-- Definition ------------------------------------------------------------------
data Thinner : Nat -> Nat -> Type where
IsBase : Thinner n (S n)
IsDrop : Thinner m n -> Thinner m (S n)
IsKeep : Thinner m n -> Thinner (S m) (S n)
export
data Thins : Nat -> Nat -> Type where
IsId : n `Thins` n
IsThinner : Thinner m n -> m `Thins` n
%name Thinner thin
%name Thins thin
-- Constructors ----------------------------------------------------------------
export
id : (0 n : Nat) -> n `Thins` n
id n = IsId
export
drop : m `Thins` n -> m `Thins` S n
drop IsId = IsThinner IsBase
drop (IsThinner thin) = IsThinner (IsDrop thin)
export
keep : m `Thins` n -> S m `Thins` S n
keep IsId = IsId
keep (IsThinner thin) = IsThinner (IsKeep thin)
-- Non-Identity ----------------------------------------------------------------
export
data IsNotId : m `Thins` n -> Type where
ItIsThinner : IsNotId (IsThinner thin)
%name IsNotId prf
-- Views -----------------------------------------------------------------------
public export
data View : m `Thins` n -> Type where
Id : (0 n : Nat) -> View (id n)
Drop : (thin : m `Thins` n) -> View (drop thin)
Keep : (thin : m `Thins` n) -> {auto 0 prf : IsNotId thin} -> View (keep thin)
export
view : (thin : m `Thins` n) -> View thin
view IsId = Id m
view (IsThinner IsBase) = Drop (id _)
view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
-- Composition -----------------------------------------------------------------
comp : Thinner m n -> Thinner k m -> Thinner k n
comp IsBase thin2 = IsDrop thin2
comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) IsBase = IsDrop thin1
comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)
export
(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
IsId . thin2 = thin2
IsThinner thin1 . IsId = IsThinner thin1
IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)
-- Categorical
comp'Assoc :
(thin3 : Thinner m n) ->
(thin2 : Thinner k m) ->
(thin1 : Thinner j k) ->
comp thin3 (comp thin2 thin1) = comp (comp thin3 thin2) thin1
comp'Assoc IsBase thin2 thin1 = Refl
comp'Assoc (IsDrop thin3) thin2 thin1 = cong IsDrop (comp'Assoc thin3 thin2 thin1)
comp'Assoc (IsKeep thin3) IsBase thin1 = Refl
comp'Assoc (IsKeep thin3) (IsDrop thin2) thin1 = cong IsDrop (comp'Assoc thin3 thin2 thin1)
comp'Assoc (IsKeep thin3) (IsKeep thin2) IsBase = Refl
comp'Assoc (IsKeep thin3) (IsKeep thin2) (IsDrop thin1) = cong IsDrop (comp'Assoc thin3 thin2 thin1)
comp'Assoc (IsKeep thin3) (IsKeep thin2) (IsKeep thin1) = cong IsKeep (comp'Assoc thin3 thin2 thin1)
export
compAssoc :
(thin3 : m `Thins` n) ->
(thin2 : k `Thins` m) ->
(thin1 : j `Thins` k) ->
thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
compAssoc IsId thin2 thin1 = Refl
compAssoc (IsThinner thin3) IsId thin1 = Refl
compAssoc (IsThinner thin3) (IsThinner thin2) IsId = Refl
compAssoc (IsThinner thin3) (IsThinner thin2) (IsThinner thin1) =
cong IsThinner (comp'Assoc thin3 thin2 thin1)
export
compLeftId : (thin : m `Thins` n) -> id n . thin = thin
compLeftId thin = Refl
export
compRightId : (thin : m `Thins` n) -> thin . id m = thin
compRightId IsId = Refl
compRightId (IsThinner thin) = Refl
-- Specific Cases
export
compLeftDrop :
(thin2 : m `Thins` n) ->
(thin1 : k `Thins` m) ->
drop thin2 . thin1 = drop (thin2 . thin1)
compLeftDrop IsId IsId = Refl
compLeftDrop IsId (IsThinner thin1) = Refl
compLeftDrop (IsThinner thin2) IsId = Refl
compLeftDrop (IsThinner thin2) (IsThinner thin1) = Refl
export
compRightDrop :
(thin2 : m `Thins` n) ->
(thin1 : k `Thins` m) ->
keep thin2 . drop thin1 = drop (thin2 . thin1)
compRightDrop IsId thin1 = Refl
compRightDrop (IsThinner thin2) IsId = Refl
compRightDrop (IsThinner thin2) (IsThinner thin1) = Refl
export
compKeep :
(thin1 : m `Thins` n) ->
(thin2 : k `Thins` m) ->
keep thin1 . keep thin2 = keep (thin1 . thin2)
compKeep IsId thin2 = Refl
compKeep (IsThinner thin1) IsId = Refl
compKeep (IsThinner thin1) (IsThinner thin2) = Refl
-- Weakening -------------------------------------------------------------------
wkn' : Fin m -> Thinner m n -> Fin n
wkn' i IsBase = FS i
wkn' i (IsDrop thin) = FS (wkn' i thin)
wkn' FZ (IsKeep thin) = FZ
wkn' (FS i) (IsKeep thin) = FS (wkn' i thin)
export
wkn : Fin m -> m `Thins` n -> Fin n
wkn i IsId = i
wkn i (IsThinner thin) = wkn' i thin
-- Properties
wkn'Homo :
(i : Fin k) ->
(thin2 : Thinner m n) ->
(thin1 : Thinner k m) ->
wkn' (wkn' i thin1) thin2 = wkn' i (comp thin2 thin1)
wkn'Homo i IsBase thin1 = Refl
wkn'Homo i (IsDrop thin2) thin1 = cong FS (wkn'Homo i thin2 thin1)
wkn'Homo i (IsKeep thin2) IsBase = Refl
wkn'Homo i (IsKeep thin2) (IsDrop thin1) = cong FS (wkn'Homo i thin2 thin1)
wkn'Homo FZ (IsKeep thin2) (IsKeep thin1) = Refl
wkn'Homo (FS i) (IsKeep thin2) (IsKeep thin1) = cong FS (wkn'Homo i thin2 thin1)
export
wknHomo :
(i : Fin k) ->
(thin1 : k `Thins` m) ->
(thin2 : m `Thins` n) ->
wkn (wkn i thin1) thin2 = wkn i (thin2 . thin1)
wknHomo i IsId thin2 = sym $ cong (wkn i) $ compRightId thin2
wknHomo i (IsThinner thin1) IsId = Refl
wknHomo i (IsThinner thin1) (IsThinner thin2) = wkn'Homo i thin2 thin1
|
