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.Complemented
open import NotionsOfDecidability.Decidable
open import UF.DiscreteAndSeparated
open import UF.Hedberg
open import UF.KrausLemma
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.