Unions of subtypes
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Louis Wasserman and Maša Žaucer.
Created on 2022-09-09.
Last modified on 2025-10-14.
module foundation.unions-subtypes where
Imports
open import foundation.decidable-subtypes open import foundation.dependent-pair-types open import foundation.disjunction open import foundation.empty-subtypes open import foundation.function-types open import foundation.functoriality-disjunction open import foundation.identity-types open import foundation.large-locale-of-subtypes open import foundation.powersets open import foundation.propositional-truncations open import foundation.raising-universe-levels open import foundation.similarity-subtypes open import foundation.subtypes open import foundation.universe-levels open import logic.de-morgan-propositions open import logic.de-morgan-subtypes open import logic.double-negation-stable-subtypes open import order-theory.least-upper-bounds-large-posets
Idea
The union of two subtypes A
and B
is the
subtype that contains the elements that are in A
or in B
.
Definition
Unions of subtypes
module _ {l l1 l2 : Level} {X : UU l} where union-subtype : subtype l1 X → subtype l2 X → subtype (l1 ⊔ l2) X union-subtype P Q x = (P x) ∨ (Q x)
Unions of decidable subtypes
union-decidable-subtype : decidable-subtype l1 X → decidable-subtype l2 X → decidable-subtype (l1 ⊔ l2) X union-decidable-subtype P Q x = disjunction-Decidable-Prop (P x) (Q x)
Unions of De Morgan subtypes
union-de-morgan-subtype : de-morgan-subtype l1 X → de-morgan-subtype l2 X → de-morgan-subtype (l1 ⊔ l2) X union-de-morgan-subtype P Q x = disjunction-De-Morgan-Prop (P x) (Q x)
Unions of families of subtypes
module _ {l1 l2 l3 : Level} {X : UU l1} where union-family-of-subtypes : {I : UU l2} (A : I → subtype l3 X) → subtype (l2 ⊔ l3) X union-family-of-subtypes = sup-powerset-Large-Locale is-least-upper-bound-union-family-of-subtypes : {I : UU l2} (A : I → subtype l3 X) → is-least-upper-bound-family-of-elements-Large-Poset ( powerset-Large-Poset X) ( A) ( union-family-of-subtypes A) is-least-upper-bound-union-family-of-subtypes = is-least-upper-bound-sup-powerset-Large-Locale
Properties
The union of families of subtypes preserves indexed inclusion
module _ {l1 l2 l3 l4 : Level} {X : UU l1} {I : UU l2} (A : I → subtype l3 X) (B : I → subtype l4 X) where preserves-order-union-family-of-subtypes : ((i : I) → A i ⊆ B i) → union-family-of-subtypes A ⊆ union-family-of-subtypes B preserves-order-union-family-of-subtypes H x p = apply-universal-property-trunc-Prop p ( union-family-of-subtypes B x) ( λ (i , q) → unit-trunc-Prop (i , H i x q))
The union operation is associative
abstract associative-union-subtype : {l1 l2 l3 l4 : Level} {X : UU l1} (S : subtype l2 X) (T : subtype l3 X) (U : subtype l4 X) → union-subtype (union-subtype S T) U = union-subtype S (union-subtype T U) associative-union-subtype S T U = eq-has-same-elements-subtype _ _ ( λ x → (right-associate-disjunction , left-associate-disjunction))
The union operation is commutative
abstract commutative-union-subtype : {l1 l2 l3 : Level} {X : UU l1} (S : subtype l2 X) (T : subtype l3 X) → union-subtype S T = union-subtype T S commutative-union-subtype S T = eq-has-same-elements-subtype _ _ ( λ s → (swap-disjunction , swap-disjunction))
The union operation is idempotent
abstract idempotent-union-subtype : {l1 l2 : Level} {X : UU l1} (S : subtype l2 X) → union-subtype S S = S idempotent-union-subtype S = eq-has-same-elements-subtype _ _ ( λ x → (elim-disjunction (S x) id id , inl-disjunction))
The empty subtype is an identity for the union operation
abstract left-unit-law-union-subtype : {l1 l2 : Level} {X : UU l1} (S : subtype l2 X) → union-subtype (empty-subtype lzero X) S = S left-unit-law-union-subtype {X = X} S = eq-has-same-elements-subtype _ _ ( λ s → ( map-left-unit-law-disjunction-is-empty-Prop ( empty-subtype _ X s) ( S s) ( is-empty-subtype-empty-subtype X s) , inr-disjunction)) right-unit-law-union-subtype : {l1 l2 : Level} {X : UU l1} (S : subtype l2 X) → union-subtype S (empty-subtype lzero X) = S right-unit-law-union-subtype S = ( commutative-union-subtype S (empty-subtype lzero _)) ∙ ( left-unit-law-union-subtype S)
The union operation preserves similarity of subtypes
abstract preserves-sim-union-subtype : {l1 l2 l3 l4 l5 : Level} {X : UU l1} → (S : subtype l2 X) (T : subtype l3 X) → sim-subtype S T → (U : subtype l4 X) (V : subtype l5 X) → sim-subtype U V → sim-subtype (union-subtype S U) (union-subtype T V) preserves-sim-union-subtype _ _ (S⊆T , T⊆S) _ _ (U⊆V , V⊆U) = ( ( λ x → map-disjunction (S⊆T x) (U⊆V x)) , ( λ x → map-disjunction (T⊆S x) (V⊆U x)))
Recent changes
- 2025-10-14. Fredrik Bakke. Some small logic additions (#1585).
- 2025-10-12. Louis Wasserman. Large monoids (#1587).
- 2025-01-07. Fredrik Bakke. Logic (#1226).
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 2023-12-12. Fredrik Bakke. Some minor refactoring surrounding Dedekind reals (#983).