Martin Escardo, November-December 2019

We consider a situation in which anonymous existence gives explicit
existence.

\begin{code}

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

module Fin.Choice where

open import Fin.Order
open import Fin.Type
open import MLTT.Spartan
open import NotionsOfDecidability.Complemented
open import NotionsOfDecidability.Decidable
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons

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

 open PropositionalTruncation pt

 Σ-min-from-∃ : FunExt → {n : ℕ} (A : Fin n → 𝓤 ̇ )
             → is-complemented A
             → is-prop-valued-family A
             → ∃ A
             → Σ-min A

 Σ-min-from-∃ fe A δ h = ∥∥-rec (Σ-min-is-prop fe A h) (Σ-gives-Σ-min A δ)

 Fin-Σ-from-∃' : FunExt
               → {n : ℕ} (A : Fin n → 𝓤 ̇ )
               → is-complemented A
               → is-prop-valued-family A
               → ∃ A
               → Σ A

 Fin-Σ-from-∃' fe A δ h e = Σ-min-gives-Σ A (Σ-min-from-∃ fe A δ h e)

\end{code}

But the prop-valuedness of A is actually not needed, with more work:

\begin{code}

 Fin-Σ-from-∃ : FunExt
              → {n : ℕ} (A : Fin n → 𝓤 ̇ )
              → is-complemented A
              → ∃ A
              → Σ A

 Fin-Σ-from-∃ {𝓤} fe {n} A δ e = γ
  where
   A' : Fin n → 𝓤 ̇
   A' x = ∥ A x ∥

   δ' : is-complemented A'
   δ' x = d (δ x)
    where
     d : is-decidable (A x) → is-decidable (A' x)
     d (inl a) = inl ∣ a ∣
     d (inr u) = inr (∥∥-rec 𝟘-is-prop u)

   f : Σ A → Σ A'
   f (x , a) = x , ∣ a ∣

   e' : ∃ A'
   e' = ∥∥-functor f e

   σ' : Σ A'
   σ' = Fin-Σ-from-∃' fe A' δ' (λ x → ∥∥-is-prop) e'

   g : Σ A' → Σ A
   g (x , a') = x , ¬¬-elim (δ x) (λ (u : ¬ A x) → ∥∥-rec 𝟘-is-prop u a')

   γ : Σ A
   γ = g σ'

\end{code}