nLab cartesian product of A-sets

 Definition

Given two $\mathcal{A}$-sets $A$ and $B$, the cartesian product $A \times 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 \times B} (c, d) \coloneqq (a \sim_A c) \wedge (b \sim_B d)$$

$$(a, b) \nsim_{A \times B} (c, d) \coloneqq (a \nsim_A c) \vee (b \nsim_B d)$$

Given a family of $\mathcal{A}$-sets $(B(x))_{x:A}$ indexed by a type $A$, the indexed cartesian product $\prod_{x:A} B(x)$ of $(B(x))_{x:A}$ is given by an $\mathcal{A}$-set structure on the underlying dependent product type $\prod_{x:A} B(x)$ defined by

$$c \sim_{\prod_{x:A} B(x)} d \coloneqq \forall x:A.c(x) \sim_{B(x)} d(x)$$

$$c \nsim_{\prod_{x:A} B(x)} d \coloneqq \exists x:A.c(x) \nsim_{B(x)} d(x)$$

Related concepts

• A-set

• cartesian product

• tensor 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)