Ordinals.IndecomposableMartin Escardo, 25th August 2022, with additions 31st July.
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).
This file has been moved to the following location:
\begin{code}
{-# OPTIONS --safe --without-K #-}
module Ordinals.Indecomposable where
open import Taboos.Decomposability using ()
\end{code}