The Clowder Project

In detail, the right tensor product of $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ is the pointed set $\webleft (X\rhd Y,\webleft [y_{0}\webright ]\webright )$ consisting of:

• The Underlying Set. The set $X\rhd Y$ defined by
  \begin{align*} X\rhd Y & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\lvert X\right\rvert \odot Y\\ & \cong \bigvee _{x\in X}\webleft (Y,y_{0}\webright ), \end{align*}

  where $\left\lvert X\right\rvert $ denotes the underlying set of $\webleft (X,x_{0}\webright )$.

• The Underlying Basepoint. The point $\webleft [\webleft (x_{0},y_{0}\webright )\webright ]$ of $\bigvee _{x\in X}\webleft (Y,y_{0}\webright )$, which is equal to $\webleft [\webleft (x,y_{0}\webright )\webright ]$ for any $x\in X$.