The current theory allows to work with a surjective pairing as opposed to a perfect (i.e. bijective) one. This is relevant, because with requring a perfect pairing the theory necessarily collapses back to finite dimensions. While IsPerfPair is currently available as a typeclass, Injective is not, and so it is now clear in how far (or how quickly) this can be achieved. Note that Dual.eval is an injective pairing.
The current theory allows to work with a surjective pairing as opposed to a perfect (i.e. bijective) one. This is relevant, because with requring a perfect pairing the theory necessarily collapses back to finite dimensions. While
IsPerfPairis currently available as a typeclass,Injectiveis not, and so it is now clear in how far (or how quickly) this can be achieved. Note thatDual.evalis an injective pairing.