Leibniz

(A === B) is a supertype of Leibniz[L,H,A,B]

Unsafe coercion between types. force abuses asInstanceOf to explicitly coerce types. It is unsafe, but needed where Leibnizian equality isn't sufficient

We can lift equality into any type constructor

We can lift equality into any type constructor

We can lift equality into any type constructor

Emir Pasalic's PhD thesis mentions that it is unknown whether or not ((A,B) === (C,D)) => (A === C) is inhabited.

Haskell can work around this issue by abusing type families as noted in Leibniz equality can be injective (Oleg Kiselyov, Haskell Cafe Mailing List 2010) but we instead turn to force.

Equality is symmetric

Equality is transitive

Equality is reflexive -- we rely on subtyping to expand this type

We can witness equality by using it to convert between types We rely on subtyping to enable this to work for any Leibniz arrow