Transport rigid structures over a monoidal equivalence. #

Given candidate data for an exact pairing, which is sent by a faithful monoidal functor to an exact pairing, the equations holds automatically.

Instances For

    Given a pair of objects which are sent by a fully faithful functor to a pair of objects with an exact pairing, we get an exact pairing.

    Instances For