Martin Escardo, 5th September 2018. Modified 27 September 2023 to
support the object of truth values to live in a different universe
than that of which the powerset is taken.


Univalence gives the usual mathematical notion of equality for the
subsets of a type: two subsets of a type are equal precisely when they
have the same elements, like in ZF (C). And *not* when they are
isomorphic, for any reasonable notion of isomorphism between subsets
of a given type.

A subset of a type X in a universe 𝓀 is an embedding of some given
type into X, or, equivalently, a map of X into the subtype classifier
Ξ© 𝓀 of the universe 𝓀 (see the module UF.Classifiers).

We generalize this to allow the powerset to have values in Ξ© π“₯. The
module UF.Powerset specializes this module to the case 𝓀=π“₯.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module UF.Powerset-MultiUniverse where

open import MLTT.Spartan
open import UF.FunExt
open import UF.Lower-FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties
open import UF.UA-FunExt
open import UF.Univalence

π“Ÿ : {π“₯ 𝓀 : Universe} β†’ 𝓀 Μ‡ β†’ 𝓀 βŠ” (π“₯ ⁺) Μ‡
π“Ÿ {π“₯} {𝓀} X = X β†’ Ξ© π“₯

powersets-are-sets'' : funext 𝓀 (π“₯ ⁺)
                     β†’ funext π“₯ π“₯
                     β†’ propext π“₯
                     β†’ {X : 𝓀 Μ‡ } β†’ is-set (π“Ÿ {π“₯} X)
powersets-are-sets'' fe fe' pe = Ξ -is-set fe (Ξ» x β†’ Ξ©-is-set fe' pe)

powersets-are-sets : funext π“₯ (π“₯ ⁺)
                   β†’ propext π“₯
                   β†’ {X : π“₯ Μ‡ } β†’ is-set (X β†’ Ξ© π“₯)
powersets-are-sets {π“₯} fe = powersets-are-sets'' fe (lower-funext π“₯ (π“₯ ⁺) fe)

π“Ÿ-is-set' : funext 𝓀 (𝓀 ⁺)
          β†’ propext 𝓀
          β†’ {X : 𝓀 Μ‡ }
          β†’ is-set (π“Ÿ {𝓀} X)
π“Ÿ-is-set' = powersets-are-sets

π“Ÿ-is-set : Univalence
         β†’ {X : 𝓀 Μ‡ }
         β†’ is-set (π“Ÿ X)
π“Ÿ-is-set {𝓀} ua = π“Ÿ-is-set'
                    (univalence-gives-funext' 𝓀 (𝓀 ⁺) (ua 𝓀) (ua (𝓀 ⁺)))
                    (univalence-gives-propext (ua 𝓀))

comprehension : (X : 𝓀 Μ‡ ) β†’ π“Ÿ {π“₯} X β†’ π“Ÿ {π“₯} X
comprehension X A = A

syntax comprehension X (Ξ» x β†’ A) = ⁅ x κž‰ X ∣ A ⁆

βˆ… : {X : 𝓀 Μ‡ } β†’  π“Ÿ {π“₯} X
βˆ… _ = 𝟘 , 𝟘-is-prop

full : {X : 𝓀 Μ‡ } β†’  π“Ÿ {π“₯} X
full _ = πŸ™ , πŸ™-is-prop

_βˆˆβ‚š_ : {X : 𝓀  Μ‡} β†’ X β†’ (X β†’ Ξ© π“₯) β†’ Ξ© π“₯
x βˆˆβ‚š A = A x

_∈_ : {X : 𝓀 Μ‡ } β†’ X β†’ π“Ÿ {π“₯} X β†’ π“₯ Μ‡
x ∈ A =  x βˆˆβ‚š A holds

_βˆ‰_ : {X : 𝓀 Μ‡ } β†’ X β†’ π“Ÿ {π“₯} X β†’ π“₯ Μ‡
x βˆ‰ A = Β¬ (x ∈ A)

is-empty-subset : {X : 𝓀 Μ‡ } β†’ π“Ÿ {π“₯} X β†’ 𝓀 βŠ” π“₯ Μ‡
is-empty-subset {𝓀} {π“₯} {X} A = (x : X) β†’ x βˆ‰ A

being-empty-subset-is-prop : Fun-Ext
                           β†’ {X : 𝓀 Μ‡ } (A : π“Ÿ {π“₯} X)
                           β†’ is-prop (is-empty-subset A)
being-empty-subset-is-prop fe {X} A = Ξ -is-prop fe (Ξ» x β†’ negations-are-props fe)

are-disjoint : {X : 𝓀 Μ‡ } β†’ π“Ÿ {π“₯} X β†’ π“Ÿ {𝓦} X β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
are-disjoint {𝓀} {π“₯} {𝓦} {X} A B = (x : X) β†’ Β¬((x ∈ A) Γ— (x ∈ B))

being-disjoint-is-prop : Fun-Ext
                       β†’ {X : 𝓀 Μ‡ } (A : π“Ÿ {π“₯} X) (B : π“Ÿ {𝓦} X)
                       β†’ is-prop (are-disjoint A B)
being-disjoint-is-prop fe A B = Ξ -is-prop fe (Ξ» _ β†’ negations-are-props fe)

_βŠ†_ _βŠ‡_ : {X : 𝓀 Μ‡ } β†’ π“Ÿ {π“₯} X β†’ π“Ÿ {𝓦} X β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
A βŠ† B = βˆ€ x β†’ x ∈ A β†’ x ∈ B
A βŠ‡ B = B βŠ† A

∈-is-prop : {X : 𝓀 Μ‡ } (A : π“Ÿ {π“₯} X) (x : X) β†’ is-prop (x ∈ A)
∈-is-prop A x = holds-is-prop (A x)

βˆ‰-is-prop : funext π“₯ 𝓀₀ β†’ {X : 𝓀 Μ‡ } (A : π“Ÿ {π“₯} X) (x : X) β†’ is-prop (x βˆ‰ A)
βˆ‰-is-prop fe A x = negations-are-props fe

module subset-complement (fe : Fun-Ext) where

 _βˆ–_ :  {X : 𝓀 Μ‡ } β†’ π“Ÿ {π“₯} X β†’ π“Ÿ {𝓦} X β†’ π“Ÿ {π“₯ βŠ” 𝓦} X
 A βˆ– B = Ξ» x β†’ (x ∈ A Γ— x βˆ‰ B) , Γ—-is-prop (∈-is-prop A x) (βˆ‰-is-prop fe B x)

 infix  45 _βˆ–_

 βˆ–-elimβ‚€ : {X : 𝓀 Μ‡ } (A : π“Ÿ {π“₯} X) (B : π“Ÿ {𝓦} X) {x : X} β†’ x ∈ A βˆ– B β†’ x ∈ A
 βˆ–-elimβ‚€ A B = pr₁

 βˆ–-elim₁ : {X : 𝓀 Μ‡ } (A : π“Ÿ {π“₯} X) (B : π“Ÿ {𝓦} X) {x : X} β†’ x ∈ A βˆ– B β†’ x βˆ‰ B
 βˆ–-elim₁ A B = prβ‚‚

module inhabited-subsets (pt : propositional-truncations-exist) where

 open PropositionalTruncation pt

 is-inhabited : {X : 𝓀 Μ‡ } β†’ π“Ÿ {π“₯} X β†’ 𝓀 βŠ” π“₯ Μ‡
 is-inhabited {𝓀} {π“₯} {X} A = βˆƒ x κž‰ X , x ∈ A

 being-inhabited-is-prop : {X : 𝓀 Μ‡ } (A : π“Ÿ {π“₯} X)
                         β†’ is-prop (is-inhabited A)
 being-inhabited-is-prop {𝓀} {π“₯} {X} A = βˆƒ-is-prop

 π“ŸβΊ : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
 π“ŸβΊ {𝓀} X = Ξ£ A κž‰ π“Ÿ X , is-inhabited A

 π“ŸβΊ-is-set' : funext 𝓀 (𝓀 ⁺) β†’ propext 𝓀 β†’ {X : 𝓀 Μ‡ } β†’ is-set (π“ŸβΊ X)
 π“ŸβΊ-is-set' fe pe {X} = subsets-of-sets-are-sets (π“Ÿ X)
                         is-inhabited
                         (π“Ÿ-is-set' fe pe)
                         (Ξ» {A} β†’ being-inhabited-is-prop A)

 π“ŸβΊ-is-set : Univalence β†’ {X : 𝓀 Μ‡ } β†’ is-set (π“ŸβΊ X)
 π“ŸβΊ-is-set {𝓀} ua = π“ŸβΊ-is-set'
                      (univalence-gives-funext' 𝓀 (𝓀 ⁺) (ua 𝓀) (ua (𝓀 ⁺)))
                      (univalence-gives-propext (ua 𝓀) )

 _∈⁺_ : {X : 𝓀 Μ‡ } β†’ X β†’ π“ŸβΊ X β†’ 𝓀 Μ‡
 x ∈⁺ (A , _) = x ∈ A

 _βˆ‰βΊ_ : {X : 𝓀 Μ‡ } β†’ X β†’ π“ŸβΊ X β†’ 𝓀 Μ‡
 x βˆ‰βΊ A = Β¬ (x ∈⁺ A)

 infix  40 _∈⁺_
 infix  40 _βˆ‰βΊ_

 open import UF.ClassicalLogic

 non-empty-subsets-are-inhabited : Excluded-Middle
                                 β†’ {X : 𝓀 Μ‡ } (B : π“Ÿ {π“₯} X)
                                 β†’ Β¬ is-empty-subset B
                                 β†’ is-inhabited B
 non-empty-subsets-are-inhabited em B = not-Ξ -not-implies-βˆƒ pt em

 uninhabited-subsets-are-empty : {X : 𝓀 Μ‡ } (B : π“Ÿ {π“₯} X)
                               β†’ Β¬ is-inhabited B
                               β†’ is-empty-subset B
 uninhabited-subsets-are-empty B ν x m = ν ∣ x , m ∣

complement :  {X : 𝓀 Μ‡ } β†’ funext 𝓀 𝓀₀ β†’ π“Ÿ X β†’ π“Ÿ X
complement fe A = Ξ» x β†’ (x βˆ‰ A) , (βˆ‰-is-prop fe A x)

βŠ†-is-prop' : funext 𝓀 π“₯
           β†’ funext π“₯ π“₯
           β†’ {X : 𝓀 Μ‡ } (A B : π“Ÿ {π“₯} X) β†’ is-prop (A βŠ† B)
βŠ†-is-prop' fe fe' A B = Ξ -is-prop fe
                         (Ξ» x β†’ Ξ -is-prop fe'
                         (Ξ» _ β†’ ∈-is-prop B x))

βŠ†-is-prop : funext 𝓀 𝓀
          β†’ {X : 𝓀 Μ‡ } (A B : π“Ÿ X) β†’ is-prop (A βŠ† B)
βŠ†-is-prop fe = βŠ†-is-prop' fe fe

module PropositionalSubsetInclusionNotation (fe : Fun-Ext) where

 _βŠ†β‚š_ _βŠ‡β‚š_ : {X : 𝓀  Μ‡} β†’ π“Ÿ {𝓀} X β†’ π“Ÿ {𝓀} X β†’ Ξ© 𝓀
 A βŠ†β‚š B = (A βŠ† B) , βŠ†-is-prop fe A B
 A βŠ‡β‚š B = (A βŠ‡ B) , βŠ†-is-prop fe B A

βˆ…-is-least' : {X : 𝓀 Μ‡ } (A : π“Ÿ {π“₯} X) β†’ βˆ… {𝓀} {π“₯} βŠ† A
βˆ…-is-least' _ x = 𝟘-induction

βˆ…-is-least : {X : 𝓀 Μ‡ } (A : π“Ÿ X) β†’ βˆ… {𝓀} {𝓀} βŠ† A
βˆ…-is-least = βˆ…-is-least'

βŠ†-refl' : {X : 𝓀 Μ‡ } (A : π“Ÿ {π“₯} X) β†’ A βŠ† A
βŠ†-refl' A x = id

βŠ†-refl : {X : 𝓀 Μ‡ } (A : π“Ÿ {π“₯} X) β†’ A βŠ† A
βŠ†-refl = βŠ†-refl'

βŠ†-trans' : {X : 𝓀 Μ‡ } (A B C : π“Ÿ {π“₯} X) β†’ A βŠ† B β†’ B βŠ† C β†’ A βŠ† C
βŠ†-trans' A B C s t x a = t x (s x a)

βŠ†-trans : {X : 𝓀 Μ‡ } (A B C : π“Ÿ {π“₯} X) β†’ A βŠ† B β†’ B βŠ† C β†’ A βŠ† C
βŠ†-trans = βŠ†-trans'

βŠ†-refl-consequence : {X : 𝓀 Μ‡ } (A B : π“Ÿ {π“₯} X)
                   β†’ A ＝ B β†’ (A βŠ† B) Γ— (B βŠ† A)

βŠ†-refl-consequence A A (refl) = βŠ†-refl A , βŠ†-refl A

subset-extensionality'' : propext π“₯
                        β†’ funext 𝓀 (π“₯ ⁺)
                        β†’ funext π“₯ π“₯
                        β†’ {X : 𝓀 Μ‡ } {A B : π“Ÿ {π“₯} X}
                        β†’ A βŠ† B β†’ B βŠ† A β†’ A ＝ B

subset-extensionality'' {π“₯} {𝓀} pe fe fe' {X} {A} {B} h k = dfunext fe Ο†
 where
  Ο† : (x : X) β†’ A x ＝ B x
  Ο† x = to-subtype-＝
           (Ξ» _ β†’ being-prop-is-prop fe')
           (pe (holds-is-prop (A x)) (holds-is-prop (B x))
               (h x) (k x))

subset-extensionality : propext 𝓀
                      β†’ funext 𝓀 (𝓀 ⁺)
                      β†’ {X : 𝓀 Μ‡ } {A B : π“Ÿ X}
                      β†’ A βŠ† B β†’ B βŠ† A β†’ A ＝ B

subset-extensionality {𝓀} pe fe = subset-extensionality'' pe fe (lower-funext 𝓀 (𝓀 ⁺) fe)

subset-extensionality' : Univalence
                       β†’ {X : 𝓀 Μ‡ } {A B : π“Ÿ X}
                       β†’ A βŠ† B β†’ B βŠ† A β†’ A ＝ B

subset-extensionality' {𝓀} ua = subset-extensionality
                                 (univalence-gives-propext (ua 𝓀))
                                 (univalence-gives-funext' 𝓀 (𝓀 ⁺) (ua 𝓀) (ua (𝓀 ⁺)))
\end{code}

Tom de Jong, 24 January 2022
(Based on code from FreeJoinSemiLattice.lagda written 18-24 December 2020.)

Notation for the "total space" of a subset.

\begin{code}

module _
        {X : 𝓀 Μ‡ }
       where

 𝕋 : π“Ÿ {π“₯} X β†’ 𝓀 βŠ” π“₯ Μ‡
 𝕋 A = Ξ£ x κž‰ X , x ∈ A

 𝕋-to-carrier : (A : π“Ÿ {π“₯} X) β†’ 𝕋 A β†’ X
 𝕋-to-carrier A = pr₁

 𝕋-to-membership : (A : π“Ÿ {π“₯} X) β†’ (t : 𝕋 A) β†’ 𝕋-to-carrier A t ∈ A
 𝕋-to-membership A = prβ‚‚

\end{code}

We use a named module when defining singleton subsets, so that we can write
❴ x ❡ without having to keep supplying the proof that the ambient type is a set.

\begin{code}

module singleton-subsets
        {X : 𝓀 Μ‡ }
        (X-is-set : is-set X)
       where

 ❴_❡ : X β†’ π“Ÿ X
 ❴ x ❡ = Ξ» y β†’ ((x ＝ y) , X-is-set)

 ∈-❴❡ : {x : X} β†’ x ∈ ❴ x ❡
 ∈-❴❡ {x} = refl

 ❴❡-subset-characterization : {x : X} (A : π“Ÿ {π“₯} X) β†’ x ∈ A ↔ ❴ x ❡ βŠ† A
 ❴❡-subset-characterization {π“₯} {x} A = ⦅⇒⦆ , ⦅⇐⦆
  where
   ⦅⇒⦆ : x ∈ A β†’ ❴ x ❡ βŠ† A
   ⦅⇒⦆ a _ refl = a
   ⦅⇐⦆ : ❴ x ❡ βŠ† A β†’ x ∈ A
   ⦅⇐⦆ s = s x ∈-❴❡

 ❴❡-is-singleton : {x : X} β†’ is-singleton (𝕋 ❴ x ❡)
 ❴❡-is-singleton {x} = singleton-types-are-singletons x

\end{code}

Next, we consider binary intersections and unions in the powerset. For the
latter, we need propositional truncations.

\begin{code}

module _
        {X : 𝓀 Μ‡ }
       where

 _∩_ : π“Ÿ {π“₯} X β†’ π“Ÿ {π“₯} X β†’ π“Ÿ {π“₯} X
 (A ∩ B) x = (x ∈ A Γ— x ∈ B) , Γ—-is-prop (∈-is-prop A x) (∈-is-prop B x)

 ∩-is-lowerbound₁ : (A B : π“Ÿ {π“₯} X) β†’ (A ∩ B) βŠ† A
 ∩-is-lowerbound₁ A B x = pr₁

 ∩-is-lowerboundβ‚‚ : (A B : π“Ÿ {π“₯} X) β†’ (A ∩ B) βŠ† B
 ∩-is-lowerboundβ‚‚ A B x = prβ‚‚

 ∩-is-upperbound-of-lowerbounds : (A B C : π“Ÿ {π“₯} X)
                                β†’ C βŠ† A β†’ C βŠ† B β†’ C βŠ† (A ∩ B)
 ∩-is-upperbound-of-lowerbounds A B C s t x c = (s x c , t x c)

module binary-unions-of-subsets
        (pt : propositional-truncations-exist)
       where

 open PropositionalTruncation pt

 module _
         {X : 𝓀 Μ‡ }
        where

  _βˆͺ_ : π“Ÿ {π“₯} X β†’ π“Ÿ {π“₯} X β†’ π“Ÿ {π“₯} X
  (A βˆͺ B) x = βˆ₯ x ∈ A + x ∈ B βˆ₯ , βˆ₯βˆ₯-is-prop

  βˆͺ-is-upperbound₁ : (A B : π“Ÿ {π“₯} X) β†’ A βŠ† (A βˆͺ B)
  βˆͺ-is-upperbound₁ A B x a = ∣ inl a ∣

  βˆͺ-is-upperboundβ‚‚ : (A B : π“Ÿ {π“₯} X) β†’ B βŠ† (A βˆͺ B)
  βˆͺ-is-upperboundβ‚‚ A B x b = ∣ inr b ∣

  βˆͺ-is-lowerbound-of-upperbounds : (A B C : π“Ÿ {π“₯} X)
                                 β†’ A βŠ† C β†’ B βŠ† C β†’ (A βˆͺ B) βŠ† C
  βˆͺ-is-lowerbound-of-upperbounds A B C s t x = βˆ₯βˆ₯-rec (∈-is-prop C x) Ξ³
    where
     Ξ³ : (x ∈ A + x ∈ B) β†’ x ∈ C
     Ξ³ (inl a) = s x a
     Ξ³ (inr b) = t x b

  βˆ…-left-neutral-for-βˆͺ' : propext π“₯
                        β†’ funext 𝓀 (π“₯ ⁺)
                        β†’ funext π“₯ π“₯
                        β†’ (A : π“Ÿ {π“₯} X) β†’ βˆ… βˆͺ A ＝ A
  βˆ…-left-neutral-for-βˆͺ' pe fe fe' A =
   subset-extensionality'' pe fe fe' s (βˆͺ-is-upperboundβ‚‚ βˆ… A)
    where
     s : (βˆ… βˆͺ A) βŠ† A
     s x = βˆ₯βˆ₯-rec (∈-is-prop A x) Ξ³
      where
       Ξ³ : x ∈ βˆ… + x ∈ A β†’ x ∈ A
       γ (inl p) = 𝟘-elim p
       Ξ³ (inr a) = a

  βˆ…-left-neutral-for-βˆͺ : propext 𝓀
                       β†’ funext 𝓀 (𝓀 ⁺)
                       β†’ (A : π“Ÿ X) β†’ βˆ… βˆͺ A ＝ A
  βˆ…-left-neutral-for-βˆͺ pe fe =
   βˆ…-left-neutral-for-βˆͺ' pe fe (lower-funext 𝓀 (𝓀 ⁺) fe)

  βˆ…-right-neutral-for-βˆͺ' : propext π“₯
                         β†’ funext 𝓀 (π“₯ ⁺)
                         β†’ funext π“₯ π“₯
                         β†’ (A : π“Ÿ {π“₯} X) β†’ A ＝ A βˆͺ βˆ…
  βˆ…-right-neutral-for-βˆͺ' pe fe fe' A =
   subset-extensionality'' pe fe fe' (βˆͺ-is-upperbound₁ A βˆ…) s
    where
     s : (A βˆͺ βˆ…) βŠ† A
     s x = βˆ₯βˆ₯-rec (∈-is-prop A x) Ξ³
      where
       Ξ³ : x ∈ A + x ∈ βˆ… β†’ x ∈ A
       Ξ³ (inl a) = a
       γ (inr p) = 𝟘-elim p

  βˆ…-right-neutral-for-βˆͺ : propext 𝓀
                        β†’ funext 𝓀 (𝓀 ⁺)
                        β†’ (A : π“Ÿ X) β†’ A ＝ A βˆͺ βˆ…
  βˆ…-right-neutral-for-βˆͺ pe fe =
   βˆ…-right-neutral-for-βˆͺ' pe fe (lower-funext 𝓀 (𝓀 ⁺) fe)

  βˆͺ-assoc' : propext π“₯
           β†’ funext 𝓀 (π“₯ ⁺)
           β†’ funext π“₯ π“₯
           β†’ associative {π“₯ ⁺ βŠ” 𝓀} {π“Ÿ {π“₯} X} (_βˆͺ_)
  βˆͺ-assoc' pe fe fe' A B C = subset-extensionality'' pe fe fe' s t
   where
    s : ((A βˆͺ B) βˆͺ C) βŠ† (A βˆͺ (B βˆͺ C))
    s x = βˆ₯βˆ₯-rec i s₁
     where
      i : is-prop (x ∈ (A βˆͺ (B βˆͺ C)))
      i = ∈-is-prop (A βˆͺ (B βˆͺ C)) x
      s₁ : x ∈ (A βˆͺ B) + x ∈ C
         β†’ x ∈ (A βˆͺ (B βˆͺ C))
      s₁ (inl u) = βˆ₯βˆ₯-rec i sβ‚‚ u
       where
        sβ‚‚ : x ∈ A + x ∈ B
           β†’ x ∈ (A βˆͺ (B βˆͺ C))
        sβ‚‚ (inl a) = βˆͺ-is-upperbound₁ A (B βˆͺ C) x a
        sβ‚‚ (inr b) = βˆͺ-is-upperboundβ‚‚ A (B βˆͺ C) x (βˆͺ-is-upperbound₁ B C x b)
      s₁ (inr c) = βˆͺ-is-upperboundβ‚‚ A (B βˆͺ C) x (βˆͺ-is-upperboundβ‚‚ B C x c)
    t : (A βˆͺ (B βˆͺ C)) βŠ† ((A βˆͺ B) βˆͺ C)
    t x = βˆ₯βˆ₯-rec i t₁
     where
      i : is-prop (x ∈ ((A βˆͺ B) βˆͺ C))
      i = ∈-is-prop ((A βˆͺ B) βˆͺ C) x
      t₁ : x ∈ A + x ∈ (B βˆͺ C)
         β†’ x ∈ ((A βˆͺ B) βˆͺ C)
      t₁ (inl a) = βˆͺ-is-upperbound₁ (A βˆͺ B) C x (βˆͺ-is-upperbound₁ A B x a)
      t₁ (inr u) = βˆ₯βˆ₯-rec i tβ‚‚ u
       where
        tβ‚‚ : x ∈ B + x ∈ C
           β†’ x ∈ ((A βˆͺ B) βˆͺ C)
        tβ‚‚ (inl b) = βˆͺ-is-upperbound₁ (A βˆͺ B) C x (βˆͺ-is-upperboundβ‚‚ A B x b)
        tβ‚‚ (inr c) = βˆͺ-is-upperboundβ‚‚ (A βˆͺ B) C x c

  βˆͺ-assoc : propext 𝓀
          β†’ funext 𝓀 (𝓀 ⁺)
          β†’ associative {𝓀 ⁺} {π“Ÿ X} (_βˆͺ_)
  βˆͺ-assoc pe fe = βˆͺ-assoc' pe fe (lower-funext 𝓀 (𝓀 ⁺) fe)

\end{code}

Again assuming propositional truncations, we can construct arbitrary suprema in
π“Ÿ (X : 𝓀) of families indexed by types in 𝓀.

\begin{code}

module unions-of-small-families
        (pt : propositional-truncations-exist)
        (π“₯ : Universe)
        (𝓣 : Universe)
        (X : 𝓀 Μ‡ )
        {I : π“₯ Μ‡ }
       where

 open PropositionalTruncation pt

 ⋃  : (Ξ± : I β†’ π“Ÿ {π“₯ βŠ” 𝓣} X) β†’ π“Ÿ {π“₯ βŠ” 𝓣} X
 ⋃ Ξ± x = (βˆƒ i κž‰ I , x ∈ Ξ± i) , βˆƒ-is-prop

 ⋃-is-upperbound : (Ξ± : I β†’ π“Ÿ {π“₯ βŠ” 𝓣} X) (i : I)
                 β†’ Ξ± i βŠ† ⋃ Ξ±
 ⋃-is-upperbound Ξ± i x a = ∣ i , a ∣

 ⋃-is-lowerbound-of-upperbounds : (Ξ± : I β†’ π“Ÿ {π“₯ βŠ” 𝓣} X) (A : π“Ÿ {π“₯ βŠ” 𝓣} X)
                                β†’ ((i : I) β†’ Ξ± i βŠ† A)
                                β†’ ⋃ Ξ± βŠ† A
 ⋃-is-lowerbound-of-upperbounds Ξ± A ub x u =
  βˆ₯βˆ₯-rec (∈-is-prop A x) Ξ³ u
   where
    Ξ³ : (Ξ£ i κž‰ I , x ∈ Ξ± i) β†’ x ∈ A
    Ξ³ (i , a) = ub i x a

\end{code}

Fixities.

\begin{code}

infix  40 _βˆˆβ‚š_
infix  40 _∈_
infix  40 _βˆ‰_

\end{code}