{-# OPTIONS --without-K #-}
open import elementary-number-theory.natural-numbers
open import foundation.booleans
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-truncation
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.truncations
open import foundation.truncation-levels
renaming (truncation-level-minus-one-ℕ to minus-one)
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels
open import e-structure.core
open import notation as N
module e-structure.property.union
{i j} (((M , _∈_) , p) : ∈-structure i j) where
[_]-Union : ℕ → UU (i ⊔ j)
[ n ]-Union = (x : M)
→ Σ M λ ⋃x → (z : M) → (z ∈ ⋃x) ≃ type-trunc (minus-one n) (Σ M λ y → (z ∈ y) × (y ∈ x))
∞-Union : UU (i ⊔ j)
∞-Union = (x : M) →
Σ M λ ⨆x → (z : M) → (z ∈ ⨆x) ≃ Σ M λ y → (z ∈ y) × (y ∈ x)
Binary-[_]-Union : ℕ → UU (i ⊔ j)
Binary-[ n ]-Union = (x y : M)
→ Σ M λ x∪y → (z : M) → (z ∈ x∪y) ≃ type-trunc (minus-one n) ((z ∈ x) + (z ∈ y))
Binary-0-Union : UU (i ⊔ j)
Binary-0-Union = Binary-[ zero-ℕ ]-Union
Binary-∞-Union : UU (i ⊔ j)
Binary-∞-Union = (x y : M)
→ Σ M λ x∪y → (z : M) → (z ∈ x∪y) ≃ ((z ∈ x) + (z ∈ y))
open import e-structure.property.unordered-tupling ((M , _∈_) , p)
module binary {n : ℕ} where
module notation (binary-union : Binary-[ n ]-Union) where
_∪_ : M → M → M
x ∪ y = pr1 (binary-union x y)
module from-unordered-pairs
(union : [ n ]-Union)
(unordered-pairs : [ n ]-UnorderedPairs) where
open unordered-pairs.notation unordered-pairs
binary-union-set : M → M → M
binary-union-set x y = pr1 (union ｛ x ,, y ｝)
∈-binary-union : (x y z : M)
→ (z ∈ (binary-union-set x y))
≃ type-trunc (minus-one n) ((z ∈ x) + (z ∈ y))
∈-binary-union x y z =
equivalence-reasoning
z ∈ (binary-union-set x y)
≃ type-trunc (minus-one n)
(Σ M (λ u → (z ∈ u) × (u ∈ ｛ x ,, y ｝))) by pr2 (union ｛ x ,, y ｝) z
≃ type-trunc (minus-one n)
(Σ M (λ u → (z ∈ u) ×
(type-trunc (minus-one n) ((x == u) + (y == u))))) by equiv-trunc (minus-one n)
(equiv-tot (λ u →
equiv-tot (λ _ →
pr2 (unordered-pairs x y) u)))
≃ type-trunc (minus-one n)
(Σ M (λ u → type-trunc (minus-one n)
((z ∈ u) ×
type-trunc (minus-one n) ((x == u) + (y == u))))) by equiv-trunc-Σ (minus-one n)
≃ type-trunc (minus-one n)
(Σ M (λ u → type-trunc (minus-one n)
((z ∈ u) × ((x == u) + (y == u))))) by equiv-trunc (minus-one n)
(equiv-tot (λ u →
inv-equiv-trunc-Σ (minus-one n)))
≃ type-trunc (minus-one n)
(Σ M (λ u → (z ∈ u) × ((x == u) + (y == u)))) by inv-equiv-trunc-Σ (minus-one n)
≃ type-trunc (minus-one n)
(Σ M (λ u →
((z ∈ u) × (x == u)) + ((z ∈ u) × (y == u)))) by equiv-trunc (minus-one n)
(equiv-tot (λ u →
left-distributive-prod-coprod _ _ _))
≃ type-trunc (minus-one n)
(Σ M (λ u → (z ∈ u) × (x == u)) +
Σ M (λ u → (z ∈ u) × (y == u))) by equiv-trunc (minus-one n)
(left-distributive-Σ-coprod _ _ _)
≃ type-trunc (minus-one n)
(Σ (Σ M λ u → x == u) (λ (u , _) → z ∈ u) +
Σ (Σ M λ u → y == u) (λ (u , _) → z ∈ u)) by equiv-trunc (minus-one n)
(equiv-coprod
(inv-associative-Σ' _ _ _ ∘e equiv-tot (λ u → commutative-prod))
(inv-associative-Σ' _ _ _ ∘e equiv-tot (λ u → commutative-prod)))
≃ type-trunc (minus-one n) ((z ∈ x) + (z ∈ y)) by equiv-trunc (minus-one n)
(equiv-coprod
(left-unit-law-Σ-is-contr
(is-torsorial-path x)
(x , refl))
(left-unit-law-Σ-is-contr
(is-torsorial-path y)
(y , refl)))
binary-union : Binary-[ n ]-Union
pr1 (binary-union x y) = binary-union-set x y
pr2 (binary-union x y) = ∈-binary-union x y
open notation binary-union public
module ∞-binary where
module notation (binary-∞-union : Binary-∞-Union) where
_∞-∪_ : M → M → M
x ∞-∪ y = pr1 (binary-∞-union x y)
module from-∞-unordered-pairs
(∞-union : ∞-Union)
(∞-unordered-pairs : ∞-UnorderedPairs) where
open ∞-unordered-pairs.notation ∞-unordered-pairs
binary-∞-union-set : M → M → M
binary-∞-union-set x y = pr1 (∞-union [ x ,, y ])
∈-binary-∞-union : (x y z : M)
→ (z ∈ (binary-∞-union-set x y))
≃ ((z ∈ x) + (z ∈ y))
∈-binary-∞-union x y z =
equivalence-reasoning
z ∈ (binary-∞-union-set x y)
≃ Σ M (λ u → (z ∈ u) × (u ∈ [ x ,, y ])) by pr2 (∞-union [ x ,, y ]) z
≃ Σ M (λ u → (z ∈ u) × ((x == u) + (y == u))) by equiv-tot (λ u →
equiv-tot (λ _ →
pr2 (∞-unordered-pairs x y) u))
≃ Σ M (λ u →
((z ∈ u) × (x == u)) + ((z ∈ u) × (y == u))) by equiv-tot (λ u →
left-distributive-prod-coprod _ _ _)
≃ Σ M (λ u → (z ∈ u) × (x == u)) +
Σ M (λ u → (z ∈ u) × (y == u)) by left-distributive-Σ-coprod _ _ _
≃ Σ (Σ M λ u → x == u) (λ (u , _) → z ∈ u) +
Σ (Σ M λ u → y == u) (λ (u , _) → z ∈ u) by equiv-coprod
(inv-associative-Σ' _ _ _ ∘e equiv-tot (λ u → commutative-prod))
(inv-associative-Σ' _ _ _ ∘e equiv-tot (λ u → commutative-prod))
≃ (z ∈ x) + (z ∈ y) by equiv-coprod
(left-unit-law-Σ-is-contr
(is-torsorial-path x)
(x , refl))
(left-unit-law-Σ-is-contr
(is-torsorial-path y)
(y , refl))
binary-∞-union : Binary-∞-Union
pr1 (binary-∞-union x y) = binary-∞-union-set x y
pr2 (binary-∞-union x y) = ∈-binary-∞-union x y
open notation binary-∞-union public