Smash Product of Pointed Types

The binary smash product X ∧ Y 𝑋 𝑌 X\wedge Y of two Pointed Types X , Y : 𝖴 ∙ X,Y:\mathsf{U}{}_{\bullet} is given by quotienting X × Y 𝑋 𝑌 X\times Y via the Equivalence Relation relation generated by ( x , ∙ ) ∼ ( ∙ , y ) similar-to 𝑥 ∙ ∙ 𝑦 (x,\bullet)\sim(\bullet,y) .