This is ported from the Midlands Graduate School 2019 lecture notes

 https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/HoTT-UF-Agda.html
 https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes

\begin{code}

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

module MGS.Choice where

open import MGS.Unique-Existence        public
open import MGS.Yoneda                  public
open import MGS.Subsingleton-Truncation public
open import MGS.Universe-Lifting        public

simple-unique-choice : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) (R : (x : X) β†’ A x β†’ 𝓦 Μ‡ )

                     β†’ ((x : X) β†’ βˆƒ! a κž‰ A x , R x a)
                     β†’ Ξ£ f κž‰ Ξ  A , ((x : X) β†’ R x (f x))

simple-unique-choice X A R s = f , Ο†
 where
  f : (x : X) β†’ A x
  f x = pr₁ (center (Ξ£ a κž‰ A x , R x a) (s x))

  Ο† : (x : X) β†’ R x (f x)
  Ο† x = prβ‚‚ (center (Ξ£ a κž‰ A x , R x a) (s x))

Unique-Choice : (𝓀 π“₯ 𝓦 : Universe) β†’ (𝓀 βŠ” π“₯ βŠ” 𝓦)⁺ Μ‡
Unique-Choice 𝓀 π“₯ 𝓦 = (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) (R : (x : X) β†’ A x β†’ 𝓦 Μ‡ )
                     β†’ ((x : X) β†’ βˆƒ! a κž‰ A x , R x a)
                     β†’ βˆƒ! f κž‰ Ξ  A , ((x : X) β†’ R x (f x))

vvfunext-gives-unique-choice : vvfunext 𝓀 (π“₯ βŠ” 𝓦) β†’ Unique-Choice 𝓀 π“₯ 𝓦
vvfunext-gives-unique-choice vv X A R s = c
 where
  a : ((x : X) β†’ Ξ£ a κž‰ A x , R x a)
    ≃ (Ξ£ f κž‰ ((x : X) β†’ A x), ((x : X) β†’ R x (f x)))

  a = Ξ Ξ£-distr-≃

  b : is-singleton ((x : X) β†’ Ξ£ a κž‰ A x , R x a)
  b = vv s

  c : is-singleton (Ξ£ f κž‰ ((x : X) β†’ A x), ((x : X) β†’ R x (f x)))
  c = equiv-to-singleton' a b

unique-choice-gives-vvfunext : Unique-Choice 𝓀 π“₯ π“₯ β†’ vvfunext 𝓀 π“₯
unique-choice-gives-vvfunext {𝓀} {π“₯} uc {X} {A} Ο† = Ξ³
 where
  R : (x : X) β†’ A x β†’ π“₯  Μ‡
  R x a = A x

  s' : (x : X) β†’ is-singleton (A x Γ— A x)
  s' x = Γ—-is-singleton (Ο† x) (Ο† x)

  s : (x : X) β†’ βˆƒ! y κž‰ A x , R x y
  s = s'

  e : βˆƒ! f κž‰ Ξ  A , ((x : X) β†’ R x (f x))
  e = uc X A R s

  e' : is-singleton (Ξ  A Γ— Ξ  A)
  e' = e

  ρ : Ξ  A ◁ Ξ  A Γ— Ξ  A
  ρ = pr₁ , (Ξ» y β†’ y , y) , refl

  Ξ³ : is-singleton (Ξ  A)
  γ = retract-of-singleton ρ e'

unique-choice-gives-hfunext : Unique-Choice 𝓀 π“₯ π“₯ β†’ hfunext 𝓀 π“₯
unique-choice-gives-hfunext {𝓀} {π“₯} uc = β†’hfunext Ξ³
 where
  Ξ³ : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) (f : Ξ  A) β†’ βˆƒ! g κž‰ Ξ  A , f ∼ g
  Ξ³ X A f = uc X A R e
   where
    R : (x : X) β†’ A x β†’ π“₯ Μ‡
    R x a = f x ＝ a
    e : (x : X) β†’ βˆƒ! a κž‰ A x , f x ＝ a
    e x = singleton-types'-are-singletons (A x) (f x)

unique-choice↔vvfunext : Unique-Choice 𝓀 π“₯ π“₯ ↔ vvfunext 𝓀 π“₯
unique-choice↔vvfunext = unique-choice-gives-vvfunext ,
                         vvfunext-gives-unique-choice

module _ (hfe : global-hfunext) where

 private
   hunapply : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {f g : Ξ  A} β†’ f ∼ g β†’ f ＝ g
   hunapply = inverse (happly _ _) (hfe _ _)

 transport-hunapply : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (R : (x : X) β†’ A x β†’ 𝓦 Μ‡ )
                      (f g : Ξ  A)
                      (Ο† : (x : X) β†’ R x (f x))
                      (h : f ∼ g)
                      (x : X)
                    β†’ transport (Ξ» - β†’ (x : X) β†’ R x (- x)) (hunapply h) Ο† x
                    ＝ transport (R x) (h x) (Ο† x)

 transport-hunapply A R f g Ο† h x =

   transport (Ξ» - β†’ βˆ€ x β†’ R x (- x)) (hunapply h) Ο† x ＝⟨ i ⟩
   transport (R x) (happly f g (hunapply h) x) (Ο† x)  ＝⟨ ii ⟩
   transport (R x) (h x) (Ο† x)                        ∎

  where
   a : {f g : Ξ  A} {Ο† : βˆ€ x β†’ R x (f x)} (p : f ＝ g) (x : domain A)
     β†’ transport (Ξ» - β†’ βˆ€ x β†’ R x (- x)) p Ο† x
     ＝ transport (R x) (happly f g p x) (Ο† x)

   a (refl _) x = refl _

   b : happly f g (hunapply h) ＝ h
   b = inverses-are-sections (happly f g) (hfe f g) h

   i  = a (hunapply h) x
   ii = ap (Ξ» - β†’ transport (R x) (- x) (Ο† x)) b

 unique-choice : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) (R : (x : X) β†’ A x β†’ 𝓦 Μ‡ )

               β†’ ((x : X) β†’ βˆƒ! a κž‰ A x , R x a)
               β†’ βˆƒ! f κž‰ ((x : X) β†’ A x), ((x : X) β†’ R x (f x))

 unique-choice X A R s = C , Ξ¦
  where
   fβ‚€ : (x : X) β†’ A x
   fβ‚€ x = pr₁ (center (Ξ£ a κž‰ A x , R x a) (s x))

   Ο†β‚€ : (x : X) β†’ R x (fβ‚€ x)
   Ο†β‚€ x = prβ‚‚ (center (Ξ£ a κž‰ A x , R x a) (s x))

   C : Ξ£ f κž‰ ((x : X) β†’ A x), ((x : X) β†’ R x (f x))
   C = fβ‚€ , Ο†β‚€

   c : (x : X) β†’ (Ο„ : Ξ£ a κž‰ A x , R x a) β†’ fβ‚€ x , Ο†β‚€ x ＝ Ο„
   c x = centrality (Ξ£ a κž‰ A x , R x a) (s x)

   c₁ : (x : X) (a : A x) (r : R x a) β†’ fβ‚€ x ＝ a
   c₁ x a r = ap pr₁ (c x (a , r))

   cβ‚‚ : (x : X) (a : A x) (r : R x a)
      β†’ transport (Ξ» - β†’ R x (pr₁ -)) (c x (a , r)) (Ο†β‚€ x) ＝ r

   cβ‚‚ x a r = apd prβ‚‚ (c x (a , r))

   Ξ¦ : (Οƒ : Ξ£ f κž‰ ((x : X) β†’ A x), ((x : X) β†’ R x (f x))) β†’ C ＝ Οƒ
   Ξ¦ (f , Ο†) = to-Ξ£-＝ (p , hunapply q)
    where
     p : fβ‚€ ＝ f
     p = hunapply (Ξ» x β†’ c₁ x (f x) (Ο† x))

     q : transport (Ξ» - β†’ (x : X) β†’ R x (- x)) p Ο†β‚€ ∼ Ο†
     q x = transport (Ξ» - β†’ (x : X) β†’ R x (- x)) p Ο†β‚€ x           ＝⟨ i ⟩
           transport (R x) (ap pr₁ (c x (f x , Ο† x))) (Ο†β‚€ x)      ＝⟨ ii ⟩
           transport (Ξ» Οƒ β†’ R x (pr₁ Οƒ)) (c x (f x , Ο† x)) (Ο†β‚€ x) ＝⟨ iii ⟩
           Ο† x                                                    ∎
      where
       i   = transport-hunapply A R fβ‚€ f Ο†β‚€ (Ξ» x β†’ c₁ x (f x) (Ο† x)) x
       ii  = (transport-ap (R x) pr₁ (c x (f x , Ο† x)) (Ο†β‚€ x))⁻¹
       iii = cβ‚‚ x (f x) (Ο† x)

module choice
        (pt  : subsingleton-truncations-exist)
        (hfe : global-hfunext)
       where

  open basic-truncation-development pt hfe public

  simple-unique-choice' : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) (R : (x : X) β†’ A x β†’ 𝓦 Μ‡ )

                        β†’ ((x : X) β†’ is-subsingleton (Ξ£ a κž‰ A x , R x a))

                        β†’ ((x : X) β†’ βˆƒ a κž‰ A x , R x a)
                        β†’ Ξ£ f κž‰ Ξ  A , ((x : X) β†’ R x (f x))

  simple-unique-choice' X A R u Ο† = simple-unique-choice X A R s
   where
    s : (x : X) β†’ βˆƒ! a κž‰ A x , R x a
    s x = inhabited-subsingletons-are-singletons (Ξ£ a κž‰ A x , R x a) (Ο† x) (u x)

  AC : βˆ€ 𝓣 (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ )
     β†’ is-set X β†’ ((x : X) β†’ is-set (A x)) β†’ 𝓣 ⁺ βŠ” 𝓀 βŠ” π“₯ Μ‡

  AC 𝓣 X A i j = (R : (x : X) β†’ A x β†’ 𝓣 Μ‡ )
               β†’ ((x : X) (a : A x) β†’ is-subsingleton (R x a))

               β†’ ((x : X) β†’ βˆƒ a κž‰ A x , R x a)
               β†’ βˆƒ f κž‰ Ξ  A , ((x : X) β†’ R x (f x))

  Choice : βˆ€ 𝓀 β†’ 𝓀 ⁺ Μ‡
  Choice 𝓀 = (X : 𝓀 Μ‡ ) (A : X β†’ 𝓀 Μ‡ ) (i : is-set X) (j : (x : X) β†’ is-set (A x))
           β†’ AC 𝓀 X A i j

  IAC : (X : 𝓀 Μ‡ ) (Y : X β†’ π“₯ Μ‡ ) β†’ is-set X β†’ ((x : X) β†’ is-set (Y x)) β†’ 𝓀 βŠ” π“₯ Μ‡
  IAC X Y i j = ((x : X) β†’ βˆ₯ Y x βˆ₯) β†’ βˆ₯ Ξ  Y βˆ₯

  IChoice : βˆ€ 𝓀 β†’ 𝓀 ⁺ Μ‡
  IChoice 𝓀 = (X : 𝓀 Μ‡ ) (Y : X β†’ 𝓀 Μ‡ ) (i : is-set X) (j : (x : X) β†’ is-set (Y x))
            β†’ IAC X Y i j

  Choice-gives-IChoice : Choice 𝓀 β†’ IChoice 𝓀
  Choice-gives-IChoice {𝓀} ac X Y i j Ο† = Ξ³
   where
    R : (x : X) β†’ Y x β†’ 𝓀 Μ‡
    R x y = x ＝ x -- Any singleton type in 𝓀 will do.

    k : (x : X) (y : Y x) β†’ is-subsingleton (R x y)
    k x y = i x x

    h : (x : X) β†’ Y x β†’ Ξ£ y κž‰ Y x , R x y
    h x y = (y , refl x)

    g : (x : X) β†’ βˆƒ y κž‰ Y x , R x y
    g x = βˆ₯βˆ₯-functor (h x) (Ο† x)

    c : βˆƒ f κž‰ Ξ  Y , ((x : X) β†’ R x (f x))
    c = ac X Y i j R k g

    Ξ³ : βˆ₯ Ξ  Y βˆ₯
    Ξ³ = βˆ₯βˆ₯-functor pr₁ c

  IChoice-gives-Choice : IChoice 𝓀 β†’ Choice 𝓀
  IChoice-gives-Choice {𝓀} iac X A i j R k ψ = Ξ³
   where
    Y : X β†’ 𝓀 Μ‡
    Y x = Ξ£ a κž‰ A x , R x a

    l : (x : X) β†’ is-set (Y x)
    l x = subsets-of-sets-are-sets (A x) (R x) (j x) (k x)

    a : βˆ₯ Ξ  Y βˆ₯
    a = iac X Y i l ψ

    h : Ξ  Y β†’ Ξ£ f κž‰ Ξ  A , ((x : X) β†’ R x (f x))
    h g = (Ξ» x β†’ pr₁ (g x)) , (Ξ» x β†’ prβ‚‚ (g x))

    Ξ³ : βˆƒ f κž‰ Ξ  A , ((x : X) β†’ R x (f x))
    Ξ³ = βˆ₯βˆ₯-functor h a

  TAC : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) β†’ is-set X β†’ ((x : X) β†’ is-set (A x)) β†’ 𝓀 βŠ” π“₯ Μ‡
  TAC X A i j = βˆ₯ ((x : X) β†’ βˆ₯ A x βˆ₯ β†’ A x)βˆ₯

  TChoice : βˆ€ 𝓀 β†’ 𝓀 ⁺ Μ‡
  TChoice 𝓀 = (X : 𝓀 Μ‡ ) (A : X β†’ 𝓀 Μ‡ ) (i : is-set X) (j : (x : X) β†’ is-set (A x))
            β†’ TAC X A i j

  IChoice-gives-TChoice : IChoice 𝓀 β†’ TChoice 𝓀
  IChoice-gives-TChoice {𝓀} iac X A i j = Ξ³
   where
    B : (x : X) β†’ βˆ₯ A x βˆ₯ β†’ 𝓀 Μ‡
    B x s = A x

    k : (x : X) (s : βˆ₯ A x βˆ₯) β†’ is-set (B x s)
    k x s = j x

    l : (x : X) β†’ is-set βˆ₯ A x βˆ₯
    l x = subsingletons-are-sets βˆ₯ A x βˆ₯ βˆ₯βˆ₯-is-subsingleton

    m : (x : X) β†’  is-set (βˆ₯ A x βˆ₯ β†’ A x)
    m x = Ξ -is-set hfe (Ξ» s β†’ j x)

    Ο† : (x : X) β†’ βˆ₯ (βˆ₯ A x βˆ₯ β†’ A x) βˆ₯
    Ο† x = iac βˆ₯ A x βˆ₯ (B x) (l x) (k x) (𝑖𝑑 βˆ₯ A x βˆ₯)

    Ξ³ : βˆ₯ ((x : X) β†’ βˆ₯ A x βˆ₯ β†’ A x)βˆ₯
    Ξ³ = iac X (Ξ» x β†’ βˆ₯ A x βˆ₯ β†’ A x) i m Ο†

  TChoice-gives-IChoice : TChoice 𝓀 β†’ IChoice 𝓀
  TChoice-gives-IChoice tac X A i j = Ξ³
   where
    Ξ³ : ((x : X) β†’ βˆ₯ A x βˆ₯) β†’ βˆ₯ Ξ  A βˆ₯
    Ξ³ g = βˆ₯βˆ₯-functor Ο† (tac X A i j)
     where
      Ο† : ((x : X) β†’ βˆ₯ A x βˆ₯ β†’ A x) β†’ Ξ  A
      Ο† f x = f x (g x)

  decidable-equality-criterion : {X : 𝓀 Μ‡ } (Ξ± : 𝟚 β†’ X)
                               β†’ ((x : X) β†’ (βˆƒ n κž‰ 𝟚 , Ξ± n ＝ x)
                                          β†’ (Ξ£ n κž‰ 𝟚 , Ξ± n ＝ x))
                               β†’ decidable (Ξ± β‚€ ＝ Ξ± ₁)

  decidable-equality-criterion Ξ± c = Ξ³ d
   where
    r : 𝟚 β†’ image Ξ±
    r = corestriction Ξ±

    Οƒ : (y : image Ξ±) β†’ Ξ£ n κž‰ 𝟚 , r n ＝ y
    Οƒ (x , t) = f u
     where
      u : Ξ£ n κž‰ 𝟚 , Ξ± n ＝ x
      u = c x t

      f : (Ξ£ n κž‰ 𝟚 , Ξ± n ＝ x) β†’ Ξ£ n κž‰ 𝟚 , r n ＝ (x , t)
      f (n , p) = n , to-subtype-＝ (Ξ» _ β†’ βˆƒ-is-subsingleton) p

    s : image Ξ± β†’ 𝟚
    s y = pr₁ (Οƒ y)

    Ξ· : (y : image Ξ±) β†’ r (s y) ＝ y
    Ξ· y = prβ‚‚ (Οƒ y)

    l : left-cancellable s
    l = sections-are-lc s (r , Ξ·)

    Ξ±r : {m n : 𝟚} β†’ Ξ± m ＝ Ξ± n β†’ r m ＝ r n
    Ξ±r p = to-subtype-＝ (Ξ» _ β†’ βˆƒ-is-subsingleton) p

    rΞ± : {m n : 𝟚} β†’ r m ＝ r n β†’ Ξ± m ＝ Ξ± n
    rΞ± = ap pr₁

    Ξ±s : {m n : 𝟚} β†’ Ξ± m ＝ Ξ± n β†’ s (r m) ＝ s (r n)
    Ξ±s p = ap s (Ξ±r p)

    sΞ± : {m n : 𝟚} β†’ s (r m) ＝ s (r n) β†’ Ξ± m ＝ Ξ± n
    sΞ± p = rΞ± (l p)

    Ξ³ : decidable (s (r β‚€) ＝ s (r ₁)) β†’ decidable (Ξ± β‚€ ＝ Ξ± ₁)
    Ξ³ (inl p) = inl (sΞ± p)
    Ξ³ (inr u) = inr (contrapositive Ξ±s u)

    d : decidable (s (r β‚€) ＝ s (r ₁))
    d = 𝟚-has-decidable-equality (s (r β‚€)) (s (r ₁))

  choice-gives-decidable-equality : TChoice 𝓀
                                  β†’ (X : 𝓀 Μ‡ ) β†’ is-set X β†’ has-decidable-equality X

  choice-gives-decidable-equality {𝓀} tac X i xβ‚€ x₁ = Ξ³
   where
    Ξ± : 𝟚 β†’ X
    Ξ± β‚€ = xβ‚€
    Ξ± ₁ = x₁

    A : X β†’ 𝓀 Μ‡
    A x = Ξ£ n κž‰ 𝟚 , Ξ± n ＝ x

    l : is-subsingleton (decidable (xβ‚€ ＝ x₁))
    l = +-is-subsingleton' hunapply (i (Ξ± β‚€) (Ξ± ₁))

    Ξ΄ : βˆ₯ ((x : X) β†’ βˆ₯ A x βˆ₯ β†’ A x)βˆ₯ β†’ decidable (xβ‚€ ＝ x₁)
    Ξ΄ = βˆ₯βˆ₯-recursion l (decidable-equality-criterion Ξ±)

    j : (x : X) β†’ is-set (A x)
    j x = subsets-of-sets-are-sets 𝟚 (Ξ» n β†’ Ξ± n ＝ x) 𝟚-is-set (Ξ» n β†’ i (Ξ± n) x)

    h : βˆ₯ ((x : X) β†’ βˆ₯ A x βˆ₯ β†’ A x)βˆ₯
    h = tac X A i j

    Ξ³ : decidable (xβ‚€ ＝ x₁)
    Ξ³ = Ξ΄ h

  choice-gives-EM : propext 𝓀 β†’ TChoice (𝓀 ⁺) β†’ EM 𝓀
  choice-gives-EM {𝓀} pe tac = em
   where
    ⊀ : Ξ© 𝓀
    ⊀ = (Lift 𝓀 πŸ™ , equiv-to-subsingleton (Lift-≃ πŸ™) πŸ™-is-subsingleton)

    Ξ΄ : (Ο‰ : Ξ© 𝓀) β†’ decidable (⊀ ＝ Ο‰)
    Ξ΄ = choice-gives-decidable-equality tac (Ξ© 𝓀) (Ξ©-is-set hunapply pe) ⊀

    em : (P : 𝓀 Μ‡ ) β†’ is-subsingleton P β†’ P + Β¬ P
    em P i = Ξ³ (Ξ΄ (P , i))
     where
      Ξ³ : decidable (⊀ ＝ (P , i)) β†’ P + Β¬ P

      Ξ³ (inl r) = inl (Idβ†’fun s (lift ⋆))
       where
        s : Lift 𝓀 πŸ™ ＝ P
        s = ap pr₁ r

      Ξ³ (inr n) = inr (contrapositive f n)
       where
        f : P β†’ ⊀ ＝ P , i
        f p = Ξ©-ext hunapply pe (Ξ» (_ : Lift 𝓀 πŸ™) β†’ p) (Ξ» (_ : P) β†’ lift ⋆)

  global-choice : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
  global-choice 𝓀 = (X : 𝓀 Μ‡ ) β†’ X + is-empty X

  global-βˆ₯βˆ₯-choice : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
  global-βˆ₯βˆ₯-choice 𝓀 = (X : 𝓀 Μ‡ ) β†’ βˆ₯ X βˆ₯ β†’ X

  open exit-βˆ₯βˆ₯ pt hfe

  global-choice-gives-wconstant : global-choice 𝓀
                                β†’ (X : 𝓀 Μ‡ ) β†’ wconstant-endomap X

  global-choice-gives-wconstant g X = decidable-has-wconstant-endomap (g X)

  global-choice-gives-global-βˆ₯βˆ₯-choice : global-choice  𝓀
                                       β†’ global-βˆ₯βˆ₯-choice 𝓀

  global-choice-gives-global-βˆ₯βˆ₯-choice {𝓀} c X = Ξ³ (c X)
   where
    Ξ³ : X + is-empty X β†’ βˆ₯ X βˆ₯ β†’ X
    Ξ³ (inl x) s = x
    Ξ³ (inr n) s = !𝟘 X (βˆ₯βˆ₯-recursion 𝟘-is-subsingleton n s)

  global-βˆ₯βˆ₯-choice-gives-all-types-are-sets : global-βˆ₯βˆ₯-choice 𝓀
                                            β†’ (X : 𝓀 Μ‡ ) β†’ is-set  X

  global-βˆ₯βˆ₯-choice-gives-all-types-are-sets {𝓀} c X =
    types-with-wconstant-＝-endomaps-are-sets X
        (Ξ» x y β†’ βˆ₯βˆ₯-choice-function-gives-wconstant-endomap (c (x ＝ y)))

  global-βˆ₯βˆ₯-choice-gives-universe-is-set : global-βˆ₯βˆ₯-choice (𝓀 ⁺)
                                         β†’ is-set (𝓀 Μ‡ )

  global-βˆ₯βˆ₯-choice-gives-universe-is-set {𝓀} c =
    global-βˆ₯βˆ₯-choice-gives-all-types-are-sets c (𝓀 Μ‡ )

  global-βˆ₯βˆ₯-choice-gives-choice : global-βˆ₯βˆ₯-choice 𝓀
                                β†’ TChoice 𝓀

  global-βˆ₯βˆ₯-choice-gives-choice {𝓀} c X A i j = ∣(Ξ» x β†’ c (A x))∣

  global-βˆ₯βˆ₯-choice-gives-EM : propext 𝓀
                           β†’ global-βˆ₯βˆ₯-choice (𝓀 ⁺)
                           β†’ EM  𝓀

  global-βˆ₯βˆ₯-choice-gives-EM {𝓀} pe c =
    choice-gives-EM pe (global-βˆ₯βˆ₯-choice-gives-choice c)

  global-βˆ₯βˆ₯-choice-gives-global-choice : propext 𝓀
                                      β†’ global-βˆ₯βˆ₯-choice 𝓀
                                      β†’ global-βˆ₯βˆ₯-choice (𝓀 ⁺)
                                      β†’ global-choice 𝓀

  global-βˆ₯βˆ₯-choice-gives-global-choice {𝓀} pe c c⁺ X = Ξ³
   where
    d : decidable βˆ₯ X βˆ₯
    d = global-βˆ₯βˆ₯-choice-gives-EM pe c⁺ βˆ₯ X βˆ₯ βˆ₯βˆ₯-is-subsingleton

    f : decidable βˆ₯ X βˆ₯ β†’ X + is-empty X
    f (inl i) = inl (c X i)
    f (inr Ο†) = inr (contrapositive ∣_∣ Ο†)

    Ξ³ : X + is-empty X
    Ξ³ = f d

  Global-Choice Global-βˆ₯βˆ₯-Choice : 𝓀ω
  Global-Choice    = βˆ€ 𝓀 β†’ global-choice  𝓀
  Global-βˆ₯βˆ₯-Choice = βˆ€ 𝓀 β†’ global-βˆ₯βˆ₯-choice 𝓀

  Global-Choice-gives-Global-βˆ₯βˆ₯-Choice : Global-Choice β†’ Global-βˆ₯βˆ₯-Choice
  Global-Choice-gives-Global-βˆ₯βˆ₯-Choice c 𝓀 =
    global-choice-gives-global-βˆ₯βˆ₯-choice (c 𝓀)

  Global-βˆ₯βˆ₯-Choice-gives-Global-Choice : global-propext
                                       β†’ Global-βˆ₯βˆ₯-Choice β†’ Global-Choice

  Global-βˆ₯βˆ₯-Choice-gives-Global-Choice pe c 𝓀 =
    global-βˆ₯βˆ₯-choice-gives-global-choice pe (c 𝓀) (c (𝓀 ⁺))

  global-βˆ₯βˆ₯-choice-inconsistent-with-univalence : Global-βˆ₯βˆ₯-Choice
                                               β†’ Univalence
                                               β†’ 𝟘

  global-βˆ₯βˆ₯-choice-inconsistent-with-univalence g ua = Ξ³ (g 𝓀₁) (ua 𝓀₀)
   where
    open example-of-a-nonset

    Ξ³ : global-βˆ₯βˆ₯-choice 𝓀₁ β†’ is-univalent 𝓀₀ β†’ 𝟘
    Ξ³ g ua = 𝓀₀-is-not-a-set ua (global-βˆ₯βˆ₯-choice-gives-universe-is-set g)

  global-choice-inconsistent-with-univalence : Global-Choice
                                             β†’ Univalence
                                             β†’ 𝟘

  global-choice-inconsistent-with-univalence g =
    global-βˆ₯βˆ₯-choice-inconsistent-with-univalence
      (Global-Choice-gives-Global-βˆ₯βˆ₯-Choice g)

  global-choice-gives-all-types-are-sets : global-choice 𝓀
                                         β†’ (X : 𝓀 Μ‡ ) β†’ is-set  X

  global-choice-gives-all-types-are-sets {𝓀} c X = hedberg (Ξ» x y β†’ c (x ＝ y))

\end{code}