Martin Escardo, 17th August 2024 and 18th September 2024.
A develop and generalize a result from 2013/03/13 first advertised in
the IAS Univalent Foundations mailing list in response to a question
by Andrej Bauer [1]:
If A : ℕ → 𝓤 is a family of decidable types,
then
∥ Σ n ꞉ ℕ , A n ∥ → Σ n : ℕ , A n.
This may seem surprising at first sight. The original proof in [1]
uses function extensionality and the assumption that A is
proposition-valued to show that the type
A m × ((k : ℕ) → A k → m ≤ k
is a proposition for any m. But, using the results of [2] (or its
extended version [3]), we can remove both assumptions.
Moreover, in [4] we show that, more generally, if A : ℕ → 𝓤 is a
family of propositions such that A (n + 1) implies that A n is
decidable, then
∥ Σ n ꞉ ℕ , A n ∥ → Σ n : ℕ , A n,
again with a proof that assumes function extensionality. Here, using
[2], we are able to remove the assumption of function extensionlity,
but not that assumption that A is proposition-valued.
Moreover, we can construct the propositional truncation of the type
Σ n ꞉ ℕ , A n in pure Spartan MLTT without assuming that propositional
truncations exist in general, by considering the type of fixed points
of a minimization endomap of Σ n ꞉ ℕ , A n. See the module UF.ExitPropTrunc.
1. Martin Escardo. 2013/03/13 message to the IAS Univalent Foundations
mailing list.
https://groups.google.com/g/univalent-foundations/c/SA0dzenV1G4/m/d5iIGdKKNxMJ
2. Nicolai Kraus, Martín Escardó, Thierry Coquand & Thorsten Altenkirch.
Generalizations of Hedberg’s Theorem.
TLCA 2013
https://doi.org/10.1007/978-3-642-38946-7_14
3. Nicolai Kraus, Martín Escardó, Thierry Coquand & Thorsten Altenkirch.
Notions of Anonymous Existence in Martin-Löf Type Theory.
Logical Methods in Computer Science, March 24, 2017, Volume 13, Issue 1.
https://doi.org/10.23638/LMCS-13(1:15)2017
4. Martín H. Escardó and Chuangjie Xu. The inconsistency of a
Brouwerian continuity principle with the Curry-Howard
interpretation. 13th International Conference on Typed Lambda
Calculi and Applications (TLCA 2015).
https://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=15006
https://doi.org/10.4230/LIPIcs.TLCA.2015.153
Although it was presented with a different proof that assumes function
extensionlity.
\begin{code}
{-# OPTIONS --safe --without-K #-}
module Naturals.ExitTruncation where
open import MLTT.Spartan
open import Naturals.Order
open import Notation.Order
open import NotionsOfDecidability.Decidable
open import UF.Hedberg
open import UF.ExitPropTrunc
open import UF.PropTrunc
open import UF.Subsingletons
module _ (A : ℕ → 𝓤 ̇ )
(δ : (n : ℕ) → A n → (k : ℕ) → k < n → is-decidable (A k))
where
minimal-witness⁺ : (Σ n ꞉ ℕ , A n)
→ Σ k ꞉ ℕ , (A k × ((i : ℕ) → A i → k ≤ i))
minimal-witness⁺ = uncurry (μ A δ)
where
μ : (A : ℕ → 𝓤 ̇ )
→ ((n : ℕ) → A n → (k : ℕ) → k < n → is-decidable (A k))
→ (n : ℕ)
→ A n
→ Σ k ꞉ ℕ , (A k × ((i : ℕ) → A i → k ≤ i))
μ A δ 0 a₀ = 0 , a₀ , (λ i aᵢ → zero-least i)
μ A δ (succ n) aₙ₊₁ = II
where
IH : Σ j ꞉ ℕ , ((A (succ j) × ((i : ℕ) → A (succ i) → j ≤ i)))
IH = μ (A ∘ succ) (λ n aₙ₊₁ j → δ (succ n) aₙ₊₁ (succ j)) n aₙ₊₁
I : type-of IH
→ Σ k ꞉ ℕ , A k × ((i : ℕ) → A i → k ≤ i)
I (j , aⱼ₊₁ , b) =
Cases (δ (succ n) aₙ₊₁ 0 (zero-least j))
(λ (a₀ : A 0) → (0 , a₀ , (λ i aᵢ → zero-least i)))
(λ (ν₀ : ¬ A 0) → (succ j , aⱼ₊₁ , I₀ ν₀))
where
I₀ : ¬ A 0 → (i : ℕ) (aᵢ : A i) → j < i
I₀ ν₀ 0 a₀ = 𝟘-elim (ν₀ a₀)
I₀ ν₀ (succ i) aᵢ₊₁ = b i aᵢ₊₁
II : Σ k ꞉ ℕ , (A k × ((i : ℕ) → A i → k ≤ i))
II = I IH
\end{code}
We name the projections for convenience.
\begin{code}
minimal-number : Σ A → ℕ
minimal-number σ = pr₁ (minimal-witness⁺ σ)
minimal-number-requirement : (σ : Σ A) → A (minimal-number σ)
minimal-number-requirement σ = pr₁ (pr₂ (minimal-witness⁺ σ))
minimality : (σ : Σ A) → (i : ℕ) → A i → minimal-number σ ≤ i
minimality σ = pr₂ (pr₂ (minimal-witness⁺ σ))
minimal-pair : Σ A → Σ A
minimal-pair σ = minimal-number σ , minimal-number-requirement σ
minimal-pair-wconstant : is-prop-valued-family A → wconstant minimal-pair
minimal-pair-wconstant A-prop-valued σ σ' =
to-subtype-＝ A-prop-valued
(need
minimal-number σ ＝ minimal-number σ'
which-is-given-by
≤-anti _ _
(minimality σ (minimal-number σ') (minimal-number-requirement σ'))
(minimality σ' (minimal-number σ) (minimal-number-requirement σ)))
\end{code}
A particular case.
\begin{code}
minimal-witness : (A : ℕ → 𝓤 ̇ )
→ ((n : ℕ) → is-decidable (A n))
→ (Σ n ꞉ ℕ , A n)
→ Σ m ꞉ ℕ , (A m × ((k : ℕ) → A k → m ≤ k))
minimal-witness A δ = minimal-witness⁺ A (λ n aₙ k l → δ k)
\end{code}
We apply the above to exit truncations.
\begin{code}
module exit-truncations (pt : propositional-truncations-exist) where
open PropositionalTruncation pt
open split-support-and-collapsibility pt
module _ (A : ℕ → 𝓤 ̇ )
(A-is-prop-valued : is-prop-valued-family A)
(δ : (n : ℕ) → A n → (k : ℕ) → k < n → is-decidable (A k))
where
exit-truncation⁺ : ∥ Σ A ∥ → Σ A
exit-truncation⁺ = collapsible-gives-split-support
(minimal-pair A δ ,
minimal-pair-wconstant A δ A-is-prop-valued)
\end{code}
Not only can be exit the truncation, but also we can say that the
result is minimal.
\begin{code}
exit-truncation⁺-minimality
: (s : ∥ Σ A ∥) (i : ℕ) → A i → pr₁ (exit-truncation⁺ s) ≤ i
exit-truncation⁺-minimality s = IV
where
I : minimal-pair A δ (exit-truncation⁺ s) ＝ exit-truncation⁺ s
I = exit-prop-trunc-is-fixed
(minimal-pair A δ)
(minimal-pair-wconstant A δ A-is-prop-valued)
s
II : minimal-number A δ (exit-truncation⁺ s) ＝ pr₁ (exit-truncation⁺ s)
II = ap pr₁ I
III : (i : ℕ) → A i → minimal-number A δ (exit-truncation⁺ s) ≤ i
III = minimality A δ (exit-truncation⁺ s)
IV : (i : ℕ) → A i → pr₁ (exit-truncation⁺ s) ≤ i
IV = transport (λ - → (i : ℕ) → A i → - ≤ i) II III
\end{code}
In the following particular case of interest, the prop-valuedness
assumption can be removed.
\begin{code}
module _ (A : ℕ → 𝓤 ̇ )
(d : (n : ℕ) → is-decidable (A n))
where
private
B : ℕ → 𝓤₀ ̇
B n = ∥ A n ∥⟨ d n ⟩
B-is-prop-valued : is-prop-valued-family B
B-is-prop-valued n = ∥∥⟨ d n ⟩-is-prop
δ : (n : ℕ) → B n → (k : ℕ) → k < n → is-decidable (B k)
δ n bₙ k l = ∥∥⟨ d k ⟩-is-decidable
f : Σ A → Σ B
f (n , aₙ) = n , ∣ aₙ ∣⟨ d n ⟩
g : Σ B → Σ A
g (n , bₙ) = (n , ∣∣⟨ d n ⟩-exit bₙ)
exit-truncation : ∥ Σ A ∥ → Σ A
exit-truncation t = g (exit-truncation⁺ B B-is-prop-valued δ (∥∥-functor f t))
exit-truncation-minimality
: (t : ∥ Σ A ∥) (i : ℕ) → A i → pr₁ (exit-truncation t) ≤ i
exit-truncation-minimality t i a =
exit-truncation⁺-minimality
B
B-is-prop-valued
δ
(∥∥-functor f t)
i
∣ a ∣⟨ d i ⟩
\end{code}
TODO. Can we remove the prop-valuedness assumption in general?
Added 19th September 2024.
The following is useful in practice to fulfill a hypothesis of
exit-truncation⁺.
\begin{code}
regression-lemma₀
: (A : ℕ → 𝓤 ̇ )
→ ((n : ℕ) → A (succ n) → is-decidable (A n))
→ ((n : ℕ) → A n → A (succ n))
→ (n : ℕ) → A (succ n) → is-decidable (A 0)
regression-lemma₀ A f g 0 = f 0
regression-lemma₀ A f g (succ n) = I
where
IH : A (succ (succ n)) → is-decidable (A 1)
IH = regression-lemma₀ (A ∘ succ) (f ∘ succ) (g ∘ succ) n
I : A (succ (succ n)) → is-decidable (A 0)
I a = Cases (IH a)
(λ (a₁ : A 1) → f 0 a₁)
(λ (ν : ¬ A 1) → inr (contrapositive (g 0) ν))
regression-lemma
: (A : ℕ → 𝓤 ̇ )
→ ((n : ℕ) → A (succ n) → is-decidable (A n))
→ ((n : ℕ) → A n → A (succ n))
→ (n : ℕ) → A n → (k : ℕ) → k < n → is-decidable (A k)
regression-lemma A f g 0 a k l = 𝟘-elim l
regression-lemma A f g (succ n) a 0 l = regression-lemma₀ A f g n a
regression-lemma A f g (succ n) a (succ k) l = regression-lemma
(A ∘ succ)
(f ∘ succ)
(g ∘ succ)
n a k l
\end{code}
Notice that these functions don't actually use the full force of the
assumption
(n : ℕ) → A n → A (succ n)
but only its contrapositive. So there is a more general result that
assumes
(n : ℕ) → ¬ A (succ n) → ¬ A n
instead, although I don't think this will ever be needed. If it is, we
can come back here and do a little bit of refactoring.