[[!redirects Sandbox &gt; history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] We need to figure out what properties of exclusive disjunction still hold constructively. Exclusive disjunction is defined as $$A \oplus B \coloneqq \sum_{x:A + B} \prod_{y:A + B} \mathrm{Id}_{A + B} (x + y)$$ Is exclusive disjunction still associative and commutative? $$((A \oplus B) \oplus C) \simeq (A \oplus (B \oplus C))$$ $$(A \oplus B) \simeq (B \oplus A)$$ Does conjunction still distribute over exclusive disjunction: $$(A \times (B \oplus C)) \simeq ((A \oplus B) \times (A \times C))$$ category: redirected to nlab