A library of monadic typed keys which can be compared for equality, returning an equality proof if equal. See http://dx.doi.org/10.1145/2976002.2976008 The authors of the cited document and of this package are disjoint.