From e8af55e77b60ba209f2ebe99719f5118b3c904d4 Mon Sep 17 00:00:00 2001 From: Martin Escardo Date: Wed, 18 Sep 2024 19:47:01 +0100 Subject: [PATCH] be more parsimonius with function extensionality universe levels --- source/Naturals/RootsTruncation.lagda | 4 +-- source/NotionsOfDecidability/Decidable.lagda | 4 +++ source/Ordinals/NotationInterpretation1.lagda | 2 +- source/Taboos/LPO.lagda | 26 +++++++++---------- source/TypeTopology/ExtendedSumCompact.lagda | 5 ++-- source/TypeTopology/PropTychonoff.lagda | 24 +++++++++-------- .../SigmaDiscreteAndTotallySeparated.lagda | 7 ++--- 7 files changed, 38 insertions(+), 34 deletions(-) diff --git a/source/Naturals/RootsTruncation.lagda b/source/Naturals/RootsTruncation.lagda index 082cb1f5f..5284314cf 100644 --- a/source/Naturals/RootsTruncation.lagda +++ b/source/Naturals/RootsTruncation.lagda @@ -346,11 +346,11 @@ module exit-truncations' (pt : propositional-truncations-exist) where open PropositionalTruncation pt open split-support-and-collapsibility pt - exit-truncation' : (A : ℕ → 𝓤 ̇ ) + 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 δ = + exit-truncation⁺ A A-prop-valued δ = collapsible-gives-split-support (minimal-pair A δ , minimal-pair-wconstant A δ A-prop-valued) diff --git a/source/NotionsOfDecidability/Decidable.lagda b/source/NotionsOfDecidability/Decidable.lagda index 545611458..c180817fa 100644 --- a/source/NotionsOfDecidability/Decidable.lagda +++ b/source/NotionsOfDecidability/Decidable.lagda @@ -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 diff --git a/source/Ordinals/NotationInterpretation1.lagda b/source/Ordinals/NotationInterpretation1.lagda index e0a8bfd9b..9d1eba7a4 100644 --- a/source/Ordinals/NotationInterpretation1.lagda +++ b/source/Ordinals/NotationInterpretation1.lagda @@ -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) → ⟨ Κ ν ⟩ → ⟨ 𝓢 ν ⟩ diff --git a/source/Taboos/LPO.lagda b/source/Taboos/LPO.lagda index 21b0c4d3a..fb3bf9ac7 100644 --- a/source/Taboos/LPO.lagda +++ b/source/Taboos/LPO.lagda @@ -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) @@ -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 ＝ ₁) @@ -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) @@ -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} @@ -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 = @@ -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 : ℕ∞ → ℕ + 𝟙 @@ -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) @@ -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} diff --git a/source/TypeTopology/ExtendedSumCompact.lagda b/source/TypeTopology/ExtendedSumCompact.lagda index aa842fb8d..800fecc50 100644 --- a/source/TypeTopology/ExtendedSumCompact.lagda +++ b/source/TypeTopology/ExtendedSumCompact.lagda @@ -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 @@ -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} diff --git a/source/TypeTopology/PropTychonoff.lagda b/source/TypeTopology/PropTychonoff.lagda index cfaa888ee..dfcea721b 100644 --- a/source/TypeTopology/PropTychonoff.lagda +++ b/source/TypeTopology/PropTychonoff.lagda @@ -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-ε = ε @@ -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} @@ -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 ⟩ ₁ ∎ @@ -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} @@ -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} diff --git a/source/TypeTopology/SigmaDiscreteAndTotallySeparated.lagda b/source/TypeTopology/SigmaDiscreteAndTotallySeparated.lagda index be8b3e0a5..3f67b9aff 100644 --- a/source/TypeTopology/SigmaDiscreteAndTotallySeparated.lagda +++ b/source/TypeTopology/SigmaDiscreteAndTotallySeparated.lagda @@ -160,10 +160,7 @@ separated types are closed under Σ. \begin{code} -module _ (fe : FunExt) where - - private - fe₀ = fe 𝓤₀ 𝓤₀ +module _ (fe₀ : funext 𝓤₀ 𝓤₀) where Σ-totally-separated-taboo : @@ -211,7 +208,7 @@ Even compact totally separated types fail to be closed under Σ: (τ ℕ∞ (λ u → u ＝ ∞ → 𝟚) (ℕ∞-compact fe₀) (λ _ → compact∙-types-are-compact - (prop-tychonoff fe (ℕ∞-is-set fe₀) (λ _ → 𝟚-is-compact∙))) + (prop-tychonoff fe₀ (ℕ∞-is-set fe₀) (λ _ → 𝟚-is-compact∙))) (ℕ∞-is-totally-separated fe₀) (λ u → Π-is-totally-separated fe₀ (λ _ → 𝟚-is-totally-separated)))