blob: 3a06612bddf318bb5e24833454d8ce1512353de4 (
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
|
module Core.Term.Thinned
import Core.Term
import Core.Thinning
import Syntax.PreorderReasoning
%prefix_record_projections off
infix 4 =~=
-- Definition ------------------------------------------------------------------
public export
record Thinned (n : Nat) where
constructor Over
{0 m : Nat}
term : Term m
thin : m `Thins` n
%name Thinned t, u, v
%inline
public export
pure : Term n -> Thinned n
pure = (`Over` id n)
%inline
public export
expand : Thinned n -> Term n
expand (term `Over` thin) = wkn term thin
public export
(=~=) : Thinned n -> Thinned n -> Type
t =~= u = expand t = expand u
-- Weakening -------------------------------------------------------------------
public export
wkn : Thinned m -> m `Thins` n -> Thinned n
wkn t thin = { thin $= (thin .) } t
export
wknCong : t =~= u -> (thin : m `Thins` n) -> wkn t thin =~= wkn u thin
wknCong {t = t `Over` thin1, u = u `Over` thin2} prf thin = Calc $
|~ wkn t (thin . thin1)
~~ wkn (wkn t thin1) thin ...(sym $ wknHomo t thin1 thin)
~~ wkn (wkn u thin2) thin ...(cong (flip wkn thin) prf)
~~ wkn u (thin . thin2) ...(wknHomo u thin2 thin)
export
wknHomo :
(t : Thinned k) ->
(thin1 : k `Thins` m) ->
(thin2 : m `Thins` n) ->
wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
wknHomo (t `Over` thin) thin1 thin2 = cong (t `Over`) (compAssoc thin2 thin1 thin)
|
