blob: f742183ce8634b052066e7ae9cabbd94e1691a26 (
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
|
TypeData : Set 1
TypeData = (index : Set) ** (x : index) -> Set
index : (type : TypeData) -> Set
index = \type => fst type
element : (type : TypeData) -> (x : index type) -> Set
element = \type => snd type
Value : (type : TypeData) -> Set
Value = \type => (x : index type) ** element type x
Equality : (left : TypeData) -> (right : TypeData) -> Prop
Equality = \left => \right =>
(indexEquality : index left ~ index right) **
(x : index left) ->
element left x ~ element right (cast (index left) (index right) indexEquality x)
Cast :
(oldType : TypeData) ->
(newType : TypeData) ->
(equality : Equality oldType newType) ->
(value : Value oldType) ->
Value newType
Cast = \oldType => \newType => \equality => \value =>
< cast (index oldType) (index newType) (fst equality) (fst value)
, cast
(element oldType (fst value))
(element newType (cast (index oldType) (index newType) (fst equality) (fst value)))
(snd equality (fst value))
(snd value)
>
EqualityCorrect :
(left : TypeData) ->
(right : TypeData) ->
Equality left right ~ (Value left ~ Value right)
EqualityCorrect = refl Equality
CastCorrect :
(oldType : TypeData) ->
(newType : TypeData) ->
(equality : Equality oldType newType) ->
(value : Value oldType) ->
Cast oldType newType equality value ~
cast (Value oldType) (Value newType) (fst (EqualityCorrect oldType newType) equality) value
CastCorrect = refl Cast
|
