# Unions of subtypes

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Maša Žaucer.

Created on 2022-09-09.

module foundation.unions-subtypes where

Imports
open import foundation.decidable-subtypes
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.large-locale-of-subtypes
open import foundation.powersets
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.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 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))