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