nLab tensor product of A-sets

 Definition

Given two $\mathcal{A}$-sets $A$ and $B$, the tensor product $A \otimes B$ of $A$ and $B$ is given by an $\mathcal{A}$-set structure on the underlying product type $A \times B$ defined by

$$(a, b) \sim_{A \otimes B} (c, d) \coloneqq (a \sim_A c) \wedge (b \sim_B d)$$

$$(a, b) \nsim_{A \otimes B} (c, d) \coloneqq \left((a \sim_A c) \to (b \nsim_B d)\right) \wedge \left((b \sim_B d) \to (a \nsim_A c)\right)$$

Related concepts

• A-set

• tensor product

• cartesian product of A-sets

 References

• Michael Shulman, Affine logic for constructive mathematics. Bulletin of Symbolic Logic, Volume 28, Issue 3, September 2022. pp. 327 - 386 (doi:10.1017/bsl.2022.28, arXiv:1805.07518)