Union of subtypes

module foundation.unions-subtypes where

open import foundation.decidable-subtypes
open import foundation.disjunction
open import foundation.large-locale-of-subtypes

open import foundation-core.subtypes
open import foundation-core.universe-levels

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 = disj-Prop (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 = disj-Decidable-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-power-set-Large-Locale