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 2026-02-04.

module foundation.unions-subtypes where
Imports 
open import foundation.coproduct-types
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.surjective-maps
open import foundation.type-arithmetic-coproduct-types
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)))

The surjection from S + T to S ∪ T

module _
  {l1 l2 l3 : Level}
  {A : UU l1}
  (S : subtype l2 A)
  (T : subtype l3 A)
  where

  surjection-coproduct-union-subtype :
    (type-subtype S + type-subtype T) ↠ type-subtype (union-subtype S T)
  surjection-coproduct-union-subtype =
    comp-surjection
      ( surjection-tot
        ( λ a →
          surjection-unit-trunc-Prop (is-in-subtype S a + is-in-subtype T a)))
      ( surjection-equiv inv-left-distributive-Σ-coproduct)

Recent changes