diff options
Diffstat (limited to 'examples/equality/Universe.obs')
| -rw-r--r-- | examples/equality/Universe.obs | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/examples/equality/Universe.obs b/examples/equality/Universe.obs new file mode 100644 index 0000000..19a8408 --- /dev/null +++ b/examples/equality/Universe.obs @@ -0,0 +1,31 @@ +TypeData : Prop +TypeData = () + +Value : (type : TypeData) -> Set 1 +Value = \type => Set + +Equality : (left : TypeData) -> (right : TypeData) -> Prop +Equality = \left => \right => () + +Cast : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Value newType +Cast = \oldType => \newType => \equality => \value => 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 |