be more parsimonius with function extensionality universe levels

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)
 

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

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) → ⟨ Κ ν ⟩ → ⟨ 𝓢 ν ⟩

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}

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}

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}
 

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)))