Martin Escardo, 25th August 2022,
written down in Agda 27th August 2022 while travelling back from
Thierry Coquand's 60th birthday celebration.

The type of ordinals is decomposable as a disjoint union of two
pointed types if and only if weak excluded middle holds (every negated
proposition is decidable, which is equivalent to De Morgan's Law).

Equivalently, there is a function f : Ordinal π€ β π such that f Ξ± οΌ 0
and f Ξ² = 1 for some ordinals Ξ± and Ξ² if and only if weak excluded
middle holds.

In other words, the type Ordinal π€ has no non-trivial decidable
property unless weak excluded middle holds.

\begin{code}

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

open import UF.FunExt

module Taboos.Decomposability (fe : FunExt) where

open import MLTT.Spartan
open import MLTT.Two-Properties
open import Ordinals.Arithmetic fe
open import Ordinals.Equivalence
open import Ordinals.Maps
open import Ordinals.Type
open import Ordinals.Underlying
open import UF.Base
open import UF.ClassicalLogic
open import UF.Classifiers
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.EquivalenceExamples
open import UF.PropTrunc
open import UF.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties
open import UF.Univalence

private
fe' : Fun-Ext
fe' {π€} {π₯} = fe π€ π₯

β_ = not fe'

\end{code}

A type X is decomposable if there are pointed types Xβ and Xβ with
X β Xβ + Xβ. Equivalently, X is decomposable if there is a
non-constant function f : X β π, in the strong sense that there are xβ
and xβ in X that are mapped to respectively β and β by f.

We first work with the type of all decompositions, in the above two
equivalent manifestations, and later we consider decomposability
defined as its propositional truncation.

\begin{code}

decomposition : π€ Μ β π€ Μ
decomposition X = Ξ£ f κ (X β π) , (Ξ£ xβ κ X , f xβ οΌ β) Γ (Ξ£ xβ κ X , f xβ οΌ β)

decomposition' : π€ Μ β π€ βΊ Μ
decomposition' {π€} X = Ξ£ Y κ (π β π€ Μ ) , (Y β + Y β β X) Γ Y β Γ Y β

\end{code}

We remark that the above two decomposition types are equivalent, but
we don't use this fact anywhere for the moment, and we work with the
first one.

\begin{code}

decomposition-lemma : is-univalent π€
β (X : π€ Μ )
β (Ξ£ Y κ (π β π€ Μ ) , (Y β + Y β β X))
β (X β π)
decomposition-lemma {π€} ua X =
(Ξ£ Y κ (π β π€ Μ ) , (Y β + Y β β X))       ββ¨ I β©
(Ξ£ Y κ (π β π€ Μ ) , ((Ξ£ n κ π , Y n) β X)) ββ¨ II β©
(X β π)                                    β
where
I  = Ξ£-cong (Ξ» Y β β-cong-left fe (β-sym alternative-+))
II = Ξ£-fibers-β ua fe'

decompositions-agree : is-univalent π€
β (X : π€ Μ )
β decomposition X β decomposition' X
decompositions-agree {π€} ua X =
(Ξ£ f κ (X β π) , fiber f β Γ fiber f β)                        ββ¨ I β©
(Ξ£ (Y , _) κ (Ξ£ Y κ (π β π€ Μ ) , (Y β + Y β β X)) , Y β Γ Y β)  ββ¨ II β©
(Ξ£ Y κ (π β π€ Μ ) , (Y β + Y β β X) Γ Y β Γ Y β)                β
where
I  = Ξ£-change-of-variable-β _ (β-sym (decomposition-lemma ua X))
II = Ξ£-assoc

WEM-gives-decomposition-of-two-pointed-types : WEM π€
β (X : π€ Μ )
β has-two-distinct-points X
β decomposition X
WEM-gives-decomposition-of-two-pointed-types wem X ((xβ , xβ) , d) = Ξ³
where
g : (x : X) β Β¬ (x β  xβ) + Β¬Β¬ (x β  xβ) β π
g x (inl _) = β
g x (inr _) = β

h : (x : X) β Β¬ (x β  xβ) + Β¬Β¬ (x β  xβ)
h x = wem (x β  xβ)

f : X β π
f x = g x (h x)

gβ : (Ξ΄ : Β¬ (xβ β  xβ) + Β¬Β¬ (xβ β  xβ)) β g xβ Ξ΄ οΌ β
gβ (inl _) = refl
gβ (inr u) = π-elim (three-negations-imply-one u refl)

eβ : f xβ οΌ β
eβ = gβ (h xβ)

gβ : (Ξ΄ : Β¬ (xβ β  xβ) + Β¬Β¬ (xβ β  xβ)) β g xβ Ξ΄ οΌ β
gβ (inl Ο) = π-elim (Ο (β -sym d))
gβ (inr _) = refl

eβ : f xβ οΌ β
eβ = gβ (h xβ)

Ξ³ : decomposition X
Ξ³ = f , (xβ , eβ) , (xβ , eβ)

WEM-gives-decomposition-of-ordinals-typeβΊ : WEM (π€ βΊ)
β decomposition (Ordinal π€)
WEM-gives-decomposition-of-ordinals-typeβΊ {π€} wem =
WEM-gives-decomposition-of-two-pointed-types wem (Ordinal π€)
((πβ , πβ) , (Ξ» (e : πβ οΌ πβ) β π-elim (idtofun π π (ap β¨_β© e) β)))

\end{code}

We can strengthen the hypothesis of the above implication to WEM π€
using the fact that the type Ordinal π€ Μ is locally small.

\begin{code}

WEM-gives-decomposition-of-two-pointed-typesβΊ : WEM π€
β (X : π€ βΊ Μ )
β is-locally-small X
β has-two-distinct-points X
β decomposition X
WEM-gives-decomposition-of-two-pointed-typesβΊ {π€} wem X l ((xβ , xβ) , d) = Ξ³
where
g : (x : X) β Β¬ (x β β¦ l β§ xβ) + Β¬Β¬ (x β β¦ l β§ xβ) β π
g x (inl _) = β
g x (inr _) = β

h : (x : X) β Β¬ (x β β¦ l β§ xβ) + Β¬Β¬ (x β β¦ l β§ xβ)
h x = wem (x β β¦ l β§ xβ)

f : X β π
f x = g x (h x)

gβ : (Ξ΄ : Β¬ (xβ β β¦ l β§ xβ) + Β¬Β¬ (xβ β β¦ l β§ xβ)) β g xβ Ξ΄ οΌ β
gβ (inl _) = refl
gβ (inr u) = π-elim (three-negations-imply-one u οΌβ¦ l β§-refl)

eβ : f xβ οΌ β
eβ = gβ (h xβ)

gβ : (Ξ΄ : Β¬ (xβ β β¦ l β§ xβ) + Β¬Β¬ (xβ β β¦ l β§ xβ)) β g xβ Ξ΄ οΌ β
gβ (inl Ο) = π-elim (Ο (β -gives-β β¦ l β§ (β -sym d)))
gβ (inr _) = refl

eβ : f xβ οΌ β
eβ = gβ (h xβ)

Ξ³ : decomposition X
Ξ³ = f , (xβ , eβ) , (xβ , eβ)

WEM-gives-decomposition-of-ordinals-type : is-univalent π€
β WEM π€
β decomposition (Ordinal π€)
WEM-gives-decomposition-of-ordinals-type {π€} ua wem =
WEM-gives-decomposition-of-two-pointed-typesβΊ wem (Ordinal π€)
(the-type-of-ordinals-is-locally-small ua fe')
((πβ , πβ) , (Ξ» (e : πβ οΌ πβ) β π-elim (idtofun π π (ap β¨_β© e) β)))

\end{code}

For the converse, we use the following notion, where Ξ© π€ is the type
of truth values, or propositions, in the universe π€. An Ξ©-path from x
to y in a type X is a function f κ Ξ© π₯ β X that maps false to x and
true to y. We collect all such functions in a type Ξ©-Path π₯ x y.

\begin{code}

Ξ©-Path : {X : π€ Μ } (π₯ : Universe) β X β X β π€ β (π₯ βΊ) Μ
Ξ©-Path {π€} {X} π₯ x y = Ξ£ f κ (Ξ© π₯ β X) , (f β₯ οΌ x) Γ (f β€ οΌ y)

\end{code}

The type of ordinals in any universe has Ξ©-paths between any two points.

\begin{code}

has-Ξ©-paths : (π₯ : Universe) β π€ Μ β π€ β (π₯ βΊ) Μ
has-Ξ©-paths π₯ X = (x y : X) β Ξ©-Path π₯ x y

type-of-ordinals-has-Ξ©-paths {π€} ua Ξ± Ξ² = f , Ξ³β₯ , Ξ³β€
where

f : Ξ© π€ β Ordinal π€
f p = (Ξ©-to-ordinal (β p) Γβ Ξ±) +β (Ξ©-to-ordinal p Γβ Ξ²)

Ξ³β₯ : f β₯ οΌ Ξ±
Ξ³β₯ = eqtoidβ ua fe' (f β₯) Ξ± (u , o , e , p)
where
u (inl (x , a)) = a

o : is-order-preserving (f β₯) Ξ± u
o (inl (x , a)) (inl (y , b)) (inl l) = l

v a = inl (π-elim , a)

vu : v β u βΌ id
vu (inl (x , a)) = ap inl (to-Γ-οΌ (dfunext fe' (Ξ» z β π-elim z)) refl)

uv : u β v βΌ id
uv a = refl

e : is-equiv u
e = qinvs-are-equivs u (v , vu , uv)

p : is-order-preserving Ξ± (f β₯) v
p a b l = inl l

Ξ³β€ : f β€ οΌ Ξ²
Ξ³β€ = eqtoidβ ua fe' (f β€) Ξ² (u , o , e , p)
where
u (inl (f , _)) = π-elim (f β)
u (inr (β , b)) = b

o : is-order-preserving (f β€) Ξ² u
o (inl (f , _)) y l = π-elim (f β)
o (inr (β , _)) (inr (β , _)) (inl l) = l

v b = inr (β , b)

vu : v β u βΌ id
vu (inl (f , _)) = π-elim (f β)
vu (inr (β , b)) = refl

uv : u β v βΌ id
uv b = refl

e : is-equiv u
e = qinvs-are-equivs u (v , vu , uv)

p : is-order-preserving Ξ² (f β€) v
p b c l = inl l

β WEM π€
{π€} pe (f , (pβ@(Pβ , iβ) , eβ) , (pβ@(Pβ , iβ) , eβ)) = V
where
g (Q , j) = ((Pβ Γ Q) + (Pβ Γ Β¬ Q)) , k
where
k : is-prop ((Pβ Γ Q) + (Pβ Γ Β¬ Q))
k = +-is-prop
(Γ-is-prop iβ j)
(Γ-is-prop iβ (negations-are-props fe'))
(Ξ» (pβ , q) (pβ , Ξ½) β Ξ½ q)

Iβ : (q : Ξ© π€) β q holds β f (g q) οΌ β
Iβ q h = II
where
I : g q οΌ pβ
I = to-subtype-οΌ
(Ξ» _ β being-prop-is-prop fe')
(pe (prβ (g q)) iβ
(cases prβ (Ξ» (_ , n) β π-elim (n h)))
(Ξ» x β inl (x , h)))

II = f (g q) οΌβ¨ ap f I β©
β       β

Iβ : (q : Ξ© π€) β Β¬ (q holds) β f (g q) οΌ β
Iβ q n = II
where
I : g q οΌ pβ
I = to-subtype-οΌ
(Ξ» _ β being-prop-is-prop fe')
(pe (prβ (g q)) iβ
(cases (Ξ» (_ , h) β π-elim (n h)) prβ)
(Ξ» x β inr (x , n)))

II = f (g q) οΌβ¨ ap f I β©
β       β

IIIβ : (q : Ξ© π€) β f (g q) οΌ β β Β¬ (q holds) + Β¬Β¬ (q holds)
IIIβ q e = inr (contrapositive (Iβ q) (equal-β-different-from-β e))

IIIβ : (q : Ξ© π€) β f (g q) οΌ β β Β¬ (q holds) + Β¬Β¬ (q holds)
IIIβ q e = inl (contrapositive (Iβ q) (equal-β-different-from-β e))

IV : (Q : π€  Μ ) β is-prop Q β Β¬ Q + Β¬Β¬ Q
IV Q j = π-equality-cases (IIIβ (Q , j)) (IIIβ (Q , j))

V : (Q : π€  Μ ) β Β¬ Q + Β¬Β¬ Q
V = WEM'-gives-WEM fe' IV

β {X : π€ Μ }
β decomposition X
β WEM π₯
{π₯} {π€} pe {X} (f , (xβ , eβ) , (xβ , eβ)) c = Ξ³
where
g : Ξ© π₯ β X
g = prβ (c xβ xβ)

gp : (g β₯ οΌ xβ) Γ (g β€ οΌ xβ)
gp = prβ (c xβ xβ)

Iβ = f (g β₯) οΌβ¨ ap f (prβ gp) β©
β       β

Iβ = f (g β€) οΌβ¨ ap f (prβ gp) β©
β       β

Ξ³ : WEM π₯
Ξ³ = decomposition-of-Ξ©-gives-WEM pe (f β g , (β₯ , Iβ) , (β€ , Iβ))

decomposition-of-ordinals-type-gives-WEM : is-univalent π€
β decomposition (Ordinal π€)
β WEM π€
decomposition-of-ordinals-type-gives-WEM ua d =
(univalence-gives-propext ua)
d

Ordinal-decomposition-iff-WEM : is-univalent π€
β decomposition (Ordinal π€) β WEM π€
Ordinal-decomposition-iff-WEM ua =
decomposition-of-ordinals-type-gives-WEM ua ,
WEM-gives-decomposition-of-ordinals-type ua

\end{code}

We now assume that propositional truncations exist to define
decomposability as the truncation of the type of decompositions. It is
a corollary of the above development that the decomposability of the
type of ordinals gives a specific decomposition.

\begin{code}

module decomposability (pt : propositional-truncations-exist) where

open PropositionalTruncation pt

decomposable : π€ Μ β π€ Μ
decomposable X = β₯ decomposition X β₯

Ordinal-decomposable-iff-WEM : is-univalent π€
β decomposable (Ordinal π€) β WEM π€
Ordinal-decomposable-iff-WEM ua =
β₯β₯-rec (WEM-is-prop fe) (decomposition-of-ordinals-type-gives-WEM ua) ,
(Ξ» wem β β£ WEM-gives-decomposition-of-ordinals-type ua wem β£)

decomposability-gives-decomposition : is-univalent π€
β decomposable (Ordinal π€)
β decomposition (Ordinal π€)
decomposability-gives-decomposition ua Ξ΄ =
WEM-gives-decomposition-of-ordinals-type ua
(lr-implication (Ordinal-decomposable-iff-WEM ua) Ξ΄)

\end{code}

Notice that the formulation of this fact doesn't refer to WEM, but its
proof uses WEM, which follows from the hypothesis. Even though the
types decomposable (Ordinal π€) and WEM are property, we get data out
of them if we are given a proof of decomposability.

Added 9th September 2022 by Tom de Jong (which is subsumed by a remark

After a discussion with MartΓ­n on 8th September 2022, we noticed that
the decomposability theorem can be generalised from Ord π€ to any
locally small π€-sup-lattice with two distinct points. (This is indeed
a generalisation because Ord π€ is a locally small π€-sup-lattice, at
least in the presence of small set quotients or set replacement, see
Ordinals.OrdinalOfOrdinalsSuprema.)

One direction is still given by the lemma above:
WEM-gives-decomposition-of-two-pointed-typesβΊ :
WEM π€
β (X : π€ βΊ Μ )
β is-locally-small X
β has-two-distinct-points X
β decomposition X

[NB. Predicatively, nontrivial π€-sup-lattices necessarily have large
carriers [dJE21,dJE22], so that the simpler lemma

WEM-gives-decomposition-of-two-pointed-types :
WEM π€
β (X : π€ Μ )
β has-two-distinct-points X
β decomposition X

is not sufficient.]

For the other we use

{X : π€ Μ }
β decomposition X
β WEM π₯

The point is that every π€-sup-lattice X has Ξ©π€-paths, because given x
y : X, we can define f : Ξ© π€ β X by mapping a proposition P to the
join of the family

Ξ΄ : π + P β X
Ξ΄(inl β) = x;
Ξ΄(inr p) = y.

The family Ξ΄ also plays a key role in [dJE21,dJE22] although we have
the restriction that x β y in those papers, because we consider a
broader collection of posets there that includes the π€-sup-lattices,
but also π€-bounded-complete posets and π€-directed complete posets.

References
----------

[dJE21] Tom de Jong and MartΓ­n HΓΆtzel EscardΓ³.
βPredicative Aspects of Order Theory in Univalent Foundationsβ.
In: 6th International Conference on Formal Structures for Computation and
Deduction (FSCD 2021). Ed. by Naoki Kobayashi. Vol. 195.
Leibniz International Proceedings in Informatics (LIPIcs).
Schloss DagstuhlβLeibniz-Zentrum fΓΌr Informatik, 2021, 8:1β8:18.
doi: 10.4230/LIPIcs.FSCD.2021.8.

[dJE22] Tom de Jong and MartΓ­n HΓΆtzel EscardΓ³.
βOn Small Types in Univalent Foundationsβ. Sept. 2022.
arXiv: 2111.00482 [cs.LO]. Revised and expanded version of [dJE21b].
Accepted pending minor revision to a special issue of Logical Methods in
Computer Science on selected papers from FSCD 2021.

TODO. Implement the above thoughts.

Added 3rd August 2023 by Martin Escardo. Injective types are
decomposable iff WEM holds. This subsumes the above developement,
because the type of ordinals is injective.

\begin{code}

open import InjectiveTypes.Blackboard fe
open import InjectiveTypes.OverSmallMaps fe
open import Ordinals.Injectivity

open ordinals-injectivity fe

\end{code}

A naive application of injectivity gives the following:

\begin{code}

β (D : π€ Μ )
β ainjective-type D π€β (π¦ βΊ)
ainjective-types-have-Ξ©-Paths-naive {π¦} {π€} pe D D-ainj xβ xβ = II I
where
f : π β D
f β = xβ
f β = xβ

I : Ξ£ g κ (Ξ© π¦ β D) , g β π-to-Ξ© βΌ f

II : type-of I β Ξ©-Path π¦ xβ xβ
II (g , h) = g , h β , h β

\end{code}

But this is too weak for applications, as the universe π¦βΊ is higher
than we can obtain in practice.

This can be improved as follows, exploiting the fact that the map
π-to-Ξ© : π β Ξ© π€ has π€-small fibers and that algebraic flabbiness
gives injectivity over embeddings with small fibers for lower
universes. The key point is that this allows to replace π¦βΊ by π¦ in the
above, so that we can apply this to the injectivity of the universe
and to that of the type of ordinals, and more examples like these.

\begin{code}

β (D : π€ Μ )
β ainjective-type D π₯ π¦
ainjective-types-have-Ξ©-Paths {π₯} {π€} {π¦} pe D D-ainj xβ xβ = II I
where
f : π β D
f β = xβ
f β = xβ

I : Ξ£ g κ (Ξ© π₯ β D) , g β π-to-Ξ© βΌ f
I = ainjectivity-over-small-maps {π€β} {π₯ βΊ} {π€} {π₯} {π₯} {π¦}
D
D-ainj
f

II : type-of I β Ξ©-Path π₯ xβ xβ
II (g , h) = g , h β , h β

decomposition-of-ainjective-type-gives-WEM : propext π₯
β (D : π€ Μ )
β ainjective-type D π₯ π¦
β decomposition D
β WEM π₯
decomposition-of-ainjective-type-gives-WEM
{π₯} {π€} {π¦} pe D D-ainj D-decomp =
pe
D-decomp
(ainjective-types-have-Ξ©-Paths {π₯} {π€} {π¦} pe D D-ainj)

\end{code}

Examples:

\begin{code}

decomposition-of-universe-gives-WEM : is-univalent π€
β decomposition (π€ Μ )
β WEM π€
decomposition-of-universe-gives-WEM {π€} ua =
decomposition-of-ainjective-type-gives-WEM {π€} {π€ βΊ} {π€}
(univalence-gives-propext ua)
(π€ Μ )
(universes-are-ainjective-Ξ  ua)

decomposition-of-ordinals-type-gives-WEM-bis : is-univalent π€
β decomposition (Ordinal π€)
β WEM π€
decomposition-of-ordinals-type-gives-WEM-bis {π€} ua =
decomposition-of-ainjective-type-gives-WEM {π€} {π€ βΊ} {π€}
(univalence-gives-propext ua)
(Ordinal π€)
(Ordinal-is-ainjective ua)

\end{code}

Added by Martin Escardo and Tom de Jong 18th July 2024. We generalize
a fact given above from ordinals to injective types.

\begin{code}

module decomposability-bis (pt : propositional-truncations-exist) where

open PropositionalTruncation pt
open decomposability pt

ainjective-type-decomposable-iff-WEM
: propext π€
β (D : π€ Μ )
β ainjective-type D π€ π₯
β has-two-distinct-points D
β decomposable D β WEM π€
ainjective-type-decomposable-iff-WEM pe D D-ainj htdp =
β₯β₯-rec
(WEM-is-prop fe)
(decomposition-of-ainjective-type-gives-WEM pe D D-ainj) ,
(Ξ» wem β β£ WEM-gives-decomposition-of-two-pointed-types wem D htdp β£)

\end{code}

Added 25th July 2024 by Tom de Jong and Martin Escardo.

The previous theorem, however, doesn't capture our examples of injective types. Indeed, the assumption that D : π€ is injective with respect to π€
and π₯ is a bit unnatural, as all known examples of injective types are
large, e.g. the universe π€ is injective w.r.t π€ and π€, as are the
ordinals in π€ and the propositions in π€. In fact, in
InjectiveTypes.Resizing we showed that such injective types are
necessarily large unless Ξ©Β¬Β¬-resizing holds. Therefore, we now improve
and generalize the above theorem to a large, but locally small,
type, so that all known examples are captured.

\begin{code}

ainjective-type-decomposable-iff-WEMβΊ
: propext π€
β (D : π€ βΊ Μ )
β is-locally-small D
β ainjective-type D π€ π₯
β has-two-distinct-points D
β decomposable D β WEM π€
ainjective-type-decomposable-iff-WEMβΊ pe D D-ls D-ainj htdp =
β₯β₯-rec
(WEM-is-prop fe)
(decomposition-of-ainjective-type-gives-WEM pe D D-ainj) ,
(Ξ» wem β β£ WEM-gives-decomposition-of-two-pointed-typesβΊ wem D D-ls htdp β£)

\end{code}

Notice that the following doesn't mention WEM in its statement, but
its proof does. Although the proof is constructive, the assumption is
necessarily non-constructive.

\begin{code}

ainjective-type-decomposability-gives-decomposition
: propext π€
β (D : π€ Μ )
β ainjective-type D π€ π₯
β has-two-distinct-points D
β decomposable D
β decomposition D
ainjective-type-decomposability-gives-decomposition pe D D-ainj htdp Ξ΄ =
WEM-gives-decomposition-of-two-pointed-types
(lr-implication (ainjective-type-decomposable-iff-WEM pe D D-ainj htdp) Ξ΄)
D
htdp

\end{code}

Also added 25th July 2024 for the same reason given above:

\begin{code}

ainjective-type-decomposability-gives-decompositionβΊ
: propext π€
β (D : π€ βΊ Μ )
β is-locally-small D
β ainjective-type D π€ π₯
β has-two-distinct-points D
β decomposable D
β decomposition D
ainjective-type-decomposability-gives-decompositionβΊ pe D D-ls D-ainj htdp Ξ΄ =
WEM-gives-decomposition-of-two-pointed-typesβΊ
(lr-implication (ainjective-type-decomposable-iff-WEMβΊ pe D D-ls D-ainj htdp) Ξ΄)
D
D-ls
htdp

\end{code}

Added by Martin Escardo 10th June 2024. From any non-trivial,
totally separated, injective type we get the double negation of the
principle of weak excluded middle. Here by non-trivial we mean that
not all two elements are equal, which means that the type is not a
proposition.

(Of course, "Ξ£" in the hypothesis can be replaced by "β" because the
type of the conclusion, being a negation, is a proposition.)

\begin{code}

open import UF.Hedberg using (wconstant)
open import TypeTopology.TotallySeparated

non-trivial-totally-separated-ainjective-type-gives-Β¬Β¬-WEM
: propext π₯
β (Ξ£ X κ π€ Μ , ((Β¬ is-prop X) Γ is-totally-separated X Γ ainjective-type X π₯ π¦))
β Β¬Β¬ WEM π₯
non-trivial-totally-separated-ainjective-type-gives-Β¬Β¬-WEM
{π₯} {π€} {π¦} pe (X , X-is-not-prop , X-is-totally-separated , X-ainj) = V
where
I : Β¬ decomposition X β (p : X β π) β wconstant p
I Ξ΄ p xβ xβ = h (p xβ) (p xβ) refl refl
where
h : (bβ bβ : π) β p xβ οΌ bβ β p xβ οΌ bβ β p xβ οΌ p xβ
h β β eβ eβ = eβ β eβ β»ΒΉ
h β β eβ eβ = π-elim (Ξ΄ (p , (xβ , eβ) , (xβ , eβ)))
h β β eβ eβ = π-elim (Ξ΄ (p , (xβ , eβ) , (xβ , eβ)))
h β β eβ eβ = eβ β eβ β»ΒΉ

II : ((p : X β π) β wconstant p) β is-prop X
II w xβ xβ = X-is-totally-separated (Ξ» p β w p xβ xβ)

III : Β¬ decomposition X β is-prop X
III = II β I

IV : Β¬Β¬ decomposition X
IV = contrapositive III X-is-not-prop

V : Β¬Β¬ WEM π₯
V = Β¬Β¬-functor
(decomposition-of-ainjective-type-gives-WEM pe X X-ainj)
IV

\end{code}

Notice that Β¬ WEM π€ is consistent and hence Β¬Β¬ WEM π€ is not
provable. But of course Β¬Β¬ WEM π€ is consistent as it follows from WEM π€,
which in turn follows from EM π€.

More examples are included in Iterative.Multisets-Addendum and