blob: 22a72728845f58077c734f685fabdea3eaac8f33 (
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 Obs.Substitution
import public Data.List.Elem
%default total
infix 5 ~|>
namespace Sorted
public export 0
Family : Type -> Type
Family a = a -> List a -> Type
public export 0
Map : List a -> Family a -> List a -> Type
Map ctx x ctx' = {s : a} -> Elem s ctx -> x s ctx'
public export 0
Hom : Family a -> Family a -> Family a
Hom x y s ctx = forall ctx' . Map ctx x ctx' -> y s ctx'
public export 0
(~|>) : Family a -> Family a -> Type
x ~|> y = forall ctx . {s : a} -> x s ctx -> y s ctx
public export
interface Rename (0 a : _) (0 x : Family a) | x where
rename : x ~|> Hom Elem x
public export
interface Rename a x => PointedRename a (0 b : a -> Type) x | x where
point : forall ctx . {s : a} -> b s -> Elem s ctx -> x s ctx
namespace Unsorted
public export 0
Family : Type -> Type
Family a = List a -> Type
public export 0
Hom : Sorted.Family a -> Unsorted.Family a -> Unsorted.Family a
Hom x y ctx = forall ctx' . Map ctx x ctx' -> y ctx'
public export 0
(~|>) : Unsorted.Family a -> Unsorted.Family a -> Type
x ~|> y = forall ctx . x ctx -> y ctx
public export
interface Rename (0 a : _) (0 x : Unsorted.Family a) | x where
rename : x ~|> Hom Elem x
public export
Sorted.Rename a Elem where
rename i f = f i
public export
PointedRename a (const ()) Elem where
point _ = id
public export
add : (0 x : Sorted.Family a) -> x s' ctx' -> Map ctx x ctx' -> Map (s' :: ctx) x ctx'
add x v f Here = v
add x v f (There i) = f i
public export
lift : PointedRename a b x => (ctx : List (s ** b s))
-> Map ctx' x ctx''
-> Map (map DPair.fst ctx ++ ctx') x (map DPair.fst ctx ++ ctx'')
lift [] f = f
lift ((s ** y) :: ctx) f = add x (point y Here) (\i => rename (lift ctx f i) There)
elemAppRight : (xs : List a) -> (0 ys : List a) -> Elem x ys -> Elem.Elem x (xs ++ ys)
elemAppRight [] _ = id
elemAppRight (x :: xs) ys = There . elemAppRight xs ys
namespace Sorted
export
weaken : Sorted.Rename a x => (ctx : _) -> x ~|> (\s, ctx' => x s (ctx ++ ctx'))
weaken ctx t = rename t (elemAppRight ctx _)
namespace Unsorted
export
weaken : Unsorted.Rename a x => (ctx : _) -> x ~|> (\ctx' => x (ctx ++ ctx'))
weaken ctx t = rename t (elemAppRight ctx _)
|
