Equal.fm

// The Equal datatype.
T Equal <A: Type> (a: A) ~ (b: A)
| Equal.to               ~ (a);

// Applies a function to both sides of an equality
Equal.apply<A: Type, B: Type, a: A, b: A, f: A -> B>(e: Equal(A,a,b)): Equal(B, f(a), f(b))
  case e:
  | Equal.to<B, f(a)>;
  : Equal(B, f(a), f(e.b));

// If a == b and b == c, then a == c
Equal.chain<A: Type, a: A, b: A, c: A>(d: Equal(A,a,b), e: Equal(A,b,c)): Equal(A,a,c)
  case e:
  | d;
  : Equal(A, a, e.b);

// If a == b, then b == a
Equal.mirror<A: Type, a: A, b: A>(e: Equal(A,a,b)): Equal(A,b,a)
  case e:
  | Equal.to<A, a>;
  : Equal(A, e.b, a);

// If a == b, then, P(a) implies P(b)
Equal.rewrite<A: Type, a: A, b: A, P: A -> Type>(e: Equal(A,a,b), x: P(a)): P(b)
  case e:
  | x;
  : P(e.b);
  
// If a == x and b == x, then a == b
Equal.left<A: Type, x: A, a: A, b: A>(r: Equal(A, a, x), s: Equal(A, b, x))
: Equal(A, a, b)
  Equal.chain<A, a, x, b>(r, Equal.mirror<A, b, x>(s))

// If x == a and x == b, then a == b
Equal.right<A: Type, x: A, a: A, b: A>(r: Equal(A, x, a), s: Equal(A, x, b))
: Equal(A, a, b)
  Equal.chain<A, a, x, b>(Equal.mirror<A, x, a>(r), s)

// Erased rewrite
Equal.cast<A: Type, a: A, b: A, P: A -> Type, e: Equal(A,a,b)>(x: P(a)): P(b)
  case e:
  | x;
  : P(e.b);

Equal.applyd<A: Type, B: A -> Type, a: A, b: A>(f: (x: A) -> B(x), e: Equal(A, a, b))
  : Equal(B(a), f(a), Equal.rewrite<A,b,a,B>(Equal.mirror<A,a,b>(e))(f(b)))
  case e:
  | Equal.to<B(a)><f(a)>;
  : Equal(B(a), f(a), Equal.rewrite<A,e.b,a,B>(Equal.mirror<A,a,e.b>(e.self),f(e.b)));