blob: e52545d643ea748967ed52d2aa4f741780d4cae7 (
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
|
module Core.Term
import Core.Context
import Core.Var
import Core.Thinning
import Syntax.PreorderReasoning
%prefix_record_projections off
-- Definition ------------------------------------------------------------------
public export
data Term : Context -> Type where
Var : Var sx -> Term sx
Set : Term sx
Pi : (n : Name) -> Term sx -> Term (sx :< n) -> Term sx
Abs : (n : Name) -> Term (sx :< n) -> Term sx
App : Term sx -> Term sx -> Term sx
%name Term t, u, v
-- Weakening -------------------------------------------------------------------
public export
wkn : Term sx -> sx `Thins` sy -> Term sy
wkn (Var i) thin = Var $ wkn i thin
wkn Set thin = Set
wkn (Pi n t u) thin = Pi n (wkn t thin) (wkn u $ keep thin n)
wkn (Abs n t) thin = Abs n (wkn t $ keep thin n)
wkn (App t u) thin = App (wkn t thin) (wkn u thin)
-- Is Homomorphic
export
wknHomo :
(t : Term sx) ->
(thin1 : sx `Thins` sy) ->
(thin2 : sy `Thins` sz) ->
wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
wknHomo (Var i) thin1 thin2 = cong Var $ wknHomo i thin1 thin2
wknHomo Set thin1 thin2 = Refl
wknHomo (Pi n t u) thin1 thin2 =
cong2 (Pi n) (wknHomo t thin1 thin2) $
Calc $
|~ wkn (wkn u (keep thin1 n)) (keep thin2 n)
~~ wkn u (keep thin2 n . keep thin1 n) ...(wknHomo u (keep thin1 n) (keep thin2 n))
~~ wkn u (keep (thin2 . thin1) n) ...(cong (wkn u) $ compKeep thin2 thin1 n)
wknHomo (Abs n t) thin1 thin2 =
cong (Abs n) $
Calc $
|~ wkn (wkn t (keep thin1 n)) (keep thin2 n)
~~ wkn t (keep thin2 n . keep thin1 n) ...(wknHomo t (keep thin1 n) (keep thin2 n))
~~ wkn t (keep (thin2 . thin1) n) ...(cong (wkn t) $ compKeep thin2 thin1 n)
wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
-- Thinned Terms ---------------------------------------------------------------
public export
record Thinned (sx : Context) where
constructor Over
{0 sy : Context}
term : Term sy
thin : sy `Thins` sx
%name Thinned t, u, v
public export
expand : Thinned sx -> Term sx
expand (term `Over` thin) = wkn term thin
public export
shift : Thinned sx -> sx `Thins` sy -> Thinned sy
shift (term `Over` thin') thin = term `Over` thin . thin'
export
expandShift :
(t : Thinned sx) ->
(thin : sx `Thins` sy) ->
expand (shift t thin) = wkn (expand t) thin
expandShift (term `Over` thin') thin = sym $ wknHomo term thin' thin
|
