Correspondence * Correspondence -- composition of correspondences

• Operator: *

• Usage:

  J * I

• Inputs:
  • I, an instance of the type Correspondence, from $X$ to $Y$
  • J, an instance of the type Correspondence, from $Y$ to $Z$
• Outputs:
  • K, an instance of the type Correspondence, from $X$ to $Z$, such that $K_* = J_* I_*$ and $K^* = I^* J^*$