The difference between boolean equality and type-level equality in Formality

equality.fm.c

// Equality with values
// ====================

// A Boolean is a set with two values
T Bool
| true;
| false;

// Boolean not is a function that receives a bool and returns a bool
bool_not(a: Bool): Bool
  case a:
  | false;
  | true;

// Boolean and is a function that receives 2 bools and returns a bool
bool_and(a: Bool, b: Bool): Bool
  case a:
  | case b:
    | false;
    | false;;
  | case b:
    | false;
    | true;;

// Boolean or is a function that receives 2 bools and returns a bool
bool_or(a: Bool, b: Bool): Bool
  case a:
  | case b:
    | false;
    | false;;
  | case b:
    | false;
    | true;;

// Boolean equal is a function that receives 2 bools and returns a bool
// The compiler doesn't connect it to the concept of "equality" because it could
// be any other `Bool -> Bool -> Bool` function. It can't use it for rewrites.
bool_equal(a: Bool, b: Bool): Bool
  case a:
  | case b:
    | true;
    | false;;
  | case b:
    | false;
    | true;;

// This is just the boolean "true"
bool_true_is_true: Bool
  bool_equal(true, true)

// This is just the boolean "false"
bool_true_is_false: Bool
  bool_equal(true, false)

// This is just the boolean "false"
bool_false_is_true: Bool
  bool_equal(false, true)

// This is just the boolean "true"
bool_false_is_false: Bool
  bool_equal(false, false)

// ...

// Equality with types
// ===================

// Type-level False is represented by an empty type (Empty on Prelude.fm).
T False

// Type-level True is represented by a non-empty type (Unit on Prelude.fm).
T True
| truth;

// Type-level Not is a function from a type `A` to the empty type (False).
Not(A: Type): Type
  A -> False

// Type-level And is just a pair (Pair on Prelude.fm).
T And<A: Type, B: Type>
| and(a: A, b: B);

// Type-level Or is just an either (Either on Prelude.fm).
T Or<A: Type, B: Type>
| or_a(a: A);
| or_b(b: B);

// Type-level Equal is a datatype with two indices assigned to the same var.
// This is the information the compiler needs to learn the concept of equality.
//      \/ polymorphic on a type A
T Equal<A: Type> ~ (a: A, b: A) // <- with two indices
| same<a: A> ~ (a, a); // <- both indices assigned to the same variable `a`

// Note:, now I see the problem with explaining the Equal type (and, thus, how
// it is different from an Equal function). The user must know how indexed
// datatypes work first. Once he does, Equal(A,a,b) becomes much clearer.

// Since the Equal type teaches the compiler the notion of sameness, we can use
// it to implement "rewrite", which converts `a` to `b` inside a type, as long as
// `a == b`. For example, if we have `vec : Vector(Nat, 3 + x)`, we can use it
// to convert it to `vec : Vector(Nat, x + 3)` (if we prove `3 + x == x + 3`).
Equal.rewrite<A: Type, a: A, b: A, P: A -> Type>(e: Equal(A,a,b)): P(a) -> P(b)
  case e:
  | (x) x;
  : P(e.a) -> P(e.b);

// A proof that true == true is the constructor same applied to true
true_is_true: Equal(Bool, true, true)
  same<Bool, true>

// A proof that false == false is the constructor same applied to false
false_is_false: Equal(Bool, false, false)
  same<Bool, false>

// A proof that true == false is a function that receives `tf: true == false`.
// It returns `truth : if true then True else False`, and uses `tf` to rewrite
// `true` by `false` on that type, resulting in `truth : False`.
true_isnt_false: Not(Equal(Bool, true, false))
  (tf) Equal.rewrite<_, true, false, (x) if x then True else False>(tf, truth)

// A proof that false == true is a function like the one above.
false_isnt_true: Not(Equal(Bool, false, true))
  (tf) Equal.rewrite<_, false, true, (x) if x then False else True>(tf, truth)

// A decision of A is either an element of A, or a proof that A is empty.
T Decision<A: Type>
| Decision.yep(proof: A);
| Decision.nop(proof: Not(A));

// A logical equality function is a function that receives 2 bools, and returns
// either a proof that `a == b` or `a != b`, depending on their values.
Compare(a: Bool, b: Bool): Decision(Equal(Bool, a,b))
  case a:
  | case b:
    | Decision.yep<>(true_is_true);
    | Decision.nop<>(true_isnt_false);
    : Decision(Equal(Bool, true, b.self));;
  | case b:
    | Decision.nop<>(false_isnt_true);
    | Decision.yep<>(false_is_false);
    : Decision(Equal(Bool, false, b.self));;
  : Decision(Equal(Bool, a.self, b));

Tabularised, to make it easier to compare them.