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