Martin Escardo, 5th September 2018.

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

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

module UF.Powerset where

open import MLTT.Spartan
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.FunExt
open import UF.Lower-FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt
open import UF.Univalence

π“Ÿ : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
π“Ÿ {𝓀} X = X β†’ Ξ© 𝓀

π“Ÿ-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 holds

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

infix  40 _∈_
infix  40 _βˆ‰_

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.ExcludedMiddle

 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

 non-inhabited-subsets-are-empty : {X : 𝓀 Μ‡ } (B : π“Ÿ X)
                                 β†’ Β¬ is-inhabited B
                                 β†’ is-empty-subset B
 non-inhabited-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

βˆ…-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 {X} 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}