Skip to content

Commit

Permalink
Merge branch 'master' of github.com:martinescardo/TypeTopology
Browse files Browse the repository at this point in the history
  • Loading branch information
@ayberkt
ayberkt committed Sep 18, 2024
2 parents 0b46052 + a250699 commit 4a4747e
Show file tree
Hide file tree
Showing 7 changed files with 151 additions and 63 deletions.
146 changes: 115 additions & 31 deletions source/Naturals/RootsTruncation.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ open import Naturals.Order
open import Notation.Order
open import UF.Hedberg
open import UF.KrausLemma
open import UF.KrausLemma
open import UF.PropTrunc
open import UF.Subsingletons

Expand Down Expand Up @@ -145,7 +146,8 @@ be empty, and still the function is well defined.
r = to-Σ-＝ (q , isolated-Id-is-prop z z-is-isolated _ _ _)

Root-has-prop-truncation : (α : ℕ → Z) → ∀ 𝓥 → has-prop-truncation 𝓥 (Root α)
Root-has-prop-truncation α = collapsible-has-prop-truncation (μρ α , μρ-constant α)
Root-has-prop-truncation α = collapsible-has-prop-truncation
(μρ α , μρ-constant α)

\end{code}

Expand Down Expand Up @@ -185,18 +187,10 @@ root truncations using the above technique.
module exit-Roots-truncation (pt : propositional-truncations-exist) where

open PropositionalTruncation pt
open split-support-and-collapsibility pt

exit-Root-truncation : (α : ℕ → Z) → (∃ n ꞉ ℕ , α n ＝ z) → Σ n ꞉ ℕ , α n ＝ z
exit-Root-truncation α = h ∘ g
where
f : (Σ n ꞉ ℕ , α n ＝ z) → fix (μρ α)
f = to-fix (μρ α) (μρ-constant α)

g : ∥(Σ n ꞉ ℕ , α n ＝ z)∥ → fix (μρ α)
g = ∥∥-rec (fix-is-prop (μρ α) (μρ-constant α)) f

h : fix (μρ α) → Σ n ꞉ ℕ , α n ＝ z
h = from-fix (μρ α)
exit-Root-truncation α = collapsible-gives-split-support (μρ α , μρ-constant α)

\end{code}

Expand Down Expand Up @@ -246,33 +240,123 @@ minimal-witness A A-is-complemented (n , aₙ) = m , aₘ , m-is-minimal-witness

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

open PropositionalTruncation pt
open PropositionalTruncation pt

exit-truncation : (A : ℕ → 𝓤 ̇ )
→ is-complemented A
→ (∃ n ꞉ ℕ , A n)
→ Σ n ꞉ ℕ , A n
exit-truncation A A-is-complemented e = IV
where
open Roots-truncation 𝟚 ₀ (λ b → 𝟚-is-discrete b ₀)
open exit-Roots-truncation pt

α : ℕ → 𝟚
α = characteristic-map A A-is-complemented

I : (Σ n ꞉ ℕ , A n) → Σ n ꞉ ℕ , α n ＝ ₀
I (n , a) = n , characteristic-map-property₀-back A A-is-complemented n a

e' : ∃ n ꞉ ℕ , α n ＝ ₀
e' = ∥∥-functor I e

II : Σ n ꞉ ℕ , α n ＝ ₀
II = exit-Root-truncation α e'

III : (Σ n ꞉ ℕ , α n ＝ ₀) → Σ n ꞉ ℕ , A n
III (n , e) = n , characteristic-map-property₀ A A-is-complemented n e

IV : Σ n ꞉ ℕ , A n
IV = III II

\end{code}

exit-truncation : (A : ℕ → 𝓤 ̇ )
→ is-complemented A
→ (∃ n ꞉ ℕ , A n)
→ Σ n ꞉ ℕ , A n
exit-truncation A A-is-complemented e = IV
Added 18th September 2024. The following "exit-truncation lemma"
generalizes the above development with a simpler proof. But this
result was already known in

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}

private
abstract
minimal-pair' : (A : ℕ → 𝓤 ̇ )
→ ((n : ℕ) → A n → (k : ℕ) → k < n → is-decidable (A k))
→ (n : ℕ)
→ A n
→ Σ (k , aₖ) ꞉ Σ A , ((i : ℕ) → A i → k ≤ i)
minimal-pair' A δ 0 a₀ = (0 , a₀) , (λ i aᵢ → zero-least i)
minimal-pair' A δ (succ n) aₙ₊₁ = II
where
open Roots-truncation 𝟚 ₀ (λ b → 𝟚-is-discrete b ₀)
open exit-Roots-truncation pt
IH : Σ (j , aⱼ₊₁) ꞉ Σ (A ∘ succ) , ((i : ℕ) → A (succ i) → j ≤ i)
IH = minimal-pair' (A ∘ succ) (λ n aₙ₊₁ j → δ (succ n) aₙ₊₁ (succ j)) n aₙ₊₁

I : type-of IH
→ Σ (k , aₖ) ꞉ Σ A , ((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ᵢ₊₁

α : ℕ → 𝟚
α = characteristic-map A A-is-complemented
II : Σ (k , aⱼ) ꞉ Σ A , ((i : ℕ) → A i → k ≤ i)
II = I IH

I : (Σ n ꞉ ℕ , A n) → Σ n ꞉ ℕ , α n ＝ ₀
I (n , a) = n , characteristic-map-property₀-back A A-is-complemented n a
module _ (A : ℕ → 𝓤 ̇ )
(δ : (n : ℕ) → A n → (k : ℕ) → k < n → is-decidable (A k))
where

minimal-pair : Σ A → Σ A
minimal-pair (n , aₙ) = pr₁ (minimal-pair' A δ n aₙ)

minimal-number : Σ A → ℕ
minimal-number = pr₁ ∘ minimal-pair

minimal-number-requirement : (σ : Σ A) → A (minimal-number σ)
minimal-number-requirement = pr₂ ∘ minimal-pair

e' : ∃ n ꞉ ℕ , α n ＝ ₀
e' = ∥∥-functor I e
minimality : (σ : Σ A) → (i : ℕ) → A i → minimal-number σ ≤ i
minimality (n , aₙ) = pr₂ (minimal-pair' A δ n aₙ)

II : Σ n ꞉ ℕ , α n ＝ ₀
II = exit-Root-truncation α e'
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 σ)))

III : (Σ n ꞉ ℕ , α n ＝ ₀) → Σ n ꞉ ℕ , A n
III (n , e) = n , characteristic-map-property₀ A A-is-complemented n e
module exit-truncations' (pt : propositional-truncations-exist) where

IV : Σ n ꞉ ℕ , A n
IV = III II
open PropositionalTruncation pt
open split-support-and-collapsibility pt

exit-truncation⁺ : (A : ℕ → 𝓤 ̇ )
→ is-prop-valued-family A
→ ((n : ℕ) → A n → (k : ℕ) → k < n → is-decidable (A k))
→ ∥ Σ A ∥ → Σ A
exit-truncation⁺ A A-prop-valued δ =
collapsible-gives-split-support
(minimal-pair A δ , minimal-pair-wconstant A δ A-prop-valued)

\end{code}

This is not quite a generalization of the previous result, because the
previous result doesn't have the assumption that A is prop-valued.

TODO. Can we remove the prop-valuedness assumption?
4 changes: 4 additions & 0 deletions source/NotionsOfDecidability/Decidable.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -315,6 +315,10 @@ and it has split support.
∥∥⟨⟩-is-prop (inl x) = 𝟙-is-prop
∥∥⟨⟩-is-prop (inr ν) = 𝟘-is-prop

∥∥⟨⟩-is-decidable : {X : 𝓤 ̇ } (δ : is-decidable X) → is-decidable ∥ X ∥⟨ δ ⟩
∥∥⟨⟩-is-decidable (inl x) = 𝟙-is-decidable
∥∥⟨⟩-is-decidable (inr ν) = 𝟘-is-decidable

∣_∣⟨_⟩ : {X : 𝓤 ̇ } → X → (δ : is-decidable X) → ∥ X ∥⟨ δ ⟩
∣ x ∣⟨ inl _ ⟩ = ⋆
∣ x ∣⟨ inr ν ⟩ = ν x
Expand Down
2 changes: 1 addition & 1 deletion source/Ordinals/NotationInterpretation1.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -495,7 +495,7 @@ module _ (pt : propositional-truncations-exist)
(sum-to-sup-is-surjection (extension (𝓢 ∘ ν)))
(Σ-is-compact∙
(ℕ∞-compact∙ fe₀)
(λ u → prop-tychonoff fe
(λ u → prop-tychonoff (fe 𝓤₀ 𝓤₀)
(ℕ-to-ℕ∞-is-embedding fe₀ u)
(λ (i , _) → 𝓢-compact∙ (ν i))))
σ : (ν : OE) → ⟨ Κ ν ⟩ → ⟨ 𝓢 ν ⟩
Expand Down
26 changes: 13 additions & 13 deletions source/Taboos/LPO.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ End of addition.

\begin{code}

LPO-is-prop : Fun-Ext → is-prop LPO
LPO-is-prop : funext₀ → is-prop LPO
LPO-is-prop fe = Π-is-prop fe f
where
a : (x : ℕ∞) → is-prop (Σ n ꞉ ℕ , x ＝ ι n)
Expand All @@ -83,7 +83,7 @@ formulation.

\begin{code}

LPO-gives-compact-ℕ : funext 𝓤₀ 𝓤₀ → LPO → is-compact ℕ
LPO-gives-compact-ℕ : funext₀ → LPO → is-compact ℕ
LPO-gives-compact-ℕ fe ℓ β = γ
where
A = (Σ n ꞉ ℕ , β n ＝ ₀) + (Π n ꞉ ℕ , β n ＝ ₁)
Expand Down Expand Up @@ -126,7 +126,7 @@ LPO-gives-compact-ℕ fe ℓ β = γ
γ : A
γ = cases a b d

compact-ℕ-gives-LPO : funext 𝓤₀ 𝓤₀ → is-compact ℕ → LPO
compact-ℕ-gives-LPO : funext₀ → is-compact ℕ → LPO
compact-ℕ-gives-LPO fe κ x = γ
where
A = is-decidable (Σ n ꞉ ℕ , x ＝ ι n)
Expand Down Expand Up @@ -180,16 +180,16 @@ knowing whether LPO holds or not!

open import TypeTopology.PropTychonoff

[LPO→ℕ]-is-compact∙ : FunExt → is-compact∙ (LPO → ℕ)
[LPO→ℕ]-is-compact∙ fe = prop-tychonoff-corollary' fe (LPO-is-prop (fe _ _)) f
[LPO→ℕ]-is-compact∙ : funext₀ → is-compact∙ (LPO → ℕ)
[LPO→ℕ]-is-compact∙ fe = prop-tychonoff-corollary' fe (LPO-is-prop fe) f
where
f : LPO → is-compact∙ ℕ
f lpo = compact-pointed-types-are-compact∙ (LPO-gives-compact-ℕ (fe 𝓤₀ 𝓤₀) lpo) 0
f lpo = compact-pointed-types-are-compact∙ (LPO-gives-compact-ℕ fe lpo) 0

[LPO→ℕ]-is-compact : FunExt → is-compact (LPO → ℕ)
[LPO→ℕ]-is-compact : funext₀ → is-compact (LPO → ℕ)
[LPO→ℕ]-is-compact fe = compact∙-types-are-compact ([LPO→ℕ]-is-compact∙ fe)

[LPO→ℕ]-is-Compact : FunExt → is-Compact (LPO → ℕ) {𝓤}
[LPO→ℕ]-is-Compact : funext₀ → is-Compact (LPO → ℕ) {𝓤}
[LPO→ℕ]-is-Compact fe = compact-types-are-Compact ([LPO→ℕ]-is-compact fe)

\end{code}
Expand All @@ -204,7 +204,7 @@ open import Naturals.Properties
open import UF.DiscreteAndSeparated

[LPO→ℕ]-discrete-gives-¬LPO-decidable
: funext 𝓤₀ 𝓤₀
: funext₀
→ is-discrete (LPO → ℕ)
→ is-decidable (¬ LPO)
[LPO→ℕ]-discrete-gives-¬LPO-decidable fe =
Expand Down Expand Up @@ -241,7 +241,7 @@ embedding ι𝟙 : ℕ + 𝟙 → ℕ∞ has a section:
ι𝟙-inverse .(ι n) (inl (n , refl)) = inl n
ι𝟙-inverse u (inr g) = inr ⋆

LPO-gives-has-section-ι𝟙 : funext 𝓤₀ 𝓤₀ → LPO → Σ s ꞉ (ℕ∞ → ℕ + 𝟙) , ι𝟙 ∘ s ∼ id
LPO-gives-has-section-ι𝟙 : funext₀ → LPO → Σ s ꞉ (ℕ∞ → ℕ + 𝟙) , ι𝟙 ∘ s ∼ id
LPO-gives-has-section-ι𝟙 fe lpo = s , ε
where
s : ℕ∞ → ℕ + 𝟙
Expand All @@ -254,7 +254,7 @@ LPO-gives-has-section-ι𝟙 fe lpo = s , ε
ε : ι𝟙 ∘ s ∼ id
ε u = φ u (lpo u)

LPO-gives-ι𝟙-is-equiv : funext 𝓤₀ 𝓤₀ → LPO → is-equiv ι𝟙
LPO-gives-ι𝟙-is-equiv : funext₀ → LPO → is-equiv ι𝟙
LPO-gives-ι𝟙-is-equiv fe lpo = embeddings-with-sections-are-equivs ι𝟙
(ι𝟙-is-embedding fe)
(LPO-gives-has-section-ι𝟙 fe lpo)
Expand All @@ -266,13 +266,13 @@ Added 3rd September 2024.

open import Taboos.WLPO

LPO-gives-WLPO : funext 𝓤₀ 𝓤₀ → LPO → WLPO
LPO-gives-WLPO : funext₀ → LPO → WLPO
LPO-gives-WLPO fe lpo u =
Cases (lpo u)
(λ (n , p) → inr (λ {refl → ∞-is-not-finite n p}))
(λ ν → inl (not-finite-is-∞ fe (λ n p → ν (n , p))))

¬WLPO-gives-¬LPO : funext 𝓤₀ 𝓤₀ → ¬ WLPO → ¬ LPO
¬WLPO-gives-¬LPO : funext₀ → ¬ WLPO → ¬ LPO
¬WLPO-gives-¬LPO fe = contrapositive (LPO-gives-WLPO fe)

\end{code}
5 changes: 3 additions & 2 deletions source/TypeTopology/ExtendedSumCompact.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ open import UF.Embeddings
module TypeTopology.ExtendedSumCompact (fe : FunExt) where

open import TypeTopology.CompactTypes
open import TypeTopology.PropTychonoff fe
open import TypeTopology.PropTychonoff

open import InjectiveTypes.Blackboard fe

Expand All @@ -23,6 +23,7 @@ extended-sum-compact∙ : {X : 𝓤 ̇ }
→ ((x : X) → is-compact∙ (Y x))
→ is-compact∙ K
→ is-compact∙ (Σ (Y / j))
extended-sum-compact∙ j e ε δ = Σ-is-compact∙ δ (λ k → prop-tychonoff (e k) (ε ∘ pr₁))
extended-sum-compact∙ {𝓤} {𝓥} {𝓦} j e ε δ =
Σ-is-compact∙ δ (λ k → prop-tychonoff (fe (𝓤 ⊔ 𝓥) 𝓦) (e k) (ε ∘ pr₁))

\end{code}
24 changes: 13 additions & 11 deletions source/TypeTopology/PropTychonoff.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,21 +40,21 @@ The point is that

open import MLTT.Spartan

open import UF.FunExt

module TypeTopology.PropTychonoff (fe : FunExt) where
module TypeTopology.PropTychonoff where

open import MLTT.Two-Properties
open import TypeTopology.CompactTypes
open import UF.Equiv
open import UF.FunExt
open import UF.PropIndexedPiSigma
open import UF.Subsingletons

prop-tychonoff : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
prop-tychonoff : funext 𝓤 𝓥
→ {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ is-prop X
→ ((x : X) → is-compact∙ (Y x))
→ is-compact∙ (Π Y)
prop-tychonoff {𝓤} {𝓥} {X} {Y} X-is-prop ε p = γ
prop-tychonoff {𝓤} {𝓥} fe {X} {Y} X-is-prop ε p = γ
where
have-ε : (x : X) → is-compact∙ (Y x)
have-ε = ε
Expand All @@ -63,7 +63,7 @@ prop-tychonoff {𝓤} {𝓥} {X} {Y} X-is-prop ε p = γ
have-p = p

𝕗 : (x : X) → Π Y ≃ Y x
𝕗 = prop-indexed-product (fe 𝓤 𝓥) X-is-prop
𝕗 = prop-indexed-product fe X-is-prop

\end{code}

Expand Down Expand Up @@ -178,7 +178,7 @@ We get the same conclusion if X is empty:
φ₀-is-universal-witness-assuming-X-empty
: (X → 𝟘) → p φ₀ ＝ ₁ → (φ : Π Y) → p φ ＝ ₁
φ₀-is-universal-witness-assuming-X-empty u r φ =
p φ ＝⟨ ap p (dfunext (fe 𝓤 𝓥) (λ x → unique-from-𝟘 (u x))) ⟩
p φ ＝⟨ ap p (dfunext fe (λ x → unique-from-𝟘 (u x))) ⟩
p φ₀ ＝⟨ r ⟩
₁ ∎

Expand Down Expand Up @@ -255,11 +255,12 @@ A particular case is the following:

\begin{code}

prop-tychonoff-corollary : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
prop-tychonoff-corollary : funext 𝓤 𝓥
→ {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-prop X
→ is-compact∙ Y
→ is-compact∙ (X → Y)
prop-tychonoff-corollary X-is-prop ε = prop-tychonoff X-is-prop (λ x → ε)
prop-tychonoff-corollary fe X-is-prop ε = prop-tychonoff fe X-is-prop (λ x → ε)

\end{code}

Expand All @@ -271,11 +272,12 @@ Better (9 Sep 2015):

\begin{code}

prop-tychonoff-corollary' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
prop-tychonoff-corollary' : funext 𝓤 𝓥
→ {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-prop X
→ (X → is-compact∙ Y)
→ is-compact∙ (X → Y)
prop-tychonoff-corollary' = prop-tychonoff
prop-tychonoff-corollary' fe = prop-tychonoff fe

\end{code}

Expand Down
Loading

0 comments on commit 4a4747e

Please sign in to comment.