Unions of subtypes

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

Created on 2022-09-09.
Last modified on 2024-04-11.

module foundation.unions-subtypes where
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


The union of two subtypes A and B is the subtype that contains the elements that are in A or in B.


Unions of subtypes

module _
  {l l1 l2 : Level} {X : UU l}

  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}

  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) 
      ( powerset-Large-Poset X)
      ( A)
      ( union-family-of-subtypes A)
  is-least-upper-bound-union-family-of-subtypes =


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)

  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))

Recent changes