transpose(Correspondence) -- reverse the direction of a correspondence

Synopsis

• Function: transpose

• Usage:

  transpose I

• Inputs:
  • I, an instance of the type Correspondence, from $X$ to $Y$
• Outputs:
  • J, an instance of the type Correspondence, from $Y$ to $X$, such that $J_* = I^*$ and $J^* = I_*$. In the case of an IncidenceCorrespondence, the intermediates are also carried along appropriately, that is, if intermediates I is the tuple $(Z,f,g)$, then intermediates J is the tuple $(Z,g,f)$.