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 --no-sized-types --no-guardedness --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

(A β© B) x = (x β A Γ x β B) , Γ-is-prop (β-is-prop A x) (β-is-prop B x)

β©-is-lowerboundβ A B x = prβ

β©-is-lowerboundβ A B x = prβ

β 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

(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}