blob: 6364e2d683e25979d24430025c12438f72561806 (
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
|
TypeData : Set 1
TypeData = (domain : Set) ** (x : domain) -> Set
domain : (type : TypeData) -> Set
domain = \type => fst type
codomain : (type : TypeData) -> (x : domain type) -> Set
codomain = \type => snd type
Value : (type : TypeData) -> Set
Value = \type => (x : domain type) -> codomain type x
Equality : (left : TypeData) -> (right : TypeData) -> Prop
Equality = \left => \right =>
(domainEquality : domain right ~ domain left) **
(x : domain right) ->
codomain left (cast (domain right) (domain left) domainEquality x) ~ codomain right x
Cast :
(oldType : TypeData) ->
(newType : TypeData) ->
(equality : Equality oldType newType) ->
(value : Value oldType) ->
Value newType
Cast = \oldType => \newType => \equality => \value =>
\x =>
cast
(codomain oldType (cast (domain newType) (domain oldType) (fst equality) x))
(codomain newType x)
(snd equality x)
(value (cast (domain newType) (domain oldType) (fst equality) x))
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
|
