blob: 8c05e03d2bfefb8403daf0eb40eadb560429701b (
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
|
module Core.Term
import Core.Thinning
import public Data.Fin
import Syntax.PreorderReasoning
-- Definition ------------------------------------------------------------------
public export
data Term : Nat -> Type where
Var : Fin n -> Term n
Set : Term n
Pi : Term n -> Term (S n) -> Term n
Abs : Term (S n) -> Term n
App : Term n -> Term n -> Term n
%name Term t, u, v
-- Impossibilities -------------------------------------------------------------
export
Uninhabited (Set = Pi f g) where uninhabited prf impossible
export
Uninhabited (Pi f g = Set) where uninhabited prf impossible
-- Weakening -------------------------------------------------------------------
public export
wkn : Term m -> m `Thins` n -> Term n
wkn (Var i) thin = Var (wkn i thin)
wkn Set thin = Set
wkn (Pi t u) thin = Pi (wkn t thin) (wkn u $ keep thin)
wkn (Abs t) thin = Abs (wkn t $ keep thin)
wkn (App t u) thin = App (wkn t thin) (wkn u thin)
export
wknId : (t : Term n) -> wkn t (id n) = t
wknId (Var i) = cong Var (wknId i)
wknId Set = Refl
wknId (Pi t u) = cong2 Pi (wknId t) (trans (cong (wkn u) $ keepIdIsId n) (wknId u))
wknId (Abs t) = cong Abs (trans (cong (wkn t) $ keepIdIsId n) (wknId t))
wknId (App t u) = cong2 App (wknId t) (wknId u)
export
wknHomo :
(t : Term k) ->
(thin1 : k `Thins` m) ->
(thin2 : m `Thins` n) ->
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 t u) thin1 thin2 =
cong2 Pi
(wknHomo t thin1 thin2)
(trans
(wknHomo u (keep thin1) (keep thin2))
(cong (wkn u) $ compKeep thin2 thin1))
wknHomo (Abs t) thin1 thin2 =
cong Abs
(trans
(wknHomo t (keep thin1) (keep thin2))
(cong (wkn t) $ compKeep thin2 thin1))
wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
export
wkn1Comm :
(t : Term m) ->
(thin : m `Thins` n) ->
wkn (wkn t thin) (wkn1 n) = wkn (wkn t $ wkn1 m) (keep thin)
wkn1Comm t thin = Calc $
|~ wkn (wkn t thin) (wkn1 n)
~~ wkn t (wkn1 n . thin) ...(wknHomo t thin (wkn1 n))
~~ wkn t (keep thin . wkn1 m) ...(sym $ cong (wkn t) $ wkn1Comm thin)
~~ wkn (wkn t $ wkn1 m) (keep thin) ...(sym $ wknHomo t (wkn1 m) (keep thin))
|
