Theorem. Isomorphisms with lifting [dt-003L]

With the lifting operator, we can relate the lazy constructions like product and sum with strict constructions like smash product and sum via isomorphism:

  • A\twoheadrightarrow B \simeq A_\bot \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B
  • A + B \simeq A_\bot \oplus B_\bot
  • (A \times B)_\bot \simeq A_\bot \otimes B_\bot