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