postulate TypeData : Set 1
postulate Value : (type : TypeData) -> Set
postulate Equality : (left : TypeData) -> (right : TypeData) -> Prop
postulate Cast :
  (oldType : TypeData) ->
  (newType : TypeData) ->
  (equality : Equality oldType newType) ->
  (value : Value oldType) ->
  Value newType

postulate EqualityCorrect :
  (left : TypeData) ->
  (right : TypeData) ->
  Equality left right ~ (Value left ~ Value right)

postulate 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